<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">Hi,<br>
<br>
I could not believe that recdef could not be replaced by fun, so
here is the patch that removes usages of recdef from
Decision_Procs. The proof rules that come out of the function
package are fine (one just needs a few split_format (complete)
attributes in a few places).<br>
<br>
I'm not sure if this is something for the repository though, since
it has a factor of >2 impact on the build-time:<br>
<br>
recdef: Finished HOL-Decision_Procs (0:03:53 elapsed time, 0:13:26
cpu time, factor 3.45)<br>
fun : Finished HOL-Decision_Procs (0:08:24 elapsed time, 0:28:10
cpu time, factor 3.35)<br>
<br>
On the other hand 8 minutes is still not much. The longest fun
invocation (numadd in MIR) takes about 2 minutes, other are all
below 20 seconds.<br>
<br>
Dmitriy<br>
<br>
On 07.06.2015 07:18, Amine Chaieb wrote:<br>
</div>
<blockquote cite="mid:5573D422.9040601@chaieb.org" type="cite">
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
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 moz-do-not-send="true"
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 moz-do-not-send="true" 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 moz-do-not-send="true" class="moz-txt-link-abbreviated"
href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<br>
<a moz-do-not-send="true" 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 moz-do-not-send="true" class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a moz-do-not-send="true" 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>
<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>