[isabelle-dev] Abbreviations and find_theorems

[Gerwin Klein]

Right, thanks for setting me straight. This is less invasive than I thought.

So the remaining question is, are we happy with replacements like

 %x. Suc _ + x ~> Suc _ + _

and proper eta contraction. Both would return potentially more matches, but not fewer. For eta contraction, we can argue that Isabelle usually operates on eta-contracted terms anyway, so this behaviour shouldn’t be too surprising.

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?

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
>