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? Larry
> On 6 Jun 2015, at 16:11, Florian Haftmann > <florian.haftm...@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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
