[isabelle-dev] find_theorems and type class axioms

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151119/c056db7a/attachment.sig>