# HG changeset patch
# User nipkow
# Date 1032944794 -7200
# Node ID a0febf6b0e9fd248bff8c217bc80a2e559d11e4c
# Parent  57c12adaec85934417cef6f56ebdcf8dbd792466
*** empty log message ***

diff -r 57c12adaec85 -r a0febf6b0e9f doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Wed Sep 25 07:57:36 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Wed Sep 25 11:06:34 2002 +0200
@@ -455,11 +455,11 @@
 For a start, the example demonstrates two new constructs:
 \begin{itemize}
 \item \isakeyword{let} introduces an abbreviation for a term, in our case
-the witness for the claim, because the term occurs multiple times in the proof.
+the witness for the claim.
 \item Proof by @{text"cases"} starts a proof by cases. Note that it remains
 implicit what the two cases are: it is merely expected that the two subproofs
-prove @{prop"P \<Longrightarrow> Q"} and @{prop"\<not>P \<Longrightarrow> Q"} for suitable @{term P} and
-@{term Q}.
+prove @{text"P \<Longrightarrow> ?thesis"} and @{text"\<not>P \<Longrightarrow> ?thesis"} (in that order)
+for some @{term P}.
 \end{itemize}
 If you wonder how to \isakeyword{obtain} @{term y}:
 via the predefined elimination rule @{thm rangeE[no_vars]}.
@@ -478,15 +478,15 @@
     then obtain y where fy: "?S = f y" ..
     show False
     proof cases
-      assume A: "y \<in> ?S"
-      hence isin: "y \<in> f y"   by(simp add:fy)
-      from A have "y \<notin> f y"   by simp
-      with isin show False    by contradiction
+      assume "y \<in> ?S"
+      hence "y \<notin> f y"   by simp
+      hence "y \<notin> ?S"    by(simp add:fy)
+      thus False        by contradiction
     next
-      assume A: "y \<notin> ?S"
-      hence notin: "y \<notin> f y"   by(simp add:fy)
-      from A have "y \<in> f y"    by simp
-      with notin show False    by contradiction
+      assume "y \<notin> ?S"
+      hence "y \<in> f y"   by simp
+      hence "y \<in> ?S"    by(simp add:fy)
+      thus False        by contradiction
     qed
   qed
 qed
@@ -562,11 +562,13 @@
 qed
 text{*\noindent Here \isakeyword{case}~@{text Nil} abbreviates
 \isakeyword{assume}~@{prop"xs = []"} and \isakeyword{case}~@{text Cons}
-abbreviates \isakeyword{assume}~@{text"xs = _ # _"}. The names of the head
-and tail of @{text xs} have been chosen by the system. Therefore we cannot
+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, in general one may have to. Hence Isar offers a simple scheme for
+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
@@ -644,42 +646,38 @@
 \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
-@{prop[display,indent=5]"(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n) \<Longrightarrow> P n"}
-via structural induction. It is well known that one needs to prove
-something more general first: *}
-lemma cind_lemma:
-  assumes A: "(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
-  shows "\<And>m. m < n \<Longrightarrow> P(m::nat)"
-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
+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
-    assume neq: "m \<noteq> n"
-    with Suc have "m < n" by simp
-    with Suc show "P m" by blast
+    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 statemt of the lemma is interesting because it deviates from the style in
+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 don't have to convert between the two kinds of
-connectives. As usual, at the end of the proof @{text"\<And>"} disappears and the
-bound variable is turned into a @{text"?"}-variable. Thus
-@{thm[source]cind_lemma} becomes @{thm[display,indent=5] cind_lemma} Complete
-induction is an easy corollary: instantiation followed by simplification,
-@{text"cind_lemma[of _ n \"Suc n\", simplified]"}, yields
-@{thm[display,indent=5] cind_lemma[of _ n "Suc n", simplified]}
+proof and means we do not have to convert between the two kinds of
+connectives.
 *}
 
 subsection{*Rule induction*}
diff -r 57c12adaec85 -r a0febf6b0e9f doc-src/TutorialI/IsarOverview/Isar/document/root.tex
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Wed Sep 25 07:57:36 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Wed Sep 25 11:06:34 2002 +0200
@@ -38,8 +38,8 @@
 {\small
 \paragraph{Acknowledgment}
 I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin,
-Stefan Berghofer,
-Gerwin Klein, Norbert Schirmer and Markus Wenzel commented on this document.
+Gertrud Bauer, Stefan Berghofer, Gerwin Klein, Norbert Schirmer and
+Markus Wenzel commented on and improved this document.
 }
 
 \begingroup