
diff -r 70a5d5fc081a -r 3323ecc0b97c doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Tue Jul 09 11:55:46 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Tue Jul 09 13:41:38 2002 +0200
@@ -1,6 +1,6 @@
 (*<*)theory Logic = Main:(*>*)
 text{* We begin by looking at a simplified grammar for Isar proofs
-where paranthesis are used for grouping and $^?$ indicates an optional item:
+where parentheses are used for grouping and $^?$ indicates an optional item:
 \begin{center}
 \begin{tabular}{lrl}
 \emph{proof} & ::= & \isakeyword{proof} \emph{method}$^?$
@@ -8,13 +8,12 @@
                      \isakeyword{qed} \\
                  &$\mid$& \isakeyword{by} \emph{method}\\[1ex]
 \emph{statement} &::= & \isakeyword{fix} \emph{variables} \\
-             &$\mid$& \isakeyword{assume} \emph{proposition}
-                      (\isakeyword{and} \emph{proposition})*\\
-             &$\mid$& (\isakeyword{from} \emph{label}$^*$ $\mid$
-                       \isakeyword{then})$^?$ 
+             &$\mid$& \isakeyword{assume} \emph{propositions} \\
+             &$\mid$& (\isakeyword{from} \emph{facts})$^?$ 
                     (\isakeyword{show} $\mid$ \isakeyword{have})
-                      \emph{string} \emph{proof} \\[1ex]
-\emph{proposition} &::=& (\emph{label}{\bf:})$^?$ \emph{string}
+                      \emph{propositions} \emph{proof} \\[1ex]
+\emph{proposition} &::=& (\emph{label}{\bf:})$^?$ \emph{string} \\[1ex]
+\emph{fact} &::=& \emph{label}
 \end{tabular}
 \end{center}
 
@@ -32,6 +31,16 @@
 \end{center}
 It proves \emph{the-assm}~@{text"\<Longrightarrow>"}~\emph{the-concl}.
 Text starting with ``--'' is a comment.
+
+Note that propositions in \isakeyword{assume} may but need not be
+separated by \isakeyword{and} whose purpose is to structure the
+assumptions into possibly named blocks, for example
+\begin{center}
+\isakeyword{assume} @{text"A:"} $A_1$ $A_2$ \isakeyword{and} @{text"B:"} $A_3$
+\isakeyword{and} $A_4$
+\end{center}
+Here label @{text A} refers to the list of propositions $A_1$ $A_2$ and
+label @{text B} to $A_3$.
 *}
 
 section{*Logic*}
@@ -67,7 +76,7 @@
 qed
 
 text{* Trivial proofs, in particular those by assumption, should be trivial
-to perform. Method ``.'' does just that (and a bit more --- see later). Thus
+to perform. Proof ``.'' does just that (and a bit more). Thus
 naming of assumptions is often superfluous: *}
 lemma "A \<longrightarrow> A"
 proof
@@ -88,7 +97,7 @@
 
 Proofs of the form \isakeyword{by}@{text"(rule"}~\emph{name}@{text")"} can be
 abbreviated to ``..''
-if \emph{name} is one of the predefined introduction rules:
+if \emph{name} refers to one of the predefined introduction rules:
 *}
 
 lemma "A \<longrightarrow> A \<and> A"
@@ -118,7 +127,7 @@
 qed
 text{*\noindent Note that the term @{text"?thesis"} always stands for the
 ``current goal'', i.e.\ the enclosing \isakeyword{show} (or
-\isakeyword{have}).
+\isakeyword{have}) statement.
 
 This is too much proof text. Elimination rules should be selected
 automatically based on their major premise, the formula or rather connective
@@ -161,9 +170,14 @@
   qed
 qed
 
