diff -r 7917e66505a4 -r 6852682eaf16 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Wed Jan 24 12:29:10 2001 +0100
@@ -71,7 +71,7 @@
 like this:
 \[  \infer{P\conj Q}{P & Q} \]
 The rule introduces the conjunction
-symbol~($\conj$) in its conclusion.  Of course, in Isabelle proofs we
+symbol~($\conj$) in its conclusion.  In Isabelle proofs we
 mainly  reason backwards.  When we apply this rule, the subgoal already has
 the form of a conjunction; the proof step makes this conjunction symbol
 disappear. 
@@ -170,7 +170,7 @@
 \isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE}
 \end{isabelle}
 When we use this sort of elimination rule backwards, it produces 
-a case split.  (We have this before, in proofs by induction.)  The following  proof
+a case split.  (We have seen this before, in proofs by induction.)  The following  proof
 illustrates the use of disjunction elimination.  
 \begin{isabelle}
 \isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\ 
@@ -184,7 +184,7 @@
 We assume \isa{P\ \isasymor\ Q} and
 must prove \isa{Q\ \isasymor\ P}\@.  Our first step uses the disjunction
 elimination rule, \isa{disjE}.  The method {\isa{erule}}  applies an
-elimination rule to the assumptions, searching for one that matches the
+elimination rule, searching for an assumption that matches the
 rule's first premise.  Deleting that assumption, it
 return the subgoals for the remaining premises.  Most of the
 time, this is  the best way to use elimination rules; only rarely is there
@@ -394,7 +394,7 @@
 As we have seen, Isabelle rules involve variables that begin  with a
 question mark. These are called \textbf{schematic} variables  and act as
 placeholders for terms. \textbf{Unification} refers to  the process of
-making two terms identical, possibly by replacing  their variables by
+making two terms identical, possibly by replacing their schematic variables by
 terms. The simplest case is when the two terms  are already the same. Next
 simplest is when the variables in only one of the term
  are replaced; this is called \textbf{pattern-matching}.  The
@@ -440,7 +440,7 @@
 A typical substitution rule allows us to replace one term by 
 another if we know that two terms are equal. 
 \[ \infer{P[t/x]}{s=t & P[s/x]} \]
-The conclusion uses a notation for substitution: $P[t/x]$ is the result of
+The rule uses a notation for substitution: $P[t/x]$ is the result of
 replacing $x$ by~$t$ in~$P$.  The rule only substitutes in the positions
 designated by~$x$.  For example, it can
 derive symmetry of equality from reflexivity.  Using $x=s$ for~$P$
@@ -566,7 +566,7 @@
 \isa{erule_tac} since above we used \isa{erule}.
 \begin{isabelle}
 \isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
