<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
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.<br>
<br>
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).<br>
<br>
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.<br>
<br>
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).<br>
<br>
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.<br>
<br>
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.<br>
<br>
Amine.<br>
<br>
<br>
<div class="moz-cite-prefix">On 06/06/2015 08:37 PM, Tobias Nipkow
wrote:<br>
</div>
<blockquote cite="mid:55733DF7.2090208@in.tum.de" type="cite">
<br>
<br>
On 06/06/2015 20:11, Larry Paulson wrote:
<br>
<blockquote type="cite">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?
<br>
</blockquote>
<br>
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.
<br>
<br>
Tobias
<br>
<br>
<blockquote type="cite">Larry
<br>
<br>
<blockquote type="cite">On 6 Jun 2015, at 16:11, Florian
Haftmann <a class="moz-txt-link-rfc2396E" href="mailto:florian.haftmann@informatik.tu-muenchen.de"><florian.haftmann@informatik.tu-muenchen.de></a>
wrote:
<br>
<br>
<blockquote type="cite">The reason for the continued existence
of recdef is that function can
<br>
cause a combinatorial explosion the way it compiles pattern
matches. I
<br>
just tried Cooper.thy and changing one of the recdefs to
function makes
<br>
Isabelle go blue (purple) in the face until one gives up.
Hardware alone
<br>
will not solve that one.
<br>
<br>
Now one could argue that since we need recdef, we should
also keep the
<br>
special variant defer_recdef, but if nobody speaks up for
it, we don't
<br>
have a proof that we really need it and it should go.
<br>
</blockquote>
<br>
At the time of their writing the recdef examples in (nowadays)
<br>
src/HOL/Decision_Procs were the power applications of their
times.
<br>
<br>
Since then power applications have grown bigger and bigger and
<br>
fun/function have been used widespread. It seems strange to
me that no
<br>
application since then had never hit the same concrete wall
again.
<br>
<br>
So are there any experience reports that the combinatorial
explosion in
<br>
pattern matching in fun/function had to be worked around
somehow? Or do
<br>
we have to conclude that the pattern complexity of the
applications in
<br>
src/HOL/Decision_Procs is indeed domain-specific?
<br>
<br>
Florian
<br>
<br>
--
<br>
<br>
PGP available:
<br>
<a class="moz-txt-link-freetext" href="http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de">http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de</a>
<br>
<br>
_______________________________________________
<br>
isabelle-dev mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<br>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
<br>
</blockquote>
<br>
</blockquote>
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>