--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Jan 12 16:28:14 2001 +0100
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Jan 12 16:32:01 2001 +0100
@@ -11,104 +11,83 @@
with an extended example of induction (\S\ref{sec:CTL-revisited}).
*};
-subsection{*Massaging the proposition*};
+subsection{*Massaging the Proposition*};
text{*\label{sec:ind-var-in-prems}
-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:
+Often we have assumed that the theorem we want to prove is already in a form
+that is amenable to induction, but sometimes it isn't.
+Here is an example.
+Since @{term"hd"} and @{term"last"} return the first and last element of a
+non-empty list, this lemma looks easy to prove:
*};
-lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs";
-apply(induct_tac xs);
+lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
+apply(induct_tac xs)
txt{*\noindent
-(where @{term"hd"} and @{term"last"} return the first and last element of a
-non-empty list)
-produces the warning
+But induction produces the warning
\begin{quote}\tt
Induction variable occurs also among premises!
\end{quote}
and leads to the base case
@{subgoals[display,indent=0,goals_limit=1]}
-which, after simplification, becomes
+After simplification, it becomes
\begin{isabelle}
\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
\end{isabelle}
We cannot prove this equality because we do not know what @{term hd} and
@{term last} return when applied to @{term"[]"}.
-The point is that we have violated the above warning. Because the induction
-formula is only the conclusion, the occurrence of @{term xs} in the premises is
-not modified by induction. Thus the case that should have been trivial
+We should not have ignored the warning. Because the induction
+formula is only the conclusion, induction does not affect the occurrence of @{term xs} in the premises.
+Thus the case that should have been trivial
becomes unprovable. Fortunately, the solution is easy:\footnote{A very similar
heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
\begin{quote}
\emph{Pull all occurrences of the induction variable into the conclusion
using @{text"\<longrightarrow>"}.}
\end{quote}
-This means we should prove
+Thus we should state the lemma as an ordinary
+implication~(@{text"\<longrightarrow>"}), letting
+@{text rule_format} (\S\ref{sec:forward}) convert the
+result to the usual @{text"\<Longrightarrow>"} form:
*};
(*<*)oops;(*>*)
-lemma hd_rev: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs";
+lemma hd_rev [rule_format]: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs";
(*<*)
apply(induct_tac xs);
(*>*)
txt{*\noindent
-This time, induction leaves us with the following base case
+This time, induction leaves us with a trivial base case:
@{subgoals[display,indent=0,goals_limit=1]}
-which is trivial, and @{text"auto"} finishes the whole proof.
+And @{text"auto"} completes the proof.
+*}
+(*<*)
+by auto;
+(*>*)
-If @{text hd_rev} is meant to be a simplification rule, you are
-done. But if you really need the @{text"\<Longrightarrow>"}-version of
-@{text 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:
-*}(*<*)by(auto);(*>*)
-lemmas hd_revI = hd_rev[THEN mp];
-
-text{*\noindent
-which yields the lemma we originally set out to prove.
-In case there are multiple premises $A@1$, \dots, $A@n$ containing the
+text{*
+If there are multiple premises $A@1$, \dots, $A@n$ containing the
induction variable, you should turn the conclusion $C$ into
\[ A@1 \longrightarrow \cdots A@n \longrightarrow C \]
(see the remark?? in \S\ref{??}).
Additionally, you may also have to universally quantify some other variables,
-which can yield a fairly complex conclusion.
+which can yield a fairly complex conclusion. However, @{text"rule_format"}
+can remove any number of occurrences of @{text"\<forall>"} and
+@{text"\<longrightarrow>"}.
+
Here is a simple example (which is proved by @{text"blast"}):
*};
-lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y";
-(*<*)by blast;(*>*)
-
-text{*\noindent
-You can get the desired lemma by explicit
-application of modus ponens and @{thm[source]spec}:
-*};
-
-lemmas myrule = simple[THEN spec, THEN mp, THEN mp];
-
-text{*\noindent
-or the wholesale stripping of @{text"\<forall>"} and
-@{text"\<longrightarrow>"} in the conclusion via @{text"rule_format"}
-*};
-
-lemmas myrule = simple[rule_format];
-
-text{*\noindent
-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[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y";
+lemma simple[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y";
(*<*)
by blast;
(*>*)
text{*
-\bigskip
+\medskip
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
@@ -131,19 +110,19 @@
the conclusion as well, under the @{text"\<forall>"}, again using @{text"\<longrightarrow>"} as shown above.
*};
-subsection{*Beyond structural and recursion induction*};
+subsection{*Beyond Structural and Recursion Induction*};
text{*\label{sec:complete-ind}
-So far, inductive proofs where by structural induction for
+So far, inductive proofs were by structural induction for
primitive recursive functions and recursion induction for total recursive
functions. But sometimes structural induction is awkward and there is no
-recursive function in sight either that could furnish a more appropriate
-induction schema. In such cases some existing standard induction schema can
+recursive function that could furnish a more appropriate
+induction schema. In such cases a general-purpose induction schema can
be helpful. We show how to apply such induction schemas by an example.
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)$
+usually known as mathematical induction. There is also \emph{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]}
Here is an example of its application.
@@ -153,11 +132,7 @@
axioms f_ax: "f(f(n)) < f(Suc(n))";
text{*\noindent
-From the above axiom\footnote{In general, the use of axioms is strongly
-discouraged, because of the danger of inconsistencies. The above axiom does
-not introduce an inconsistency because, for example, the identity function
-satisfies it.}
-for @{term"f"} it follows that @{prop"n <= f n"}, which can
+The axiom for @{term"f"} implies @{prop"n <= f n"}, which can
be proved by induction on @{term"f n"}. Following the recipe outlined
above, we have to phrase the proposition as follows to allow induction:
*};
@@ -191,14 +166,23 @@
by(blast intro!: f_ax Suc_leI intro: le_less_trans);
text{*\noindent
-It is not surprising if you find the last step puzzling.
+If you find the last step puzzling, here are the
+two other lemmas used above:
+\begin{isabelle}
+@{thm Suc_leI[no_vars]}
+\rulename{Suc_leI}\isanewline
+@{thm le_less_trans[no_vars]}
+\rulename{le_less_trans}
+\end{isabelle}
+%
The proof goes like this (writing @{term"j"} instead of @{typ"nat"}).
Since @{prop"i = Suc j"} it suffices to show
-@{prop"j < f(Suc j)"} (by @{thm[source]Suc_leI}: @{thm"Suc_leI"[no_vars]}). This is
+\hbox{@{prop"j < f(Suc j)"}},
+by @{thm[source]Suc_leI}\@. This is
proved as follows. From @{thm[source]f_ax} we have @{prop"f (f j) < f (Suc j)"}
-(1) which implies @{prop"f j <= f (f j)"} (by the induction hypothesis).
-Using (1) once more we obtain @{prop"f j < f(Suc j)"} (2) by transitivity
-(@{thm[source]le_less_trans}: @{thm"le_less_trans"[no_vars]}).
+(1) which implies @{prop"f j <= f (f j)"} by the induction hypothesis.
+Using (1) once more we obtain @{prop"f j < f(Suc j)"} (2) by the transitivity
+rule @{thm[source]le_less_trans}.
Using the induction hypothesis once more we obtain @{prop"j <= f j"}
which, together with (2) yields @{prop"j < f (Suc j)"} (again by
@{thm[source]le_less_trans}).
@@ -206,7 +190,7 @@
This last step shows both the power and the danger of automatic proofs: they
will usually not tell you how the proof goes, because it can be very hard to
translate the internal proof into a human-readable format. Therefore
-\S\ref{sec:part2?} introduces a language for writing readable yet concise
+Chapter~\ref{sec:part2?} introduces a language for writing readable
proofs.
We can now derive the desired @{prop"i <= f i"} from @{text"f_incr"}:
@@ -215,19 +199,25 @@
lemmas f_incr = f_incr_lem[rule_format, OF refl];
text{*\noindent
-The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. Again,
-we could have included this derivation in the original statement of the lemma:
+The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}.
+We could have included this derivation in the original statement of the lemma:
*};
lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
(*<*)oops;(*>*)
text{*
-\begin{exercise}
-From the above axiom and lemma for @{term"f"} show that @{term"f"} is the
-identity.
-\end{exercise}
+\begin{warn}
+We discourage the use of axioms because of the danger of
+inconsistencies. Axiom @{text f_ax} does
+not introduce an inconsistency because, for example, the identity function
+satisfies it. Axioms can be useful in exploratory developments, say when
+you assume some well-known theorems so that you can quickly demonstrate some
+point about methodology. If your example turns into a substantial proof
+development, you should replace the axioms by proofs.
+\end{warn}
+\bigskip
In general, @{text induct_tac} can be applied with any rule $r$
whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
format is
@@ -245,9 +235,14 @@
\begin{quote}
\isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"and"} \dots\ @{text"and"} $z@1 \dots z@m$ @{text"rule:"} $r$@{text")"}
\end{quote}
+
+\begin{exercise}
+From the axiom and lemma for @{term"f"}, show that @{term"f"} is the
+identity function.
+\end{exercise}
*};
-subsection{*Derivation of new induction schemas*};
+subsection{*Derivation of New Induction Schemas*};
text{*\label{sec:derive-ind}
Induction schemas are ordinary theorems and you can derive new ones
@@ -270,7 +265,8 @@
by(blast elim:less_SucE)
text{*\noindent
-The elimination rule @{thm[source]less_SucE} expresses the case distinction:
+The elimination rule @{thm[source]less_SucE} expresses the case distinction
+mentioned above:
@{thm[display]"less_SucE"[no_vars]}
Now it is straightforward to derive the original version of
@@ -287,8 +283,8 @@
text{*
Finally we should remind the reader that HOL already provides the mother of
all inductions, well-founded induction (see \S\ref{sec:Well-founded}). For
-example theorem @{thm[source]nat_less_induct} can be viewed (and derived) as
+example theorem @{thm[source]nat_less_induct} is
a special case of @{thm[source]wf_induct} where @{term r} is @{text"<"} on
-@{typ nat}. The details can be found in the HOL library.
+@{typ nat}. The details can be found in theory \isa{Wellfounded_Recursion}.
*}
(*<*)end(*>*)