# HG changeset patch
# User nipkow
# Date 1033397439 -7200
# Node ID 531f1f524848bd67cb410abd037c05132b990bf8
# Parent  55d32e76ef4e136f79cc51cdb036c250780ea9d8
*** empty log message ***

diff -r 55d32e76ef4e -r 531f1f524848 NEWS
--- a/NEWS	Mon Sep 30 16:48:15 2002 +0200
+++ b/NEWS	Mon Sep 30 16:50:39 2002 +0200
@@ -74,6 +74,9 @@
 
 * the simplifier trace now shows the names of the applied rewrite rules
 
+* induct over a !!-quantified statement (say !!x1..xn):
+  each "case" automatically performs "fix x1 .. xn" with exactly those names.
+
 * GroupTheory: converted to Isar theories, using locales with implicit structures;
 
 * Real/HahnBanach: updated and adapted to locales;
diff -r 55d32e76ef4e -r 531f1f524848 doc-src/TutorialI/IsarOverview/Isar/Calc.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Calc.thy	Mon Sep 30 16:48:15 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Calc.thy	Mon Sep 30 16:50:39 2002 +0200
@@ -1,5 +1,7 @@
 theory Calc = Main:
 
+subsection{* Chains of equalities *}
+
 axclass
   group < zero, plus, minus
   assoc:       "(x + y) + z = x + (y + z)"
@@ -17,6 +19,23 @@
   finally show ?thesis .
 qed
 
+subsection{* Inequalities and substitution *}
+
+lemmas distrib = zadd_zmult_distrib zadd_zmult_distrib2
+                 zdiff_zmult_distrib zdiff_zmult_distrib2
+declare numeral_2_eq_2[simp]
+
+
+lemma fixes a :: int shows "(a+b)\<twosuperior> \<le> 2*(a\<twosuperior> + b\<twosuperior>)"
+proof -
+       have "(a+b)\<twosuperior> \<le> (a+b)\<twosuperior> + (a-b)\<twosuperior>"  by simp
+  also have "(a+b)\<twosuperior> \<le> a\<twosuperior> + b\<twosuperior> + 2*a*b"  by(simp add:distrib)
+  also have "(a-b)\<twosuperior> = a\<twosuperior> + b\<twosuperior> - 2*a*b"  by(simp add:distrib)
+  finally show ?thesis by simp
+qed
+
+
+subsection{* More transitivity *}
 
 lemma assumes R: "(a,b) \<in> R" "(b,c) \<in> R" "(c,d) \<in> R"
       shows "(a,d) \<in> R\<^sup>*"
