[isabelle-dev] Remaining uses of defer_recdef?
traytel at in.tum.de
Sun Jun 7 08:38:15 CEST 2015
I could not believe that recdef could not be replaced by fun, so here is
the patch that removes usages of recdef from Decision_Procs. The proof
rules that come out of the function package are fine (one just needs a
few split_format (complete) attributes in a few places).
I'm not sure if this is something for the repository though, since it
has a factor of >2 impact on the build-time:
recdef: Finished HOL-Decision_Procs (0:03:53 elapsed time, 0:13:26 cpu
time, factor 3.45)
fun : Finished HOL-Decision_Procs (0:08:24 elapsed time, 0:28:10 cpu
time, factor 3.35)
On the other hand 8 minutes is still not much. The longest fun
invocation (numadd in MIR) takes about 2 minutes, other are all below 20
On 07.06.2015 07:18, Amine Chaieb wrote:
> 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.
> 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
>>>> 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
>>>>> Isabelle go blue (purple) in the face until one gives up. Hardware
>>>>> will not solve that one.
>>>>> Now one could argue that since we need recdef, we should also keep
>>>>> special variant defer_recdef, but if nobody speaks up for it, we
>>>>> 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?
>>>> PGP available:
>>>> isabelle-dev mailing list
>>>> isabelle-dev at in.tum.de
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An HTML attachment was scrubbed...
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 73121 bytes
Desc: not available
More information about the isabelle-dev