diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Fri Jan 12 16:07:20 2001 +0100
@@ -12,21 +12,22 @@
 with an extended example of induction (\S\ref{sec:CTL-revisited}).%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Massaging the proposition%
+\isamarkupsubsection{Massaging the Proposition%
 }
 %
 \begin{isamarkuptext}%
 \label{sec:ind-var-in-prems}
-So far we have assumed that the theorem we want to prove is already in a form
-that is amenable to induction, but this is not always the case:%
+Often we have assumed that the theorem we want to prove 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
+non-empty list, this lemma looks easy to prove:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
-(where \isa{hd} and \isa{last} return the first and last element of a
-non-empty list)
-produces the warning
+But induction produces the warning
 \begin{quote}\tt
 Induction variable occurs also among premises!
 \end{quote}
@@ -34,74 +35,52 @@
 \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%
 \end{isabelle}
-which, after simplification, becomes
+After simplification, it becomes
 \begin{isabelle}
 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
 \end{isabelle}
 We cannot prove this equality because we do not know what \isa{hd} and
 \isa{last} return when applied to \isa{{\isacharbrackleft}{\isacharbrackright}}.
 
-The point is that we have violated the above warning. Because the induction
-formula is only the conclusion, the occurrence of \isa{xs} in the premises is
-not modified by induction. Thus the case that should have been trivial
+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
 heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
 \begin{quote}
 \emph{Pull all occurrences of the induction variable into the conclusion
 using \isa{{\isasymlongrightarrow}}.}
 \end{quote}
-This means we should prove%
+Thus we should state the lemma as an ordinary 
+implication~(\isa{{\isasymlongrightarrow}}), letting
+\isa{rule{\isacharunderscore}format} (\S\ref{sec:forward}) convert the
+result to the usual \isa{{\isasymLongrightarrow}} form:%
 \end{isamarkuptxt}%
-\isacommand{lemma}\ hd{\isacharunderscore}rev{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}%
+\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}%
 \begin{isamarkuptxt}%
 \noindent
-This time, induction leaves us with the following base case
+This time, induction leaves us with a trivial base case:
 \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%
 \end{isabelle}
-which is trivial, and \isa{auto} finishes the whole proof.
-
-If \isa{hd{\isacharunderscore}rev} is meant to be a simplification rule, you are
-done. But if you really need the \isa{{\isasymLongrightarrow}}-version of
-\isa{hd{\isacharunderscore}rev}, for example because you want to apply it as an
-introduction rule, you need to derive it separately, by combining it with
-modus ponens:%
+And \isa{auto} completes the proof.%
 \end{isamarkuptxt}%
-\isacommand{lemmas}\ hd{\isacharunderscore}revI\ {\isacharequal}\ hd{\isacharunderscore}rev{\isacharbrackleft}THEN\ mp{\isacharbrackright}%
+%
 \begin{isamarkuptext}%
-\noindent
-which yields the lemma we originally set out to prove.
-
-In case there are multiple premises $A@1$, \dots, $A@n$ containing the
+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 \]
 (see the remark?? in \S\ref{??}).
 Additionally, you may also have to universally quantify some other variables,
-which can yield a fairly complex conclusion.
+which can yield a fairly complex conclusion.  However, \isa{rule{\isacharunderscore}format} 
+can remove any number of occurrences of \isa{{\isasymforall}} and
+\isa{{\isasymlongrightarrow}}.
+
 Here is a simple example (which is proved by \isa{blast}):%
 \end{isamarkuptext}%
-\isacommand{lemma}\ simple{\isacharcolon}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymand}\ A\ y{\isachardoublequote}%
-\begin{isamarkuptext}%
-\noindent
-You can get the desired lemma by explicit
-application of modus ponens and \isa{spec}:%
-\end{isamarkuptext}%
-\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}THEN\ spec{\isacharcomma}\ THEN\ mp{\isacharcomma}\ THEN\ mp{\isacharbrackright}%
+\isacommand{lemma}\ simple{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymand}\ A\ y{\isachardoublequote}%
 \begin{isamarkuptext}%
-\noindent
-or the wholesale stripping of \isa{{\isasymforall}} and
-\isa{{\isasymlongrightarrow}} in the conclusion via \isa{rule{\isacharunderscore}format}%
-\end{isamarkuptext}%
-\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}%
-\begin{isamarkuptext}%
-\noindent
-yielding \isa{{\isasymlbrakk}A\ y{\isacharsemicolon}\ B\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ B\ y\ {\isasymand}\ A\ y}.
-You can go one step further and include these derivations already in the
-statement of your original lemma, thus avoiding the intermediate step:%
-\end{isamarkuptext}%
-\isacommand{lemma}\ myrule{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymand}\ A\ y{\isachardoublequote}%
-\begin{isamarkuptext}%
-\bigskip
+\medskip
 
 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
@@ -124,21 +103,21 @@
 the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Beyond structural and recursion induction%
+\isamarkupsubsection{Beyond Structural and Recursion Induction%
 }
 %
 \begin{isamarkuptext}%
 \label{sec:complete-ind}
