[isabelle-dev] Remaining uses of defer_recdef?

[Amine Chaieb]

I remember trying to convert Cooper's as well as other Decision proc's 
recdefs to fun, also with the help of Alex but gave up at some point.

I think the killer at the time was rather the induction principle and 
not the simp rules. The one derived by recdef really fits the definition 
and "spirit" of development. Also runtime at the time was not 
acceptable. I also remember havin the runtime problem with fun vs. 
primrec (so we left those there too).

   Context: Deep embedding of datatype + normal form on this data type + 
set of recursive functions on syntax preserving normal form. The normal 
Form has conditions on nested patterns --> introduce new constructor for 
these common nested patterns in normal form.

We had combinatorial explosion due to the depth of the patterns (which 
is the main reason to introduce special constructors in the datatype, to 
reduce deep patterns).

The induction priciples with recdef really fitted, i.e. induct auto with 
spice did the job for lemmas you do not expect to spend time thinking as 
a software developer.

One could argue that one should introduce a new data type for normalized 
syntactic elements and perform such computations as needed. I dismissed 
this idea and did not explore it, since it comes with a high price. 
Perhaps there are better ways to do the formalization.

Amine.


On 06/06/2015 08:37 PM, Tobias Nipkow wrote:
>
>
> 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 
>>>
>>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150607/37022c2e/attachment-0002.html>