[isabelle-dev] Abbreviations and find_theorems
florian.haftmann at informatik.tu-muenchen.de
Thu Nov 27 08:36:33 CET 2014
> 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
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
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev