diff -r 619531d87ce4 -r 4e2ee88276d2 doc-src/TutorialI/document/AdvancedInd.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/AdvancedInd.tex	Thu Jul 26 19:59:06 2012 +0200
@@ -0,0 +1,436 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{AdvancedInd}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\begin{isamarkuptext}%
+\noindent
+Now that we have learned about rules and logic, we take another look at 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
+with an extended example of induction (\S\ref{sec:CTL-revisited}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Massaging the Proposition%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\label{sec:ind-var-in-prems}
+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
+non-empty list, this lemma looks easy to prove:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ hd{\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\noindent
+But induction produces the warning
+\begin{quote}\tt
+Induction variable occurs also among premises!
+\end{quote}
+and leads to the base case
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ hd\ {\isaliteral{28}{\isacharparenleft}}rev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}%
+\end{isabelle}
+Simplification reduces the base case to this:
+\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{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}.
+
+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 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{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}.}
+\end{quote}
+Thus we should state the lemma as an ordinary 
+implication~(\isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}), letting
+\attrdx{rule_format} (\S\ref{sec:forward}) convert the
+result to the usual \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} form:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isacommand{lemma}\isamarkupfalse%
+\ hd{\isaliteral{5F}{\isacharunderscore}}rev\ {\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ hd{\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ xs{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\noindent
+This time, induction leaves us with a trivial base case:
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ hd\ {\isaliteral{28}{\isacharparenleft}}rev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}%
+\end{isabelle}
+And \isa{auto} completes the proof.
+
+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. \]
+Additionally, you may also have to universally quantify some other variables,
+which can yield a fairly complex conclusion.  However, \isa{rule{\isaliteral{5F}{\isacharunderscore}}format} 
+can remove any number of occurrences of \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}} and
+\isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}.
+
+\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 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.
+\end{equation}
+where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.
+Now you can 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
+that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is
+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. \]
+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
+the conclusion as well, under the \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}}, again using \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}} as shown above.
+
+Readers who are puzzled by the form of statement
+(\ref{eqn:ind-over-term}) above should remember that the
+transformation is only performed to permit induction. Once induction
+has been applied, the statement can be transformed back into something quite
+intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\
+$\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a
+little leads to the goal
+\[ \bigwedge\overline{y}.\ 
+   \forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z}
+    \ \Longrightarrow\ C\,\overline{y} \]
+where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and
+$C$ on the free variables of $t$ has been made explicit.
+Unfortunately, this induction schema cannot be expressed as a
+single theorem because it depends on the number of free variables in $t$ ---
+the notation $\overline{y}$ is merely an informal device.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Beyond Structural and Recursion Induction%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\label{sec:complete-ind}
+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 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 \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}%
+\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ P\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n%
+\end{isabelle}
+As an application, we prove a property of the following
+function:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\isamarkupfalse%
+\ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isacommand{axioms}\isamarkupfalse%
+\ f{\isaliteral{5F}{\isacharunderscore}}ax{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}f{\isaliteral{28}{\isacharparenleft}}f{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ f{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\begin{warn}
+We discourage the use of axioms because of the danger of
+inconsistencies.  Axiom \isa{f{\isaliteral{5F}{\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 axioms by theorems.
+\end{warn}\noindent
+The axiom for \isa{f} implies \isa{n\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ n}, which can
+be proved by induction on \mbox{\isa{f\ n}}. Following the recipe outlined
+above, we have to phrase the proposition as follows to allow induction:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ f{\isaliteral{5F}{\isacharunderscore}}incr{\isaliteral{5F}{\isacharunderscore}}lem{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ k\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\noindent
+To perform induction on \isa{k} using \isa{nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct}, we use
+the same general induction method as for recursion induction (see
+\S\ref{sec:fun-induction}):%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ k\ rule{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\noindent
+We get the following proof state:
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ m\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i%
+\end{isabelle}
+After stripping the \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i}, the proof continues with a case
+distinction on \isa{i}. The case \isa{i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} is trivial and we focus on
+the other case:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}rule\ allI{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ i{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n\ i\ nat{\isaliteral{2E}{\isachardot}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ m\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i{\isaliteral{3B}{\isacharsemicolon}}\ i\ {\isaliteral{3D}{\isacharequal}}\ Suc\ nat{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{by}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{21}{\isacharbang}}{\isaliteral{3A}{\isacharcolon}}\ f{\isaliteral{5F}{\isacharunderscore}}ax\ Suc{\isaliteral{5F}{\isacharunderscore}}leI\ intro{\isaliteral{3A}{\isacharcolon}}\ le{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+If you find the last step puzzling, here are the two lemmas it employs:
+\begin{isabelle}
+\isa{m\ {\isaliteral{3C}{\isacharless}}\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ m\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n}
+\rulename{Suc_leI}\isanewline
+\isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}x\ {\isaliteral{5C3C6C653E}{\isasymle}}\ y{\isaliteral{3B}{\isacharsemicolon}}\ y\ {\isaliteral{3C}{\isacharless}}\ z{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{3C}{\isacharless}}\ z}
+\rulename{le_less_trans}
+\end{isabelle}
+%
+The proof goes like this (writing \isa{j} instead of \isa{nat}).
+Since \isa{i\ {\isaliteral{3D}{\isacharequal}}\ Suc\ j} it suffices to show
+\hbox{\isa{j\ {\isaliteral{3C}{\isacharless}}\ f\ {\isaliteral{28}{\isacharparenleft}}Suc\ j{\isaliteral{29}{\isacharparenright}}}},
+by \isa{Suc{\isaliteral{5F}{\isacharunderscore}}leI}\@.  This is
+proved as follows. From \isa{f{\isaliteral{5F}{\isacharunderscore}}ax} we have \isa{f\ {\isaliteral{28}{\isacharparenleft}}f\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ f\ {\isaliteral{28}{\isacharparenleft}}Suc\ j{\isaliteral{29}{\isacharparenright}}}
+(1) which implies \isa{f\ j\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ {\isaliteral{28}{\isacharparenleft}}f\ j{\isaliteral{29}{\isacharparenright}}} by the induction hypothesis.
+Using (1) once more we obtain \isa{f\ j\ {\isaliteral{3C}{\isacharless}}\ f\ {\isaliteral{28}{\isacharparenleft}}Suc\ j{\isaliteral{29}{\isacharparenright}}} (2) by the transitivity
+rule \isa{le{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}trans}.
+Using the induction hypothesis once more we obtain \isa{j\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ j}
+which, together with (2) yields \isa{j\ {\isaliteral{3C}{\isacharless}}\ f\ {\isaliteral{28}{\isacharparenleft}}Suc\ j{\isaliteral{29}{\isacharparenright}}} (again by
+\isa{le{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\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 hard to
+translate the internal proof into a human-readable format.  Automatic
+proofs are easy to write but hard to read and understand.
+
+The desired result, \isa{i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i}, follows from \isa{f{\isaliteral{5F}{\isacharunderscore}}incr{\isaliteral{5F}{\isacharunderscore}}lem}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemmas}\isamarkupfalse%
+\ f{\isaliteral{5F}{\isacharunderscore}}incr\ {\isaliteral{3D}{\isacharequal}}\ f{\isaliteral{5F}{\isacharunderscore}}incr{\isaliteral{5F}{\isacharunderscore}}lem{\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{2C}{\isacharcomma}}\ OF\ refl{\isaliteral{5D}{\isacharbrackright}}%
+\begin{isamarkuptext}%
+\noindent
+The final \isa{refl} gets rid of the premise \isa{{\isaliteral{3F}{\isacharquery}}k\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{3F}{\isacharquery}}i}. 
+We could have included this derivation in the original statement of the lemma:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ f{\isaliteral{5F}{\isacharunderscore}}incr{\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{2C}{\isacharcomma}}\ OF\ refl{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ k\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\begin{exercise}
+From the axiom and lemma for \isa{f}, show that \isa{f} is the
+identity function.
+\end{exercise}
+
+Method \methdx{induct_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
+\begin{quote}
+\isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac} $y@1 \dots y@n$ \isa{rule{\isaliteral{3A}{\isacharcolon}}} $r$\isa{{\isaliteral{29}{\isacharparenright}}}
+\end{quote}
+where $y@1, \dots, y@n$ are variables in the conclusion of the first subgoal.
+
+A further useful induction rule is \isa{length{\isaliteral{5F}{\isacharunderscore}}induct},
+induction on the length of a list\indexbold{*length_induct}
+\begin{isabelle}%
+\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}xs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}ys{\isaliteral{2E}{\isachardot}}\ length\ ys\ {\isaliteral{3C}{\isacharless}}\ length\ xs\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ xs%
+\end{isabelle}
+which is a special case of \isa{measure{\isaliteral{5F}{\isacharunderscore}}induct}
+\begin{isabelle}%
+\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ f\ y\ {\isaliteral{3C}{\isacharless}}\ f\ x\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ a%
+\end{isabelle}
+where \isa{f} may be any function into type \isa{nat}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Derivation of New Induction Schemas%
+}
+\isamarkuptrue%
+%
+\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, using the example
+of \isa{nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct}. Assume we only have structural induction
+available for \isa{nat} and want to derive complete induction.  We
+must generalize the statement as shown:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ induct{\isaliteral{5F}{\isacharunderscore}}lem{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ P\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ P\ m{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ n{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\noindent
+The base case is vacuously true. For the induction step (\isa{m\ {\isaliteral{3C}{\isacharless}}\ Suc\ n}) we distinguish two cases: case \isa{m\ {\isaliteral{3C}{\isacharless}}\ n} is true by induction
+hypothesis and case \isa{m\ {\isaliteral{3D}{\isacharequal}}\ n} follows from the assumption, again using
+the induction hypothesis:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{by}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}blast\ elim{\isaliteral{3A}{\isacharcolon}}\ less{\isaliteral{5F}{\isacharunderscore}}SucE{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+The elimination rule \isa{less{\isaliteral{5F}{\isacharunderscore}}SucE} expresses the case distinction:
+\begin{isabelle}%
+\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}m\ {\isaliteral{3C}{\isacharless}}\ Suc\ n{\isaliteral{3B}{\isacharsemicolon}}\ m\ {\isaliteral{3C}{\isacharless}}\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{3B}{\isacharsemicolon}}\ m\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P%
+\end{isabelle}
+
+Now it is straightforward to derive the original version of
+\isa{nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct} by manipulating the conclusion of the above
+lemma: instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n}
+and remove the trivial condition \isa{n\ {\isaliteral{3C}{\isacharless}}\ Suc\ n}. Fortunately, this
+happens automatically when we add the lemma as a new premise to the
+desired goal:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\isamarkupfalse%
+\ nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ P\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}insert\ induct{\isaliteral{5F}{\isacharunderscore}}lem{\isaliteral{2C}{\isacharcomma}}\ blast{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+HOL already provides the mother of
+all inductions, well-founded induction (see \S\ref{sec:Well-founded}).  For
+example theorem \isa{nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct} is
+a special case of \isa{wf{\isaliteral{5F}{\isacharunderscore}}induct} where \isa{r} is \isa{{\isaliteral{3C}{\isacharless}}} on
+\isa{nat}. The details can be found in theory \isa{Wellfounded_Recursion}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: