--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Aug 28 14:09:33 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Aug 28 15:13:55 2000 +0200
@@ -55,7 +55,7 @@
\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:%
@@ -73,7 +73,7 @@
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
@@ -88,11 +88,11 @@
\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
@@ -104,7 +104,7 @@
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
@@ -121,7 +121,7 @@
\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}
@@ -169,11 +169,11 @@
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}).
@@ -188,6 +188,7 @@
\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}%
@@ -209,17 +210,65 @@
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}
+{\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}%