[isabelle-dev] find_theorems and type class axioms

[Andreas Lochbihler]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>