[isabelle-dev] Remaining uses of defer_recdef?
florian.haftmann at informatik.tu-muenchen.de
Sun Jun 7 21:29:21 CEST 2015
>> 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.)
OK, the dragons are still there and not just a historic relic.
> 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.
I would definitely not suggest to use recdef for any new application…
the open question is whether we have to think about a refinement or
extension of function.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev