I remember trying to convert Cooper's as well as other Decision proc's
recdefs to fun, also with the help of Alex but gave up at some point.
I think the killer at the time was rather the induction principle and
not the simp rules. The one derived by recdef really fits the definition
and "spirit" of development. Also runtime at the time was not
acceptable. I also remember havin the runtime problem with fun vs.
primrec (so we left those there too).
Context: Deep embedding of datatype + normal form on this data type +
set of recursive functions on syntax preserving normal form. The normal
Form has conditions on nested patterns --> introduce new constructor for
these common nested patterns in normal form.
We had combinatorial explosion due to the depth of the patterns (which
is the main reason to introduce special constructors in the datatype, to
reduce deep patterns).
The induction priciples with recdef really fitted, i.e. induct auto with
spice did the job for lemmas you do not expect to spend time thinking as
a software developer.
One could argue that one should introduce a new data type for normalized
syntactic elements and perform such computations as needed. I dismissed
this idea and did not explore it, since it comes with a high price.
Perhaps there are better ways to do the formalization.
Amine.
On 06/06/2015 08:37 PM, Tobias Nipkow wrote:
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
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