diff -r 55d32e76ef4e -r 531f1f524848 doc-src/TutorialI/IsarOverview/Isar/Induction.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/IsarOverview/Isar/Induction.thy	Mon Sep 30 16:50:39 2002 +0200
@@ -0,0 +1,262 @@
+(*<*)theory Induction = Main:(*>*)
+
+section{*Case distinction and induction \label{sec:Induct}*}
+
+
+subsection{*Case distinction*}
+
+text{* We have already met the @{text cases} method for performing
+binary case splits. Here is another example: *}
+lemma "P \<or> \<not> P"
+proof cases
+  assume "P" thus ?thesis ..
+next
+  assume "\<not> P" thus ?thesis ..
+qed
+text{*\noindent Note that the two cases must come in this order.
+
+This form is appropriate if @{term P} is textually small.  However, if
+@{term P} is large, we don't want to repeat it. This can be avoided by
+the following idiom *}
+
+lemma "P \<or> \<not> P"
+proof (cases "P")
+  case True thus ?thesis ..
+next
+  case False thus ?thesis ..
+qed
+text{*\noindent which is simply a shorthand for the previous
+proof. More precisely, the phrases \isakeyword{case}~@{prop
+True}/@{prop False} abbreviate the corresponding assumptions @{prop P}
+and @{prop"\<not>P"}. In contrast to the previous proof we can prove the cases
+in arbitrary order.
+
+The same game can be played with other datatypes, for example lists:
+*}
+(*<*)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}~@{prop"xs = []"} and \isakeyword{case}~@{text Cons}
+abbreviates \isakeyword{fix}~@{text"? ??"}
+\isakeyword{assume}~@{text"xs = ? # ??"} where @{text"?"} and @{text"??"}
+stand for variable names that have been chosen by the system.
+Therefore we cannot
+refer to them (this would lead to obscure proofs) and have not even shown
+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, for example,
+@{text"(Cons y ys)"}, which abbreviates \isakeyword{fix}~@{text"y ys"}
+\isakeyword{assume}~@{text"xs = Cons y ys"}, i.e.\ @{prop"xs = y # ys"}. Here
+is a (somewhat contrived) example: *}
+
+lemma "length(tl xs) = length xs - 1"
+proof (cases xs)
+  case Nil thus ?thesis by simp
+next
+  case (Cons y ys)
+  hence "length(tl xs) = length ys  \<and>  length xs = length ys + 1"
+    by simp
+  thus ?thesis by simp
+qed
+
+
+subsection{*Structural induction*}
+
+text{* We start with a simple inductive proof where both cases are proved automatically: *}
+lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)"
+by (induct n, simp_all)
+
+text{*\noindent 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<n+1. 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<n+1. 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 same as 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{*Induction formulae involving @{text"\<And>"} or @{text"\<Longrightarrow>"}*}
+
+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,
+@{text ?case} would be of the same 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"}. To fix the name of the
+bound variable @{term x} you may write @{text"(Suc n x)"}, thus abbreviating
+\isakeyword{fix}~@{term x}.
+It should be clear how this example generalizes to more complex formulae.
+
+As a concrete example we will now prove complete induction via
+structural induction: *}
+
+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 m)    -- {*@{text"?m < n \<Longrightarrow> P ?m"}  and  @{prop"m < Suc n"}*}
+    show ?case       -- {*@{term ?case}*}
+    proof cases
+      assume eq: "m = n"
+      from Suc 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, 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 @{text"\<forall>"} or
+@{text"\<longrightarrow>"} into a theorem to strengthen it for induction. In structured 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.
+*}
+
+subsection{*Rule induction*}
+
+text{* We define our own version of reflexive transitive closure of a
+relation *}
+consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)
+inductive "r*"
+intros
+refl:  "(x,x) \<in> r*"
+step:  "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
+
+text{* \noindent and 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 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
+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
+see very clearly how things fit together and permit ourselves the
+obvious forward step @{text"IH[OF B]"}. *}
+
+subsection{*More induction*}
+
+text{* 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. The example is an unusual
+definition of rotation: *}
+
+consts rot :: "'a list \<Rightarrow> 'a list"
+recdef rot "measure length"
+"rot [] = []"
+"rot [x] = [x]"
+"rot (x#y#zs) = y # rot(x#zs)"
+
+text{* In the first proof we set up each case explicitly, merely using
+pattern matching to abbreviate the statement: *}
+
+lemma "length(rot xs) = length xs" (is "?P xs")
+proof (induct xs rule: rot.induct)
+  show "?P []" by simp
+next
+  fix x show "?P [x]" by simp
+next
+  fix x y zs assume "?P (x#zs)"
+  thus "?P (x#y#zs)" by simp
+qed
+text{*\noindent
+This proof skeleton works for arbitrary induction rules, not just
+@{thm[source]rot.induct}.
+
+In the following proof we rely 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. *}
+
+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 thus ?case by simp
+qed
+
+text{*\noindent Why can case 2 get away with \isakeyword{show} instead of
+\isakeyword{thus}?
+
+Of course both proofs are so simple that they can be condensed to*}
+(*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
+by (induct xs rule: rot.induct, simp_all)
+(*<*)end(*>*)
diff -r 55d32e76ef4e -r 531f1f524848 doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Mon Sep 30 16:48:15 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Mon Sep 30 16:50:39 2002 +0200
@@ -1,50 +1,6 @@
 (*<*)theory Logic = Main:(*>*)
-text{* We begin by looking at a simplified grammar for Isar proofs
-where parentheses are used for grouping and $^?$ indicates an optional item:
-\begin{center}
-\begin{tabular}{lrl}
-\emph{proof} & ::= & \isakeyword{proof} \emph{method}$^?$
-                     \emph{statement}*
-                     \isakeyword{qed} \\
-                 &$\mid$& \isakeyword{by} \emph{method}\\[1ex]
-\emph{statement} &::= & \isakeyword{fix} \emph{variables} \\
-             &$\mid$& \isakeyword{assume} \emph{propositions} \\
-             &$\mid$& (\isakeyword{from} \emph{facts})$^?$ 
-                    (\isakeyword{show} $\mid$ \isakeyword{have})
-                      \emph{propositions} \emph{proof} \\[1ex]
-\emph{proposition} &::=& (\emph{label}{\bf:})$^?$ \emph{string} \\[1ex]
-\emph{fact} &::=& \emph{label}
-\end{tabular}
-\end{center}
 
-This is a typical proof skeleton:
-\begin{center}
-\begin{tabular}{@ {}ll}
-\isakeyword{proof}\\
-\hspace*{3ex}\isakeyword{assume} @{text"\""}\emph{the-assm}@{text"\""}\\
-\hspace*{3ex}\isakeyword{have} @{text"\""}\dots@{text"\""}  & --- intermediate result\\
-\hspace*{3ex}\vdots\\
-\hspace*{3ex}\isakeyword{have} @{text"\""}\dots@{text"\""}  & --- intermediate result\\
-\hspace*{3ex}\isakeyword{show} @{text"\""}\emph{the-concl}@{text"\""}\\
-\isakeyword{qed}
-\end{tabular}
-\end{center}
-It proves \emph{the-assm}~@{text"\<Longrightarrow>"}~\emph{the-concl}.
-Text starting with ``---'' is a comment.
-
-Note that \emph{propositions} (following \isakeyword{assume} etc)
-may but need not be
-separated by \isakeyword{and}, whose purpose is to structure them
-into possibly named blocks. For example in
-\begin{center}
-\isakeyword{assume} @{text"A:"} $A_1$ $A_2$ \isakeyword{and} @{text"B:"} $A_3$
-\isakeyword{and} $A_4$
-\end{center}
-label @{text A} refers to the list of propositions $A_1$ $A_2$ and
-label @{text B} to $A_3$.
-*}
-
-section{*Logic*}
+section{*Logic \label{sec:Logic}*}
 
 subsection{*Propositional logic*}
 
@@ -90,7 +46,7 @@
 by assumption: *}
 lemma "A \<longrightarrow> A \<and> A"
 proof
