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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