-So far, inductive proofs where by structural induction for
+So far, inductive proofs were by structural induction for
 primitive recursive functions and recursion induction for total recursive
 functions. But sometimes structural induction is awkward and there is no
-recursive function in sight either that could furnish a more appropriate
-induction schema. In such cases some existing standard induction schema can
+recursive function that could furnish a more appropriate
+induction schema. In such cases a general-purpose induction schema can
 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 ``complete
-induction'', where you must prove $P(n)$ under the assumption that $P(m)$
+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}:
 \begin{isabelle}%
 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
@@ -149,11 +128,7 @@
 \isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-From the above axiom\footnote{In general, the use of axioms is strongly
-discouraged, because of the danger of inconsistencies. The above axiom does
-not introduce an inconsistency because, for example, the identity function
-satisfies it.}
-for \isa{f} it follows that \isa{n\ {\isasymle}\ f\ n}, which can
+The axiom for \isa{f} implies \isa{n\ {\isasymle}\ f\ n}, which can
 be proved by induction on \isa{f\ n}. Following the recipe outlined
 above, we have to phrase the proposition as follows to allow induction:%
 \end{isamarkuptext}%
@@ -189,14 +164,23 @@
 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
-It is not surprising if you find the last step puzzling.
+If you find the last step puzzling, here are the 
+two other lemmas used above:
+\begin{isabelle}
+\isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}
+\rulename{Suc_leI}\isanewline
+\isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}
+\rulename{le_less_trans}
+\end{isabelle}
+%
 The proof goes like this (writing \isa{j} instead of \isa{nat}).
 Since \isa{i\ {\isacharequal}\ Suc\ j} it suffices to show
-\isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (by \isa{Suc{\isacharunderscore}leI}: \isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}). This is
+\hbox{\isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}},
+by \isa{Suc{\isacharunderscore}leI}\@.  This is
 proved as follows. From \isa{f{\isacharunderscore}ax} we have \isa{f\ {\isacharparenleft}f\ j{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}
-(1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} (by the induction hypothesis).
-Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by transitivity
-(\isa{le{\isacharunderscore}less{\isacharunderscore}trans}: \isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}).
+(1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} by the induction hypothesis.
+Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by the transitivity
+rule \isa{le{\isacharunderscore}less{\isacharunderscore}trans}.
 Using the induction hypothesis once more we obtain \isa{j\ {\isasymle}\ f\ j}
 which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by
 \isa{le{\isacharunderscore}less{\isacharunderscore}trans}).
@@ -204,7 +188,7 @@
 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
-\S\ref{sec:part2?} introduces a language for writing readable yet concise
+Chapter~\ref{sec:part2?} introduces a language for writing readable
 proofs.
 
 We can now derive the desired \isa{i\ {\isasymle}\ f\ i} from \isa{f{\isacharunderscore}incr}:%
@@ -212,16 +196,22 @@
 \isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}%
 \begin{isamarkuptext}%
 \noindent
-The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. Again,
-we could have included this derivation in the original statement of the lemma:%
+The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. 
+We could have included this derivation in the original statement of the lemma:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
 \begin{isamarkuptext}%
-\begin{exercise}
-From the above axiom and lemma for \isa{f} show that \isa{f} is the
-identity.
-\end{exercise}
+\begin{warn}
+We discourage the use of axioms because of the danger of
+inconsistencies.  Axiom \isa{f{\isacharunderscore}ax} does
+not introduce an inconsistency because, for example, the identity function
+satisfies it.  Axioms can be useful in exploratory developments, say when 
+you assume some well-known theorems so that you can quickly demonstrate some
+point about methodology.  If your example turns into a substantial proof
+development, you should replace the axioms by proofs.
+\end{warn}
 
+\bigskip
 In general, \isa{induct{\isacharunderscore}tac} can be applied with any rule $r$
 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
 format is
@@ -240,10 +230,15 @@
 which case the application is
 \begin{quote}
 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{and} \dots\ \isa{and} $z@1 \dots z@m$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
-\end{quote}%
+\end{quote}
+
+\begin{exercise}
+From the axiom and lemma for \isa{f}, show that \isa{f} is the
+identity function.
+\end{exercise}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Derivation of new induction schemas%
+\isamarkupsubsection{Derivation of New Induction Schemas%
 }
 %
 \begin{isamarkuptext}%
@@ -266,7 +261,8 @@
 \isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}less{\isacharunderscore}SucE{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
-The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
+The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction
+mentioned above:
 \begin{isabelle}%
 \ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
 \end{isabelle}
@@ -283,9 +279,9 @@
 \begin{isamarkuptext}%
 Finally we should remind the reader that 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} can be viewed (and derived) as
+example theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} is
 a special case of \isa{wf{\isacharunderscore}induct} where \isa{r} is \isa{{\isacharless}} on
-\isa{nat}. The details can be found in the HOL library.%
+\isa{nat}. The details can be found in theory \isa{Wellfounded_Recursion}.%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables: