On 06/06/2015 20:11, Larry Paulson wrote:
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?
You can always turn all patterns of the lhs into cases on the rhs and derive the individual equations as lemmas. You also need to derive an induction principle. I would rather keep recdef than do all that by hand.
Tobias
LarryOn 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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
