doc-src/TutorialI/Rules/rules.tex
changeset 10971 6852682eaf16
parent 10967 69937e62a28e
child 10978 5eebea8f359f
     1.1 --- a/doc-src/TutorialI/Rules/rules.tex	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4  like this:
     1.5  \[  \infer{P\conj Q}{P & Q} \]
     1.6  The rule introduces the conjunction
     1.7 -symbol~($\conj$) in its conclusion.  Of course, in Isabelle proofs we
     1.8 +symbol~($\conj$) in its conclusion.  In Isabelle proofs we
     1.9  mainly  reason backwards.  When we apply this rule, the subgoal already has
    1.10  the form of a conjunction; the proof step makes this conjunction symbol
    1.11  disappear. 
    1.12 @@ -170,7 +170,7 @@
    1.13  \isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE}
    1.14  \end{isabelle}
    1.15  When we use this sort of elimination rule backwards, it produces 
    1.16 -a case split.  (We have this before, in proofs by induction.)  The following  proof
    1.17 +a case split.  (We have seen this before, in proofs by induction.)  The following  proof
    1.18  illustrates the use of disjunction elimination.  
    1.19  \begin{isabelle}
    1.20  \isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\ 
    1.21 @@ -184,7 +184,7 @@
    1.22  We assume \isa{P\ \isasymor\ Q} and
    1.23  must prove \isa{Q\ \isasymor\ P}\@.  Our first step uses the disjunction
    1.24  elimination rule, \isa{disjE}.  The method {\isa{erule}}  applies an
    1.25 -elimination rule to the assumptions, searching for one that matches the
    1.26 +elimination rule, searching for an assumption that matches the
    1.27  rule's first premise.  Deleting that assumption, it
    1.28  return the subgoals for the remaining premises.  Most of the
    1.29  time, this is  the best way to use elimination rules; only rarely is there
    1.30 @@ -394,7 +394,7 @@
    1.31  As we have seen, Isabelle rules involve variables that begin  with a
    1.32  question mark. These are called \textbf{schematic} variables  and act as
    1.33  placeholders for terms. \textbf{Unification} refers to  the process of
    1.34 -making two terms identical, possibly by replacing  their variables by
    1.35 +making two terms identical, possibly by replacing their schematic variables by
    1.36  terms. The simplest case is when the two terms  are already the same. Next
    1.37  simplest is when the variables in only one of the term
    1.38   are replaced; this is called \textbf{pattern-matching}.  The
    1.39 @@ -440,7 +440,7 @@
    1.40  A typical substitution rule allows us to replace one term by 
    1.41  another if we know that two terms are equal. 
    1.42  \[ \infer{P[t/x]}{s=t & P[s/x]} \]
    1.43 -The conclusion uses a notation for substitution: $P[t/x]$ is the result of
    1.44 +The rule uses a notation for substitution: $P[t/x]$ is the result of
    1.45  replacing $x$ by~$t$ in~$P$.  The rule only substitutes in the positions
    1.46  designated by~$x$.  For example, it can
    1.47  derive symmetry of equality from reflexivity.  Using $x=s$ for~$P$
    1.48 @@ -566,7 +566,7 @@
    1.49  \isa{erule_tac} since above we used \isa{erule}.
    1.50  \begin{isabelle}
    1.51  \isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
    1.52 -\isacommand{by}\ (erule_tac\ P="\isasymlambda u.\ P\ u\ u\ x"\ 
    1.53 +\isacommand{by}\ (erule_tac\ P = "\isasymlambda u.\ P\ u\ u\ x"\ 
    1.54  \isakeyword{in}\ ssubst)
    1.55  \end{isabelle}
    1.56  %
    1.57 @@ -580,7 +580,7 @@
    1.58  An alternative to \isa{rule_tac} is to use \isa{rule} with the
    1.59  \isa{of} directive, described in \S\ref{sec:forward} below.   An
    1.60  advantage  of \isa{rule_tac} is that the instantiations may refer to 
    1.61 -variables bound in the current subgoal.
    1.62 +\isasymAnd-bound variables in the current subgoal.
    1.63  
    1.64  
    1.65  \section{Negation}
    1.66 @@ -632,7 +632,7 @@
    1.67  \isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\
    1.68  \isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\
    1.69  R"\isanewline
    1.70 -\isacommand{apply}\ (erule_tac\ Q="R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
    1.71 +\isacommand{apply}\ (erule_tac\ Q = "R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
    1.72  contrapos_np)\isanewline
    1.73  \isacommand{apply}\ intro\isanewline
    1.74  \isacommand{by}\ (erule\ notE)
    1.75 @@ -664,7 +664,7 @@
    1.76  \isa{by} command.
    1.77  Now when Isabelle selects the first assumption, it tries to prove \isa{P\
    1.78  \isasymlongrightarrow\ Q} and fails; it then backtracks, finds the 
    1.79 -assumption~\isa{\isasymnot\ R} and finally proves \isa{R} by assumption.  That
    1.80 +assumption \isa{\isasymnot~R} and finally proves \isa{R} by assumption.  That
    1.81  concludes the proof.
    1.82  
    1.83  \medskip
    1.84 @@ -691,7 +691,8 @@
    1.85  \end{isabelle}
    1.86  Next we apply the {\isa{elim}} method, which repeatedly applies 
    1.87  elimination rules; here, the elimination rules given 
    1.88 -in the command.  One of the subgoals is trivial, leaving us with one other:
    1.89 +in the command.  One of the subgoals is trivial (\isa{\isacommand{apply} assumption}),
    1.90 +leaving us with one other:
    1.91  \begin{isabelle}
    1.92  \ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P%
    1.93  \end{isabelle}
    1.94 @@ -704,8 +705,7 @@
    1.95  is robust: the \isa{conjI} forces the \isa{erule} to select a
    1.96  conjunction.  The two subgoals are the ones we would expect from applying
    1.97  conjunction introduction to
    1.98 -\isa{Q\
    1.99 -\isasymand\ R}:  
   1.100 +\isa{Q~\isasymand~R}:  
   1.101  \begin{isabelle}
   1.102  \ 1.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\
   1.103  Q\isanewline
   1.104 @@ -926,10 +926,12 @@
   1.105  \end{isabelle}
   1.106  If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
   1.107  P(x)$ is also true.  It is a dual of the universal elimination rule, and
   1.108 -logic texts present it using the same notation for substitution.  The existential
   1.109 +logic texts present it using the same notation for substitution.
   1.110 +
   1.111 +The existential
   1.112  elimination rule looks like this
   1.113  in a logic text: 
   1.114 -\[ \infer{R}{\exists x.\,P & \infer*{R}{[P]}} \]
   1.115 +\[ \infer{Q}{\exists x.\,P & \infer*{Q}{[P]}} \]
   1.116  %
   1.117  It looks like this in Isabelle: 
   1.118  \begin{isabelle}
   1.119 @@ -953,17 +955,18 @@
   1.120  
   1.121  
   1.122  \section{Hilbert's Epsilon-Operator}
   1.123 +\label{sec:SOME}
   1.124  
   1.125 -Isabelle/HOL provides Hilbert's
   1.126 -$\epsilon$-operator.  The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
   1.127 +HOL provides Hilbert's
   1.128 +$\varepsilon$-operator.  The term $\varepsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
   1.129  true, provided such a value exists.  Using this operator, we can express an
   1.130  existential destruction rule:
   1.131 -\[ \infer{P[(\epsilon x. P) / \, x]}{\exists x.\,P} \]
   1.132 +\[ \infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P} \]
   1.133  This rule is seldom used, for it can cause exponential blow-up.  
   1.134  
   1.135  \subsection{Definite Descriptions}
   1.136  
   1.137 -In ASCII, we write \isa{SOME} for $\epsilon$.
   1.138 +In ASCII, we write \isa{SOME} for $\varepsilon$.
   1.139  \REMARK{the internal constant is \isa{Eps}}
   1.140  The main use of \hbox{\isa{SOME\ x.\ P\ x}} is as a \textbf{definite
   1.141  description}: when \isa{P} is satisfied by a unique value,~\isa{a}. 
   1.142 @@ -979,7 +982,7 @@
   1.143  prove that the cardinality of the empty set is zero (since $n=0$ satisfies the
   1.144  description) and proceed to prove other facts.
   1.145  
   1.146 -Here is an example.  HOL defines \isa{inv},\indexbold{*inv (constant)}
   1.147 +Here is another example.  Isabelle/HOL defines \isa{inv},\indexbold{*inv (constant)}
   1.148  which expresses inverses of functions, as a definite
   1.149  description:
   1.150  \begin{isabelle}
   1.151 @@ -1025,7 +1028,6 @@
   1.152  \ 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
   1.153  \ \ \ \ \ \ \ \ \isasymLongrightarrow \ x\ =\ k%
   1.154  \end{isabelle}
   1.155 -
   1.156  As always with \isa{some_equality}, we must show existence and
   1.157  uniqueness of the claimed solution,~\isa{k}.  Existence, the first
   1.158  subgoal, is trivial.  Uniqueness, the second subgoal, follows by antisymmetry:
   1.159 @@ -1063,6 +1065,7 @@
   1.160  \ "(\isasymforall x.\ \isasymexists \ y.\ P\ x\ y)\ \isasymLongrightarrow \
   1.161  \isasymexists f.\ \isasymforall x.\ P\ x\ (f\ x)"\isanewline
   1.162  \isacommand{apply}\ (rule\ exI,\ rule\ allI)\isanewline
   1.163 +
   1.164  \ 1.\ \isasymAnd x.\ \isasymforall x.\ \isasymexists y.\ P\ x\ y\
   1.165  \isasymLongrightarrow \ P\ x\ (?f\ x)
   1.166  \end{isabelle}
   1.167 @@ -1072,6 +1075,7 @@
   1.168  
   1.169  \begin{isabelle}
   1.170  \isacommand{apply}\ (drule\ spec,\ erule\ exE)\isanewline
   1.171 +
   1.172  \ 1.\ \isasymAnd x\ y.\ P\ (?x2\ x)\ y\ \isasymLongrightarrow \ P\ x\ (?f\ x)
   1.173  \end{isabelle}
   1.174  
   1.175 @@ -1141,7 +1145,8 @@
   1.176  \begin{isabelle}
   1.177  *** empty result sequence -- proof command failed
   1.178  \end{isabelle}
   1.179 -We can tell Isabelle to abandon a failed proof using the \isacommand{oops} command.
   1.180 +If we interact with Isabelle via the shell interface,
   1.181 +we abandon a failed proof with the \isacommand{oops} command.
   1.182  
   1.183  \medskip 
   1.184  
   1.185 @@ -1301,7 +1306,7 @@
   1.186  \begin{isabelle}
   1.187  \isacommand{lemma}\
   1.188  [iff]:\ "(xs{\isacharat}ys\ =\ [])\ =\
   1.189 -(xs=[]\ \isacharampersand\ ys=[])"\isanewline
   1.190 +(xs=[]\ \isasymand\ ys=[])"\isanewline
   1.191  \isacommand{apply}\ (induct_tac\ xs)\isanewline
   1.192  \isacommand{apply}\ (simp_all)\isanewline
   1.193  \isacommand{done}
   1.194 @@ -1314,7 +1319,7 @@
   1.195  (\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
   1.196  \end{isabelle}
   1.197  A product is zero if and only if one of the factors is zero.  The
   1.198 -reasoning  involves a logical \textsc{or}.  Proving new rules for
   1.199 +reasoning  involves a disjunction.  Proving new rules for
   1.200  disjunctive reasoning  is hard, but translating to an actual disjunction
   1.201  works:  the classical reasoner handles disjunction properly.
   1.202  
   1.203 @@ -1490,8 +1495,8 @@
   1.204  We state it with the \isa{iff} attribute so that 
   1.205  Isabelle can use it to remove some occurrences of \isa{gcd}. 
   1.206  The theorem has a one-line 
   1.207 -proof using \isa{blast} supplied with four introduction 
   1.208 -rules: note the {\isa{intro}} attribute. The exclamation mark 
   1.209 +proof using \isa{blast} supplied with two additional introduction 
   1.210 +rules. The exclamation mark 
   1.211  ({\isa{intro}}{\isa{!}})\ signifies safe rules, which are 
   1.212  applied aggressively.  Rules given without the exclamation mark 
   1.213  are applied reluctantly and their uses can be undone if 
   1.214 @@ -1519,8 +1524,8 @@
   1.215  
   1.216  Of the latter methods, the most useful is {\isa{clarify}}. It performs 
   1.217  all obvious reasoning steps without splitting the goal into multiple 
   1.218 -parts. It does not apply rules that could render the 
   1.219 -goal unprovable (so-called unsafe rules). By performing the obvious 
   1.220 +parts. It does not apply unsafe rules that could render the 
   1.221 +goal unprovable. By performing the obvious 
   1.222  steps, {\isa{clarify}} lays bare the difficult parts of the problem, 
   1.223  where human intervention is necessary. 
   1.224  
   1.225 @@ -1568,7 +1573,7 @@
   1.226  That makes them slower but enables them to work correctly in the 
   1.227  presence of the more unusual features of Isabelle rules, such 
   1.228  as type classes and function unknowns. For example, recall the introduction rule
   1.229 -for Hilbert's epsilon-operator: 
   1.230 +for Hilbert's $\varepsilon$-operator: 
   1.231  \begin{isabelle}
   1.232  ?P\ ?x\ \isasymLongrightarrow\ ?P\ (SOME\ x.\ ?P x)
   1.233  \rulename{someI}
   1.234 @@ -1796,7 +1801,7 @@
   1.235  instance of a rule by specifying facts for its premises.  Let us try
   1.236  it with this rule:
   1.237  \begin{isabelle}
   1.238 -\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ (?m * ?n)\isasymrbrakk\
   1.239 +\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\
   1.240  \isasymLongrightarrow\ ?k\ dvd\ ?m
   1.241  \rulename{relprime_dvd_mult}
   1.242  \end{isabelle}
   1.243 @@ -1809,7 +1814,7 @@
   1.244  We have evaluated an application of the \isa{gcd} function by
   1.245  simplification.  Expression evaluation  is not guaranteed to terminate, and
   1.246  certainly is not  efficient; Isabelle performs arithmetic operations by 
   1.247 -rewriting symbolic bit strings.  Here, however, the simplification takes
   1.248 +rewriting symbolic bit strings.  Here, however, the simplification above takes
   1.249  less than one second.  We can specify this new lemma to \isa{OF},
   1.250  generating an instance of \isa{relprime_dvd_mult}.  The expression
   1.251  \begin{isabelle}
   1.252 @@ -1826,7 +1831,7 @@
   1.253  \isasymlbrakk?k\ dvd\ ?m;\
   1.254  ?k\ dvd\ ?n\isasymrbrakk\
   1.255  \isasymLongrightarrow\ ?k\ dvd\
   1.256 -(?m\ +\ ?n)
   1.257 +?m\ +\ ?n
   1.258  \rulename{dvd_add}\isanewline
   1.259  ?m\ dvd\ ?m%
   1.260  \rulename{dvd_refl}
   1.261 @@ -1846,7 +1851,7 @@
   1.262  \end{isabelle}
   1.263  The result is 
   1.264  \begin{isabelle}
   1.265 -\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ +\ ?k)
   1.266 +\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ ?m\ +\ ?k
   1.267  \end{isabelle}
   1.268  
   1.269  You may have noticed that \isa{THEN} and \isa{OF} are based on 
   1.270 @@ -1933,7 +1938,7 @@
   1.271  \begin{isabelle}
   1.272  \isacommand{lemma}\
   1.273  relprime_dvd_mult:\isanewline
   1.274 -\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\ k\ dvd\ (m*n)\
   1.275 +\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\ k\ dvd\ m*n\
   1.276  \isasymrbrakk\
   1.277  \isasymLongrightarrow\ k\ dvd\
   1.278  m"\isanewline
   1.279 @@ -1943,11 +1948,7 @@
   1.280  In the resulting subgoal, note how the equation has been 
   1.281  inserted: 
   1.282  \begin{isabelle}
   1.283 -\isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\
   1.284 -dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
   1.285 -m\isanewline
   1.286 -\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
   1.287 -\ \ \ \ \ m\ *\ gcd\
   1.288 +\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ m\ *\ n{;}\ m\ *\ gcd\
   1.289  (k,\ n)\
   1.290  =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
   1.291  \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
   1.292 @@ -1956,12 +1957,8 @@
   1.293  utilizes the assumption \isa{gcd(k,n)\ =\
   1.294  1}. Here is the result: 
   1.295  \begin{isabelle}
   1.296 -\isasymlbrakk gcd\ (k,\
   1.297 -n)\ =\ 1;\ k\
   1.298 -dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
   1.299 -m\isanewline
   1.300 -\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
   1.301 -\ \ \ \ \ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
   1.302 +\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}
   1.303 +\ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
   1.304  \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
   1.305  \end{isabelle}
   1.306  Simplification has yielded an equation for \isa{m} that will be used to
   1.307 @@ -2042,8 +2039,7 @@
   1.308  \ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
   1.309  \ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36
   1.310  \end{isabelle}
   1.311 -
   1.312 -The first subgoal is trivial, but for the second Isabelle needs help to eliminate
   1.313 +The first subgoal is trivial (\isa{blast}), but for the second Isabelle needs help to eliminate
   1.314  the case
   1.315  \isa{z}=35.  The second invocation  of {\isa{subgoal_tac}} leaves two
   1.316  subgoals: 
   1.317 @@ -2056,8 +2052,8 @@
   1.318  \ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35
   1.319  \end{isabelle}
   1.320  
   1.321 -Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic:
   1.322 -the method {\isa{arith}}. For the second subgoal we apply the method \isa{force}, 
   1.323 +Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic
   1.324 +(\isa{arith}). For the second subgoal we apply the method \isa{force}, 
   1.325  which proceeds by assuming that \isa{z}=35 and arriving at a contradiction.
   1.326  
   1.327