author nipkow Tue, 21 Sep 1999 19:10:39 +0200 changeset 7569 1d9263172b54 parent 7568 436c87ac2fac child 7570 a9391550eea1
?
 doc-src/Tutorial/fp.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Tutorial/fp.tex	Tue Sep 21 19:05:38 1999 +0200
+++ b/doc-src/Tutorial/fp.tex	Tue Sep 21 19:10:39 1999 +0200
@@ -569,7 +569,7 @@
is explained in \S\ref{sec:InductionHeuristics}

\begin{exercise}
-  We strengthen the definition of a {\em normal\/} If-expression as follows:
+  We strengthen the definition of a \texttt{normal} If-expression as follows:
the first argument of all \texttt{IF}s must be a variable. Adapt the above
development to this changed requirement. (Hint: you may need to formulate
some of the goals as implications (\texttt{-->}) rather than equalities
@@ -1399,11 +1399,9 @@
would be something like
\begin{ttbox}
\input{Datatype/tunfoldeddata}\end{ttbox}
-Although we do not recommend this unfolding to the user, this is how Isabelle
-deals with nested recursion internally. Strictly speaking, this information
-is irrelevant at the user level (and might change in the future), but it
-motivates why \texttt{primrec} and induction work for nested types the way
-they do. We now return to the initial definition of \texttt{term} using
+Although we do not recommend this unfolding to the user, it shows how to
+simulate nested recursion by mutual recursion.
nested recursion.

Let us define a substitution function on terms. Because terms involve term
@@ -1437,14 +1435,14 @@
definition is found in the theorem \texttt{o_def}).
\end{exercise}

-If you feel that the \texttt{App}-equation in the definition of substitution
-is overly complicated, you are right: the simpler
+Returning to the definition of \texttt{subst}, we have to admit that it does
+not really need the auxiliary \texttt{substs} function. The \texttt{App}-case
+can directly be expressed as
\begin{ttbox}
\input{Datatype/appmap}\end{ttbox}
-would have done the job. Unfortunately, Isabelle insists on the more verbose
-equation given above. Nevertheless, we can easily {\em prove} that the
-\texttt{map}-equation holds: simply by induction on \texttt{ts} followed by
-\texttt{Auto_tac}.
+Although Isabelle insists on the more verbose version, we can easily {\em
+  prove} that the \texttt{map}-equation holds: simply by induction on
+\texttt{ts} followed by \texttt{Auto_tac}.

%FIXME: forward pointer to section where better induction principles are
%derived?
@@ -1467,8 +1465,8 @@

How far can we push nested recursion? By the unfolding argument above, we can
reduce nested to mutual recursion provided the nested recursion only involves
-previously defined datatypes. Isabelle is a bit more generous and also permits
-products as in the \texttt{data} example above.
+previously defined datatypes. The \texttt{data} example above involves
+products, which is fine because products are also datatypes.
However, functions are most emphatically not allowed:
\begin{ttbox}
datatype t = C (t => bool)
@@ -1649,7 +1647,7 @@
this is not always the case. Arbitrary total recursive functions can be
defined by means of \texttt{recdef}: you can use full pattern-matching,
recursion need not involve datatypes, and termination is proved by showing
-that each recursive call makes the argument smaller in a suitable (user
+that the arguments of all recursive calls are smaller in a suitable (user
supplied) sense.

\subsection{Defining recursive functions}