# HG changeset patch
# User nipkow
# Date 1194806486 -3600
# Node ID 359b179fc9635c8c19d7e57fe9ba4f494c29abf8
# Parent  0a1005435e110e72bd1cf115ebcdcffa8e91b123
updates

diff -r 0a1005435e11 -r 359b179fc963 doc-src/IsarOverview/Isar/Induction.thy
--- 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
diff -r 0a1005435e11 -r 359b179fc963 doc-src/IsarOverview/Isar/document/Induction.tex
--- a/doc-src/IsarOverview/Isar/document/Induction.tex	Sun Nov 11 17:18:38 2007 +0100
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Sun Nov 11 19:41:26 2007 +0100
@@ -165,15 +165,10 @@
 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.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Structural induction%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
+of this.
+
+\subsection{Structural induction}
+
 We start with an inductive proof where both cases are proved automatically:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -311,33 +306,82 @@
 \begin{isamarkuptext}%
 \noindent Of course we could again have written
 \isakeyword{thus}~\isa{{\isacharquery}case} instead of giving the term explicitly
-but we wanted to use \isa{i} somewhere.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Induction formulae involving \isa{{\isasymAnd}} or \isa{{\isasymLongrightarrow}}\label{sec:full-Ind}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Let us now consider the situation where the goal to be proved contains
-\isa{{\isasymAnd}} or \isa{{\isasymLongrightarrow}}, say \isa{{\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ Q\ x} --- motivation and a
-real example follow shortly.  This means that in each case of the induction,
-\isa{{\isacharquery}case} would be of the form \isa{{\isasymAnd}x{\isachardot}\ P{\isacharprime}\ x\ {\isasymLongrightarrow}\ Q{\isacharprime}\ x}.  Thus the
-first proof steps will be the canonical ones, fixing \isa{x} and assuming
-\isa{P{\isacharprime}\ x}. To avoid this tedium, induction performs these steps
-automatically: for example in case \isa{{\isacharparenleft}Suc\ n{\isacharparenright}}, \isa{{\isacharquery}case} is only
-\isa{Q{\isacharprime}\ x} whereas the assumptions (named \isa{Suc}!) contain both the
-usual induction hypothesis \emph{and} \isa{P{\isacharprime}\ x}.
-It should be clear how this generalises to more complex formulae.
+but we wanted to use \isa{i} somewhere.
+
+\subsection{Generalization via \isa{arbitrary}}
 
-As an example we will now prove complete induction via
-structural induction.%
+It is frequently necessary to generalize a claim before it becomes
+provable by induction. The tutorial~\cite{LNCS2283} demonstrates this
+with \isa{itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys}, where \isa{ys}
+needs to be universally quantified before induction succeeds.\footnote{\isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}},\quad \isa{rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}},\\ \isa{itrev\ {\isacharbrackleft}{\isacharbrackright}\ ys\ {\isacharequal}\ ys},\quad \isa{itrev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharequal}\ itrev\ xs\ {\isacharparenleft}x\ {\isacharhash}\ ys{\isacharparenright}}} 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:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isacharparenleft}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{shows}\ {\isachardoublequoteopen}P{\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs\ arbitrary{\isacharcolon}\ ys{\isacharparenright}\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent The annotation \isa{arbitrary{\isacharcolon}}~\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.
+
+The nice thing about generalization via \isa{arbitrary{\isacharcolon}} is that in
+the induction step the claim is available in unquantified form but
+with the generalized variables replaced by \isa{{\isacharquery}}-variables, ready
+for instantiation. In the above example the
+induction hypothesis is \isa{itrev\ xs\ {\isacharquery}ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharquery}ys}.
+
+For the curious: \isa{arbitrary{\isacharcolon}} introduces \isa{{\isasymAnd}}
+behind the scenes.
+
+\subsection{Inductive proofs of conditional formulae}
+
+Induction also copes well with formulae involving \isa{{\isasymLongrightarrow}}, for example%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ auto%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent This is an improvement over that style the
+tutorial~\cite{LNCS2283} advises, which requires \isa{{\isasymlongrightarrow}}.
+A further improvement is shown in the following proof:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ \ {\isachardoublequoteopen}map\ f\ xs\ {\isacharequal}\ map\ f\ ys\ {\isasymLongrightarrow}\ length\ xs\ {\isacharequal}\ length\ ys{\isachardoublequoteclose}\isanewline
 %
 \isadelimproof
 %
