doc-src/TutorialI/Misc/document/AdvancedInd.tex

 \begin{isabellepar}%
 \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
 \end{isabellepar}%
 which is trivial, and \isa{auto} finishes the whole proof.
 
-If \isa{hd\_rev} is meant to be simplification rule, you are done. But if you
+If \isa{hd\_rev} is meant to be a simplification rule, you are done. But if you
 really need the \isa{\isasymLongrightarrow}-version of \isa{hd\_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:%
 \end{isamarkuptext}%
 \isacommand{lemmas}\ hd{\isacharunderscore}revI\ {\isacharequal}\ hd{\isacharunderscore}rev{\isacharbrackleft}THEN\ mp{\isacharbrackright}%

 (see the remark?? in \S\ref{??}).
 Additionally, you may also have to universally quantify some other variables,
 which can yield a fairly complex conclusion.
 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\ {\isacharampersand}\ A\ y{\isachardoublequote}%
+\isacommand{lemma}\ simple{\isacharcolon}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 You can get the desired lemma by explicit
 application of modus ponens and \isa{spec}:%
 \end{isamarkuptext}%

 \isa{\isasymlongrightarrow} in the conclusion via \isa{rulify}%
 \end{isamarkuptext}%
 \isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rulify{\isacharbrackright}%
 \begin{isamarkuptext}%
 \noindent
-yielding \isa{{\isasymlbrakk}\mbox{{\isacharquery}A}\ \mbox{{\isacharquery}y}{\isacharsemicolon}\ \mbox{{\isacharquery}B}\ \mbox{{\isacharquery}y}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}B}\ \mbox{{\isacharquery}y}\ {\isasymand}\ \mbox{{\isacharquery}A}\ \mbox{{\isacharquery}y}}.
+yielding \isa{{\isasymlbrakk}\mbox{A}\ \mbox{y}{\isacharsemicolon}\ \mbox{B}\ \mbox{y}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{B}\ \mbox{y}\ {\isasymand}\ \mbox{A}\ \mbox{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}rulify{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}\ y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
+\isacommand{lemma}\ myrule{\isacharbrackleft}rulify{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
 \begin{isamarkuptext}%
 \bigskip
 
 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

 \[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \] 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 below.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Beyond structural induction}
+\isamarkupsubsection{Beyond structural and recursion induction}
 %
 \begin{isamarkuptext}%
 So far, inductive proofs where by structural induction for
 primitive recursive functions and recursion induction for total recursive
 functions. But sometimes structural induction is awkward and there is no

 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{less\_induct}:
 \begin{quote}
 
 \begin{isabelle}%
-{\isacharparenleft}{\isasymAnd}\mbox{n}{\isachardot}\ {\isasymforall}\mbox{m}{\isachardot}\ \mbox{m}\ {\isacharless}\ \mbox{n}\ {\isasymlongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{m}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{n}{\isacharparenright}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{{\isacharquery}n}
+{\isacharparenleft}{\isasymAnd}\mbox{n}{\isachardot}\ {\isasymforall}\mbox{m}{\isachardot}\ \mbox{m}\ {\isacharless}\ \mbox{n}\ {\isasymlongrightarrow}\ \mbox{P}\ \mbox{m}\ {\isasymLongrightarrow}\ \mbox{P}\ \mbox{n}{\isacharparenright}\ {\isasymLongrightarrow}\ \mbox{P}\ \mbox{n}
 \end{isabelle}%
 
 \end{quote}
 Here is an example of its application.%
 \end{isamarkuptext}%

 \begin{isamarkuptext}%
 \noindent
 It is not surprising if you find the last step puzzling.
 The proof goes like this (writing \isa{j} instead of \isa{nat}).
 Since \isa{\mbox{i}\ {\isacharequal}\ Suc\ \mbox{j}} it suffices to show
-\isa{\mbox{j}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}} (by \isa{Suc\_leI}: \isa{\mbox{{\isacharquery}m}\ {\isacharless}\ \mbox{{\isacharquery}n}\ {\isasymLongrightarrow}\ Suc\ \mbox{{\isacharquery}m}\ {\isasymle}\ \mbox{{\isacharquery}n}}). This is
+\isa{\mbox{j}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}} (by \isa{Suc\_leI}: \isa{\mbox{m}\ {\isacharless}\ \mbox{n}\ {\isasymLongrightarrow}\ Suc\ \mbox{m}\ {\isasymle}\ \mbox{n}}). This is
 proved as follows. From \isa{f\_ax} we have \isa{f\ {\isacharparenleft}f\ \mbox{j}{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}}
 (1) which implies \isa{f\ \mbox{j}\ {\isasymle}\ f\ {\isacharparenleft}f\ \mbox{j}{\isacharparenright}} (by the induction hypothesis).
 Using (1) once more we obtain \isa{f\ \mbox{j}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}} (2) by transitivity
