author nipkow Fri, 31 Mar 2000 10:08:26 +0200 changeset 8628 b3d9d8446473 parent 8627 44ec33bb5c5b child 8629 c3d90724abcc
updated recdef
 doc-src/HOL/HOL.tex file | annotate | diff | comparison | revisions
--- a/doc-src/HOL/HOL.tex	Thu Mar 30 21:26:10 2000 +0200
+++ b/doc-src/HOL/HOL.tex	Fri Mar 31 10:08:26 2000 +0200
@@ -2703,17 +2703,15 @@
$f$ is defined by pattern-matching on components of its argument whose type
is a \texttt{datatype}.

-  Unlike with \texttt{primrec}, the reduction rules are not added to the
-  default simpset, and individual rules may not be labelled with identifiers.
-  However, the identifier $f$\texttt{.rules} is visible at the \ML\ level
-  as a list of theorems.
+  The \ML\ identifier $f$\texttt{.simps} contains the reduction rules as
+  a list of theorems.
\end{itemize}

With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to
prove one termination condition.  It remains as a precondition of the
-recursion theorems.
+recursion theorems:
\begin{ttbox}
-gcd.rules;
+gcd.simps;
{\out ["! m n. n ~= 0 --> m mod n < n}
{\out   ==> gcd (?m, ?n) = (if ?n = 0 then ?m else gcd (?n, ?m mod ?n))"] }
{\out : thm list}
@@ -2721,17 +2719,17 @@
The theory \texttt{HOL/ex/Primes} illustrates how to prove termination
conditions afterwards.  The function \texttt{Tfl.tgoalw} is like the standard
function \texttt{goalw}, which sets up a goal to prove, but its argument
-should be the identifier $f$\texttt{.rules} and its effect is to set up a
+should be the identifier $f$\texttt{.simps} and its effect is to set up a
proof of the termination conditions:
\begin{ttbox}
-Tfl.tgoalw thy [] gcd.rules;
+Tfl.tgoalw thy [] gcd.simps;
{\out Level 0}
{\out ! m n. n ~= 0 --> m mod n < n}
{\out  1. ! m n. n ~= 0 --> m mod n < n}
\end{ttbox}
This subgoal has a one-step proof using \texttt{simp_tac}.  Once the theorem
is proved, it can be used to eliminate the termination conditions from
-elements of \texttt{gcd.rules}.  Theory \texttt{HOL/Subst/Unify} is a much
+elements of \texttt{gcd.simps}.  Theory \texttt{HOL/Subst/Unify} is a much
more complicated example of this process, where the termination conditions can
only be proved by complicated reasoning involving the recursive function
itself.
@@ -2744,6 +2742,16 @@
"gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
\end{ttbox}

+If all termination conditions were proved automatically, $f$\texttt{.simps}
+is added to the simpset automatically, just as in \texttt{primrec}.
+The simplification rules corresponding to clause $i$ (where counting starts
+at 0) are called $f$\texttt{.}$i$ and can be accessed as \texttt{thms
+  "$f$.$i$"},
+which returns a list of theorems. Thus you can, for example, remove specific
+clauses from the simpset. Note that a single clause may give rise to a set of
+simplification rules in order to capture the fact that if clauses overlap,
+their order disambiguates them.
+
A \texttt{recdef} definition also returns an induction rule specialised for
the recursive function.  For the \texttt{gcd} function above, the induction
rule is