>> 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.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
