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
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
