author  paulson 
Fri, 12 Jan 2001 17:59:37 +0100  
changeset 10887  7fb42b97413a 
parent 10854  d1ff1ff5c5ad 
child 10967  69937e62a28e 
permissions  rwrr 
10792  1 
% $Id$ 
10295  2 
\chapter{The Rules of the Game} 
3 
\label{chap:rules} 

4 

5 
Until now, we have proved everything using only induction and simplification. 

6 
Substantial proofs require more elaborate forms of inference. This chapter 

7 
outlines the concepts and techniques that underlie reasoning in Isabelle. The examples 

8 
are mainly drawn from predicate logic. The first examples in this 

9 
chapter will consist of detailed, lowlevel proof steps. Later, we shall 

10 
see how to automate such reasoning using the methods \isa{blast}, 

11 
\isa{auto} and others. 

12 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

13 
\section{Natural Deduction} 
10295  14 

15 
In Isabelle, proofs are constructed using inference rules. The 

16 
most familiar inference rule is probably \emph{modus ponens}: 

17 
\[ \infer{Q}{P\imp Q & P} \] 

18 
This rule says that from $P\imp Q$ and $P$ 

19 
we may infer~$Q$. 

20 

21 
%Early logical formalisms had this 

22 
%rule and at most one or two others, along with many complicated 

23 
%axioms. Any desired theorem could be obtained by applying \emph{modus 

24 
%ponens} or other rules to the axioms, but proofs were 

25 
%hard to find. For example, a standard inference system has 

26 
%these two axioms (amongst others): 

27 
%\begin{gather*} 

28 
% P\imp(Q\imp P) \tag{K}\\ 

29 
% (P\imp(Q\imp R))\imp ((P\imp Q)\imp(P\imp R)) \tag{S} 

30 
%\end{gather*} 

31 
%Try proving the trivial fact $P\imp P$ using these axioms and \emph{modus 

32 
%ponens}! 

33 

34 
\textbf{Natural deduction} is an attempt to formalize logic in a way 

35 
that mirrors human reasoning patterns. 

36 
% 

37 
%Instead of having a few 

38 
%inference rules and many axioms, it has many inference rules 

39 
%and few axioms. 

40 
% 

41 
For each logical symbol (say, $\conj$), there 

42 
are two kinds of rules: \textbf{introduction} and \textbf{elimination} rules. 

43 
The introduction rules allow us to infer this symbol (say, to 

44 
infer conjunctions). The elimination rules allow us to deduce 

45 
consequences from this symbol. Ideally each rule should mention 

46 
one symbol only. For predicate logic this can be 

47 
done, but when users define their own concepts they typically 

48 
have to refer to other symbols as well. It is best not be dogmatic. 

49 

50 
Natural deduction generally deserves its name. It is easy to use. Each 

51 
proof step consists of identifying the outermost symbol of a formula and 

52 
applying the corresponding rule. It creates new subgoals in 

53 
an obvious way from parts of the chosen formula. Expanding the 

54 
definitions of constants can blow up the goal enormously. Deriving natural 

55 
deduction rules for such constants lets us reason in terms of their key 

56 
properties, which might otherwise be obscured by the technicalities of its 

57 
definition. Natural deduction rules also lend themselves to automation. 

58 
Isabelle's 

59 
\textbf{classical reasoner} accepts any suitable collection of natural deduction 

60 
rules and uses them to search for proofs automatically. Isabelle is designed around 

61 
natural deduction and many of its tools use the terminology of introduction and 

62 
elimination rules. 

63 

64 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

65 
\section{Introduction Rules} 
10295  66 

67 
An \textbf{introduction} rule tells us when we can infer a formula 

68 
containing a specific logical symbol. For example, the conjunction 

69 
introduction rule says that if we have $P$ and if we have $Q$ then 

70 
we have $P\conj Q$. In a mathematics text, it is typically shown 

71 
like this: 

72 
\[ \infer{P\conj Q}{P & Q} \] 

73 
The rule introduces the conjunction 

74 
symbol~($\conj$) in its conclusion. Of course, in Isabelle proofs we 

75 
mainly reason backwards. When we apply this rule, the subgoal already has 

76 
the form of a conjunction; the proof step makes this conjunction symbol 

77 
disappear. 

78 

79 
In Isabelle notation, the rule looks like this: 

80 
\begin{isabelle} 

81 
\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulename{conjI} 

82 
\end{isabelle} 

83 
Carefully examine the syntax. The premises appear to the 

84 
left of the arrow and the conclusion to the right. The premises (if 

85 
more than one) are grouped using the fat brackets. The question marks 

86 
indicate \textbf{schematic variables} (also called \textbf{unknowns}): they may 

87 
be replaced by arbitrary formulas. If we use the rule backwards, Isabelle 

88 
tries to unify the current subgoal with the conclusion of the rule, which 

89 
has the form \isa{?P\ \isasymand\ ?Q}. (Unification is discussed below, 

90 
\S\ref{sec:unification}.) If successful, 

91 
it yields new subgoals given by the formulas assigned to 

92 
\isa{?P} and \isa{?Q}. 

93 

94 
The following trivial proof illustrates this point. 

95 
\begin{isabelle} 

10596  96 
\isacommand{lemma}\ conj_rule:\ "\isasymlbrakk P;\ 
10295  97 
Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ 
10301  98 
(Q\ \isasymand\ P)"\isanewline 
10295  99 
\isacommand{apply}\ (rule\ conjI)\isanewline 
100 
\ \isacommand{apply}\ assumption\isanewline 

101 
\isacommand{apply}\ (rule\ conjI)\isanewline 

102 
\ \isacommand{apply}\ assumption\isanewline 

103 
\isacommand{apply}\ assumption 

104 
\end{isabelle} 

105 
At the start, Isabelle presents 

106 
us with the assumptions (\isa{P} and~\isa{Q}) and with the goal to be proved, 

107 
\isa{P\ \isasymand\ 

108 
(Q\ \isasymand\ P)}. We are working backwards, so when we 

109 
apply conjunction introduction, the rule removes the outermost occurrence 

110 
of the \isa{\isasymand} symbol. To apply a rule to a subgoal, we apply 

10596  111 
the proof method \isa{rule}  here with {\isa{conjI}}, the conjunction 
10295  112 
introduction rule. 
113 
\begin{isabelle} 

10596  114 
%\isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\ 
10295  115 
%\isasymand\ P\isanewline 
10596  116 
\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline 
117 
\ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P 

10295  118 
\end{isabelle} 
119 
Isabelle leaves two new subgoals: the two halves of the original conjunction. 

120 
The first is simply \isa{P}, which is trivial, since \isa{P} is among 

10596  121 
the assumptions. We can apply the \isa{assumption} 
10295  122 
method, which proves a subgoal by finding a matching assumption. 
123 
\begin{isabelle} 

10596  124 
\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ 
10295  125 
Q\ \isasymand\ P 
126 
\end{isabelle} 

127 
We are left with the subgoal of proving 

128 
\isa{Q\ \isasymand\ P} from the assumptions \isa{P} and~\isa{Q}. We apply 

129 
\isa{rule conjI} again. 

130 
\begin{isabelle} 

10596  131 
\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline 
132 
\ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P 

10295  133 
\end{isabelle} 
134 
We are left with two new subgoals, \isa{Q} and~\isa{P}, each of which can be proved 

10596  135 
using the \isa{assumption} method. 
10295  136 

137 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

138 
\section{Elimination Rules} 
10295  139 

140 
\textbf{Elimination} rules work in the opposite direction from introduction 

141 
rules. In the case of conjunction, there are two such rules. 

142 
From $P\conj Q$ we infer $P$. also, from $P\conj Q$ 

143 
we infer $Q$: 

144 
\[ \infer{P}{P\conj Q} \qquad \infer{Q}{P\conj Q} \] 

145 

146 
Now consider disjunction. There are two introduction rules, which resemble inverted forms of the 

147 
conjunction elimination rules: 

148 
\[ \infer{P\disj Q}{P} \qquad \infer{P\disj Q}{Q} \] 

149 

150 
What is the disjunction elimination rule? The situation is rather different from 

151 
conjunction. From $P\disj Q$ we cannot conclude that $P$ is true and we 

152 
cannot conclude that $Q$ is true; there are no direct 

153 
elimination rules of the sort that we have seen for conjunction. Instead, 

154 
there is an elimination rule that works indirectly. If we are trying to prove 

155 
something else, say $R$, and we know that $P\disj Q$ holds, then we have to consider 

156 
two cases. We can assume that $P$ is true and prove $R$ and then assume that $Q$ is 

157 
true and prove $R$ a second time. Here we see a fundamental concept used in natural 

158 
deduction: that of the \textbf{assumptions}. We have to prove $R$ twice, under 

159 
different assumptions. The assumptions are local to these subproofs and are visible 

160 
nowhere else. 

161 

162 
In a logic text, the disjunction elimination rule might be shown 

163 
like this: 

164 
\[ \infer{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}} \] 

165 
The assumptions $[P]$ and $[Q]$ are bracketed 

166 
to emphasize that they are local to their subproofs. In Isabelle 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

167 
notation, the alreadyfamiliar \isa{\isasymLongrightarrow} syntax serves the 
10295  168 
same purpose: 
169 
\begin{isabelle} 

170 
\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE} 

