author | nipkow |

Tue Sep 21 19:10:39 1999 +0200 (1999-09-21 ago) | |

changeset 7569 | 1d9263172b54 |

parent 7568 | 436c87ac2fac |

child 7570 | a9391550eea1 |

?

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}