[isabelle-dev] Remaining uses of defer_recdef?

[Tobias Nipkow]

On 06/06/2015 20:11, Larry Paulson wrote:
> Pattern matching is a convenience, and can always be eliminated manually. Is there really no reasonable way to re-express the definitions in Cooper.thy?

You can always turn all patterns of the lhs into cases on the rhs and derive the 
individual equations as lemmas. You also need to derive an induction principle. 
I would rather keep recdef than do all that by hand.

Tobias

> Larry
>
>> On 6 Jun 2015, at 16:11, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
>>
>>> The reason for the continued existence of recdef is that function can
>>> cause a combinatorial explosion the way it compiles pattern matches. I
>>> just tried Cooper.thy and changing one of the recdefs to function makes
>>> Isabelle go blue (purple) in the face until one gives up. Hardware alone
>>> will not solve that one.
>>>
>>> Now one could argue that since we need recdef, we should also keep the
>>> special variant defer_recdef, but if nobody speaks up for it, we don't
>>> have a proof that we really need it and it should go.
>>
>> At the time of their writing the recdef examples in (nowadays)
>> src/HOL/Decision_Procs were the power applications of their times.
>>
>> Since then power applications have grown bigger and bigger and
>> fun/function have been used widespread.  It seems strange to me that no
>> application since then had never hit the same concrete wall again.
>>
>> So are there any experience reports that the combinatorial explosion in
>> pattern matching in fun/function had to be worked around somehow?  Or do
>> we have to conclude that the pattern complexity of the applications in
>> src/HOL/Decision_Procs is indeed domain-specific?
>>
>> 	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
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5112 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150606/66d84f63/attachment.bin>