-text{*\noindent
-A final simplification: \isakeyword{from}~@{text this} can be
-abbreviated to \isakeyword{thus}.
+text{*\noindent Because of the frequency of \isakeyword{from}~@{text
+this} Isar provides two abbreviations:
+\begin{center}
+\begin{tabular}{rcl}
+\isakeyword{then} &=& \isakeyword{from} @{text this} \\
+\isakeyword{thus} &=& \isakeyword{then} \isakeyword{show}
+\end{tabular}
+\end{center}
 \medskip
 
 Here is an alternative proof that operates purely by forward reasoning: *}
@@ -175,7 +189,7 @@
   from b a show "B \<and> A" ..
 qed
 text{*\noindent
-It is worth examining this text in detail because it exhibits a number of new features.
+It is worth examining this text in detail because it exhibits a number of new concepts.
 
 For a start, this is the first time we have proved intermediate propositions
 (\isakeyword{have}) on the way to the final \isakeyword{show}. This is the
@@ -187,7 +201,8 @@
 The \isakeyword{show} command illustrates two things:
 \begin{itemize}
 \item \isakeyword{from} can be followed by any number of facts.
-Given \isakeyword{from}~@{text f}$_1$~\dots~@{text f}$_n$, \isakeyword{show}
+Given \isakeyword{from}~@{text f}$_1$~\dots~@{text f}$_n$, the
+\isakeyword{proof} step after \isakeyword{show}
 tries to find an elimination rule whose first $n$ premises can be proved
 by the given facts in the given order.
 \item If there is no matching elimination rule, introduction rules are tried,
@@ -203,7 +218,7 @@
 with \isakeyword{by}@{text"(rule conjI)"}. 
 
 Note that Isar's predefined introduction and elimination rules include all the
-usual natural deduction rules for propositional logic. We conclude this
+usual natural deduction rules. We conclude this
 section with an extended example --- which rules are used implicitly where?
 Rule @{thm[source]ccontr} is @{thm ccontr[no_vars]}.
 *}
@@ -247,27 +262,27 @@
 text{* So far our examples have been a bit unnatural: normally we want to
 prove rules expressed with @{text"\<Longrightarrow>"}, not @{text"\<longrightarrow>"}. Here is an example:
 *}
-lemma "(A \<Longrightarrow> False) \<Longrightarrow> \<not> A"
+lemma "A \<and> B \<Longrightarrow> B \<and> A"
 proof
-  assume "A \<Longrightarrow> False" "A"
-  thus False .
+  assume "A \<and> B" thus "B" ..
+next
+  assume "A \<and> B" thus "A" ..
 qed
 text{*\noindent The \isakeyword{proof} always works on the conclusion,
-@{prop"\<not>A"} in our case, thus selecting $\neg$-introduction. Hence we can
-additionally assume @{prop"A"}. Why does ``.'' prove @{prop False}? Because
-``.'' tries any of the assumptions, including proper rules (here: @{prop"A \<Longrightarrow>
-False"}), such that all of its premises can be solved directly by some other
-assumption (here: @{prop A}).
+@{prop"B \<and> A"} in our case, thus selecting $\land$-introduction. Hence
+we must show @{prop B} and @{prop A}; both are proved by
+$\land$-elimination.
 
 This is all very well as long as formulae are small. Let us now look at some
 devices to avoid repeating (possibly large) formulae. A very general method
 is pattern matching: *}
 
-lemma "(large_formula \<Longrightarrow> False) \<Longrightarrow> \<not> large_formula"
-      (is "(?P \<Longrightarrow> _) \<Longrightarrow> _")
+lemma "large_A \<and> large_B \<Longrightarrow> large_B \<and> large_A"
+      (is "?AB \<Longrightarrow> ?B \<and> ?A")
 proof
-  assume "?P \<Longrightarrow> False" ?P
-  thus False .
+  assume ?AB thus ?B ..
+next
+  assume ?AB thus ?A ..
 qed
 text{*\noindent Any formula may be followed by
 @{text"("}\isakeyword{is}~\emph{pattern}@{text")"} which causes the pattern
@@ -276,20 +291,39 @@
 them to be replaced by the terms they stand for.
 
 We can simplify things even more by stating the theorem by means of the
-\isakeyword{assumes} and \isakeyword{shows} primitives which allow direct
+\isakeyword{assumes} and \isakeyword{shows} elements which allow direct
 naming of assumptions: *}
 
-lemma assumes A: "large_formula \<Longrightarrow> False"
-  shows "\<not> large_formula" (is "\<not> ?P")
+lemma assumes AB: "large_A \<and> large_B"
+  shows "large_B \<and> large_A" (is "?B \<and> ?A")
 proof
-  assume ?P
-  with A show False .
+  from AB show ?B ..
+next
+  from AB show ?A ..
 qed
-text{*\noindent Here we have used the abbreviation
+text{*\noindent Note the difference between @{text ?AB}, a term, and
+@{text AB}, a fact.
+
+Finally we want to start the proof with $\land$-elimination so we
+don't have to perform it twice, as above. Here is a slick way to
+achieve this: *}
+
+lemma assumes AB: "large_A \<and> large_B"
+  shows "large_B \<and> large_A" (is "?B \<and> ?A")
+using AB
+proof
+  assume ?A and ?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}
+is the only such fact and it triggers $\land$-elimination. Another
+frequent usage is as follows:
 \begin{center}
-\isakeyword{with}~\emph{facts} \quad = \quad
-\isakeyword{from}~\emph{facts} \isakeyword{and} @{text this}
+\isakeyword{from} \emph{important facts}
+\isakeyword{show} \emph{something}
+\isakeyword{using} \emph{minor facts}
 \end{center}
+\medskip
 
 Sometimes it is necessary to supress the implicit application of rules in a
 \isakeyword{proof}. For example \isakeyword{show}~@{prop"A \<or> B"} would
@@ -305,12 +339,13 @@
     assume B show ?thesis ..
   qed
 qed
-
+text{*\noindent Could \isakeyword{using} help to eliminate this ``@{text"-"}''? *}
 
 subsection{*Predicate calculus*}
 
 text{* Command \isakeyword{fix} introduces new local variables into a
-proof. It corresponds to @{text"\<And>"} (the universal quantifier at the
+proof. The pair \isakeyword{fix}-\isakeyword{show} corresponds to @{text"\<And>"}
+(the universal quantifier at the
 meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to
 @{text"\<Longrightarrow>"}. Here is a sample proof, annotated with the rules that are
 applied implictly: *}
@@ -321,7 +356,7 @@
 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
-names is irrelevant.
+local names is irrelevant.
 
 Next we look at @{text"\<exists>"} which is a bit more tricky.
 *}
@@ -337,20 +372,19 @@
 qed
 text{*\noindent Explicit $\exists$-elimination as seen above can become
 cumbersome in practice.  The derived Isar language element
-\isakeyword{obtain} provides a more handsome way to perform generalized
+\isakeyword{obtain} provides a more appealing form of generalized
 existence reasoning: *}
 
 lemma assumes Pf: "\<exists>x. P(f x)" shows "\<exists>y. P y"
 proof -
-  from Pf obtain a where "P(f a)" ..
+  from Pf obtain x where "P(f x)" ..
   thus "\<exists>y. P y" ..
 qed
 text{*\noindent Note how the proof text follows the usual mathematical style
 of concluding $P(x)$ from $\exists x. P(x)$, while carefully introducing $x$
 as a new local variable.  Technically, \isakeyword{obtain} is similar to
 \isakeyword{fix} and \isakeyword{assume} together with a soundness proof of
-the elimination involved.  Thus it behaves similar to any other forward proof
-element.
+the elimination involved.
 
 Here is a proof of a well known tautology which employs another useful
 abbreviation: \isakeyword{hence} abbreviates \isakeyword{from}~@{text
@@ -386,7 +420,7 @@
   qed
 qed
 text{*\noindent
-For a start, the example demonstrates two new language elements:
+For a start, the example demonstrates three new language elements:
 \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.
@@ -394,6 +428,11 @@
 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}.
+\item \isakeyword{with} is an abbreviation:
+\begin{center}
+\isakeyword{with}~\emph{facts} \quad = \quad
+\isakeyword{from}~\emph{facts} \isakeyword{and} @{text this}
+\end{center}
 \end{itemize}
 If you wonder how to \isakeyword{obtain} @{term y}:
 via the predefined elimination rule @{thm rangeE[no_vars]}.
@@ -425,7 +464,7 @@
   qed
 qed
 text{*\noindent Method @{text contradiction} succeeds if both $P$ and
-$\neg P$ are among the assumptions and the facts fed into that step.
+$\neg P$ are among the assumptions and the facts fed into that step, in any order.
 
 As it happens, Cantor's theorem can be proved automatically by best-first
 search. Depth-first search would diverge, but best-first search successfully
@@ -440,7 +479,7 @@
 Finally, whole scripts may appear in the leaves of the proof tree, although
 this is best avoided.  Here is a contrived example: *}
 
-lemma "A \<longrightarrow> (A \<longrightarrow>B) \<longrightarrow> B"
+lemma "A \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> B"
 proof
   assume a: A
   show "(A \<longrightarrow>B) \<longrightarrow> B"
@@ -466,7 +505,7 @@
 next
   assume "\<not> P" thus ?thesis ..
 qed
-text{*\noindent As always, the cases can be tackled in any order.
+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
@@ -481,13 +520,12 @@
 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"}.
+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
@@ -498,10 +536,10 @@
 \isakeyword{assume}~@{prop"x = []"} 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
-refer to them (this would lead to brittle proofs) and have not even shown
-them. Luckily, the proof is simple enough we do not need to refer to them.
+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
-naming those variables: Replace the anonymous @{text Cons} by, for example,
+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: *}
@@ -515,8 +553,7 @@
     by simp
   thus ?thesis by simp
 qed
-text{* New case distincion rules can be declared any time, even with
-named cases. *}
+
 
 subsection{*Induction*}
 
@@ -552,7 +589,7 @@
 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 @{term n}
+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)"}: *}
@@ -609,7 +646,7 @@
 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 additonal parameter coming from the @{text"\<And>m"} in the main
-\isakeyword{shows} clause. Thus  Thus @{text"(Suc n m)"} does not mean that
+\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}. *}
@@ -625,39 +662,20 @@
 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*" (is "PROP ?P x y")
+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
-(*
-lemma assumes A: "(x,y) \<in> r*"
-  shows "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*" (is "PROP ?P x y")
-proof -
-  from A show "PROP ?P x y"
-  proof induct
-    fix x show "PROP ?P x x" .
-  next
-    fix x' x y
-    assume "(x',x) \<in> r"
-           "PROP ?P x y"   -- "induction hypothesis"
-    thus "PROP ?P x' y" by(blast intro: rtc.step)
-  qed
-qed
-*)
-text{*\noindent Rule induction is triggered by a fact $(x_1,\dots,x_n) \in R$
-piped into the proof, here \isakeyword{from}~@{text A}. The proof itself
-follows the two rules of the inductive definition very closely.  The only
-surprising thing should be the keyword @{text PROP}: because of certain
-syntactic subleties it is required in front of terms of type @{typ prop} (the
-type of meta-level propositions) which are not obviously of type @{typ prop}
-(e.g.\ @{text"?P x y"}) because they do not contain a tell-tale constant such
-as @{text"\<And>"} or @{text"\<Longrightarrow>"}.
+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, the proof is rather terse. Here is a more readable version:
+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*"
@@ -675,14 +693,12 @@
     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 first proof step, here
-induction. Since @{text B} is left over we don't just prove @{text
-?thesis} but @{text"B \<Longrightarrow> ?thesis"}, just as in the previous
-proof, only more elegantly. 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]"}. *}
+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]"}. *}
 
 (*<*)end(*>*)




