Hi Larry and Florian,
the sort constraints for open, dist, and norm are changed in
http://isabelle.in.tum.de/repos/isabelle/file/e89cfc004f18/src/HOL/Real_Vector_Spaces.thy#l1218
These constraints were introduced by Brian Huffman in 2d91b2416de8 while he was reworking
the type class hierarchy for topological spaces in 2009. I do not know his reasons for
this, but I guess that they are meant to save type annotations.
Best,
Andreas
On 19/11/15 10:10, Florian Haftmann wrote:
Hi Larry,
Andreas’s message reminds me that axioms of type classes are still not
picked up:
class dist_norm = dist + norm + minus +
assumes dist_norm: "dist x y = norm (x - y)”
This item has the status of a theorem. However, the query
dist "norm(_-_)”
doesn’t find it. Surely it should?
my mail from this summer still applies:
There is nothing wrong with type classes here:
class involutory =
fixes f :: "'a ⇒ 'a"
assumes involutory: "f (f x) = x"
begin
lemma involutory3:
"f (f (f x)) = f x"
by (fact involutory)
end
find_theorems "f"
It seems to be a constraint issue:
find_theorems "_ = norm (_ - _)"
~> 'a::real_normed_vector is inferred
find_theorems "_ = norm ((_::'a::dist_norm) - _)"
~> typing error
Maybe some naughty tweaking of sort constraints or an unforseen
behaviour of coercions, but these are mere guesses. I do not understand
these parts of the type class hierarchy.
I do not know why and how the default constraints of »dist« are changed,
but this is the basic cause for the behaviour you experience.
Cheers,
Florian
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
