[isabelle-dev] Remaining uses of defer_recdef?

[Dmitriy Traytel]

Hi Florian,

On 06.06.2015 17:11, Florian Haftmann 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?
I have some experience with the combinatorial explosion in fun. You 
don't need much: just take extended regular expressions (~10 
constructors) and define binary normalizing constructors (by some 
sequential pattern matching on both arguments). The AFP entry 
MSO_Regex_Equivalence is full of ~30 sec fun declarations.

While this is still on the edge of being bearable, try to add one more 
constructor... (I've seen examples where fun from 10 lines of 
specification produced something like 10^5 simp equations.) In a 
different formalization (AFP entry Formula_Derivatives) where I needed 
to have more then 10 constructors, I had to work around the function 
package by separating the datatype into two and defining the functions 
separately. (In the end, the separation had also positive effects, but 
still it felt like fighting the system when doing it.)

Note that the domain is quite similar to Cooper---syntactic 
manipulations of expressions/formulas---but isn't it what we do quite 
often in Isabelle? Orthogonally, I have no idea, whether recdef would 
have helped me.

Dmitriy