1.1 --- a/doc-src/TutorialI/Rules/rules.tex Tue Dec 05 18:55:45 2000 +0100
1.2 +++ b/doc-src/TutorialI/Rules/rules.tex Tue Dec 05 18:56:18 2000 +0100
1.3 @@ -92,7 +92,7 @@
1.4
1.5 The following trivial proof illustrates this point.
1.6 \begin{isabelle}
1.7 -\isacommand{lemma}\ conj_rule:\ "{\isasymlbrakk}P;\
1.8 +\isacommand{lemma}\ conj_rule:\ "\isasymlbrakk P;\
1.9 Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\
1.10 (Q\ \isasymand\ P)"\isanewline
1.11 \isacommand{apply}\ (rule\ conjI)\isanewline
1.12 @@ -107,31 +107,31 @@
1.13 (Q\ \isasymand\ P)}. We are working backwards, so when we
1.14 apply conjunction introduction, the rule removes the outermost occurrence
1.15 of the \isa{\isasymand} symbol. To apply a rule to a subgoal, we apply
1.16 -the proof method {\isa{rule}} --- here with {\isa{conjI}}, the conjunction
1.17 +the proof method \isa{rule} --- here with {\isa{conjI}}, the conjunction
1.18 introduction rule.
1.19 \begin{isabelle}
1.20 -%{\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\
1.21 +%\isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\
1.22 %\isasymand\ P\isanewline
1.23 -\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
1.24 -\ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P
1.25 +\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
1.26 +\ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P
1.27 \end{isabelle}
1.28 Isabelle leaves two new subgoals: the two halves of the original conjunction.
1.29 The first is simply \isa{P}, which is trivial, since \isa{P} is among
1.30 -the assumptions. We can apply the {\isa{assumption}}
1.31 +the assumptions. We can apply the \isa{assumption}
1.32 method, which proves a subgoal by finding a matching assumption.
1.33 \begin{isabelle}
1.34 -\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\
1.35 +\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\
1.36 Q\ \isasymand\ P
1.37 \end{isabelle}
1.38 We are left with the subgoal of proving
1.39 \isa{Q\ \isasymand\ P} from the assumptions \isa{P} and~\isa{Q}. We apply
1.40 \isa{rule conjI} again.
1.41 \begin{isabelle}
1.42 -\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline
1.43 -\ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P
1.44 +\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline
1.45 +\ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P
1.46 \end{isabelle}
1.47 We are left with two new subgoals, \isa{Q} and~\isa{P}, each of which can be proved
1.48 -using the {\isa{assumption}} method.
1.49 +using the \isa{assumption} method.
1.50
1.51
1.52 \section{Elimination rules}
1.53 @@ -198,12 +198,12 @@
1.54 second assumes \isa{Q}. Tackling the first subgoal, we need to
1.55 show \isa{Q\ \isasymor\ P}\@. The second introduction rule (\isa{disjI2})
1.56 can reduce this to \isa{P}, which matches the assumption. So, we apply the
1.57 -{\isa{rule}} method with \isa{disjI2} \ldots
1.58 +\isa{rule} method with \isa{disjI2} \ldots
1.59 \begin{isabelle}
1.60 \ 1.\ P\ \isasymLongrightarrow\ P\isanewline
1.61 \ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
1.62 \end{isabelle}
1.63 -\ldots and finish off with the {\isa{assumption}}
1.64 +\ldots and finish off with the \isa{assumption}
1.65 method. We are left with the other subgoal, which
1.66 assumes \isa{Q}.
1.67 \begin{isabelle}
1.68 @@ -324,12 +324,12 @@
1.69 \begin{isabelle}
1.70 %P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R\ \isasymLongrightarrow\ P\
1.71 %\isasymand\ Q\ \isasymlongrightarrow\ R\isanewline
1.72 -\ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R
1.73 +\ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R
1.74 \end{isabelle}
1.75 Next, we apply conjunction elimination (\isa{erule conjE}), which splits this
1.76 conjunction into two parts.
1.77 \begin{isabelle}
1.78 -\ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\
1.79 +\ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\
1.80 Q\isasymrbrakk\ \isasymLongrightarrow\ R
1.81 \end{isabelle}
1.82 Now, we work on the assumption \isa{P\ \isasymlongrightarrow\ (Q\
1.83 @@ -340,13 +340,13 @@
1.84 \isasymlongrightarrow\ R}, but first we must prove the extra subgoal
1.85 \isa{P}, which we do by assumption.
1.86 \begin{isabelle}
1.87 -\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
1.88 -\ 2.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R
1.89 +\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
1.90 +\ 2.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R
1.91 \end{isabelle}
1.92 Repeating these steps for \isa{Q\
1.93 \isasymlongrightarrow\ R} yields the conclusion we seek, namely~\isa{R}.
1.94 \begin{isabelle}
1.95 -\ 1.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\
1.96 +\ 1.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\
1.97 \isasymLongrightarrow\ R
1.98 \end{isabelle}
1.99
1.100 @@ -380,9 +380,9 @@
1.101 terms. The simplest case is when the two terms are already the same. Next
1.102 simplest is when the variables in only one of the term
1.103 are replaced; this is called \textbf{pattern-matching}. The
1.104 -{\isa{rule}} method typically matches the rule's conclusion
1.105 +\isa{rule} method typically matches the rule's conclusion
1.106 against the current subgoal. In the most complex case, variables in both
1.107 -terms are replaced; the {\isa{rule}} method can do this the goal
1.108 +terms are replaced; the \isa{rule} method can do this the goal
1.109 itself contains schematic variables. Other occurrences of the variables in
1.110 the rule or proof state are updated at the same time.
1.111
1.112 @@ -445,10 +445,8 @@
1.113 rule gives us more control. Consider this proof:
1.114 \begin{isabelle}
1.115 \isacommand{lemma}\
1.116 -"{\isasymlbrakk}\ x\
1.117 -=\ f\ x;\ odd(f\
1.118 -x)\ \isasymrbrakk\ \isasymLongrightarrow\ odd\
1.119 -x"\isanewline
1.120 +"\isasymlbrakk \ x\ =\ f\ x;\ odd(f\ x)\ \isasymrbrakk\ \isasymLongrightarrow\
1.121 +odd\ x"\isanewline
1.122 \isacommand{apply}\ (erule\ ssubst)\isanewline
1.123 \isacommand{apply}\ assumption\isanewline
1.124 \isacommand{done}\end{isabelle}
1.125 @@ -471,7 +469,7 @@
1.126
1.127 Higher-order unification can be tricky, as this example indicates:
1.128 \begin{isabelle}
1.129 -\isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\
1.130 +\isacommand{lemma}\ "\isasymlbrakk \ x\ =\
1.131 f\ x;\ triple\ (f\ x)\
1.132 (f\ x)\ x\ \isasymrbrakk\
1.133 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
1.134 @@ -525,9 +523,7 @@
1.135 use. We get a one-line proof of our example:
1.136 \begin{isabelle}
1.137 \isacommand{lemma}\
1.138 -"{\isasymlbrakk}\ x\
1.139 -=\ f\ x;\ triple\ (f\
1.140 -x)\ (f\ x)\ x\
1.141 +"\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\
1.142 \isasymrbrakk\
1.143 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
1.144 \isacommand{apply}\ (erule\ ssubst,\ assumption)\isanewline
1.145 @@ -535,18 +531,16 @@
1.146 \end{isabelle}
1.147
1.148 The most general way to get rid of the {\isa{back}} command is
1.149 -to instantiate variables in the rule. The method {\isa{rule\_tac}} is
1.150 +to instantiate variables in the rule. The method \isa{rule_tac} is
1.151 similar to \isa{rule}, but it
1.152 makes some of the rule's variables denote specified terms.
1.153 -Also available are {\isa{drule\_tac}} and \isa{erule\_tac}. Here we need
1.154 -\isa{erule\_tac} since above we used
1.155 +Also available are {\isa{drule_tac}} and \isa{erule_tac}. Here we need
1.156 +\isa{erule_tac} since above we used
1.157 \isa{erule}.
1.158 \begin{isabelle}
1.159 -\isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
1.160 -\isacommand{apply}\ (erule_tac\
1.161 -P="{\isasymlambda}u.\ triple\ u\
1.162 -u\ x"\ \isakeyword{in}\
1.163 -ssubst)\isanewline
1.164 +\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
1.165 +\isacommand{apply}\ (erule_tac\ P="{\isasymlambda}u.\ triple\ u\ u\ x"\
1.166 +\isakeyword{in}\ ssubst)\isanewline
1.167 \isacommand{apply}\ assumption\isanewline
1.168 \isacommand{done}
1.169 \end{isabelle}
1.170 @@ -557,9 +551,9 @@
1.171 u\ x} indicate that the first two arguments have to be substituted, leaving
1.172 the third unchanged.
1.173
1.174 -An alternative to {\isa{rule\_tac}} is to use \isa{rule} with the
1.175 -{\isa{of}} directive, described in \S\ref{sec:forward} below. An
1.176 -advantage of {\isa{rule\_tac}} is that the instantiations may refer to
1.177 +An alternative to \isa{rule_tac} is to use \isa{rule} with the
1.178 +\isa{of} directive, described in \S\ref{sec:forward} below. An
1.179 +advantage of \isa{rule_tac} is that the instantiations may refer to
1.180 variables bound in the current subgoal.
1.181
1.182
1.183 @@ -633,7 +627,8 @@
1.184
1.185 We can now apply introduction rules. We use the {\isa{intro}} method, which
1.186 repeatedly applies built-in introduction rules. Here its effect is equivalent
1.187 -to \isa{rule impI}.\begin{isabelle}
1.188 +to \isa{rule impI}.
1.189 +\begin{isabelle}
1.190 \ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ R;\
1.191 R\isasymrbrakk\ \isasymLongrightarrow\ Q%
1.192 \end{isabelle}
1.193 @@ -696,9 +691,9 @@
1.194 \isa{Q\
1.195 \isasymand\ R}:
1.196 \begin{isabelle}
1.197 -\ 1.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\
1.198 +\ 1.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\
1.199 Q\isanewline
1.200 -\ 2.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R%
1.201 +\ 2.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R%
1.202 \end{isabelle}
1.203 The rest of the proof is trivial.
1.204
1.205 @@ -723,7 +718,7 @@
1.206 Returning to the universal quantifier, we find that having a similar quantifier
1.207 as part of the meta-logic makes the introduction rule trivial to express:
1.208 \begin{isabelle}
1.209 -({\isasymAnd}x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI}
1.210 +(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI}
1.211 \end{isabelle}
1.212
1.213
1.214 @@ -738,7 +733,7 @@
1.215 The first step invokes the rule by applying the method \isa{rule allI}.
1.216 \begin{isabelle}
1.217 %{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x\isanewline
1.218 -\ 1.\ {\isasymAnd}x.\ P\ x\ \isasymlongrightarrow\ P\ x
1.219 +\ 1.\ \isasymAnd x.\ P\ x\ \isasymlongrightarrow\ P\ x
1.220 \end{isabelle}
1.221 Note that the resulting proof state has a bound variable,
1.222 namely~\bigisa{x}. The rule has replaced the universal quantifier of
1.223 @@ -747,9 +742,9 @@
1.224 \isa{P\ x\ \isasymlongrightarrow\ P\ x} for arbitrary~\isa{x}; it is
1.225 an implication, so we apply the corresponding introduction rule (\isa{impI}).
1.226 \begin{isabelle}
1.227 -\ 1.\ {\isasymAnd}x.\ P\ x\ \isasymLongrightarrow\ P\ x
1.228 +\ 1.\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow\ P\ x
1.229 \end{isabelle}
1.230 -The {\isa{assumption}} method proves this last subgoal.
1.231 +The \isa{assumption} method proves this last subgoal.
1.232
1.233 \medskip
1.234 Now consider universal elimination. In a logic text,
1.235 @@ -792,7 +787,7 @@
1.236 \begin{isabelle}
1.237 %{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x\ \isasymLongrightarrow\ P\
1.238 %\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)\isanewline
1.239 -\ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x
1.240 +\ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x
1.241 \end{isabelle}
1.242 As before, it replaces the HOL
1.243 quantifier by a meta-level quantifier, producing a subgoal that
1.244 @@ -809,8 +804,8 @@
1.245 method. This rule is called \isa{spec} because it specializes a universal formula
1.246 to a particular term.
1.247 \begin{isabelle}
1.248 -\ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ P\ \isasymlongrightarrow\ Q\ (?x2\
1.249 -x){\isasymrbrakk}\ \isasymLongrightarrow\ Q\ x
1.250 +\ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ P\ \isasymlongrightarrow\ Q\ (?x2\
1.251 +x)\isasymrbrakk\ \isasymLongrightarrow\ Q\ x
1.252 \end{isabelle}
1.253 Observe how the context has changed. The quantified formula is gone,
1.254 replaced by a new assumption derived from its body. Informally, we have
1.255 @@ -822,7 +817,7 @@
1.256 an implication, so we can use \emph{modus ponens} on it. As before, it requires
1.257 proving the antecedent (in this case \isa{P}) and leaves us with the consequent.
1.258 \begin{isabelle}
1.259 -\ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ Q\ (?x2\ x){\isasymrbrakk}\
1.260 +\ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ Q\ (?x2\ x)\isasymrbrakk\
1.261 \isasymLongrightarrow\ Q\ x
1.262 \end{isabelle}
1.263 The consequent is \isa{Q} applied to that placeholder. It may be replaced by any
1.264 @@ -889,7 +884,7 @@
1.265 %
1.266 It looks like this in Isabelle:
1.267 \begin{isabelle}
1.268 -\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ {\isasymAnd}x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE}
1.269 +\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE}
1.270 \end{isabelle}
1.271 %
1.272 Given an existentially quantified theorem and some
1.273 @@ -943,13 +938,13 @@
1.274 \begin{isabelle}
1.275 %({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\
1.276 %\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x\isanewline
1.277 -\ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
1.278 +\ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
1.279 \end{isabelle}
1.280 %
1.281 When we remove the other quantifier, we get a different bound
1.282 variable in the subgoal. (The name \isa{xa} is generated automatically.)
1.283 \begin{isabelle}
1.284 -\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\
1.285 +\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\
1.286 \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
1.287 \end{isabelle}
1.288 The proviso of the existential elimination rule has forced the variables to
1.289 @@ -961,15 +956,15 @@
1.290 and the other to become~\bigisa{xa}, but Isabelle requires all instances of a
1.291 placeholder to be identical.
1.292 \begin{isabelle}
1.293 -\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\
1.294 +\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\
1.295 \isasymLongrightarrow\ P\ (?x3\ x\ xa)\isanewline
1.296 -\ 2.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa)
1.297 +\ 2.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa)
1.298 \end{isabelle}
1.299 We can prove either subgoal
1.300 using the \isa{assumption} method. If we prove the first one, the placeholder
1.301 changes into~\bigisa{x}.
1.302 \begin{isabelle}
1.303 -\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\
1.304 +\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\
1.305 \isasymLongrightarrow\ Q\ x
1.306 \end{isabelle}
1.307 We are left with a subgoal that cannot be proved,
1.308 @@ -1007,13 +1002,13 @@
1.309 Next, we remove the universal quantifier
1.310 from the conclusion, putting the bound variable~\isa{y} into the subgoal.
1.311 \begin{isabelle}
1.312 -\ 1.\ {\isasymAnd}y.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ R\ ?x\ y
1.313 +\ 1.\ \isasymAnd y.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ R\ ?x\ y
1.314 \end{isabelle}
1.315 Finally, we try to apply our reflexivity assumption. We obtain a
1.316 new assumption whose identical placeholders may be replaced by
1.317 any term involving~\bigisa{y}.
1.318 \begin{isabelle}
1.319 -\ 1.\ {\isasymAnd}y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y
1.320 +\ 1.\ \isasymAnd y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y
1.321 \end{isabelle}
1.322 This subgoal can only be proved by putting \bigisa{y} for all the placeholders,
1.323 making the assumption and conclusion become \isa{R\ y\ y}.
1.324 @@ -1036,7 +1031,7 @@
1.325 discussed, concerning negation and disjunction. Isabelle's
1.326 \textbf{classical reasoner} is a family of tools that perform such
1.327 proofs automatically. The most important of these is the
1.328 -{\isa{blast}} method.
1.329 +\isa{blast} method.
1.330
1.331 In this section, we shall first see how to use the classical
1.332 reasoner in its default mode and then how to insert additional
1.333 @@ -1048,7 +1043,7 @@
1.334 \footnote{Pelletier~\cite{pelletier86} describes it and many other
1.335 problems for automatic theorem provers.}
1.336 The nested biconditionals cause an exponential explosion: the formal
1.337 -proof is enormous. However, the {\isa{blast}} method proves it in
1.338 +proof is enormous. However, the \isa{blast} method proves it in
1.339 a fraction of a second.
1.340 \begin{isabelle}
1.341 \isacommand{lemma}\
1.342 @@ -1072,7 +1067,7 @@
1.343 \isacommand{done}
1.344 \end{isabelle}
1.345 The next example is a logic problem composed by Lewis Carroll.
1.346 -The {\isa{blast}} method finds it trivial. Moreover, it turns out
1.347 +The \isa{blast} method finds it trivial. Moreover, it turns out
1.348 that not all of the assumptions are necessary. We can easily
1.349 experiment with variations of this formula and see which ones
1.350 can be proved.
1.351 @@ -1108,7 +1103,7 @@
1.352 \isacommand{apply}\ blast\isanewline
1.353 \isacommand{done}
1.354 \end{isabelle}
1.355 -The {\isa{blast}} method is also effective for set theory, which is
1.356 +The \isa{blast} method is also effective for set theory, which is
1.357 described in the next chapter. This formula below may look horrible, but
1.358 the \isa{blast} method proves it easily.
1.359 \begin{isabelle}
1.360 @@ -1133,7 +1128,7 @@
1.361 An important special case avoids all these complications. A logical
1.362 equivalence, which in higher-order logic is an equality between
1.363 formulas, can be given to the classical
1.364 -reasoner and simplifier by using the attribute {\isa{iff}}. You
1.365 +reasoner and simplifier by using the attribute \isa{iff}. You
1.366 should do so if the right hand side of the equivalence is
1.367 simpler than the left-hand side.
1.368
1.369 @@ -1141,7 +1136,7 @@
1.370 The result of appending two lists is empty if and only if both
1.371 of the lists are themselves empty. Obviously, applying this equivalence
1.372 will result in a simpler goal. When stating this lemma, we include
1.373 -the {\isa{iff}} attribute. Once we have proved the lemma, Isabelle
1.374 +the \isa{iff} attribute. Once we have proved the lemma, Isabelle
1.375 will make it known to the classical reasoner (and to the simplifier).
1.376 \begin{isabelle}
1.377 \isacommand{lemma}\
1.378 @@ -1159,17 +1154,17 @@
1.379 \end{isabelle}
1.380 %
1.381 This fact about multiplication is also appropriate for
1.382 -the {\isa{iff}} attribute:\REMARK{the ?s are ugly here but we need
1.383 +the \isa{iff} attribute:\REMARK{the ?s are ugly here but we need
1.384 them again when talking about \isa{of}; we need a consistent style}
1.385 \begin{isabelle}
1.386 -(\mbox{?m}\ \isacharasterisk\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
1.387 +(\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
1.388 \end{isabelle}
1.389 A product is zero if and only if one of the factors is zero. The
1.390 reasoning involves a logical \textsc{or}. Proving new rules for
1.391 disjunctive reasoning is hard, but translating to an actual disjunction
1.392 works: the classical reasoner handles disjunction properly.
1.393
1.394 -In more detail, this is how the {\isa{iff}} attribute works. It converts
1.395 +In more detail, this is how the \isa{iff} attribute works. It converts
1.396 the equivalence $P=Q$ to a pair of rules: the introduction
1.397 rule $Q\Imp P$ and the destruction rule $P\Imp Q$. It gives both to the
1.398 classical reasoner as safe rules, ensuring that all occurrences of $P$ in
1.399 @@ -1186,23 +1181,23 @@
1.400
1.401 A brief development will illustrate advanced use of
1.402 \isa{blast}. In \S\ref{sec:recdef-simplification}, we declared the
1.403 -recursive function {\isa{gcd}}:
1.404 +recursive function \isa{gcd}:
1.405 \begin{isabelle}
1.406 -\isacommand{consts}\ gcd\ ::\ "nat{\isacharasterisk}nat\ \isasymRightarrow\ nat"\
1.407 +\isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\
1.408 \
1.409 \
1.410 \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
1.411 \isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n)\
1.412 -::nat{\isacharasterisk}nat\ \isasymRightarrow\ nat)"\isanewline
1.413 +::nat*nat\ \isasymRightarrow\ nat)"\isanewline
1.414 \ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))"
1.415 \end{isabelle}
1.416 Let us prove that it computes the greatest common
1.417 divisor of its two arguments.
1.418 %
1.419 %The declaration yields a recursion
1.420 -%equation for {\isa{gcd}}. Simplifying with this equation can
1.421 +%equation for \isa{gcd}. Simplifying with this equation can
1.422 %cause looping, expanding to ever-larger expressions of if-then-else
1.423 -%and {\isa{gcd}} calls. To prevent this, we prove separate simplification rules
1.424 +%and \isa{gcd} calls. To prevent this, we prove separate simplification rules
1.425 %for $n=0$\ldots
1.426 %\begin{isabelle}
1.427 %\isacommand{lemma}\ gcd_0\ [simp]:\ "gcd(m,0)\ =\ m"\isanewline
1.428 @@ -1219,18 +1214,18 @@
1.429 %does not loop because it is conditional. It can be applied only
1.430 %when the second argument is known to be non-zero.
1.431 %Armed with our two new simplification rules, we now delete the
1.432 -%original {\isa{gcd}} recursion equation.
1.433 +%original \isa{gcd} recursion equation.
1.434 %\begin{isabelle}
1.435 %\isacommand{declare}\ gcd.simps\ [simp\ del]
1.436 %\end{isabelle}
1.437 %
1.438 -%Now we can prove some interesting facts about the {\isa{gcd}} function,
1.439 +%Now we can prove some interesting facts about the \isa{gcd} function,
1.440 %for exampe, that it computes a common divisor of its arguments.
1.441 %
1.442 The theorem is expressed in terms of the familiar
1.443 \textbf{divides} relation from number theory:
1.444 \begin{isabelle}
1.445 -?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ \isacharasterisk\ k
1.446 +?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
1.447 \rulename{dvd_def}
1.448 \end{isabelle}
1.449 %
1.450 @@ -1251,12 +1246,12 @@
1.451 half of the conjunction establishes the other. The first three proof steps
1.452 are applying induction, performing a case analysis on \isa{n},
1.453 and simplifying. Let us pass over these quickly and consider
1.454 -the use of {\isa{blast}}. We have reached the following
1.455 +the use of \isa{blast}. We have reached the following
1.456 subgoal:
1.457 \begin{isabelle}
1.458 %gcd\ (m,\ n)\ dvd\ m\ \isasymand\ gcd\ (m,\ n)\ dvd\ n\isanewline
1.459 -\ 1.\ {\isasymAnd}m\ n.\ \isasymlbrakk0\ \isacharless\ n;\isanewline
1.460 - \ \ \ \ \ \ \ \ \ \ \ \ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand\ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n){\isasymrbrakk}\isanewline
1.461 +\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk0\ \isacharless\ n;\isanewline
1.462 + \ \ \ \ \ \ \ \ \ \ \ \ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand\ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n)\isasymrbrakk\isanewline
1.463 \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ gcd\ (n,\ m\ mod\ n)\ dvd\ m
1.464 \end{isabelle}
1.465 %
1.466 @@ -1292,7 +1287,7 @@
1.467 tells Isabelle to transform a theorem in some way and to
1.468 give a name to the resulting theorem. Attributes can be given,
1.469 here \isa{iff}, which supplies the new theorems to the classical reasoner
1.470 -and the simplifier. The directive {\isa{THEN}}, which will be explained
1.471 +and the simplifier. The directive \isa{THEN}, which will be explained
1.472 below, supplies the lemma
1.473 \isa{gcd_dvd_both} to the
1.474 destruction rule \isa{conjunct1} in order to extract the first part.
1.475 @@ -1313,7 +1308,7 @@
1.476 \end{isabelle}
1.477 Later, we shall explore this type of forward reasoning in detail.
1.478
1.479 -To complete the verification of the {\isa{gcd}} function, we must
1.480 +To complete the verification of the \isa{gcd} function, we must
1.481 prove that it returns the greatest of all the common divisors
1.482 of its arguments. The proof is by induction and simplification.
1.483 \begin{isabelle}
1.484 @@ -1347,12 +1342,12 @@
1.485 \isacommand{apply}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans)\isanewline
1.486 \isacommand{done}
1.487 \end{isabelle}
1.488 -This theorem concisely expresses the correctness of the {\isa{gcd}}
1.489 +This theorem concisely expresses the correctness of the \isa{gcd}
1.490 function.
1.491 -We state it with the {\isa{iff}} attribute so that
1.492 -Isabelle can use it to remove some occurrences of {\isa{gcd}}.
1.493 +We state it with the \isa{iff} attribute so that
1.494 +Isabelle can use it to remove some occurrences of \isa{gcd}.
1.495 The theorem has a one-line
1.496 -proof using {\isa{blast}} supplied with four introduction
1.497 +proof using \isa{blast} supplied with four introduction
1.498 rules: note the {\isa{intro}} attribute. The exclamation mark
1.499 ({\isa{intro}}{\isa{!}})\ signifies safe rules, which are
1.500 applied aggressively. Rules given without the exclamation mark
1.501 @@ -1374,7 +1369,7 @@
1.502
1.503 \section{Other classical reasoning methods}
1.504
1.505 -The {\isa{blast}} method is our main workhorse for proving theorems
1.506 +The \isa{blast} method is our main workhorse for proving theorems
1.507 automatically. Other components of the classical reasoner interact
1.508 with the simplifier. Still others perform classical reasoning
1.509 to a limited extent, giving the user fine control over the proof.
1.510 @@ -1393,10 +1388,10 @@
1.511 \isasymand\ Q\ x)"\isanewline
1.512 \isacommand{apply}\ clarify
1.513 \end{isabelle}
1.514 -The {\isa{blast}} method would simply fail, but {\isa{clarify}} presents
1.515 +The \isa{blast} method would simply fail, but {\isa{clarify}} presents
1.516 a subgoal that helps us see why we cannot continue the proof.
1.517 \begin{isabelle}
1.518 -\ 1.\ {\isasymAnd}x\ xa.\ \isasymlbrakk{\isasymforall}x.\ P\ x;\ Q\
1.519 +\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk{\isasymforall}x.\ P\ x;\ Q\
1.520 xa\isasymrbrakk\ \isasymLongrightarrow\ P\ x\ \isasymand\ Q\ x
1.521 \end{isabelle}
1.522 The proof must fail because the assumption \isa{Q\ xa} and conclusion \isa{Q\ x}
1.523 @@ -1423,8 +1418,8 @@
1.524 its goal, so it can take much longer to terminate.
1.525
1.526 Older components of the classical reasoner have largely been
1.527 -superseded by {\isa{blast}}, but they still have niche applications.
1.528 -Most important among these are {\isa{fast}} and {\isa{best}}. While {\isa{blast}}
1.529 +superseded by \isa{blast}, but they still have niche applications.
1.530 +Most important among these are \isa{fast} and \isa{best}. While \isa{blast}
1.531 searches for proofs using a built-in first-order reasoner, these
1.532 earlier methods search for proofs using standard Isabelle inference.
1.533 That makes them slower but enables them to work correctly in the
1.534 @@ -1439,7 +1434,7 @@
1.535 The repeated occurrence of the variable \isa{?P} makes this rule tricky
1.536 to apply. Consider this contrived example:
1.537 \begin{isabelle}
1.538 -\isacommand{lemma}\ "{\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\isanewline
1.539 +\isacommand{lemma}\ "\isasymlbrakk Q\ a;\ P\ a\isasymrbrakk\isanewline
1.540 \ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ P\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)\
1.541 \isasymand\ Q\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)"\isanewline
1.542 \isacommand{apply}\ (rule\ someI)
1.543 @@ -1448,21 +1443,21 @@
1.544 We can apply rule \isa{someI} explicitly. It yields the
1.545 following subgoal:
1.546 \begin{isabelle}
1.547 -\ 1.\ {\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P\ ?x\
1.548 +\ 1.\ \isasymlbrakk Q\ a;\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P\ ?x\
1.549 \isasymand\ Q\ ?x%
1.550 \end{isabelle}
1.551 The proof from this point is trivial. The question now arises, could we have
1.552 -proved the theorem with a single command? Not using {\isa{blast}} method: it
1.553 +proved the theorem with a single command? Not using \isa{blast} method: it
1.554 cannot perform the higher-order unification that is necessary here. The
1.555 -{\isa{fast}} method succeeds:
1.556 +\isa{fast} method succeeds:
1.557 \begin{isabelle}
1.558 \isacommand{apply}\ (fast\ intro!:\ someI)
1.559 \end{isabelle}
1.560
1.561 -The {\isa{best}} method is similar to {\isa{fast}} but it uses a
1.562 +The \isa{best} method is similar to \isa{fast} but it uses a
1.563 best-first search instead of depth-first search. Accordingly,
1.564 it is slower but is less susceptible to divergence. Transitivity
1.565 -rules usually cause {\isa{fast}} to loop where often {\isa{best}}
1.566 +rules usually cause \isa{fast} to loop where often \isa{best}
1.567 can manage.
1.568
1.569 Here is a summary of the classical reasoning methods:
1.570 @@ -1512,7 +1507,7 @@
1.571 Now let us reproduce our examples in Isabelle. Here is the distributive
1.572 law:
1.573 \begin{isabelle}%
1.574 -?k\ \isacharasterisk\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ \isacharasterisk\ ?m,\ ?k\ \isacharasterisk\ ?n)
1.575 +?k\ *\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ *\ ?m,\ ?k\ *\ ?n)
1.576 \rulename{gcd_mult_distrib2}
1.577 \end{isabelle}%
1.578 The first step is to replace \isa{?m} by~1 in this law. We refer to the
1.579 @@ -1529,7 +1524,7 @@
1.580 \isa{thm gcd_mult_0}
1.581 displays the resulting theorem:
1.582 \begin{isabelle}
1.583 -\ \ \ \ \ k\ \isacharasterisk\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ \isacharasterisk\ 1,\ k\ \isacharasterisk\ ?n)
1.584 +\ \ \ \ \ k\ *\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ *\ 1,\ k\ *\ ?n)
1.585 \end{isabelle}
1.586 Something is odd: {\isa{k}} is an ordinary variable, while {\isa{?n}}
1.587 is schematic. We did not specify an instantiation
1.588 @@ -1549,7 +1544,7 @@
1.589 %
1.590 Again, we display the resulting theorem:
1.591 \begin{isabelle}
1.592 -\ \ \ \ \ k\ =\ gcd\ (k,\ k\ \isacharasterisk\ ?n)
1.593 +\ \ \ \ \ k\ =\ gcd\ (k,\ k\ *\ ?n)
1.594 \end{isabelle}
1.595 %
1.596 To re-orient the equation requires the symmetry rule:
1.597 @@ -1567,12 +1562,11 @@
1.598 %
1.599 Here is the result:
1.600 \begin{isabelle}
1.601 -\ \ \ \ \ gcd\ (k,\ k\ \isacharasterisk\
1.602 -?n)\ =\ k%
1.603 +\ \ \ \ \ gcd\ (k,\ k\ *\ ?n)\ =\ k%
1.604 \end{isabelle}
1.605 \isa{THEN~sym} gives the current theorem to the rule \isa{sym} and returns the
1.606 resulting conclusion.\REMARK{figure necessary?} The effect is to exchange the
1.607 -two operands of the equality. Typically {\isa{THEN}} is used with destruction
1.608 +two operands of the equality. Typically \isa{THEN} is used with destruction
1.609 rules. Above we have used
1.610 \isa{THEN~conjunct1} to extract the first part of the theorem
1.611 \isa{gcd_dvd_both}. Also useful is \isa{THEN~spec}, which removes the quantifier
1.612 @@ -1581,13 +1575,10 @@
1.613 Similar to \isa{mp} are the following two rules, which extract
1.614 the two directions of reasoning about a boolean equivalence:
1.615 \begin{isabelle}
1.616 -\isasymlbrakk?Q\ =\
1.617 -?P;\ ?Q\isasymrbrakk\
1.618 -\isasymLongrightarrow\ ?P%
1.619 +\isasymlbrakk?Q\ =\ ?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
1.620 \rulename{iffD1}%
1.621 \isanewline
1.622 -\isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\
1.623 -\isasymLongrightarrow\ ?P%
1.624 +\isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
1.625 \rulename{iffD2}
1.626 \end{isabelle}
1.627 %
1.628 @@ -1609,9 +1600,7 @@
1.629 \begin{isabelle}
1.630 \isacommand{lemma}\ gcd_mult\
1.631 [simp]:\
1.632 -"gcd(k,\
1.633 -k{\isacharasterisk}n)\ =\
1.634 -k"\isanewline
1.635 +"gcd(k,\ k*n)\ =\ k"\isanewline
1.636 \isacommand{apply}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym])\isanewline
1.637 \isacommand{done}
1.638 \end{isabelle}
1.639 @@ -1633,7 +1622,7 @@
1.640 instance of a rule by specifying facts for its premises. Let us try
1.641 it with this rule:
1.642 \begin{isabelle}
1.643 -{\isasymlbrakk}gcd(?k,?n){=}1;\ ?k\ dvd\ (?m * ?n){\isasymrbrakk}\
1.644 +\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ (?m * ?n)\isasymrbrakk\
1.645 \isasymLongrightarrow\ ?k\ dvd\ ?m
1.646 \rulename{relprime_dvd_mult}
1.647 \end{isabelle}
1.648 @@ -1648,24 +1637,23 @@
1.649 simplification. Expression evaluation is not guaranteed to terminate, and
1.650 certainly is not efficient; Isabelle performs arithmetic operations by
1.651 rewriting symbolic bit strings. Here, however, the simplification takes
1.652 -less than one second. We can specify this new lemma to {\isa{OF}},
1.653 +less than one second. We can specify this new lemma to \isa{OF},
1.654 generating an instance of \isa{relprime_dvd_mult}. The expression
1.655 \begin{isabelle}
1.656 \ \ \ \ \ relprime_dvd_mult [OF relprime_20_81]
1.657 \end{isabelle}
1.658 yields the theorem
1.659 \begin{isabelle}
1.660 -\ \ \ \ \ \isacharhash20\ dvd\ (?m\ \isacharasterisk\ \isacharhash81)\ \isasymLongrightarrow\ \isacharhash20\ dvd\ ?m%
1.661 +\ \ \ \ \ \#20\ dvd\ (?m\ *\ \#81)\ \isasymLongrightarrow\ \#20\ dvd\ ?m%
1.662 \end{isabelle}
1.663 %
1.664 -{\isa{OF}} takes any number of operands. Consider
1.665 +\isa{OF} takes any number of operands. Consider
1.666 the following facts about the divides relation:
1.667 \begin{isabelle}
1.668 \isasymlbrakk?k\ dvd\ ?m;\
1.669 ?k\ dvd\ ?n\isasymrbrakk\
1.670 \isasymLongrightarrow\ ?k\ dvd\
1.671 -(?m\ \isacharplus\
1.672 -?n)
1.673 +(?m\ +\ ?n)
1.674 \rulename{dvd_add}\isanewline
1.675 ?m\ dvd\ ?m%
1.676 \rulename{dvd_refl}
1.677 @@ -1676,7 +1664,7 @@
1.678 \end{isabelle}
1.679 Here is the theorem that we have expressed:
1.680 \begin{isabelle}
1.681 -\ \ \ \ \ ?k\ dvd\ (?k\ \isacharplus\ ?k)
1.682 +\ \ \ \ \ ?k\ dvd\ (?k\ +\ ?k)
1.683 \end{isabelle}
1.684 As with \isa{of}, we can use the \isa{_} symbol to leave some positions
1.685 unspecified:
1.686 @@ -1685,10 +1673,10 @@
1.687 \end{isabelle}
1.688 The result is
1.689 \begin{isabelle}
1.690 -\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ \isacharplus\ ?k)
1.691 +\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ +\ ?k)
1.692 \end{isabelle}
1.693
1.694 -You may have noticed that {\isa{THEN}} and {\isa{OF}} are based on
1.695 +You may have noticed that \isa{THEN} and \isa{OF} are based on
1.696 the same idea, namely to combine two rules. They differ in the
1.697 order of the combination and thus in their effect. We use \isa{THEN}
1.698 typically with a destruction rule to extract a subformula of the current
1.699 @@ -1698,9 +1686,9 @@
1.700
1.701 Here is a summary of the primitives for forward reasoning:
1.702 \begin{itemize}
1.703 -\item {\isa{of}} instantiates the variables of a rule to a list of terms
1.704 -\item {\isa{OF}} applies a rule to a list of theorems
1.705 -\item {\isa{THEN}} gives a theorem to a named rule and returns the
1.706 +\item \isa{of} instantiates the variables of a rule to a list of terms
1.707 +\item \isa{OF} applies a rule to a list of theorems
1.708 +\item \isa{THEN} gives a theorem to a named rule and returns the
1.709 conclusion
1.710 \end{itemize}
1.711
1.712 @@ -1711,7 +1699,7 @@
1.713 proof. Also in that spirit is the \isa{insert} method, which inserts a
1.714 given theorem as a new assumption of the current subgoal. This already
1.715 is a forward step; moreover, we may (as always when using a theorem) apply
1.716 -{\isa{of}}, {\isa{THEN}} and other directives. The new assumption can then
1.717 +\isa{of}, \isa{THEN} and other directives. The new assumption can then
1.718 be used to help prove the subgoal.
1.719
1.720 For example, consider this theorem about the divides relation.
1.721 @@ -1720,9 +1708,9 @@
1.722 \begin{isabelle}
1.723 \isacommand{lemma}\
1.724 relprime_dvd_mult:\isanewline
1.725 -\ \ \ \ \ \ \ "{\isasymlbrakk}\ gcd(k,n){=}1;\
1.726 +\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\
1.727 k\ dvd\ (m*n)\
1.728 -{\isasymrbrakk}\
1.729 +\isasymrbrakk\
1.730 \isasymLongrightarrow\ k\ dvd\
1.731 m"\isanewline
1.732 \isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\
1.733 @@ -1731,31 +1719,25 @@
1.734 In the resulting subgoal, note how the equation has been
1.735 inserted:
1.736 \begin{isabelle}
1.737 -{\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\
1.738 -dvd\ (m\ \isacharasterisk\
1.739 -n){\isasymrbrakk}\ \isasymLongrightarrow\ k\ dvd\
1.740 +\isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\
1.741 +dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
1.742 m\isanewline
1.743 -\ 1.\ {\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ \isacharasterisk\ n){;}\isanewline
1.744 -\ \ \ \ \ m\ \isacharasterisk\ gcd\
1.745 +\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
1.746 +\ \ \ \ \ m\ *\ gcd\
1.747 (k,\ n)\
1.748 -=\ gcd\ (m\ \isacharasterisk\
1.749 -k,\ m\ \isacharasterisk\
1.750 -n){\isasymrbrakk}\isanewline
1.751 +=\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
1.752 \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
1.753 \end{isabelle}
1.754 The next proof step, \isa{\isacommand{apply}(simp)},
1.755 utilizes the assumption \isa{gcd(k,n)\ =\
1.756 1}. Here is the result:
1.757 \begin{isabelle}
1.758 -{\isasymlbrakk}gcd\ (k,\
1.759 +\isasymlbrakk gcd\ (k,\
1.760 n)\ =\ 1;\ k\
1.761 -dvd\ (m\ \isacharasterisk\
1.762 -n){\isasymrbrakk}\ \isasymLongrightarrow\ k\ dvd\
1.763 +dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
1.764 m\isanewline
1.765 -\ 1.\ {\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ \isacharasterisk\ n){;}\isanewline
1.766 -\ \ \ \ \ m\ =\ gcd\ (m\
1.767 -\isacharasterisk\ k,\ m\ \isacharasterisk\
1.768 -n){\isasymrbrakk}\isanewline
1.769 +\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
1.770 +\ \ \ \ \ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
1.771 \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
1.772 \end{isabelle}
1.773 Simplification has yielded an equation for \isa{m} that will be used to
1.774 @@ -1765,17 +1747,16 @@
1.775 Here is another proof using \isa{insert}. \REMARK{Effect with unknowns?}
1.776 Division and remainder obey a well-known law:
1.777 \begin{isabelle}
1.778 -(?m\ div\ ?n)\ \isacharasterisk\
1.779 -?n\ \isacharplus\ ?m\ mod\ ?n\
1.780 -=\ ?m
1.781 +(?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m
1.782 \rulename{mod_div_equality}
1.783 \end{isabelle}
1.784
1.785 We refer to this law explicitly in the following proof:
1.786 \begin{isabelle}
1.787 \isacommand{lemma}\ div_mult_self_is_m:\ \isanewline
1.788 -\ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m{\isacharasterisk}n)\ div\ n\ =\ (m::nat)"\isanewline
1.789 -\isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m{\isacharasterisk}n"\ n])\isanewline
1.790 +\ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m*n)\ div\ n\ =\
1.791 +(m::nat)"\isanewline
1.792 +\isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m*n"\ n])\isanewline
1.793 \isacommand{apply}\ (simp)\isanewline
1.794 \isacommand{done}
1.795 \end{isabelle}
1.796 @@ -1785,20 +1766,19 @@
1.797 subgoal, with its new assumption:
1.798 \begin{isabelle}
1.799 %0\ \isacharless\ n\ \isasymLongrightarrow\ (m\
1.800 -%\isacharasterisk\ n)\ div\ n\ =\ m\isanewline
1.801 +%*\ n)\ div\ n\ =\ m\isanewline
1.802 \ 1.\ \isasymlbrakk0\ \isacharless\
1.803 -n;\ \ (m\ \isacharasterisk\ n)\ div\ n\
1.804 -\isacharasterisk\ n\ \isacharplus\ (m\ \isacharasterisk\ n)\ mod\ n\
1.805 -=\ m\ \isacharasterisk\ n\isasymrbrakk\isanewline
1.806 -\ \ \ \ \isasymLongrightarrow\ (m\ \isacharasterisk\ n)\ div\ n\
1.807 +n;\ \ (m\ *\ n)\ div\ n\ *\ n\ +\ (m\ *\ n)\ mod\ n\
1.808 +=\ m\ *\ n\isasymrbrakk\isanewline
1.809 +\ \ \ \ \isasymLongrightarrow\ (m\ *\ n)\ div\ n\
1.810 =\ m
1.811 \end{isabelle}
1.812 -Simplification reduces \isa{(m\ \isacharasterisk\ n)\ mod\ n} to zero.
1.813 +Simplification reduces \isa{(m\ *\ n)\ mod\ n} to zero.
1.814 Then it cancels the factor~\isa{n} on both
1.815 sides of the equation, proving the theorem.
1.816
1.817 \medskip
1.818 -A similar method is {\isa{subgoal\_tac}}. Instead of inserting
1.819 +A similar method is {\isa{subgoal_tac}}. Instead of inserting
1.820 a theorem as an assumption, it inserts an arbitrary formula.
1.821 This formula must be proved later as a separate subgoal. The
1.822 idea is to claim that the formula holds on the basis of the current
1.823 @@ -1830,25 +1810,25 @@
1.824 step is to claim that \isa{z} is either 34 or 36. The resulting proof
1.825 state gives us two subgoals:
1.826 \begin{isabelle}
1.827 -%{\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\
1.828 +%\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\
1.829 %Q\ \#34;\ Q\ \#36\isasymrbrakk\ \isasymLongrightarrow\ Q\ z\isanewline
1.830 -\ 1.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
1.831 +\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
1.832 \ \ \ \ \ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isasymrbrakk\isanewline
1.833 \ \ \ \ \isasymLongrightarrow\ Q\ z\isanewline
1.834 -\ 2.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
1.835 +\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
1.836 \ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36
1.837 \end{isabelle}
1.838
1.839 The first subgoal is trivial, but for the second Isabelle needs help to eliminate
1.840 the case
1.841 -\isa{z}=35. The second invocation of {\isa{subgoal\_tac}} leaves two
1.842 +\isa{z}=35. The second invocation of {\isa{subgoal_tac}} leaves two
1.843 subgoals:
1.844 \begin{isabelle}
1.845 -\ 1.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\
1.846 +\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\
1.847 \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
1.848 \ \ \ \ \ z\ \isasymnoteq\ \#35\isasymrbrakk\isanewline
1.849 \ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isanewline
1.850 -\ 2.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
1.851 +\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
1.852 \ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35
1.853 \end{isabelle}
1.854