-(\isa{le_less_trans}: \isa{{\isasymlbrakk}\mbox{{\isacharquery}i}\ {\isasymle}\ \mbox{{\isacharquery}j}{\isacharsemicolon}\ \mbox{{\isacharquery}j}\ {\isacharless}\ \mbox{{\isacharquery}k}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}i}\ {\isacharless}\ \mbox{{\isacharquery}k}}).
+(\isa{le_less_trans}: \isa{{\isasymlbrakk}\mbox{i}\ {\isasymle}\ \mbox{j}{\isacharsemicolon}\ \mbox{j}\ {\isacharless}\ \mbox{k}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{i}\ {\isacharless}\ \mbox{k}}).
 Using the induction hypothesis once more we obtain \isa{\mbox{j}\ {\isasymle}\ f\ \mbox{j}}
 which, together with (2) yields \isa{\mbox{j}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ \mbox{j}{\isacharparenright}} (again by
 \isa{le_less_trans}).
 
 This last step shows both the power and the danger of automatic proofs: they

 
 We can now derive the desired \isa{\mbox{i}\ {\isasymle}\ f\ \mbox{i}} from \isa{f\_incr}:%
 \end{isamarkuptext}%
 \isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rulify{\isacharcomma}\ OF\ refl{\isacharbrackright}%
 \begin{isamarkuptext}%
+\noindent
 The final \isa{refl} gets rid of the premise \isa{?k = f ?i}. Again, we could
 have included this derivation in the original statement of the lemma:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rulify{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
 \begin{isamarkuptext}%

 In fact, \isa{induct\_tac} even allows the conclusion of
 \isa{r} to be an (iterated) conjunction of formulae of the above form, in
 which case the application is
 \begin{ttbox}
 apply(induct_tac y1 ... yn and ... and z1 ... zm rule: r)
-\end{ttbox}
-
+\end{ttbox}%
+\end{isamarkuptext}%
+%
+\isamarkupsubsection{Derivation of new induction schemas}
+%
+\begin{isamarkuptext}%
+\label{sec:derive-ind}
+Induction schemas are ordinary theorems and you can derive new ones
+whenever you wish.  This section shows you how to, using the example
+of \isa{less\_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:%
+\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}\ {\isacharequal}{\isacharequal}{\isachargreater}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+The base case is trivially true. For the induction step (\isa{\mbox{m}\ {\isacharless}\ Suc\ \mbox{n}}) we distinguish two cases: \isa{\mbox{m}\ {\isacharless}\ \mbox{n}} is true by induction
+hypothesis and \isa{\mbox{m}\ {\isacharequal}\ \mbox{n}} follow from the assumption again using
+the induction hypothesis:%
+\end{isamarkuptxt}%
+\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
+\isanewline
+\isacommand{ML}{\isachardoublequote}set\ quick{\isacharunderscore}and{\isacharunderscore}dirty{\isachardoublequote}\isanewline
+\isacommand{sorry}\isanewline
+\isacommand{ML}{\isachardoublequote}reset\ quick{\isacharunderscore}and{\isacharunderscore}dirty{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+The elimination rule \isa{less_SucE} expresses the case distinction:
+\begin{quote}
+
+\begin{isabelle}%
+{\isasymlbrakk}\mbox{m}\ {\isacharless}\ Suc\ \mbox{n}{\isacharsemicolon}\ \mbox{m}\ {\isacharless}\ \mbox{n}\ {\isasymLongrightarrow}\ \mbox{P}{\isacharsemicolon}\ \mbox{m}\ {\isacharequal}\ \mbox{n}\ {\isasymLongrightarrow}\ \mbox{P}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{P}
+\end{isabelle}%
+
+\end{quote}
+
+Now it is straightforward to derive the original version of
+\isa{less\_induct} by manipulting the conclusion of the above lemma:
+instantiate \isa{n} by \isa{Suc\ \mbox{n}} and \isa{m} by \isa{n} and
+remove the trivial condition \isa{\mbox{n}\ {\isacharless}\ \mbox{Sc}\ \mbox{n}}. Fortunately, this
+happens automatically when we add the lemma as a new premise to the
+desired goal:%
+\end{isamarkuptext}%
+\isacommand{theorem}\ less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ P\ n{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
 Finally we should mention that HOL already provides the mother of all
 inductions, \emph{wellfounded induction} (\isa{wf\_induct}):
 \begin{quote}
 
 \begin{isabelle}%
-{\isasymlbrakk}wf\ \mbox{{\isacharquery}r}{\isacharsemicolon}\ {\isasymAnd}\mbox{x}{\isachardot}\ {\isasymforall}\mbox{y}{\isachardot}\ {\isacharparenleft}\mbox{y}{\isacharcomma}\ \mbox{x}{\isacharparenright}\ {\isasymin}\ \mbox{{\isacharquery}r}\ {\isasymlongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{y}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{x}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{{\isacharquery}P}\ \mbox{{\isacharquery}a}
-\end{isabelle}%
-
-\end{quote}
+{\isasymlbrakk}wf\ \mbox{r}{\isacharsemicolon}\ {\isasymAnd}\mbox{x}{\isachardot}\ {\isasymforall}\mbox{y}{\isachardot}\ {\isacharparenleft}\mbox{y}{\isacharcomma}\ \mbox{x}{\isacharparenright}\ {\isasymin}\ \mbox{r}\ {\isasymlongrightarrow}\ \mbox{P}\ \mbox{y}\ {\isasymLongrightarrow}\ \mbox{P}\ \mbox{x}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{P}\ \mbox{a}
+\end{isabelle}%
+
+\end{quote}
+where \isa{wf\ \mbox{r}} means that the relation \isa{r} is wellfounded.
+For example \isa{less\_induct} is the special case where \isa{r} is \isa{<} on \isa{nat}.
 For details see the library.%
 \end{isamarkuptext}%
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex