2 \chapter{The Rules of the Game}
5 This chapter outlines the concepts and techniques that underlie reasoning
6 in Isabelle. Until now, we have proved everything using only induction and
7 simplification, but any serious verification project requires more elaborate
8 forms of inference. The chapter also introduces the fundamentals of
9 predicate logic. The first examples in this chapter will consist of
10 detailed, low-level proof steps. Later, we shall see how to automate such
11 reasoning using the methods
13 \isa{auto} and others. Backward or goal-directed proof is our usual style,
14 but the chapter also introduces forward reasoning, where one theorem is
15 transformed to yield another.
17 \section{Natural Deduction}
19 \index{natural deduction|(}%
20 In Isabelle, proofs are constructed using inference rules. The
21 most familiar inference rule is probably \emph{modus ponens}:%
22 \index{modus ponens@\emph{modus ponens}}
23 \[ \infer{Q}{P\imp Q & P} \]
24 This rule says that from $P\imp Q$ and $P$ we may infer~$Q$.
26 \textbf{Natural deduction} is an attempt to formalize logic in a way
27 that mirrors human reasoning patterns.
28 For each logical symbol (say, $\conj$), there
29 are two kinds of rules: \textbf{introduction} and \textbf{elimination} rules.
30 The introduction rules allow us to infer this symbol (say, to
31 infer conjunctions). The elimination rules allow us to deduce
32 consequences from this symbol. Ideally each rule should mention
33 one symbol only. For predicate logic this can be
34 done, but when users define their own concepts they typically
35 have to refer to other symbols as well. It is best not to be dogmatic.
36 Our system is not based on pure natural deduction, but includes elements from the sequent calculus
37 and free-variable tableaux.
39 Natural deduction generally deserves its name. It is easy to use. Each
40 proof step consists of identifying the outermost symbol of a formula and
41 applying the corresponding rule. It creates new subgoals in
42 an obvious way from parts of the chosen formula. Expanding the
43 definitions of constants can blow up the goal enormously. Deriving natural
44 deduction rules for such constants lets us reason in terms of their key
45 properties, which might otherwise be obscured by the technicalities of its
46 definition. Natural deduction rules also lend themselves to automation.
48 \textbf{classical reasoner} accepts any suitable collection of natural deduction
49 rules and uses them to search for proofs automatically. Isabelle is designed around
50 natural deduction and many of its tools use the terminology of introduction
51 and elimination rules.%
52 \index{natural deduction|)}
55 \section{Introduction Rules}
57 \index{introduction rules|(}%
58 An introduction rule tells us when we can infer a formula
59 containing a specific logical symbol. For example, the conjunction
60 introduction rule says that if we have $P$ and if we have $Q$ then
61 we have $P\conj Q$. In a mathematics text, it is typically shown
63 \[ \infer{P\conj Q}{P & Q} \]
64 The rule introduces the conjunction
65 symbol~($\conj$) in its conclusion. In Isabelle proofs we
66 mainly reason backwards. When we apply this rule, the subgoal already has
67 the form of a conjunction; the proof step makes this conjunction symbol
70 In Isabelle notation, the rule looks like this:
72 \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulenamedx{conjI}
74 Carefully examine the syntax. The premises appear to the
75 left of the arrow and the conclusion to the right. The premises (if
76 more than one) are grouped using the fat brackets. The question marks
77 indicate \textbf{schematic variables} (also called
78 \textbf{unknowns}):\index{unknowns|bold} they may
79 be replaced by arbitrary formulas. If we use the rule backwards, Isabelle
80 tries to unify the current subgoal with the conclusion of the rule, which
81 has the form \isa{?P\ \isasymand\ ?Q}. (Unification is discussed below,
82 {\S}\ref{sec:unification}.) If successful,
83 it yields new subgoals given by the formulas assigned to
84 \isa{?P} and \isa{?Q}.
86 The following trivial proof illustrates how rules work. It also introduces a
87 style of indentation. If a command adds a new subgoal, then the next
88 command's indentation is increased by one space; if it proves a subgoal, then
89 the indentation is reduced. This provides the reader with hints about the
92 \isacommand{lemma}\ conj_rule:\ "\isasymlbrakk P;\
93 Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\
94 (Q\ \isasymand\ P)"\isanewline
95 \isacommand{apply}\ (rule\ conjI)\isanewline
96 \ \isacommand{apply}\ assumption\isanewline
97 \isacommand{apply}\ (rule\ conjI)\isanewline
98 \ \isacommand{apply}\ assumption\isanewline
99 \isacommand{apply}\ assumption
101 At the start, Isabelle presents
102 us with the assumptions (\isa{P} and~\isa{Q}) and with the goal to be proved,
104 (Q\ \isasymand\ P)}. We are working backwards, so when we
105 apply conjunction introduction, the rule removes the outermost occurrence
106 of the \isa{\isasymand} symbol. To apply a rule to a subgoal, we apply
107 the proof method \isa{rule} --- here with \isa{conjI}, the conjunction
110 %\isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\
111 %\isasymand\ P\isanewline
112 \ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
113 \ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P
115 Isabelle leaves two new subgoals: the two halves of the original conjunction.
116 The first is simply \isa{P}, which is trivial, since \isa{P} is among
117 the assumptions. We can apply the \methdx{assumption}
118 method, which proves a subgoal by finding a matching assumption.
120 \ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\
123 We are left with the subgoal of proving
124 \isa{Q\ \isasymand\ P} from the assumptions \isa{P} and~\isa{Q}. We apply
125 \isa{rule conjI} again.
127 \ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline
128 \ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P
130 We are left with two new subgoals, \isa{Q} and~\isa{P}, each of which can be proved
131 using the \isa{assumption} method.%
132 \index{introduction rules|)}
135 \section{Elimination Rules}
137 \index{elimination rules|(}%
138 Elimination rules work in the opposite direction from introduction
139 rules. In the case of conjunction, there are two such rules.
140 From $P\conj Q$ we infer $P$. also, from $P\conj Q$
142 \[ \infer{P}{P\conj Q} \qquad \infer{Q}{P\conj Q} \]
144 Now consider disjunction. There are two introduction rules, which resemble inverted forms of the
145 conjunction elimination rules:
146 \[ \infer{P\disj Q}{P} \qquad \infer{P\disj Q}{Q} \]
148 What is the disjunction elimination rule? The situation is rather different from
149 conjunction. From $P\disj Q$ we cannot conclude that $P$ is true and we
150 cannot conclude that $Q$ is true; there are no direct
151 elimination rules of the sort that we have seen for conjunction. Instead,
152 there is an elimination rule that works indirectly. If we are trying to prove
153 something else, say $R$, and we know that $P\disj Q$ holds, then we have to consider
154 two cases. We can assume that $P$ is true and prove $R$ and then assume that $Q$ is
155 true and prove $R$ a second time. Here we see a fundamental concept used in natural
156 deduction: that of the \textbf{assumptions}. We have to prove $R$ twice, under
157 different assumptions. The assumptions are local to these subproofs and are visible
160 In a logic text, the disjunction elimination rule might be shown
162 \[ \infer{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}} \]
163 The assumptions $[P]$ and $[Q]$ are bracketed
164 to emphasize that they are local to their subproofs. In Isabelle
165 notation, the already-familiar \isa{\isasymLongrightarrow} syntax serves the
168 \isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{disjE}
170 When we use this sort of elimination rule backwards, it produces
171 a case split. (We have seen this before, in proofs by induction.) The following proof
172 illustrates the use of disjunction elimination.
174 \isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\
175 \isasymLongrightarrow\ Q\ \isasymor\ P"\isanewline
176 \isacommand{apply}\ (erule\ disjE)\isanewline
177 \ \isacommand{apply}\ (rule\ disjI2)\isanewline
178 \ \isacommand{apply}\ assumption\isanewline
179 \isacommand{apply}\ (rule\ disjI1)\isanewline
180 \isacommand{apply}\ assumption
182 We assume \isa{P\ \isasymor\ Q} and
183 must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction
184 elimination rule, \isa{disjE}\@. We invoke it using \methdx{erule}, a
185 method designed to work with elimination rules. It looks for an assumption that
186 matches the rule's first premise. It deletes the matching assumption,
187 regards the first premise as proved and returns subgoals corresponding to
188 the remaining premises. When we apply \isa{erule} to \isa{disjE}, only two
189 subgoals result. This is better than applying it using \isa{rule}
190 to get three subgoals, then proving the first by assumption: the other
191 subgoals would have the redundant assumption
192 \hbox{\isa{P\ \isasymor\ Q}}.
193 Most of the time, \isa{erule} is the best way to use elimination rules, since it
194 replaces an assumption by its subformulas; only rarely does the original
195 assumption remain useful.
198 %P\ \isasymor\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline
199 \ 1.\ P\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline
200 \ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
202 These are the two subgoals returned by \isa{erule}. The first assumes
203 \isa{P} and the second assumes \isa{Q}. Tackling the first subgoal, we
204 need to show \isa{Q\ \isasymor\ P}\@. The second introduction rule
205 (\isa{disjI2}) can reduce this to \isa{P}, which matches the assumption.
207 \isa{rule} method with \isa{disjI2} \ldots
209 \ 1.\ P\ \isasymLongrightarrow\ P\isanewline
210 \ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
212 \ldots and finish off with the \isa{assumption}
213 method. We are left with the other subgoal, which
216 \ 1.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
218 Its proof is similar, using the introduction
221 The result of this proof is a new inference rule \isa{disj_swap}, which is neither
222 an introduction nor an elimination rule, but which might
223 be useful. We can use it to replace any goal of the form $Q\disj P$
224 by one of the form $P\disj Q$.%
225 \index{elimination rules|)}
228 \section{Destruction Rules: Some Examples}
230 \index{destruction rules|(}%
231 Now let us examine the analogous proof for conjunction.
233 \isacommand{lemma}\ conj_swap:\ "P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P"\isanewline
234 \isacommand{apply}\ (rule\ conjI)\isanewline
235 \ \isacommand{apply}\ (drule\ conjunct2)\isanewline
236 \ \isacommand{apply}\ assumption\isanewline
237 \isacommand{apply}\ (drule\ conjunct1)\isanewline
238 \isacommand{apply}\ assumption
240 Recall that the conjunction elimination rules --- whose Isabelle names are
241 \isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half
242 of a conjunction. Rules of this sort (where the conclusion is a subformula of a
243 premise) are called \textbf{destruction} rules because they take apart and destroy
245 \footnote{This Isabelle terminology is not used in standard logic texts,
246 although the distinction between the two forms of elimination rule is well known.
247 Girard \cite[page 74]{girard89},\index{Girard, Jean-Yves|fnote}
248 for example, writes ``The elimination rules
249 [for $\disj$ and $\exists$] are very
250 bad. What is catastrophic about them is the parasitic presence of a formula [$R$]
251 which has no structural link with the formula which is eliminated.''
252 These Isabelle rules are inspired by the sequent calculus.}
254 The first proof step applies conjunction introduction, leaving
257 %P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P\isanewline
258 \ 1.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\isanewline
259 \ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P
262 To invoke the elimination rule, we apply a new method, \isa{drule}.
263 Think of the \isa{d} as standing for \textbf{destruction} (or \textbf{direct}, if
264 you prefer). Applying the
265 second conjunction rule using \isa{drule} replaces the assumption
266 \isa{P\ \isasymand\ Q} by \isa{Q}.
268 \ 1.\ Q\ \isasymLongrightarrow\ Q\isanewline
269 \ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P
271 The resulting subgoal can be proved by applying \isa{assumption}.
272 The other subgoal is similarly proved, using the \isa{conjunct1} rule and the
273 \isa{assumption} method.
275 Choosing among the methods \isa{rule}, \isa{erule} and \isa{drule} is up to
276 you. Isabelle does not attempt to work out whether a rule
277 is an introduction rule or an elimination rule. The
278 method determines how the rule will be interpreted. Many rules
279 can be used in more than one way. For example, \isa{disj_swap} can
280 be applied to assumptions as well as to goals; it replaces any
281 assumption of the form
282 $P\disj Q$ by a one of the form $Q\disj P$.
284 Destruction rules are simpler in form than indirect rules such as \isa{disjE},
285 but they can be inconvenient. Each of the conjunction rules discards half
286 of the formula, when usually we want to take both parts of the conjunction as new
287 assumptions. The easiest way to do so is by using an
288 alternative conjunction elimination rule that resembles \isa{disjE}\@. It is
289 seldom, if ever, seen in logic books. In Isabelle syntax it looks like this:
291 \isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{conjE}
293 \index{destruction rules|)}
296 Use the rule \isa{conjE} to shorten the proof above.
300 \section{Implication}
302 \index{implication|(}%
303 At the start of this chapter, we saw the rule \emph{modus ponens}. It is, in fact,
304 a destruction rule. The matching introduction rule looks like this
307 (?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\
308 \isasymlongrightarrow\ ?Q\rulenamedx{impI}
310 And this is \emph{modus ponens}\index{modus ponens@\emph{modus ponens}}:
312 \isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\
313 \isasymLongrightarrow\ ?Q
317 Here is a proof using the implication rules. This
318 lemma performs a sort of uncurrying, replacing the two antecedents
319 of a nested implication by a conjunction. The proof illustrates
320 how assumptions work. At each proof step, the subgoals inherit the previous
321 assumptions, perhaps with additions or deletions. Rules such as
322 \isa{impI} and \isa{disjE} add assumptions, while applying \isa{erule} or
323 \isa{drule} deletes the matching assumption.
325 \isacommand{lemma}\ imp_uncurry:\
326 "P\ \isasymlongrightarrow\ (Q\
327 \isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\
328 \isasymand\ Q\ \isasymlongrightarrow\
330 \isacommand{apply}\ (rule\ impI)\isanewline
331 \isacommand{apply}\ (erule\ conjE)\isanewline
332 \isacommand{apply}\ (drule\ mp)\isanewline
333 \ \isacommand{apply}\ assumption\isanewline
334 \isacommand{apply}\ (drule\ mp)\isanewline
335 \ \ \isacommand{apply}\ assumption\isanewline
336 \ \isacommand{apply}\ assumption
338 First, we state the lemma and apply implication introduction (\isa{rule impI}),
339 which moves the conjunction to the assumptions.
341 %P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R\ \isasymLongrightarrow\ P\
342 %\isasymand\ Q\ \isasymlongrightarrow\ R\isanewline
343 \ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R
345 Next, we apply conjunction elimination (\isa{erule conjE}), which splits this
346 conjunction into two parts.
348 \ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\
349 Q\isasymrbrakk\ \isasymLongrightarrow\ R
351 Now, we work on the assumption \isa{P\ \isasymlongrightarrow\ (Q\
352 \isasymlongrightarrow\ R)}, where the parentheses have been inserted for
353 clarity. The nested implication requires two applications of
354 \textit{modus ponens}: \isa{drule mp}. The first use yields the
356 \isasymlongrightarrow\ R}, but first we must prove the extra subgoal
357 \isa{P}, which we do by assumption.
359 \ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
360 \ 2.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R
362 Repeating these steps for \isa{Q\
363 \isasymlongrightarrow\ R} yields the conclusion we seek, namely~\isa{R}.
365 \ 1.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\
366 \isasymLongrightarrow\ R
369 The symbols \isa{\isasymLongrightarrow} and \isa{\isasymlongrightarrow}
370 both stand for implication, but they differ in many respects. Isabelle
371 uses \isa{\isasymLongrightarrow} to express inference rules; the symbol is
372 built-in and Isabelle's inference mechanisms treat it specially. On the
373 other hand, \isa{\isasymlongrightarrow} is just one of the many connectives
374 available in higher-order logic. We reason about it using inference rules
375 such as \isa{impI} and \isa{mp}, just as we reason about the other
376 connectives. You will have to use \isa{\isasymlongrightarrow} in any
377 context that requires a formula of higher-order logic. Use
378 \isa{\isasymLongrightarrow} to separate a theorem's preconditions from its
380 \index{implication|)}
383 \index{by@\isacommand{by} (command)|(}%
384 The \isacommand{by} command is useful for proofs like these that use
385 \isa{assumption} heavily. It executes an
386 \isacommand{apply} command, then tries to prove all remaining subgoals using
387 \isa{assumption}. Since (if successful) it ends the proof, it also replaces the
388 \isacommand{done} symbol. For example, the proof above can be shortened:
390 \isacommand{lemma}\ imp_uncurry:\
391 "P\ \isasymlongrightarrow\ (Q\
392 \isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\
393 \isasymand\ Q\ \isasymlongrightarrow\
395 \isacommand{apply}\ (rule\ impI)\isanewline
396 \isacommand{apply}\ (erule\ conjE)\isanewline
397 \isacommand{apply}\ (drule\ mp)\isanewline
398 \ \isacommand{apply}\ assumption\isanewline
399 \isacommand{by}\ (drule\ mp)
401 We could use \isacommand{by} to replace the final \isacommand{apply} and
402 \isacommand{done} in any proof, but typically we use it
403 to eliminate calls to \isa{assumption}. It is also a nice way of expressing a
405 \index{by@\isacommand{by} (command)|)}
412 Negation causes surprising complexity in proofs. Its natural
413 deduction rules are straightforward, but additional rules seem
414 necessary in order to handle negated assumptions gracefully. This section
415 also illustrates the \isa{intro} method: a convenient way of
416 applying introduction rules.
418 Negation introduction deduces $\lnot P$ if assuming $P$ leads to a
419 contradiction. Negation elimination deduces any formula in the
420 presence of $\lnot P$ together with~$P$:
422 (?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P%
423 \rulenamedx{notI}\isanewline
424 \isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R%
428 Classical logic allows us to assume $\lnot P$
429 when attempting to prove~$P$:
431 (\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P%
432 \rulenamedx{classical}
435 \index{contrapositives|(}%
436 The implications $P\imp Q$ and $\lnot Q\imp\lnot P$ are logically
437 equivalent, and each is called the
438 \textbf{contrapositive} of the other. Four further rules support
439 reasoning about contrapositives. They differ in the placement of the
442 \isasymlbrakk?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
443 \rulename{contrapos_pp}\isanewline
444 \isasymlbrakk?Q;\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\
446 \rulename{contrapos_pn}\isanewline
447 \isasymlbrakk{\isasymnot}\ ?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
448 \rulename{contrapos_np}\isanewline
449 \isasymlbrakk{\isasymnot}\ ?Q;\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ \isasymnot\ ?P%
450 \rulename{contrapos_nn}
453 These rules are typically applied using the \isa{erule} method, where
454 their effect is to form a contrapositive from an
455 assumption and the goal's conclusion.%
456 \index{contrapositives|)}
458 The most important of these is \isa{contrapos_np}. It is useful
459 for applying introduction rules to negated assumptions. For instance,
460 the assumption $\lnot(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we
461 might want to use conjunction introduction on it.
462 Before we can do so, we must move that assumption so that it
463 becomes the conclusion. The following proof demonstrates this
466 \isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\
467 \isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\
469 \isacommand{apply}\ (erule_tac\ Q = "R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
470 contrapos_np)\isanewline
471 \isacommand{apply}\ (intro\ impI)\isanewline
472 \isacommand{by}\ (erule\ notE)
475 There are two negated assumptions and we need to exchange the conclusion with the
476 second one. The method \isa{erule contrapos_np} would select the first assumption,
477 which we do not want. So we specify the desired assumption explicitly
478 using a new method, \isa{erule_tac}. This is the resulting subgoal:
480 \ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\
481 R\isasymrbrakk\ \isasymLongrightarrow\ R\ \isasymlongrightarrow\ Q%
483 The former conclusion, namely \isa{R}, now appears negated among the assumptions,
484 while the negated formula \isa{R\ \isasymlongrightarrow\ Q} becomes the new
487 We can now apply introduction rules. We use the \methdx{intro} method, which
488 repeatedly applies the given introduction rules. Here its effect is equivalent
491 \ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ R;\
492 R\isasymrbrakk\ \isasymLongrightarrow\ Q%
494 We can see a contradiction in the form of assumptions \isa{\isasymnot\ R}
495 and~\isa{R}, which suggests using negation elimination. If applied on its own,
496 \isa{notE} will select the first negated assumption, which is useless.
497 Instead, we invoke the rule using the
499 Now when Isabelle selects the first assumption, it tries to prove \isa{P\
500 \isasymlongrightarrow\ Q} and fails; it then backtracks, finds the
501 assumption \isa{\isasymnot~R} and finally proves \isa{R} by assumption. That
506 The following example may be skipped on a first reading. It involves a
507 peculiar but important rule, a form of disjunction introduction:
509 (\isasymnot \ ?Q\ \isasymLongrightarrow \ ?P)\ \isasymLongrightarrow \ ?P\ \isasymor \ ?Q%
512 This rule combines the effects of \isa{disjI1} and \isa{disjI2}. Its great
513 advantage is that we can remove the disjunction symbol without deciding
514 which disjunction to prove. This treatment of disjunction is standard in sequent
518 \isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\
519 \isasymLongrightarrow\ P\ \isasymor\ (Q\ \isasymand\ R)"\isanewline
520 \isacommand{apply}\ (rule\ disjCI)\isanewline
521 \isacommand{apply}\ (elim\ conjE\ disjE)\isanewline
522 \ \isacommand{apply}\ assumption
524 \isacommand{by}\ (erule\ contrapos_np,\ rule\ conjI)
527 The first proof step to applies the introduction rules \isa{disjCI}.
528 The resulting subgoal has the negative assumption
529 \hbox{\isa{\isasymnot(Q\ \isasymand\ R)}}.
532 \ 1.\ \isasymlbrakk(P\ \isasymor\ Q)\ \isasymand\ R;\ \isasymnot\ (Q\ \isasymand\
533 R)\isasymrbrakk\ \isasymLongrightarrow\ P%
535 Next we apply the \isa{elim} method, which repeatedly applies
536 elimination rules; here, the elimination rules given
537 in the command. One of the subgoals is trivial (\isa{\isacommand{apply} assumption}),
538 leaving us with one other:
540 \ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P%
543 Now we must move the formula \isa{Q\ \isasymand\ R} to be the conclusion. The
546 \ \ \ \ \ (erule\ contrapos_np,\ rule\ conjI)
548 is robust: the \isa{conjI} forces the \isa{erule} to select a
549 conjunction. The two subgoals are the ones we would expect from applying
550 conjunction introduction to
551 \isa{Q~\isasymand~R}:
553 \ 1.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\
555 \ 2.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R%
557 They are proved by assumption, which is implicit in the \isacommand{by}
562 \section{Interlude: the Basic Methods for Rules}
564 We have seen examples of many tactics that operate on individual rules. It
565 may be helpful to review how they work given an arbitrary rule such as this:
566 \[ \infer{Q}{P@1 & \ldots & P@n} \]
567 Below, we refer to $P@1$ as the \bfindex{major premise}. This concept
568 applies only to elimination and destruction rules. These rules act upon an
569 instance of their major premise, typically to replace it by subformulas of itself.
571 Suppose that the rule above is called~\isa{R}\@. Here are the basic rule
572 methods, most of which we have already seen:
575 Method \isa{rule\ R} unifies~$Q$ with the current subgoal, replacing it
576 by $n$ new subgoals: instances of $P@1$, \ldots,~$P@n$.
577 This is backward reasoning and is appropriate for introduction rules.
579 Method \isa{erule\ R} unifies~$Q$ with the current subgoal and
580 simultaneously unifies $P@1$ with some assumption. The subgoal is
581 replaced by the $n-1$ new subgoals of proving
583 \ldots,~$P@n$, with the matching assumption deleted. It is appropriate for
584 elimination rules. The method
585 \isa{(rule\ R,\ assumption)} is similar, but it does not delete an
588 Method \isa{drule\ R} unifies $P@1$ with some assumption, which it
589 then deletes. The subgoal is
590 replaced by the $n-1$ new subgoals of proving $P@2$, \ldots,~$P@n$; an
591 $n$th subgoal is like the original one but has an additional assumption: an
592 instance of~$Q$. It is appropriate for destruction rules.
594 Method \isa{frule\ R} is like \isa{drule\ R} except that the matching
595 assumption is not deleted. (See {\S}\ref{sec:frule} below.)
598 Other methods apply a rule while constraining some of its
599 variables. The typical form is
601 \ \ \ \ \ \methdx{rule_tac}\ $v@1$ = $t@1$ \isakeyword{and} \ldots \isakeyword{and}
603 $t@k$ \isakeyword{in} R
605 This method behaves like \isa{rule R}, while instantiating the variables
607 $v@k$ as specified. We similarly have \methdx{erule_tac}, \methdx{drule_tac} and
608 \methdx{frule_tac}. These methods also let us specify which subgoal to
609 operate on. By default it is the first subgoal, as with nearly all
610 methods, but we can specify that rule \isa{R} should be applied to subgoal
613 \ \ \ \ \ rule_tac\ [$i$] R
618 \section{Unification and Substitution}\label{sec:unification}
620 \index{unification|(}%
621 As we have seen, Isabelle rules involve schematic variables, which begin with
622 a question mark and act as
623 placeholders for terms. \textbf{Unification} --- well known to Prolog programmers --- is the act of
624 making two terms identical, possibly replacing their schematic variables by
625 terms. The simplest case is when the two terms are already the same. Next
626 simplest is \textbf{pattern-matching}, which replaces variables in only one of the
628 \isa{rule} method typically matches the rule's conclusion
629 against the current subgoal. The
630 \isa{assumption} method matches the current subgoal's conclusion
631 against each of its assumptions. Unification can instantiate variables in both terms; the \isa{rule} method can do this if the goal
632 itself contains schematic variables. Other occurrences of the variables in
633 the rule or proof state are updated at the same time.
635 Schematic variables in goals represent unknown terms. Given a goal such
636 as $\exists x.\,P$, they let us proceed with a proof. They can be
637 filled in later, sometimes in stages and often automatically.
640 If unification fails when you think it should succeed, try setting the Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$
641 \pgmenu{Trace Unification},
642 which makes Isabelle show the cause of unification failures (in Proof
643 General's \pgmenu{Trace} buffer).
646 For example, suppose we are trying to prove this subgoal by assumption:
648 \ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a)
650 The \isa{assumption} method having failed, we try again with the flag set:
652 \isacommand{apply} assumption
654 In this trivial case, the output clearly shows that \isa{e} clashes with \isa{c}:
660 \textbf{higher-order} unification, which works in the
661 typed $\lambda$-calculus. The procedure requires search and is potentially
662 undecidable. For our purposes, however, the differences from ordinary
663 unification are straightforward. It handles bound variables
664 correctly, avoiding capture. The two terms
665 \isa{{\isasymlambda}x.\ f(x,z)} and \isa{{\isasymlambda}y.\ f(y,z)} are
666 trivially unifiable because they differ only by a bound variable renaming. The two terms \isa{{\isasymlambda}x.\ ?P} and
667 \isa{{\isasymlambda}x.\ t x} are not unifiable; replacing \isa{?P} by
668 \isa{t x} is forbidden because the free occurrence of~\isa{x} would become
669 bound. Unfortunately, even if \isa{trace_unify_fail} is set, Isabelle displays no information about this type of failure.
672 Higher-order unification sometimes must invent
673 $\lambda$-terms to replace function variables,
674 which can lead to a combinatorial explosion. However, Isabelle proofs tend
675 to involve easy cases where there are few possibilities for the
676 $\lambda$-term being constructed. In the easiest case, the
677 function variable is applied only to bound variables,
678 as when we try to unify \isa{{\isasymlambda}x\ y.\ f(?h x y)} and
679 \isa{{\isasymlambda}x\ y.\ f(x+y+a)}. The only solution is to replace
680 \isa{?h} by \isa{{\isasymlambda}x\ y.\ x+y+a}. Such cases admit at most
681 one unifier, like ordinary unification. A harder case is
682 unifying \isa{?h a} with~\isa{a+b}; it admits two solutions for \isa{?h},
683 namely \isa{{\isasymlambda}x.~a+b} and \isa{{\isasymlambda}x.~x+b}.
684 Unifying \isa{?h a} with~\isa{a+a+b} admits four solutions; their number is
685 exponential in the number of occurrences of~\isa{a} in the second term.
690 \subsection{Substitution and the {\tt\slshape subst} Method}
693 \index{substitution|(}%
694 Isabelle also uses function variables to express \textbf{substitution}.
695 A typical substitution rule allows us to replace one term by
696 another if we know that two terms are equal.
697 \[ \infer{P[t/x]}{s=t & P[s/x]} \]
698 The rule uses a notation for substitution: $P[t/x]$ is the result of
699 replacing $x$ by~$t$ in~$P$. The rule only substitutes in the positions
700 designated by~$x$. For example, it can
701 derive symmetry of equality from reflexivity. Using $x=s$ for~$P$
702 replaces just the first $s$ in $s=s$ by~$t$:
703 \[ \infer{t=s}{s=t & \infer{s=s}{}} \]
705 The Isabelle version of the substitution rule looks like this:
707 \isasymlbrakk?t\ =\ ?s;\ ?P\ ?s\isasymrbrakk\ \isasymLongrightarrow\ ?P\
711 Crucially, \isa{?P} is a function
712 variable. It can be replaced by a $\lambda$-term
713 with one bound variable, whose occurrences identify the places
714 in which $s$ will be replaced by~$t$. The proof above requires \isa{?P}
715 to be replaced by \isa{{\isasymlambda}x.~x=s}; the second premise will then
716 be \isa{s=s} and the conclusion will be \isa{t=s}.
718 The \isa{simp} method also replaces equals by equals, but the substitution
719 rule gives us more control. Consider this proof:
722 "\isasymlbrakk x\ =\ f\ x;\ odd(f\ x)\isasymrbrakk\ \isasymLongrightarrow\
724 \isacommand{by}\ (erule\ ssubst)
727 The assumption \isa{x\ =\ f\ x}, if used for rewriting, would loop,
728 replacing \isa{x} by \isa{f x} and then by
729 \isa{f(f x)} and so forth. (Here \isa{simp}
730 would see the danger and would re-orient the equality, but in more complicated
731 cases it can be fooled.) When we apply the substitution rule,
732 Isabelle replaces every
733 \isa{x} in the subgoal by \isa{f x} just once. It cannot loop. The
734 resulting subgoal is trivial by assumption, so the \isacommand{by} command
735 proves it implicitly.
737 We are using the \isa{erule} method in a novel way. Hitherto,
738 the conclusion of the rule was just a variable such as~\isa{?R}, but it may
739 be any term. The conclusion is unified with the subgoal just as
740 it would be with the \isa{rule} method. At the same time \isa{erule} looks
741 for an assumption that matches the rule's first premise, as usual. With
742 \isa{ssubst} the effect is to find, use and delete an equality
745 The \methdx{subst} method performs individual substitutions. In simple cases,
746 it closely resembles a use of the substitution rule. Suppose a
747 proof has reached this point:
749 \ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \ \isasymLongrightarrow \ f\ z\ =\ x\ *\ y%
751 Now we wish to apply a commutative law:
753 ?m\ *\ ?n\ =\ ?n\ *\ ?m%
754 \rulename{mult_commute}
756 Isabelle rejects our first attempt:
758 apply (simp add: mult_commute)
760 The simplifier notices the danger of looping and refuses to apply the
762 \footnote{More precisely, it only applies such a rule if the new term is
763 smaller under a specified ordering; here, \isa{x\ *\ y}
764 is already smaller than
767 The \isa{subst} method applies \isa{mult_commute} exactly once.
769 \isacommand{apply}\ (subst\ mult_commute)\isanewline
770 \ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \
771 \isasymLongrightarrow \ f\ z\ =\ y\ *\ x%
773 As we wanted, \isa{x\ *\ y} has become \isa{y\ *\ x}.
776 This use of the \methdx{subst} method has the same effect as the command
778 \isacommand{apply}\ (rule\ mult_commute [THEN ssubst])
780 The attribute \isa{THEN}, which combines two rules, is described in
781 {\S}\ref{sec:THEN} below. The \methdx{subst} method is more powerful than
782 applying the substitution rule. It can perform substitutions in a subgoal's
783 assumptions. Moreover, if the subgoal contains more than one occurrence of
784 the left-hand side of the equality, the \methdx{subst} method lets us specify which occurrence should be replaced.
787 \subsection{Unification and Its Pitfalls}
789 Higher-order unification can be tricky. Here is an example, which you may
790 want to skip on your first reading:
792 \isacommand{lemma}\ "\isasymlbrakk x\ =\
793 f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\
794 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
795 \isacommand{apply}\ (erule\ ssubst)\isanewline
796 \isacommand{back}\isanewline
797 \isacommand{back}\isanewline
798 \isacommand{back}\isanewline
799 \isacommand{back}\isanewline
800 \isacommand{apply}\ assumption\isanewline
804 By default, Isabelle tries to substitute for all the
805 occurrences. Applying \isa{erule\ ssubst} yields this subgoal:
807 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ (f\ x)
809 The substitution should have been done in the first two occurrences
810 of~\isa{x} only. Isabelle has gone too far. The \commdx{back}
811 command allows us to reject this possibility and demand a new one:
813 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ (f\ x)\ (f\ x)
816 Now Isabelle has left the first occurrence of~\isa{x} alone. That is
817 promising but it is not the desired combination. So we use \isacommand{back}
820 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ x\ (f\ x)
823 This also is wrong, so we use \isacommand{back} again:
825 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ x\ (f\ x)
828 And this one is wrong too. Looking carefully at the series
829 of alternatives, we see a binary countdown with reversed bits: 111,
830 011, 101, 001. Invoke \isacommand{back} again:
832 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ x%
834 At last, we have the right combination! This goal follows by assumption.%
835 \index{unification|)}
838 This example shows that unification can do strange things with
839 function variables. We were forced to select the right unifier using the
840 \isacommand{back} command. That is all right during exploration, but \isacommand{back}
841 should never appear in the final version of a proof. You can eliminate the
842 need for \isacommand{back} by giving Isabelle less freedom when you apply a rule.
844 One way to constrain the inference is by joining two methods in a
845 \isacommand{apply} command. Isabelle applies the first method and then the
846 second. If the second method fails then Isabelle automatically backtracks.
847 This process continues until the first method produces an output that the
848 second method can use. We get a one-line proof of our example:
850 \isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\
851 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
852 \isacommand{apply}\ (erule\ ssubst,\ assumption)\isanewline
857 The \isacommand{by} command works too, since it backtracks when
858 proving subgoals by assumption:
860 \isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\
861 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
862 \isacommand{by}\ (erule\ ssubst)
866 The most general way to constrain unification is
867 by instantiating variables in the rule. The method \isa{rule_tac} is
868 similar to \isa{rule}, but it
869 makes some of the rule's variables denote specified terms.
870 Also available are {\isa{drule_tac}} and \isa{erule_tac}. Here we need
871 \isa{erule_tac} since above we used \isa{erule}.
873 \isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
874 \isacommand{by}\ (erule_tac\ P = "\isasymlambda u.\ triple\ u\ u\ x"\
875 \isakeyword{in}\ ssubst)
878 To specify a desired substitution
879 requires instantiating the variable \isa{?P} with a $\lambda$-expression.
880 The bound variable occurrences in \isa{{\isasymlambda}u.\ P\ u\
881 u\ x} indicate that the first two arguments have to be substituted, leaving
882 the third unchanged. With this instantiation, backtracking is neither necessary
885 An alternative to \isa{rule_tac} is to use \isa{rule} with a theorem
886 modified using~\isa{of}, described in
887 {\S}\ref{sec:forward} below. But \isa{rule_tac}, unlike \isa{of}, can
888 express instantiations that refer to
889 \isasymAnd-bound variables in the current subgoal.%
890 \index{substitution|)}
893 \section{Quantifiers}
895 \index{quantifiers!universal|(}%
896 Quantifiers require formalizing syntactic substitution and the notion of
897 arbitrary value. Consider the universal quantifier. In a logic
898 book, its introduction rule looks like this:
899 \[ \infer{\forall x.\,P}{P} \]
900 Typically, a proviso written in English says that $x$ must not
901 occur in the assumptions. This proviso guarantees that $x$ can be regarded as
902 arbitrary, since it has not been assumed to satisfy any special conditions.
903 Isabelle's underlying formalism, called the
904 \bfindex{meta-logic}, eliminates the need for English. It provides its own
905 universal quantifier (\isasymAnd) to express the notion of an arbitrary value.
906 We have already seen another operator of the meta-logic, namely
907 \isa\isasymLongrightarrow, which expresses inference rules and the treatment
908 of assumptions. The only other operator in the meta-logic is \isa\isasymequiv,
909 which can be used to define constants.
911 \subsection{The Universal Introduction Rule}
913 Returning to the universal quantifier, we find that having a similar quantifier
914 as part of the meta-logic makes the introduction rule trivial to express:
916 (\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulenamedx{allI}
920 The following trivial proof demonstrates how the universal introduction
923 \isacommand{lemma}\ "{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x"\isanewline
924 \isacommand{apply}\ (rule\ allI)\isanewline
925 \isacommand{by}\ (rule\ impI)
927 The first step invokes the rule by applying the method \isa{rule allI}.
929 \ 1.\ \isasymAnd x.\ P\ x\ \isasymlongrightarrow\ P\ x
931 Note that the resulting proof state has a bound variable,
932 namely~\isa{x}. The rule has replaced the universal quantifier of
933 higher-order logic by Isabelle's meta-level quantifier. Our goal is to
935 \isa{P\ x\ \isasymlongrightarrow\ P\ x} for arbitrary~\isa{x}; it is
936 an implication, so we apply the corresponding introduction rule (\isa{impI}).
938 \ 1.\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow\ P\ x
940 This last subgoal is implicitly proved by assumption.
942 \subsection{The Universal Elimination Rule}
944 Now consider universal elimination. In a logic text,
945 the rule looks like this:
946 \[ \infer{P[t/x]}{\forall x.\,P} \]
947 The conclusion is $P$ with $t$ substituted for the variable~$x$.
948 Isabelle expresses substitution using a function variable:
950 {\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulenamedx{spec}
952 This destruction rule takes a
953 universally quantified formula and removes the quantifier, replacing
954 the bound variable \isa{x} by the schematic variable \isa{?x}. Recall that a
955 schematic variable starts with a question mark and acts as a
956 placeholder: it can be replaced by any term.
958 The universal elimination rule is also
959 available in the standard elimination format. Like \isa{conjE}, it never
960 appears in logic books:
962 \isasymlbrakk \isasymforall x.\ ?P\ x;\ ?P\ ?x\ \isasymLongrightarrow \ ?R\isasymrbrakk \ \isasymLongrightarrow \ ?R%
965 The methods \isa{drule~spec} and \isa{erule~allE} do precisely the
968 To see how $\forall$-elimination works, let us derive a rule about reducing
969 the scope of a universal quantifier. In mathematical notation we write
970 \[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \]
971 with the proviso ``$x$ not free in~$P$.'' Isabelle's treatment of
972 substitution makes the proviso unnecessary. The conclusion is expressed as
974 \isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the
975 variable \isa{P} can introduce a dependence upon~\isa{x}: that would be a
976 bound variable capture. Let us walk through the proof.
978 \isacommand{lemma}\ "(\isasymforall x.\ P\ \isasymlongrightarrow \ Q\ x)\
979 \isasymLongrightarrow \ P\ \isasymlongrightarrow \ (\isasymforall x.\ Q\
982 First we apply implies introduction (\isa{impI}),
983 which moves the \isa{P} from the conclusion to the assumptions. Then
984 we apply universal introduction (\isa{allI}).
986 \isacommand{apply}\ (rule\ impI,\ rule\ allI)\isanewline
987 \ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\
988 x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x
990 As before, it replaces the HOL
991 quantifier by a meta-level quantifier, producing a subgoal that
992 binds the variable~\isa{x}. The leading bound variables
993 (here \isa{x}) and the assumptions (here \isa{{\isasymforall}x.\ P\
994 \isasymlongrightarrow\ Q\ x} and \isa{P}) form the \textbf{context} for the
995 conclusion, here \isa{Q\ x}. Subgoals inherit the context,
996 although assumptions can be added or deleted (as we saw
997 earlier), while rules such as \isa{allI} add bound variables.
999 Now, to reason from the universally quantified
1000 assumption, we apply the elimination rule using the \isa{drule}
1001 method. This rule is called \isa{spec} because it specializes a universal formula
1002 to a particular term.
1004 \isacommand{apply}\ (drule\ spec)\isanewline
1005 \ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ P\ \isasymlongrightarrow\ Q\ (?x2\
1006 x)\isasymrbrakk\ \isasymLongrightarrow\ Q\ x
1008 Observe how the context has changed. The quantified formula is gone,
1009 replaced by a new assumption derived from its body. We have
1010 removed the quantifier and replaced the bound variable
1012 \isa{?x2~x}. This term is a placeholder: it may become any term that can be
1013 built from~\isa{x}. (Formally, \isa{?x2} is an unknown of function type, applied
1014 to the argument~\isa{x}.) This new assumption is an implication, so we can use
1015 \emph{modus ponens} on it, which concludes the proof.
1017 \isacommand{by}\ (drule\ mp)
1019 Let us take a closer look at this last step. \emph{Modus ponens} yields
1020 two subgoals: one where we prove the antecedent (in this case \isa{P}) and
1021 one where we may assume the consequent. Both of these subgoals are proved
1023 \isa{assumption} method, which is implicit in the
1024 \isacommand{by} command. Replacing the \isacommand{by} command by
1025 \isa{\isacommand{apply} (drule\ mp, assumption)} would have left one last
1028 \ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ Q\ (?x2\ x)\isasymrbrakk\
1029 \isasymLongrightarrow\ Q\ x
1031 The consequent is \isa{Q} applied to that placeholder. It may be replaced by any
1032 term built from~\isa{x}, and here
1033 it should simply be~\isa{x}. The assumption need not
1034 be identical to the conclusion, provided the two formulas are unifiable.%
1035 \index{quantifiers!universal|)}
1038 \subsection{The Existential Quantifier}
1040 \index{quantifiers!existential|(}%
1041 The concepts just presented also apply
1042 to the existential quantifier, whose introduction rule looks like this in
1045 ?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulenamedx{exI}
1047 If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
1048 P(x)$ is also true. It is a dual of the universal elimination rule, and
1049 logic texts present it using the same notation for substitution.
1052 elimination rule looks like this
1054 \[ \infer{Q}{\exists x.\,P & \infer*{Q}{[P]}} \]
1056 It looks like this in Isabelle:
1058 \isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulenamedx{exE}
1061 Given an existentially quantified theorem and some
1062 formula $Q$ to prove, it creates a new assumption by removing the quantifier. As with
1063 the universal introduction rule, the textbook version imposes a proviso on the
1064 quantified variable, which Isabelle expresses using its meta-logic. It is
1065 enough to have a universal quantifier in the meta-logic; we do not need an existential
1066 quantifier to be built in as well.
1071 \[ \exists x.\, P\conj Q(x)\Imp P\conj(\exists x.\, Q(x)). \]
1072 \emph{Hint}: the proof is similar
1073 to the one just above for the universal quantifier.
1075 \index{quantifiers!existential|)}
1078 \subsection{Renaming a Bound Variable: {\tt\slshape rename_tac}}
1080 \index{assumptions!renaming|(}\index{*rename_tac (method)|(}%
1081 When you apply a rule such as \isa{allI}, the quantified variable
1082 becomes a new bound variable of the new subgoal. Isabelle tries to avoid
1083 changing its name, but sometimes it has to choose a new name in order to
1084 avoid a clash. The result may not be ideal:
1086 \isacommand{lemma}\ "x\ <\ y\ \isasymLongrightarrow \ \isasymforall x\ y.\ P\ x\
1088 \isacommand{apply}\ (intro allI)\isanewline
1089 \ 1.\ \isasymAnd xa\ ya.\ x\ <\ y\ \isasymLongrightarrow \ P\ xa\ (f\ ya)
1092 The names \isa{x} and \isa{y} were already in use, so the new bound variables are
1093 called \isa{xa} and~\isa{ya}. You can rename them by invoking \isa{rename_tac}:
1096 \isacommand{apply}\ (rename_tac\ v\ w)\isanewline
1097 \ 1.\ \isasymAnd v\ w.\ x\ <\ y\ \isasymLongrightarrow \ P\ v\ (f\ w)
1099 Recall that \isa{rule_tac}\index{*rule_tac (method)!and renaming}
1101 theorem with specified terms. These terms may involve the goal's bound
1102 variables, but beware of referring to variables
1103 like~\isa{xa}. A future change to your theories could change the set of names
1104 produced at top level, so that \isa{xa} changes to~\isa{xb} or reverts to~\isa{x}.
1105 It is safer to rename automatically-generated variables before mentioning them.
1107 If the subgoal has more bound variables than there are names given to
1108 \isa{rename_tac}, the rightmost ones are renamed.%
1109 \index{assumptions!renaming|)}\index{*rename_tac (method)|)}
1112 \subsection{Reusing an Assumption: {\tt\slshape frule}}
1115 \index{assumptions!reusing|(}\index{*frule (method)|(}%
1116 Note that \isa{drule spec} removes the universal quantifier and --- as
1117 usual with elimination rules --- discards the original formula. Sometimes, a
1118 universal formula has to be kept so that it can be used again. Then we use a new
1119 method: \isa{frule}. It acts like \isa{drule} but copies rather than replaces
1120 the selected assumption. The \isa{f} is for \emph{forward}.
1122 In this example, going from \isa{P\ a} to \isa{P(h(h~a))}
1123 requires two uses of the quantified assumption, one for each~\isa{h}
1126 \isacommand{lemma}\ "\isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);
1127 \ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P(h\ (h\ a))"
1130 Examine the subgoal left by \isa{frule}:
1132 \isacommand{apply}\ (frule\ spec)\isanewline
1133 \ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);\ P\ a;\ P\ ?x\ \isasymlongrightarrow\ P\ (h\ ?x)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a))
1135 It is what \isa{drule} would have left except that the quantified
1136 assumption is still present. Next we apply \isa{mp} to the
1137 implication and the assumption~\isa{P\ a}:
1139 \isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
1140 \ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);\ P\ a;\ P\ (h\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a))
1143 We have created the assumption \isa{P(h\ a)}, which is progress. To
1144 continue the proof, we apply \isa{spec} again. We shall not need it
1145 again, so we can use
1148 \isacommand{apply}\ (drule\ spec)\isanewline
1149 \ 1.\ \isasymlbrakk P\ a;\ P\ (h\ a);\ P\ ?x2\
1150 \isasymlongrightarrow \ P\ (h\ ?x2)\isasymrbrakk \ \isasymLongrightarrow \
1154 The new assumption bridges the gap between \isa{P(h\ a)} and \isa{P(h(h\ a))}.
1156 \isacommand{by}\ (drule\ mp)
1160 \emph{A final remark}. Replacing this \isacommand{by} command with
1162 \isacommand{apply}\ (drule\ mp,\ assumption)
1164 would not work: it would add a second copy of \isa{P(h~a)} instead
1165 of the desired assumption, \isa{P(h(h~a))}. The \isacommand{by}
1166 command forces Isabelle to backtrack until it finds the correct one.
1167 Alternatively, we could have used the \isacommand{apply} command and bundled the
1168 \isa{drule mp} with \emph{two} calls of \isa{assumption}. Or, of course,
1169 we could have given the entire proof to \isa{auto}.%
1170 \index{assumptions!reusing|)}\index{*frule (method)|)}
1174 \subsection{Instantiating a Quantifier Explicitly}
1175 \index{quantifiers!instantiating}
1177 We can prove a theorem of the form $\exists x.\,P\, x$ by exhibiting a
1178 suitable term~$t$ such that $P\,t$ is true. Dually, we can use an
1179 assumption of the form $\forall x.\,P\, x$ to generate a new assumption $P\,t$ for
1180 a suitable term~$t$. In many cases,
1181 Isabelle makes the correct choice automatically, constructing the term by
1182 unification. In other cases, the required term is not obvious and we must
1183 specify it ourselves. Suitable methods are \isa{rule_tac}, \isa{drule_tac}
1184 and \isa{erule_tac}.
1186 We have seen (just above, {\S}\ref{sec:frule}) a proof of this lemma:
1188 \isacommand{lemma}\ "\isasymlbrakk \isasymforall x.\ P\ x\
1189 \isasymlongrightarrow \ P\ (h\ x);\ P\ a\isasymrbrakk \
1190 \isasymLongrightarrow \ P(h\ (h\ a))"
1192 We had reached this subgoal:
1194 \ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\
1195 x);\ P\ a;\ P\ (h\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a))
1198 The proof requires instantiating the quantified assumption with the
1201 \isacommand{apply}\ (drule_tac\ x\ =\ "h\ a"\ \isakeyword{in}\
1203 \ 1.\ \isasymlbrakk P\ a;\ P\ (h\ a);\ P\ (h\ a)\ \isasymlongrightarrow \
1204 P\ (h\ (h\ a))\isasymrbrakk \ \isasymLongrightarrow \ P\ (h\ (h\ a))
1206 We have forced the desired instantiation.
1209 Existential formulas can be instantiated too. The next example uses the
1210 \textbf{divides} relation\index{divides relation}
1213 ?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
1217 Let us prove that multiplication of natural numbers is monotone with
1218 respect to the divides relation:
1220 \isacommand{lemma}\ mult_dvd_mono:\ "{\isasymlbrakk}i\ dvd\ m;\ j\ dvd\
1221 n\isasymrbrakk\ \isasymLongrightarrow\ i*j\ dvd\ (m*n\ ::\ nat)"\isanewline
1222 \isacommand{apply}\ (simp\ add:\ dvd_def)
1225 Unfolding the definition of divides has left this subgoal:
1227 \ 1.\ \isasymlbrakk \isasymexists k.\ m\ =\ i\ *\ k;\ \isasymexists k.\ n\
1228 =\ j\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\
1232 Next, we eliminate the two existential quantifiers in the assumptions:
1234 \isacommand{apply}\ (erule\ exE)\isanewline
1235 \ 1.\ \isasymAnd k.\ \isasymlbrakk \isasymexists k.\ n\ =\ j\ *\ k;\ m\ =\
1236 i\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\
1239 \isacommand{apply}\ (erule\ exE)
1241 \ 1.\ \isasymAnd k\ ka.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\
1242 ka\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\ =\ i\
1246 The term needed to instantiate the remaining quantifier is~\isa{k*ka}. But
1247 \isa{ka} is an automatically-generated name. As noted above, references to
1248 such variable names makes a proof less resilient to future changes. So,
1249 first we rename the most recent variable to~\isa{l}:
1251 \isacommand{apply}\ (rename_tac\ l)\isanewline
1252 \ 1.\ \isasymAnd k\ l.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\ l\isasymrbrakk \
1253 \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\ =\ i\ *\ j\ *\ k%
1256 We instantiate the quantifier with~\isa{k*l}:
1258 \isacommand{apply}\ (rule_tac\ x="k*l"\ \isakeyword{in}\ exI)\ \isanewline
1259 \ 1.\ \isasymAnd k\ ka.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\
1260 ka\isasymrbrakk \ \isasymLongrightarrow \ m\ *\ n\ =\ i\
1264 The rest is automatic, by arithmetic.
1266 \isacommand{apply}\ simp\isanewline
1267 \isacommand{done}\isanewline
1272 \section{Description Operators}
1275 \index{description operators|(}%
1276 HOL provides two description operators.
1277 A \textbf{definite description} formalizes the word ``the,'' as in
1278 ``the greatest divisior of~$n$.''
1279 It returns an arbitrary value unless the formula has a unique solution.
1280 An \textbf{indefinite description} formalizes the word ``some,'' as in
1281 ``some member of~$S$.'' It differs from a definite description in not
1282 requiring the solution to be unique: it uses the axiom of choice to pick any
1286 Description operators can be hard to reason about. Novices
1287 should try to avoid them. Fortunately, descriptions are seldom required.
1290 \subsection{Definite Descriptions}
1292 \index{descriptions!definite}%
1293 A definite description is traditionally written $\iota x. P(x)$. It denotes
1294 the $x$ such that $P(x)$ is true, provided there exists a unique such~$x$;
1295 otherwise, it returns an arbitrary value of the expected type.
1296 Isabelle uses \sdx{THE} for the Greek letter~$\iota$.
1298 %(The traditional notation could be provided, but it is not legible on screen.)
1300 We reason using this rule, where \isa{a} is the unique solution:
1302 \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \
1303 \isasymLongrightarrow \ (THE\ x.\ P\ x)\ =\ a%
1304 \rulenamedx{the_equality}
1306 For instance, we can define the
1307 cardinality of a finite set~$A$ to be that
1308 $n$ such that $A$ is in one-to-one correspondence with $\{1,\ldots,n\}$. We can then
1309 prove that the cardinality of the empty set is zero (since $n=0$ satisfies the
1310 description) and proceed to prove other facts.
1312 A more challenging example illustrates how Isabelle/HOL defines the least number
1313 operator, which denotes the least \isa{x} satisfying~\isa{P}:%
1314 \index{least number operator|see{\protect\isa{LEAST}}}
1316 (LEAST\ x.\ P\ x)\ = (THE\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
1317 P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))
1320 Let us prove the analogue of \isa{the_equality} for \sdx{LEAST}\@.
1322 \isacommand{theorem}\ Least_equality:\isanewline
1323 \ \ \ \ \ "\isasymlbrakk P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline
1324 \isacommand{apply}\ (simp\ add:\ Least_def)\isanewline
1326 \ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\isasymrbrakk \isanewline
1327 \isaindent{\ 1.\ }\isasymLongrightarrow \ (THE\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))\ =\ k%
1329 The first step has merely unfolded the definition.
1331 \isacommand{apply}\ (rule\ the_equality)\isanewline
1333 \ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\
1334 \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ P\ k\ \isasymand \
1335 (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ k\ \isasymle \ y)\isanewline
1336 \ 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
1337 \ \ \ \ \ \ \ \ \isasymLongrightarrow \ x\ =\ k%
1339 As always with \isa{the_equality}, we must show existence and
1340 uniqueness of the claimed solution,~\isa{k}. Existence, the first
1341 subgoal, is trivial. Uniqueness, the second subgoal, follows by antisymmetry:
1343 \isasymlbrakk x\ \isasymle \ y;\ y\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ x\ =\ y%
1344 \rulename{order_antisym}
1346 The assumptions imply both \isa{k~\isasymle~x} and \isa{x~\isasymle~k}. One
1347 call to \isa{auto} does it all:
1349 \isacommand{by}\ (auto\ intro:\ order_antisym)
1353 \subsection{Indefinite Descriptions}
1355 \index{Hilbert's $\varepsilon$-operator}%
1356 \index{descriptions!indefinite}%
1357 An indefinite description is traditionally written $\varepsilon x. P(x)$ and is
1358 known as Hilbert's $\varepsilon$-operator. It denotes
1359 some $x$ such that $P(x)$ is true, provided one exists.
1360 Isabelle uses \sdx{SOME} for the Greek letter~$\varepsilon$.
1362 Here is the definition of~\cdx{inv},\footnote{In fact, \isa{inv} is defined via a second constant \isa{inv_into}, which we ignore here.} which expresses inverses of
1365 inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%
1368 Using \isa{SOME} rather than \isa{THE} makes \isa{inv~f} behave well
1369 even if \isa{f} is not injective. As it happens, most useful theorems about
1370 \isa{inv} do assume the function to be injective.
1372 The inverse of \isa{f}, when applied to \isa{y}, returns some~\isa{x} such that
1373 \isa{f~x~=~y}. For example, we can prove \isa{inv~Suc} really is the inverse
1374 of the \isa{Suc} function
1376 \isacommand{lemma}\ "inv\ Suc\ (Suc\ n)\ =\ n"\isanewline
1377 \isacommand{by}\ (simp\ add:\ inv_def)
1381 The proof is a one-liner: the subgoal simplifies to a degenerate application of
1382 \isa{SOME}, which is then erased. In detail, the left-hand side simplifies
1383 to \isa{SOME\ x.\ Suc\ x\ =\ Suc\ n}, then to \isa{SOME\ x.\ x\ =\ n} and
1386 We know nothing about what
1387 \isa{inv~Suc} returns when applied to zero. The proof above still treats
1388 \isa{SOME} as a definite description, since it only reasons about
1389 situations in which the value is described uniquely. Indeed, \isa{SOME}
1390 satisfies this rule:
1392 \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \
1393 \isasymLongrightarrow \ (SOME\ x.\ P\ x)\ =\ a%
1394 \rulenamedx{some_equality}
1397 tricky and requires rules such as these:
1399 P\ x\ \isasymLongrightarrow \ P\ (SOME\ x.\ P\ x)
1400 \rulenamedx{someI}\isanewline
1401 \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ Q\
1402 x\isasymrbrakk \ \isasymLongrightarrow \ Q\ (SOME\ x.\ P\ x)
1405 Rule \isa{someI} is basic: if anything satisfies \isa{P} then so does
1406 \hbox{\isa{SOME\ x.\ P\ x}}. The repetition of~\isa{P} in the conclusion makes it
1407 difficult to apply in a backward proof, so the derived rule \isa{someI2} is
1411 For example, let us prove the \rmindex{axiom of choice}:
1413 \isacommand{theorem}\ axiom_of_choice:
1414 \ "(\isasymforall x.\ \isasymexists y.\ P\ x\ y)\ \isasymLongrightarrow \
1415 \isasymexists f.\ \isasymforall x.\ P\ x\ (f\ x)"\isanewline
1416 \isacommand{apply}\ (rule\ exI,\ rule\ allI)\isanewline
1418 \ 1.\ \isasymAnd x.\ \isasymforall x.\ \isasymexists y.\ P\ x\ y\
1419 \isasymLongrightarrow \ P\ x\ (?f\ x)
1422 We have applied the introduction rules; now it is time to apply the elimination
1426 \isacommand{apply}\ (drule\ spec,\ erule\ exE)\isanewline
1428 \ 1.\ \isasymAnd x\ y.\ P\ (?x2\ x)\ y\ \isasymLongrightarrow \ P\ x\ (?f\ x)
1432 The rule \isa{someI} automatically instantiates
1433 \isa{f} to \hbox{\isa{\isasymlambda x.\ SOME y.\ P\ x\ y}}, which is the choice
1434 function. It also instantiates \isa{?x2\ x} to \isa{x}.
1436 \isacommand{by}\ (rule\ someI)\isanewline
1439 \subsubsection{Historical Note}
1440 The original purpose of Hilbert's $\varepsilon$-operator was to express an
1441 existential destruction rule:
1442 \[ \infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P} \]
1443 This rule is seldom used for that purpose --- it can cause exponential
1444 blow-up --- but it is occasionally used as an introduction rule
1445 for the~$\varepsilon$-operator. Its name in HOL is \tdxbold{someI_ex}.%%
1446 \index{description operators|)}
1449 \section{Some Proofs That Fail}
1451 \index{proofs!examples of failing|(}%
1452 Most of the examples in this tutorial involve proving theorems. But not every
1453 conjecture is true, and it can be instructive to see how
1454 proofs fail. Here we attempt to prove a distributive law involving
1455 the existential quantifier and conjunction.
1457 \isacommand{lemma}\ "({\isasymexists}x.\ P\ x)\ \isasymand\
1458 ({\isasymexists}x.\ Q\ x)\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\
1461 The first steps are routine. We apply conjunction elimination to break
1462 the assumption into two existentially quantified assumptions.
1463 Applying existential elimination removes one of the quantifiers.
1465 \isacommand{apply}\ (erule\ conjE)\isanewline
1466 \isacommand{apply}\ (erule\ exE)\isanewline
1467 \ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
1470 When we remove the other quantifier, we get a different bound
1471 variable in the subgoal. (The name \isa{xa} is generated automatically.)
1473 \isacommand{apply}\ (erule\ exE)\isanewline
1474 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\
1475 \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
1477 The proviso of the existential elimination rule has forced the variables to
1478 differ: we can hardly expect two arbitrary values to be equal! There is
1479 no way to prove this subgoal. Removing the
1480 conclusion's existential quantifier yields two
1481 identical placeholders, which can become any term involving the variables \isa{x}
1482 and~\isa{xa}. We need one to become \isa{x}
1483 and the other to become~\isa{xa}, but Isabelle requires all instances of a
1484 placeholder to be identical.
1486 \isacommand{apply}\ (rule\ exI)\isanewline
1487 \isacommand{apply}\ (rule\ conjI)\isanewline
1488 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\
1489 \isasymLongrightarrow\ P\ (?x3\ x\ xa)\isanewline
1490 \ 2.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa)
1492 We can prove either subgoal
1493 using the \isa{assumption} method. If we prove the first one, the placeholder
1494 changes into~\isa{x}.
1496 \ \isacommand{apply}\ assumption\isanewline
1497 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\
1498 \isasymLongrightarrow\ Q\ x
1500 We are left with a subgoal that cannot be proved. Applying the \isa{assumption}
1501 method results in an error message:
1503 *** empty result sequence -- proof command failed
1505 When interacting with Isabelle via the shell interface,
1506 you can abandon a proof using the \isacommand{oops} command.
1510 Here is another abortive proof, illustrating the interaction between
1511 bound variables and unknowns.
1512 If $R$ is a reflexive relation,
1513 is there an $x$ such that $R\,x\,y$ holds for all $y$? Let us see what happens when
1514 we attempt to prove it.
1516 \isacommand{lemma}\ "\isasymforall y.\ R\ y\ y\ \isasymLongrightarrow
1517 \ \isasymexists x.\ \isasymforall y.\ R\ x\ y"
1519 First, we remove the existential quantifier. The new proof state has an
1520 unknown, namely~\isa{?x}.
1522 \isacommand{apply}\ (rule\ exI)\isanewline
1523 \ 1.\ \isasymforall y.\ R\ y\ y\ \isasymLongrightarrow \ \isasymforall y.\ R\ ?x\ y%
1525 It looks like we can just apply \isa{assumption}, but it fails. Isabelle
1526 refuses to substitute \isa{y}, a bound variable, for~\isa{?x}; that would be
1527 a bound variable capture. We can still try to finish the proof in some
1528 other way. We remove the universal quantifier from the conclusion, moving
1529 the bound variable~\isa{y} into the subgoal. But note that it is still
1532 \isacommand{apply}\ (rule\ allI)\isanewline
1533 \ 1.\ \isasymAnd y.\ \isasymforall y.\ R\ y\ y\ \isasymLongrightarrow \ R\ ?x\ y%
1535 Finally, we try to apply our reflexivity assumption. We obtain a
1536 new assumption whose identical placeholders may be replaced by
1537 any term involving~\isa{y}.
1539 \isacommand{apply}\ (drule\ spec)\isanewline
1540 \ 1.\ \isasymAnd y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y
1542 This subgoal can only be proved by putting \isa{y} for all the placeholders,
1543 making the assumption and conclusion become \isa{R\ y\ y}. Isabelle can
1544 replace \isa{?z2~y} by \isa{y}; this involves instantiating
1545 \isa{?z2} to the identity function. But, just as two steps earlier,
1546 Isabelle refuses to substitute~\isa{y} for~\isa{?x}.
1547 This example is typical of how Isabelle enforces sound quantifier reasoning.
1548 \index{proofs!examples of failing|)}
1550 \section{Proving Theorems Using the {\tt\slshape blast} Method}
1552 \index{*blast (method)|(}%
1553 It is hard to prove many theorems using the methods
1554 described above. A proof may be hundreds of steps long. You
1555 may need to search among different ways of proving certain
1556 subgoals. Often a choice that proves one subgoal renders another
1557 impossible to prove. There are further complications that we have not
1558 discussed, concerning negation and disjunction. Isabelle's
1559 \textbf{classical reasoner} is a family of tools that perform such
1560 proofs automatically. The most important of these is the
1563 In this section, we shall first see how to use the classical
1564 reasoner in its default mode and then how to insert additional
1565 rules, enabling it to work in new problem domains.
1567 We begin with examples from pure predicate logic. The following
1568 example is known as Andrew's challenge. Peter Andrews designed
1569 it to be hard to prove by automatic means.
1570 It is particularly hard for a resolution prover, where
1571 converting the nested biconditionals to
1572 clause form produces a combinatorial
1573 explosion~\cite{pelletier86}. However, the
1574 \isa{blast} method proves it in a fraction of a second.
1577 "(({\isasymexists}x.\
1581 (({\isasymexists}x.\
1582 q(x))=({\isasymforall}y.\
1584 \ \ =\ \ \ \ \isanewline
1586 (({\isasymexists}x.\
1588 q(x){=}q(y))\ =\ (({\isasymexists}x.\ p(x))=({\isasymforall}y.\ q(y))))"\isanewline
1589 \isacommand{by}\ blast
1591 The next example is a logic problem composed by Lewis Carroll.
1592 The \isa{blast} method finds it trivial. Moreover, it turns out
1593 that not all of the assumptions are necessary. We can
1594 experiment with variations of this formula and see which ones
1598 "({\isasymforall}x.\
1599 honest(x)\ \isasymand\
1600 industrious(x)\ \isasymlongrightarrow\
1602 \isasymand\ \ \isanewline
1603 \ \ \ \ \ \ \ \ \isasymnot\ ({\isasymexists}x.\
1604 grocer(x)\ \isasymand\
1606 \isasymand\ \isanewline
1607 \ \ \ \ \ \ \ \ ({\isasymforall}x.\
1608 industrious(x)\ \isasymand\
1609 grocer(x)\ \isasymlongrightarrow\
1611 \isasymand\ \isanewline
1612 \ \ \ \ \ \ \ \ ({\isasymforall}x.\
1613 cyclist(x)\ \isasymlongrightarrow\
1615 \isasymand\ \isanewline
1616 \ \ \ \ \ \ \ \ ({\isasymforall}x.\
1617 {\isasymnot}healthy(x)\ \isasymand\
1618 cyclist(x)\ \isasymlongrightarrow\
1619 {\isasymnot}honest(x))\
1621 \ \ \ \ \ \ \ \ \isasymlongrightarrow\
1623 grocer(x)\ \isasymlongrightarrow\
1624 {\isasymnot}cyclist(x))"\isanewline
1625 \isacommand{by}\ blast
1627 The \isa{blast} method is also effective for set theory, which is
1628 described in the next chapter. The formula below may look horrible, but
1629 the \isa{blast} method proves it in milliseconds.
1631 \isacommand{lemma}\ "({\isasymUnion}i{\isasymin}I.\ A(i))\ \isasyminter\ ({\isasymUnion}j{\isasymin}J.\ B(j))\ =\isanewline
1632 \ \ \ \ \ \ \ \ ({\isasymUnion}i{\isasymin}I.\ {\isasymUnion}j{\isasymin}J.\ A(i)\ \isasyminter\ B(j))"\isanewline
1633 \isacommand{by}\ blast
1636 Few subgoals are couched purely in predicate logic and set theory.
1637 We can extend the scope of the classical reasoner by giving it new rules.
1638 Extending it effectively requires understanding the notions of
1639 introduction, elimination and destruction rules. Moreover, there is a
1640 distinction between safe and unsafe rules. A
1641 \textbf{safe}\indexbold{safe rules} rule is one that can be applied
1642 backwards without losing information; an
1643 \textbf{unsafe}\indexbold{unsafe rules} rule loses information, perhaps
1644 transforming the subgoal into one that cannot be proved. The safe/unsafe
1645 distinction affects the proof search: if a proof attempt fails, the
1646 classical reasoner backtracks to the most recent unsafe rule application
1647 and makes another choice.
1649 An important special case avoids all these complications. A logical
1650 equivalence, which in higher-order logic is an equality between
1651 formulas, can be given to the classical
1652 reasoner and simplifier by using the attribute \attrdx{iff}. You
1653 should do so if the right hand side of the equivalence is
1654 simpler than the left-hand side.
1656 For example, here is a simple fact about list concatenation.
1657 The result of appending two lists is empty if and only if both
1658 of the lists are themselves empty. Obviously, applying this equivalence
1659 will result in a simpler goal. When stating this lemma, we include
1660 the \attrdx{iff} attribute. Once we have proved the lemma, Isabelle
1661 will make it known to the classical reasoner (and to the simplifier).
1664 [iff]:\ "(xs{\isacharat}ys\ =\ [])\ =\
1665 (xs=[]\ \isasymand\ ys=[])"\isanewline
1666 \isacommand{apply}\ (induct_tac\ xs)\isanewline
1667 \isacommand{apply}\ (simp_all)\isanewline
1671 This fact about multiplication is also appropriate for
1672 the \attrdx{iff} attribute:
1674 (\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
1676 A product is zero if and only if one of the factors is zero. The
1677 reasoning involves a disjunction. Proving new rules for
1678 disjunctive reasoning is hard, but translating to an actual disjunction
1679 works: the classical reasoner handles disjunction properly.
1681 In more detail, this is how the \attrdx{iff} attribute works. It converts
1682 the equivalence $P=Q$ to a pair of rules: the introduction
1683 rule $Q\Imp P$ and the destruction rule $P\Imp Q$. It gives both to the
1684 classical reasoner as safe rules, ensuring that all occurrences of $P$ in
1685 a subgoal are replaced by~$Q$. The simplifier performs the same
1686 replacement, since \isa{iff} gives $P=Q$ to the
1689 Classical reasoning is different from
1690 simplification. Simplification is deterministic. It applies rewrite rules
1691 repeatedly, as long as possible, transforming a goal into another goal. Classical
1692 reasoning uses search and backtracking in order to prove a goal outright.%
1693 \index{*blast (method)|)}%
1696 \section{Other Classical Reasoning Methods}
1698 The \isa{blast} method is our main workhorse for proving theorems
1699 automatically. Other components of the classical reasoner interact
1700 with the simplifier. Still others perform classical reasoning
1701 to a limited extent, giving the user fine control over the proof.
1703 Of the latter methods, the most useful is
1706 all obvious reasoning steps without splitting the goal into multiple
1707 parts. It does not apply unsafe rules that could render the
1708 goal unprovable. By performing the obvious
1709 steps, \isa{clarify} lays bare the difficult parts of the problem,
1710 where human intervention is necessary.
1712 For example, the following conjecture is false:
1714 \isacommand{lemma}\ "({\isasymforall}x.\ P\ x)\ \isasymand\
1715 ({\isasymexists}x.\ Q\ x)\ \isasymlongrightarrow\ ({\isasymforall}x.\ P\ x\
1716 \isasymand\ Q\ x)"\isanewline
1717 \isacommand{apply}\ clarify
1719 The \isa{blast} method would simply fail, but \isa{clarify} presents
1720 a subgoal that helps us see why we cannot continue the proof.
1722 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk{\isasymforall}x.\ P\ x;\ Q\
1723 xa\isasymrbrakk\ \isasymLongrightarrow\ P\ x\ \isasymand\ Q\ x
1725 The proof must fail because the assumption \isa{Q\ xa} and conclusion \isa{Q\ x}
1726 refer to distinct bound variables. To reach this state, \isa{clarify} applied
1727 the introduction rules for \isa{\isasymlongrightarrow} and \isa{\isasymforall}
1728 and the elimination rule for \isa{\isasymand}. It did not apply the introduction
1729 rule for \isa{\isasymand} because of its policy never to split goals.
1731 Also available is \methdx{clarsimp}, a method
1732 that interleaves \isa{clarify} and \isa{simp}. Also there is \methdx{safe},
1733 which like \isa{clarify} performs obvious steps but even applies those that
1736 The \methdx{force} method applies the classical
1737 reasoner and simplifier to one goal.
1738 Unless it can prove the goal, it fails. Contrast
1739 that with the \isa{auto} method, which also combines classical reasoning
1740 with simplification. The latter's purpose is to prove all the
1741 easy subgoals and parts of subgoals. Unfortunately, it can produce
1742 large numbers of new subgoals; also, since it proves some subgoals
1743 and splits others, it obscures the structure of the proof tree.
1744 The \isa{force} method does not have these drawbacks. Another
1745 difference: \isa{force} tries harder than {\isa{auto}} to prove
1746 its goal, so it can take much longer to terminate.
1748 Older components of the classical reasoner have largely been
1749 superseded by \isa{blast}, but they still have niche applications.
1750 Most important among these are \isa{fast} and \isa{best}. While \isa{blast}
1751 searches for proofs using a built-in first-order reasoner, these
1752 earlier methods search for proofs using standard Isabelle inference.
1753 That makes them slower but enables them to work in the
1754 presence of the more unusual features of Isabelle rules, such
1755 as type classes and function unknowns. For example, recall the introduction rule
1756 for Hilbert's $\varepsilon$-operator:
1758 ?P\ ?x\ \isasymLongrightarrow\ ?P\ (SOME\ x.\ ?P x)
1762 The repeated occurrence of the variable \isa{?P} makes this rule tricky
1763 to apply. Consider this contrived example:
1765 \isacommand{lemma}\ "\isasymlbrakk Q\ a;\ P\ a\isasymrbrakk\isanewline
1766 \ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ P\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)\
1767 \isasymand\ Q\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)"\isanewline
1768 \isacommand{apply}\ (rule\ someI)
1771 We can apply rule \isa{someI} explicitly. It yields the
1774 \ 1.\ \isasymlbrakk Q\ a;\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P\ ?x\
1777 The proof from this point is trivial. Could we have
1778 proved the theorem with a single command? Not using \isa{blast}: it
1779 cannot perform the higher-order unification needed here. The
1780 \methdx{fast} method succeeds:
1782 \isacommand{apply}\ (fast\ intro!:\ someI)
1785 The \methdx{best} method is similar to
1786 \isa{fast} but it uses a best-first search instead of depth-first search.
1787 Accordingly, it is slower but is less susceptible to divergence.
1788 Transitivity rules usually cause \isa{fast} to loop where \isa{best}
1791 Here is a summary of the classical reasoning methods:
1793 \item \methdx{blast} works automatically and is the fastest
1795 \item \methdx{clarify} and \methdx{clarsimp} perform obvious steps without
1796 splitting the goal; \methdx{safe} even splits goals
1798 \item \methdx{force} uses classical reasoning and simplification to prove a goal;
1799 \methdx{auto} is similar but leaves what it cannot prove
1801 \item \methdx{fast} and \methdx{best} are legacy methods that work well with rules
1802 involving unusual features
1804 A table illustrates the relationships among four of these methods.
1806 \begin{tabular}{r|l|l|}
1807 & no split & split \\ \hline
1808 no simp & \methdx{clarify} & \methdx{safe} \\ \hline
1809 simp & \methdx{clarsimp} & \methdx{auto} \\ \hline
1813 \section{Finding More Theorems}
1818 \section{Forward Proof: Transforming Theorems}\label{sec:forward}
1820 \index{forward proof|(}%
1821 Forward proof means deriving new facts from old ones. It is the
1822 most fundamental type of proof. Backward proof, by working from goals to
1823 subgoals, can help us find a difficult proof. But it is
1824 not always the best way of presenting the proof thus found. Forward
1825 proof is particularly good for reasoning from the general
1826 to the specific. For example, consider this distributive law for
1827 the greatest common divisor:
1828 \[ k\times\gcd(m,n) = \gcd(k\times m,k\times n)\]
1830 Putting $m=1$ we get (since $\gcd(1,n)=1$ and $k\times1=k$)
1831 \[ k = \gcd(k,k\times n)\]
1832 We have derived a new fact; if re-oriented, it might be
1833 useful for simplification. After re-orienting it and putting $n=1$, we
1834 derive another useful law:
1836 Substituting values for variables --- instantiation --- is a forward step.
1837 Re-orientation works by applying the symmetry of equality to
1838 an equation, so it too is a forward step.
1840 \subsection{Modifying a Theorem using {\tt\slshape of}, {\tt\slshape where}
1841 and {\tt\slshape THEN}}
1845 Let us reproduce our examples in Isabelle. Recall that in
1846 {\S}\ref{sec:fun-simplification} we declared the recursive function
1847 \isa{gcd}:\index{*gcd (constant)|(}
1849 \isacommand{fun}\ gcd\ ::\ "nat\ \isasymRightarrow \ nat\ \isasymRightarrow \ nat"\ \isakeyword{where}\isanewline
1850 \ \ "gcd\ m\ n\ =\ (if\ n=0\ then\ m\ else\ gcd\ n\ (m\ mod\ n))"
1853 From this definition, it is possible to prove the distributive law.
1854 That takes us to the starting point for our example.
1856 ?k\ *\ gcd\ ?m\ ?n\ =\ gcd\ (?k\ *\ ?m)\ (?k\ *\ ?n)
1857 \rulename{gcd_mult_distrib2}
1860 The first step in our derivation is to replace \isa{?m} by~1. We instantiate the
1861 theorem using~\attrdx{of}, which identifies variables in order of their
1862 appearance from left to right. In this case, the variables are \isa{?k}, \isa{?m}
1863 and~\isa{?n}. So, the expression
1864 \hbox{\texttt{[of k 1]}} replaces \isa{?k} by~\isa{k} and \isa{?m}
1867 \isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1]
1870 The keyword \commdx{lemmas} declares a new theorem, which can be derived
1871 from an existing one using attributes such as \isa{[of~k~1]}.
1873 \isa{thm gcd_mult_0}
1874 displays the result:
1876 \ \ \ \ \ k\ *\ gcd\ 1\ ?n\ =\ gcd\ (k\ *\ 1)\ (k\ *\ ?n)
1878 Something is odd: \isa{k} is an ordinary variable, while \isa{?n}
1879 is schematic. We did not specify an instantiation
1880 for \isa{?n}. In its present form, the theorem does not allow
1881 substitution for \isa{k}. One solution is to avoid giving an instantiation for
1882 \isa{?k}: instead of a term we can put an underscore~(\isa{_}). For example,
1884 \ \ \ \ \ gcd_mult_distrib2\ [of\ _\ 1]
1886 replaces \isa{?m} by~\isa{1} but leaves \isa{?k} unchanged.
1888 An equivalent solution is to use the attribute \isa{where}.
1890 \ \ \ \ \ gcd\_mult\_distrib2\ [where\ m=1]
1892 While \isa{of} refers to
1893 variables by their position, \isa{where} refers to variables by name. Multiple
1894 instantiations are separated by~\isa{and}, as in this example:
1896 \ \ \ \ \ gcd\_mult\_distrib2\ [where\ m=1\ and\ k=1]
1899 We now continue the present example with the version of \isa{gcd_mult_0}
1900 shown above, which has \isa{k} instead of \isa{?k}.
1901 Once we have replaced \isa{?m} by~1, we must next simplify
1902 the theorem \isa{gcd_mult_0}, performing the steps
1903 $\gcd(1,n)=1$ and $k\times1=k$. The \attrdx{simplified}
1904 attribute takes a theorem
1905 and returns the result of simplifying it, with respect to the default
1906 simplification rules:
1908 \isacommand{lemmas}\ gcd_mult_1\ =\ gcd_mult_0\
1912 Again, we display the resulting theorem:
1914 \ \ \ \ \ k\ =\ gcd\ k\ (k\ *\ ?n)
1917 To re-orient the equation requires the symmetry rule:
1920 \isasymLongrightarrow\ ?t\ =\
1924 The following declaration gives our equation to \isa{sym}:
1926 \ \ \ \isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_1\ [THEN\ sym]
1931 \ \ \ \ \ gcd\ k\ (k\ *\ ?n)\ =\ k%
1933 \isa{THEN~sym}\indexbold{*THEN (attribute)} gives the current theorem to the
1934 rule \isa{sym} and returns the resulting conclusion. The effect is to
1935 exchange the two operands of the equality. Typically \isa{THEN} is used
1936 with destruction rules. Also useful is \isa{THEN~spec}, which removes the
1937 quantifier from a theorem of the form $\forall x.\,P$, and \isa{THEN~mp},
1938 which converts the implication $P\imp Q$ into the rule
1939 $\vcenter{\infer{Q}{P}}$. Similar to \isa{mp} are the following two rules,
1940 which extract the two directions of reasoning about a boolean equivalence:
1942 \isasymlbrakk?Q\ =\ ?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
1945 \isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
1949 Normally we would never name the intermediate theorems
1950 such as \isa{gcd_mult_0} and \isa{gcd_mult_1} but would combine
1951 the three forward steps:
1953 \isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]%
1955 The directives, or attributes, are processed from left to right. This
1956 declaration of \isa{gcd_mult} is equivalent to the
1959 Such declarations can make the proof script hard to read. Better
1960 is to state the new lemma explicitly and to prove it using a single
1961 \isa{rule} method whose operand is expressed using forward reasoning:
1963 \isacommand{lemma}\ gcd\_mult\ [simp]:\ "gcd\ k\ (k*n)\ =\ k"\isanewline
1964 \isacommand{by}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym])
1966 Compared with the previous proof of \isa{gcd_mult}, this
1967 version shows the reader what has been proved. Also, the result will be processed
1968 in the normal way. In particular, Isabelle generalizes over all variables: the
1969 resulting theorem will have {\isa{?k}} instead of {\isa{k}}.
1971 At the start of this section, we also saw a proof of $\gcd(k,k)=k$. Here
1972 is the Isabelle version:\index{*gcd (constant)|)}
1974 \isacommand{lemma}\ gcd\_self\ [simp]:\ "gcd\ k\ k\ =\ k"\isanewline
1975 \isacommand{by}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified])
1979 To give~\isa{of} a nonatomic term, enclose it in quotation marks, as in
1980 \isa{[of "k*m"]}. The term must not contain unknowns: an
1982 \isa{[of "?k*m"]} will be rejected.
1985 %Answer is now included in that section! Is a modified version of this
1986 % exercise worth including? E.g. find a difference between the two ways
1989 %In {\S}\ref{sec:subst} the method \isa{subst\ mult_commute} was applied. How
1990 %can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}?
1991 %% answer rule (mult_commute [THEN ssubst])
1994 \subsection{Modifying a Theorem using {\tt\slshape OF}}
1996 \index{*OF (attribute)|(}%
1997 Recall that \isa{of} generates an instance of a
1998 rule by specifying values for its variables. Analogous is \isa{OF}, which
1999 generates an instance of a rule by specifying facts for its premises.
2001 We again need the divides relation\index{divides relation} of number theory, which
2002 as we recall is defined by
2004 ?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
2008 Suppose, for example, that we have proved the following rule.
2009 It states that if $k$ and $n$ are relatively prime
2010 and if $k$ divides $m\times n$ then $k$ divides $m$.
2012 \isasymlbrakk gcd ?k ?n {=} 1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\
2013 \isasymLongrightarrow\ ?k\ dvd\ ?m
2014 \rulename{relprime_dvd_mult}
2016 We can use \isa{OF} to create an instance of this rule.
2018 prove an instance of its first premise:
2020 \isacommand{lemma}\ relprime\_20\_81:\ "gcd\ 20\ 81\ =\ 1"\isanewline
2021 \isacommand{by}\ (simp\ add:\ gcd.simps)
2023 We have evaluated an application of the \isa{gcd} function by
2024 simplification. Expression evaluation involving recursive functions is not
2025 guaranteed to terminate, and it can be slow; Isabelle
2026 performs arithmetic by rewriting symbolic bit strings. Here,
2027 however, the simplification takes less than one second. We can
2028 give this new lemma to \isa{OF}. The expression
2030 \ \ \ \ \ relprime_dvd_mult [OF relprime_20_81]
2034 \ \ \ \ \ 20\ dvd\ (?m\ *\ 81)\ \isasymLongrightarrow\ 20\ dvd\ ?m%
2037 \isa{OF} takes any number of operands. Consider
2038 the following facts about the divides relation:
2040 \isasymlbrakk?k\ dvd\ ?m;\
2041 ?k\ dvd\ ?n\isasymrbrakk\
2042 \isasymLongrightarrow\ ?k\ dvd\
2044 \rulename{dvd_add}\isanewline
2048 Let us supply \isa{dvd_refl} for each of the premises of \isa{dvd_add}:
2050 \ \ \ \ \ dvd_add [OF dvd_refl dvd_refl]
2052 Here is the theorem that we have expressed:
2054 \ \ \ \ \ ?k\ dvd\ (?k\ +\ ?k)
2056 As with \isa{of}, we can use the \isa{_} symbol to leave some positions
2059 \ \ \ \ \ dvd_add [OF _ dvd_refl]
2063 \ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ ?m\ +\ ?k
2066 You may have noticed that \isa{THEN} and \isa{OF} are based on
2067 the same idea, namely to combine two rules. They differ in the
2068 order of the combination and thus in their effect. We use \isa{THEN}
2069 typically with a destruction rule to extract a subformula of the current
2070 theorem. We use \isa{OF} with a list of facts to generate an instance of
2071 the current theorem.%
2072 \index{*OF (attribute)|)}
2074 Here is a summary of some primitives for forward reasoning:
2076 \item \attrdx{of} instantiates the variables of a rule to a list of terms
2077 \item \attrdx{OF} applies a rule to a list of theorems
2078 \item \attrdx{THEN} gives a theorem to a named rule and returns the
2080 %\item \attrdx{rule_format} puts a theorem into standard form
2081 % by removing \isa{\isasymlongrightarrow} and~\isa{\isasymforall}
2082 \item \attrdx{simplified} applies the simplifier to a theorem
2083 \item \isacommand{lemmas} assigns a name to the theorem produced by the
2088 \section{Forward Reasoning in a Backward Proof}
2090 We have seen that the forward proof directives work well within a backward
2091 proof. There are many ways to achieve a forward style using our existing
2092 proof methods. We shall also meet some new methods that perform forward
2095 The methods \isa{drule}, \isa{frule}, \isa{drule_tac}, etc.,
2096 reason forward from a subgoal. We have seen them already, using rules such as
2098 \isa{spec} to operate on formulae. They can also operate on terms, using rules
2101 x\ =\ y\ \isasymLongrightarrow \ f\ x\ =\ f\ y%
2102 \rulenamedx{arg_cong}\isanewline
2103 i\ \isasymle \ j\ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ k%
2104 \rulename{mult_le_mono1}
2107 For example, let us prove a fact about divisibility in the natural numbers:
2109 \isacommand{lemma}\ "2\ \isasymle \ u\ \isasymLongrightarrow \ u*m\ \isasymnoteq
2110 \ Suc(u*n)"\isanewline
2111 \isacommand{apply}\ (intro\ notI)\isanewline
2112 \ 1.\ \isasymlbrakk 2\ \isasymle \ u;\ u\ *\ m\ =\ Suc\ (u\ *\ n)\isasymrbrakk \ \isasymLongrightarrow \ False%
2115 The key step is to apply the function \ldots\isa{mod\ u} to both sides of the
2117 \isa{u*m\ =\ Suc(u*n)}:\index{*drule_tac (method)}
2119 \isacommand{apply}\ (drule_tac\ f="\isasymlambda x.\ x\ mod\ u"\ \isakeyword{in}\
2120 arg_cong)\isanewline
2121 \ 1.\ \isasymlbrakk 2\ \isasymle \ u;\ u\ *\ m\ mod\ u\ =\ Suc\ (u\ *\ n)\ mod\
2122 u\isasymrbrakk \ \isasymLongrightarrow \ False
2125 Simplification reduces the left side to 0 and the right side to~1, yielding the
2126 required contradiction.
2128 \isacommand{apply}\ (simp\ add:\ mod_Suc)\isanewline
2132 Our proof has used a fact about remainder:
2134 Suc\ m\ mod\ n\ =\isanewline
2135 (if\ Suc\ (m\ mod\ n)\ =\ n\ then\ 0\ else\ Suc\ (m\ mod\ n))
2139 \subsection{The Method {\tt\slshape insert}}
2141 \index{*insert (method)|(}%
2142 The \isa{insert} method
2143 inserts a given theorem as a new assumption of all subgoals. This
2144 already is a forward step; moreover, we may (as always when using a
2146 \isa{of}, \isa{THEN} and other directives. The new assumption can then
2147 be used to help prove the subgoals.
2149 For example, consider this theorem about the divides relation. The first
2150 proof step inserts the distributive law for
2151 \isa{gcd}. We specify its variables as shown.
2153 \isacommand{lemma}\ relprime\_dvd\_mult:\ \isanewline
2154 \ \ \ \ \ \ "\isasymlbrakk \ gcd\ k\ n\ =\ 1;\ k\ dvd\ m*n\ \isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ m"\isanewline
2155 \isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\ n])
2157 In the resulting subgoal, note how the equation has been
2160 \ 1.\ \isasymlbrakk gcd\ k\ n\ =\ 1;\ k\ dvd\ m\ *\ n;\ m\ *\ gcd\ k\ n\ =\ gcd\ (m\ *\ k)\ (m\ *\ n)\isasymrbrakk \isanewline
2161 \isaindent{\ 1.\ }\isasymLongrightarrow \ k\ dvd\ m%
2163 The next proof step utilizes the assumption \isa{gcd\ k\ n\ =\ 1}
2164 (note that \isa{Suc\ 0} is another expression for 1):
2166 \isacommand{apply}(simp)\isanewline
2167 \ 1.\ \isasymlbrakk gcd\ k\ n\ =\ Suc\ 0;\ k\ dvd\ m\ *\ n;\ m\ =\ gcd\ (m\ *\ k)\ (m\ *\ n)\isasymrbrakk \isanewline
2168 \isaindent{\ 1.\ }\isasymLongrightarrow \ k\ dvd\ m%
2170 Simplification has yielded an equation for~\isa{m}. The rest of the proof
2174 Here is another demonstration of \isa{insert}. Division and
2175 remainder obey a well-known law:
2177 (?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m
2178 \rulename{mod_div_equality}
2181 We refer to this law explicitly in the following proof:
2183 \isacommand{lemma}\ div_mult_self_is_m:\ \isanewline
2184 \ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m*n)\ div\ n\ =\
2185 (m::nat)"\isanewline
2186 \isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m*n"\ n])\isanewline
2187 \isacommand{apply}\ (simp)\isanewline
2190 The first step inserts the law, specifying \isa{m*n} and
2191 \isa{n} for its variables. Notice that non-trivial expressions must be
2192 enclosed in quotation marks. Here is the resulting
2193 subgoal, with its new assumption:
2195 %0\ \isacharless\ n\ \isasymLongrightarrow\ (m\
2196 %*\ n)\ div\ n\ =\ m\isanewline
2197 \ 1.\ \isasymlbrakk0\ \isacharless\
2198 n;\ \ (m\ *\ n)\ div\ n\ *\ n\ +\ (m\ *\ n)\ mod\ n\
2199 =\ m\ *\ n\isasymrbrakk\isanewline
2200 \ \ \ \ \isasymLongrightarrow\ (m\ *\ n)\ div\ n\
2203 Simplification reduces \isa{(m\ *\ n)\ mod\ n} to zero.
2204 Then it cancels the factor~\isa{n} on both
2205 sides of the equation \isa{(m\ *\ n)\ div\ n\ *\ n\ =\ m\ *\ n}, proving the
2209 Any unknowns in the theorem given to \methdx{insert} will be universally
2210 quantified in the new assumption.
2212 \index{*insert (method)|)}
2214 \subsection{The Method {\tt\slshape subgoal_tac}}
2216 \index{*subgoal_tac (method)}%
2217 A related method is \isa{subgoal_tac}, but instead
2218 of inserting a theorem as an assumption, it inserts an arbitrary formula.
2219 This formula must be proved later as a separate subgoal. The
2220 idea is to claim that the formula holds on the basis of the current
2221 assumptions, to use this claim to complete the proof, and finally
2222 to justify the claim. It gives the proof
2223 some structure. If you find yourself generating a complex assumption by a
2224 long series of forward steps, consider using \isa{subgoal_tac} instead: you can
2225 state the formula you are aiming for, and perhaps prove it automatically.
2227 Look at the following example.
2229 \isacommand{lemma}\ "\isasymlbrakk(z::int)\ <\ 37;\ 66\ <\ 2*z;\ z*z\
2230 \isasymnoteq\ 1225;\ Q(34);\ Q(36)\isasymrbrakk\isanewline
2231 \ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ Q(z)"\isanewline
2232 \isacommand{apply}\ (subgoal_tac\ "z\ =\ 34\ \isasymor\ z\ =\
2234 \isacommand{apply}\ blast\isanewline
2235 \isacommand{apply}\ (subgoal_tac\ "z\ \isasymnoteq\ 35")\isanewline
2236 \isacommand{apply}\ arith\isanewline
2237 \isacommand{apply}\ force\isanewline
2240 The first assumption tells us
2241 that \isa{z} is no greater than~36. The second tells us that \isa{z}
2242 is at least~34. The third assumption tells us that \isa{z} cannot be 35, since
2243 $35\times35=1225$. So \isa{z} is either 34 or~36, and since \isa{Q} holds for
2244 both of those values, we have the conclusion.
2246 The Isabelle proof closely follows this reasoning. The first
2247 step is to claim that \isa{z} is either 34 or 36. The resulting proof
2248 state gives us two subgoals:
2250 %\isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\
2251 %Q\ 34;\ Q\ 36\isasymrbrakk\ \isasymLongrightarrow\ Q\ z\isanewline
2252 \ 1.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36;\isanewline
2253 \ \ \ \ \ z\ =\ 34\ \isasymor\ z\ =\ 36\isasymrbrakk\isanewline
2254 \ \ \ \ \isasymLongrightarrow\ Q\ z\isanewline
2255 \ 2.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36\isasymrbrakk\isanewline
2256 \ \ \ \ \isasymLongrightarrow\ z\ =\ 34\ \isasymor\ z\ =\ 36
2258 The first subgoal is trivial (\isa{blast}), but for the second Isabelle needs help to eliminate
2260 \isa{z}=35. The second invocation of {\isa{subgoal_tac}} leaves two
2263 \ 1.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\
2264 1225;\ Q\ 34;\ Q\ 36;\isanewline
2265 \ \ \ \ \ z\ \isasymnoteq\ 35\isasymrbrakk\isanewline
2266 \ \ \ \ \isasymLongrightarrow\ z\ =\ 34\ \isasymor\ z\ =\ 36\isanewline
2267 \ 2.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36\isasymrbrakk\isanewline
2268 \ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ 35
2271 Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic
2272 (\isa{arith}). For the second subgoal we apply the method \isa{force},
2273 which proceeds by assuming that \isa{z}=35 and arriving at a contradiction.
2277 Summary of these methods:
2279 \item \methdx{insert} adds a theorem as a new assumption
2280 \item \methdx{subgoal_tac} adds a formula as a new assumption and leaves the
2281 subgoal of proving that formula
2283 \index{forward proof|)}
2286 \section{Managing Large Proofs}
2288 Naturally you should try to divide proofs into manageable parts. Look for lemmas
2289 that can be proved separately. Sometimes you will observe that they are
2290 instances of much simpler facts. On other occasions, no lemmas suggest themselves
2291 and you are forced to cope with a long proof involving many subgoals.
2293 \subsection{Tacticals, or Control Structures}
2295 \index{tacticals|(}%
2296 If the proof is long, perhaps it at least has some regularity. Then you can
2297 express it more concisely using \textbf{tacticals}, which provide control
2298 structures. Here is a proof (it would be a one-liner using
2299 \isa{blast}, but forget that) that contains a series of repeated
2303 \isacommand{lemma}\ "\isasymlbrakk P\isasymlongrightarrow Q;\
2304 Q\isasymlongrightarrow R;\ R\isasymlongrightarrow S;\ P\isasymrbrakk \
2305 \isasymLongrightarrow \ S"\isanewline
2306 \isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
2307 \isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
2308 \isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
2309 \isacommand{apply}\ (assumption)\isanewline
2313 Each of the three identical commands finds an implication and proves its
2314 antecedent by assumption. The first one finds \isa{P\isasymlongrightarrow Q} and
2315 \isa{P}, concluding~\isa{Q}; the second one concludes~\isa{R} and the third one
2316 concludes~\isa{S}. The final step matches the assumption \isa{S} with the goal to
2319 Suffixing a method with a plus sign~(\isa+)\index{*"+ (tactical)}
2320 expresses one or more repetitions:
2322 \isacommand{lemma}\ "\isasymlbrakk P\isasymlongrightarrow Q;\ Q\isasymlongrightarrow R;\ R\isasymlongrightarrow S;\ P\isasymrbrakk \ \isasymLongrightarrow \ S"\isanewline
2323 \isacommand{by}\ (drule\ mp,\ assumption)+
2326 Using \isacommand{by} takes care of the final use of \isa{assumption}. The new
2327 proof is more concise. It is also more general: the repetitive method works
2328 for a chain of implications having any length, not just three.
2330 Choice is another control structure. Separating two methods by a vertical
2331 % we must use ?? rather than "| as the sorting item because somehow the presence
2332 % of | (even quoted) stops hyperref from putting |hyperpage at the end of the index
2334 bar~(\isa|)\index{??@\texttt{"|} (tactical)} gives the effect of applying the
2335 first method, and if that fails, trying the second. It can be combined with
2336 repetition, when the choice must be made over and over again. Here is a chain of
2337 implications in which most of the antecedents are proved by assumption, but one is
2338 proved by arithmetic:
2340 \isacommand{lemma}\ "\isasymlbrakk Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ x<5\isasymlongrightarrow P;\
2341 Suc\ x\ <\ 5\isasymrbrakk \ \isasymLongrightarrow \ R"\ \isanewline
2342 \isacommand{by}\ (drule\ mp,\ (assumption|arith))+
2345 method can prove $x<5$ from $x+1<5$, but it cannot duplicate the effect of
2346 \isa{assumption}. Therefore, we combine these methods using the choice
2349 A postfixed question mark~(\isa?)\index{*"? (tactical)} expresses zero or one
2350 repetitions of a method. It can also be viewed as the choice between executing a
2351 method and doing nothing. It is useless at top level but can be valuable
2352 within other control structures; for example,
2353 \isa{($m$+)?} performs zero or more repetitions of method~$m$.%
2357 \subsection{Subgoal Numbering}
2359 Another problem in large proofs is contending with huge
2360 subgoals or many subgoals. Induction can produce a proof state that looks
2363 \ 1.\ bigsubgoal1\isanewline
2364 \ 2.\ bigsubgoal2\isanewline
2365 \ 3.\ bigsubgoal3\isanewline
2366 \ 4.\ bigsubgoal4\isanewline
2367 \ 5.\ bigsubgoal5\isanewline
2370 If each \isa{bigsubgoal} is 15 lines or so, the proof state will be too big to
2371 scroll through. By default, Isabelle displays at most 10 subgoals. The
2372 \commdx{pr} command lets you change this limit:
2374 \isacommand{pr}\ 2\isanewline
2375 \ 1.\ bigsubgoal1\isanewline
2376 \ 2.\ bigsubgoal2\isanewline
2377 A total of 6 subgoals...
2381 All methods apply to the first subgoal.
2382 Sometimes, not only in a large proof, you may want to focus on some other
2383 subgoal. Then you should try the commands \isacommand{defer} or \isacommand{prefer}.
2385 In the following example, the first subgoal looks hard, while the others
2386 look as if \isa{blast} alone could prove them:
2388 \ 1.\ hard\isanewline
2389 \ 2.\ \isasymnot \ \isasymnot \ P\ \isasymLongrightarrow \ P\isanewline
2390 \ 3.\ Q\ \isasymLongrightarrow \ Q%
2393 The \commdx{defer} command moves the first subgoal into the last position.
2395 \isacommand{defer}\ 1\isanewline
2396 \ 1.\ \isasymnot \ \isasymnot \ P\ \isasymLongrightarrow \ P\isanewline
2397 \ 2.\ Q\ \isasymLongrightarrow \ Q\isanewline
2401 Now we apply \isa{blast} repeatedly to the easy subgoals:
2403 \isacommand{apply}\ blast+\isanewline
2406 Using \isacommand{defer}, we have cleared away the trivial parts of the proof so
2407 that we can devote attention to the difficult part.
2410 The \commdx{prefer} command moves the specified subgoal into the
2411 first position. For example, if you suspect that one of your subgoals is
2412 invalid (not a theorem), then you should investigate that subgoal first. If it
2413 cannot be proved, then there is no point in proving the other subgoals.
2415 \ 1.\ ok1\isanewline
2416 \ 2.\ ok2\isanewline
2420 We decide to work on the third subgoal.
2422 \isacommand{prefer}\ 3\isanewline
2423 \ 1.\ doubtful\isanewline
2424 \ 2.\ ok1\isanewline
2427 If we manage to prove \isa{doubtful}, then we can work on the other
2428 subgoals, confident that we are not wasting our time. Finally we revise the
2429 proof script to remove the \isacommand{prefer} command, since we needed it only to
2430 focus our exploration. The previous example is different: its use of
2431 \isacommand{defer} stops trivial subgoals from cluttering the rest of the
2432 proof. Even there, we should consider proving \isa{hard} as a preliminary
2433 lemma. Always seek ways to streamline your proofs.
2439 \item the control structures \isa+, \isa? and \isa| help express complicated proofs
2440 \item the \isacommand{pr} command can limit the number of subgoals to display
2441 \item the \isacommand{defer} and \isacommand{prefer} commands move a
2442 subgoal to the last or first position
2446 Explain the use of \isa? and \isa+ in this proof.
2448 \isacommand{lemma}\ "\isasymlbrakk P\isasymand Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ R"\isanewline
2449 \isacommand{by}\ (drule\ mp,\ (intro conjI)?,\ assumption+)+
2455 \section{Proving the Correctness of Euclid's Algorithm}
2456 \label{sec:proving-euclid}
2458 \index{Euclid's algorithm|(}\index{*gcd (constant)|(}\index{divides relation|(}%
2459 A brief development will demonstrate the techniques of this chapter,
2460 including \isa{blast} applied with additional rules. We shall also see
2461 \isa{case_tac} used to perform a Boolean case split.
2463 Let us prove that \isa{gcd} computes the greatest common
2464 divisor of its two arguments.
2466 We use induction: \isa{gcd.induct} is the
2467 induction rule returned by \isa{fun}. We simplify using
2468 rules proved in {\S}\ref{sec:fun-simplification}, since rewriting by the
2469 definition of \isa{gcd} can loop.
2471 \isacommand{lemma}\ gcd\_dvd\_both:\ "(gcd\ m\ n\ dvd\ m)\ \isasymand \ (gcd\ m\ n\ dvd\ n)"
2473 The induction formula must be a conjunction. In the
2474 inductive step, each conjunct establishes the other.
2476 \ 1.\ \isasymAnd m\ n.\ (n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
2477 \isaindent{\ 1.\ \isasymAnd m\ n.\ (}gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \isanewline
2478 \isaindent{\ 1.\ \isasymAnd m\ n.\ (}gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n)\ \isasymLongrightarrow \isanewline
2479 \isaindent{\ 1.\ \isasymAnd m\ n.\ }gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n%
2482 The conditional induction hypothesis suggests doing a case
2483 analysis on \isa{n=0}. We apply \methdx{case_tac} with type
2484 \isa{bool} --- and not with a datatype, as we have done until now. Since
2485 \isa{nat} is a datatype, we could have written
2486 \isa{case_tac~n} instead of \isa{case_tac~"n=0"}. However, the definition
2487 of \isa{gcd} makes a Boolean decision:
2489 \ \ \ \ "gcd\ m\ n\ =\ (if\ n=0\ then\ m\ else\ gcd\ n\ (m\ mod\ n))"
2491 Proofs about a function frequently follow the function's definition, so we perform
2492 case analysis over the same formula.
2494 \isacommand{apply}\ (case_tac\ "n=0")\isanewline
2495 \ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
2496 \isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
2497 \isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline
2498 \isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n\isanewline
2499 \ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
2500 \isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
2501 \isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk \isanewline
2502 \isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n%
2505 Simplification leaves one subgoal:
2507 \isacommand{apply}\ (simp_all)\isanewline
2508 \ 1.\ \isasymAnd m\ n.\ \isasymlbrakk gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
2509 \isaindent{\ 1.\ \isasymAnd m\ n.\ \ }0\ <\ n\isasymrbrakk \isanewline
2510 \isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ n\ (m\ mod\ n)\ dvd\ m%
2513 Here, we can use \isa{blast}.
2514 One of the assumptions, the induction hypothesis, is a conjunction.
2515 The two divides relationships it asserts are enough to prove
2516 the conclusion, for we have the following theorem at our disposal:
2518 \isasymlbrakk?k\ dvd\ (?m\ mod\ ?n){;}\ ?k\ dvd\ ?n\isasymrbrakk\ \isasymLongrightarrow\ ?k\ dvd\ ?m%
2519 \rulename{dvd_mod_imp_dvd}
2522 This theorem can be applied in various ways. As an introduction rule, it
2523 would cause backward chaining from the conclusion (namely
2524 \isa{?k~dvd~?m}) to the two premises, which
2525 also involve the divides relation. This process does not look promising
2526 and could easily loop. More sensible is to apply the rule in the forward
2527 direction; each step would eliminate an occurrence of the \isa{mod} symbol, so the
2528 process must terminate.
2530 \isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline
2533 Attaching the \attrdx{dest} attribute to \isa{dvd_mod_imp_dvd} tells
2534 \isa{blast} to use it as destruction rule; that is, in the forward direction.
2537 We have proved a conjunction. Now, let us give names to each of the
2540 \isacommand{lemmas}\ gcd_dvd1\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct1]\isanewline
2541 \isacommand{lemmas}\ gcd_dvd2\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct2]%
2543 Here we see \commdx{lemmas}
2544 used with the \attrdx{iff} attribute, which supplies the new theorems to the
2545 classical reasoner and the simplifier. Recall that \attrdx{THEN} is
2546 frequently used with destruction rules; \isa{THEN conjunct1} extracts the
2547 first half of a conjunctive theorem. Given \isa{gcd_dvd_both} it yields
2549 \ \ \ \ \ gcd\ ?m1\ ?n1\ dvd\ ?m1
2551 The variable names \isa{?m1} and \isa{?n1} arise because
2552 Isabelle renames schematic variables to prevent
2553 clashes. The second \isacommand{lemmas} declaration yields
2555 \ \ \ \ \ gcd\ ?m1\ ?n1\ dvd\ ?n1
2559 To complete the verification of the \isa{gcd} function, we must
2560 prove that it returns the greatest of all the common divisors
2561 of its arguments. The proof is by induction, case analysis and simplification.
2563 \isacommand{lemma}\ gcd\_greatest\ [rule\_format]:\isanewline
2564 \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n"
2567 The goal is expressed using HOL implication,
2568 \isa{\isasymlongrightarrow}, because the induction affects the two
2569 preconditions. The directive \isa{rule_format} tells Isabelle to replace
2570 each \isa{\isasymlongrightarrow} by \isa{\isasymLongrightarrow} before
2571 storing the eventual theorem. This directive can also remove outer
2572 universal quantifiers, converting the theorem into the usual format for
2573 inference rules. It can replace any series of applications of
2574 \isa{THEN} to the rules \isa{mp} and \isa{spec}. We did not have to
2577 \isacommand{lemma}\ gcd_greatest\
2578 [THEN mp, THEN mp]:\isanewline
2579 \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n"
2582 Because we are again reasoning about \isa{gcd}, we perform the same
2583 induction and case analysis as in the previous proof:
2584 \begingroup\samepage
2586 \ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
2587 \isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ n\ (m\ mod\ n);\isanewline
2588 \isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline
2589 \isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n\isanewline
2590 \ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
2591 \isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ n\ (m\ mod\ n);\isanewline
2592 \isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk \isanewline
2593 \isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n%
2597 \noindent Simplification proves both subgoals.
2599 \isacommand{apply}\ (simp_all\ add:\ dvd_mod)\isanewline
2602 In the first, where \isa{n=0}, the implication becomes trivial: \isa{k\ dvd\
2603 gcd\ m\ n} goes to~\isa{k\ dvd\ m}. The second subgoal is proved by
2604 an unfolding of \isa{gcd}, using this rule about divides:
2606 \isasymlbrakk ?f\ dvd\ ?m;\ ?f\ dvd\ ?n\isasymrbrakk \
2607 \isasymLongrightarrow \ ?f\ dvd\ ?m\ mod\ ?n%
2613 The facts proved above can be summarized as a single logical
2614 equivalence. This step gives us a chance to see another application
2617 \isacommand{theorem}\ gcd\_greatest\_iff\ [iff]:\ \isanewline
2618 \ \ \ \ \ \ \ \ "(k\ dvd\ gcd\ m\ n)\ =\ (k\ dvd\ m\ \isasymand \ k\ dvd\ n)"\isanewline
2619 \isacommand{by}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans)
2621 This theorem concisely expresses the correctness of the \isa{gcd}
2623 We state it with the \isa{iff} attribute so that
2624 Isabelle can use it to remove some occurrences of \isa{gcd}.
2625 The theorem has a one-line
2626 proof using \isa{blast} supplied with two additional introduction
2627 rules. The exclamation mark
2628 ({\isa{intro}}{\isa{!}})\ signifies safe rules, which are
2629 applied aggressively. Rules given without the exclamation mark
2630 are applied reluctantly and their uses can be undone if
2631 the search backtracks. Here the unsafe rule expresses transitivity
2632 of the divides relation:
2634 \isasymlbrakk?m\ dvd\ ?n;\ ?n\ dvd\ ?p\isasymrbrakk\ \isasymLongrightarrow\ ?m\ dvd\ ?p%
2635 \rulename{dvd_trans}
2637 Applying \isa{dvd_trans} as
2638 an introduction rule entails a risk of looping, for it multiplies
2639 occurrences of the divides symbol. However, this proof relies
2640 on transitivity reasoning. The rule {\isa{gcd\_greatest}} is safe to apply
2641 aggressively because it yields simpler subgoals. The proof implicitly
2642 uses \isa{gcd_dvd1} and \isa{gcd_dvd2} as safe rules, because they were
2643 declared using \isa{iff}.%
2644 \index{Euclid's algorithm|)}\index{*gcd (constant)|)}\index{divides relation|)}