[isabelle-dev] Abbreviations and find_theorems

[Florian Haftmann]

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

-------------- 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/56bf2cad/attachment.sig>