author  paulson 
Wed, 10 Jan 2001 11:12:45 +0100  
changeset 10848  7b3ee4695fe6 
parent 10792  78dfc5904eea 
child 10854  d1ff1ff5c5ad 
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}. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

877 
One final remark: applying \isa{spec} by the command 
10295  878 
\begin{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

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

881 
does not work the second time. It adds a second copy of \isa{P(h\ a)} instead of 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

882 
the desired assumption, \isa{P(h(h\ a))}. We have used the \isacommand{by} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

883 
command, which causes Isabelle to backtrack until it finds the correct one. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

884 
Equivalently, we could have used the \isacommand{apply} command and bundled the 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

885 
\isa{drule mp} with two \isa{assumption} calls. 
10295  886 

887 

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

888 
\subsection{The Existential Quantifier} 
10295  889 

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

891 
whose introduction rule looks like this in Isabelle: 

892 
\begin{isabelle} 

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

894 
\end{isabelle} 

895 
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

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

899 
in a logic text: 

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

901 
% 

902 
It looks like this in Isabelle: 

903 
\begin{isabelle} 

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

907 
Given an existentially quantified theorem and some 

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

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

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

911 
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

912 
quantifier to be built in as well. 
10295  913 

914 

915 
\begin{exercise} 

916 
Prove the lemma 

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

918 
\emph{Hint}: the proof is similar 

919 
to the one just above for the universal quantifier. 

920 
\end{exercise} 

921 

922 

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

923 
\section{Hilbert's $\epsilon$Operator} 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

924 

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

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

926 
$\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

927 
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

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

929 
\[ \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

930 
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

931 

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

932 
\subsection{Definite Descriptions} 
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 
In ASCII, we write \isa{SOME} for $\epsilon$. 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

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

936 
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

937 
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

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

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

940 
\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

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

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

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

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

945 
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

946 
$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

947 
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

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

949 

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

950 
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

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

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

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

954 
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

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

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

957 
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

958 
\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

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

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

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

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

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

964 

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

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

966 
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

967 
\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

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

969 

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

970 

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

971 
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

972 
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

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

974 
(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

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

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

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

978 

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

979 
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

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

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

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

983 
\ \ \ \ \ "\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

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

985 
%\ 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

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

987 
%\ \ \ \ \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

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

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

990 
\ 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

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

992 
(\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

993 
\ 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

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

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

996 

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

997 
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

998 
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

999 
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

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

1001 
\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

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

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

1004 
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

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

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

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

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

1009 

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

1010 

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

1011 
\subsection{Indefinite Descriptions} 
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 
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

1014 
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

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

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

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

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

1019 
\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

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

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

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

1023 
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

1024 
\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

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

1026 

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

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

1028 
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

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

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

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

1032 
\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

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

1034 
\ 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

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

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

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

1038 
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

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

1040 

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

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

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

1043 
\ 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

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

1045 

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

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

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

1048 
\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

1049 
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

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

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

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

1053 

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

1054 

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

1055 
\section{Some Proofs That Fail} 
10295  1056 

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

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

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

1060 
the existential quantifier and conjunction. 

1061 
\begin{isabelle} 

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

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

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

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

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

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

1068 
\ \isacommand{apply}\ assumption\isanewline 

1069 
\isacommand{oops} 

1070 
\end{isabelle} 

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

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

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

1074 
the quantifiers. 

1075 
\begin{isabelle} 

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

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

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

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

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

1083 
\begin{isabelle} 

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

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

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

1089 
no way to prove this subgoal. Removing the 

1090 
conclusion's existential quantifier yields two 

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

1091 
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

1092 
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

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

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

1101 
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

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

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

1107 
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

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

1111 
\end{isabelle} 

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

1113 

1114 
\medskip 

1115 

1116 
Here is another abortive proof, illustrating the interaction between 

1117 
bound variables and unknowns. 

1118 
If $R$ is a reflexive relation, 

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

1120 
we attempt to prove it. 

1121 
\begin{isabelle} 

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

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

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

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

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

1127 
\isacommand{oops} 

1128 
\end{isabelle} 

1129 
First, 

1130 
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

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

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

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

1136 
\end{isabelle} 

1137 
Next, we remove the universal quantifier 

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

1139 
\begin{isabelle} 

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

1143 
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

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

1148 
This subgoal can only be proved by putting \isa{y} for all the placeholders, 
10295  1149 
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

1150 
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

1151 
\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

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

1154 
\isa{?z2} to the identity function. 
10295  1155 

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

1157 

1158 

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

1159 
\section{Proving Theorems Using the {\tt\slshape blast} Method} 
10295  1160 

1161 
It is hard to prove substantial theorems using the methods 

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

1163 
may need to search among different ways of proving certain 

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

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

1166 
discussed, concerning negation and disjunction. Isabelle's 

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

1168 
proofs automatically. The most important of these is the 

10596  1169 
\isa{blast} method. 
10295  1170 

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

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

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

1174 

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

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

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

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

1179 
problems for automatic theorem provers.} 

1180 
The nested biconditionals cause an exponential explosion: the formal 

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

1184 
\isacommand{lemma}\ 

1185 
"(({\isasymexists}x.\ 

1186 
{\isasymforall}y.\ 

10301  1187 
p(x){=}p(y))\ 
10295  1188 
=\ 
1189 
(({\isasymexists}x.\ 

10301  1190 
q(x))=({\isasymforall}y.\ 
1191 
p(y))))\ 

10295  1192 
\ \ =\ \ \ \ \isanewline 
1193 
\ \ \ \ \ \ \ \ 

1194 
(({\isasymexists}x.\ 

1195 
{\isasymforall}y.\ 

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

1196 
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

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

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

1203 
can be proved. 

1204 
\begin{isabelle} 

1205 
\isacommand{lemma}\ 

1206 
"({\isasymforall}x.\ 

1207 
honest(x)\ \isasymand\ 

1208 
industrious(x)\ \isasymlongrightarrow\ 

10301  1209 
healthy(x))\ 
10295  1210 
\isasymand\ \ \isanewline 
1211 
\ \ \ \ \ \ \ \ \isasymnot\ ({\isasymexists}x.\ 

1212 
grocer(x)\ \isasymand\ 

10301  1213 
healthy(x))\ 
10295  1214 
\isasymand\ \isanewline 
1215 
\ \ \ \ \ \ \ \ ({\isasymforall}x.\ 

1216 
industrious(x)\ \isasymand\ 

1217 
grocer(x)\ \isasymlongrightarrow\ 

10301  1218 
honest(x))\ 
10295  1219 
\isasymand\ \isanewline 
1220 
\ \ \ \ \ \ \ \ ({\isasymforall}x.\ 

1221 
cyclist(x)\ \isasymlongrightarrow\ 

10301  1222 
industrious(x))\ 
10295  1223 
\isasymand\ \isanewline 
1224 
\ \ \ \ \ \ \ \ ({\isasymforall}x.\ 

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

1226 
cyclist(x)\ \isasymlongrightarrow\ 

10301  1227 
{\isasymnot}honest(x))\ 
10295  1228 
\ \isanewline 
1229 
\ \ \ \ \ \ \ \ \isasymlongrightarrow\ 

1230 
({\isasymforall}x.\ 

1231 
grocer(x)\ \isasymlongrightarrow\ 

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

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

1238 
\begin{isabelle} 

10301  1239 
\isacommand{lemma}\ "({\isasymUnion}i{\isasymin}I.\ A(i))\ \isasyminter\ ({\isasymUnion}j{\isasymin}J.\ B(j))\ =\isanewline 
1240 
\ \ \ \ \ \ \ \ ({\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

1241 
\isacommand{by}\ blast 
10295  1242 
\end{isabelle} 
1243 

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

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

1246 
Extending it effectively requires understanding the notions of 

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

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

1249 
that can be applied backwards without losing information; an 

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

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

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

1253 
classical reasoner backtracks to the most recent unsafe rule application 

1254 
and makes another choice. 

1255 

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

1257 
equivalence, which in higherorder logic is an equality between 

1258 
formulas, can be given to the classical 

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

1262 

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

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

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

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

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

1270 
\isacommand{lemma}\ 

10301  1271 
[iff]:\ 
10295  1272 
"(xs{\isacharat}ys\ =\ 
1273 
\isacharbrackleft{]})\ =\ 

1274 
(xs=[]\ 

1275 
\isacharampersand\ 

10301  1276 
ys=[])"\isanewline 
10295  1277 
\isacommand{apply}\ (induct_tac\ 
1278 
xs)\isanewline 

1279 
\isacommand{apply}\ (simp_all) 

1280 
\isanewline 

1281 
\isacommand{done} 

1282 
\end{isabelle} 

1283 
% 

1284 
This fact about multiplication is also appropriate for 

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

1285 
the \isa{iff} attribute: 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1286 
%%\REMARK{the ?s are ugly here but we need 
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1287 
%% them again when talking about \isa{of}; we need a consistent style} 
10295  1288 
\begin{isabelle} 
10596  1289 
(\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0) 
10295  1290 
\end{isabelle} 
1291 
A product is zero if and only if one of the factors is zero. The 

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

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

1294 
works: the classical reasoner handles disjunction properly. 

1295 

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

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

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

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

1302 
simplifier. But classical reasoning is different from 

1303 
simplification. Simplification is deterministic: it applies rewrite rules 

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

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

1306 

1307 

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

1308 
\section{Proving the Correctness of Euclid's Algorithm} 
10295  1309 
\label{sec:provingeuclid} 
1310 

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

1311 
A brief development will illustrate the advanced use of 
10295  1312 
\isa{blast}. In \S\ref{sec:recdefsimplification}, we declared the 
10596  1313 
recursive function \isa{gcd}: 
10295  1314 
\begin{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

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

1321 
divisor of its two arguments. 

1322 
% 

1323 
%The declaration yields a recursion 

10596  1324 
%equation for \isa{gcd}. Simplifying with this equation can 
10295  1325 
%cause looping, expanding to everlarger expressions of ifthenelse 
10596  1326 
%and \isa{gcd} calls. To prevent this, we prove separate simplification rules 
10295  1327 
%for $n=0$\ldots 
1328 
%\begin{isabelle} 

10301  1329 
%\isacommand{lemma}\ gcd_0\ [simp]:\ "gcd(m,0)\ =\ m"\isanewline 
10295  1330 
%\isacommand{apply}\ (simp)\isanewline 
1331 
%\isacommand{done} 

1332 
%\end{isabelle} 

1333 
%\ldots{} and for $n>0$: 

1334 
%\begin{isabelle} 

10301  1335 
%\isacommand{lemma}\ gcd_non_0:\ "0{\isacharless}n\ \isasymLongrightarrow\ gcd(m,n)\ =\ gcd\ (n,\ m\ mod\ n)"\isanewline 
10295  1336 
%\isacommand{apply}\ (simp)\isanewline 
1337 
%\isacommand{done} 

1338 
%\end{isabelle} 

1339 
%This second rule is similar to the original equation but 

1340 
%does not loop because it is conditional. It can be applied only 

1341 
%when the second argument is known to be nonzero. 

1342 
%Armed with our two new simplification rules, we now delete the 

10596  1343 
%original \isa{gcd} recursion equation. 
10295  1344 
%\begin{isabelle} 
10301  1345 
%\isacommand{declare}\ gcd.simps\ [simp\ del] 
10295  1346 
%\end{isabelle} 
1347 
% 

10596  1348 
%Now we can prove some interesting facts about the \isa{gcd} function, 
10295  1349 
%for exampe, that it computes a common divisor of its arguments. 
1350 
% 

1351 
The theorem is expressed in terms of the familiar 

1352 
\textbf{divides} relation from number theory: 

1353 
\begin{isabelle} 

10596  1354 
?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k 
10295  1355 
\rulename{dvd_def} 
1356 
\end{isabelle} 

1357 
% 

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

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

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

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

1362 
\begin{isabelle} 

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

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

10295  1366 
\isacommand{apply}\ (simp_all)\isanewline 
1367 
\isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline 

1368 
\isacommand{done}% 

1369 
\end{isabelle} 

8eb12693cead
the Rules chapter and theories
pa 