@@ -345,52 +389,41 @@
 %
 \isatagproof
 \isacommand{proof}\isamarkupfalse%
-\ {\isacharparenleft}rule\ A{\isacharparenright}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{proof}\isamarkupfalse%
-\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{case}\isamarkupfalse%
-\ {\isadigit{0}}\ \isacommand{thus}\isamarkupfalse%
+\ {\isacharparenleft}induct\ ys\ arbitrary{\isacharcolon}\ xs{\isacharparenright}\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ Nil\ \isacommand{thus}\isamarkupfalse%
 \ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ {\isacharparenleft}Cons\ y\ ys{\isacharparenright}\ \ \isacommand{note}\isamarkupfalse%
+\ Asm\ {\isacharequal}\ Cons\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}case\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\ {\isacharparenleft}cases\ xs{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{case}\isamarkupfalse%
+\ Nil\isanewline
+\ \ \ \ \isacommand{hence}\isamarkupfalse%
+\ False\ \isacommand{using}\isamarkupfalse%
+\ Asm{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \ \ \isacommand{thus}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
 \ \ \isacommand{next}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{case}\isamarkupfalse%
-\ {\isacharparenleft}Suc\ n{\isacharparenright}\ \ \ %
-\isamarkupcmt{\isakeyword{fix} \isa{m} \isakeyword{assume} \isa{Suc}: \isa{{\isachardoublequote}{\isacharquery}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ {\isacharquery}m{\isachardoublequote}} \isa{{\isachardoublequote}m\ {\isacharless}\ Suc\ n{\isachardoublequote}}%
-}
-\isanewline
-\ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}case\ \ \ \ %
-\isamarkupcmt{\isa{P\ m}%
-}
-\isanewline
-\ \ \ \ \isacommand{proof}\isamarkupfalse%
-\ cases\isanewline
-\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ eq{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
-\ Suc\ \isakeyword{and}\ A\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}P\ n{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
-\ eq\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}P\ m{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}Cons\ x\ xs{\isacharprime}{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{with}\isamarkupfalse%
+\ Asm{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}map\ f\ xs{\isacharprime}\ {\isacharequal}\ map\ f\ ys{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ auto\isanewline
+\ \ \ \ \isacommand{from}\isamarkupfalse%
+\ Asm{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}OF\ this{\isacharbrackright}\ {\isacharbackquoteopen}xs\ {\isacharequal}\ x{\isacharhash}xs{\isacharprime}{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
-\ \ \ \ \isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}m\ {\isasymnoteq}\ n{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
-\ Suc\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}m\ {\isacharless}\ n{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ arith\isanewline
-\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
-\ {\isachardoublequoteopen}P\ m{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-{\isacharparenleft}rule\ Suc{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
-\isanewline
 \ \ \isacommand{qed}\isamarkupfalse%
 \isanewline
 \isacommand{qed}\isamarkupfalse%
@@ -403,29 +436,41 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-\noindent Given the explanations above and the comments in the
-proof text (only necessary for novices), the proof should be quite
-readable.
-
-The statement of the lemma is interesting because it deviates from the style in
-the Tutorial~\cite{LNCS2283}, which suggests to introduce \isa{{\isasymforall}} or
-\isa{{\isasymlongrightarrow}} into a theorem to strengthen it for induction. In Isar
-proofs we can use \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} instead. This simplifies the
-proof and means we do not have to convert between the two kinds of
-connectives.
+\noindent
+The base case is trivial. In the step case Isar assumes
+(under the name \isa{Cons}) two propositions:
+\begin{center}
+\begin{tabular}{l}
+\isa{map\ f\ {\isacharquery}xs\ {\isacharequal}\ map\ f\ ys\ {\isasymLongrightarrow}\ length\ {\isacharquery}xs\ {\isacharequal}\ length\ ys}\\
+\isa{map\ f\ xs\ {\isacharequal}\ map\ f\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}}
+\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
+\isa{length\ xs\ {\isacharequal}\ length\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}}. The assumptions are given the new name
+\isa{Asm} to avoid a name clash further down. The proof procedes with a case distinction on \isa{xs}. In the case \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, the second of our two
+assumptions (\isa{Asm{\isacharparenleft}{\isadigit{2}}{\isacharparenright}}) implies the contradiction \isa{{\isadigit{0}}\ {\isacharequal}\ Suc{\isacharparenleft}{\isasymdots}{\isacharparenright}}.
+ In the case \isa{xs\ {\isacharequal}\ x\ {\isacharhash}\ xs{\isacharprime}}, we first obtain
+\isa{map\ f\ xs{\isacharprime}\ {\isacharequal}\ map\ f\ ys}, from which a forward step with the first assumption (\isa{Asm{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}OF\ this{\isacharbrackright}}) yields \isa{length\ xs{\isacharprime}\ {\isacharequal}\ length\ ys}. Together
+with \isa{xs\ {\isacharequal}\ x\ {\isacharhash}\ xs} this yields the goal
+\isa{length\ xs\ {\isacharequal}\ length\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}}.
 
-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}~\isa{outer{\isacharunderscore}IH\ {\isacharequal}\ Suc}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Rule induction%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
+
+\subsection{Induction formulae involving \isa{{\isasymAnd}} or \isa{{\isasymLongrightarrow}}}
+\label{sec:full-Ind}
+
+Let us now consider abstractly the situation where the goal to be proved
+contains both \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}}, say \isa{{\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ Q\ x}.
+This means that in each case of the induction,
+\isa{{\isacharquery}case} would be of the form \isa{{\isasymAnd}x{\isachardot}\ P{\isacharprime}\ x\ {\isasymLongrightarrow}\ Q{\isacharprime}\ x}.  Thus the
+first proof steps will be the canonical ones, fixing \isa{x} and assuming
+\isa{P{\isacharprime}\ x}. To avoid this tedium, induction performs the canonical steps
+automatically: in each step case, the assumptions contain both the
+usual induction hypothesis and \isa{P{\isacharprime}\ x}, whereas \isa{{\isacharquery}case} is only
+\isa{Q{\isacharprime}\ 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.%
@@ -487,44 +532,38 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isakeyword{and}\ B{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
+\ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
+\isacommand{using}\isamarkupfalse%
+\ assms\isanewline
 \isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \isacommand{from}\isamarkupfalse%
-\ A\ B\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis\isanewline
-\ \ \isacommand{proof}\isamarkupfalse%
 \ induct\isanewline
-\ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ \ \isacommand{fix}\isamarkupfalse%
 \ x\ \isacommand{assume}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \ %
 \isamarkupcmt{\isa{B}[\isa{y} := \isa{x}]%
 }
 \isanewline
-\ \ \ \ \isacommand{thus}\isamarkupfalse%
+\ \ \isacommand{thus}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
 \isanewline
-\ \ \isacommand{next}\isamarkupfalse%
+\isacommand{next}\isamarkupfalse%
 \isanewline
-\ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ \ \isacommand{fix}\isamarkupfalse%
 \ x{\isacharprime}\ x\ y\isanewline
-\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ \ \isacommand{assume}\isamarkupfalse%
 \ {\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharprime}{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ IH{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ B{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{from}\isamarkupfalse%
+\ \ \ \ \ \ \ \ \ IH{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
+\ \ \ \ \ \ \ \ \ B{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{from}\isamarkupfalse%
 \ {\isadigit{1}}\ IH{\isacharbrackleft}OF\ B{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharprime}{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 {\isacharparenleft}rule\ rtc{\isachardot}step{\isacharparenright}\isanewline
-\ \ \isacommand{qed}\isamarkupfalse%
-\isanewline
 \isacommand{qed}\isamarkupfalse%
 %
 \endisatagproof
@@ -535,29 +574,28 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-\noindent We start the proof with \isakeyword{from}~\isa{A\ B}. Only \isa{A} is ``consumed'' by the induction step.
-Since \isa{B} is left over we don't just prove \isa{{\isacharquery}thesis} but \isa{B\ {\isasymLongrightarrow}\ {\isacharquery}thesis}, just as in the previous proof. The
-base case is trivial. In the assumptions for the induction step we can
+\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 \isa{{\isacharquery}thesis} but
+\isa{{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharquery}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 \isa{IH{\isacharbrackleft}OF\ B{\isacharbrackright}}.
 
-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.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{More induction%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
+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 \isa{step{\isacharparenleft}{\isachardot}{\isacharparenright}},
+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
@@ -567,25 +605,20 @@
 The example is an unusual definition of rotation:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ rot\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
-\isacommand{recdef}\isamarkupfalse%
-\ rot\ {\isachardoublequoteopen}measure\ length{\isachardoublequoteclose}\ \ %
-\isamarkupcmt{for the internal termination proof%
-}
-\isanewline
-{\isachardoublequoteopen}rot\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}rot\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\isacommand{fun}\isamarkupfalse%
+\ rot\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+{\isachardoublequoteopen}rot\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
+{\isachardoublequoteopen}rot\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
 {\isachardoublequoteopen}rot\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y\ {\isacharhash}\ rot{\isacharparenleft}x{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent This yields, among other things, the induction rule
 \isa{rot{\isachardot}induct}: \begin{isabelle}%
-{\isasymlbrakk}P\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ P\ {\isacharbrackleft}x{\isacharbrackright}{\isacharsemicolon}\ {\isasymAnd}x\ y\ zs{\isachardot}\ P\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x%
+{\isasymlbrakk}P\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ P\ {\isacharbrackleft}x{\isacharbrackright}{\isacharsemicolon}\ {\isasymAnd}x\ y\ zs{\isachardot}\ P\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ a{\isadigit{0}}%
 \end{isabelle}
-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.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
@@ -640,11 +673,11 @@
 \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
 \isa{{\isasymAnd}}-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.
 
diff -r 0a1005435e11 -r 359b179fc963 doc-src/IsarOverview/Isar/document/root.bib
--- a/doc-src/IsarOverview/Isar/document/root.bib	Sun Nov 11 17:18:38 2007 +0100
+++ b/doc-src/IsarOverview/Isar/document/root.bib	Sun Nov 11 19:41:26 2007 +0100
@@ -48,5 +48,5 @@
 
 @article{WenzelW-JAR,author={Markus Wenzel and Freek Wiedijk},
 title={A comparison of the mathematical proof languages {Mizar} and {Isar}},
-journal=JAR,year=2003,note={To appear}}
+journal=JAR,year=2002,pages={389--411}}
 
diff -r 0a1005435e11 -r 359b179fc963 doc-src/IsarOverview/Isar/document/root.tex
--- a/doc-src/IsarOverview/Isar/document/root.tex	Sun Nov 11 17:18:38 2007 +0100
+++ b/doc-src/IsarOverview/Isar/document/root.tex	Sun Nov 11 19:41:26 2007 +0100
@@ -33,12 +33,6 @@
 \input{Logic.tex}
 \input{Induction.tex}
 
-\small
-\paragraph{Acknowledgement}
-I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin,
-Gertrud Bauer, Stefan Berghofer, Gerwin Klein, Norbert Schirmer,
-Markus Wenzel and Freek Wiedijk commented on and improved this paper.
-
 \begingroup
 \bibliographystyle{plain} \small\raggedright\frenchspacing
 \bibliography{root}