171 
\end{isabelle} 

172 
When we use this sort of elimination rule backwards, it produces 

173 
a case split. (We have this before, in proofs by induction.) The following proof 

174 
illustrates the use of disjunction elimination. 

175 
\begin{isabelle} 

10301  176 
\isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\ 
10295  177 
\isasymLongrightarrow\ Q\ \isasymor\ P"\isanewline 
178 
\isacommand{apply}\ (erule\ disjE)\isanewline 

179 
\ \isacommand{apply}\ (rule\ disjI2)\isanewline 

180 
\ \isacommand{apply}\ assumption\isanewline 

181 
\isacommand{apply}\ (rule\ disjI1)\isanewline 

182 
\isacommand{apply}\ assumption 

183 
\end{isabelle} 

184 
We assume \isa{P\ \isasymor\ Q} and 

185 
must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction 

186 
elimination rule, \isa{disjE}. The method {\isa{erule}} applies an 

187 
elimination rule to the assumptions, searching for one that matches the 

188 
rule's first premise. Deleting that assumption, it 

189 
return the subgoals for the remaining premises. Most of the 

190 
time, this is the best way to use elimination rules; only rarely is there 

191 
any point in keeping the assumption. 

192 

193 
\begin{isabelle} 

194 
%P\ \isasymor\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline 

195 
\ 1.\ P\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline 

196 
\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P 

197 
\end{isabelle} 

198 
Here it leaves us with two subgoals. The first assumes \isa{P} and the 

199 
second assumes \isa{Q}. Tackling the first subgoal, we need to 

200 
show \isa{Q\ \isasymor\ P}\@. The second introduction rule (\isa{disjI2}) 

201 
can reduce this to \isa{P}, which matches the assumption. So, we apply the 

10596  202 
\isa{rule} method with \isa{disjI2} \ldots 
10295  203 
\begin{isabelle} 
204 
\ 1.\ P\ \isasymLongrightarrow\ P\isanewline 

205 
\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P 

206 
\end{isabelle} 

10596  207 
\ldots and finish off with the \isa{assumption} 
10295  208 
method. We are left with the other subgoal, which 
209 
assumes \isa{Q}. 

210 
\begin{isabelle} 

211 
\ 1.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P 

212 
\end{isabelle} 

213 
Its proof is similar, using the introduction 

214 
rule \isa{disjI1}. 

215 

216 
The result of this proof is a new inference rule \isa{disj_swap}, which is neither 

217 
an introduction nor an elimination rule, but which might 

218 
be useful. We can use it to replace any goal of the form $Q\disj P$ 

219 
by a one of the form $P\disj Q$. 

220 

221 

222 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

223 
\section{Destruction Rules: Some Examples} 
10295  224 

225 
Now let us examine the analogous proof for conjunction. 

226 
\begin{isabelle} 

10301  227 
\isacommand{lemma}\ conj_swap:\ "P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P"\isanewline 
10295  228 
\isacommand{apply}\ (rule\ conjI)\isanewline 
229 
\ \isacommand{apply}\ (drule\ conjunct2)\isanewline 

230 
\ \isacommand{apply}\ assumption\isanewline 

231 
\isacommand{apply}\ (drule\ conjunct1)\isanewline 

232 
\isacommand{apply}\ assumption 

233 
\end{isabelle} 

234 
Recall that the conjunction elimination rules  whose Isabelle names are 

235 
\isa{conjunct1} and \isa{conjunct2}  simply return the first or second half 

236 
of a conjunction. Rules of this sort (where the conclusion is a subformula of a 

237 
premise) are called \textbf{destruction} rules, by analogy with the destructor 

10301  238 
functions of functional programming.% 
10295  239 
\footnote{This Isabelle terminology has no counterpart in standard logic texts, 
240 
although the distinction between the two forms of elimination rule is well known. 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

241 
Girard \cite[page 74]{girard89}, for example, writes ``The elimination rules 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

242 
[for $\disj$ and $\exists$] are very 
10295  243 
bad. What is catastrophic about them is the parasitic presence of a formula [$R$] 
244 
which has no structural link with the formula which is eliminated.''} 

245 

246 
The first proof step applies conjunction introduction, leaving 

247 
two subgoals: 

248 
\begin{isabelle} 

249 
%P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P\isanewline 

250 
\ 1.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\isanewline 

251 
\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P 

252 
\end{isabelle} 

253 

254 
To invoke the elimination rule, we apply a new method, \isa{drule}. 

255 
Think of the \isa{d} as standing for \textbf{destruction} (or \textbf{direct}, if 

256 
you prefer). Applying the 

257 
second conjunction rule using \isa{drule} replaces the assumption 

258 
\isa{P\ \isasymand\ Q} by \isa{Q}. 

259 
\begin{isabelle} 

260 
\ 1.\ Q\ \isasymLongrightarrow\ Q\isanewline 

261 
\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P 

262 
\end{isabelle} 

263 
The resulting subgoal can be proved by applying \isa{assumption}. 

264 
The other subgoal is similarly proved, using the \isa{conjunct1} rule and the 

265 
\isa{assumption} method. 

266 

267 
Choosing among the methods \isa{rule}, \isa{erule} and \isa{drule} is up to 

268 
you. Isabelle does not attempt to work out whether a rule 

269 
is an introduction rule or an elimination rule. The 

270 
method determines how the rule will be interpreted. Many rules 

271 
can be used in more than one way. For example, \isa{disj_swap} can 

272 
be applied to assumptions as well as to goals; it replaces any 

273 
assumption of the form 

274 
$P\disj Q$ by a one of the form $Q\disj P$. 

275 

276 
Destruction rules are simpler in form than indirect rules such as \isa{disjE}, 

277 
but they can be inconvenient. Each of the conjunction rules discards half 

278 
of the formula, when usually we want to take both parts of the conjunction as new 

279 
assumptions. The easiest way to do so is by using an 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

280 
alternative conjunction elimination rule that resembles \isa{disjE}\@. It is 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

281 
seldom, if ever, seen in logic books. In Isabelle syntax it looks like this: 
10295  282 
\begin{isabelle} 
283 
\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{conjE} 

284 
\end{isabelle} 

285 

286 
\begin{exercise} 

287 
Use the rule {\isa{conjE}} to shorten the proof above. 

288 
\end{exercise} 

289 

290 

291 
\section{Implication} 

292 

293 
At the start of this chapter, we saw the rule \textit{modus ponens}. It is, in fact, 

294 
a destruction rule. The matching introduction rule looks like this 

295 
in Isabelle: 

296 
\begin{isabelle} 

