# HG changeset patch
# User nipkow
# Date 1026402988 -7200
# Node ID bc1fb6941b54370001e802251c65f6642bb956c6
# Parent  626b79677dfa0017e802b5b4c5b447df55ee3067
*** empty log message ***

diff -r 626b79677dfa -r bc1fb6941b54 doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Thu Jul 11 17:18:28 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Thu Jul 11 17:56:28 2002 +0200
@@ -357,9 +357,9 @@
 @{text"\<Longrightarrow>"}. Here is a sample proof, annotated with the rules that are
 applied implicitly: *}
 lemma assumes P: "\<forall>x. P x" shows "\<forall>x. P(f x)"
-proof    -- "@{thm[source]allI}: @{thm allI}"
+proof                       --"@{thm[source]allI}: @{thm allI}"
   fix a
-  from P show "P(f a)" ..   --"@{thm[source]allE}: @{thm allE}"
+  from P show "P(f a)" ..  --"@{thm[source]allE}: @{thm allE}"
 qed
 text{*\noindent Note that in the proof we have chosen to call the bound
 variable @{term a} instead of @{term x} merely to show that the choice of
@@ -371,10 +371,10 @@
 lemma assumes Pf: "\<exists>x. P(f x)" shows "\<exists>y. P y"
 proof -
   from Pf show ?thesis
-  proof  -- "@{thm[source]exE}: @{thm exE[no_vars]}"
-    fix a
-    assume "P(f a)"
-    show ?thesis ..  --"@{thm[source]exI}: @{thm exI[no_vars]}"
+  proof              -- "@{thm[source]exE}: @{thm exE}"
+    fix x
+    assume "P(f x)"
+    show ?thesis ..  -- "@{thm[source]exI}: @{thm exI}"
   qed
 qed
 text{*\noindent Explicit $\exists$-elimination as seen above can become
@@ -600,9 +600,24 @@
 
 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{*Induction formulae involving @{text"\<And>"} or @{text"\<Longrightarrow>"}*}
 
-Let us now tackle a more ambitious lemma: proving complete induction
+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
 @{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: *}
@@ -612,8 +627,8 @@
 proof (induct n)
   case 0 thus ?case by simp
 next
-  case (Suc n m)  --{*@{thm[source]Suc}: @{thm Suc}*}
-  show ?case      --{*@{text ?case}: @{term ?case}*}
+  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
@@ -624,29 +639,21 @@
     with Suc show "P m" by blast
   qed
 qed
-text{* \noindent Let us first examine the statement of the lemma.
-In contrast to the style advertised in the
-Tutorial~\cite{LNCS2283}, structured Isar proofs do not need to
-introduce @{text"\<forall>"} or @{text"\<longrightarrow>"} into a theorem to strengthen it
-for induction --- we 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, @{thm[source] cind_lemma[of _ n "Suc n", simplified]},
-yields @{thm[display,indent=5] cind_lemma[of _ n "Suc n", simplified]}
+text{* \noindent Given the explanations above and the comments in
+the proof text, the proof should be quite readable.
 
-Now we examine the proof.  So what is this funny case @{text"(Suc n m)"}? It
-looks confusing at first and reveals that the very suggestive @{text"(Suc
-n)"} used above is not the whole truth. The variable names after the case
-name (here: @{term Suc}) are the names of the parameters of that subgoal. So
-far the only parameters where the arguments to the constructor, but now we
-have an additional parameter coming from the @{text"\<And>m"} in the main
-\isakeyword{shows} clause. Thus @{text"(Suc n m)"} does not mean that
-constructor @{term Suc} is applied to two arguments but that the two
-parameters in the @{term Suc} case are to be named @{text n} and @{text m}. *}
+The statemt 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]}
+*}
 
 subsection{*Rule induction*}
 
diff -r 626b79677dfa -r bc1fb6941b54 doc-src/TutorialI/IsarOverview/Isar/document/root.tex
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Thu Jul 11 17:18:28 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Thu Jul 11 17:56:28 2002 +0200
@@ -17,7 +17,11 @@
 \maketitle
 
 \noindent
-This is a very compact introduction to structured proofs in
+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}. 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}.