[isabelle-dev] Remaining uses of defer_recdef?

[Dmitriy Traytel]

Hi,

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 
seconds.

Dmitriy

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.
>
> 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
>
>
>
> _______________________________________________
> 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/095753e8/attachment-0002.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: no_recdef.patch
Type: text/x-patch
Size: 73121 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150607/095753e8/attachment-0002.bin>