--- a/doc-src/TutorialI/Advanced/document/Partial.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Thu Aug 09 18:12:15 2001 +0200
@@ -3,8 +3,8 @@
\def\isabellecontext{Partial}%
%
\begin{isamarkuptext}%
-\noindent Throughout the tutorial we have emphasized the fact
-that all functions in HOL are total. Hence we cannot hope to define
+\noindent Throughout this tutorial, we have emphasized
+that all functions in HOL are total. We cannot hope to define
truly partial functions, but must make them total. A straightforward
method is to lift the result type of the function from $\tau$ to
$\tau$~\isa{option} (see \ref{sec:option}), where \isa{None} is
@@ -47,6 +47,7 @@
}
%
\begin{isamarkuptext}%
+\index{recursion!guarded}%
Neither \isacommand{primrec} nor \isacommand{recdef} allow to
prefix an equation with a condition in the way ordinary definitions do
(see \isa{minus} above). Instead we have to move the condition over
@@ -76,7 +77,7 @@
As a more substantial example we consider the problem of searching a graph.
For simplicity our graph is given by a function \isa{f} of
type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} which
-maps each node to its successor, i.e.\ the graph is really a tree.
+maps each node to its successor; the graph is really a tree.
The task is to find the end of a chain, modelled by a node pointing to
itself. Here is a first attempt:
\begin{isabelle}%
@@ -126,19 +127,19 @@
argument stays unchanged and the second one descends along \isa{step{\isadigit{1}}\ f}. The proof requires unfolding the definition of \isa{step{\isadigit{1}}},
as specified in the \isacommand{hints} above.
-Normally you will then derive the following conditional variant of and from
-the recursion equation%
+Normally you will then derive the following conditional variant from
+the recursion equation:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{by}\ simp%
\begin{isamarkuptext}%
-\noindent and then disable the original recursion equation:%
+\noindent Then you should disable the original recursion equation:%
\end{isamarkuptext}%
\isacommand{declare}\ find{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}%
\begin{isamarkuptext}%
-We can reason about such underdefined functions just like about any other
-recursive function. Here is a simple example of recursion induction:%
+Reasoning about such underdefined functions is like that for other
+recursive functions. Here is a simple example of recursion induction:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymlongrightarrow}\ f{\isacharparenleft}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}find{\isachardot}induct{\isacharparenright}\isanewline
@@ -162,8 +163,8 @@
\begin{verbatim}
x := s; while b(x) do x := c(x); return x
\end{verbatim}
-In general, \isa{s} will be a tuple (better still: a record). As an example
-consider the following definition of function \isa{find} above:%
+In general, \isa{s} will be a tuple or record. As an example
+consider the following definition of function \isa{find}:%
\end{isamarkuptext}%
\isacommand{constdefs}\ find{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}find{\isadigit{2}}\ f\ x\ {\isasymequiv}\isanewline
@@ -178,7 +179,7 @@
Although the definition of tail recursive functions via \isa{while} avoids
termination proofs, there is no free lunch. When proving properties of
functions defined by \isa{while}, termination rears its ugly head
-again. Here is \isa{while{\isacharunderscore}rule}, the well known proof rule for total
+again. Here is \tdx{while_rule}, the well known proof rule for total
correctness of loops expressed with \isa{while}:
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline
@@ -214,7 +215,7 @@
\begin{isamarkuptext}%
Let us conclude this section on partial functions by a
discussion of the merits of the \isa{while} combinator. We have
-already seen that the advantage (if it is one) of not having to
+already seen that the advantage of not having to
provide a termination argument when defining a function via \isa{while} merely puts off the evil hour. On top of that, tail recursive
functions tend to be more complicated to reason about. So why use
\isa{while} at all? The only reason is executability: the recursion