--- a/doc-src/IsarOverview/Isar/Induction.thy Sun Nov 11 17:18:38 2007 +0100
+++ b/doc-src/IsarOverview/Isar/Induction.thy Sun Nov 11 19:41:26 2007 +0100
@@ -1,4 +1,8 @@
-(*<*)theory Induction imports Main begin(*>*)
+(*<*)theory Induction imports Main begin
+fun itrev where
+"itrev [] ys = ys" |
+"itrev (x#xs) ys = itrev xs (x#ys)"
+(*>*)
section{*Case distinction and induction \label{sec:Induct}*}
@@ -72,11 +76,11 @@
In each \isakeyword{case} the assumption can be
referred to inside the proof by the name of the constructor. In
Section~\ref{sec:full-Ind} below we will come across an example
-of this. *}
+of this.
-subsection{*Structural induction*}
+\subsection{Structural induction}
-text{* We start with an inductive proof where both cases are proved automatically: *}
+We start with an inductive proof where both cases are proved automatically: *}
lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)"
by (induct n, simp_all)
@@ -121,63 +125,100 @@
text{* \noindent Of course we could again have written
\isakeyword{thus}~@{text ?case} instead of giving the term explicitly
-but we wanted to use @{term i} somewhere. *}
+but we wanted to use @{term i} somewhere.
+
+\subsection{Generalization via @{text arbitrary}}
+
+It is frequently necessary to generalize a claim before it becomes
+provable by induction. The tutorial~\cite{LNCS2283} demonstrates this
+with @{prop"itrev xs ys = rev xs @ ys"}, where @{text ys}
+needs to be universally quantified before induction succeeds.\footnote{@{thm rev.simps(1)},\quad @{thm rev.simps(2)[no_vars]},\\ @{thm itrev.simps(1)[no_vars]},\quad @{thm itrev.simps(2)[no_vars]}} But
+strictly speaking, this quantification step is already part of the
+proof and the quantifiers should not clutter the original claim. This
+is how the quantification step can be combined with induction: *}
+lemma "itrev xs ys = rev xs @ ys"
+by (induct xs arbitrary: ys) auto
+text{*\noindent The annotation @{text"arbitrary:"}~\emph{vars}
+universally quantifies all \emph{vars} before the induction. Hence
+they can be replaced by \emph{arbitrary} values in the proof.
+This proof also demonstrates that \isakeyword{by} can take two arguments,
+one to start and one to finish the proof --- the latter is optional.
-subsection{*Induction formulae involving @{text"\<And>"} or @{text"\<Longrightarrow>"}\label{sec:full-Ind}*}
+The nice thing about generalization via @{text"arbitrary:"} is that in
+the induction step the claim is available in unquantified form but
+with the generalized variables replaced by @{text"?"}-variables, ready
+for instantiation. In the above example the
+induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"}.
+
+For the curious: @{text"arbitrary:"} introduces @{text"\<And>"}
+behind the scenes.
+
+\subsection{Inductive proofs of conditional formulae}
+
+Induction also copes well with formulae involving @{text"\<Longrightarrow>"}, for example
+*}
+
+lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
+by (induct xs) auto
+
+text{*\noindent This is an improvement over that style the
+tutorial~\cite{LNCS2283} advises, which requires @{text"\<longrightarrow>"}.
+A further improvement is shown in the following proof:
+*}
-text{* Let us now consider the situation where the goal to be proved contains
-@{text"\<And>"} or @{text"\<Longrightarrow>"}, say @{prop"\<And>x. P x \<Longrightarrow> Q x"} --- motivation and a
-real example follow shortly. This means that in each case of the induction,
+lemma "map f xs = map f ys \<Longrightarrow> length xs = length ys"
+proof (induct ys arbitrary: xs)
+ case Nil thus ?case by simp
+next
+ case (Cons y ys) note Asm = Cons
+ show ?case
+ proof (cases xs)
+ case Nil
+ hence False using Asm(2) by simp
+ thus ?thesis ..
+ next
+ case (Cons x xs')
+ with Asm(2) have "map f xs' = map f ys" by auto
+ from Asm(1)[OF this] `xs = x#xs'` show ?thesis by simp
+ qed
+qed
+
+text{*\noindent
+The base case is trivial. In the step case Isar assumes
+(under the name @{text Cons}) two propositions:
+\begin{center}
+\begin{tabular}{l}
+@{text"map f ?xs = map f ys \<Longrightarrow> length ?xs = length ys"}\\
+@{prop"map f xs = map f (y # ys)"}
+\end{tabular}
+\end{center}
+The first is the induction hypothesis, the second, and this is new,
+is the premise of the induction step. The actual goal at this point is merely
+@{prop"length xs = length (y#ys)"}. The assumptions are given the new name
+@{text Asm} to avoid a name clash further down. The proof procedes with a case distinction on @{text xs}. In the case @{prop"xs = []"}, the second of our two
+assumptions (@{text"Asm(2)"}) implies the contradiction @{text"0 = Suc(\<dots>)"}.
+ In the case @{prop"xs = x#xs'"}, we first obtain
+@{prop"map f xs' = map f ys"}, from which a forward step with the first assumption (@{text"Asm(1)[OF this]"}) yields @{prop"length xs' = length ys"}. Together
+with @{prop"xs = x#xs"} this yields the goal
+@{prop"length xs = length (y#ys)"}.
+
+
+\subsection{Induction formulae involving @{text"\<And>"} or @{text"\<Longrightarrow>"}}
+\label{sec:full-Ind}
+
+Let us now consider abstractly the situation where the goal to be proved
+contains both @{text"\<And>"} and @{text"\<Longrightarrow>"}, say @{prop"\<And>x. P x \<Longrightarrow> Q x"}.
+This means that in each case of the induction,
@{text ?case} would be of the form @{prop"\<And>x. P' x \<Longrightarrow> Q' x"}. Thus the
first proof steps will be the canonical ones, fixing @{text x} and assuming
-@{prop"P' x"}. To avoid this tedium, induction performs these steps
-automatically: for example in case @{text"(Suc n)"}, @{text ?case} is only
-@{prop"Q' x"} whereas the assumptions (named @{term Suc}!) contain both the
-usual induction hypothesis \emph{and} @{prop"P' x"}.
-It should be clear how this generalises to more complex formulae.
-
-As an example we will now prove complete induction via
-structural induction. *}
+@{prop"P' x"}. To avoid this tedium, induction performs the canonical steps
+automatically: in each step case, the assumptions contain both the
+usual induction hypothesis and @{prop"P' x"}, whereas @{text ?case} is only
+@{prop"Q' x"}.
-lemma assumes A: "(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
- shows "P(n::nat)"
-proof (rule A)
- show "\<And>m. m < n \<Longrightarrow> P m"
- proof (induct n)
- case 0 thus ?case by simp
- next
- case (Suc n) -- {*\isakeyword{fix} @{term m} \isakeyword{assume} @{text Suc}: @{text[source]"?m < n \<Longrightarrow> P ?m"} @{prop[source]"m < Suc n"}*}
- show ?case -- {*@{term ?case}*}
- proof cases
- assume eq: "m = n"
- from Suc and A have "P n" by blast
- with eq show "P m" by simp
- next
- assume "m \<noteq> n"
- with Suc have "m < n" by arith
- thus "P m" by(rule Suc)
- qed
- qed
-qed
-text{* \noindent Given the explanations above and the comments in the
-proof text (only necessary for novices), the proof should be quite
-readable.
+\subsection{Rule induction}
-The statement of the lemma is interesting because it deviates from the style in
-the Tutorial~\cite{LNCS2283}, which suggests to introduce @{text"\<forall>"} or
-@{text"\<longrightarrow>"} into a theorem to strengthen it for induction. In Isar
-proofs we can use @{text"\<And>"} and @{text"\<Longrightarrow>"} instead. This simplifies the
-proof and means we do not have to convert between the two kinds of
-connectives.
-
-Note that in a nested induction over the same data type, the inner
-case labels hide the outer ones of the same name. If you want to refer
-to the outer ones inside, you need to name them on the outside, e.g.\
-\isakeyword{note}~@{text"outer_IH = Suc"}. *}
-
-subsection{*Rule induction*}
-
-text{* HOL also supports inductively defined sets. See \cite{LNCS2283}
+HOL also supports inductively defined sets. See \cite{LNCS2283}
for details. As an example we define our own version of the reflexive
transitive closure of a relation --- HOL provides a predefined one as well.*}
inductive_set
@@ -209,42 +250,41 @@
However, this proof is rather terse. Here is a more readable version:
*}
-lemma assumes A: "(x,y) \<in> r*" and B: "(y,z) \<in> r*"
- shows "(x,z) \<in> r*"
-proof -
- from A B show ?thesis
- proof induct
- fix x assume "(x,z) \<in> r*" -- {*@{text B}[@{text y} := @{text x}]*}
- thus "(x,z) \<in> r*" .
- next
- fix x' x y
- assume 1: "(x',x) \<in> r" and
- IH: "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*" and
- B: "(y,z) \<in> r*"
- from 1 IH[OF B] show "(x',z) \<in> r*" by(rule rtc.step)
- qed
+lemma assumes "(x,y) \<in> r*" and "(y,z) \<in> r*" shows "(x,z) \<in> r*"
+using assms
+proof induct
+ fix x assume "(x,z) \<in> r*" -- {*@{text B}[@{text y} := @{text x}]*}
+ thus "(x,z) \<in> r*" .
+next
+ fix x' x y
+ assume 1: "(x',x) \<in> r" and
+ IH: "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*" and
+ B: "(y,z) \<in> r*"
+ from 1 IH[OF B] show "(x',z) \<in> r*" by(rule rtc.step)
qed
-text{*\noindent We start the proof with \isakeyword{from}~@{text"A
-B"}. Only @{text A} is ``consumed'' by the induction step.
-Since @{text B} is left over we don't just prove @{text
-?thesis} but @{text"B \<Longrightarrow> ?thesis"}, just as in the previous proof. The
-base case is trivial. In the assumptions for the induction step we can
+text{*\noindent
+This time, merely for a change, we start the proof with by feeding both
+assumptions into the inductive proof. Only the first assumption is
+``consumed'' by the induction.
+Since the second one is left over we don't just prove @{text ?thesis} but
+@{text"(y,z) \<in> r* \<Longrightarrow> ?thesis"}, just as in the previous proof.
+The base case is trivial. In the assumptions for the induction step we can
see very clearly how things fit together and permit ourselves the
obvious forward step @{text"IH[OF B]"}.
-The notation `\isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)}'
-is also supported for inductive definitions. The \emph{constructor} is (the
-name of) the rule and the \emph{vars} fix the free variables in the
+The notation \isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)}
+is also supported for inductive definitions. The \emph{constructor} is the
+name of the rule and the \emph{vars} fix the free variables in the
rule; the order of the \emph{vars} must correspond to the
-\emph{alphabetical order} of the variables as they appear in the rule.
+left-to-right order of the variables as they appear in the rule.
For example, we could start the above detailed proof of the induction
-with \isakeyword{case}~\isa{(step x' x y)}. However, we can then only
-refer to the assumptions named \isa{step} collectively and not
-individually, as the above proof requires. *}
+with \isakeyword{case}~\isa{(step x' x y)}. In that case we don't need
+to spell out the assumptions but can refer to them by @{text"step(.)"},
+although the resulting text will be quite cryptic.
-subsection{*More induction*}
+\subsection{More induction}
-text{* We close the section by demonstrating how arbitrary induction
+We close the section by demonstrating how arbitrary induction
rules are applied. As a simple example we have chosen recursion
induction, i.e.\ induction based on a recursive function
definition. However, most of what we show works for induction in
@@ -252,17 +292,16 @@
The example is an unusual definition of rotation: *}
-consts rot :: "'a list \<Rightarrow> 'a list"
-recdef rot "measure length" --"for the internal termination proof"
-"rot [] = []"
-"rot [x] = [x]"
+fun rot :: "'a list \<Rightarrow> 'a list" where
+"rot [] = []" |
+"rot [x] = [x]" |
"rot (x#y#zs) = y # rot(x#zs)"
text{*\noindent This yields, among other things, the induction rule
@{thm[source]rot.induct}: @{thm[display]rot.induct[no_vars]}
-In the following proof we rely on a default naming scheme for cases: they are
+The following proof relies on a default naming scheme for cases: they are
called 1, 2, etc, unless they have been named explicitly. The latter happens
-only with datatypes and inductively defined sets, but not with recursive
-functions. *}
+only with datatypes and inductively defined sets, but (usually)
+not with recursive functions. *}
lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"
proof (induct xs rule: rot.induct)
@@ -280,11 +319,11 @@
text{*\noindent
The third case is only shown in gory detail (see \cite{BauerW-TPHOLs01}
for how to reason with chains of equations) to demonstrate that the
-`\isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)}' notation also
+\isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)} notation also
works for arbitrary induction theorems with numbered cases. The order
of the \emph{vars} corresponds to the order of the
@{text"\<And>"}-quantified variables in each case of the induction
-theorem. For induction theorems produced by \isakeyword{recdef} it is
+theorem. For induction theorems produced by \isakeyword{fun} it is
the order in which the variables appear on the left-hand side of the
equation.
@@ -295,3 +334,25 @@
by (induct xs rule: rot.induct, simp_all)
(*<*)end(*>*)
+(*
+lemma assumes A: "(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
+ shows "P(n::nat)"
+proof (rule A)
+ show "\<And>m. m < n \<Longrightarrow> P m"
+ proof (induct n)
+ case 0 thus ?case by simp
+ next
+ case (Suc n) -- {*\isakeyword{fix} @{term m} \isakeyword{assume} @{text Suc}: @{text[source]"?m < n \<Longrightarrow> P ?m"} @{prop[source]"m < Suc n"}*}
+ show ?case -- {*@{term ?case}*}
+ proof cases
+ assume eq: "m = n"
+ from Suc and A have "P n" by blast
+ with eq show "P m" by simp
+ next
+ assume "m \<noteq> n"
+ with Suc have "m < n" by arith
+ thus "P m" by(rule Suc)
+ qed
+ qed
+qed
+*)
\ No newline at end of file