--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Aug 25 12:17:09 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Mon Aug 28 09:32:51 2000 +0200
@@ -7,15 +7,15 @@
finer points of induction. The two questions we answer are: what to do if the
proposition to be proved is not directly amenable to induction, and how to
utilize and even derive new induction schemas.
-*}
+*};
-subsection{*Massaging the proposition\label{sec:ind-var-in-prems}*}
+subsection{*Massaging the proposition\label{sec:ind-var-in-prems}*};
text{*
\noindent
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:
-*}
+*};
lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) = last xs";
apply(induct_tac xs);
@@ -47,11 +47,11 @@
using \isa{\isasymlongrightarrow}.}
\end{quote}
This means we should prove
-*}
-(*<*)oops(*>*)
+*};
+(*<*)oops;(*>*)
lemma hd_rev: "xs \\<noteq> [] \\<longrightarrow> hd(rev xs) = last xs";
(*<*)
-by(induct_tac xs, auto)
+by(induct_tac xs, auto);
(*>*)
text{*\noindent
@@ -61,13 +61,13 @@
\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:
-*}
+*};
-lemmas hd_revI = hd_rev[THEN mp]
+lemmas hd_revI = hd_rev[THEN mp];
text{*\noindent
which yields the lemma we originally set out to prove.
@@ -79,34 +79,34 @@
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}):
-*}
+*};
-lemma simple: "\\<forall> y. A y \\<longrightarrow> B y \<longrightarrow> B y & A y"
-(*<*)by blast(*>*)
+lemma simple: "\\<forall>y. A y \\<longrightarrow> B y \<longrightarrow> B y & A y";
+(*<*)by blast;(*>*)
text{*\noindent
You can get the desired lemma by explicit
application of modus ponens and \isa{spec}:
-*}
+*};
-lemmas myrule = simple[THEN spec, THEN mp, THEN mp]
+lemmas myrule = simple[THEN spec, THEN mp, THEN mp];
text{*\noindent
or the wholesale stripping of \isa{\isasymforall} and
\isa{\isasymlongrightarrow} in the conclusion via \isa{rulify}
-*}
+*};
-lemmas myrule = simple[rulify]
+lemmas myrule = simple[rulify];
text{*\noindent
-yielding @{thm"myrule"}.
+yielding @{thm"myrule"[no_vars]}.
You can go one step further and include these derivations already in the
statement of your original lemma, thus avoiding the intermediate step:
-*}
+*};
-lemma myrule[rulify]: "\\<forall> y. A y \\<longrightarrow> B y \<longrightarrow> B y & A y"
+lemma myrule[rulify]: "\\<forall>y. A y \\<longrightarrow> B y \<longrightarrow> B y & A y";
(*<*)
-by blast
+by blast;
(*>*)
text{*
@@ -118,10 +118,9 @@
\[ \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.
+*};
-*}
-
-subsection{*Beyond structural induction*}
+subsection{*Beyond structural and recursion induction*};
text{*
So far, inductive proofs where by structural induction for
@@ -136,13 +135,13 @@
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}
-@{thm[display]"less_induct"}
+@{thm[display]"less_induct"[no_vars]}
\end{quote}
Here is an example of its application.
-*}
+*};
-consts f :: "nat => nat"
-axioms f_ax: "f(f(n)) < f(Suc(n))"
+consts f :: "nat => nat";
+axioms f_ax: "f(f(n)) < f(Suc(n))";
text{*\noindent
From the above axiom\footnote{In general, the use of axioms is strongly
@@ -152,19 +151,19 @@
for \isa{f} it follows that @{term"n <= f n"}, which can
be proved by induction on @{term"f n"}. Following the recipy outlined
above, we have to phrase the proposition as follows to allow induction:
-*}
+*};
-lemma f_incr_lem: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i"
+lemma f_incr_lem: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
txt{*\noindent
To perform induction on \isa{k} using \isa{less\_induct}, we use the same
general induction method as for recursion induction (see
\S\ref{sec:recdef-induction}):
-*}
+*};
-apply(induct_tac k rule:less_induct)
+apply(induct_tac k rule:less_induct);
(*<*)
-apply(rule allI)
+apply(rule allI);
apply(case_tac i);
apply(simp);
(*>*)
@@ -182,7 +181,7 @@
\ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i});\ \mbox{i}\ =\ Suc\ \mbox{nat}{\isasymrbrakk}\isanewline
\ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
\end{isabellepar}%
-*}
+*};
by(blast intro!: f_ax Suc_leI intro:le_less_trans);
@@ -190,11 +189,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 @{term"i = Suc j"} it suffices to show
-@{term"j < f(Suc j)"} (by \isa{Suc\_leI}: @{thm"Suc_leI"}). This is
+@{term"j < f(Suc j)"} (by \isa{Suc\_leI}: @{thm"Suc_leI"[no_vars]}). This is
proved as follows. From \isa{f\_ax} we have @{term"f (f j) < f (Suc j)"}
(1) which implies @{term"f j <= f (f j)"} (by the induction hypothesis).
Using (1) once more we obtain @{term"f j < f(Suc j)"} (2) by transitivity
-(\isa{le_less_trans}: @{thm"le_less_trans"}).
+(\isa{le_less_trans}: @{thm"le_less_trans"[no_vars]}).
Using the induction hypothesis once more we obtain @{term"j <= f j"}
which, together with (2) yields @{term"j < f (Suc j)"} (again by
\isa{le_less_trans}).
@@ -206,17 +205,17 @@
proofs.
We can now derive the desired @{term"i <= f i"} from \isa{f\_incr}:
-*}
+*};
lemmas f_incr = f_incr_lem[rulify, OF refl];
-text{*
+text{*\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:
-*}
+*};
-lemma f_incr[rulify, OF refl]: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i"
-(*<*)oops(*>*)
+lemma f_incr[rulify, OF refl]: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
+(*<*)oops;(*>*)
text{*
\begin{exercise}
@@ -236,14 +235,61 @@
\begin{ttbox}
apply(induct_tac y1 ... yn and ... and z1 ... zm rule: r)
\end{ttbox}
+*};
+subsection{*Derivation of new induction schemas*};
+
+text{*\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 @{typ"nat"} and want to derive complete induction. This
+requires us to generalize the statement first:
+*};
+
+lemma induct_lem: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) ==> \\<forall>m<n. P m";
+apply(induct_tac n);
+
+txt{*\noindent
+The base case is trivially true. For the induction step (@{term"m <
+Suc n"}) we distinguish two cases: @{term"m < n"} is true by induction
+hypothesis and @{term"m = n"} follow from the assumption again using
+the induction hypothesis:
+*};
+
+apply(blast);
+(* apply(blast elim:less_SucE); *)
+ML"set quick_and_dirty"
+sorry;
+ML"reset quick_and_dirty"
+
+text{*\noindent
+The elimination rule \isa{less_SucE} expresses the case distinction:
+\begin{quote}
+@{thm[display]"less_SucE"[no_vars]}
+\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 @{term"Suc n"} and \isa{m} by \isa{n} and
+remove the trivial condition @{term"n < Sc n"}. Fortunately, this
+happens automatically when we add the lemma as a new premise to the
+desired goal:
+*};
+
+theorem less_induct: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) ==> P n";
+by(insert induct_lem, blast);
+
+text{*\noindent
Finally we should mention that HOL already provides the mother of all
inductions, \emph{wellfounded induction} (\isa{wf\_induct}):
\begin{quote}
-@{thm[display]"wf_induct"}
+@{thm[display]"wf_induct"[no_vars]}
\end{quote}
+where @{term"wf r"} means that the relation \isa{r} is wellfounded.
+For example \isa{less\_induct} is the special case where \isa{r} is \isa{<} on @{typ"nat"}.
For details see the library.
-*}
+*};
(*<*)
end