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.
37 Natural deduction generally deserves its name. It is easy to use. Each
38 proof step consists of identifying the outermost symbol of a formula and
39 applying the corresponding rule. It creates new subgoals in
40 an obvious way from parts of the chosen formula. Expanding the
41 definitions of constants can blow up the goal enormously. Deriving natural
42 deduction rules for such constants lets us reason in terms of their key
43 properties, which might otherwise be obscured by the technicalities of its
44 definition. Natural deduction rules also lend themselves to automation.
46 \textbf{classical reasoner} accepts any suitable collection of natural deduction
47 rules and uses them to search for proofs automatically. Isabelle is designed around
48 natural deduction and many of its tools use the terminology of introduction
49 and elimination rules.%
50 \index{natural deduction|)}
53 \section{Introduction Rules}
55 \index{introduction rules|(}%
56 An introduction rule tells us when we can infer a formula
57 containing a specific logical symbol. For example, the conjunction
58 introduction rule says that if we have $P$ and if we have $Q$ then
59 we have $P\conj Q$. In a mathematics text, it is typically shown
61 \[ \infer{P\conj Q}{P & Q} \]
62 The rule introduces the conjunction
63 symbol~($\conj$) in its conclusion. In Isabelle proofs we
64 mainly reason backwards. When we apply this rule, the subgoal already has
65 the form of a conjunction; the proof step makes this conjunction symbol
68 In Isabelle notation, the rule looks like this:
70 \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulenamedx{conjI}
72 Carefully examine the syntax. The premises appear to the
73 left of the arrow and the conclusion to the right. The premises (if
74 more than one) are grouped using the fat brackets. The question marks
75 indicate \textbf{schematic variables} (also called
76 \textbf{unknowns}):\index{unknowns|bold} they may
77 be replaced by arbitrary formulas. If we use the rule backwards, Isabelle
78 tries to unify the current subgoal with the conclusion of the rule, which
79 has the form \isa{?P\ \isasymand\ ?Q}. (Unification is discussed below,
80 {\S}\ref{sec:unification}.) If successful,
81 it yields new subgoals given by the formulas assigned to
82 \isa{?P} and \isa{?Q}.
84 The following trivial proof illustrates how rules work. It also introduces a
85 style of indentation. If a command adds a new subgoal, then the next
86 command's indentation is increased by one space; if it proves a subgoal, then
87 the indentation is reduced. This provides the reader with hints about the
90 \isacommand{lemma}\ conj_rule:\ "\isasymlbrakk P;\
91 Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\
92 (Q\ \isasymand\ P)"\isanewline
93 \isacommand{apply}\ (rule\ conjI)\isanewline
94 \ \isacommand{apply}\ assumption\isanewline
95 \isacommand{apply}\ (rule\ conjI)\isanewline
96 \ \isacommand{apply}\ assumption\isanewline
97 \isacommand{apply}\ assumption
99 At the start, Isabelle presents
100 us with the assumptions (\isa{P} and~\isa{Q}) and with the goal to be proved,
102 (Q\ \isasymand\ P)}. We are working backwards, so when we
103 apply conjunction introduction, the rule removes the outermost occurrence
104 of the \isa{\isasymand} symbol. To apply a rule to a subgoal, we apply
105 the proof method \isa{rule} --- here with \isa{conjI}, the conjunction
108 %\isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\
109 %\isasymand\ P\isanewline
110 \ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
111 \ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P
113 Isabelle leaves two new subgoals: the two halves of the original conjunction.
114 The first is simply \isa{P}, which is trivial, since \isa{P} is among
115 the assumptions. We can apply the \methdx{assumption}
116 method, which proves a subgoal by finding a matching assumption.
118 \ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\
121 We are left with the subgoal of proving
122 \isa{Q\ \isasymand\ P} from the assumptions \isa{P} and~\isa{Q}. We apply
123 \isa{rule conjI} again.
125 \ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline
126 \ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P
128 We are left with two new subgoals, \isa{Q} and~\isa{P}, each of which can be proved
129 using the \isa{assumption} method.%
130 \index{introduction rules|)}
133 \section{Elimination Rules}
135 \index{elimination rules|(}%
136 Elimination rules work in the opposite direction from introduction
137 rules. In the case of conjunction, there are two such rules.
138 From $P\conj Q$ we infer $P$. also, from $P\conj Q$
140 \[ \infer{P}{P\conj Q} \qquad \infer{Q}{P\conj Q} \]
142 Now consider disjunction. There are two introduction rules, which resemble inverted forms of the
143 conjunction elimination rules:
144 \[ \infer{P\disj Q}{P} \qquad \infer{P\disj Q}{Q} \]
146 What is the disjunction elimination rule? The situation is rather different from
147 conjunction. From $P\disj Q$ we cannot conclude that $P$ is true and we
148 cannot conclude that $Q$ is true; there are no direct
149 elimination rules of the sort that we have seen for conjunction. Instead,
150 there is an elimination rule that works indirectly. If we are trying to prove
151 something else, say $R$, and we know that $P\disj Q$ holds, then we have to consider
152 two cases. We can assume that $P$ is true and prove $R$ and then assume that $Q$ is
153 true and prove $R$ a second time. Here we see a fundamental concept used in natural
154 deduction: that of the \textbf{assumptions}. We have to prove $R$ twice, under
155 different assumptions. The assumptions are local to these subproofs and are visible
158 In a logic text, the disjunction elimination rule might be shown
160 \[ \infer{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}} \]
161 The assumptions $[P]$ and $[Q]$ are bracketed
162 to emphasize that they are local to their subproofs. In Isabelle
163 notation, the already-familiar \isa{\isasymLongrightarrow} syntax serves the
166 \isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{disjE}
168 When we use this sort of elimination rule backwards, it produces
169 a case split. (We have seen this before, in proofs by induction.) The following proof
170 illustrates the use of disjunction elimination.
172 \isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\
173 \isasymLongrightarrow\ Q\ \isasymor\ P"\isanewline
174 \isacommand{apply}\ (erule\ disjE)\isanewline
175 \ \isacommand{apply}\ (rule\ disjI2)\isanewline
176 \ \isacommand{apply}\ assumption\isanewline
177 \isacommand{apply}\ (rule\ disjI1)\isanewline
178 \isacommand{apply}\ assumption
180 We assume \isa{P\ \isasymor\ Q} and
181 must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction
182 elimination rule, \isa{disjE}\@. We invoke it using \methdx{erule}, a
183 method designed to work with elimination rules. It looks for an assumption that
184 matches the rule's first premise. It deletes the matching assumption,
185 regards the first premise as proved and returns subgoals corresponding to
186 the remaining premises. When we apply \isa{erule} to \isa{disjE}, only two
187 subgoals result. This is better than applying it using \isa{rule}
188 to get three subgoals, then proving the first by assumption: the other
189 subgoals would have the redundant assumption
190 \hbox{\isa{P\ \isasymor\ Q}}.
191 Most of the time, \isa{erule} is the best way to use elimination rules, since it
192 replaces an assumption by its subformulas; only rarely does the original
193 assumption remain useful.
196 %P\ \isasymor\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline
197 \ 1.\ P\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline
198 \ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
200 These are the two subgoals returned by \isa{erule}. The first assumes
201 \isa{P} and the second assumes \isa{Q}. Tackling the first subgoal, we
202 need to show \isa{Q\ \isasymor\ P}\@. The second introduction rule
203 (\isa{disjI2}) can reduce this to \isa{P}, which matches the assumption.
205 \isa{rule} method with \isa{disjI2} \ldots
207 \ 1.\ P\ \isasymLongrightarrow\ P\isanewline
208 \ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
210 \ldots and finish off with the \isa{assumption}
211 method. We are left with the other subgoal, which
214 \ 1.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
216 Its proof is similar, using the introduction
219 The result of this proof is a new inference rule \isa{disj_swap}, which is neither
220 an introduction nor an elimination rule, but which might
221 be useful. We can use it to replace any goal of the form $Q\disj P$
222 by a one of the form $P\disj Q$.%
223 \index{elimination rules|)}
226 \section{Destruction Rules: Some Examples}
228 \index{destruction rules|(}%
229 Now let us examine the analogous proof for conjunction.
231 \isacommand{lemma}\ conj_swap:\ "P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P"\isanewline
232 \isacommand{apply}\ (rule\ conjI)\isanewline
233 \ \isacommand{apply}\ (drule\ conjunct2)\isanewline
234 \ \isacommand{apply}\ assumption\isanewline
235 \isacommand{apply}\ (drule\ conjunct1)\isanewline
236 \isacommand{apply}\ assumption
238 Recall that the conjunction elimination rules --- whose Isabelle names are
239 \isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half
240 of a conjunction. Rules of this sort (where the conclusion is a subformula of a
241 premise) are called \textbf{destruction} rules because they take apart and destroy
243 \footnote{This Isabelle terminology has no counterpart in standard logic texts,
244 although the distinction between the two forms of elimination rule is well known.
245 Girard \cite[page 74]{girard89},\index{Girard, Jean-Yves|fnote}
246 for example, writes ``The elimination rules
247 [for $\disj$ and $\exists$] are very
248 bad. What is catastrophic about them is the parasitic presence of a formula [$R$]
249 which has no structural link with the formula which is eliminated.''}
251 The first proof step applies conjunction introduction, leaving
254 %P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P\isanewline
255 \ 1.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\isanewline
256 \ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P
259 To invoke the elimination rule, we apply a new method, \isa{drule}.
260 Think of the \isa{d} as standing for \textbf{destruction} (or \textbf{direct}, if
261 you prefer). Applying the
262 second conjunction rule using \isa{drule} replaces the assumption
263 \isa{P\ \isasymand\ Q} by \isa{Q}.
265 \ 1.\ Q\ \isasymLongrightarrow\ Q\isanewline
266 \ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P
268 The resulting subgoal can be proved by applying \isa{assumption}.
269 The other subgoal is similarly proved, using the \isa{conjunct1} rule and the
270 \isa{assumption} method.
272 Choosing among the methods \isa{rule}, \isa{erule} and \isa{drule} is up to
273 you. Isabelle does not attempt to work out whether a rule
274 is an introduction rule or an elimination rule. The
275 method determines how the rule will be interpreted. Many rules
276 can be used in more than one way. For example, \isa{disj_swap} can
277 be applied to assumptions as well as to goals; it replaces any
278 assumption of the form
279 $P\disj Q$ by a one of the form $Q\disj P$.
281 Destruction rules are simpler in form than indirect rules such as \isa{disjE},
282 but they can be inconvenient. Each of the conjunction rules discards half
283 of the formula, when usually we want to take both parts of the conjunction as new
284 assumptions. The easiest way to do so is by using an
285 alternative conjunction elimination rule that resembles \isa{disjE}\@. It is
286 seldom, if ever, seen in logic books. In Isabelle syntax it looks like this:
288 \isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{conjE}
290 \index{destruction rules|)}
293 Use the rule \isa{conjE} to shorten the proof above.
297 \section{Implication}
299 \index{implication|(}%
300 At the start of this chapter, we saw the rule \emph{modus ponens}. It is, in fact,
301 a destruction rule. The matching introduction rule looks like this
304 (?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\
305 \isasymlongrightarrow\ ?Q\rulenamedx{impI}
307 And this is \emph{modus ponens}\index{modus ponens@\emph{modus ponens}}:
309 \isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\
310 \isasymLongrightarrow\ ?Q
314 Here is a proof using the implication rules. This
315 lemma performs a sort of uncurrying, replacing the two antecedents
316 of a nested implication by a conjunction. The proof illustrates
317 how assumptions work. At each proof step, the subgoals inherit the previous
318 assumptions, perhaps with additions or deletions. Rules such as
319 \isa{impI} and \isa{disjE} add assumptions, while applying \isa{erule} or
320 \isa{drule} deletes the matching assumption.
322 \isacommand{lemma}\ imp_uncurry:\
323 "P\ \isasymlongrightarrow\ (Q\
324 \isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\
325 \isasymand\ Q\ \isasymlongrightarrow\
327 \isacommand{apply}\ (rule\ impI)\isanewline
328 \isacommand{apply}\ (erule\ conjE)\isanewline
329 \isacommand{apply}\ (drule\ mp)\isanewline
330 \ \isacommand{apply}\ assumption\isanewline
331 \isacommand{apply}\ (drule\ mp)\isanewline
332 \ \ \isacommand{apply}\ assumption\isanewline
333 \ \isacommand{apply}\ assumption
335 First, we state the lemma and apply implication introduction (\isa{rule impI}),
336 which moves the conjunction to the assumptions.
338 %P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R\ \isasymLongrightarrow\ P\
339 %\isasymand\ Q\ \isasymlongrightarrow\ R\isanewline
340 \ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R
342 Next, we apply conjunction elimination (\isa{erule conjE}), which splits this
343 conjunction into two parts.
345 \ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\
346 Q\isasymrbrakk\ \isasymLongrightarrow\ R
348 Now, we work on the assumption \isa{P\ \isasymlongrightarrow\ (Q\
349 \isasymlongrightarrow\ R)}, where the parentheses have been inserted for
350 clarity. The nested implication requires two applications of
351 \textit{modus ponens}: \isa{drule mp}. The first use yields the
353 \isasymlongrightarrow\ R}, but first we must prove the extra subgoal
354 \isa{P}, which we do by assumption.
356 \ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
357 \ 2.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R
359 Repeating these steps for \isa{Q\
360 \isasymlongrightarrow\ R} yields the conclusion we seek, namely~\isa{R}.
362 \ 1.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\
363 \isasymLongrightarrow\ R
366 The symbols \isa{\isasymLongrightarrow} and \isa{\isasymlongrightarrow}
367 both stand for implication, but they differ in many respects. Isabelle
368 uses \isa{\isasymLongrightarrow} to express inference rules; the symbol is
369 built-in and Isabelle's inference mechanisms treat it specially. On the
370 other hand, \isa{\isasymlongrightarrow} is just one of the many connectives
371 available in higher-order logic. We reason about it using inference rules
372 such as \isa{impI} and \isa{mp}, just as we reason about the other
373 connectives. You will have to use \isa{\isasymlongrightarrow} in any
374 context that requires a formula of higher-order logic. Use
375 \isa{\isasymLongrightarrow} to separate a theorem's preconditions from its
377 \index{implication|)}
380 \index{by@\isacommand{by} (command)|(}%
381 The \isacommand{by} command is useful for proofs like these that use
382 \isa{assumption} heavily. It executes an
383 \isacommand{apply} command, then tries to prove all remaining subgoals using
384 \isa{assumption}. Since (if successful) it ends the proof, it also replaces the
385 \isacommand{done} symbol. For example, the proof above can be shortened:
387 \isacommand{lemma}\ imp_uncurry:\
388 "P\ \isasymlongrightarrow\ (Q\
389 \isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\
390 \isasymand\ Q\ \isasymlongrightarrow\
392 \isacommand{apply}\ (rule\ impI)\isanewline
393 \isacommand{apply}\ (erule\ conjE)\isanewline
394 \isacommand{apply}\ (drule\ mp)\isanewline
395 \ \isacommand{apply}\ assumption\isanewline
396 \isacommand{by}\ (drule\ mp)
398 We could use \isacommand{by} to replace the final \isacommand{apply} and
399 \isacommand{done} in any proof, but typically we use it
400 to eliminate calls to \isa{assumption}. It is also a nice way of expressing a
402 \index{by@\isacommand{by} (command)|)}
409 Negation causes surprising complexity in proofs. Its natural
410 deduction rules are straightforward, but additional rules seem
411 necessary in order to handle negated assumptions gracefully. This section
412 also illustrates the \isa{intro} method: a convenient way of
413 applying introduction rules.
415 Negation introduction deduces $\lnot P$ if assuming $P$ leads to a
416 contradiction. Negation elimination deduces any formula in the
417 presence of $\lnot P$ together with~$P$:
419 (?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P%
420 \rulenamedx{notI}\isanewline
421 \isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R%
425 Classical logic allows us to assume $\lnot P$
426 when attempting to prove~$P$:
428 (\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P%
429 \rulenamedx{classical}
432 \index{contrapositives|(}%
433 The implications $P\imp Q$ and $\lnot Q\imp\lnot P$ are logically
434 equivalent, and each is called the
435 \textbf{contrapositive} of the other. Four further rules support
436 reasoning about contrapositives. They differ in the placement of the
439 \isasymlbrakk?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
440 \rulename{contrapos_pp}\isanewline
441 \isasymlbrakk?Q;\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\
443 \rulename{contrapos_pn}\isanewline
444 \isasymlbrakk{\isasymnot}\ ?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
445 \rulename{contrapos_np}\isanewline
446 \isasymlbrakk{\isasymnot}\ ?Q;\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ \isasymnot\ ?P%
447 \rulename{contrapos_nn}
450 These rules are typically applied using the \isa{erule} method, where
451 their effect is to form a contrapositive from an
452 assumption and the goal's conclusion.%
453 \index{contrapositives|)}
455 The most important of these is \isa{contrapos_np}. It is useful
456 for applying introduction rules to negated assumptions. For instance,
457 the assumption $\lnot(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we
458 might want to use conjunction introduction on it.
459 Before we can do so, we must move that assumption so that it
460 becomes the conclusion. The following proof demonstrates this
463 \isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\
464 \isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\
466 \isacommand{apply}\ (erule_tac\ Q = "R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
467 contrapos_np)\isanewline
468 \isacommand{apply}\ (intro\ impI)\isanewline
469 \isacommand{by}\ (erule\ notE)
472 There are two negated assumptions and we need to exchange the conclusion with the
473 second one. The method \isa{erule contrapos_np} would select the first assumption,
474 which we do not want. So we specify the desired assumption explicitly
475 using a new method, \isa{erule_tac}. This is the resulting subgoal:
477 \ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\
478 R\isasymrbrakk\ \isasymLongrightarrow\ R\ \isasymlongrightarrow\ Q%
480 The former conclusion, namely \isa{R}, now appears negated among the assumptions,
481 while the negated formula \isa{R\ \isasymlongrightarrow\ Q} becomes the new
484 We can now apply introduction rules. We use the \methdx{intro} method, which
485 repeatedly applies the given introduction rules. Here its effect is equivalent
488 \ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ R;\
489 R\isasymrbrakk\ \isasymLongrightarrow\ Q%
491 We can see a contradiction in the form of assumptions \isa{\isasymnot\ R}
492 and~\isa{R}, which suggests using negation elimination. If applied on its own,
493 \isa{notE} will select the first negated assumption, which is useless.
494 Instead, we invoke the rule using the
496 Now when Isabelle selects the first assumption, it tries to prove \isa{P\
497 \isasymlongrightarrow\ Q} and fails; it then backtracks, finds the
498 assumption \isa{\isasymnot~R} and finally proves \isa{R} by assumption. That
503 The following example may be skipped on a first reading. It involves a
504 peculiar but important rule, a form of disjunction introduction:
506 (\isasymnot \ ?Q\ \isasymLongrightarrow \ ?P)\ \isasymLongrightarrow \ ?P\ \isasymor \ ?Q%
509 This rule combines the effects of \isa{disjI1} and \isa{disjI2}. Its great
510 advantage is that we can remove the disjunction symbol without deciding
511 which disjunction to prove. This treatment of disjunction is standard in sequent
515 \isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\
516 \isasymLongrightarrow\ P\ \isasymor\ (Q\ \isasymand\ R)"\isanewline
517 \isacommand{apply}\ (intro\ disjCI\ conjI)\isanewline
518 \isacommand{apply}\ (elim\ conjE\ disjE)\isanewline
519 \ \isacommand{apply}\ assumption
521 \isacommand{by}\ (erule\ contrapos_np,\ rule\ conjI)
524 The first proof step uses \isa{intro} to apply
525 the introduction rules \isa{disjCI} and \isa{conjI}. The resulting
526 subgoal has the negative assumption
527 \hbox{\isa{\isasymnot(Q\ \isasymand\ R)}}.
530 \ 1.\ \isasymlbrakk(P\ \isasymor\ Q)\ \isasymand\ R;\ \isasymnot\ (Q\ \isasymand\
531 R)\isasymrbrakk\ \isasymLongrightarrow\ P%
533 Next we apply the \isa{elim} method, which repeatedly applies
534 elimination rules; here, the elimination rules given
535 in the command. One of the subgoals is trivial (\isa{\isacommand{apply} assumption}),
536 leaving us with one other:
538 \ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P%
541 Now we must move the formula \isa{Q\ \isasymand\ R} to be the conclusion. The
544 \ \ \ \ \ (erule\ contrapos_np,\ rule\ conjI)
546 is robust: the \isa{conjI} forces the \isa{erule} to select a
547 conjunction. The two subgoals are the ones we would expect from applying
548 conjunction introduction to
549 \isa{Q~\isasymand~R}:
551 \ 1.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\
553 \ 2.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R%
555 They are proved by assumption, which is implicit in the \isacommand{by}
560 \section{Interlude: the Basic Methods for Rules}
562 We have seen examples of many tactics that operate on individual rules. It
563 may be helpful to review how they work given an arbitrary rule such as this:
564 \[ \infer{Q}{P@1 & \ldots & P@n} \]
565 Below, we refer to $P@1$ as the \bfindex{major premise}. This concept
566 applies only to elimination and destruction rules. These rules act upon an
567 instance of their major premise, typically to replace it by subformulas of itself.
569 Suppose that the rule above is called~\isa{R}\@. Here are the basic rule
570 methods, most of which we have already seen:
573 Method \isa{rule\ R} unifies~$Q$ with the current subgoal, replacing it
574 by $n$ new subgoals: instances of $P@1$, \ldots,~$P@n$.
575 This is backward reasoning and is appropriate for introduction rules.
577 Method \isa{erule\ R} unifies~$Q$ with the current subgoal and
578 simultaneously unifies $P@1$ with some assumption. The subgoal is
579 replaced by the $n-1$ new subgoals of proving
581 \ldots,~$P@n$, with the matching assumption deleted. It is appropriate for
582 elimination rules. The method
583 \isa{(rule\ R,\ assumption)} is similar, but it does not delete an
586 Method \isa{drule\ R} unifies $P@1$ with some assumption, which it
587 then deletes. The subgoal is
588 replaced by the $n-1$ new subgoals of proving $P@2$, \ldots,~$P@n$; an
589 $n$th subgoal is like the original one but has an additional assumption: an
590 instance of~$Q$. It is appropriate for destruction rules.
592 Method \isa{frule\ R} is like \isa{drule\ R} except that the matching
593 assumption is not deleted. (See {\S}\ref{sec:frule} below.)
596 Other methods apply a rule while constraining some of its
597 variables. The typical form is
599 \ \ \ \ \ \methdx{rule_tac}\ $v@1$ = $t@1$ \isakeyword{and} \ldots \isakeyword{and}
601 $t@k$ \isakeyword{in} R
603 This method behaves like \isa{rule R}, while instantiating the variables
605 $v@k$ as specified. We similarly have \methdx{erule_tac}, \methdx{drule_tac} and
606 \methdx{frule_tac}. These methods also let us specify which subgoal to
607 operate on. By default it is the first subgoal, as with nearly all
608 methods, but we can specify that rule \isa{R} should be applied to subgoal
611 \ \ \ \ \ rule_tac\ [$i$] R
616 \section{Unification and Substitution}\label{sec:unification}
618 \index{unification|(}%
619 As we have seen, Isabelle rules involve schematic variables, which begin with
620 a question mark and act as
621 placeholders for terms. \textbf{Unification} --- well known to Prolog programmers --- is the act of
622 making two terms identical, possibly replacing their schematic variables by
623 terms. The simplest case is when the two terms are already the same. Next
624 simplest is \textbf{pattern-matching}, which replaces variables in only one of the
626 \isa{rule} method typically matches the rule's conclusion
627 against the current subgoal. The
628 \isa{assumption} method matches the current subgoal's conclusion
629 against each of its assumptions. Unification can instantiate variables in both terms; the \isa{rule} method can do this if the goal
630 itself contains schematic variables. Other occurrences of the variables in
631 the rule or proof state are updated at the same time.
633 Schematic variables in goals represent unknown terms. Given a goal such
634 as $\exists x.\,P$, they let us proceed with a proof. They can be
635 filled in later, sometimes in stages and often automatically.
638 If unification fails when you think it should succeed, try setting the Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$
639 \textsf{Trace Unification},
640 which makes Isabelle show the cause of unification failures (in Proof
641 General's \textsf{Trace} buffer).
644 For example, suppose we are trying to prove this subgoal by assumption:
646 \ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a)
648 The \isa{assumption} method having failed, we try again with the flag set:
650 \isacommand{apply} assumption
652 In this trivial case, the output clearly shows that \isa{e} clashes with \isa{c}:
658 \textbf{higher-order} unification, which works in the
659 typed $\lambda$-calculus. The procedure requires search and is potentially
660 undecidable. For our purposes, however, the differences from ordinary
661 unification are straightforward. It handles bound variables
662 correctly, avoiding capture. The two terms
663 \isa{{\isasymlambda}x.\ f(x,z)} and \isa{{\isasymlambda}y.\ f(y,z)} are
664 trivially unifiable because they differ only by a bound variable renaming. The two terms \isa{{\isasymlambda}x.\ ?P} and
665 \isa{{\isasymlambda}x.\ t x} are not unifiable; replacing \isa{?P} by
666 \isa{t x} is forbidden because the free occurrence of~\isa{x} would become
667 bound. Unfortunately, even if \isa{trace_unify_fail} is set, Isabelle displays no information about this type of failure.
670 Higher-order unification sometimes must invent
671 $\lambda$-terms to replace function variables,
672 which can lead to a combinatorial explosion. However, Isabelle proofs tend
673 to involve easy cases where there are few possibilities for the
674 $\lambda$-term being constructed. In the easiest case, the
675 function variable is applied only to bound variables,
676 as when we try to unify \isa{{\isasymlambda}x\ y.\ f(?h x y)} and
677 \isa{{\isasymlambda}x\ y.\ f(x+y+a)}. The only solution is to replace
678 \isa{?h} by \isa{{\isasymlambda}x\ y.\ x+y+a}. Such cases admit at most
679 one unifier, like ordinary unification. A harder case is
680 unifying \isa{?h a} with~\isa{a+b}; it admits two solutions for \isa{?h},
681 namely \isa{{\isasymlambda}x.~a+b} and \isa{{\isasymlambda}x.~x+b}.
682 Unifying \isa{?h a} with~\isa{a+a+b} admits four solutions; their number is
683 exponential in the number of occurrences of~\isa{a} in the second term.
688 \subsection{Substitution and the {\tt\slshape subst} Method}
691 \index{substitution|(}%
692 Isabelle also uses function variables to express \textbf{substitution}.
693 A typical substitution rule allows us to replace one term by
694 another if we know that two terms are equal.
695 \[ \infer{P[t/x]}{s=t & P[s/x]} \]
696 The rule uses a notation for substitution: $P[t/x]$ is the result of
697 replacing $x$ by~$t$ in~$P$. The rule only substitutes in the positions
698 designated by~$x$. For example, it can
699 derive symmetry of equality from reflexivity. Using $x=s$ for~$P$
700 replaces just the first $s$ in $s=s$ by~$t$:
701 \[ \infer{t=s}{s=t & \infer{s=s}{}} \]
703 The Isabelle version of the substitution rule looks like this:
705 \isasymlbrakk?t\ =\ ?s;\ ?P\ ?s\isasymrbrakk\ \isasymLongrightarrow\ ?P\
709 Crucially, \isa{?P} is a function
710 variable. It can be replaced by a $\lambda$-term
711 with one bound variable, whose occurrences identify the places
712 in which $s$ will be replaced by~$t$. The proof above requires \isa{?P}
713 to be replaced by \isa{{\isasymlambda}x.~x=s}; the second premise will then
714 be \isa{s=s} and the conclusion will be \isa{t=s}.
716 The \isa{simp} method also replaces equals by equals, but the substitution
717 rule gives us more control. Consider this proof:
720 "\isasymlbrakk x\ =\ f\ x;\ odd(f\ x)\isasymrbrakk\ \isasymLongrightarrow\
722 \isacommand{by}\ (erule\ ssubst)
725 The assumption \isa{x\ =\ f\ x}, if used for rewriting, would loop,
726 replacing \isa{x} by \isa{f x} and then by
727 \isa{f(f x)} and so forth. (Here \isa{simp}
728 would see the danger and would re-orient the equality, but in more complicated
729 cases it can be fooled.) When we apply the substitution rule,
730 Isabelle replaces every
731 \isa{x} in the subgoal by \isa{f x} just once. It cannot loop. The
732 resulting subgoal is trivial by assumption, so the \isacommand{by} command
733 proves it implicitly.
735 We are using the \isa{erule} method in a novel way. Hitherto,
736 the conclusion of the rule was just a variable such as~\isa{?R}, but it may
737 be any term. The conclusion is unified with the subgoal just as
738 it would be with the \isa{rule} method. At the same time \isa{erule} looks
739 for an assumption that matches the rule's first premise, as usual. With
740 \isa{ssubst} the effect is to find, use and delete an equality
743 The \methdx{subst} method performs individual substitutions. In simple cases,
744 it closely resembles a use of the substitution rule. Suppose a
745 proof has reached this point:
747 \ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \ \isasymLongrightarrow \ f\ z\ =\ x\ *\ y%
749 Now we wish to apply a commutative law:
751 ?m\ *\ ?n\ =\ ?n\ *\ ?m%
752 \rulename{mult_commute}
754 Isabelle rejects our first attempt:
756 apply (simp add: mult_commute)
758 The simplifier notices the danger of looping and refuses to apply the
760 \footnote{More precisely, it only applies such a rule if the new term is
761 smaller under a specified ordering; here, \isa{x\ *\ y}
762 is already smaller than
765 The \isa{subst} method applies \isa{mult_commute} exactly once.
767 \isacommand{apply}\ (subst\ mult_commute)\isanewline
768 \ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \
769 \isasymLongrightarrow \ f\ z\ =\ y\ *\ x%
771 As we wanted, \isa{x\ *\ y} has become \isa{y\ *\ x}.
774 This use of the \methdx{subst} method has the same effect as the command
776 \isacommand{apply}\ (rule\ mult_commute [THEN ssubst])
778 The attribute \isa{THEN}, which combines two rules, is described in
779 {\S}\ref{sec:THEN} below. The \methdx{subst} method is more powerful than
780 applying the substitution rule. It can perform substitutions in a subgoal's
781 assumptions. Moreover, if the subgoal contains more than one occurrence of
782 the left-hand side of the equality, the \methdx{subst} method lets us specify which occurrence should be replaced.
785 \subsection{Unification and Its Pitfalls}
787 Higher-order unification can be tricky. Here is an example, which you may
788 want to skip on your first reading:
790 \isacommand{lemma}\ "\isasymlbrakk x\ =\
791 f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\
792 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
793 \isacommand{apply}\ (erule\ ssubst)\isanewline
794 \isacommand{back}\isanewline
795 \isacommand{back}\isanewline
796 \isacommand{back}\isanewline
797 \isacommand{back}\isanewline
798 \isacommand{apply}\ assumption\isanewline
802 By default, Isabelle tries to substitute for all the
803 occurrences. Applying \isa{erule\ ssubst} yields this subgoal:
805 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ (f\ x)
807 The substitution should have been done in the first two occurrences
808 of~\isa{x} only. Isabelle has gone too far. The \commdx{back}
809 command allows us to reject this possibility and demand a new one:
811 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ (f\ x)\ (f\ x)
814 Now Isabelle has left the first occurrence of~\isa{x} alone. That is
815 promising but it is not the desired combination. So we use \isacommand{back}
818 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ x\ (f\ x)
821 This also is wrong, so we use \isacommand{back} again:
823 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ x\ (f\ x)
826 And this one is wrong too. Looking carefully at the series
827 of alternatives, we see a binary countdown with reversed bits: 111,
828 011, 101, 001. Invoke \isacommand{back} again:
830 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ x%
832 At last, we have the right combination! This goal follows by assumption.%
833 \index{unification|)}
836 This example shows that unification can do strange things with
837 function variables. We were forced to select the right unifier using the
838 \isacommand{back} command. That is all right during exploration, but \isacommand{back}
839 should never appear in the final version of a proof. You can eliminate the
840 need for \isacommand{back} by giving Isabelle less freedom when you apply a rule.
842 One way to constrain the inference is by joining two methods in a
843 \isacommand{apply} command. Isabelle applies the first method and then the
844 second. If the second method fails then Isabelle automatically backtracks.
845 This process continues until the first method produces an output that the
846 second method can use. We get a one-line proof of our example:
848 \isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\
849 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
850 \isacommand{apply}\ (erule\ ssubst,\ assumption)\isanewline
855 The \isacommand{by} command works too, since it backtracks when
856 proving subgoals by assumption:
858 \isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\
859 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
860 \isacommand{by}\ (erule\ ssubst)
864 The most general way to constrain unification is
865 by instantiating variables in the rule. The method \isa{rule_tac} is
866 similar to \isa{rule}, but it
867 makes some of the rule's variables denote specified terms.
868 Also available are {\isa{drule_tac}} and \isa{erule_tac}. Here we need
869 \isa{erule_tac} since above we used \isa{erule}.
871 \isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
872 \isacommand{by}\ (erule_tac\ P = "\isasymlambda u.\ triple\ u\ u\ x"\
873 \isakeyword{in}\ ssubst)
876 To specify a desired substitution
877 requires instantiating the variable \isa{?P} with a $\lambda$-expression.
878 The bound variable occurrences in \isa{{\isasymlambda}u.\ P\ u\
879 u\ x} indicate that the first two arguments have to be substituted, leaving
880 the third unchanged. With this instantiation, backtracking is neither necessary
883 An alternative to \isa{rule_tac} is to use \isa{rule} with a theorem
884 modified using~\isa{of}, described in
885 {\S}\ref{sec:forward} below. But \isa{rule_tac}, unlike \isa{of}, can
886 express instantiations that refer to
887 \isasymAnd-bound variables in the current subgoal.%
888 \index{substitution|)}
891 \section{Quantifiers}
893 \index{quantifiers!universal|(}%
894 Quantifiers require formalizing syntactic substitution and the notion of
895 arbitrary value. Consider the universal quantifier. In a logic
896 book, its introduction rule looks like this:
897 \[ \infer{\forall x.\,P}{P} \]
898 Typically, a proviso written in English says that $x$ must not
899 occur in the assumptions. This proviso guarantees that $x$ can be regarded as
900 arbitrary, since it has not been assumed to satisfy any special conditions.
901 Isabelle's underlying formalism, called the
902 \bfindex{meta-logic}, eliminates the need for English. It provides its own
903 universal quantifier (\isasymAnd) to express the notion of an arbitrary value. We
904 have already seen another symbol of the meta-logic, namely
905 \isa\isasymLongrightarrow, which expresses inference rules and the treatment of
906 assumptions. The only other symbol in the meta-logic is \isa\isasymequiv, which
907 can be used to define constants.
909 \subsection{The Universal Introduction Rule}
911 Returning to the universal quantifier, we find that having a similar quantifier
912 as part of the meta-logic makes the introduction rule trivial to express:
914 (\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulenamedx{allI}
918 The following trivial proof demonstrates how the universal introduction
921 \isacommand{lemma}\ "{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x"\isanewline
922 \isacommand{apply}\ (rule\ allI)\isanewline
923 \isacommand{by}\ (rule\ impI)
925 The first step invokes the rule by applying the method \isa{rule allI}.
927 \ 1.\ \isasymAnd x.\ P\ x\ \isasymlongrightarrow\ P\ x
929 Note that the resulting proof state has a bound variable,
930 namely~\isa{x}. The rule has replaced the universal quantifier of
931 higher-order logic by Isabelle's meta-level quantifier. Our goal is to
933 \isa{P\ x\ \isasymlongrightarrow\ P\ x} for arbitrary~\isa{x}; it is
934 an implication, so we apply the corresponding introduction rule (\isa{impI}).
936 \ 1.\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow\ P\ x
938 This last subgoal is implicitly proved by assumption.
940 \subsection{The Universal Elimination Rule}
942 Now consider universal elimination. In a logic text,
943 the rule looks like this:
944 \[ \infer{P[t/x]}{\forall x.\,P} \]
945 The conclusion is $P$ with $t$ substituted for the variable~$x$.
946 Isabelle expresses substitution using a function variable:
948 {\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulenamedx{spec}
950 This destruction rule takes a
951 universally quantified formula and removes the quantifier, replacing
952 the bound variable \isa{x} by the schematic variable \isa{?x}. Recall that a
953 schematic variable starts with a question mark and acts as a
954 placeholder: it can be replaced by any term.
956 The universal elimination rule is also
957 available in the standard elimination format. Like \isa{conjE}, it never
958 appears in logic books:
960 \isasymlbrakk \isasymforall x.\ ?P\ x;\ ?P\ ?x\ \isasymLongrightarrow \ ?R\isasymrbrakk \ \isasymLongrightarrow \ ?R%
963 The methods \isa{drule~spec} and \isa{erule~allE} do precisely the
966 To see how $\forall$-elimination works, let us derive a rule about reducing
967 the scope of a universal quantifier. In mathematical notation we write
968 \[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \]
969 with the proviso ``$x$ not free in~$P$.'' Isabelle's treatment of
970 substitution makes the proviso unnecessary. The conclusion is expressed as
972 \isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the
973 variable \isa{P} can introduce a dependence upon~\isa{x}: that would be a
974 bound variable capture. Let us walk through the proof.
976 \isacommand{lemma}\ "(\isasymforall x.\ P\ \isasymlongrightarrow \ Q\ x)\
977 \isasymLongrightarrow \ P\ \isasymlongrightarrow \ (\isasymforall x.\ Q\
980 First we apply implies introduction (\isa{impI}),
981 which moves the \isa{P} from the conclusion to the assumptions. Then
982 we apply universal introduction (\isa{allI}).
984 \isacommand{apply}\ (rule\ impI,\ rule\ allI)\isanewline
985 \ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\
986 x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x
988 As before, it replaces the HOL
989 quantifier by a meta-level quantifier, producing a subgoal that
990 binds the variable~\isa{x}. The leading bound variables
991 (here \isa{x}) and the assumptions (here \isa{{\isasymforall}x.\ P\
992 \isasymlongrightarrow\ Q\ x} and \isa{P}) form the \textbf{context} for the
993 conclusion, here \isa{Q\ x}. Subgoals inherit the context,
994 although assumptions can be added or deleted (as we saw
995 earlier), while rules such as \isa{allI} add bound variables.
997 Now, to reason from the universally quantified
998 assumption, we apply the elimination rule using the \isa{drule}
999 method. This rule is called \isa{spec} because it specializes a universal formula
1000 to a particular term.
1002 \isacommand{apply}\ (drule\ spec)\isanewline
1003 \ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ P\ \isasymlongrightarrow\ Q\ (?x2\
1004 x)\isasymrbrakk\ \isasymLongrightarrow\ Q\ x
1006 Observe how the context has changed. The quantified formula is gone,
1007 replaced by a new assumption derived from its body. We have
1008 removed the quantifier and replaced the bound variable
1010 \isa{?x2~x}. This term is a placeholder: it may become any term that can be
1011 built from~\isa{x}. (Formally, \isa{?x2} is an unknown of function type, applied
1012 to the argument~\isa{x}.) This new assumption is an implication, so we can use
1013 \emph{modus ponens} on it, which concludes the proof.
1015 \isacommand{by}\ (drule\ mp)
1017 Let us take a closer look at this last step. \emph{Modus ponens} yields
1018 two subgoals: one where we prove the antecedent (in this case \isa{P}) and
1019 one where we may assume the consequent. Both of these subgoals are proved
1021 \isa{assumption} method, which is implicit in the
1022 \isacommand{by} command. Replacing the \isacommand{by} command by
1023 \isa{\isacommand{apply} (drule\ mp, assumption)} would have left one last
1026 \ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ Q\ (?x2\ x)\isasymrbrakk\
1027 \isasymLongrightarrow\ Q\ x
1029 The consequent is \isa{Q} applied to that placeholder. It may be replaced by any
1030 term built from~\isa{x}, and here
1031 it should simply be~\isa{x}. The assumption need not
1032 be identical to the conclusion, provided the two formulas are unifiable.%
1033 \index{quantifiers!universal|)}
1036 \subsection{The Existential Quantifier}
1038 \index{quantifiers!existential|(}%
1039 The concepts just presented also apply
1040 to the existential quantifier, whose introduction rule looks like this in
1043 ?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulenamedx{exI}
1045 If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
1046 P(x)$ is also true. It is a dual of the universal elimination rule, and
1047 logic texts present it using the same notation for substitution.
1050 elimination rule looks like this
1052 \[ \infer{Q}{\exists x.\,P & \infer*{Q}{[P]}} \]
1054 It looks like this in Isabelle:
1056 \isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulenamedx{exE}
1059 Given an existentially quantified theorem and some
1060 formula $Q$ to prove, it creates a new assumption by removing the quantifier. As with
1061 the universal introduction rule, the textbook version imposes a proviso on the
1062 quantified variable, which Isabelle expresses using its meta-logic. It is
1063 enough to have a universal quantifier in the meta-logic; we do not need an existential
1064 quantifier to be built in as well.
1069 \[ \exists x.\, P\conj Q(x)\Imp P\conj(\exists x.\, Q(x)). \]
1070 \emph{Hint}: the proof is similar
1071 to the one just above for the universal quantifier.
1073 \index{quantifiers!existential|)}
1076 \subsection{Renaming an Assumption: {\tt\slshape rename_tac}}
1078 \index{assumptions!renaming|(}\index{*rename_tac (method)|(}%
1079 When you apply a rule such as \isa{allI}, the quantified variable
1080 becomes a new bound variable of the new subgoal. Isabelle tries to avoid
1081 changing its name, but sometimes it has to choose a new name in order to
1082 avoid a clash. The result may not be ideal:
1084 \isacommand{lemma}\ "x\ <\ y\ \isasymLongrightarrow \ \isasymforall x\ y.\ P\ x\
1086 \isacommand{apply}\ (intro allI)\isanewline
1087 \ 1.\ \isasymAnd xa\ ya.\ x\ <\ y\ \isasymLongrightarrow \ P\ xa\ (f\ ya)
1090 The names \isa{x} and \isa{y} were already in use, so the new bound variables are
1091 called \isa{xa} and~\isa{ya}. You can rename them by invoking \isa{rename_tac}:
1094 \isacommand{apply}\ (rename_tac\ v\ w)\isanewline
1095 \ 1.\ \isasymAnd v\ w.\ x\ <\ y\ \isasymLongrightarrow \ P\ v\ (f\ w)
1097 Recall that \isa{rule_tac}\index{*rule_tac (method)!and renaming}
1099 theorem with specified terms. These terms may involve the goal's bound
1100 variables, but beware of referring to variables
1101 like~\isa{xa}. A future change to your theories could change the set of names
1102 produced at top level, so that \isa{xa} changes to~\isa{xb} or reverts to~\isa{x}.
1103 It is safer to rename automatically-generated variables before mentioning them.
1105 If the subgoal has more bound variables than there are names given to
1106 \isa{rename_tac}, the rightmost ones are renamed.%
1107 \index{assumptions!renaming|)}\index{*rename_tac (method)|)}
1110 \subsection{Reusing an Assumption: {\tt\slshape frule}}
1113 \index{assumptions!reusing|(}\index{*frule (method)|(}%
1114 Note that \isa{drule spec} removes the universal quantifier and --- as
1115 usual with elimination rules --- discards the original formula. Sometimes, a
1116 universal formula has to be kept so that it can be used again. Then we use a new
1117 method: \isa{frule}. It acts like \isa{drule} but copies rather than replaces
1118 the selected assumption. The \isa{f} is for \emph{forward}.
1120 In this example, going from \isa{P\ a} to \isa{P(h(h~a))}
1121 requires two uses of the quantified assumption, one for each~\isa{h}
1124 \isacommand{lemma}\ "\isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);
1125 \ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P(h\ (h\ a))"
1128 Examine the subgoal left by \isa{frule}:
1130 \isacommand{apply}\ (frule\ spec)\isanewline
1131 \ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);\ P\ a;\ P\ ?x\ \isasymlongrightarrow\ P\ (h\ ?x)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a))
1133 It is what \isa{drule} would have left except that the quantified
1134 assumption is still present. Next we apply \isa{mp} to the
1135 implication and the assumption~\isa{P\ a}:
1137 \isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
1138 \ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);\ P\ a;\ P\ (h\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a))
1141 We have created the assumption \isa{P(h\ a)}, which is progress. To
1142 continue the proof, we apply \isa{spec} again. We shall not need it
1143 again, so we can use
1146 \isacommand{apply}\ (drule\ spec)\isanewline
1147 \ 1.\ \isasymlbrakk P\ a;\ P\ (h\ a);\ P\ ?x2\
1148 \isasymlongrightarrow \ P\ (h\ ?x2)\isasymrbrakk \ \isasymLongrightarrow \
1152 The new assumption bridges the gap between \isa{P(h\ a)} and \isa{P(h(h\ a))}.
1154 \isacommand{by}\ (drule\ mp)
1158 \emph{A final remark}. Replacing this \isacommand{by} command with
1160 \isacommand{apply}\ (drule\ mp,\ assumption)
1162 would not work: it would add a second copy of \isa{P(h~a)} instead
1163 of the desired assumption, \isa{P(h(h~a))}. The \isacommand{by}
1164 command forces Isabelle to backtrack until it finds the correct one.
1165 Alternatively, we could have used the \isacommand{apply} command and bundled the
1166 \isa{drule mp} with \emph{two} calls of \isa{assumption}. Or, of course,
1167 we could have given the entire proof to \isa{auto}.%
1168 \index{assumptions!reusing|)}\index{*frule (method)|)}
1172 \subsection{Instantiating a Quantifier Explicitly}
1173 \index{quantifiers!instantiating}
1175 We can prove a theorem of the form $\exists x.\,P\, x$ by exhibiting a
1176 suitable term~$t$ such that $P\,t$ is true. Dually, we can use an
1177 assumption of the form $\forall x.\,P\, x$ to generate a new assumption $P\,t$ for
1178 a suitable term~$t$. In many cases,
1179 Isabelle makes the correct choice automatically, constructing the term by
1180 unification. In other cases, the required term is not obvious and we must
1181 specify it ourselves. Suitable methods are \isa{rule_tac}, \isa{drule_tac}
1182 and \isa{erule_tac}.
1184 We have seen (just above, {\S}\ref{sec:frule}) a proof of this lemma:
1186 \isacommand{lemma}\ "\isasymlbrakk \isasymforall x.\ P\ x\
1187 \isasymlongrightarrow \ P\ (h\ x);\ P\ a\isasymrbrakk \
1188 \isasymLongrightarrow \ P(h\ (h\ a))"
1190 We had reached this subgoal:
1192 \ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\
1193 x);\ P\ a;\ P\ (h\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a))
1196 The proof requires instantiating the quantified assumption with the
1199 \isacommand{apply}\ (drule_tac\ x\ =\ "h\ a"\ \isakeyword{in}\
1201 \ 1.\ \isasymlbrakk P\ a;\ P\ (h\ a);\ P\ (h\ a)\ \isasymlongrightarrow \
1202 P\ (h\ (h\ a))\isasymrbrakk \ \isasymLongrightarrow \ P\ (h\ (h\ a))
1204 We have forced the desired instantiation.
1207 Existential formulas can be instantiated too. The next example uses the
1208 \textbf{divides} relation\index{divides relation}
1211 ?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
1215 Let us prove that multiplication of natural numbers is monotone with
1216 respect to the divides relation:
1218 \isacommand{lemma}\ mult_dvd_mono:\ "{\isasymlbrakk}i\ dvd\ m;\ j\ dvd\
1219 n\isasymrbrakk\ \isasymLongrightarrow\ i*j\ dvd\ (m*n\ ::\ nat)"\isanewline
1220 \isacommand{apply}\ (simp\ add:\ dvd_def)
1223 Unfolding the definition of divides has left this subgoal:
1225 \ 1.\ \isasymlbrakk \isasymexists k.\ m\ =\ i\ *\ k;\ \isasymexists k.\ n\
1226 =\ j\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\
1230 Next, we eliminate the two existential quantifiers in the assumptions:
1232 \isacommand{apply}\ (erule\ exE)\isanewline
1233 \ 1.\ \isasymAnd k.\ \isasymlbrakk \isasymexists k.\ n\ =\ j\ *\ k;\ m\ =\
1234 i\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\
1237 \isacommand{apply}\ (erule\ exE)
1239 \ 1.\ \isasymAnd k\ ka.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\
1240 ka\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\ =\ i\
1244 The term needed to instantiate the remaining quantifier is~\isa{k*ka}. But
1245 \isa{ka} is an automatically-generated name. As noted above, references to
1246 such variable names makes a proof less resilient to future changes. So,
1247 first we rename the most recent variable to~\isa{l}:
1249 \isacommand{apply}\ (rename_tac\ l)\isanewline
1250 \ 1.\ \isasymAnd k\ l.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\ l\isasymrbrakk \
1251 \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\ =\ i\ *\ j\ *\ k%
1254 We instantiate the quantifier with~\isa{k*l}:
1256 \isacommand{apply}\ (rule_tac\ x="k*l"\ \isakeyword{in}\ exI)\ \isanewline
1257 \ 1.\ \isasymAnd k\ ka.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\
1258 ka\isasymrbrakk \ \isasymLongrightarrow \ m\ *\ n\ =\ i\
1262 The rest is automatic, by arithmetic.
1264 \isacommand{apply}\ simp\isanewline
1265 \isacommand{done}\isanewline
1270 \section{Description Operators}
1273 \index{description operators|(}%
1274 HOL provides two description operators.
1275 A \textbf{definite description} formalizes the word ``the,'' as in
1276 ``the greatest divisior of~$n$.''
1277 It returns an arbitrary value unless the formula has a unique solution.
1278 An \textbf{indefinite description} formalizes the word ``some,'' as in
1279 ``some member of~$S$.'' It differs from a definite description in not
1280 requiring the solution to be unique: it uses the axiom of choice to pick any
1284 Description operators can be hard to reason about. Novices
1285 should try to avoid them. Fortunately, descriptions are seldom required.
1288 \subsection{Definite Descriptions}
1290 \index{descriptions!definite}%
1291 A definite description is traditionally written $\iota x. P(x)$. It denotes
1292 the $x$ such that $P(x)$ is true, provided there exists a unique such~$x$;
1293 otherwise, it returns an arbitrary value of the expected type.
1294 Isabelle uses \sdx{THE} for the Greek letter~$\iota$.
1296 %(The traditional notation could be provided, but it is not legible on screen.)
1298 We reason using this rule, where \isa{a} is the unique solution:
1300 \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \
1301 \isasymLongrightarrow \ (THE\ x.\ P\ x)\ =\ a%
1302 \rulenamedx{the_equality}
1304 For instance, we can define the
1305 cardinality of a finite set~$A$ to be that
1306 $n$ such that $A$ is in one-to-one correspondence with $\{1,\ldots,n\}$. We can then
1307 prove that the cardinality of the empty set is zero (since $n=0$ satisfies the
1308 description) and proceed to prove other facts.
1310 A more challenging example illustrates how Isabelle/HOL defines the least number
1311 operator, which denotes the least \isa{x} satisfying~\isa{P}:%
1312 \index{least number operator|see{\protect\isa{LEAST}}}
1314 (LEAST\ x.\ P\ x)\ = (THE\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
1315 P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))
1318 Let us prove the analogue of \isa{the_equality} for \sdx{LEAST}\@.
1320 \isacommand{theorem}\ Least_equality:\isanewline
1321 \ \ \ \ \ "\isasymlbrakk P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline
1322 \isacommand{apply}\ (simp\ add:\ Least_def)\isanewline
1324 \ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\isasymrbrakk \isanewline
1325 \isaindent{\ 1.\ }\isasymLongrightarrow \ (THE\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))\ =\ k%
1327 The first step has merely unfolded the definition.
1329 \isacommand{apply}\ (rule\ the_equality)\isanewline
1331 \ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\
1332 \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ P\ k\ \isasymand \
1333 (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ k\ \isasymle \ y)\isanewline
1334 \ 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
1335 \ \ \ \ \ \ \ \ \isasymLongrightarrow \ x\ =\ k%
1337 As always with \isa{the_equality}, we must show existence and
1338 uniqueness of the claimed solution,~\isa{k}. Existence, the first
1339 subgoal, is trivial. Uniqueness, the second subgoal, follows by antisymmetry:
1341 \isasymlbrakk x\ \isasymle \ y;\ y\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ x\ =\ y%
1342 \rulename{order_antisym}
1344 The assumptions imply both \isa{k~\isasymle~x} and \isa{x~\isasymle~k}. One
1345 call to \isa{auto} does it all:
1347 \isacommand{by}\ (auto\ intro:\ order_antisym)
1351 \subsection{Indefinite Descriptions}
1353 \index{Hilbert's $\varepsilon$-operator}%
1354 \index{descriptions!indefinite}%
1355 An indefinite description is traditionally written $\varepsilon x. P(x)$ and is
1356 known as Hilbert's $\varepsilon$-operator. It denotes
1357 some $x$ such that $P(x)$ is true, provided one exists.
1358 Isabelle uses \sdx{SOME} for the Greek letter~$\varepsilon$.
1360 Here is the definition of~\cdx{inv}, which expresses inverses of
1363 inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%
1366 Using \isa{SOME} rather than \isa{THE} makes \isa{inv~f} behave well
1367 even if \isa{f} is not injective. As it happens, most useful theorems about
1368 \isa{inv} do assume the function to be injective.
1370 The inverse of \isa{f}, when applied to \isa{y}, returns some~\isa{x} such that
1371 \isa{f~x~=~y}. For example, we can prove \isa{inv~Suc} really is the inverse
1372 of the \isa{Suc} function
1374 \isacommand{lemma}\ "inv\ Suc\ (Suc\ n)\ =\ n"\isanewline
1375 \isacommand{by}\ (simp\ add:\ inv_def)
1379 The proof is a one-liner: the subgoal simplifies to a degenerate application of
1380 \isa{SOME}, which is then erased. In detail, the left-hand side simplifies
1381 to \isa{SOME\ x.\ Suc\ x\ =\ Suc\ n}, then to \isa{SOME\ x.\ x\ =\ n} and
1384 We know nothing about what
1385 \isa{inv~Suc} returns when applied to zero. The proof above still treats
1386 \isa{SOME} as a definite description, since it only reasons about
1387 situations in which the value is described uniquely. Indeed, \isa{SOME}
1388 satisfies this rule:
1390 \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \
1391 \isasymLongrightarrow \ (SOME\ x.\ P\ x)\ =\ a%
1392 \rulenamedx{some_equality}
1395 tricky and requires rules such as these:
1397 P\ x\ \isasymLongrightarrow \ P\ (SOME\ x.\ P\ x)
1398 \rulenamedx{someI}\isanewline
1399 \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ Q\
1400 x\isasymrbrakk \ \isasymLongrightarrow \ Q\ (SOME\ x.\ P\ x)
1403 Rule \isa{someI} is basic: if anything satisfies \isa{P} then so does
1404 \hbox{\isa{SOME\ x.\ P\ x}}. The repetition of~\isa{P} in the conclusion makes it
1405 difficult to apply in a backward proof, so the derived rule \isa{someI2} is
1409 For example, let us prove the \rmindex{axiom of choice}:
1411 \isacommand{theorem}\ axiom_of_choice:
1412 \ "(\isasymforall x.\ \isasymexists y.\ P\ x\ y)\ \isasymLongrightarrow \
1413 \isasymexists f.\ \isasymforall x.\ P\ x\ (f\ x)"\isanewline
1414 \isacommand{apply}\ (rule\ exI,\ rule\ allI)\isanewline
1416 \ 1.\ \isasymAnd x.\ \isasymforall x.\ \isasymexists y.\ P\ x\ y\
1417 \isasymLongrightarrow \ P\ x\ (?f\ x)
1420 We have applied the introduction rules; now it is time to apply the elimination
1424 \isacommand{apply}\ (drule\ spec,\ erule\ exE)\isanewline
1426 \ 1.\ \isasymAnd x\ y.\ P\ (?x2\ x)\ y\ \isasymLongrightarrow \ P\ x\ (?f\ x)
1430 The rule \isa{someI} automatically instantiates
1431 \isa{f} to \hbox{\isa{\isasymlambda x.\ SOME y.\ P\ x\ y}}, which is the choice
1432 function. It also instantiates \isa{?x2\ x} to \isa{x}.
1434 \isacommand{by}\ (rule\ someI)\isanewline
1437 \subsubsection{Historical Note}
1438 The original purpose of Hilbert's $\varepsilon$-operator was to express an
1439 existential destruction rule:
1440 \[ \infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P} \]
1441 This rule is seldom used for that purpose --- it can cause exponential
1442 blow-up --- but it is occasionally used as an introduction rule
1443 for the~$\varepsilon$-operator. Its name in HOL is \tdxbold{someI_ex}.%%
1444 \index{description operators|)}
1447 \section{Some Proofs That Fail}
1449 \index{proofs!examples of failing|(}%
1450 Most of the examples in this tutorial involve proving theorems. But not every
1451 conjecture is true, and it can be instructive to see how
1452 proofs fail. Here we attempt to prove a distributive law involving
1453 the existential quantifier and conjunction.
1455 \isacommand{lemma}\ "({\isasymexists}x.\ P\ x)\ \isasymand\
1456 ({\isasymexists}x.\ Q\ x)\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\
1459 The first steps are routine. We apply conjunction elimination to break
1460 the assumption into two existentially quantified assumptions.
1461 Applying existential elimination removes one of the quantifiers.
1463 \isacommand{apply}\ (erule\ conjE)\isanewline
1464 \isacommand{apply}\ (erule\ exE)\isanewline
1465 \ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
1468 When we remove the other quantifier, we get a different bound
1469 variable in the subgoal. (The name \isa{xa} is generated automatically.)
1471 \isacommand{apply}\ (erule\ exE)\isanewline
1472 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\
1473 \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
1475 The proviso of the existential elimination rule has forced the variables to
1476 differ: we can hardly expect two arbitrary values to be equal! There is
1477 no way to prove this subgoal. Removing the
1478 conclusion's existential quantifier yields two
1479 identical placeholders, which can become any term involving the variables \isa{x}
1480 and~\isa{xa}. We need one to become \isa{x}
1481 and the other to become~\isa{xa}, but Isabelle requires all instances of a
1482 placeholder to be identical.
1484 \isacommand{apply}\ (rule\ exI)\isanewline
1485 \isacommand{apply}\ (rule\ conjI)\isanewline
1486 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\
1487 \isasymLongrightarrow\ P\ (?x3\ x\ xa)\isanewline
1488 \ 2.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa)
1490 We can prove either subgoal
1491 using the \isa{assumption} method. If we prove the first one, the placeholder
1492 changes into~\isa{x}.
1494 \ \isacommand{apply}\ assumption\isanewline
1495 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\
1496 \isasymLongrightarrow\ Q\ x
1498 We are left with a subgoal that cannot be proved. Applying the \isa{assumption}
1499 method results in an error message:
1501 *** empty result sequence -- proof command failed
1503 When interacting with Isabelle via the shell interface,
1504 you can abandon a proof using the \isacommand{oops} command.
1508 Here is another abortive proof, illustrating the interaction between
1509 bound variables and unknowns.
1510 If $R$ is a reflexive relation,
1511 is there an $x$ such that $R\,x\,y$ holds for all $y$? Let us see what happens when
1512 we attempt to prove it.
1514 \isacommand{lemma}\ "\isasymforall y.\ R\ y\ y\ \isasymLongrightarrow
1515 \ \isasymexists x.\ \isasymforall y.\ R\ x\ y"
1517 First, we remove the existential quantifier. The new proof state has an
1518 unknown, namely~\isa{?x}.
1520 \isacommand{apply}\ (rule\ exI)\isanewline
1521 \ 1.\ \isasymforall y.\ R\ y\ y\ \isasymLongrightarrow \ \isasymforall y.\ R\ ?x\ y%
1523 It looks like we can just apply \isa{assumption}, but it fails. Isabelle
1524 refuses to substitute \isa{y}, a bound variable, for~\isa{?x}; that would be
1525 a bound variable capture. We can still try to finish the proof in some
1526 other way. We remove the universal quantifier from the conclusion, moving
1527 the bound variable~\isa{y} into the subgoal. But note that it is still
1530 \isacommand{apply}\ (rule\ allI)\isanewline
1531 \ 1.\ \isasymAnd y.\ \isasymforall y.\ R\ y\ y\ \isasymLongrightarrow \ R\ ?x\ y%
1533 Finally, we try to apply our reflexivity assumption. We obtain a
1534 new assumption whose identical placeholders may be replaced by
1535 any term involving~\isa{y}.
1537 \isacommand{apply}\ (drule\ spec)\isanewline
1538 \ 1.\ \isasymAnd y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y
1540 This subgoal can only be proved by putting \isa{y} for all the placeholders,
1541 making the assumption and conclusion become \isa{R\ y\ y}. Isabelle can
1542 replace \isa{?z2~y} by \isa{y}; this involves instantiating
1543 \isa{?z2} to the identity function. But, just as two steps earlier,
1544 Isabelle refuses to substitute~\isa{y} for~\isa{?x}.
1545 This example is typical of how Isabelle enforces sound quantifier reasoning.
1546 \index{proofs!examples of failing|)}
1548 \section{Proving Theorems Using the {\tt\slshape blast} Method}
1550 \index{*blast (method)|(}%
1551 It is hard to prove many theorems using the methods
1552 described above. A proof may be hundreds of steps long. You
1553 may need to search among different ways of proving certain
1554 subgoals. Often a choice that proves one subgoal renders another
1555 impossible to prove. There are further complications that we have not
1556 discussed, concerning negation and disjunction. Isabelle's
1557 \textbf{classical reasoner} is a family of tools that perform such
1558 proofs automatically. The most important of these is the
1561 In this section, we shall first see how to use the classical
1562 reasoner in its default mode and then how to insert additional
1563 rules, enabling it to work in new problem domains.
1565 We begin with examples from pure predicate logic. The following
1566 example is known as Andrew's challenge. Peter Andrews designed
1567 it to be hard to prove by automatic means.
1568 It is particularly hard for a resolution prover, where
1569 converting the nested biconditionals to
1570 clause form produces a combinatorial
1571 explosion~\cite{pelletier86}. However, the
1572 \isa{blast} method proves it in a fraction of a second.
1575 "(({\isasymexists}x.\
1579 (({\isasymexists}x.\
1580 q(x))=({\isasymforall}y.\
1582 \ \ =\ \ \ \ \isanewline
1584 (({\isasymexists}x.\
1586 q(x){=}q(y))\ =\ (({\isasymexists}x.\ p(x))=({\isasymforall}y.\ q(y))))"\isanewline
1587 \isacommand{by}\ blast
1589 The next example is a logic problem composed by Lewis Carroll.
1590 The \isa{blast} method finds it trivial. Moreover, it turns out
1591 that not all of the assumptions are necessary. We can
1592 experiment with variations of this formula and see which ones
1596 "({\isasymforall}x.\
1597 honest(x)\ \isasymand\
1598 industrious(x)\ \isasymlongrightarrow\
1600 \isasymand\ \ \isanewline
1601 \ \ \ \ \ \ \ \ \isasymnot\ ({\isasymexists}x.\
1602 grocer(x)\ \isasymand\
1604 \isasymand\ \isanewline
1605 \ \ \ \ \ \ \ \ ({\isasymforall}x.\
1606 industrious(x)\ \isasymand\
1607 grocer(x)\ \isasymlongrightarrow\
1609 \isasymand\ \isanewline
1610 \ \ \ \ \ \ \ \ ({\isasymforall}x.\
1611 cyclist(x)\ \isasymlongrightarrow\
1613 \isasymand\ \isanewline
1614 \ \ \ \ \ \ \ \ ({\isasymforall}x.\
1615 {\isasymnot}healthy(x)\ \isasymand\
1616 cyclist(x)\ \isasymlongrightarrow\
1617 {\isasymnot}honest(x))\
1619 \ \ \ \ \ \ \ \ \isasymlongrightarrow\
1621 grocer(x)\ \isasymlongrightarrow\
1622 {\isasymnot}cyclist(x))"\isanewline
1623 \isacommand{by}\ blast
1625 The \isa{blast} method is also effective for set theory, which is
1626 described in the next chapter. The formula below may look horrible, but
1627 the \isa{blast} method proves it in milliseconds.
1629 \isacommand{lemma}\ "({\isasymUnion}i{\isasymin}I.\ A(i))\ \isasyminter\ ({\isasymUnion}j{\isasymin}J.\ B(j))\ =\isanewline
1630 \ \ \ \ \ \ \ \ ({\isasymUnion}i{\isasymin}I.\ {\isasymUnion}j{\isasymin}J.\ A(i)\ \isasyminter\ B(j))"\isanewline
1631 \isacommand{by}\ blast
1634 Few subgoals are couched purely in predicate logic and set theory.
1635 We can extend the scope of the classical reasoner by giving it new rules.
1636 Extending it effectively requires understanding the notions of
1637 introduction, elimination and destruction rules. Moreover, there is a
1638 distinction between safe and unsafe rules. A
1639 \textbf{safe}\indexbold{safe rules} rule is one that can be applied
1640 backwards without losing information; an
1641 \textbf{unsafe}\indexbold{unsafe rules} rule loses information, perhaps
1642 transforming the subgoal into one that cannot be proved. The safe/unsafe
1643 distinction affects the proof search: if a proof attempt fails, the
1644 classical reasoner backtracks to the most recent unsafe rule application
1645 and makes another choice.
1647 An important special case avoids all these complications. A logical
1648 equivalence, which in higher-order logic is an equality between
1649 formulas, can be given to the classical
1650 reasoner and simplifier by using the attribute \attrdx{iff}. You
1651 should do so if the right hand side of the equivalence is
1652 simpler than the left-hand side.
1654 For example, here is a simple fact about list concatenation.
1655 The result of appending two lists is empty if and only if both
1656 of the lists are themselves empty. Obviously, applying this equivalence
1657 will result in a simpler goal. When stating this lemma, we include
1658 the \attrdx{iff} attribute. Once we have proved the lemma, Isabelle
1659 will make it known to the classical reasoner (and to the simplifier).
1662 [iff]:\ "(xs{\isacharat}ys\ =\ [])\ =\
1663 (xs=[]\ \isasymand\ ys=[])"\isanewline
1664 \isacommand{apply}\ (induct_tac\ xs)\isanewline
1665 \isacommand{apply}\ (simp_all)\isanewline
1669 This fact about multiplication is also appropriate for
1670 the \attrdx{iff} attribute:
1672 (\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
1674 A product is zero if and only if one of the factors is zero. The
1675 reasoning involves a disjunction. Proving new rules for
1676 disjunctive reasoning is hard, but translating to an actual disjunction
1677 works: the classical reasoner handles disjunction properly.
1679 In more detail, this is how the \attrdx{iff} attribute works. It converts
1680 the equivalence $P=Q$ to a pair of rules: the introduction
1681 rule $Q\Imp P$ and the destruction rule $P\Imp Q$. It gives both to the
1682 classical reasoner as safe rules, ensuring that all occurrences of $P$ in
1683 a subgoal are replaced by~$Q$. The simplifier performs the same
1684 replacement, since \isa{iff} gives $P=Q$ to the
1687 Classical reasoning is different from
1688 simplification. Simplification is deterministic. It applies rewrite rules
1689 repeatedly, as long as possible, transforming a goal into another goal. Classical
1690 reasoning uses search and backtracking in order to prove a goal outright.%
1691 \index{*blast (method)|)}%
1694 \section{Other Classical Reasoning Methods}
1696 The \isa{blast} method is our main workhorse for proving theorems
1697 automatically. Other components of the classical reasoner interact
1698 with the simplifier. Still others perform classical reasoning
1699 to a limited extent, giving the user fine control over the proof.
1701 Of the latter methods, the most useful is
1704 all obvious reasoning steps without splitting the goal into multiple
1705 parts. It does not apply unsafe rules that could render the
1706 goal unprovable. By performing the obvious
1707 steps, \isa{clarify} lays bare the difficult parts of the problem,
1708 where human intervention is necessary.
1710 For example, the following conjecture is false:
1712 \isacommand{lemma}\ "({\isasymforall}x.\ P\ x)\ \isasymand\
1713 ({\isasymexists}x.\ Q\ x)\ \isasymlongrightarrow\ ({\isasymforall}x.\ P\ x\
1714 \isasymand\ Q\ x)"\isanewline
1715 \isacommand{apply}\ clarify
1717 The \isa{blast} method would simply fail, but \isa{clarify} presents
1718 a subgoal that helps us see why we cannot continue the proof.
1720 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk{\isasymforall}x.\ P\ x;\ Q\
1721 xa\isasymrbrakk\ \isasymLongrightarrow\ P\ x\ \isasymand\ Q\ x
1723 The proof must fail because the assumption \isa{Q\ xa} and conclusion \isa{Q\ x}
1724 refer to distinct bound variables. To reach this state, \isa{clarify} applied
1725 the introduction rules for \isa{\isasymlongrightarrow} and \isa{\isasymforall}
1726 and the elimination rule for \isa{\isasymand}. It did not apply the introduction
1727 rule for \isa{\isasymand} because of its policy never to split goals.
1729 Also available is \methdx{clarsimp}, a method
1730 that interleaves \isa{clarify} and \isa{simp}. Also there is \methdx{safe},
1731 which like \isa{clarify} performs obvious steps but even applies those that
1734 The \methdx{force} method applies the classical
1735 reasoner and simplifier to one goal.
1736 Unless it can prove the goal, it fails. Contrast
1737 that with the \isa{auto} method, which also combines classical reasoning
1738 with simplification. The latter's purpose is to prove all the
1739 easy subgoals and parts of subgoals. Unfortunately, it can produce
1740 large numbers of new subgoals; also, since it proves some subgoals
1741 and splits others, it obscures the structure of the proof tree.
1742 The \isa{force} method does not have these drawbacks. Another
1743 difference: \isa{force} tries harder than {\isa{auto}} to prove
1744 its goal, so it can take much longer to terminate.
1746 Older components of the classical reasoner have largely been
1747 superseded by \isa{blast}, but they still have niche applications.
1748 Most important among these are \isa{fast} and \isa{best}. While \isa{blast}
1749 searches for proofs using a built-in first-order reasoner, these
1750 earlier methods search for proofs using standard Isabelle inference.
1751 That makes them slower but enables them to work in the
1752 presence of the more unusual features of Isabelle rules, such
1753 as type classes and function unknowns. For example, recall the introduction rule
1754 for Hilbert's $\varepsilon$-operator:
1756 ?P\ ?x\ \isasymLongrightarrow\ ?P\ (SOME\ x.\ ?P x)
1760 The repeated occurrence of the variable \isa{?P} makes this rule tricky
1761 to apply. Consider this contrived example:
1763 \isacommand{lemma}\ "\isasymlbrakk Q\ a;\ P\ a\isasymrbrakk\isanewline
1764 \ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ P\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)\
1765 \isasymand\ Q\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)"\isanewline
1766 \isacommand{apply}\ (rule\ someI)
1769 We can apply rule \isa{someI} explicitly. It yields the
1772 \ 1.\ \isasymlbrakk Q\ a;\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P\ ?x\
1775 The proof from this point is trivial. Could we have
1776 proved the theorem with a single command? Not using \isa{blast}: it
1777 cannot perform the higher-order unification needed here. The
1778 \methdx{fast} method succeeds:
1780 \isacommand{apply}\ (fast\ intro!:\ someI)
1783 The \methdx{best} method is similar to
1784 \isa{fast} but it uses a best-first search instead of depth-first search.
1785 Accordingly, it is slower but is less susceptible to divergence.
1786 Transitivity rules usually cause \isa{fast} to loop where \isa{best}
1789 Here is a summary of the classical reasoning methods:
1791 \item \methdx{blast} works automatically and is the fastest
1793 \item \methdx{clarify} and \methdx{clarsimp} perform obvious steps without
1794 splitting the goal; \methdx{safe} even splits goals
1796 \item \methdx{force} uses classical reasoning and simplification to prove a goal;
1797 \methdx{auto} is similar but leaves what it cannot prove
1799 \item \methdx{fast} and \methdx{best} are legacy methods that work well with rules
1800 involving unusual features
1802 A table illustrates the relationships among four of these methods.
1804 \begin{tabular}{r|l|l|}
1805 & no split & split \\ \hline
1806 no simp & \methdx{clarify} & \methdx{safe} \\ \hline
1807 simp & \methdx{clarsimp} & \methdx{auto} \\ \hline
1812 \section{Forward Proof: Transforming Theorems}\label{sec:forward}
1814 \index{forward proof|(}%
1815 Forward proof means deriving new facts from old ones. It is the
1816 most fundamental type of proof. Backward proof, by working from goals to
1817 subgoals, can help us find a difficult proof. But it is
1818 not always the best way of presenting the proof thus found. Forward
1819 proof is particularly good for reasoning from the general
1820 to the specific. For example, consider this distributive law for
1821 the greatest common divisor:
1822 \[ k\times\gcd(m,n) = \gcd(k\times m,k\times n)\]
1824 Putting $m=1$ we get (since $\gcd(1,n)=1$ and $k\times1=k$)
1825 \[ k = \gcd(k,k\times n)\]
1826 We have derived a new fact; if re-oriented, it might be
1827 useful for simplification. After re-orienting it and putting $n=1$, we
1828 derive another useful law:
1830 Substituting values for variables --- instantiation --- is a forward step.
1831 Re-orientation works by applying the symmetry of equality to
1832 an equation, so it too is a forward step.
1834 \subsection{Modifying a Theorem using {\tt\slshape of}, {\tt\slshape where}
1835 and {\tt\slshape THEN}}
1839 Let us reproduce our examples in Isabelle. Recall that in
1840 {\S}\ref{sec:recdef-simplification} we declared the recursive function
1841 \isa{gcd}:\index{*gcd (constant)|(}
1843 \isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline
1844 \isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n))"\isanewline
1845 \ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))"
1848 From this definition, it is possible to prove the distributive law.
1849 That takes us to the starting point for our example.
1851 ?k\ *\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ *\ ?m,\ ?k\ *\ ?n)
1852 \rulename{gcd_mult_distrib2}
1855 The first step in our derivation is to replace \isa{?m} by~1. We instantiate the
1856 theorem using~\attrdx{of}, which identifies variables in order of their
1857 appearance from left to right. In this case, the variables are \isa{?k}, \isa{?m}
1858 and~\isa{?n}. So, the expression
1859 \hbox{\texttt{[of k 1]}} replaces \isa{?k} by~\isa{k} and \isa{?m}
1862 \isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1]
1865 The keyword \commdx{lemmas} declares a new theorem, which can be derived
1866 from an existing one using attributes such as \isa{[of~k~1]}.
1868 \isa{thm gcd_mult_0}
1869 displays the result:
1871 \ \ \ \ \ k\ *\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ *\ 1,\ k\ *\ ?n)
1873 Something is odd: \isa{k} is an ordinary variable, while \isa{?n}
1874 is schematic. We did not specify an instantiation
1875 for \isa{?n}. In its present form, the theorem does not allow
1876 substitution for \isa{k}. One solution is to avoid giving an instantiation for
1877 \isa{?k}: instead of a term we can put an underscore~(\isa{_}). For example,
1879 \ \ \ \ \ gcd_mult_distrib2\ [of\ _\ 1]
1881 replaces \isa{?m} by~\isa{1} but leaves \isa{?k} unchanged.
1883 An equivalent solution is to use the attribute \isa{where}.
1885 \ \ \ \ \ gcd\_mult\_distrib2\ [where\ m=1]
1887 While \isa{of} refers to
1888 variables by their position, \isa{where} refers to variables by name. Multiple
1889 instantiations are separated by~\isa{and}, as in this example:
1891 \ \ \ \ \ gcd\_mult\_distrib2\ [where\ m=1\ and\ k=1]
1894 We now continue the present example with the version of \isa{gcd_mult_0}
1895 shown above, which has \isa{k} instead of \isa{?k}.
1896 Once we have replaced \isa{?m} by~1, we must next simplify
1897 the theorem \isa{gcd_mult_0}, performing the steps
1898 $\gcd(1,n)=1$ and $k\times1=k$. The \attrdx{simplified}
1899 attribute takes a theorem
1900 and returns the result of simplifying it, with respect to the default
1901 simplification rules:
1903 \isacommand{lemmas}\ gcd_mult_1\ =\ gcd_mult_0\
1907 Again, we display the resulting theorem:
1909 \ \ \ \ \ k\ =\ gcd\ (k,\ k\ *\ ?n)
1912 To re-orient the equation requires the symmetry rule:
1915 \isasymLongrightarrow\ ?t\ =\
1919 The following declaration gives our equation to \isa{sym}:
1921 \ \ \ \isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_1\ [THEN\ sym]
1926 \ \ \ \ \ gcd\ (k,\ k\ *\ ?n)\ =\ k%
1928 \isa{THEN~sym}\indexbold{*THEN (attribute)} gives the current theorem to the
1929 rule \isa{sym} and returns the resulting conclusion. The effect is to
1930 exchange the two operands of the equality. Typically \isa{THEN} is used
1931 with destruction rules. Also useful is \isa{THEN~spec}, which removes the
1932 quantifier from a theorem of the form $\forall x.\,P$, and \isa{THEN~mp},
1933 which converts the implication $P\imp Q$ into the rule
1934 $\vcenter{\infer{Q}{P}}$. Similar to \isa{mp} are the following two rules,
1935 which extract the two directions of reasoning about a boolean equivalence:
1937 \isasymlbrakk?Q\ =\ ?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
1940 \isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
1944 Normally we would never name the intermediate theorems
1945 such as \isa{gcd_mult_0} and \isa{gcd_mult_1} but would combine
1946 the three forward steps:
1948 \isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]%
1950 The directives, or attributes, are processed from left to right. This
1951 declaration of \isa{gcd_mult} is equivalent to the
1954 Such declarations can make the proof script hard to read. Better
1955 is to state the new lemma explicitly and to prove it using a single
1956 \isa{rule} method whose operand is expressed using forward reasoning:
1958 \isacommand{lemma}\ gcd_mult\
1960 "gcd(k,\ k*n)\ =\ k"\isanewline
1961 \isacommand{by}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym])
1963 Compared with the previous proof of \isa{gcd_mult}, this
1964 version shows the reader what has been proved. Also, the result will be processed
1965 in the normal way. In particular, Isabelle generalizes over all variables: the
1966 resulting theorem will have {\isa{?k}} instead of {\isa{k}}.
1968 At the start of this section, we also saw a proof of $\gcd(k,k)=k$. Here
1969 is the Isabelle version:\index{*gcd (constant)|)}
1971 \isacommand{lemma}\ gcd_self\ [simp]:\ "gcd(k,k)\ =\ k"\isanewline
1972 \isacommand{by}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified])
1976 To give~\isa{of} a nonatomic term, enclose it in quotation marks, as in
1977 \isa{[of "k*m"]}. The term must not contain unknowns: an
1979 \isa{[of "?k*m"]} will be rejected.
1982 %Answer is now included in that section! Is a modified version of this
1983 % exercise worth including? E.g. find a difference between the two ways
1986 %In {\S}\ref{sec:subst} the method \isa{subst\ mult_commute} was applied. How
1987 %can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}?
1988 %% answer rule (mult_commute [THEN ssubst])
1991 \subsection{Modifying a Theorem using {\tt\slshape OF}}
1993 \index{*OF (attribute)|(}%
1994 Recall that \isa{of} generates an instance of a
1995 rule by specifying values for its variables. Analogous is \isa{OF}, which
1996 generates an instance of a rule by specifying facts for its premises.
1998 We again need the divides relation\index{divides relation} of number theory, which
1999 as we recall is defined by
2001 ?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
2005 Suppose, for example, that we have proved the following rule.
2006 It states that if $k$ and $n$ are relatively prime
2007 and if $k$ divides $m\times n$ then $k$ divides $m$.
2009 \isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\
2010 \isasymLongrightarrow\ ?k\ dvd\ ?m
2011 \rulename{relprime_dvd_mult}
2013 We can use \isa{OF} to create an instance of this rule.
2015 prove an instance of its first premise:
2017 \isacommand{lemma}\ relprime_20_81:\ "gcd(20,81)\ =\ 1"\isanewline
2018 \isacommand{by}\ (simp\ add:\ gcd.simps)
2020 We have evaluated an application of the \isa{gcd} function by
2021 simplification. Expression evaluation involving recursive functions is not
2022 guaranteed to terminate, and it can be slow; Isabelle
2023 performs arithmetic by rewriting symbolic bit strings. Here,
2024 however, the simplification takes less than one second. We can
2025 give this new lemma to \isa{OF}. The expression
2027 \ \ \ \ \ relprime_dvd_mult [OF relprime_20_81]
2031 \ \ \ \ \ 20\ dvd\ (?m\ *\ 81)\ \isasymLongrightarrow\ 20\ dvd\ ?m%
2034 \isa{OF} takes any number of operands. Consider
2035 the following facts about the divides relation:
2037 \isasymlbrakk?k\ dvd\ ?m;\
2038 ?k\ dvd\ ?n\isasymrbrakk\
2039 \isasymLongrightarrow\ ?k\ dvd\
2041 \rulename{dvd_add}\isanewline
2045 Let us supply \isa{dvd_refl} for each of the premises of \isa{dvd_add}:
2047 \ \ \ \ \ dvd_add [OF dvd_refl dvd_refl]
2049 Here is the theorem that we have expressed:
2051 \ \ \ \ \ ?k\ dvd\ (?k\ +\ ?k)
2053 As with \isa{of}, we can use the \isa{_} symbol to leave some positions
2056 \ \ \ \ \ dvd_add [OF _ dvd_refl]
2060 \ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ ?m\ +\ ?k
2063 You may have noticed that \isa{THEN} and \isa{OF} are based on
2064 the same idea, namely to combine two rules. They differ in the
2065 order of the combination and thus in their effect. We use \isa{THEN}
2066 typically with a destruction rule to extract a subformula of the current
2067 theorem. We use \isa{OF} with a list of facts to generate an instance of
2068 the current theorem.%
2069 \index{*OF (attribute)|)}
2071 Here is a summary of some primitives for forward reasoning:
2073 \item \attrdx{of} instantiates the variables of a rule to a list of terms
2074 \item \attrdx{OF} applies a rule to a list of theorems
2075 \item \attrdx{THEN} gives a theorem to a named rule and returns the
2077 %\item \attrdx{rule_format} puts a theorem into standard form
2078 % by removing \isa{\isasymlongrightarrow} and~\isa{\isasymforall}
2079 \item \attrdx{simplified} applies the simplifier to a theorem
2080 \item \isacommand{lemmas} assigns a name to the theorem produced by the
2085 \section{Forward Reasoning in a Backward Proof}
2087 We have seen that the forward proof directives work well within a backward
2088 proof. There are many ways to achieve a forward style using our existing
2089 proof methods. We shall also meet some new methods that perform forward
2092 The methods \isa{drule}, \isa{frule}, \isa{drule_tac}, etc.,
2093 reason forward from a subgoal. We have seen them already, using rules such as
2095 \isa{spec} to operate on formulae. They can also operate on terms, using rules
2098 x\ =\ y\ \isasymLongrightarrow \ f\ x\ =\ f\ y%
2099 \rulenamedx{arg_cong}\isanewline
2100 i\ \isasymle \ j\ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ k%
2101 \rulename{mult_le_mono1}
2104 For example, let us prove a fact about divisibility in the natural numbers:
2106 \isacommand{lemma}\ "2\ \isasymle \ u\ \isasymLongrightarrow \ u*m\ \isasymnoteq
2107 \ Suc(u*n)"\isanewline
2108 \isacommand{apply}\ (intro\ notI)\isanewline
2109 \ 1.\ \isasymlbrakk 2\ \isasymle \ u;\ u\ *\ m\ =\ Suc\ (u\ *\ n)\isasymrbrakk \ \isasymLongrightarrow \ False%
2112 The key step is to apply the function \ldots\isa{mod\ u} to both sides of the
2114 \isa{u*m\ =\ Suc(u*n)}:\index{*drule_tac (method)}
2116 \isacommand{apply}\ (drule_tac\ f="\isasymlambda x.\ x\ mod\ u"\ \isakeyword{in}\
2117 arg_cong)\isanewline
2118 \ 1.\ \isasymlbrakk 2\ \isasymle \ u;\ u\ *\ m\ mod\ u\ =\ Suc\ (u\ *\ n)\ mod\
2119 u\isasymrbrakk \ \isasymLongrightarrow \ False
2122 Simplification reduces the left side to 0 and the right side to~1, yielding the
2123 required contradiction.
2125 \isacommand{apply}\ (simp\ add:\ mod_Suc)\isanewline
2129 Our proof has used a fact about remainder:
2131 Suc\ m\ mod\ n\ =\isanewline
2132 (if\ Suc\ (m\ mod\ n)\ =\ n\ then\ 0\ else\ Suc\ (m\ mod\ n))
2136 \subsection{The Method {\tt\slshape insert}}
2138 \index{*insert (method)|(}%
2139 The \isa{insert} method
2140 inserts a given theorem as a new assumption of the current subgoal. This
2141 already is a forward step; moreover, we may (as always when using a
2143 \isa{of}, \isa{THEN} and other directives. The new assumption can then
2144 be used to help prove the subgoal.
2146 For example, consider this theorem about the divides relation. The first
2147 proof step inserts the distributive law for
2148 \isa{gcd}. We specify its variables as shown.
2151 relprime_dvd_mult:\isanewline
2152 \ \ \ \ \ \ \ "\isasymlbrakk gcd(k,n){=}1;\ k\ dvd\ m*n\isasymrbrakk\
2153 \isasymLongrightarrow\ k\ dvd\
2155 \isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\
2158 In the resulting subgoal, note how the equation has been
2161 \ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ m\ *\ n{;}\ m\ *\ gcd\
2163 =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
2164 \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
2166 The next proof step utilizes the assumption \isa{gcd(k,n)\ =\ 1}:
2168 \isacommand{apply}(simp)\isanewline
2169 \ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\
2171 \ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
2172 \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
2174 Simplification has yielded an equation for~\isa{m}. The rest of the proof
2178 Here is another demonstration of \isa{insert}. Division and
2179 remainder obey a well-known law:
2181 (?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m
2182 \rulename{mod_div_equality}
2185 We refer to this law explicitly in the following proof:
2187 \isacommand{lemma}\ div_mult_self_is_m:\ \isanewline
2188 \ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m*n)\ div\ n\ =\
2189 (m::nat)"\isanewline
2190 \isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m*n"\ n])\isanewline
2191 \isacommand{apply}\ (simp)\isanewline
2194 The first step inserts the law, specifying \isa{m*n} and
2195 \isa{n} for its variables. Notice that non-trivial expressions must be
2196 enclosed in quotation marks. Here is the resulting
2197 subgoal, with its new assumption:
2199 %0\ \isacharless\ n\ \isasymLongrightarrow\ (m\
2200 %*\ n)\ div\ n\ =\ m\isanewline
2201 \ 1.\ \isasymlbrakk0\ \isacharless\
2202 n;\ \ (m\ *\ n)\ div\ n\ *\ n\ +\ (m\ *\ n)\ mod\ n\
2203 =\ m\ *\ n\isasymrbrakk\isanewline
2204 \ \ \ \ \isasymLongrightarrow\ (m\ *\ n)\ div\ n\
2207 Simplification reduces \isa{(m\ *\ n)\ mod\ n} to zero.
2208 Then it cancels the factor~\isa{n} on both
2209 sides of the equation \isa{(m\ *\ n)\ div\ n\ *\ n\ =\ m\ *\ n}, proving the
2213 Any unknowns in the theorem given to \methdx{insert} will be universally
2214 quantified in the new assumption.
2216 \index{*insert (method)|)}
2218 \subsection{The Method {\tt\slshape subgoal_tac}}
2220 \index{*subgoal_tac (method)}%
2221 A related method is \isa{subgoal_tac}, but instead
2222 of inserting a theorem as an assumption, it inserts an arbitrary formula.
2223 This formula must be proved later as a separate subgoal. The
2224 idea is to claim that the formula holds on the basis of the current
2225 assumptions, to use this claim to complete the proof, and finally
2226 to justify the claim. It gives the proof
2227 some structure. If you find yourself generating a complex assumption by a
2228 long series of forward steps, consider using \isa{subgoal_tac} instead: you can
2229 state the formula you are aiming for, and perhaps prove it automatically.
2231 Look at the following example.
2233 \isacommand{lemma}\ "\isasymlbrakk(z::int)\ <\ 37;\ 66\ <\ 2*z;\ z*z\
2234 \isasymnoteq\ 1225;\ Q(34);\ Q(36)\isasymrbrakk\isanewline
2235 \ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ Q(z)"\isanewline
2236 \isacommand{apply}\ (subgoal_tac\ "z\ =\ 34\ \isasymor\ z\ =\
2238 \isacommand{apply}\ blast\isanewline
2239 \isacommand{apply}\ (subgoal_tac\ "z\ \isasymnoteq\ 35")\isanewline
2240 \isacommand{apply}\ arith\isanewline
2241 \isacommand{apply}\ force\isanewline
2244 The first assumption tells us
2245 that \isa{z} is no greater than~36. The second tells us that \isa{z}
2246 is at least~34. The third assumption tells us that \isa{z} cannot be 35, since
2247 $35\times35=1225$. So \isa{z} is either 34 or~36, and since \isa{Q} holds for
2248 both of those values, we have the conclusion.
2250 The Isabelle proof closely follows this reasoning. The first
2251 step is to claim that \isa{z} is either 34 or 36. The resulting proof
2252 state gives us two subgoals:
2254 %\isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\
2255 %Q\ 34;\ Q\ 36\isasymrbrakk\ \isasymLongrightarrow\ Q\ z\isanewline
2256 \ 1.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36;\isanewline
2257 \ \ \ \ \ z\ =\ 34\ \isasymor\ z\ =\ 36\isasymrbrakk\isanewline
2258 \ \ \ \ \isasymLongrightarrow\ Q\ z\isanewline
2259 \ 2.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36\isasymrbrakk\isanewline
2260 \ \ \ \ \isasymLongrightarrow\ z\ =\ 34\ \isasymor\ z\ =\ 36
2262 The first subgoal is trivial (\isa{blast}), but for the second Isabelle needs help to eliminate
2264 \isa{z}=35. The second invocation of {\isa{subgoal_tac}} leaves two
2267 \ 1.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\
2268 1225;\ Q\ 34;\ Q\ 36;\isanewline
2269 \ \ \ \ \ z\ \isasymnoteq\ 35\isasymrbrakk\isanewline
2270 \ \ \ \ \isasymLongrightarrow\ z\ =\ 34\ \isasymor\ z\ =\ 36\isanewline
2271 \ 2.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36\isasymrbrakk\isanewline
2272 \ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ 35
2275 Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic
2276 (\isa{arith}). For the second subgoal we apply the method \isa{force},
2277 which proceeds by assuming that \isa{z}=35 and arriving at a contradiction.
2281 Summary of these methods:
2283 \item \methdx{insert} adds a theorem as a new assumption
2284 \item \methdx{subgoal_tac} adds a formula as a new assumption and leaves the
2285 subgoal of proving that formula
2287 \index{forward proof|)}
2290 \section{Managing Large Proofs}
2292 Naturally you should try to divide proofs into manageable parts. Look for lemmas
2293 that can be proved separately. Sometimes you will observe that they are
2294 instances of much simpler facts. On other occasions, no lemmas suggest themselves
2295 and you are forced to cope with a long proof involving many subgoals.
2297 \subsection{Tacticals, or Control Structures}
2299 \index{tacticals|(}%
2300 If the proof is long, perhaps it at least has some regularity. Then you can
2301 express it more concisely using \textbf{tacticals}, which provide control
2302 structures. Here is a proof (it would be a one-liner using
2303 \isa{blast}, but forget that) that contains a series of repeated
2307 \isacommand{lemma}\ "\isasymlbrakk P\isasymlongrightarrow Q;\
2308 Q\isasymlongrightarrow R;\ R\isasymlongrightarrow S;\ P\isasymrbrakk \
2309 \isasymLongrightarrow \ S"\isanewline
2310 \isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
2311 \isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
2312 \isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
2313 \isacommand{apply}\ (assumption)\isanewline
2317 Each of the three identical commands finds an implication and proves its
2318 antecedent by assumption. The first one finds \isa{P\isasymlongrightarrow Q} and
2319 \isa{P}, concluding~\isa{Q}; the second one concludes~\isa{R} and the third one
2320 concludes~\isa{S}. The final step matches the assumption \isa{S} with the goal to
2323 Suffixing a method with a plus sign~(\isa+)\index{*"+ (tactical)}
2324 expresses one or more repetitions:
2326 \isacommand{lemma}\ "\isasymlbrakk P\isasymlongrightarrow Q;\ Q\isasymlongrightarrow R;\ R\isasymlongrightarrow S;\ P\isasymrbrakk \ \isasymLongrightarrow \ S"\isanewline
2327 \isacommand{by}\ (drule\ mp,\ assumption)+
2330 Using \isacommand{by} takes care of the final use of \isa{assumption}. The new
2331 proof is more concise. It is also more general: the repetitive method works
2332 for a chain of implications having any length, not just three.
2334 Choice is another control structure. Separating two methods by a vertical
2335 % we must use ?? rather than "| as the sorting item because somehow the presence
2336 % of | (even quoted) stops hyperref from putting |hyperpage at the end of the index
2338 bar~(\isa|)\index{??@\texttt{"|} (tactical)} gives the effect of applying the
2339 first method, and if that fails, trying the second. It can be combined with
2340 repetition, when the choice must be made over and over again. Here is a chain of
2341 implications in which most of the antecedents are proved by assumption, but one is
2342 proved by arithmetic:
2344 \isacommand{lemma}\ "\isasymlbrakk Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ x<5\isasymlongrightarrow P;\
2345 Suc\ x\ <\ 5\isasymrbrakk \ \isasymLongrightarrow \ R"\ \isanewline
2346 \isacommand{by}\ (drule\ mp,\ (assumption|arith))+
2349 method can prove $x<5$ from $x+1<5$, but it cannot duplicate the effect of
2350 \isa{assumption}. Therefore, we combine these methods using the choice
2353 A postfixed question mark~(\isa?)\index{*"? (tactical)} expresses zero or one
2354 repetitions of a method. It can also be viewed as the choice between executing a
2355 method and doing nothing. It is useless at top level but can be valuable
2356 within other control structures; for example,
2357 \isa{($m$+)?} performs zero or more repetitions of method~$m$.%
2361 \subsection{Subgoal Numbering}
2363 Another problem in large proofs is contending with huge
2364 subgoals or many subgoals. Induction can produce a proof state that looks
2367 \ 1.\ bigsubgoal1\isanewline
2368 \ 2.\ bigsubgoal2\isanewline
2369 \ 3.\ bigsubgoal3\isanewline
2370 \ 4.\ bigsubgoal4\isanewline
2371 \ 5.\ bigsubgoal5\isanewline
2374 If each \isa{bigsubgoal} is 15 lines or so, the proof state will be too big to
2375 scroll through. By default, Isabelle displays at most 10 subgoals. The
2376 \commdx{pr} command lets you change this limit:
2378 \isacommand{pr}\ 2\isanewline
2379 \ 1.\ bigsubgoal1\isanewline
2380 \ 2.\ bigsubgoal2\isanewline
2381 A total of 6 subgoals...
2385 All methods apply to the first subgoal.
2386 Sometimes, not only in a large proof, you may want to focus on some other
2387 subgoal. Then you should try the commands \isacommand{defer} or \isacommand{prefer}.
2389 In the following example, the first subgoal looks hard, while the others
2390 look as if \isa{blast} alone could prove them:
2392 \ 1.\ hard\isanewline
2393 \ 2.\ \isasymnot \ \isasymnot \ P\ \isasymLongrightarrow \ P\isanewline
2394 \ 3.\ Q\ \isasymLongrightarrow \ Q%
2397 The \commdx{defer} command moves the first subgoal into the last position.
2399 \isacommand{defer}\ 1\isanewline
2400 \ 1.\ \isasymnot \ \isasymnot \ P\ \isasymLongrightarrow \ P\isanewline
2401 \ 2.\ Q\ \isasymLongrightarrow \ Q\isanewline
2405 Now we apply \isa{blast} repeatedly to the easy subgoals:
2407 \isacommand{apply}\ blast+\isanewline
2410 Using \isacommand{defer}, we have cleared away the trivial parts of the proof so
2411 that we can devote attention to the difficult part.
2414 The \commdx{prefer} command moves the specified subgoal into the
2415 first position. For example, if you suspect that one of your subgoals is
2416 invalid (not a theorem), then you should investigate that subgoal first. If it
2417 cannot be proved, then there is no point in proving the other subgoals.
2419 \ 1.\ ok1\isanewline
2420 \ 2.\ ok2\isanewline
2424 We decide to work on the third subgoal.
2426 \isacommand{prefer}\ 3\isanewline
2427 \ 1.\ doubtful\isanewline
2428 \ 2.\ ok1\isanewline
2431 If we manage to prove \isa{doubtful}, then we can work on the other
2432 subgoals, confident that we are not wasting our time. Finally we revise the
2433 proof script to remove the \isacommand{prefer} command, since we needed it only to
2434 focus our exploration. The previous example is different: its use of
2435 \isacommand{defer} stops trivial subgoals from cluttering the rest of the
2436 proof. Even there, we should consider proving \isa{hard} as a preliminary
2437 lemma. Always seek ways to streamline your proofs.
2443 \item the control structures \isa+, \isa? and \isa| help express complicated proofs
2444 \item the \isacommand{pr} command can limit the number of subgoals to display
2445 \item the \isacommand{defer} and \isacommand{prefer} commands move a
2446 subgoal to the last or first position
2450 Explain the use of \isa? and \isa+ in this proof.
2452 \isacommand{lemma}\ "\isasymlbrakk P\isasymand Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ R"\isanewline
2453 \isacommand{by}\ (drule\ mp,\ (intro conjI)?,\ assumption+)+
2459 \section{Proving the Correctness of Euclid's Algorithm}
2460 \label{sec:proving-euclid}
2462 \index{Euclid's algorithm|(}\index{*gcd (constant)|(}\index{divides relation|(}%
2463 A brief development will demonstrate the techniques of this chapter,
2464 including \isa{blast} applied with additional rules. We shall also see
2465 \isa{case_tac} used to perform a Boolean case split.
2467 Let us prove that \isa{gcd} computes the greatest common
2468 divisor of its two arguments.
2470 We use induction: \isa{gcd.induct} is the
2471 induction rule returned by \isa{recdef}. We simplify using
2472 rules proved in {\S}\ref{sec:recdef-simplification}, since rewriting by the
2473 definition of \isa{gcd} can loop.
2475 \isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\
2478 The induction formula must be a conjunction. In the
2479 inductive step, each conjunct establishes the other.
2481 \isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline
2482 \ 1.\ \isasymAnd m\ n.\ n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
2483 \isaindent{\ 1.\ \isasymAnd m\ n.\ }gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand
2484 \ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\ n\isanewline
2485 \isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow\ gcd\ (m,\ n)\
2486 dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n%
2489 The conditional induction hypothesis suggests doing a case
2490 analysis on \isa{n=0}. We apply \methdx{case_tac} with type
2491 \isa{bool} --- and not with a datatype, as we have done until now. Since
2492 \isa{nat} is a datatype, we could have written
2493 \isa{case_tac~n} instead of \isa{case_tac~"n=0"}. However, the definition
2494 of \isa{gcd} makes a Boolean decision:
2496 \ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))"
2498 Proofs about a function frequently follow the function's definition, so we perform
2499 case analysis over the same formula.
2501 \isacommand{apply}\ (case_tac\ "n=0")\isanewline
2502 \ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
2503 \isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
2504 \isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline
2505 \isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ (m,\ n)\ dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n\isanewline
2506 \ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
2507 \isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
2508 \isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk
2510 \isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ (m,\ n)\ dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n%
2513 Simplification leaves one subgoal:
2515 \isacommand{apply}\ (simp_all)\isanewline
2516 \ 1.\ \isasymAnd m\ n.\ \isasymlbrakk 0\ <\ n;\isanewline
2517 \isaindent{\ 1.\ \isasymAnd m\ n.\ \ }gcd\ (n,\ m\ mod\ n)\ dvd\ n\
2518 \isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\
2519 n\isasymrbrakk \isanewline
2520 \isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ (n,\ m\ mod\ n)\ dvd\ m%
2523 Here, we can use \isa{blast}.
2524 One of the assumptions, the induction hypothesis, is a conjunction.
2525 The two divides relationships it asserts are enough to prove
2526 the conclusion, for we have the following theorem at our disposal:
2528 \isasymlbrakk?k\ dvd\ (?m\ mod\ ?n){;}\ ?k\ dvd\ ?n\isasymrbrakk\ \isasymLongrightarrow\ ?k\ dvd\ ?m%
2529 \rulename{dvd_mod_imp_dvd}
2532 This theorem can be applied in various ways. As an introduction rule, it
2533 would cause backward chaining from the conclusion (namely
2534 \isa{?k~dvd~?m}) to the two premises, which
2535 also involve the divides relation. This process does not look promising
2536 and could easily loop. More sensible is to apply the rule in the forward
2537 direction; each step would eliminate an occurrence of the \isa{mod} symbol, so the
2538 process must terminate.
2540 \isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline
2543 Attaching the \attrdx{dest} attribute to \isa{dvd_mod_imp_dvd} tells
2544 \isa{blast} to use it as destruction rule; that is, in the forward direction.
2547 We have proved a conjunction. Now, let us give names to each of the
2550 \isacommand{lemmas}\ gcd_dvd1\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct1]\isanewline
2551 \isacommand{lemmas}\ gcd_dvd2\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct2]%
2553 Here we see \commdx{lemmas}
2554 used with the \attrdx{iff} attribute, which supplies the new theorems to the
2555 classical reasoner and the simplifier. Recall that \attrdx{THEN} is
2556 frequently used with destruction rules; \isa{THEN conjunct1} extracts the
2557 first half of a conjunctive theorem. Given \isa{gcd_dvd_both} it yields
2559 \ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?m1
2561 The variable names \isa{?m1} and \isa{?n1} arise because
2562 Isabelle renames schematic variables to prevent
2563 clashes. The second \isacommand{lemmas} declaration yields
2565 \ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?n1
2569 To complete the verification of the \isa{gcd} function, we must
2570 prove that it returns the greatest of all the common divisors
2571 of its arguments. The proof is by induction, case analysis and simplification.
2573 \isacommand{lemma}\ gcd_greatest\
2574 [rule_format]:\isanewline
2575 \ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ \isasymlongrightarrow\
2579 The goal is expressed using HOL implication,
2580 \isa{\isasymlongrightarrow}, because the induction affects the two
2581 preconditions. The directive \isa{rule_format} tells Isabelle to replace
2582 each \isa{\isasymlongrightarrow} by \isa{\isasymLongrightarrow} before
2583 storing the eventual theorem. This directive can also remove outer
2584 universal quantifiers, converting the theorem into the usual format for
2585 inference rules. It can replace any series of applications of
2586 \isa{THEN} to the rules \isa{mp} and \isa{spec}. We did not have to
2589 \ \ \ \ \ \isacommand{lemma}\ gcd_greatest\
2590 [THEN mp, THEN mp]:\isanewline
2591 \ \ \ \ \ \ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\
2592 \isasymlongrightarrow\ k\ dvd\ gcd(m,n)"
2595 Because we are again reasoning about \isa{gcd}, we perform the same
2596 induction and case analysis as in the previous proof:
2597 \begingroup\samepage
2599 \isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline
2600 \isacommand{apply}\ (case_tac\ "n=0")\isanewline
2601 \ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\
2602 \isasymlongrightarrow \isanewline
2603 \isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline
2604 \isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline
2605 \isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n)\isanewline
2606 \ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
2607 \isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline
2608 \isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk
2610 \isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n)
2614 \noindent Simplification proves both subgoals.
2616 \isacommand{apply}\ (simp_all\ add:\ dvd_mod)\isanewline
2619 In the first, where \isa{n=0}, the implication becomes trivial: \isa{k\ dvd\
2620 gcd\ (m,\ n)} goes to~\isa{k\ dvd\ m}. The second subgoal is proved by
2621 an unfolding of \isa{gcd}, using this rule about divides:
2623 \isasymlbrakk ?f\ dvd\ ?m;\ ?f\ dvd\ ?n\isasymrbrakk \
2624 \isasymLongrightarrow \ ?f\ dvd\ ?m\ mod\ ?n%
2630 The facts proved above can be summarized as a single logical
2631 equivalence. This step gives us a chance to see another application
2634 \isacommand{theorem}\ gcd_greatest_iff\ [iff]:\isanewline
2635 \ \ \ \ \ \ \ \ \ "(k\ dvd\ gcd(m,n))\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\
2637 \isacommand{by}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans)
2639 This theorem concisely expresses the correctness of the \isa{gcd}
2641 We state it with the \isa{iff} attribute so that
2642 Isabelle can use it to remove some occurrences of \isa{gcd}.
2643 The theorem has a one-line
2644 proof using \isa{blast} supplied with two additional introduction
2645 rules. The exclamation mark
2646 ({\isa{intro}}{\isa{!}})\ signifies safe rules, which are
2647 applied aggressively. Rules given without the exclamation mark
2648 are applied reluctantly and their uses can be undone if
2649 the search backtracks. Here the unsafe rule expresses transitivity
2650 of the divides relation:
2652 \isasymlbrakk?m\ dvd\ ?n;\ ?n\ dvd\ ?p\isasymrbrakk\ \isasymLongrightarrow\ ?m\ dvd\ ?p%
2653 \rulename{dvd_trans}
2655 Applying \isa{dvd_trans} as
2656 an introduction rule entails a risk of looping, for it multiplies
2657 occurrences of the divides symbol. However, this proof relies
2658 on transitivity reasoning. The rule {\isa{gcd\_greatest}} is safe to apply
2659 aggressively because it yields simpler subgoals. The proof implicitly
2660 uses \isa{gcd_dvd1} and \isa{gcd_dvd2} as safe rules, because they were
2661 declared using \isa{iff}.%
2662 \index{Euclid's algorithm|)}\index{*gcd (constant)|)}\index{divides relation|)}