[isabelle-dev] find_theorems and type class axioms

[Gerwin Klein]

I agree, we should do something about it.

All relevant people on our side currently are pretty busy with a project deliverable for 1st Dec, but we should be able to give find_theorems some of the TLC it deserves after that.

This may not be easy to solve - it probably is just how matching/unification plays out, but we’ll see what we can do.

Cheers,
Gerwin

> On 19 Nov 2015, at 10:57 pm, Manuel Eberl <eberlm at in.tum.de> wrote:
>
> 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
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.