[isabelle-dev] find_theorems and type class axioms

[Manuel Eberl]

This particular issue has, in fact, annoyed me a great deal. I needed 
the ‘dist_norm’ lemma a lot lately and was never able to find it with 
‘find_theorems’, which was very frustrating. I eventually found it by 
reading a proof that used it somewhere.

I did not think much of it at the time, but I would very much like to 
see this resolved in some way if it is possible.


On 19/11/15 12:49, Lawrence Paulson wrote:
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev