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.23 +Now we return to the initial definition of \texttt{term} using
    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}