--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Oct 20 08:46:41 2000 +0200
@@ -6,7 +6,8 @@
Now that we have learned about rules and logic, we take another look at the
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.
+utilize and even derive new induction schemas. We conclude with some slightly subtle
+examples of induction.
*};
subsection{*Massaging the proposition*};
@@ -82,7 +83,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 \<and> A y";
(*<*)by blast;(*>*)
text{*\noindent
@@ -105,7 +106,7 @@
statement of your original lemma, thus avoiding the intermediate step:
*};
-lemma myrule[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
+lemma myrule[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y";
(*<*)
by blast;
(*>*)
@@ -129,6 +130,9 @@
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 @{text"\<forall>"}, again using @{text"\<longrightarrow>"} as shown above.
*};
subsection{*Beyond structural and recursion induction*};
@@ -149,7 +153,7 @@
Here is an example of its application.
*};
-consts f :: "nat => nat";
+consts f :: "nat \<Rightarrow> nat";
axioms f_ax: "f(f(n)) < f(Suc(n))";
text{*\noindent
@@ -289,7 +293,6 @@
by(insert induct_lem, blast);
text{*
-
Finally we should mention that HOL already provides the mother of all
inductions, \textbf{well-founded
induction}\indexbold{induction!well-founded}\index{well-founded