--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Sep 12 15:43:15 2000 +0200
@@ -17,7 +17,7 @@
that is amenable to induction, but this is not always the case:
*};
-lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) = last xs";
+lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs";
apply(induct_tac xs);
txt{*\noindent
@@ -49,7 +49,7 @@
This means we should prove
*};
(*<*)oops;(*>*)
-lemma hd_rev: "xs \\<noteq> [] \\<longrightarrow> hd(rev xs) = last xs";
+lemma hd_rev: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs";
(*<*)
by(induct_tac xs, auto);
(*>*)
@@ -82,7 +82,7 @@
Here is a simple example (which is proved by @{text"blast"}):
*};
-lemma simple: "\\<forall>y. A y \\<longrightarrow> B y \<longrightarrow> B y & A y";
+lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
(*<*)by blast;(*>*)
text{*\noindent
@@ -105,7 +105,7 @@
statement of your original lemma, thus avoiding the intermediate step:
*};
-lemma myrule[rulified]: "\\<forall>y. A y \\<longrightarrow> B y \<longrightarrow> B y & A y";
+lemma myrule[rulified]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
(*<*)
by blast;
(*>*)
@@ -134,8 +134,8 @@
Structural induction on @{typ"nat"} is
usually known as ``mathematical induction''. There is also ``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 @{thm [source] nat_less_induct}:
-@{thm[display] nat_less_induct [no_vars]}
+holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]nat_less_induct}:
+@{thm[display]"nat_less_induct"[no_vars]}
Here is an example of its application.
*};
@@ -152,10 +152,10 @@
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 @{term"k"} using @{thm [source] nat_less_induct}, we use the same
+To perform induction on @{term"k"} using @{thm[source]nat_less_induct}, we use the same
general induction method as for recursion induction (see
\S\ref{sec:recdef-induction}):
*};
@@ -213,7 +213,7 @@
we could have included this derivation in the original statement of the lemma:
*};
-lemma f_incr[rulified, OF refl]: "\\<forall>i. k = f i \\<longrightarrow> i \\<le> f i";
+lemma f_incr[rulified, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
(*<*)oops;(*>*)
text{*
@@ -242,49 +242,46 @@
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 @{thm [source] nat_less_induct}. Assume we only have structural induction
+of @{thm[source]nat_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) \\<Longrightarrow> \\<forall>m<n. P m";
+lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m";
apply(induct_tac n);
txt{*\noindent
The base case is trivially true. For the induction step (@{prop"m <
-Suc n"}) we distinguish two cases: @{prop"m < n"} is true by induction
-hypothesis and @{prop"m = n"} follow from the assumption again using
+Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction
+hypothesis and case @{prop"m = n"} follows 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"
+by(blast elim:less_SucE)
text{*\noindent
The elimination rule @{thm[source]less_SucE} expresses the case distinction:
@{thm[display]"less_SucE"[no_vars]}
Now it is straightforward to derive the original version of
-@{thm [source] nat_less_induct} by manipulting the conclusion of the above lemma:
+@{thm[source]nat_less_induct} by manipulting the conclusion of the above lemma:
instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} and
remove the trivial condition @{prop"n < Sc n"}. Fortunately, this
happens automatically when we add the lemma as a new premise to the
desired goal:
*};
-theorem nat_less_induct: "(\\<And>n::nat. \\<forall>m<n. P m \\<Longrightarrow> P n) \\<Longrightarrow> P n";
+theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n";
by(insert induct_lem, blast);
-text{*\noindent
+text{*
Finally we should mention that HOL already provides the mother of all
inductions, \emph{wellfounded induction} (@{thm[source]wf_induct}):
@{thm[display]"wf_induct"[no_vars]}
where @{term"wf r"} means that the relation @{term"r"} is wellfounded.
-For example @{thm [source] nat_less_induct} is the special case where @{term"r"} is
-@{text"<"} on @{typ"nat"}. For details see the library.
+For example, theorem @{thm[source]nat_less_induct} can be viewed (and
+derived) as a special case of @{thm[source]wf_induct} where
+@{term"r"} is @{text"<"} on @{typ"nat"}. For details see the library.
*};
(*<*)