[isabelle-dev] Abbreviations and find_theorems

[Gerwin Klein]

Hi Florian,

I'm not worried about the eta conversion and am happy with your solution on that one.

The abstraction expansion worried me more, but since I seem to be the only one who makes use of crazy patterns that would benefit from it not being there, let's go with your solution there as well.

I'm happy for you to just push your proposal to the repo (I can do it as well if you prefer).

Cheers,
Gerwin

> On 04.12.2014, at 7:36 pm, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
>
>>> 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.
>
> Silence has fallen on this thread.  Let me put the matter into a more
> technical shape.
>
> As it is »by now«, search patterns in find_theorems are not matched
> modulo eta-conversion.
>
> I see two technical solutions to resolve this:
> a) Make the underlying pattern match implementation work modulo
> eta-conversion.
> b) Expand the search patterns themselves, as proposed above.
>
> Why I have been reluctant to implement a) is that this would complicate
> a potentially time-critical code.  Hence the more pragmatic solution b).
>
> So, which path is better to follow from now?  In case of doubt, we can
> choose b) and still later get back to it.
>
> 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


________________________________

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.