[isabelle-dev] Abbreviations and find_theorems

[Florian Haftmann]

> The abstraction expansion would basically mean you can’t search for abstractions at all any more. I.e. even something like (%_. _) would be expanded into (_ _). That’s not necessarily catastrophic, but probably counter-intuitive.
> 
> Has anyone apart from me ever searched for an abstraction that was not an abbreviation? If yes, why?

Well, there are parts of the system without implicit eta-conversion, and
some with.  I personally would not bother about find patterns working
modulo eta-conversion implicitly.

	Florian

> 
> Cheers,
> Gerwin
> 
>> On 27.11.2014, at 18:36, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
>>
>> Hi Gerwin,
>>
>>> Do I read find_eta.txt right that the eta expansion is applied to all
>> patterns? If yes, then that is a problem, because now partially applied
>> constants won’t be found any more (i.e. the occurrence of `Suc` in `map
>> Suc ?xs` would be missed if you make it always search for `Suc _`).
>>
>> It is not eta-expansion.  It is an expansion of abstractions, e.g.
>>
>> 	%f. inj_on f UNIV ~> inj_on _ UNIV
>>
>> but not
>>
>> 	Suc ~/~> Suc _
>>
>>> Also, always eta-contracting the pattern is not necessarily a good idea.
>>> The user might have specifically used the non-contracted form to exclude matches she is not interested in
>>> (e.g. might specifically not want `map Suc ?xs`).
>>
>> It is proper eta-contraction and thus only affecting abstractions.  E.g.
>>
>> 	%n. Suc n ~> Suc
>>
>> but not
>>
>> 	Suc _ ~/~> Suc
>>
>> I played a little bit in my head with the semantic consequences and
>> judged them quite consistent and convenient.  But maybe I have
>> overlooked significant counterexamples.
>>
>> Cheers,
>> 	Florian
>>
>> -- 
>>
>> PGP available:
>> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>>
> 
> _______________________________________________
> 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: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141127/9866b176/attachment.sig>