--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Aug 09 18:12:15 2001 +0200
@@ -5,7 +5,7 @@
\begin{isamarkuptext}%
\noindent
Now that we have learned about rules and logic, we take another look at the
-finer points of induction. The two questions we answer are: what to do if the
+finer points of induction. We consider two questions: what to do if the
proposition to be proved is not directly amenable to induction
(\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})
and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude
@@ -17,7 +17,7 @@
%
\begin{isamarkuptext}%
\label{sec:ind-var-in-prems}
-Often we have assumed that the theorem we want to prove is already in a form
+Often we have assumed that the theorem to be proved is already in a form
that is amenable to induction, but sometimes it isn't.
Here is an example.
Since \isa{hd} and \isa{last} return the first and last element of a
@@ -35,7 +35,7 @@
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%
\end{isabelle}
-After simplification, it becomes
+Simplification reduces the base case to this:
\begin{isabelle}
\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
\end{isabelle}
@@ -45,7 +45,7 @@
We should not have ignored the warning. Because the induction
formula is only the conclusion, induction does not affect the occurrence of \isa{xs} in the premises.
Thus the case that should have been trivial
-becomes unprovable. Fortunately, the solution is easy:\footnote{A very similar
+becomes unprovable. Fortunately, the solution is easy:\footnote{A similar
heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
\begin{quote}
\emph{Pull all occurrences of the induction variable into the conclusion
@@ -53,7 +53,7 @@
\end{quote}
Thus we should state the lemma as an ordinary
implication~(\isa{{\isasymlongrightarrow}}), letting
-\isa{rule{\isacharunderscore}format} (\S\ref{sec:forward}) convert the
+\attrdx{rule_format} (\S\ref{sec:forward}) convert the
result to the usual \isa{{\isasymLongrightarrow}} form:%
\end{isamarkuptxt}%
\isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}%
@@ -67,7 +67,7 @@
If there are multiple premises $A@1$, \dots, $A@n$ containing the
induction variable, you should turn the conclusion $C$ into
-\[ A@1 \longrightarrow \cdots A@n \longrightarrow C \]
+\[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \]
Additionally, you may also have to universally quantify some other variables,
which can yield a fairly complex conclusion. However, \isa{rule{\isacharunderscore}format}
can remove any number of occurrences of \isa{{\isasymforall}} and
@@ -75,15 +75,17 @@
\end{isamarkuptxt}%
%
\begin{isamarkuptext}%
+\index{induction!on a term}%
A second reason why your proposition may not be amenable to induction is that
-you want to induct on a whole term, rather than an individual variable. In
-general, when inducting on some term $t$ you must rephrase the conclusion $C$
+you want to induct on a complex term, rather than a variable. In
+general, induction on a term~$t$ requires rephrasing the conclusion~$C$
as
\begin{equation}\label{eqn:ind-over-term}
-\forall y@1 \dots y@n.~ x = t \longrightarrow C
+\forall y@1 \dots y@n.~ x = t \longrightarrow C.
\end{equation}
-where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and
-perform induction on $x$ afterwards. An example appears in
+where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.
+Now you can perform
+perform induction on~$x$. An example appears in
\S\ref{sec:complete-ind} below.
The very same problem may occur in connection with rule induction. Remember
@@ -91,7 +93,7 @@
some inductively defined set and the $x@i$ are variables. If instead we have
a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we
replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
-\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \]
+\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C. \]
For an example see \S\ref{sec:CTL-revisited} below.
Of course, all premises that share free variables with $t$ need to be pulled into
@@ -127,13 +129,14 @@
be helpful. We show how to apply such induction schemas by an example.
Structural induction on \isa{nat} is
-usually known as mathematical induction. There is also \emph{complete}
-induction, where you must prove $P(n)$ under the assumption that $P(m)$
-holds for all $m<n$. In Isabelle, this is the theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}:
+usually known as mathematical induction. There is also \textbf{complete}
+\index{induction!complete}%
+induction, where you prove $P(n)$ under the assumption that $P(m)$
+holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}:
\begin{isabelle}%
\ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
\end{isabelle}
-As an example of its application we prove a property of the following
+As an application, we prove a property of the following
function:%
\end{isamarkuptext}%
\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
@@ -162,7 +165,7 @@
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-which leaves us with the following proof state:
+We get the following proof state:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ }{\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
@@ -204,13 +207,12 @@
which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by
\isa{le{\isacharunderscore}less{\isacharunderscore}trans}).
-This last step shows both the power and the danger of automatic proofs: they
-will usually not tell you how the proof goes, because it can be very hard to
-translate the internal proof into a human-readable format. Therefore
-Chapter~\ref{sec:part2?} introduces a language for writing readable
-proofs.
+This last step shows both the power and the danger of automatic proofs. They
+will usually not tell you how the proof goes, because it can be hard to
+translate the internal proof into a human-readable format. Automatic
+proofs are easy to write but hard to read and understand.
-We can now derive the desired \isa{i\ {\isasymle}\ f\ i} from \isa{f{\isacharunderscore}incr{\isacharunderscore}lem}:%
+The desired result, \isa{i\ {\isasymle}\ f\ i}, follows from \isa{f{\isacharunderscore}incr{\isacharunderscore}lem}:%
\end{isamarkuptext}%
\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}%
\begin{isamarkuptext}%
@@ -255,11 +257,12 @@
%
\begin{isamarkuptext}%
\label{sec:derive-ind}
+\index{induction!deriving new schemas}%
Induction schemas are ordinary theorems and you can derive new ones
-whenever you wish. This section shows you how to, using the example
+whenever you wish. This section shows you how, using the example
of \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}. Assume we only have structural induction
-available for \isa{nat} and want to derive complete induction. This
-requires us to generalize the statement first:%
+available for \isa{nat} and want to derive complete induction. We
+must generalize the statement as shown:%
\end{isamarkuptext}%
\isacommand{lemma}\ induct{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}%
@@ -288,7 +291,7 @@
\isacommand{theorem}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
\isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
\begin{isamarkuptext}%
-Finally we should remind the reader that HOL already provides the mother of
+HOL already provides the mother of
all inductions, well-founded induction (see \S\ref{sec:Well-founded}). For
example theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} is
a special case of \isa{wf{\isacharunderscore}induct} where \isa{r} is \isa{{\isacharless}} on