--- a/doc-src/IsarOverview/Isar/Induction.thy Wed Apr 04 10:04:25 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,357 +0,0 @@
-(*<*)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}*}
-
-text{* Computer science applications abound with inductively defined
-structures, which is why we treat them in more detail. HOL already
-comes with a datatype of lists with the two constructors @{text Nil}
-and @{text Cons}. @{text Nil} is written @{term"[]"} and @{text"Cons x
-xs"} is written @{term"x # xs"}. *}
-
-subsection{*Case distinction\label{sec:CaseDistinction}*}
-
-text{* We have already met the @{text cases} method for performing
-binary case splits. Here is another example: *}
-lemma "\<not> A \<or> A"
-proof cases
- assume "A" thus ?thesis ..
-next
- assume "\<not> A" thus ?thesis ..
-qed
-
-text{*\noindent The two cases must come in this order because @{text
-cases} merely abbreviates @{text"(rule case_split)"} where
-@{thm[source] case_split} is @{thm case_split}. If we reverse
-the order of the two cases in the proof, the first case would prove
-@{prop"\<not> A \<Longrightarrow> \<not> A \<or> A"} which would solve the first premise of
-@{thm[source] case_split}, instantiating @{text ?P} with @{term "\<not>
-A"}, thus making the second premise @{prop"\<not> \<not> A \<Longrightarrow> \<not> A \<or> A"}.
-Therefore the order of subgoals is not always completely arbitrary.
-
-The above proof is appropriate if @{term A} is textually small.
-However, if @{term A} is large, we do not want to repeat it. This can
-be avoided by the following idiom *}
-
-lemma "\<not> A \<or> A"
-proof (cases "A")
- case True thus ?thesis ..
-next
- case False thus ?thesis ..
-qed
-
-text{*\noindent which is like the previous proof but instantiates
-@{text ?P} right away with @{term A}. Thus we could prove the two
-cases in any order. The phrase \isakeyword{case}~@{text True}
-abbreviates \isakeyword{assume}~@{text"True: A"} and analogously for
-@{text"False"} and @{prop"\<not>A"}.
-
-The same game can be played with other datatypes, for example lists,
-where @{term tl} is the tail of a list, and @{text length} returns a
-natural number (remember: $0-1=0$):
-*}
-(*<*)declare length_tl[simp del](*>*)
-lemma "length(tl xs) = length xs - 1"
-proof (cases xs)
- case Nil thus ?thesis by simp
-next
- case Cons thus ?thesis by simp
-qed
-text{*\noindent Here \isakeyword{case}~@{text Nil} abbreviates
-\isakeyword{assume}~@{text"Nil:"}~@{prop"xs = []"} and
-\isakeyword{case}~@{text Cons} abbreviates \isakeyword{fix}~@{text"? ??"}
-\isakeyword{assume}~@{text"Cons:"}~@{text"xs = ? # ??"},
-where @{text"?"} and @{text"??"}
-stand for variable names that have been chosen by the system.
-Therefore we cannot refer to them.
-Luckily, this proof is simple enough we do not need to refer to them.
-However, sometimes one may have to. Hence Isar offers a simple scheme for
-naming those variables: replace the anonymous @{text Cons} by
-@{text"(Cons y ys)"}, which abbreviates \isakeyword{fix}~@{text"y ys"}
-\isakeyword{assume}~@{text"Cons:"}~@{text"xs = y # ys"}.
-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.
-
-\subsection{Structural induction}
-
-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
-
-text{*\noindent The constraint @{text"::nat"} is needed because all of
-the operations involved are overloaded.
-This proof also demonstrates that \isakeyword{by} can take two arguments,
-one to start and one to finish the proof --- the latter is optional.
-
-If we want to expose more of the structure of the
-proof, we can use pattern matching to avoid having to repeat the goal
-statement: *}
-lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)" (is "?P n")
-proof (induct n)
- show "?P 0" by simp
-next
- fix n assume "?P n"
- thus "?P(Suc n)" by simp
-qed
-
-text{* \noindent We could refine this further to show more of the equational
-proof. Instead we explore the same avenue as for case distinctions:
-introducing context via the \isakeyword{case} command: *}
-lemma "2 * (\<Sum>i::nat \<le> n. i) = n*(n+1)"
-proof (induct n)
- case 0 show ?case by simp
-next
- case Suc thus ?case by simp
-qed
-
-text{* \noindent The implicitly defined @{text ?case} refers to the
-corresponding case to be proved, i.e.\ @{text"?P 0"} in the first case and
-@{text"?P(Suc n)"} in the second case. Context \isakeyword{case}~@{text 0} is
-empty whereas \isakeyword{case}~@{text Suc} assumes @{text"?P n"}. Again we
-have the same problem as with case distinctions: we cannot refer to an anonymous @{term n}
-in the induction step because it has not been introduced via \isakeyword{fix}
-(in contrast to the previous proof). The solution is the one outlined for
-@{text Cons} above: replace @{term Suc} by @{text"(Suc i)"}: *}
-lemma fixes n::nat shows "n < n*n + 1"
-proof (induct n)
- case 0 show ?case by simp
-next
- case (Suc i) thus "Suc i < Suc i * Suc i + 1" by simp
-qed
-
-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.
-
-\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) simp_all
-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.
-
-Generalization via @{text"arbitrary"} is particularly convenient
-if the induction step is a structured proof as opposed to the automatic
-example above. Then the claim is available in unquantified form but
-with the generalized variables replaced by @{text"?"}-variables, ready
-for instantiation. In the above example, in the @{const[source] Cons} case the
-induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"} (available
-under the name @{const[source] Cons}).
-
-
-\subsection{Inductive proofs of conditional formulae}
-\label{sec:full-Ind}
-
-Induction also copes well with formulae involving @{text"\<Longrightarrow>"}, for example
-*}
-
-lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
-by (induct xs) simp_all
-
-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:
-*}
-
-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 simp
- 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>"}}
-
-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 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"}.
-
-\subsection{Rule induction}
-
-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
- rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
- for r :: "('a \<times> 'a)set"
-where
- refl: "(x,x) \<in> r*"
-| step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
-
-text{* \noindent
-First the constant is declared as a function on binary
-relations (with concrete syntax @{term"r*"} instead of @{text"rtc
-r"}), then the defining clauses are given. We will now prove that
-@{term"r*"} is indeed transitive: *}
-
-lemma assumes A: "(x,y) \<in> r*" shows "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*"
-using A
-proof induct
- case refl thus ?case .
-next
- case step thus ?case by(blast intro: rtc.step)
-qed
-text{*\noindent Rule induction is triggered by a fact $(x_1,\dots,x_n)
-\in R$ piped into the proof, here \isakeyword{using}~@{text A}. The
-proof itself follows the inductive definition very
-closely: there is one case for each rule, and it has the same name as
-the rule, analogous to structural induction.
-
-However, this proof is rather terse. Here is a more readable version:
-*}
-
-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
-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
-rule; the order of the \emph{vars} must correspond to the
-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)}. 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}
-
-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
-general.
-
-The example is an unusual definition of rotation: *}
-
-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]}
-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 (usually)
-not with recursive functions. *}
-
-lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"
-proof (induct xs rule: rot.induct)
- case 1 thus ?case by simp
-next
- case 2 show ?case by simp
-next
- case (3 a b cs)
- have "rot (a # b # cs) = b # rot(a # cs)" by simp
- also have "\<dots> = b # tl(a # cs) @ [hd(a # cs)]" by(simp add:3)
- also have "\<dots> = tl (a # b # cs) @ [hd (a # b # cs)]" by simp
- finally show ?case .
-qed
-
-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
-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{fun} it is
-the order in which the variables appear on the left-hand side of the
-equation.
-
-The proof is so simple that it can be condensed to
-*}
-
-(*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
-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