297 
(?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\ 

298 
\isasymlongrightarrow\ ?Q\rulename{impI} 

299 
\end{isabelle} 

300 
And this is \textit{modus ponens}: 

301 
\begin{isabelle} 

302 
\isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\ 

303 
\isasymLongrightarrow\ ?Q 

304 
\rulename{mp} 

305 
\end{isabelle} 

306 

307 
Here is a proof using the rules for implication. This 

308 
lemma performs a sort of uncurrying, replacing the two antecedents 

309 
of a nested implication by a conjunction. 

310 
\begin{isabelle} 

311 
\isacommand{lemma}\ imp_uncurry:\ 

10301  312 
"P\ \isasymlongrightarrow\ (Q\ 
10295  313 
\isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\ 
314 
\isasymand\ Q\ \isasymlongrightarrow\ 

315 
R"\isanewline 

316 
\isacommand{apply}\ (rule\ impI)\isanewline 

317 
\isacommand{apply}\ (erule\ conjE)\isanewline 

318 
\isacommand{apply}\ (drule\ mp)\isanewline 

319 
\ \isacommand{apply}\ assumption\isanewline 

320 
\isacommand{apply}\ (drule\ mp)\isanewline 

321 
\ \ \isacommand{apply}\ assumption\isanewline 

322 
\ \isacommand{apply}\ assumption 

323 
\end{isabelle} 

324 
First, we state the lemma and apply implication introduction (\isa{rule impI}), 

325 
which moves the conjunction to the assumptions. 

326 
\begin{isabelle} 

327 
%P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R\ \isasymLongrightarrow\ P\ 

328 
%\isasymand\ Q\ \isasymlongrightarrow\ R\isanewline 

10596  329 
\ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R 
10295  330 
\end{isabelle} 
331 
Next, we apply conjunction elimination (\isa{erule conjE}), which splits this 

332 
conjunction into two parts. 

333 
\begin{isabelle} 

10596  334 
\ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\ 
10295  335 
Q\isasymrbrakk\ \isasymLongrightarrow\ R 
336 
\end{isabelle} 

337 
Now, we work on the assumption \isa{P\ \isasymlongrightarrow\ (Q\ 

338 
\isasymlongrightarrow\ R)}, where the parentheses have been inserted for 

339 
clarity. The nested implication requires two applications of 

340 
\textit{modus ponens}: \isa{drule mp}. The first use yields the 

341 
implication \isa{Q\ 

342 
\isasymlongrightarrow\ R}, but first we must prove the extra subgoal 

343 
\isa{P}, which we do by assumption. 

344 
\begin{isabelle} 

10596  345 
\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline 
346 
\ 2.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R 

10295  347 
\end{isabelle} 
348 
Repeating these steps for \isa{Q\ 

349 
\isasymlongrightarrow\ R} yields the conclusion we seek, namely~\isa{R}. 

350 
\begin{isabelle} 

10596  351 
\ 1.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ 
10295  352 
\isasymLongrightarrow\ R 
353 
\end{isabelle} 

354 

355 
The symbols \isa{\isasymLongrightarrow} and \isa{\isasymlongrightarrow} 

356 
both stand for implication, but they differ in many respects. Isabelle 

357 
uses \isa{\isasymLongrightarrow} to express inference rules; the symbol is 

358 
builtin and Isabelle's inference mechanisms treat it specially. On the 

359 
other hand, \isa{\isasymlongrightarrow} is just one of the many connectives 

360 
available in higherorder logic. We reason about it using inference rules 

361 
such as \isa{impI} and \isa{mp}, just as we reason about the other 

362 
connectives. You will have to use \isa{\isasymlongrightarrow} in any 

363 
context that requires a formula of higherorder logic. Use 

364 
\isa{\isasymLongrightarrow} to separate a theorem's preconditions from its 

365 
conclusion. 

366 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

367 
\medskip 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

368 
\indexbold{by} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

369 
The \isacommand{by} command is useful for proofs like these that use 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

370 
\isa{assumption} heavily. It executes an 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

371 
\isacommand{apply} command, then tries to prove all remaining subgoals using 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

372 
\isa{assumption}. Since (if successful) it ends the proof, it also replaces the 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

373 
\isacommand{done} symbol. For example, the proof above can be shortened: 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

374 
\begin{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

375 
\isacommand{lemma}\ imp_uncurry:\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

376 
"P\ \isasymlongrightarrow\ (Q\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

377 
\isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

378 
\isasymand\ Q\ \isasymlongrightarrow\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

379 
R"\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

380 
\isacommand{apply}\ (rule\ impI)\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

381 
\isacommand{apply}\ (erule\ conjE)\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

382 
\isacommand{apply}\ (drule\ mp)\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

383 
\ \isacommand{apply}\ assumption\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

384 
\isacommand{by}\ (drule\ mp) 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

385 
\end{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

386 
We could use \isacommand{by} to replace the final \isacommand{apply} and 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

387 
\isacommand{done} in any proof, but typically we use it 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

388 
to eliminate calls to \isa{assumption}. It is also a nice way of expressing a 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

389 
oneline proof. 
10295  390 

391 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

392 
\section{Unification and Substitution}\label{sec:unification} 
10295  393 

394 
As we have seen, Isabelle rules involve variables that begin with a 

395 
question mark. These are called \textbf{schematic} variables and act as 

396 
placeholders for terms. \textbf{Unification} refers to the process of 

397 
making two terms identical, possibly by replacing their variables by 

398 
terms. The simplest case is when the two terms are already the same. Next 

399 
simplest is when the variables in only one of the term 

400 
are replaced; this is called \textbf{patternmatching}. The 

10596  401 
\isa{rule} method typically matches the rule's conclusion 
10295  402 
against the current subgoal. In the most complex case, variables in both 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

403 
terms are replaced; the \isa{rule} method can do this if the goal 
10295  404 
itself contains schematic variables. Other occurrences of the variables in 
405 
the rule or proof state are updated at the same time. 

406 

407 
Schematic variables in goals are sometimes called \textbf{unknowns}. They 

408 
are useful because they let us proceed with a proof even when we do not 

409 
know what certain terms should be  as when the goal is $\exists x.\,P$. 

410 
They can be filled in later, often automatically. 

411 

412 
Unification is well known to Prolog programmers. Isabelle uses \textbf{higherorder} 

413 
unification, which is unification in the 

414 
typed $\lambda$calculus. The general case is 

415 
undecidable, but for our purposes, the differences from ordinary 

416 
unification are straightforward. It handles bound variables 

417 
correctly, avoiding capture. The two terms \isa{{\isasymlambda}x.\ ?P} and 

418 
\isa{{\isasymlambda}x.\ t x} are not unifiable; replacing \isa{?P} by 

419 
\isa{t x} is forbidden because the free occurrence of~\isa{x} would become 

420 
bound. The two terms 

421 
\isa{{\isasymlambda}x.\ f(x,z)} and \isa{{\isasymlambda}y.\ f(y,z)} are 

422 
trivially unifiable because they differ only by a bound variable renaming. 

423 

424 
Higherorder unification sometimes must invent 

425 
$\lambda$terms to replace function variables, 

426 
which can lead to a combinatorial explosion. However, Isabelle proofs tend 

427 
to involve easy cases where there are few possibilities for the 

428 
$\lambda$term being constructed. In the easiest case, the 

429 
function variable is applied only to bound variables, 

430 
as when we try to unify \isa{{\isasymlambda}x\ y.\ f(?h x y)} and 

431 
\isa{{\isasymlambda}x\ y.\ f(x+y+a)}. The only solution is to replace 

432 
\isa{?h} by \isa{{\isasymlambda}x\ y.\ x+y+a}. Such cases admit at most 

433 
one unifier, like ordinary unification. A harder case is 

434 
unifying \isa{?h a} with~\isa{a+b}; it admits two solutions for \isa{?h}, 

435 
namely \isa{{\isasymlambda}x.~a+b} and \isa{{\isasymlambda}x.~x+b}. 

436 
Unifying \isa{?h a} with~\isa{a+a+b} admits four solutions; their number is 

437 
exponential in the number of occurrences of~\isa{a} in the second term. 

438 

439 
Isabelle also uses function variables to express \textbf{substitution}. 

440 
A typical substitution rule allows us to replace one term by 

441 
another if we know that two terms are equal. 

442 
\[ \infer{P[t/x]}{s=t & P[s/x]} \] 

443 
The conclusion uses a notation for substitution: $P[t/x]$ is the result of 

444 
replacing $x$ by~$t$ in~$P$. The rule only substitutes in the positions 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

445 
designated by~$x$. For example, it can 
10295  446 
derive symmetry of equality from reflexivity. Using $x=s$ for~$P$ 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

447 
replaces just the first $s$ in $s=s$ by~$t$: 
10295  448 
\[ \infer{t=s}{s=t & \infer{s=s}{}} \] 
449 

450 
The Isabelle version of the substitution rule looks like this: 

451 
\begin{isabelle} 

452 
\isasymlbrakk?t\ =\ ?s;\ ?P\ ?s\isasymrbrakk\ \isasymLongrightarrow\ ?P\ 

453 
?t 

454 
\rulename{ssubst} 

455 
\end{isabelle} 

456 
Crucially, \isa{?P} is a function 

457 
variable: it can be replaced by a $\lambda$expression 

458 
involving one bound variable whose occurrences identify the places 

459 
in which $s$ will be replaced by~$t$. The proof above requires 

460 
\isa{{\isasymlambda}x.~x=s}. 

461 

462 
The \isa{simp} method replaces equals by equals, but using the substitution 

463 
rule gives us more control. Consider this proof: 

464 
\begin{isabelle} 

465 
\isacommand{lemma}\ 

10596  466 
"\isasymlbrakk \ x\ =\ f\ x;\ odd(f\ x)\ \isasymrbrakk\ \isasymLongrightarrow\ 
467 
odd\ x"\isanewline 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

468 
\isacommand{by}\ (erule\ ssubst) 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

469 
\end{isabelle} 
10295  470 
% 
471 
The simplifier might loop, replacing \isa{x} by \isa{f x} and then by 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

472 
\isa{f(f x)} and so forth. (Here \isa{simp} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

473 
can see the danger and would reorient the equality, but in more complicated 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

474 
cases it can be fooled.) When we apply substitution, Isabelle replaces every 
10295  475 
\isa{x} in the subgoal by \isa{f x} just once: it cannot loop. The 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

476 
resulting subgoal is trivial by assumption, so the \isacommand{by} command 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

477 
proves it implicitly. 
10295  478 

479 
We are using the \isa{erule} method it in a novel way. Hitherto, 

480 
the conclusion of the rule was just a variable such as~\isa{?R}, but it may 

481 
be any term. The conclusion is unified with the subgoal just as 

482 
it would be with the \isa{rule} method. At the same time \isa{erule} looks 

483 
for an assumption that matches the rule's first premise, as usual. With 

484 
\isa{ssubst} the effect is to find, use and delete an equality 

485 
assumption. 

486 

487 

488 
Higherorder unification can be tricky, as this example indicates: 

489 
\begin{isabelle} 

10596  490 
\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ 
10295  491 
f\ x;\ triple\ (f\ x)\ 
492 
(f\ x)\ x\ \isasymrbrakk\ 

493 
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline 

494 
\isacommand{apply}\ (erule\ ssubst)\isanewline 

495 
\isacommand{back}\isanewline 

496 
\isacommand{back}\isanewline 

497 
\isacommand{back}\isanewline 

498 
\isacommand{back}\isanewline 

499 
\isacommand{apply}\ assumption\isanewline 

500 
\isacommand{done} 

501 
\end{isabelle} 

502 
% 

503 
By default, Isabelle tries to substitute for all the 

504 
occurrences. Applying \isa{erule\ ssubst} yields this subgoal: 

505 
\begin{isabelle} 

506 
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ (f\ x) 

507 
\end{isabelle} 

508 
The substitution should have been done in the first two occurrences 

509 
of~\isa{x} only. Isabelle has gone too far. The \isa{back} 

510 
method allows us to reject this possibility and get a new one: 

511 
\begin{isabelle} 

512 
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ (f\ x)\ (f\ x) 

513 
\end{isabelle} 

514 
% 

515 
Now Isabelle has left the first occurrence of~\isa{x} alone. That is 

516 
promising but it is not the desired combination. So we use \isa{back} 

517 
again: 

518 
\begin{isabelle} 

519 
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ x\ (f\ x) 

520 
\end{isabelle} 

521 
% 

522 
This also is wrong, so we use \isa{back} again: 

523 
\begin{isabelle} 

524 
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ x\ (f\ x) 

525 
\end{isabelle} 

526 
% 

527 
And this one is wrong too. Looking carefully at the series 

528 
of alternatives, we see a binary countdown with reversed bits: 111, 

529 
011, 101, 001. Invoke \isa{back} again: 

530 
\begin{isabelle} 

531 
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ x% 

532 
\end{isabelle} 

533 
At last, we have the right combination! This goal follows by assumption. 

534 

535 
Never use {\isa{back}} in the final version of a proof. 

536 
It should only be used for exploration. One way to get rid of {\isa{back}} 

537 
to combine two methods in a single \textbf{apply} command. Isabelle 

538 
applies the first method and then the second. If the second method 

539 
fails then Isabelle automatically backtracks. This process continues until 

540 
the first method produces an output that the second method can 

541 
use. We get a oneline proof of our example: 

542 
\begin{isabelle} 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

543 
\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ 
10295  544 
\isasymrbrakk\ 
545 
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline 

546 
\isacommand{apply}\ (erule\ ssubst,\ assumption)\isanewline 

547 
\isacommand{done} 

548 
\end{isabelle} 

549 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

550 
\noindent 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

551 
The \isacommand{by} command works too, since it backtracks when 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

552 
proving subgoals by assumption: 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

553 
\begin{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

554 
\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

555 
\isasymrbrakk\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

556 
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

557 
\isacommand{by}\ (erule\ ssubst) 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

558 
\end{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

559 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

560 

10295  561 
The most general way to get rid of the {\isa{back}} command is 
10596  562 
to instantiate variables in the rule. The method \isa{rule_tac} is 
10295  563 
similar to \isa{rule}, but it 
564 
makes some of the rule's variables denote specified terms. 

10596  565 
Also available are {\isa{drule_tac}} and \isa{erule_tac}. Here we need 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

566 
\isa{erule_tac} since above we used \isa{erule}. 
10295  567 
\begin{isabelle} 
10596  568 
\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

569 
\isacommand{by}\ (erule_tac\ P="\isasymlambda u.\ P\ u\ u\ x"\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

570 
\isakeyword{in}\ ssubst) 
10295  571 
\end{isabelle} 
572 
% 

573 
To specify a desired substitution 

574 
requires instantiating the variable \isa{?P} with a $\lambda$expression. 

575 
The bound variable occurrences in \isa{{\isasymlambda}u.\ P\ u\ 

576 
u\ x} indicate that the first two arguments have to be substituted, leaving 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

577 
the third unchanged. With this instantiation, backtracking is neither necessary 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

578 
nor possible. 
10295  579 

10596  580 
An alternative to \isa{rule_tac} is to use \isa{rule} with the 
581 
\isa{of} directive, described in \S\ref{sec:forward} below. An 

582 
advantage of \isa{rule_tac} is that the instantiations may refer to 

10295  583 
variables bound in the current subgoal. 
584 

585 

586 
\section{Negation} 

587 

588 
Negation causes surprising complexity in proofs. Its natural 

589 
deduction rules are straightforward, but additional rules seem 

590 
necessary in order to handle negated assumptions gracefully. 

591 

592 
Negation introduction deduces $\neg P$ if assuming $P$ leads to a 

593 
contradiction. Negation elimination deduces any formula in the 

594 
presence of $\neg P$ together with~$P$: 

595 
\begin{isabelle} 

596 
(?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P% 

597 
\rulename{notI}\isanewline 

598 
\isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R% 

599 
\rulename{notE} 

600 
\end{isabelle} 

601 
% 

602 
Classical logic allows us to assume $\neg P$ 

603 
when attempting to prove~$P$: 

604 
\begin{isabelle} 

605 
(\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P% 

606 
\rulename{classical} 

607 
\end{isabelle} 

608 
% 

609 
Three further rules are variations on the theme of contrapositive. 

610 
They differ in the placement of the negation symbols: 

611 
\begin{isabelle} 

612 
\isasymlbrakk?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% 

613 
\rulename{contrapos_pp}\isanewline 

614 
\isasymlbrakk{\isasymnot}\ ?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% 

615 
\rulename{contrapos_np}\isanewline 

616 
\isasymlbrakk{\isasymnot}\ ?Q;\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ \isasymnot\ ?P% 

617 
\rulename{contrapos_nn} 

618 
\end{isabelle} 

619 
% 

620 
These rules are typically applied using the {\isa{erule}} method, where 

621 
their effect is to form a contrapositive from an 

622 
assumption and the goal's conclusion. 

623 

624 
The most important of these is \isa{contrapos_np}. It is useful 

625 
for applying introduction rules to negated assumptions. For instance, 

626 
the assumption $\neg(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we 

627 
might want to use conjunction introduction on it. 

628 
Before we can do so, we must move that assumption so that it 

629 
becomes the conclusion. The following proof demonstrates this 

630 
technique: 

631 
\begin{isabelle} 

632 
\isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\ 

633 
\isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\ 

634 
R"\isanewline 

635 
\isacommand{apply}\ (erule_tac\ Q="R{\isasymlongrightarrow}Q"\ \isakeyword{in}\ 

636 
contrapos_np)\isanewline 

637 
\isacommand{apply}\ intro\isanewline 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

638 
\isacommand{by}\ (erule\ notE) 
10295  639 
\end{isabelle} 
640 
% 

641 
There are two negated assumptions and we need to exchange the conclusion with the 

642 
second one. The method \isa{erule contrapos_np} would select the first assumption, 

643 
which we do not want. So we specify the desired assumption explicitly, using 

644 
\isa{erule_tac}. This is the resulting subgoal: 

645 
\begin{isabelle} 

646 
\ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ 

647 
R\isasymrbrakk\ \isasymLongrightarrow\ R\ \isasymlongrightarrow\ Q% 

648 
\end{isabelle} 

649 
The former conclusion, namely \isa{R}, now appears negated among the assumptions, 

650 
while the negated formula \isa{R\ \isasymlongrightarrow\ Q} becomes the new 

651 
conclusion. 

652 

653 
We can now apply introduction rules. We use the {\isa{intro}} method, which 

654 
repeatedly applies builtin introduction rules. Here its effect is equivalent 

10596  655 
to \isa{rule impI}. 
656 
\begin{isabelle} 

10295  657 
\ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ R;\ 
658 
R\isasymrbrakk\ \isasymLongrightarrow\ Q% 

659 
\end{isabelle} 

660 
We can see a contradiction in the form of assumptions \isa{\isasymnot\ R} 

661 
and~\isa{R}, which suggests using negation elimination. If applied on its own, 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

662 
\isa{notE} will select the first negated assumption, which is useless. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

663 
Instead, we invoke the rule using the 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

664 
\isa{by} command. 
10295  665 
Now when Isabelle selects the first assumption, it tries to prove \isa{P\ 
666 
\isasymlongrightarrow\ Q} and fails; it then backtracks, finds the 

667 
assumption~\isa{\isasymnot\ R} and finally proves \isa{R} by assumption. That 

668 
concludes the proof. 

669 

670 
\medskip 

671 

672 
Here is another example. 

673 
\begin{isabelle} 

674 
\isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\ 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

675 
\isasymLongrightarrow\ P\ \isasymor\ (Q\ \isasymand\ R)"\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

676 
\isacommand{apply}\ intro\isanewline 
10295  677 
\isacommand{apply}\ (elim\ conjE\ disjE)\isanewline 
678 
\ \isacommand{apply}\ assumption 

679 
\isanewline 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

680 
\isacommand{by}\ (erule\ contrapos_np,\ rule\ conjI) 
10295  681 
\end{isabelle} 
682 
% 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

683 
The first proof step applies the {\isa{intro}} method, which repeatedly uses 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

684 
builtin introduction rules. Here it creates the negative assumption 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

685 
\hbox{\isa{\isasymnot(Q\ \isasymand\ R)}}. That comes from \isa{disjCI}, a 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

686 
disjunction introduction rule that combines the effects of 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

687 
\isa{disjI1} and \isa{disjI2}. 
10295  688 
\begin{isabelle} 
689 
\ 1.\ \isasymlbrakk(P\ \isasymor\ Q)\ \isasymand\ R;\ \isasymnot\ (Q\ \isasymand\ 

690 
R)\isasymrbrakk\ \isasymLongrightarrow\ P% 

691 
\end{isabelle} 

692 
Next we apply the {\isa{elim}} method, which repeatedly applies 

693 
elimination rules; here, the elimination rules given 

694 
in the command. One of the subgoals is trivial, leaving us with one other: 

695 
\begin{isabelle} 

696 
\ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P% 

697 
\end{isabelle} 

698 
% 

699 
Now we must move the formula \isa{Q\ \isasymand\ R} to be the conclusion. The 

700 
combination 

701 
\begin{isabelle} 

702 
\ \ \ \ \ (erule\ contrapos_np,\ rule\ conjI) 

703 
\end{isabelle} 

704 
is robust: the \isa{conjI} forces the \isa{erule} to select a 

10301  705 
conjunction. The two subgoals are the ones we would expect from applying 
10295  706 
conjunction introduction to 
707 
\isa{Q\ 

708 
\isasymand\ R}: 

709 
\begin{isabelle} 

10596  710 
\ 1.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ 
10295  711 
Q\isanewline 
10596  712 
\ 2.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R% 
10295  713 
\end{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

714 
They are proved by assumption, which is implicit in the \isacommand{by} command. 
10295  715 

716 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

717 
\section{Quantifiers} 
10295  718 

719 
Quantifiers require formalizing syntactic substitution and the notion of \textbf{arbitrary 

720 
value}. Consider the universal quantifier. In a logic book, its 

721 
introduction rule looks like this: 

722 
\[ \infer{\forall x.\,P}{P} \] 

723 
Typically, a proviso written in English says that $x$ must not 

724 
occur in the assumptions. This proviso guarantees that $x$ can be regarded as 

725 
arbitrary, since it has not been assumed to satisfy any special conditions. 

726 
Isabelle's underlying formalism, called the 

727 
\textbf{metalogic}, eliminates the need for English. It provides its own universal 

728 
quantifier (\isasymAnd) to express the notion of an arbitrary value. We have 

729 
already seen another symbol of the metalogic, namely 

730 
\isa\isasymLongrightarrow, which expresses inference rules and the treatment of 

731 
assumptions. The only other symbol in the metalogic is \isa\isasymequiv, which 

732 
can be used to define constants. 

733 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

734 
\subsection{The Universal Introduction Rule} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

735 

10295  736 
Returning to the universal quantifier, we find that having a similar quantifier 
737 
as part of the metalogic makes the introduction rule trivial to express: 

738 
\begin{isabelle} 

10596  739 
(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI} 
10295  740 
\end{isabelle} 
741 

742 

743 
The following trivial proof demonstrates how the universal introduction 

744 
rule works. 

745 
\begin{isabelle} 

746 
\isacommand{lemma}\ "{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x"\isanewline 

747 
\isacommand{apply}\ (rule\ allI)\isanewline 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

748 
\isacommand{by}\ (rule\ impI) 
10295  749 
\end{isabelle} 
750 
The first step invokes the rule by applying the method \isa{rule allI}. 

751 
\begin{isabelle} 

752 
%{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x\isanewline 

10596  753 
\ 1.\ \isasymAnd x.\ P\ x\ \isasymlongrightarrow\ P\ x 
10295  754 
\end{isabelle} 
755 
Note that the resulting proof state has a bound variable, 

756 
namely~\bigisa{x}. The rule has replaced the universal quantifier of 

757 
higherorder logic by Isabelle's metalevel quantifier. Our goal is to 

758 
prove 

759 
\isa{P\ x\ \isasymlongrightarrow\ P\ x} for arbitrary~\isa{x}; it is 

760 
an implication, so we apply the corresponding introduction rule (\isa{impI}). 

761 
\begin{isabelle} 

10596  762 
\ 1.\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow\ P\ x 
10295  763 
\end{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

764 
This last subgoal is implicitly proved by assumption. 
10295  765 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

766 
\subsection{The Universal Elimination Rule} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

767 

10295  768 
Now consider universal elimination. In a logic text, 
769 
the rule looks like this: 

770 
\[ \infer{P[t/x]}{\forall x.\,P} \] 

771 
The conclusion is $P$ with $t$ substituted for the variable~$x$. 

772 
Isabelle expresses substitution using a function variable: 

773 
\begin{isabelle} 

774 
{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulename{spec} 

775 
\end{isabelle} 

776 
This destruction rule takes a 

777 
universally quantified formula and removes the quantifier, replacing 

778 
the bound variable \bigisa{x} by the schematic variable \bigisa{?x}. Recall that a 

779 
schematic variable starts with a question mark and acts as a 

780 
placeholder: it can be replaced by any term. 

781 

782 
To see how this works, let us derive a rule about reducing 

783 
the scope of a universal quantifier. In mathematical notation we write 

784 
\[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \] 

785 
with the proviso `$x$ not free in~$P$.' Isabelle's treatment of 

786 
substitution makes the proviso unnecessary. The conclusion is expressed as 

787 
\isa{P\ 

788 
\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the 

789 
variable \isa{P} can introduce a dependence upon~\isa{x}: that would be a 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

790 
bound variable capture. Here is the Isabelle proof in full: 
10295  791 
\begin{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

792 
\isacommand{lemma}\ "(\isasymforall x.\ P\ \isasymlongrightarrow \ Q\ x)\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

793 
\isasymLongrightarrow \ P\ \isasymlongrightarrow \ (\isasymforall x.\ Q\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

794 
x)"\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

795 
\isacommand{apply}\ (rule\ impI,\ rule\ allI)\isanewline 
10295  796 
\isacommand{apply}\ (drule\ spec)\isanewline 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

797 
\isacommand{by}\ (drule\ mp) 
10295  798 
\end{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

799 
First we apply implies introduction (\isa{impI}), 
10295  800 
which moves the \isa{P} from the conclusion to the assumptions. Then 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

801 
we apply universal introduction (\isa{allI}). 
10295  802 
\begin{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

803 
\ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

804 
x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x 
10295  805 
\end{isabelle} 
806 
As before, it replaces the HOL 

807 
quantifier by a metalevel quantifier, producing a subgoal that 

808 
binds the variable~\bigisa{x}. The leading bound variables 

809 
(here \isa{x}) and the assumptions (here \isa{{\isasymforall}x.\ P\ 

810 
\isasymlongrightarrow\ Q\ x} and \isa{P}) form the \textbf{context} for the 

811 
conclusion, here \isa{Q\ x}. At each proof step, the subgoals inherit the 

812 
previous context, though some context elements may be added or deleted. 

813 
Applying \isa{erule} deletes an assumption, while many natural deduction 

814 
rules add bound variables or assumptions. 

815 

816 
Now, to reason from the universally quantified 

817 
assumption, we apply the elimination rule using the {\isa{drule}} 

818 
method. This rule is called \isa{spec} because it specializes a universal formula 

819 
to a particular term. 

820 
\begin{isabelle} 

10596  821 
\ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ P\ \isasymlongrightarrow\ Q\ (?x2\ 
822 
x)\isasymrbrakk\ \isasymLongrightarrow\ Q\ x 

10295  823 
\end{isabelle} 
824 
Observe how the context has changed. The quantified formula is gone, 

825 
replaced by a new assumption derived from its body. Informally, we have 

826 
removed the quantifier. The quantified variable 

827 
has been replaced by the curious term 

828 
\bigisa{?x2~x}; it acts as a placeholder that may be replaced 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

829 
by any term that can be built from~\bigisa{x}. (Formally, \bigisa{?x2} is an 
10295  830 
unknown of function type, applied to the argument~\bigisa{x}.) This new assumption is 
831 
an implication, so we can use \emph{modus ponens} on it. As before, it requires 

832 
proving the antecedent (in this case \isa{P}) and leaves us with the consequent. 

833 
\begin{isabelle} 

10596  834 
\ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ Q\ (?x2\ x)\isasymrbrakk\ 
10295  835 
\isasymLongrightarrow\ Q\ x 
836 
\end{isabelle} 

837 
The consequent is \isa{Q} applied to that placeholder. It may be replaced by any 

838 
term built from~\bigisa{x}, and here 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

839 
it should simply be~\bigisa{x}. The \isa{assumption} method, implicit in the 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

840 
\isacommand{by} command, proves this subgoal. The assumption need not 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

841 
be identical to the conclusion, provided the two formulas are unifiable. 
10295  842 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

843 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

844 
\subsection{Reusing an Assumption: the {\tt\slshape frule} Method} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

845 

10295  846 
Note that \isa{drule spec} removes the universal quantifier and  as 
847 
usual with elimination rules  discards the original formula. Sometimes, a 

848 
universal formula has to be kept so that it can be used again. Then we use a new 

849 
method: \isa{frule}. It acts like \isa{drule} but copies rather than replaces 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

850 
the selected assumption. The \isa{f} is for \emph{forward}. 
10295  851 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

852 
In this example, going from \isa{P\ a} to \isa{P(h(h~a))} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

853 
requires two uses of the quantified assumption, one for each~\isa{h} being 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

854 
affixed to the term~\isa{a}. 
10295  855 
\begin{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

856 
\isacommand{lemma}\ "\isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x); 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

857 
\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P(h\ (h\ a))"\isanewline 
10295  858 
\isacommand{apply}\ (frule\ spec)\isanewline 
859 
\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline 

860 
\isacommand{apply}\ (drule\ spec)\isanewline 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

861 
\isacommand{by}\ (drule\ mp) 
10295  862 
\end{isabelle} 
863 
% 

864 
Applying \isa{frule\ spec} leaves this subgoal: 

865 
\begin{isabelle} 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

866 
\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);\ P\ a;\ P\ ?x\ \isasymlongrightarrow\ P\ (h\ ?x)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a)) 
10295  867 
\end{isabelle} 
868 
It is just what \isa{drule} would have left except that the quantified 

869 
assumption is still present. The next step is to apply \isa{mp} to the 

870 
implication and the assumption \isa{P\ a}, which leaves this subgoal: 

871 
\begin{isabelle} 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

872 
\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);\ P\ a;\ P\ (h\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a)) 
10295  873 
\end{isabelle} 
874 
% 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

875 
We have created the assumption \isa{P(h\ a)}, which is progress. To finish the 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

876 
proof, we apply \isa{spec} one last time, using \isa{drule}. 
10854  877 

878 
\medskip 

879 
\emph{A final remark}. Applying \isa{spec} by the command 

10295  880 
\begin{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

881 
\isacommand{apply}\ (drule\ mp,\ assumption) 
10295  882 
\end{isabelle} 
10854  883 
would not work a second time: it would add a second copy of \isa{P(h~a)} instead 
884 
of the desired assumption, \isa{P(h(h~a))}. The \isacommand{by} 

885 
command forces Isabelle to backtrack until it finds the correct one. 

886 
Alternatively, we could have used the \isacommand{apply} command and bundled the 

887 
\isa{drule mp} with \emph{two} calls of \isa{assumption}. 

10295  888 

889 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

890 
\subsection{The Existential Quantifier} 
10295  891 

892 
The concepts just presented also apply to the existential quantifier, 

893 
whose introduction rule looks like this in Isabelle: 

894 
\begin{isabelle} 

895 
?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulename{exI} 

896 
\end{isabelle} 

897 
If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x. 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

898 
P(x)$ is also true. It is a dual of the universal elimination rule, and 
10295  899 
logic texts present it using the same notation for substitution. The existential 
900 
elimination rule looks like this 

901 
in a logic text: 

902 
\[ \infer{R}{\exists x.\,P & \infer*{R}{[P]}} \] 

903 
% 

904 
It looks like this in Isabelle: 

905 
\begin{isabelle} 

10596  906 
\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE} 
10295  907 
\end{isabelle} 
908 
% 

909 
Given an existentially quantified theorem and some 

910 
formula $Q$ to prove, it creates a new assumption by removing the quantifier. As with 

911 
the universal introduction rule, the textbook version imposes a proviso on the 

912 
quantified variable, which Isabelle expresses using its metalogic. Note that it is 

913 
enough to have a universal quantifier in the metalogic; we do not need an existential 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

914 
quantifier to be built in as well. 
10295  915 

916 

917 
\begin{exercise} 

918 
Prove the lemma 

919 
\[ \exists x.\, P\conj Q(x)\Imp P\conj(\exists x.\, Q(x)). \] 

920 
\emph{Hint}: the proof is similar 

921 
to the one just above for the universal quantifier. 

922 
\end{exercise} 

923 

924 

10887
7fb42b97413a
the \\epsilon character causes font errors in a section title
paulson
parents:
10854
diff
changeset

925 
\section{Hilbert's EpsilonOperator} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

926 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

927 
Isabelle/HOL provides Hilbert's 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

928 
$\epsilon$operator. The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

929 
true, provided such a value exists. Using this operator, we can express an 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

930 
existential destruction rule: 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

931 
\[ \infer{P[(\epsilon x. P) / \, x]}{\exists x.\,P} \] 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

932 
This rule is seldom used, for it can cause exponential blowup. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

933 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

934 
\subsection{Definite Descriptions} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

935 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

936 
In ASCII, we write \isa{SOME} for $\epsilon$. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

937 
\REMARK{the internal constant is \isa{Eps}} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

938 
The main use of \hbox{\isa{SOME\ x.\ P\ x}} is as a \textbf{definite 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

939 
description}: when \isa{P} is satisfied by a unique value,~\isa{a}. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

940 
We reason using this rule: 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

941 
\begin{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

942 
\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

943 
\isasymLongrightarrow \ (SOME\ x.\ P\ x)\ =\ a% 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

944 
\rulename{some_equality} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

945 
\end{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

946 
For instance, we can define the 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

947 
cardinality of a finite set~$A$ to be that 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

948 
$n$ such that $A$ is in onetoone correspondence with $\{1,\ldots,n\}$. We can then 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

949 
prove that the cardinality of the empty set is zero (since $n=0$ satisfies the 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

950 
description) and proceed to prove other facts. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

951 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

952 
Here is an example. HOL defines \isa{inv},\indexbold{*inv (constant)} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

953 
which expresses inverses of functions, as a definite 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

954 
description: 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

955 
\begin{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

956 
inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y% 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

957 
\rulename{inv_def} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

958 
\end{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

959 
The inverse of \isa{f}, when applied to \isa{y}, returns some {x} such that 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

960 
\isa{f~x~=~y}. For example, we can prove \isa{inv~Suc} really is the inverse 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

961 
of the \isa{Suc} function 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

962 
\begin{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

963 
\isacommand{lemma}\ "inv\ Suc\ (Suc\ x)\ =\ x"\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

964 
\isacommand{by}\ (simp\ add:\ inv_def) 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

965 
\end{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

966 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

967 
\noindent 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

968 
The proof is a oneliner: the subgoal simplifies to a degenerate application of 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

969 
\isa{SOME}, which is then erased. The definition says nothing about what 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

970 
\isa{inv~Suc} returns when applied to zero. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

971 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

972 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

973 
A more challenging example illustrates how Isabelle/HOL defines the leastnumber 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

974 
operator, which denotes the least \isa{x} satisfying~\isa{P}: 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

975 
\begin{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

976 
(LEAST\ x.\ P\ x)\ \isasymequiv \ SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

977 
P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y) 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

978 
\rulename{Least_def} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

979 
\end{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

980 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

981 
Let us prove the counterpart of \isa{some_equality} for this operator. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

982 
The first step merely unfolds the definition: 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

983 
\begin{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

984 
\isacommand{theorem}\ Least_equality:\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

985 
\ \ \ \ \ "\isasymlbrakk \ P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\ \isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

986 
\isacommand{apply}\ (simp\ add:\ Least_def)\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

987 
%\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

988 
%\isasymle \ x\isasymrbrakk \isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

989 
%\ \ \ \ \isasymLongrightarrow \ (SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))\ =\ k% 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

990 
\isacommand{apply}\ (rule\ some_equality)\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

991 
\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

992 
\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

993 
\isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ P\ k\ \isasymand \ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

994 
(\isasymforall y.\ P\ y\ \isasymlongrightarrow \ k\ \isasymle \ y)\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

995 
\ 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 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

996 
\ \ \ \ \ \ \ \ \isasymLongrightarrow \ x\ =\ k% 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

997 
\end{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

998 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

999 
As always with \isa{some_equality}, we must show existence and 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1000 
uniqueness of the claimed solution,~\isa{k}. Existence, the first 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1001 
subgoal, is trivial. Uniqueness, the second subgoal, follows by antisymmetry: 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1002 
\begin{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1003 
\isasymlbrakk x\ \isasymle \ y;\ y\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ x\ =\ y% 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1004 
\rulename{order_antisym} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1005 
\end{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1006 
The assumptions imply both \isa{k~\isasymle~x} and \isa{x~\isasymle~k}. One call 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1007 
to \isa{auto} does it all: 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1008 
\begin{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1009 
\isacommand{by}\ (auto\ intro:\ order_antisym) 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1010 
\end{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1011 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1012 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1013 
\subsection{Indefinite Descriptions} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1014 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1015 
Occasionally, \hbox{\isa{SOME\ x.\ P\ x}} serves as an \textbf{indefinite 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1016 
description}, when it makes an arbitrary selection from the values 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1017 
satisfying~\isa{P}\@. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1018 
\begin{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1019 
P\ x\ \isasymLongrightarrow \ P\ (SOME\ x.\ P\ x) 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1020 
\rulename{someI}\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1021 
\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ Q\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1022 
x\isasymrbrakk \ \isasymLongrightarrow \ Q\ (SOME\ x.\ P\ x) 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1023 
\rulename{someI2} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1024 
\end{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1025 
Rule \isa{someI} is basic (if anything satisfies \isa{P} then so does 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1026 
\hbox{\isa{SOME\ x.\ P\ x}}). Rule \isa{someI2} is easier to apply in a backward 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1027 
proof. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1028 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1029 
\medskip 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1030 
For example, let us prove the Axiom of Choice: 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1031 
\begin{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1032 
\isacommand{theorem}\ axiom_of_choice: 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1033 
\ "(\isasymforall x.\ \isasymexists \ y.\ P\ x\ y)\ \isasymLongrightarrow \ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1034 
\isasymexists f.\ \isasymforall x.\ P\ x\ (f\ x)"\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1035 
\isacommand{apply}\ (rule\ exI,\ rule\ allI)\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1036 
\ 1.\ \isasymAnd x.\ \isasymforall x.\ \isasymexists y.\ P\ x\ y\ 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1037 
\isasymLongrightarrow \ P\ x\ (?f\ x) 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1038 
\end{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1039 
% 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1040 
We have applied the introduction rules; now it is time to apply the elimination 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1041 
rules. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1042 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1043 
\begin{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1044 
\isacommand{apply}\ (drule\ spec,\ erule\ exE)\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1045 
\ 1.\ \isasymAnd x\ y.\ P\ (?x2\ x)\ y\ \isasymLongrightarrow \ P\ x\ (?f\ x) 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1046 
\end{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1047 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1048 
\noindent 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1049 
The rule \isa{someI} automatically instantiates 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1050 
\isa{f} to \hbox{\isa{\isasymlambda x.\ SOME y.\ P\ x\ y}}, which is the choice 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1051 
function. It also instantiates \isa{?x2\ x} to \isa{x}. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1052 
\begin{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1053 
\isacommand{by}\ (rule\ someI)\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1054 
\end{isabelle} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1055 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1056 

7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1057 
\section{Some Proofs That Fail} 
10295  1058 

1059 
Most of the examples in this tutorial involve proving theorems. But not every 

1060 
conjecture is true, and it can be instructive to see how 

1061 
proofs fail. Here we attempt to prove a distributive law involving 

1062 
the existential quantifier and conjunction. 

1063 
\begin{isabelle} 

1064 
\isacommand{lemma}\ "({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x"\isanewline 

1065 
\isacommand{apply}\ (erule\ conjE)\isanewline 

1066 
\isacommand{apply}\ (erule\ exE)\isanewline 

1067 
\isacommand{apply}\ (erule\ exE)\isanewline 

1068 
\isacommand{apply}\ (rule\ exI)\isanewline 

1069 
\isacommand{apply}\ (rule\ conjI)\isanewline 

1070 
\ \isacommand{apply}\ assumption\isanewline 

1071 
\isacommand{oops} 

1072 
\end{isabelle} 

1073 
The first steps are routine. We apply conjunction elimination (\isa{erule 

1074 
conjE}) to split the assumption in two, leaving two existentially quantified 

1075 
assumptions. Applying existential elimination (\isa{erule exE}) removes one of 

1076 
the quantifiers. 

1077 
\begin{isabelle} 

1078 
%({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\ 

1079 
%\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x\isanewline 

10596  1080 
\ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x 
10295  1081 
\end{isabelle} 
1082 
% 

1083 
When we remove the other quantifier, we get a different bound 

1084 
variable in the subgoal. (The name \isa{xa} is generated automatically.) 

1085 
\begin{isabelle} 

10596  1086 
\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ 
10295  1087 
\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x 
1088 
\end{isabelle} 

1089 
The proviso of the existential elimination rule has forced the variables to 

1090 
differ: we can hardly expect two arbitrary values to be equal! There is 

1091 
no way to prove this subgoal. Removing the 

1092 
conclusion's existential quantifier yields two 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1093 
identical placeholders, which can become any term involving the variables \isa{x} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1094 
and~\isa{xa}. We need one to become \isa{x} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1095 
and the other to become~\isa{xa}, but Isabelle requires all instances of a 
10295  1096 
placeholder to be identical. 
1097 
\begin{isabelle} 

10596  1098 
\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ 
10295  1099 
\isasymLongrightarrow\ P\ (?x3\ x\ xa)\isanewline 
10596  1100 
\ 2.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa) 
10295  1101 
\end{isabelle} 
1102 
We can prove either subgoal 

1103 
using the \isa{assumption} method. If we prove the first one, the placeholder 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1104 
changes into~\isa{x}. 
10295  1105 
\begin{isabelle} 
10596  1106 
\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ 
10295  1107 
\isasymLongrightarrow\ Q\ x 
1108 
\end{isabelle} 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1109 
We are left with a subgoal that cannot be proved. Applying the \isa{assumption} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1110 
method results in an error message: 
10295  1111 
\begin{isabelle} 
1112 
*** empty result sequence  proof command failed 

1113 
\end{isabelle} 

1114 
We can tell Isabelle to abandon a failed proof using the \isacommand{oops} command. 

1115 

1116 
\medskip 

1117 

1118 
Here is another abortive proof, illustrating the interaction between 

1119 
bound variables and unknowns. 

1120 
If $R$ is a reflexive relation, 

1121 
is there an $x$ such that $R\,x\,y$ holds for all $y$? Let us see what happens when 

1122 
we attempt to prove it. 

1123 
\begin{isabelle} 

1124 
\isacommand{lemma}\ "{\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ 

1125 
{\isasymexists}x.\ {\isasymforall}y.\ R\ x\ y"\isanewline 

1126 
\isacommand{apply}\ (rule\ exI)\isanewline 

1127 
\isacommand{apply}\ (rule\ allI)\isanewline 

1128 
\isacommand{apply}\ (drule\ spec)\isanewline 

1129 
\isacommand{oops} 

1130 
\end{isabelle} 

1131 
First, 

1132 
we remove the existential quantifier. The new proof state has 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1133 
an unknown, namely~\isa{?x}. 
10295  1134 
\begin{isabelle} 
1135 
%{\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymexists}x.\ 

1136 
%{\isasymforall}y.\ R\ x\ y\isanewline 

1137 
\ 1.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymforall}y.\ R\ ?x\ y 

1138 
\end{isabelle} 

1139 
Next, we remove the universal quantifier 

1140 
from the conclusion, putting the bound variable~\isa{y} into the subgoal. 

1141 
\begin{isabelle} 

10596  1142 
\ 1.\ \isasymAnd y.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ R\ ?x\ y 
10295  1143 
\end{isabelle} 
1144 
Finally, we try to apply our reflexivity assumption. We obtain a 

1145 
new assumption whose identical placeholders may be replaced by 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1146 
any term involving~\isa{y}. 
10295  1147 
\begin{isabelle} 
10596  1148 
\ 1.\ \isasymAnd y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y 
10295  1149 
\end{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1150 
This subgoal can only be proved by putting \isa{y} for all the placeholders, 
10295  1151 
making the assumption and conclusion become \isa{R\ y\ y}. 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1152 
But Isabelle refuses to substitute \isa{y}, a bound variable, for 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1153 
\isa{?x}; that would be a bound variable capture. The proof fails. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1154 
Note that Isabelle can replace \isa{?z2~y} by \isa{y}; this involves 
10295  1155 
instantiating 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1156 
\isa{?z2} to the identity function. 
10295  1157 

1158 
This example is typical of how Isabelle enforces sound quantifier reasoning. 

1159 

1160 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1161 
\section{Proving Theorems Using the {\tt\slshape blast} Method} 
10295  1162 

1163 
It is hard to prove substantial theorems using the methods 

1164 
described above. A proof may be dozens or hundreds of steps long. You 

1165 
may need to search among different ways of proving certain 

1166 
subgoals. Often a choice that proves one subgoal renders another 

1167 
impossible to prove. There are further complications that we have not 

1168 
discussed, concerning negation and disjunction. Isabelle's 

1169 
\textbf{classical reasoner} is a family of tools that perform such 

1170 
proofs automatically. The most important of these is the 

10596  1171 
\isa{blast} method. 
10295  1172 

1173 
In this section, we shall first see how to use the classical 

1174 
reasoner in its default mode and then how to insert additional 

1175 
rules, enabling it to work in new problem domains. 

1176 

1177 
We begin with examples from pure predicate logic. The following 

1178 
example is known as Andrew's challenge. Peter Andrews designed 

1179 
it to be hard to prove by automatic means.% 

1180 
\footnote{Pelletier~\cite{pelletier86} describes it and many other 

1181 
problems for automatic theorem provers.} 

1182 
The nested biconditionals cause an exponential explosion: the formal 

10596  1183 
proof is enormous. However, the \isa{blast} method proves it in 
10295  1184 
a fraction of a second. 
1185 
\begin{isabelle} 

1186 
\isacommand{lemma}\ 

1187 
"(({\isasymexists}x.\ 

1188 
{\isasymforall}y.\ 

10301  1189 
p(x){=}p(y))\ 
10295  1190 
=\ 
1191 
(({\isasymexists}x.\ 

10301  1192 
q(x))=({\isasymforall}y.\ 
1193 
p(y))))\ 

10295  1194 
\ \ =\ \ \ \ \isanewline 
1195 
\ \ \ \ \ \ \ \ 

1196 
(({\isasymexists}x.\ 

1197 
{\isasymforall}y.\ 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1198 
q(x){=}q(y))\ =\ (({\isasymexists}x.\ p(x))=({\isasymforall}y.\ q(y))))"\isanewline 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1199 
\isacommand{by}\ blast 
10295  1200 
\end{isabelle} 
1201 
The next example is a logic problem composed by Lewis Carroll. 

10596  1202 
The \isa{blast} method finds it trivial. Moreover, it turns out 
10295  1203 
that not all of the assumptions are necessary. We can easily 
1204 
experiment with variations of this formula and see which ones 

1205 
can be proved. 

1206 
\begin{isabelle} 

1207 
\isacommand{lemma}\ 

1208 
"({\isasymforall}x.\ 

1209 
honest(x)\ \isasymand\ 

1210 
industrious(x)\ \isasymlongrightarrow\ 

10301  1211 
healthy(x))\ 
10295  1212 
\isasymand\ \ \isanewline 
1213 
\ \ \ \ \ \ \ \ \isasymnot\ ({\isasymexists}x.\ 

1214 
grocer(x)\ \isasymand\ 

10301  1215 
healthy(x))\ 
10295  1216 
\isasymand\ \isanewline 
1217 
\ \ \ \ \ \ \ \ ({\isasymforall}x.\ 

1218 
industrious(x)\ \isasymand\ 

1219 
grocer(x)\ \isasymlongrightarrow\ 

10301  1220 
honest(x))\ 
10295  1221 
\isasymand\ \isanewline 
1222 
\ \ \ \ \ \ \ \ ({\isasymforall}x.\ 

1223 
cyclist(x)\ \isasymlongrightarrow\ 

10301  1224 
industrious(x))\ 
10295  1225 
\isasymand\ \isanewline 
1226 
\ \ \ \ \ \ \ \ ({\isasymforall}x.\ 

1227 
{\isasymnot}healthy(x)\ \isasymand\ 

1228 
cyclist(x)\ \isasymlongrightarrow\ 

10301  1229 
{\isasymnot}honest(x))\ 
10295  1230 
\ \isanewline 
1231 
\ \ \ \ \ \ \ \ \isasymlongrightarrow\ 

1232 
({\isasymforall}x.\ 

1233 
grocer(x)\ \isasymlongrightarrow\ 

10301  1234 
{\isasymnot}cyclist(x))"\isanewline 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1235 
\isacommand{by}\ blast 
10295  1236 
\end{isabelle} 
10596  1237 
The \isa{blast} method is also effective for set theory, which is 
10295  1238 
described in the next chapter. This formula below may look horrible, but 
1239 
the \isa{blast} method proves it easily. 

1240 
\begin{isabelle} 

10301  1241 
\isacommand{lemma}\ "({\isasymUnion}i{\isasymin}I.\ A(i))\ \isasyminter\ ({\isasymUnion}j{\isasymin}J.\ B(j))\ =\isanewline 
1242 
\ \ \ \ \ \ \ \ ({\isasymUnion}i{\isasymin}I.\ {\isasymUnion}j{\isasymin}J.\ A(i)\ \isasyminter\ B(j))"\isanewline 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1243 
\isacommand{by}\ blast 
10295  1244 
\end{isabelle} 
1245 

1246 
Few subgoals are couched purely in predicate logic and set theory. 

1247 
We can extend the scope of the classical reasoner by giving it new rules. 

1248 
Extending it effectively requires understanding the notions of 

1249 
introduction, elimination and destruction rules. Moreover, there is a 

1250 
distinction between safe and unsafe rules. A \textbf{safe} rule is one 

1251 
that can be applied backwards without losing information; an 

1252 
\textbf{unsafe} rule loses information, perhaps transforming the subgoal 

1253 
into one that cannot be proved. The safe/unsafe 

1254 
distinction affects the proof search: if a proof attempt fails, the 

1255 
classical reasoner backtracks to the most recent unsafe rule application 

1256 
and makes another choice. 

1257 

1258 
An important special case avoids all these complications. A logical 

1259 
equivalence, which in higherorder logic is an equality between 

1260 
formulas, can be given to the classical 

10596  1261 
reasoner and simplifier by using the attribute \isa{iff}. You 
10295  1262 
should do so if the right hand side of the equivalence is 
1263 
simpler than the lefthand side. 

1264 

1265 
For example, here is a simple fact about list concatenation. 

1266 
The result of appending two lists is empty if and only if both 

1267 
of the lists are themselves empty. Obviously, applying this equivalence 

1268 
will result in a simpler goal. When stating this lemma, we include 

10596  1269 
the \isa{iff} attribute. Once we have proved the lemma, Isabelle 
10295  1270 
will make it known to the classical reasoner (and to the simplifier). 
1271 
\begin{isabelle} 

1272 
\isacommand{lemma}\ 

10854  1273 
[iff]:\ "(xs{\isacharat}ys\ =\ [])\ =\ 
1274 
(xs=[]\ \isacharampersand\ ys=[])"\isanewline 

1275 
\isacommand{apply}\ (induct_tac\ xs)\isanewline 

1276 
\isacommand{apply}\ (simp_all)\isanewline 

10295  1277 
\isacommand{done} 
1278 
\end{isabelle} 

1279 
% 

1280 
This fact about multiplication is also appropriate for 

10854  1281 
the \isa{iff} attribute:\REMARK{the ?s are ugly here but we need 
1282 
them again when talking about \isa{of}; we need a consistent style} 

10295  1283 
\begin{isabelle} 
10596  1284 
(\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0) 
10295  1285 
\end{isabelle} 
1286 
A product is zero if and only if one of the factors is zero. The 

1287 
reasoning involves a logical \textsc{or}. Proving new rules for 

1288 
disjunctive reasoning is hard, but translating to an actual disjunction 

1289 
works: the classical reasoner handles disjunction properly. 

1290 

10596  1291 
In more detail, this is how the \isa{iff} attribute works. It converts 
10295  1292 
the equivalence $P=Q$ to a pair of rules: the introduction 
1293 
rule $Q\Imp P$ and the destruction rule $P\Imp Q$. It gives both to the 

1294 
classical reasoner as safe rules, ensuring that all occurrences of $P$ in 

1295 
a subgoal are replaced by~$Q$. The simplifier performs the same 

1296 
replacement, since \isa{iff} gives $P=Q$ to the 

1297 
simplifier. But classical reasoning is different from 

1298 
simplification. Simplification is deterministic: it applies rewrite rules 

1299 
repeatedly, as long as possible, in order to \emph{transform} a goal. Classical 

1300 
reasoning uses search and backtracking in order to \emph{prove} a goal. 

1301 

1302 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1303 
\section{Proving the Correctness of Euclid's Algorithm} 
10295  1304 
\label{sec:provingeuclid} 
1305 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1306 
A brief development will illustrate the advanced use of 
10854  1307 
\isa{blast}. We shall also see \isa{case_tac} used to perform a Boolean 
1308 
case split. 

1309 

1310 
In \S\ref{sec:recdefsimplification}, we declared the 

10596  1311 
recursive function \isa{gcd}: 
10295  1312 
\begin{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1313 
\isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline 
10301  1314 
\isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n)\ 
10596  1315 
::nat*nat\ \isasymRightarrow\ nat)"\isanewline 
10301  1316 
\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))" 
10295  1317 
\end{isabelle} 
1318 
Let us prove that it computes the greatest common 

1319 
divisor of its two arguments. 

1320 
The theorem is expressed in terms of the familiar 

1321 
\textbf{divides} relation from number theory: 

1322 
\begin{isabelle} 

10596  1323 
?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k 
10295  1324 
\rulename{dvd_def} 
1325 
\end{isabelle} 

1326 
% 

1327 
A simple induction proves the theorem. Here \isa{gcd.induct} refers to the 

1328 
induction rule returned by \isa{recdef}. The proof relies on the simplification 

1329 
rules proved in \S\ref{sec:recdefsimplification}, since rewriting by the 

1330 
definition of \isa{gcd} can cause looping. 

1331 
\begin{isabelle} 

10301  1332 
\isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\ n)"\isanewline 
1333 
\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline 

1334 
\isacommand{apply}\ (case_tac\ "n=0")\isanewline 

10295  1335 
\isacommand{apply}\ (simp_all)\isanewline 
1336 
\isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline 

1337 
\isacommand{done}% 

1338 
\end{isabelle} 

1339 
Notice that the induction formula 

1340 
is a conjunction. This is necessary: in the inductive step, each 

1341 
half of the conjunction establishes the other. The first three proof steps 

1342 
are applying induction, performing a case analysis on \isa{n}, 

10854  1343 
and simplifying. Let us pass over these quickly  we shall discuss 
1344 
\isa{case_tac} below  and consider the use of \isa{blast}. We have reached the 

1345 
following subgoal: 

10295  1346 
\begin{isabelle} 
1347 
%gcd\ (m,\ n)\ dvd\ m\ \isasymand\ gcd\ (m,\ n)\ dvd\ n\isanewline 

10596  1348 
\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk0\ \isacharless\ n;\isanewline 
1349 
\ \ \ \ \ \ \ \ \ \ \ \ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand\ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n)\isasymrbrakk\isanewline 

10546  1350 
\ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ gcd\ (n,\ m\ mod\ n)\ dvd\ m 
10295  1351 
\end{isabelle} 
1352 
% 

1353 
One of the assumptions, the induction hypothesis, is a conjunction. 

1354 
The two divides relationships it asserts are enough to prove 

1355 
the conclusion, for we have the following theorem at our disposal: 

1356 
\begin{isabelle} 

1357 
\isasymlbrakk?k\ dvd\ (?m\ mod\ ?n){;}\ ?k\ dvd\ ?n\isasymrbrakk\ \isasymLongrightarrow\ ?k\ dvd\ ?m% 

1358 
\rulename{dvd_mod_imp_dvd} 

1359 
\end{isabelle} 

1360 
% 

1361 
This theorem can be applied in various ways. As an introduction rule, it 

1362 
would cause backward chaining from the conclusion (namely 

10854  1363 
\isa{?k~dvd~?m}) to the two premises, which 
10295  1364 
also involve the divides relation. This process does not look promising 
1365 
and could easily loop. More sensible is to apply the rule in the forward 

10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1366 
direction; each step would eliminate an occurrence of the \isa{mod} symbol, so the 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1367 
process must terminate. 
10295  1368 

1369 
So the final proof step applies the \isa{blast} method. 

1370 
Attaching the {\isa{dest}} attribute to \isa{dvd_mod_imp_dvd} tells \isa{blast} 

1371 
to use it as destruction rule: in the forward direction. 

1372 