[isabelle-dev] find_theorems and type class axioms

[Lawrence Paulson]

I had no idea that sort constraints played any role in the finding of theorems, or why they should play a role. Whatever function they have in a search doesn’t prevent the very similar query

	dist norm "op=“

from picking up quite a few things. To my mind it’s quite unintuitive and maybe should be looked at again.

Larry

> On 19 Nov 2015, at 09:21, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
> 
> 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