[isabelle-dev] Abbreviations and find_theorems

[Gerwin Klein]

Hi Florian,

thanks for looking at that.

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 _`).

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

The behaviour should be that for proper constants, the pattern is left as specified by the user, and only for abbreviations it is expanded (because for abbreviations it will find nothing otherwise).

c61fe520602b looks like we had tried to solve this once before, and I remember that we discussed the two problems above at length. It seems the mechanism broke silently at some point and was forgotten. I wonder if it would be feasible to create a regression test for interactive commands like find_theorems so this noticed earlier, but that is a different topic.

Cheers,
Gerwin

> On 27.11.2014, at 05:40, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
>
> The following is based against 43e07797269b.  If you do not want apply
> the patched just copy find_theorems.ML to src/Pure/Tools.
>
> I merely implemented that patterns which are abstractions (after
> eta-contraction!) are implicitly expanded with schematic parameters.
>
> Hence
>
>  inj ~> %f. inj_on f UNIV ~> inj_on _ UNIV
>
> This seems a quite reasonable, generic approach to give semantics to
> search patterns.
>
> @Timothy: in the progress of investigating I stumbled over your
> changeset (c61fe520602b, actually brought in by Gerwin) and dismantled
> it.  Do you remember what it had been intended for resp. by which
> criterion we can decide whether the dismantling is really admissible?
> Before going ahead and pushing something, I would like to resolve this
> question.
>
> Thanks a lot,
>       Florian
>
> --
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> <find_theorems.txt><tuned_find.txt><find_revert.txt><find_eta.txt><find_theorems.ML>_______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.