[isabelle-dev] find_theorems and type class axioms

[Florian Haftmann]

Hi all,

> 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.

just to make sure.  The sort constraints of constants play *no* role for
searching theorems.  The sort constraints of terms to be searched *do*,
and in my view this is the desired behaviour:  if I formulate a property
on partial orders, I do not want to be bothered by facts which only
apply to linear orders.

I do not think find_theorems is to be blamed for the confusion
concerning dist_norm.  Instead, somebody a little bit familiar with the
topic has to find out why the sort constraints of norm are manipulated
in the way they are and whether there is room for improvement here.

Cheers,
	Florian

> 
> 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
> 

-- 

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/20151126/510de9ea/attachment.sig>