doc-src/Tutorial/fp.tex
 changeset 7569 1d9263172b54 parent 6691 8a1b5f9d8420 child 7587 ee0b835ca8fa
     1.1 --- a/doc-src/Tutorial/fp.tex	Tue Sep 21 19:05:38 1999 +0200
1.2 +++ b/doc-src/Tutorial/fp.tex	Tue Sep 21 19:10:39 1999 +0200
1.3 @@ -569,7 +569,7 @@
1.4  is explained in \S\ref{sec:InductionHeuristics}
1.5
1.6  \begin{exercise}
1.7 -  We strengthen the definition of a {\em normal\/} If-expression as follows:
1.8 +  We strengthen the definition of a \texttt{normal} If-expression as follows:
1.9    the first argument of all \texttt{IF}s must be a variable. Adapt the above
1.10    development to this changed requirement. (Hint: you may need to formulate
1.11    some of the goals as implications (\texttt{-->}) rather than equalities
1.12 @@ -1399,11 +1399,9 @@
1.13  would be something like
1.14  \begin{ttbox}
1.15  \input{Datatype/tunfoldeddata}\end{ttbox}
1.16 -Although we do not recommend this unfolding to the user, this is how Isabelle
1.17 -deals with nested recursion internally. Strictly speaking, this information
1.18 -is irrelevant at the user level (and might change in the future), but it
1.19 -motivates why \texttt{primrec} and induction work for nested types the way
1.20 -they do. We now return to the initial definition of \texttt{term} using
1.21 +Although we do not recommend this unfolding to the user, it shows how to
1.22 +simulate nested recursion by mutual recursion.
1.24  nested recursion.
1.25
1.26  Let us define a substitution function on terms. Because terms involve term
1.27 @@ -1437,14 +1435,14 @@
1.28  definition is found in the theorem \texttt{o_def}).
1.29  \end{exercise}
1.30
1.31 -If you feel that the \texttt{App}-equation in the definition of substitution
1.32 -is overly complicated, you are right: the simpler
1.33 +Returning to the definition of \texttt{subst}, we have to admit that it does
1.34 +not really need the auxiliary \texttt{substs} function. The \texttt{App}-case
1.35 +can directly be expressed as
1.36  \begin{ttbox}
1.37  \input{Datatype/appmap}\end{ttbox}
1.38 -would have done the job. Unfortunately, Isabelle insists on the more verbose
1.39 -equation given above. Nevertheless, we can easily {\em prove} that the
1.40 -\texttt{map}-equation holds: simply by induction on \texttt{ts} followed by
1.41 -\texttt{Auto_tac}.
1.42 +Although Isabelle insists on the more verbose version, we can easily {\em
1.43 +  prove} that the \texttt{map}-equation holds: simply by induction on
1.44 +\texttt{ts} followed by \texttt{Auto_tac}.
1.45
1.46  %FIXME: forward pointer to section where better induction principles are
1.47  %derived?
1.48 @@ -1467,8 +1465,8 @@
1.49
1.50  How far can we push nested recursion? By the unfolding argument above, we can
1.51  reduce nested to mutual recursion provided the nested recursion only involves
1.52 -previously defined datatypes. Isabelle is a bit more generous and also permits
1.53 -products as in the \texttt{data} example above.
1.54 +previously defined datatypes. The \texttt{data} example above involves
1.55 +products, which is fine because products are also datatypes.
1.56  However, functions are most emphatically not allowed:
1.57  \begin{ttbox}
1.58  datatype t = C (t => bool)
1.59 @@ -1649,7 +1647,7 @@
1.60  this is not always the case. Arbitrary total recursive functions can be
1.61  defined by means of \texttt{recdef}: you can use full pattern-matching,
1.62  recursion need not involve datatypes, and termination is proved by showing
1.63 -that each recursive call makes the argument smaller in a suitable (user
1.64 +that the arguments of all recursive calls are smaller in a suitable (user
1.65  supplied) sense.
1.66
1.67  \subsection{Defining recursive functions}