-\isacommand{by}\ (erule_tac\ P="\isasymlambda u.\ P\ u\ u\ x"\ 
+\isacommand{by}\ (erule_tac\ P = "\isasymlambda u.\ P\ u\ u\ x"\ 
 \isakeyword{in}\ ssubst)
 \end{isabelle}
 %
@@ -580,7 +580,7 @@
 An alternative to \isa{rule_tac} is to use \isa{rule} with the
 \isa{of} directive, described in \S\ref{sec:forward} below.   An
 advantage  of \isa{rule_tac} is that the instantiations may refer to 
-variables bound in the current subgoal.
+\isasymAnd-bound variables in the current subgoal.
 
 
 \section{Negation}
@@ -632,7 +632,7 @@
 \isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\
 \isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\
 R"\isanewline
-\isacommand{apply}\ (erule_tac\ Q="R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
+\isacommand{apply}\ (erule_tac\ Q = "R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
 contrapos_np)\isanewline
 \isacommand{apply}\ intro\isanewline
 \isacommand{by}\ (erule\ notE)
@@ -664,7 +664,7 @@
 \isa{by} command.
 Now when Isabelle selects the first assumption, it tries to prove \isa{P\
 \isasymlongrightarrow\ Q} and fails; it then backtracks, finds the 
-assumption~\isa{\isasymnot\ R} and finally proves \isa{R} by assumption.  That
+assumption \isa{\isasymnot~R} and finally proves \isa{R} by assumption.  That
 concludes the proof.
 
 \medskip
@@ -691,7 +691,8 @@
 \end{isabelle}
 Next we apply the {\isa{elim}} method, which repeatedly applies 
 elimination rules; here, the elimination rules given 
-in the command.  One of the subgoals is trivial, leaving us with one other:
+in the command.  One of the subgoals is trivial (\isa{\isacommand{apply} assumption}),
+leaving us with one other:
 \begin{isabelle}
 \ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P%
 \end{isabelle}
@@ -704,8 +705,7 @@
 is robust: the \isa{conjI} forces the \isa{erule} to select a
 conjunction.  The two subgoals are the ones we would expect from applying
 conjunction introduction to
-\isa{Q\
-\isasymand\ R}:  
+\isa{Q~\isasymand~R}:  
 \begin{isabelle}
 \ 1.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\
 Q\isanewline
@@ -926,10 +926,12 @@
 \end{isabelle}
 If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
 P(x)$ is also true.  It is a dual of the universal elimination rule, and
-logic texts present it using the same notation for substitution.  The existential
+logic texts present it using the same notation for substitution.
+
+The existential
 elimination rule looks like this
 in a logic text: 
-\[ \infer{R}{\exists x.\,P & \infer*{R}{[P]}} \]
+\[ \infer{Q}{\exists x.\,P & \infer*{Q}{[P]}} \]
 %
 It looks like this in Isabelle: 
 \begin{isabelle}
@@ -953,17 +955,18 @@
 
 
 \section{Hilbert's Epsilon-Operator}
+\label{sec:SOME}
 
-Isabelle/HOL provides Hilbert's
-$\epsilon$-operator.  The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
+HOL provides Hilbert's
+$\varepsilon$-operator.  The term $\varepsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
 true, provided such a value exists.  Using this operator, we can express an
 existential destruction rule:
-\[ \infer{P[(\epsilon x. P) / \, x]}{\exists x.\,P} \]
+\[ \infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P} \]
 This rule is seldom used, for it can cause exponential blow-up.  
 
 \subsection{Definite Descriptions}
 
-In ASCII, we write \isa{SOME} for $\epsilon$.
+In ASCII, we write \isa{SOME} for $\varepsilon$.
 \REMARK{the internal constant is \isa{Eps}}
 The main use of \hbox{\isa{SOME\ x.\ P\ x}} is as a \textbf{definite
 description}: when \isa{P} is satisfied by a unique value,~\isa{a}. 
@@ -979,7 +982,7 @@
 prove that the cardinality of the empty set is zero (since $n=0$ satisfies the
 description) and proceed to prove other facts.
 
-Here is an example.  HOL defines \isa{inv},\indexbold{*inv (constant)}
+Here is another example.  Isabelle/HOL defines \isa{inv},\indexbold{*inv (constant)}
 which expresses inverses of functions, as a definite
 description:
 \begin{isabelle}
@@ -1025,7 +1028,6 @@
 \ 2.\ \isasymAnd x.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x;\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)\isasymrbrakk \isanewline
 \ \ \ \ \ \ \ \ \isasymLongrightarrow \ x\ =\ k%
 \end{isabelle}
-
 As always with \isa{some_equality}, we must show existence and
 uniqueness of the claimed solution,~\isa{k}.  Existence, the first
 subgoal, is trivial.  Uniqueness, the second subgoal, follows by antisymmetry:
@@ -1063,6 +1065,7 @@
 \ "(\isasymforall x.\ \isasymexists \ y.\ P\ x\ y)\ \isasymLongrightarrow \
 \isasymexists f.\ \isasymforall x.\ P\ x\ (f\ x)"\isanewline
 \isacommand{apply}\ (rule\ exI,\ rule\ allI)\isanewline
+
 \ 1.\ \isasymAnd x.\ \isasymforall x.\ \isasymexists y.\ P\ x\ y\
 \isasymLongrightarrow \ P\ x\ (?f\ x)
 \end{isabelle}
@@ -1072,6 +1075,7 @@
 
 \begin{isabelle}
 \isacommand{apply}\ (drule\ spec,\ erule\ exE)\isanewline
+
 \ 1.\ \isasymAnd x\ y.\ P\ (?x2\ x)\ y\ \isasymLongrightarrow \ P\ x\ (?f\ x)
 \end{isabelle}
 
@@ -1141,7 +1145,8 @@
 \begin{isabelle}
 *** empty result sequence -- proof command failed
 \end{isabelle}
-We can tell Isabelle to abandon a failed proof using the \isacommand{oops} command.
+If we interact with Isabelle via the shell interface,
+we abandon a failed proof with the \isacommand{oops} command.
 
 \medskip 
 
@@ -1301,7 +1306,7 @@
 \begin{isabelle}
 \isacommand{lemma}\
 [iff]:\ "(xs{\isacharat}ys\ =\ [])\ =\
-(xs=[]\ \isacharampersand\ ys=[])"\isanewline
+(xs=[]\ \isasymand\ ys=[])"\isanewline
 \isacommand{apply}\ (induct_tac\ xs)\isanewline
 \isacommand{apply}\ (simp_all)\isanewline
 \isacommand{done}
@@ -1314,7 +1319,7 @@
 (\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
 \end{isabelle}
 A product is zero if and only if one of the factors is zero.  The
-reasoning  involves a logical \textsc{or}.  Proving new rules for
+reasoning  involves a disjunction.  Proving new rules for
 disjunctive reasoning  is hard, but translating to an actual disjunction
 works:  the classical reasoner handles disjunction properly.
 
@@ -1490,8 +1495,8 @@
 We state it with the \isa{iff} attribute so that 
 Isabelle can use it to remove some occurrences of \isa{gcd}. 
 The theorem has a one-line 
-proof using \isa{blast} supplied with four introduction 
-rules: note the {\isa{intro}} attribute. The exclamation mark 
+proof using \isa{blast} supplied with two additional introduction 
+rules. The exclamation mark 
 ({\isa{intro}}{\isa{!}})\ signifies safe rules, which are 
 applied aggressively.  Rules given without the exclamation mark 
 are applied reluctantly and their uses can be undone if 
@@ -1519,8 +1524,8 @@
 
 Of the latter methods, the most useful is {\isa{clarify}}. It performs 
 all obvious reasoning steps without splitting the goal into multiple 
-parts. It does not apply rules that could render the 
-goal unprovable (so-called unsafe rules). By performing the obvious 
+parts. It does not apply unsafe rules that could render the 
+goal unprovable. By performing the obvious 
 steps, {\isa{clarify}} lays bare the difficult parts of the problem, 
 where human intervention is necessary. 
 
@@ -1568,7 +1573,7 @@
 That makes them slower but enables them to work correctly in the 
 presence of the more unusual features of Isabelle rules, such 
 as type classes and function unknowns. For example, recall the introduction rule
-for Hilbert's epsilon-operator: 
+for Hilbert's $\varepsilon$-operator: 
 \begin{isabelle}
 ?P\ ?x\ \isasymLongrightarrow\ ?P\ (SOME\ x.\ ?P x)
 \rulename{someI}
@@ -1796,7 +1801,7 @@
 instance of a rule by specifying facts for its premises.  Let us try
 it with this rule:
 \begin{isabelle}
-\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ (?m * ?n)\isasymrbrakk\
+\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\
 \isasymLongrightarrow\ ?k\ dvd\ ?m
 \rulename{relprime_dvd_mult}
 \end{isabelle}
@@ -1809,7 +1814,7 @@
 We have evaluated an application of the \isa{gcd} function by
 simplification.  Expression evaluation  is not guaranteed to terminate, and
 certainly is not  efficient; Isabelle performs arithmetic operations by 
-rewriting symbolic bit strings.  Here, however, the simplification takes
+rewriting symbolic bit strings.  Here, however, the simplification above takes
 less than one second.  We can specify this new lemma to \isa{OF},
 generating an instance of \isa{relprime_dvd_mult}.  The expression
 \begin{isabelle}
@@ -1826,7 +1831,7 @@
 \isasymlbrakk?k\ dvd\ ?m;\
 ?k\ dvd\ ?n\isasymrbrakk\
 \isasymLongrightarrow\ ?k\ dvd\
-(?m\ +\ ?n)
+?m\ +\ ?n
 \rulename{dvd_add}\isanewline
 ?m\ dvd\ ?m%
 \rulename{dvd_refl}
@@ -1846,7 +1851,7 @@
 \end{isabelle}
 The result is 
 \begin{isabelle}
-\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ +\ ?k)
+\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ ?m\ +\ ?k
 \end{isabelle}
 
 You may have noticed that \isa{THEN} and \isa{OF} are based on 
@@ -1933,7 +1938,7 @@
 \begin{isabelle}
 \isacommand{lemma}\
 relprime_dvd_mult:\isanewline
-\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\ k\ dvd\ (m*n)\
+\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\ k\ dvd\ m*n\
 \isasymrbrakk\
 \isasymLongrightarrow\ k\ dvd\
 m"\isanewline
@@ -1943,11 +1948,7 @@
 In the resulting subgoal, note how the equation has been 
 inserted: 
 \begin{isabelle}
-\isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\
-dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
-m\isanewline
-\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
-\ \ \ \ \ m\ *\ gcd\
+\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ m\ *\ n{;}\ m\ *\ gcd\
 (k,\ n)\
 =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
 \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
@@ -1956,12 +1957,8 @@
 utilizes the assumption \isa{gcd(k,n)\ =\
 1}. Here is the result: 
 \begin{isabelle}
-\isasymlbrakk gcd\ (k,\
-n)\ =\ 1;\ k\
-dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
-m\isanewline
-\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
-\ \ \ \ \ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
+\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}
+\ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
 \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
 \end{isabelle}
 Simplification has yielded an equation for \isa{m} that will be used to
@@ -2042,8 +2039,7 @@
 \ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
 \ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36
 \end{isabelle}
-
-The first subgoal is trivial, but for the second Isabelle needs help to eliminate
+The first subgoal is trivial (\isa{blast}), but for the second Isabelle needs help to eliminate
 the case
 \isa{z}=35.  The second invocation  of {\isa{subgoal_tac}} leaves two
 subgoals: 
@@ -2056,8 +2052,8 @@
 \ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35
 \end{isabelle}
 
-Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic:
-the method {\isa{arith}}. For the second subgoal we apply the method \isa{force}, 
+Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic
+(\isa{arith}). For the second subgoal we apply the method \isa{force}, 
 which proceeds by assuming that \isa{z}=35 and arriving at a contradiction.