-  assume A
+  assume "A"
   show "A \<and> A" by(rule conjI)
 qed
 text{*\noindent A drawback of these implicit proofs by assumption is that it
@@ -103,7 +59,7 @@
 
 lemma "A \<longrightarrow> A \<and> A"
 proof
-  assume A
+  assume "A"
   show "A \<and> A" ..
 qed
 text{*\noindent
@@ -122,7 +78,7 @@
   assume AB: "A \<and> B"
   show "B \<and> A"
   proof (rule conjE[OF AB])  -- {*@{text"conjE[OF AB]"}: @{thm conjE[OF AB]} *}
-    assume A and B
+    assume "A" "B"
     show ?thesis ..
   qed
 qed
@@ -151,7 +107,7 @@
   assume AB: "A \<and> B"
   from AB show "B \<and> A"
   proof
-    assume A and B
+    assume "A" "B"
     show ?thesis ..
   qed
 qed
@@ -169,7 +125,7 @@
   assume "A \<and> B"
   from this show "B \<and> A"
   proof
-    assume A and B
+    assume "A" "B"
     show ?thesis ..
   qed
 qed
@@ -188,8 +144,8 @@
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
   assume ab: "A \<and> B"
-  from ab have a: A ..
-  from ab have b: B ..
+  from ab have a: "A" ..
+  from ab have b: "B" ..
   from b a show "B \<and> A" ..
 qed
 text{*\noindent
@@ -232,9 +188,9 @@
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
   assume ab: "A \<and> B"
-  from ab have B ..
+  from ab have "B" ..
   moreover
-  from ab have A ..
+  from ab have "A" ..
   ultimately show "B \<and> A" ..
 qed
 text{*\noindent You can combine any number of facts @{term A1} \dots\ @{term
@@ -255,10 +211,10 @@
     assume nn: "\<not> (\<not> A \<or> \<not> B)"
     have "\<not> A"
     proof
-      assume A
+      assume "A"
       have "\<not> B"
       proof
-        assume B
+        assume "B"
         have "A \<and> B" ..
         with n show False ..
       qed
@@ -279,7 +235,7 @@
 \begin{tabular}{lcl}
 \isakeyword{hence} &=& \isakeyword{then} \isakeyword{have} \\
 \isakeyword{with}~\emph{facts} &=&
-\isakeyword{from}~\emph{facts} \isakeyword{and} @{text this}
+\isakeyword{from}~\emph{facts} @{text this}
 \end{tabular}
 \end{center}
 *}
@@ -313,9 +269,9 @@
 lemma "large_A \<and> large_B \<Longrightarrow> large_B \<and> large_A"
       (is "?AB \<Longrightarrow> ?B \<and> ?A")
 proof
-  assume ?AB thus ?B ..
+  assume "?AB" thus "?B" ..
 next
-  assume ?AB thus ?A ..
+  assume "?AB" thus "?A" ..
 qed
 text{*\noindent Any formula may be followed by
 @{text"("}\isakeyword{is}~\emph{pattern}@{text")"} which causes the pattern
@@ -330,9 +286,9 @@
 lemma assumes AB: "large_A \<and> large_B"
   shows "large_B \<and> large_A" (is "?B \<and> ?A")
 proof
-  from AB show ?B ..
+  from AB show "?B" ..
 next
-  from AB show ?A ..
+  from AB show "?A" ..
 qed
 text{*\noindent Note the difference between @{text ?AB}, a term, and
 @{text AB}, a fact.
@@ -345,7 +301,7 @@
   shows "large_B \<and> large_A" (is "?B \<and> ?A")
 using AB
 proof
-  assume ?A and ?B show ?thesis ..
+  assume "?A" "?B" show ?thesis ..
 qed
 text{*\noindent Command \isakeyword{using} can appear before a proof
 and adds further facts to those piped into the proof. Here @{text AB}
@@ -361,7 +317,7 @@
 Sometimes it is necessary to suppress the implicit application of rules in a
 \isakeyword{proof}. For example \isakeyword{show}~@{prop"A \<or> B"} would
 trigger $\lor$-introduction, requiring us to prove @{prop A}. A simple
-``@{text"-"}'' prevents this \emph{faut pas}: *}
+``@{text"-"}'' prevents this \emph{faux pas}: *}
 
 lemma assumes AB: "A \<or> B" shows "B \<or> A"
 proof -
@@ -509,7 +465,7 @@
 
 lemma "A \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> B"
 proof
-  assume a: A
+  assume a: "A"
   show "(A \<longrightarrow>B) \<longrightarrow> B"
     apply(rule impI)
     apply(erule impE)
@@ -520,263 +476,4 @@
 text{*\noindent You may need to resort to this technique if an automatic step
 fails to prove the desired proposition. *}
 
-section{*Case distinction and induction*}
-
-
-subsection{*Case distinction*}
-
-text{* We have already met the @{text cases} method for performing
-binary case splits. Here is another example: *}
-lemma "P \<or> \<not> P"
-proof cases
-  assume "P" thus ?thesis ..
-next
-  assume "\<not> P" thus ?thesis ..
-qed
-text{*\noindent Note that the two cases must come in this order.
-
-This form is appropriate if @{term P} is textually small.  However, if
-@{term P} is large, we don't want to repeat it. This can be avoided by
-the following idiom *}
-
-lemma "P \<or> \<not> P"
-proof (cases "P")
-  case True thus ?thesis ..
-next
-  case False thus ?thesis ..
-qed
-text{*\noindent which is simply a shorthand for the previous
-proof. More precisely, the phrases \isakeyword{case}~@{prop
-True}/@{prop False} abbreviate the corresponding assumptions @{prop P}
-and @{prop"\<not>P"}. In contrast to the previous proof we can prove the cases
-in arbitrary order.
-
-The same game can be played with other datatypes, for example lists:
-*}
-(*<*)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}~@{prop"xs = []"} and \isakeyword{case}~@{text Cons}
-abbreviates \isakeyword{fix}~@{text"? ??"}
-\isakeyword{assume}~@{text"xs = ? # ??"} where @{text"?"} and @{text"??"}
-stand for variable names that have been chosen by the system.
-Therefore we cannot
-refer to them (this would lead to obscure proofs) and have not even shown
-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, for example,
-@{text"(Cons y ys)"}, which abbreviates \isakeyword{fix}~@{text"y ys"}
-\isakeyword{assume}~@{text"xs = Cons y ys"}, i.e.\ @{prop"xs = y # ys"}. Here
-is a (somewhat contrived) example: *}
-
-lemma "length(tl xs) = length xs - 1"
-proof (cases xs)
-  case Nil thus ?thesis by simp
-next
-  case (Cons y ys)
-  hence "length(tl xs) = length ys  \<and>  length xs = length ys + 1"
-    by simp
-  thus ?thesis by simp
-qed
-
-
-subsection{*Structural induction*}
-
-text{* We start with a simple inductive proof where both cases are proved automatically: *}
-lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)"
-by (induct n, simp_all)
-
-text{*\noindent 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<n+1. 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<n+1. 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 same as 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{*Induction formulae involving @{text"\<And>"} or @{text"\<Longrightarrow>"}*}
-
-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,
-@{text ?case} would be of the same 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"}. To fix the name of the
-bound variable @{term x} you may write @{text"(Suc n x)"}, thus abbreviating
-\isakeyword{fix}~@{term x}.
-It should be clear how this example generalizes to more complex formulae.
-
-As a concrete example we will now prove complete induction via
-structural induction: *}
-
-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 m)    -- {*@{text"?m < n \<Longrightarrow> P ?m"}  and  @{prop"m < Suc n"}*}
-    show ?case       -- {*@{term ?case}*}
-    proof cases
-      assume eq: "m = n"
-      from Suc 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, 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 @{text"\<forall>"} or
-@{text"\<longrightarrow>"} into a theorem to strengthen it for induction. In structured 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.
-*}
-
-subsection{*Rule induction*}
-
-text{* We define our own version of reflexive transitive closure of a
-relation *}
-consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)
-inductive "r*"
-intros
-refl:  "(x,x) \<in> r*"
-step:  "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
-
-text{* \noindent and 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 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
-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
-see very clearly how things fit together and permit ourselves the
-obvious forward step @{text"IH[OF B]"}. *}
-
-subsection{*More induction*}
-
-text{* 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. The example is an unusual
-definition of rotation: *}
-
-consts rot :: "'a list \<Rightarrow> 'a list"
-recdef rot "measure length"
-"rot [] = []"
-"rot [x] = [x]"
-"rot (x#y#zs) = y # rot(x#zs)"
-
-text{* In the first proof we set up each case explicitly, merely using
-pattern matching to abbreviate the statement: *}
-
-lemma "length(rot xs) = length xs" (is "?P xs")
-proof (induct xs rule: rot.induct)
-  show "?P []" by simp
-next
-  fix x show "?P [x]" by simp
-next
-  fix x y zs assume "?P (x#zs)"
-  thus "?P (x#y#zs)" by simp
-qed
-text{*\noindent
-This proof skeleton works for arbitrary induction rules, not just
-@{thm[source]rot.induct}.
-
-In the following proof we rely 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. *}
-
-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 thus ?case by simp
-qed
-
-text{*\noindent Why can case 2 get away with \isakeyword{show} instead of
-\isakeyword{thus}?
-
-Of course both proofs are so simple that they can be condensed to*}
-(*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
-by (induct xs rule: rot.induct, simp_all)
 (*<*)end(*>*)
diff -r 55d32e76ef4e -r 531f1f524848 doc-src/TutorialI/IsarOverview/Isar/ROOT.ML
--- a/doc-src/TutorialI/IsarOverview/Isar/ROOT.ML	Mon Sep 30 16:48:15 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/ROOT.ML	Mon Sep 30 16:50:39 2002 +0200
@@ -1,1 +1,2 @@
-use_thy "Logic"
+use_thy "Logic";
+use_thy "Induction"
diff -r 55d32e76ef4e -r 531f1f524848 doc-src/TutorialI/IsarOverview/Isar/document/root.bib
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.bib	Mon Sep 30 16:48:15 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.bib	Mon Sep 30 16:50:39 2002 +0200
@@ -1,6 +1,10 @@
 @string{LNCS="Lect.\ Notes in Comp.\ Sci."}
 @string{Springer="Springer-Verlag"}
 
+@book{LCF,author="M.C.J. Gordon and Robin Milner and C.P. Wadsworth",
+title="Edinburgh {LCF}: a Mechanised Logic of Computation",
+publisher=Springer,series=LNCS,volume=78,year=1979}
+
 @book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
 title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
 publisher=Springer,series=LNCS,volume=2283,year=2002,
diff -r 55d32e76ef4e -r 531f1f524848 doc-src/TutorialI/IsarOverview/Isar/document/root.tex
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Mon Sep 30 16:48:15 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Mon Sep 30 16:50:39 2002 +0200
@@ -10,23 +10,162 @@
 
 \begin{document}
 
-\title{A Compact Overview of Structured Proofs in Isar/HOL}
+\title{A Compact Introduction to Structured Proofs in Isar/HOL}
 \author{Tobias Nipkow\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\
  {\small\url{http://www.in.tum.de/~nipkow/}}}
 \date{}
 \maketitle
 
-\noindent
-Isar is an extension of Isabelle with structured proofs in a
-stylized language of mathematics. These proofs are readable for both a human
-and a machine.
+\begin{abstract}
+  Isar is an extension of the theorem prover Isabelle with a language
+  for writing human-readable structured proofs. This paper is an
+  introduction to the basic constructs of this language. It is aimed
+  at potential users of Isar but also discusses the design rationals
+  behind the language and its constructs.
+\end{abstract}
+
+\section{Introduction}
+
+Isar is an extension of Isabelle with structured proofs in a stylized
+language of mathematics. These proofs are readable for both a human
+and a machine.  This document is a very compact introduction to
+structured proofs in Isar/HOL, an extension of
+Isabelle/HOL~\cite{LNCS2283}. We intentionally do not present the full
+language but concentrate on the essentials. Neither do we give a
+formal semantics of Isar. Instead we introduce Isar by example. Again
+this is intentional: we believe that the language ``speaks for
+itself'' in the same way that traditional mathamtical proofs do, which
+are also introduced by example rather than by teaching students logic
+first. A detailed exposition of Isar can be found in Markus Wenzel's
+PhD thesis~\cite{Wenzel-PhD} and the Isar reference
+manual~\cite{Isar-Ref-Man}.
+
+\subsection{Background}
+
+Interactive theorem proving has been dominated by a model of proof
+that goes back to the LCF system~\cite{LCF}: a proof is a more or less
+structured sequence of commands that manipulate an implicit proof
+state. Thus the proof proof text is only suitable for the machine; for
+a human, the proof only comes alive when he can see the state changes
+caused by the stepwise execution of the commands. Such a proof is like
+an uncommented assembly language program. We call them
+\emph{tactic-style} proofs because LCF proof-commands were called
+tactics.
+
+A radically different approach was taken by the Mizar
+system~\cite{Mizar} where proofs are written a stylized language akin
+to that used in ordinary mathematics texts. The most important
+argument in favour of a mathematics-like proof language is
+communication: as soon as not just the theorem but also the proof
+becomes an object of interest, it should be readable as it is.  From a
+system development point of view there is a second important argument
+against tactic-style proofs: they are much harder to maintain when the
+system is modified. The reason is as follows. Since it is usually
+quite unclear what exactly is proved at some point in the middle of a
+command sequence, updating a failed proof often requires executing the
+proof up to the point of failure using the old version of the system.
+In contrast, mathematics-like proofs contain enough information
+to tell you what is proved at any point.
+
+For these reasons the Isabelle system, originally firmly in the
+LCF-tradition, was extended with a language for writing structured
+proofs in a mathematics-like style. As the name already indicates,
+Isar was certainly inspired by Mizar. However, there are very many
+differences. For a start, Isar is generic: only a few of the language
+constructs described below are specific to HOL; many are generic and
+thus available for any logic defined in Isabelle, e.g.\ ZF.
+Furthermore, we have Isabelle's powerful automatic proof procedures
+(e.g.\ simplification and a tableau-style prover) at our disposal.
+A closer comparison of Isar and Mizar can be found
+elsewhere~\cite{Isar-Mizar}.
 
-This document is a very compact introduction to structured proofs in
-Isar/HOL, an extension of Isabelle/HOL~\cite{LNCS2283}. A detailed
-exposition of this material can be found in Markus Wenzel's PhD
-thesis~\cite{Wenzel-PhD} and the Isar reference manual~\cite{Isar-Ref-Man}.
+Finally, a word of warning for potential writers of structured Isar
+proofs.  It has always been easier to write obscure rather than
+readable texts. Similarly, tactic-based proofs are often (though by no
+means always!) easier to write than readable ones: structure does not
+emerge automatically but needs to be understood and imposed. If the
+precise structure of the proof is not clear from the beginning, it can
+be useful to start in a tactic-based style for exploratory purposes
+until one has found a proof which can then be converted into a
+structured text in a second step. Top down conversion is possible
+because Isar allows tactic-based proofs as components of structured
+ones.
+
+\subsection{An overview of the Isar syntax}
+
+We begin by looking at a simplified grammar for Isar proofs
+where parentheses are used for grouping and $^?$ indicates an optional item:
+\begin{center}
+\begin{tabular}{lrl}
+\emph{proof} & ::= & \isakeyword{proof} \emph{method}$^?$
+                     \emph{statement}*
+                     \isakeyword{qed} \\
+                 &$\mid$& \isakeyword{by} \emph{method}\\[1ex]
+\emph{statement} &::= & \isakeyword{fix} \emph{variables} \\
+             &$\mid$& \isakeyword{assume} \emph{propositions} \\
+             &$\mid$& (\isakeyword{from} \emph{facts})$^?$ 
+                    (\isakeyword{show} $\mid$ \isakeyword{have})
+                      \emph{propositions} \emph{proof} \\[1ex]
+\emph{proposition} &::=& (\emph{label}{\bf:})$^?$ \emph{string} \\[1ex]
+\emph{fact} &::=& \emph{label}
+\end{tabular}
+\end{center}
+A proof can be either compound (\isakeyword{proof} --
+\isakeyword{qed}) or atomic (\isakeyword{by}). A \emph{method} is a
+proof method offered by the underlying theorem prover, for example
+\isa{rule} or \isa{simp} in Isabelle.  Thus this grammar is
+generic both w.r.t.\ the logic and the theorem prover.
+
+This is a typical proof skeleton:
+\begin{center}
+\begin{tabular}{@{}ll}
+\isakeyword{proof}\\
+\hspace*{3ex}\isakeyword{assume} \isa{"}\emph{the-assm}\isa{"}\\
+\hspace*{3ex}\isakeyword{have} \isa{"}\dots\isa{"} & --- intermediate result\\
+\hspace*{3ex}\vdots\\
+\hspace*{3ex}\isakeyword{have} \isa{"}\dots\isa{"} & --- intermediate result\\
+\hspace*{3ex}\isakeyword{show} \isa{"}\emph{the-concl}\isa{"}\\
+\isakeyword{qed}
+\end{tabular}
+\end{center}
+It proves \emph{the-assm}~$\Longrightarrow$~\emph{the-concl}. Text starting with
+``---'' is a comment. The intermediate \isakeyword{have}s are only
+there to bridge the gap between the assumption and the conclusion and
+do not contribute to the theorem being proved. In contrast,
+\isakeyword{show} establishes the conclusion of the theorem.
+
+As a final bit of syntax note that \emph{propositions} (following
+\isakeyword{assume} etc) may but need not be separated by
+\isakeyword{and}, whose purpose is to structure them into possibly
+named blocks. For example in
+\begin{center}
+\isakeyword{assume} \isa{A:} $A_1$ $A_2$ \isakeyword{and} \isa{B:} $A_3$
+\isakeyword{and} $A_4$
+\end{center}
+label \isa{A} refers to the list of propositions $A_1$ $A_2$ and
+label \isa{B} to $A_3$.
+
+\subsection{Overview of the paper}
+
+The rest of the paper is divided into two parts.
+Section~\ref{sec:Logic} introduces proofs in pure logic based on
+natural deduction. Section~\ref{sec:Induct} is dedicated to induction,
+the key reasoning principle for computer science applications.
+
+There are at least two further areas where Isar provides specific
+support, but which we do not document here: reasoning by chains of
+(in)equations is described elsewhere~\cite{BauerW-TPHOL}, whereas
+reasoning about axiomatically defined structures by means of so called
+``locales'' \cite{BallarinPW-TPHOL} is only described in a very early
+form and has evolved much since then.
+
+Do not be mislead by the simplicity of the formulae being proved,
+especially in the beginning. Isar has been used very successfully in
+large applications, for example the formalization of Java, in
+particular the verification of the bytecode verifier~\cite{KleinN-TCS}.
 
 \input{Logic.tex}
+\input{Induction.tex}
 
 %\input{Isar.tex}
 
diff -r 55d32e76ef4e -r 531f1f524848 doc-src/TutorialI/IsarOverview/Isar/makeDemo
--- a/doc-src/TutorialI/IsarOverview/Isar/makeDemo	Mon Sep 30 16:48:15 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/makeDemo	Mon Sep 30 16:50:39 2002 +0200
@@ -13,6 +13,8 @@
     s/text\{\*([^*]|\*[^}])*\*\}//sg;       # actual work done here
     s/\(\*<\*\)//sg;
     s/\(\*>\*\)//sg;
+    s/--(\ )*"([^"])*"//sg;
+    s/--(\ )*\{\*([^*]|\*[^}])*\*\}//sg;
 
     $result = $_;