author  paulson 
Wed, 16 May 2001 17:58:48 +0200  
changeset 11300  5b6887aedc76 
parent 11255  ca546b170471 
child 11406  2b17622e1929 
permissions  rwrr 
10792  1 
% $Id$ 
10295  2 
\chapter{The Rules of the Game} 
3 
\label{chap:rules} 

4 

11077  5 
This chapter outlines the concepts and techniques that underlie reasoning 
6 
in Isabelle. Until now, we have proved everything using only induction and 

7 
simplification, but any serious verification project require more elaborate 

8 
forms of inference. The chapter also introduces the fundamentals of 

9 
predicate logic. The first examples in this chapter will consist of 

10 
detailed, lowlevel proof steps. Later, we shall see how to automate such 

11 
reasoning using the methods 

12 
\isa{blast}, 

13 
\isa{auto} and others. Backward or goaldirected proof is our usual style, 

14 
but the chapter also introduces forward reasoning, where one theorem is 

15 
transformed to yield another. 

10295  16 

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

17 
\section{Natural Deduction} 
10295  18 

11077  19 
\index{natural deduction(}% 
10295  20 
In Isabelle, proofs are constructed using inference rules. The 
21 
most familiar inference rule is probably \emph{modus ponens}: 

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

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

24 
we may infer~$Q$. 

25 

26 
%Early logical formalisms had this 

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

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

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

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

31 
%these two axioms (amongst others): 

32 
%\begin{gather*} 

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

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

35 
%\end{gather*} 

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

37 
%ponens}! 

38 

11077  39 
\emph{Natural deduction} is an attempt to formalize logic in a way 
10295  40 
that mirrors human reasoning patterns. 
41 
% 

42 
%Instead of having a few 

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

44 
%and few axioms. 

45 
% 

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

11077  47 
are two kinds of rules: \emph{introduction} and \emph{elimination} rules. 
10295  48 
The introduction rules allow us to infer this symbol (say, to 
49 
infer conjunctions). The elimination rules allow us to deduce 

50 
consequences from this symbol. Ideally each rule should mention 

51 
one symbol only. For predicate logic this can be 

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

11255  53 
have to refer to other symbols as well. It is best not to be dogmatic. 
10295  54 

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

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

57 
applying the corresponding rule. It creates new subgoals in 

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

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

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

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

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

63 
Isabelle's 

11077  64 
\emph{classical reasoner} accepts any suitable collection of natural deduction 
10295  65 
rules and uses them to search for proofs automatically. Isabelle is designed around 
11077  66 
natural deduction and many of its tools use the terminology of introduction 
67 
and elimination rules.% 

68 
\index{natural deduction)} 

10295  69 

70 

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

71 
\section{Introduction Rules} 
10295  72 

11077  73 
\index{introduction rules(}% 
74 
An introduction rule tells us when we can infer a formula 

10295  75 
containing a specific logical symbol. For example, the conjunction 
76 
introduction rule says that if we have $P$ and if we have $Q$ then 

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

78 
like this: 

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

80 
The rule introduces the conjunction 

10971  81 
symbol~($\conj$) in its conclusion. In Isabelle proofs we 
10295  82 
mainly reason backwards. When we apply this rule, the subgoal already has 
83 
the form of a conjunction; the proof step makes this conjunction symbol 

84 
disappear. 

85 

86 
In Isabelle notation, the rule looks like this: 

87 
\begin{isabelle} 

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

89 
\end{isabelle} 

90 
Carefully examine the syntax. The premises appear to the 

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

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

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

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

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

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

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

98 
it yields new subgoals given by the formulas assigned to 

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

100 

101 
The following trivial proof illustrates this point. 

102 
\begin{isabelle} 

10596  103 
\isacommand{lemma}\ conj_rule:\ "\isasymlbrakk P;\ 
10295  104 
Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ 
10301  105 
(Q\ \isasymand\ P)"\isanewline 
10295  106 
\isacommand{apply}\ (rule\ conjI)\isanewline 
107 
\ \isacommand{apply}\ assumption\isanewline 

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

109 
\ \isacommand{apply}\ assumption\isanewline 

110 
\isacommand{apply}\ assumption 

111 
\end{isabelle} 

112 
At the start, Isabelle presents 

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

114 
\isa{P\ \isasymand\ 

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

116 
apply conjunction introduction, the rule removes the outermost occurrence 

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

10596  118 
the proof method \isa{rule}  here with {\isa{conjI}}, the conjunction 
10295  119 
introduction rule. 
120 
\begin{isabelle} 

10596  121 
%\isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\ 
10295  122 
%\isasymand\ P\isanewline 
10596  123 
\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline 
124 
\ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P 

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

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

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

10596  131 
\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ 
10295  132 
Q\ \isasymand\ P 
133 
\end{isabelle} 

134 
We are left with the subgoal of proving 

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

136 
\isa{rule conjI} again. 

137 
\begin{isabelle} 

10596  138 
\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline 
139 
\ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P 

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

11077  142 
using the \isa{assumption} method.% 
143 
\index{introduction rules)} 

10295  144 

145 

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

146 
\section{Elimination Rules} 
10295  147 

11077  148 
\index{elimination rules(}% 
149 
Elimination rules work in the opposite direction from introduction 

10295  150 
rules. In the case of conjunction, there are two such rules. 
151 
From $P\conj Q$ we infer $P$. also, from $P\conj Q$ 

152 
we infer $Q$: 

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

154 

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

156 
conjunction elimination rules: 

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

158 

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

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

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

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

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

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

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

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

11077  167 
deduction: that of the \emph{assumptions}. We have to prove $R$ twice, under 
10295  168 
different assumptions. The assumptions are local to these subproofs and are visible 
169 
nowhere else. 

170 

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

172 
like this: 

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

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

175 
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

176 
notation, the alreadyfamiliar \isa{\isasymLongrightarrow} syntax serves the 
10295  177 
same purpose: 
178 
\begin{isabelle} 

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

180 
\end{isabelle} 

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

10971  182 
a case split. (We have seen this before, in proofs by induction.) The following proof 
10295  183 
illustrates the use of disjunction elimination. 
184 
\begin{isabelle} 

10301  185 
\isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\ 
10295  186 
\isasymLongrightarrow\ Q\ \isasymor\ P"\isanewline 
187 
\isacommand{apply}\ (erule\ disjE)\isanewline 

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

189 
\ \isacommand{apply}\ assumption\isanewline 

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

191 
\isacommand{apply}\ assumption 

192 
\end{isabelle} 

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

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

11077  195 
elimination rule, \isa{disjE}. We invoke it using \isa{erule}, a method 
196 
designed to work with elimination rules. It looks for an assumption that 

197 
matches the rule's first premise. It deletes the matching assumption, 

198 
regards the first premise as proved and returns subgoals corresponding to 

199 
the remaining premises. When we apply \isa{erule} to \isa{disjE}, only two 

200 
subgoals result. This is better than applying it using \isa{rule} 

201 
to get three subgoals, then proving the first by assumption: the other 

202 
subgoals would have the redundant assumption 

203 
\hbox{\isa{P\ \isasymor\ Q}}. 

204 
Most of the 

205 
time, \isa{erule} is the best way to use elimination rules. Only rarely 

206 
can an assumption be used more than once. 

10295  207 

208 
\begin{isabelle} 

209 
%P\ \isasymor\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline 

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

211 
\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P 

212 
\end{isabelle} 

11077  213 
These are the two subgoals returned by \isa{erule}. The first assumes 
214 
\isa{P} and the second assumes \isa{Q}. Tackling the first subgoal, we 

215 
need to show \isa{Q\ \isasymor\ P}\@. The second introduction rule 

216 
(\isa{disjI2}) can reduce this to \isa{P}, which matches the assumption. 

217 
So, we apply the 

10596  218 
\isa{rule} method with \isa{disjI2} \ldots 
10295  219 
\begin{isabelle} 
220 
\ 1.\ P\ \isasymLongrightarrow\ P\isanewline 

221 
\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P 

222 
\end{isabelle} 

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

226 
\begin{isabelle} 

227 
\ 1.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P 

228 
\end{isabelle} 

229 
Its proof is similar, using the introduction 

230 
rule \isa{disjI1}. 

231 

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

233 
an introduction nor an elimination rule, but which might 

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

11077  235 
by a one of the form $P\disj Q$.% 
236 
\index{elimination rules)} 

10295  237 

238 

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

239 
\section{Destruction Rules: Some Examples} 
10295  240 

11077  241 
\index{destruction rules(}% 
10295  242 
Now let us examine the analogous proof for conjunction. 
243 
\begin{isabelle} 

10301  244 
\isacommand{lemma}\ conj_swap:\ "P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P"\isanewline 
10295  245 
\isacommand{apply}\ (rule\ conjI)\isanewline 
246 
\ \isacommand{apply}\ (drule\ conjunct2)\isanewline 

247 
\ \isacommand{apply}\ assumption\isanewline 

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

249 
\isacommand{apply}\ assumption 

250 
\end{isabelle} 

251 
Recall that the conjunction elimination rules  whose Isabelle names are 

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

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

11077  254 
premise) are called \emph{destruction} rules because they take apart and destroy 
10978  255 
a premise.% 
10295  256 
\footnote{This Isabelle terminology has no counterpart in standard logic texts, 
257 
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

258 
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

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

262 

263 
The first proof step applies conjunction introduction, leaving 

264 
two subgoals: 

265 
\begin{isabelle} 

266 
%P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P\isanewline 

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

268 
\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P 

269 
\end{isabelle} 

270 

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

11077  272 
Think of the \isa{d} as standing for \emph{destruction} (or \emph{direct}, if 
10295  273 
you prefer). Applying the 
274 
second conjunction rule using \isa{drule} replaces the assumption 

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

276 
\begin{isabelle} 

277 
\ 1.\ Q\ \isasymLongrightarrow\ Q\isanewline 

278 
\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P 

279 
\end{isabelle} 

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

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

282 
\isa{assumption} method. 

283 

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

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

286 
is an introduction rule or an elimination rule. The 

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

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

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

290 
assumption of the form 

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

292 

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

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

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

296 
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

297 
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

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

301 
\end{isabelle} 

11077  302 
\index{destruction rules)} 
10295  303 

304 
\begin{exercise} 

11077  305 
Use the rule \isa{conjE} to shorten the proof above. 
10295  306 
\end{exercise} 
307 

308 

309 
\section{Implication} 

310 

11077  311 
\index{implication(}% 
10295  312 
At the start of this chapter, we saw the rule \textit{modus ponens}. It is, in fact, 
313 
a destruction rule. The matching introduction rule looks like this 

314 
in Isabelle: 

315 
\begin{isabelle} 

316 
(?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\ 

317 
\isasymlongrightarrow\ ?Q\rulename{impI} 

318 
\end{isabelle} 

319 
And this is \textit{modus ponens}: 

320 
\begin{isabelle} 

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

322 
\isasymLongrightarrow\ ?Q 

323 
\rulename{mp} 

324 
\end{isabelle} 

325 

11077  326 
Here is a proof using the implication rules. This 
10295  327 
lemma performs a sort of uncurrying, replacing the two antecedents 
11077  328 
of a nested implication by a conjunction. The proof illustrates 
329 
how assumptions work. At each proof step, the subgoals inherit the previous 

330 
assumptions, perhaps with additions or deletions. Rules such as 

331 
\isa{impI} and \isa{disjE} add assumptions, while applying \isa{erule} or 

332 
\isa{drule} deletes the matching assumption. 

10295  333 
\begin{isabelle} 
334 
\isacommand{lemma}\ imp_uncurry:\ 

10301  335 
"P\ \isasymlongrightarrow\ (Q\ 
10295  336 
\isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\ 
337 
\isasymand\ Q\ \isasymlongrightarrow\ 

338 
R"\isanewline 

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

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

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

342 
\ \isacommand{apply}\ assumption\isanewline 

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

344 
\ \ \isacommand{apply}\ assumption\isanewline 

345 
\ \isacommand{apply}\ assumption 

346 
\end{isabelle} 

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

348 
which moves the conjunction to the assumptions. 

349 
\begin{isabelle} 

350 
%P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R\ \isasymLongrightarrow\ P\ 

351 
%\isasymand\ Q\ \isasymlongrightarrow\ R\isanewline 

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

355 
conjunction into two parts. 

356 
\begin{isabelle} 

10596  357 
\ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\ 
10295  358 
Q\isasymrbrakk\ \isasymLongrightarrow\ R 
359 
\end{isabelle} 

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

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

362 
clarity. The nested implication requires two applications of 

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

364 
implication \isa{Q\ 

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

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

367 
\begin{isabelle} 

10596  368 
\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline 
369 
\ 2.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R 

10295  370 
\end{isabelle} 
371 
Repeating these steps for \isa{Q\ 

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

373 
\begin{isabelle} 

10596  374 
\ 1.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ 
10295  375 
\isasymLongrightarrow\ R 
376 
\end{isabelle} 

377 

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

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

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

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

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

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

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

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

386 
context that requires a formula of higherorder logic. Use 

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

11077  388 
conclusion.% 
389 
\index{implication)} 

10295  390 

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

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

392 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

409 
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

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

411 
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

412 
oneline proof. 
10295  413 

414 

415 
\section{Negation} 

416 

11077  417 
\index{negation(}% 
10295  418 
Negation causes surprising complexity in proofs. Its natural 
419 
deduction rules are straightforward, but additional rules seem 

11077  420 
necessary in order to handle negated assumptions gracefully. This section 
421 
also illustrates the \isa{intro} method: a convenient way of 

422 
applying introduction rules. 

10295  423 

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

425 
contradiction. Negation elimination deduces any formula in the 

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

427 
\begin{isabelle} 

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

429 
\rulename{notI}\isanewline 

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

431 
\rulename{notE} 

432 
\end{isabelle} 

433 
% 

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

435 
when attempting to prove~$P$: 

436 
\begin{isabelle} 

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

438 
\rulename{classical} 

439 
\end{isabelle} 

11077  440 

441 
The implications $P\imp Q$ and $\neg Q\imp\neg P$ are logically 

442 
equivalent, and each is called the 

443 
\bfindex{contrapositive} of the other. Three further rules support 

444 
reasoning about contrapositives. They differ in the placement of the 

445 
negation symbols: 

10295  446 
\begin{isabelle} 
447 
\isasymlbrakk?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% 

448 
\rulename{contrapos_pp}\isanewline 

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

450 
\rulename{contrapos_np}\isanewline 

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

452 
\rulename{contrapos_nn} 

453 
\end{isabelle} 

454 
% 

11077  455 
These rules are typically applied using the \isa{erule} method, where 
10295  456 
their effect is to form a contrapositive from an 
457 
assumption and the goal's conclusion. 

458 

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

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

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

462 
might want to use conjunction introduction on it. 

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

464 
becomes the conclusion. The following proof demonstrates this 

465 
technique: 

466 
\begin{isabelle} 

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

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

469 
R"\isanewline 

10971  470 
\isacommand{apply}\ (erule_tac\ Q = "R{\isasymlongrightarrow}Q"\ \isakeyword{in}\ 
10295  471 
contrapos_np)\isanewline 
472 
\isacommand{apply}\ intro\isanewline 

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

473 
\isacommand{by}\ (erule\ notE) 
10295  474 
\end{isabelle} 
475 
% 

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

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

11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

478 
which we do not want. So we specify the desired assumption explicitly 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

479 
using a new method, \isa{erule_tac}. This is the resulting subgoal: 
10295  480 
\begin{isabelle} 
481 
\ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ 

482 
R\isasymrbrakk\ \isasymLongrightarrow\ R\ \isasymlongrightarrow\ Q% 

483 
\end{isabelle} 

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

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

486 
conclusion. 

487 

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

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

10596  490 
to \isa{rule impI}. 
491 
\begin{isabelle} 

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

494 
\end{isabelle} 

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

496 
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

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

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

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

10971  502 
assumption \isa{\isasymnot~R} and finally proves \isa{R} by assumption. That 
10295  503 
concludes the proof. 
504 

505 
\medskip 

506 

11077  507 
The following example may be skipped on a first reading. It involves a 
508 
peculiar but important rule, a form of disjunction introduction: 

509 
\begin{isabelle} 

510 
(\isasymnot \ ?Q\ \isasymLongrightarrow \ ?P)\ \isasymLongrightarrow \ ?P\ \isasymor \ ?Q% 

511 
\rulename{disjCI} 

512 
\end{isabelle} 

513 
This rule combines the effects of \isa{disjI1} and \isa{disjI2}. Its great 

514 
advantage is that we can remove the disjunction symbol without deciding 

515 
which disjunction to prove.% 

516 
\footnote{This type of reasoning is standard in sequent and tableau 

517 
calculi.} 

518 

10295  519 
\begin{isabelle} 
520 
\isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\ 

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

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

522 
\isacommand{apply}\ intro\isanewline 
10295  523 
\isacommand{apply}\ (elim\ conjE\ disjE)\isanewline 
524 
\ \isacommand{apply}\ assumption 

525 
\isanewline 

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

526 
\isacommand{by}\ (erule\ contrapos_np,\ rule\ conjI) 
10295  527 
\end{isabelle} 
528 
% 

11077  529 
The first proof step applies the \isa{intro} method, which repeatedly uses 
530 
builtin introduction rules. Among these are \isa{disjCI}, which creates 

531 
the negative assumption 

532 
\hbox{\isa{\isasymnot(Q\ \isasymand\ R)}}. 

533 

10295  534 
\begin{isabelle} 
535 
\ 1.\ \isasymlbrakk(P\ \isasymor\ Q)\ \isasymand\ R;\ \isasymnot\ (Q\ \isasymand\ 

536 
R)\isasymrbrakk\ \isasymLongrightarrow\ P% 

537 
\end{isabelle} 

11077  538 
Next we apply the \isa{elim} method, which repeatedly applies 
10295  539 
elimination rules; here, the elimination rules given 
10971  540 
in the command. One of the subgoals is trivial (\isa{\isacommand{apply} assumption}), 
541 
leaving us with one other: 

10295  542 
\begin{isabelle} 
543 
\ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P% 

544 
\end{isabelle} 

545 
% 

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

547 
combination 

548 
\begin{isabelle} 

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

550 
\end{isabelle} 

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

10301  552 
conjunction. The two subgoals are the ones we would expect from applying 
10295  553 
conjunction introduction to 
10971  554 
\isa{Q~\isasymand~R}: 
10295  555 
\begin{isabelle} 
10596  556 
\ 1.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ 
10295  557 
Q\isanewline 
10596  558 
\ 2.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R% 
10295  559 
\end{isabelle} 
11077  560 
They are proved by assumption, which is implicit in the \isacommand{by} 
561 
command.% 

562 
\index{negation)} 

563 

564 

11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

565 
\section{Interlude: the Basic Methods for Rules} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

566 

bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

567 
We have seen examples of many tactics that operate on individual rules. It 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

568 
may be helpful to review how they work given an arbitrary rule such as this: 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

569 
\[ \infer{Q}{P@1 & \ldots & P@n} \] 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

570 
Below, we refer to $P@1$ as the \textbf{major premise}. This concept 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

571 
applies only to elimination and destruction rules. These rules act upon an 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

572 
instance of their major premise, typically to replace it by other 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

573 
assumptions. 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

574 

bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

575 
Suppose that the rule above is called~\isa{R}\@. Here are the basic rule 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

576 
methods, most of which we have already seen: 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

577 
\begin{itemize} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

578 
\item 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

579 
Method \isa{rule\ R} unifies~$Q$ with the current subgoal, which it 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

580 
replaces by $n$ new subgoals, to prove instances of $P@1$, \ldots,~$P@n$. 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

581 
This is backward reasoning and is appropriate for introduction rules. 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

582 
\item 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

583 
Method \isa{erule\ R} unifies~$Q$ with the current subgoal and 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

584 
simultaneously unifies $P@1$ with some assumption. The subgoal is 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

585 
replaced by the $n1$ new subgoals of proving 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

586 
instances of $P@2$, 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

587 
\ldots,~$P@n$, with the matching assumption deleted. It is appropriate for 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

588 
elimination rules. The method 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

589 
\isa{(rule\ R,\ assumption)} is similar, but it does not delete an 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

590 
assumption. 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

591 
\item 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

592 
Method \isa{drule\ R} unifies $P@1$ with some assumption, which is 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

593 
then deleted. The subgoal is 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

594 
replaced by the $n1$ new subgoals of proving $P@2$, \ldots,~$P@n$; an 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

595 
$n$th subgoal is like the original one but has an additional assumption: an 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

596 
instance of~$Q$. It is appropriate for destruction rules. 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

597 
\item 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

598 
Method \isa{frule\ R} is like \isa{drule\ R} except that the matching 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

599 
assumption is not deleted. (See \S\ref{sec:frule} below.) 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

600 
\end{itemize} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

601 

bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

602 
When applying a rule, we can constrain some of its 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

603 
variables: 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

604 
\begin{isabelle} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

605 
\ \ \ \ \ rule_tac\ $v@1$ = $t@1$ \isakeyword{and} \ldots \isakeyword{and} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

606 
$v@k$ = 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

607 
$t@k$ \isakeyword{in} R 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

608 
\end{isabelle} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

609 
This method behaves like \isa{rule R}, while instantiating the variables 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

610 
$v@1$, \ldots, 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

611 
$v@k$ as specified. We similarly have \isa{erule_tac}, \isa{drule_tac} and 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

612 
\isa{frule_tac}. These methods also let us specify which subgoal to 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

613 
operate on. By default it is the first subgoal, as with nearly all 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

614 
methods, but we can specify that rule \isa{R} should be applied to subgoal 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

615 
number~$i$: 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

616 
\begin{isabelle} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

617 
\ \ \ \ \ rule_tac\ [$i$] R 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

618 
\end{isabelle} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

619 

bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

620 

bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

621 

bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

622 

11077  623 
\section{Unification and Substitution}\label{sec:unification} 
624 

625 
\index{unification(}% 

626 
As we have seen, Isabelle rules involve schematic variables that begin with 

627 
a question mark and act as 

628 
placeholders for terms. \emph{Unification} refers to the process of 

629 
making two terms identical, possibly by replacing their schematic variables by 

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

11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

631 
simplest is when the variables in only one of the term 
11077  632 
are replaced; this is called patternmatching. The 
633 
\isa{rule} method typically matches the rule's conclusion 

634 
against the current subgoal. In the most complex case, variables in both 

635 
terms are replaced; the \isa{rule} method can do this if the goal 

636 
itself contains schematic variables. Other occurrences of the variables in 

637 
the rule or proof state are updated at the same time. 

638 

639 
Schematic variables in goals represent unknown terms. Given a goal such 

640 
as $\exists x.\,P$, they let us proceed with a proof. They can be 

641 
filled in later, sometimes in stages and often automatically. 

642 

643 
Unification is well known to Prolog programmers. Isabelle uses 

644 
\emph{higherorder} unification, which works in the 

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

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

647 
unification are straightforward. It handles bound variables 

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

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

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

651 
bound. The two terms 

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

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

654 

655 
\begin{warn} 

656 
Higherorder unification sometimes must invent 

657 
$\lambda$terms to replace function variables, 

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

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

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

661 
function variable is applied only to bound variables, 

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

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

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

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

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

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

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

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

670 
\end{warn} 

671 

672 

11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

673 
\subsection{Substitution and the {\tt\slshape subst} Method} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

674 
\label{sec:subst} 
11077  675 

676 
\index{substitution(}% 

677 
Isabelle also uses function variables to express \emph{substitution}. 

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

679 
another if we know that two terms are equal. 

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

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

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

683 
designated by~$x$. For example, it can 

684 
derive symmetry of equality from reflexivity. Using $x=s$ for~$P$ 

685 
replaces just the first $s$ in $s=s$ by~$t$: 

686 
\[ \infer{t=s}{s=t & \infer{s=s}{}} \] 

687 

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

689 
\begin{isabelle} 

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

691 
?t 

692 
\rulename{ssubst} 

693 
\end{isabelle} 

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

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

696 
involving one bound variable whose occurrences identify the places 

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

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

699 

11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

700 
The \isa{simp} method replaces equals by equals, but the substitution 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

701 
rule gives us more control. The \isa{subst} method is the easiest way to 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

702 
use the substitution rule. Suppose a 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

703 
proof has reached this point: 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

704 
\begin{isabelle} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

705 
\ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \ \isasymLongrightarrow \ f\ z\ =\ x\ *\ y% 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

706 
\end{isabelle} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

707 
Now we wish to apply a commutative law: 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

708 
\begin{isabelle} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

709 
?m\ *\ ?n\ =\ ?n\ *\ ?m% 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

710 
\rulename{mult_commute} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

711 
\end{isabelle} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

712 
Isabelle rejects our first attempt: 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

713 
\begin{isabelle} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

714 
apply (simp add: mult_commute) 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

715 
\end{isabelle} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

716 
The simplifier notices the danger of looping and refuses to apply the 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

717 
rule.% 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

718 
\footnote{More precisely, it only applies such a rule if the new term is 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

719 
smaller under a specified ordering; here, \isa{x\ *\ y} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

720 
is already smaller than 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

721 
\isa{y\ *\ x}.} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

722 
% 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

723 
The \isa{subst} method applies \isa{mult_commute} exactly once. 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

724 
\begin{isabelle} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

725 
\isacommand{apply}\ (subst\ mult_commute)\isanewline 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

726 
\ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \ 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

727 
\isasymLongrightarrow \ f\ z\ =\ y\ *\ x% 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

728 
\end{isabelle} 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

729 
As we wanted, \isa{x\ *\ y} has become \isa{y\ *\ x}. 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

730 

bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

731 
\medskip 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

732 
The \isa{subst} method is convenient, but to see how it works, let us 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

733 
examine an explicit use of the rule \isa{ssubst}. 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

734 
Consider this proof: 
11077  735 
\begin{isabelle} 
736 
\isacommand{lemma}\ 

11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

737 
"\isasymlbrakk x\ =\ f\ x;\ odd(f\ x)\isasymrbrakk\ \isasymLongrightarrow\ 
11077  738 
odd\ x"\isanewline 
739 
\isacommand{by}\ (erule\ ssubst) 

740 
\end{isabelle} 

741 
% 

742 
The simplifier might loop, replacing \isa{x} by \isa{f x} and then by 

743 
\isa{f(f x)} and so forth. (Here \isa{simp} 

744 
can see the danger and would reorient the equality, but in more complicated 

745 
cases it can be fooled.) When we apply substitution, Isabelle replaces every 

746 
\isa{x} in the subgoal by \isa{f x} just once: it cannot loop. The 

747 
resulting subgoal is trivial by assumption, so the \isacommand{by} command 

748 
proves it implicitly. 

749 

11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

750 
We are using the \isa{erule} method it in a novel way. Hitherto, 
11077  751 
the conclusion of the rule was just a variable such as~\isa{?R}, but it may 
752 
be any term. The conclusion is unified with the subgoal just as 

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

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

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

756 
assumption. 

757 

758 

759 
\subsection{Unification and Its Pitfalls} 

760 

761 
Higherorder unification can be tricky. Here is an example, which you may 

762 
want to skip on your first reading: 

763 
\begin{isabelle} 

11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

764 
\isacommand{lemma}\ "\isasymlbrakk x\ =\ 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

765 
f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\ 
11077  766 
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline 
767 
\isacommand{apply}\ (erule\ ssubst)\isanewline 

768 
\isacommand{back}\isanewline 

769 
\isacommand{back}\isanewline 

770 
\isacommand{back}\isanewline 

771 
\isacommand{back}\isanewline 

772 
\isacommand{apply}\ assumption\isanewline 

773 
\isacommand{done} 

774 
\end{isabelle} 

775 
% 

776 
By default, Isabelle tries to substitute for all the 

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

778 
\begin{isabelle} 

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

780 
\end{isabelle} 

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

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

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

784 
\begin{isabelle} 

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

786 
\end{isabelle} 

787 
% 

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

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

790 
again: 

791 
\begin{isabelle} 

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

793 
\end{isabelle} 

794 
% 

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

796 
\begin{isabelle} 

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

798 
\end{isabelle} 

799 
% 

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

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

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

803 
\begin{isabelle} 

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

805 
\end{isabelle} 

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

807 
\index{unification)} 

808 

809 
\subsection{Keeping Unification under Control} 

810 

811 
The previous example showed that unification can do strange things with 

812 
function variables. We were forced to select the right unifier using the 

813 
\isa{back} command. That is all right during exploration, but \isa{back} 

814 
should never appear in the final version of a proof. You can eliminate the 

815 
need for \isa{back} by giving Isabelle less freedom when you apply a rule. 

816 

817 
One way to constrain the inference is by joining two methods in a 

818 
\isacommand{apply} command. Isabelle applies the first method and then the 

819 
second. If the second method fails then Isabelle automatically backtracks. 

820 
This process continues until the first method produces an output that the 

821 
second method can use. We get a oneline proof of our example: 

822 
\begin{isabelle} 

11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

823 
\isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\ 
11077  824 
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline 
825 
\isacommand{apply}\ (erule\ ssubst,\ assumption)\isanewline 

826 
\isacommand{done} 

827 
\end{isabelle} 

828 

829 
\noindent 

830 
The \isacommand{by} command works too, since it backtracks when 

831 
proving subgoals by assumption: 

832 
\begin{isabelle} 

11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

833 
\isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\ 
11077  834 
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline 
835 
\isacommand{by}\ (erule\ ssubst) 

836 
\end{isabelle} 

837 

838 

839 
The most general way to constrain unification is 

840 
by instantiating variables in the rule. The method \isa{rule_tac} is 

841 
similar to \isa{rule}, but it 

842 
makes some of the rule's variables denote specified terms. 

843 
Also available are {\isa{drule_tac}} and \isa{erule_tac}. Here we need 

844 
\isa{erule_tac} since above we used \isa{erule}. 

845 
\begin{isabelle} 

11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

846 
\isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

847 
\isacommand{by}\ (erule_tac\ P = "\isasymlambda u.\ triple\ u\ u\ x"\ 
11077  848 
\isakeyword{in}\ ssubst) 
849 
\end{isabelle} 

850 
% 

851 
To specify a desired substitution 

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

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

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

855 
the third unchanged. With this instantiation, backtracking is neither necessary 

856 
nor possible. 

857 

858 
An alternative to \isa{rule_tac} is to use \isa{rule} with the 

859 
\isa{of} directive, described in \S\ref{sec:forward} below. An 

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

861 
\isasymAndbound variables in the current subgoal.% 

862 
\index{substitution)} 

10295  863 

864 

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

865 
\section{Quantifiers} 
10295  866 

11077  867 
\index{quantifiers(}\index{quantifiers!universal(}% 
868 
Quantifiers require formalizing syntactic substitution and the notion of 

869 
\emph{arbitrary value}. Consider the universal quantifier. In a logic 

870 
book, its introduction rule looks like this: 

10295  871 
\[ \infer{\forall x.\,P}{P} \] 
872 
Typically, a proviso written in English says that $x$ must not 

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

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

875 
Isabelle's underlying formalism, called the 

11077  876 
\emph{metalogic}, eliminates the need for English. It provides its own universal 
10295  877 
quantifier (\isasymAnd) to express the notion of an arbitrary value. We have 
878 
already seen another symbol of the metalogic, namely 

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

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

881 
can be used to define constants. 

882 

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

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

884 

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

887 
\begin{isabelle} 

10596  888 
(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI} 
10295  889 
\end{isabelle} 
890 

891 

892 
The following trivial proof demonstrates how the universal introduction 

893 
rule works. 

894 
\begin{isabelle} 

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

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

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

897 
\isacommand{by}\ (rule\ impI) 
10295  898 
\end{isabelle} 
899 
The first step invokes the rule by applying the method \isa{rule allI}. 

900 
\begin{isabelle} 

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

11077  904 
namely~\isa{x}. The rule has replaced the universal quantifier of 
10295  905 
higherorder logic by Isabelle's metalevel quantifier. Our goal is to 
906 
prove 

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

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

909 
\begin{isabelle} 

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

912 
This last subgoal is implicitly proved by assumption. 
10295  913 

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

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

915 

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

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

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

920 
Isabelle expresses substitution using a function variable: 

921 
\begin{isabelle} 

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

923 
\end{isabelle} 

924 
This destruction rule takes a 

925 
universally quantified formula and removes the quantifier, replacing 

11077  926 
the bound variable \isa{x} by the schematic variable \isa{?x}. Recall that a 
10295  927 
schematic variable starts with a question mark and acts as a 
11077  928 
placeholder: it can be replaced by any term. 
10295  929 

11077  930 
The universal elimination rule is also 
931 
available in the standard elimination format. Like \isa{conjE}, it never 

932 
appears in logic books: 

933 
\begin{isabelle} 

934 
\isasymlbrakk \isasymforall x.\ ?P\ x;\ ?P\ ?x\ \isasymLongrightarrow \ ?R\isasymrbrakk \ \isasymLongrightarrow \ ?R% 

935 
\rulename{allE} 

936 
\end{isabelle} 

937 
The methods \isa{drule~spec} and \isa{erule~allE} do precisely the 

938 
same inference. 

939 

940 
To see how $\forall$elimination works, let us derive a rule about reducing 

10295  941 
the scope of a universal quantifier. In mathematical notation we write 
942 
\[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \] 

10978  943 
with the proviso ``$x$ not free in~$P$.'' Isabelle's treatment of 
10295  944 
substitution makes the proviso unnecessary. The conclusion is expressed as 
945 
\isa{P\ 

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

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

11077  948 
bound variable capture. Let us walk through the proof. 
10295  949 
\begin{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

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

951 
\isasymLongrightarrow \ P\ \isasymlongrightarrow \ (\isasymforall x.\ Q\ 
11077  952 
x)" 
10295  953 
\end{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

954 
First we apply implies introduction (\isa{impI}), 
10295  955 
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

956 
we apply universal introduction (\isa{allI}). 
10295  957 
\begin{isabelle} 
11077  958 
\isacommand{apply}\ (rule\ impI,\ rule\ allI)\isanewline 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

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

960 
x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x 
10295  961 
\end{isabelle} 
962 
As before, it replaces the HOL 

963 
quantifier by a metalevel quantifier, producing a subgoal that 

11077  964 
binds the variable~\isa{x}. The leading bound variables 
10295  965 
(here \isa{x}) and the assumptions (here \isa{{\isasymforall}x.\ P\ 
11077  966 
\isasymlongrightarrow\ Q\ x} and \isa{P}) form the \emph{context} for the 
967 
conclusion, here \isa{Q\ x}. Subgoals inherit the context, 

968 
although assumptions can be added or deleted (as we saw 

969 
earlier), while rules such as \isa{allI} add bound variables. 

10295  970 

971 
Now, to reason from the universally quantified 

10967  972 
assumption, we apply the elimination rule using the \isa{drule} 
10295  973 
method. This rule is called \isa{spec} because it specializes a universal formula 
974 
to a particular term. 

975 
\begin{isabelle} 

11077  976 
\isacommand{apply}\ (drule\ spec)\isanewline 
10596  977 
\ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ P\ \isasymlongrightarrow\ Q\ (?x2\ 
978 
x)\isasymrbrakk\ \isasymLongrightarrow\ Q\ x 

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

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

982 
removed the quantifier. The quantified variable 

983 
has been replaced by the curious term 

11077  984 
\isa{?x2~x}; it acts as a placeholder that may be replaced 
985 
by any term that can be built from~\isa{x}. (Formally, \isa{?x2} is an 

986 
unknown of function type, applied to the argument~\isa{x}.) This new assumption is 

987 
an implication, so we can use \emph{modus ponens} on it, which concludes 

988 
the proof. 

989 
\begin{isabelle} 

990 
\isacommand{by}\ (drule\ mp) 

991 
\end{isabelle} 

992 
Let us take a closer look at this last step. \emph{Modus ponens} yields 

993 
two subgoals: one where we prove the antecedent (in this case \isa{P}) and 

994 
one where we may assume the consequent. Both of these subgoals are proved 

995 
by the 

996 
\isa{assumption} method, which is implicit in the 

997 
\isacommand{by} command. Replacing the \isacommand{by} command by 

998 
\isa{\isacommand{apply} (drule\ mp, assumption)} would have left one last 

999 
subgoal: 

10295  1000 
\begin{isabelle} 
10596  1001 
\ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ Q\ (?x2\ x)\isasymrbrakk\ 
10295  1002 
\isasymLongrightarrow\ Q\ x 
1003 
\end{isabelle} 

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

11077  1005 
term built from~\isa{x}, and here 
1006 
it should simply be~\isa{x}. The assumption need not 

1007 
be identical to the conclusion, provided the two formulas are unifiable.% 

1008 
\index{quantifiers!universal)} 

10295  1009 

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

1010 

11234  1011 
\subsection{The Existential Quantifier} 
1012 

1013 
\index{quantifiers!existential(}% 

1014 
The concepts just presented also apply 

1015 
to the existential quantifier, whose introduction rule looks like this in 

1016 
Isabelle: 

1017 
\begin{isabelle} 

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

1019 
\end{isabelle} 

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

1021 
P(x)$ is also true. It is a dual of the universal elimination rule, and 

1022 
logic texts present it using the same notation for substitution. 

1023 

1024 
The existential 

1025 
elimination rule looks like this 

1026 
in a logic text: 

1027 
\[ \infer{Q}{\exists x.\,P & \infer*{Q}{[P]}} \] 

1028 
% 

1029 
It looks like this in Isabelle: 

1030 
\begin{isabelle} 

1031 
\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE} 

1032 
\end{isabelle} 

1033 
% 

1034 
Given an existentially quantified theorem and some 

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

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

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

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

1039 
quantifier to be built in as well. 

1040 

1041 

1042 
\begin{exercise} 

1043 
Prove the lemma 

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

1045 
\emph{Hint}: the proof is similar 

1046 
to the one just above for the universal quantifier. 

1047 
\end{exercise} 

1048 
\index{quantifiers)}\index{quantifiers!existential)} 

1049 

1050 

10967  1051 
\subsection{Renaming an Assumption: {\tt\slshape rename_tac}} 
1052 

11077  1053 
\index{assumptions!renaming(}\index{*rename_tac(}% 
1054 
When you apply a rule such as \isa{allI}, the quantified variable 

1055 
becomes a new bound variable of the new subgoal. Isabelle tries to avoid 

1056 
changing its name, but sometimes it has to choose a new name in order to 

11234  1057 
avoid a clash. The result may not be ideal: 
10967  1058 
\begin{isabelle} 
1059 
\isacommand{lemma}\ "x\ <\ y\ \isasymLongrightarrow \ \isasymforall x\ y.\ P\ x\ 

1060 
(f\ y)"\isanewline 

1061 
\isacommand{apply}\ intro\isanewline 

1062 
\ 1.\ \isasymAnd xa\ ya.\ x\ <\ y\ \isasymLongrightarrow \ P\ xa\ (f\ ya) 

1063 
\end{isabelle} 

1064 
% 

1065 
The names \isa{x} and \isa{y} were already in use, so the new bound variables are 

1066 
called \isa{xa} and~\isa{ya}. You can rename them by invoking \isa{rename_tac}: 

1067 

1068 
\begin{isabelle} 

1069 
\isacommand{apply}\ (rename_tac\ v\ w)\isanewline 

1070 
\ 1.\ \isasymAnd v\ w.\ x\ <\ y\ \isasymLongrightarrow \ P\ v\ (f\ w) 

1071 
\end{isabelle} 

10978  1072 
Recall that \isa{rule_tac}\index{*rule_tac!and renaming} instantiates a 
10967  1073 
theorem with specified terms. These terms may involve the goal's bound 
1074 
variables, but beware of referring to variables 

1075 
like~\isa{xa}. A future change to your theories could change the set of names 

1076 
produced at top level, so that \isa{xa} changes to~\isa{xb} or reverts to~\isa{x}. 

1077 
It is safer to rename automaticallygenerated variables before mentioning them. 

1078 

1079 
If the subgoal has more bound variables than there are names given to 

11077  1080 
\isa{rename_tac}, the rightmost ones are renamed.% 
1081 
\index{assumptions!renaming)}\index{*rename_tac)} 

10967  1082 

1083 

1084 
\subsection{Reusing an Assumption: {\tt\slshape frule}} 

11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

1085 
\label{sec:frule} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1086 

11077  1087 
\index{assumptions!reusing(}\index{*frule(}% 
10295  1088 
Note that \isa{drule spec} removes the universal quantifier and  as 
1089 
usual with elimination rules  discards the original formula. Sometimes, a 

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

1091 
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

1092 
the selected assumption. The \isa{f} is for \emph{forward}. 
10295  1093 

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

1094 
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

1095 
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

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

1098 
\isacommand{lemma}\ "\isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x); 
11077  1099 
\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P(h\ (h\ a))" 
10295  1100 
\end{isabelle} 
1101 
% 

11077  1102 
Examine the subgoal left by \isa{frule}: 
10295  1103 
\begin{isabelle} 
11077  1104 
\isacommand{apply}\ (frule\ spec)\isanewline 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1105 
\ 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  1106 
\end{isabelle} 
11077  1107 
It is what \isa{drule} would have left except that the quantified 
1108 
assumption is still present. Next we apply \isa{mp} to the 

1109 
implication and the assumption~\isa{P\ a}: 

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

1112 
\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);\ P\ a;\ P\ (h\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a)) 
10295  1113 
\end{isabelle} 
1114 
% 

11077  1115 
We have created the assumption \isa{P(h\ a)}, which is progress. To 
1116 
continue the proof, we apply \isa{spec} again. We shall not need it 

1117 
again, so we can use 

1118 
\isa{drule}. 

1119 
\begin{isabelle} 

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

1121 
\ 1.\ \isasymlbrakk P\ a;\ P\ (h\ a);\ P\ ?x2\ 

1122 
\isasymlongrightarrow \ P\ (h\ ?x2)\isasymrbrakk \ \isasymLongrightarrow \ 

1123 
P\ (h\ (h\ a)) 

1124 
\end{isabelle} 

1125 
% 

1126 
The new assumption bridges the gap between \isa{P(h\ a)} and \isa{P(h(h\ a))}. 

1127 
\begin{isabelle} 

1128 
\isacommand{by}\ (drule\ mp) 

1129 
\end{isabelle} 

10854  1130 

1131 
\medskip 

11077  1132 
\emph{A final remark}. Replacing this \isacommand{by} command with 
10295  1133 
\begin{isabelle} 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1134 
\isacommand{apply}\ (drule\ mp,\ assumption) 
10295  1135 
\end{isabelle} 
11077  1136 
would not work: it would add a second copy of \isa{P(h~a)} instead 
10854  1137 
of the desired assumption, \isa{P(h(h~a))}. The \isacommand{by} 
1138 
command forces Isabelle to backtrack until it finds the correct one. 

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

11234  1140 
\isa{drule mp} with \emph{two} calls of \isa{assumption}. Or, of course, 
1141 
we could have given the entire proof to \isa{auto}.% 

11077  1142 
\index{assumptions!reusing)}\index{*frule)} 
10295  1143 

1144 

11234  1145 

1146 
\subsection{Instantiating a Quantifier Explicitly} 

1147 
\index{quantifiers!instantiating} 

10295  1148 

11234  1149 
We can prove a theorem of the form $\exists x.\,P\, x$ by exhibiting a 
1150 
suitable term~$t$ such that $P\,t$ is true. Dually, we can use an 

1151 
assumption of the form $\forall x.\,P\, x$ by exhibiting a 

1152 
suitable term~$t$ such that $P\,t$ is false, or (more generally) 

1153 
that contributes in some way to the proof at hand. In many cases, 

1154 
Isabelle makes the correct choice automatically, constructing the term by 

1155 
unification. In other cases, the required term is not obvious and we must 

1156 
specify it ourselves. Suitable methods are \isa{rule_tac}, \isa{drule_tac} 

1157 
and \isa{erule_tac}. 

1158 

1159 
We have just seen a proof of this lemma: 

10295  1160 
\begin{isabelle} 
11234  1161 
\isacommand{lemma}\ "\isasymlbrakk \isasymforall x.\ P\ x\ 
1162 
\isasymlongrightarrow \ P\ (h\ x);\ P\ a\isasymrbrakk \ 

1163 
\isasymLongrightarrow \ P(h\ (h\ a))" 

10295  1164 
\end{isabelle} 
11234  1165 
We had reached this subgoal: 
10295  1166 
\begin{isabelle} 
11234  1167 
\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ 
1168 
x);\ P\ a;\ P\ (h\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a)) 

10295  1169 
\end{isabelle} 
1170 
% 

11234  1171 
The proof requires instantiating the quantified assumption with the 
1172 
term~\isa{h~a}. 

1173 
\begin{isabelle} 

1174 
\isacommand{apply}\ (drule_tac\ x\ =\ "h\ a"\ \isakeyword{in}\ 

1175 
spec)\isanewline 

1176 
\ 1.\ \isasymlbrakk P\ a;\ P\ (h\ a);\ P\ (h\ a)\ \isasymlongrightarrow \ 

1177 
P\ (h\ (h\ a))\isasymrbrakk \ \isasymLongrightarrow \ P\ (h\ (h\ a)) 

1178 
\end{isabelle} 

1179 
We have forced the desired instantiation. 

1180 

1181 
\medskip 

1182 
Existential formulas can be instantiated too. The next example uses the 

1183 
\emph{divides} relation of number theory: 

1184 
\begin{isabelle} 

1185 
?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k 

1186 
\rulename{dvd_def} 

1187 
\end{isabelle} 

10295  1188 

11234  1189 
Let us prove that multiplication of natural numbers is monotone with 
1190 
respect to the divides relation: 

1191 
\begin{isabelle} 

1192 
\isacommand{lemma}\ mult_dvd_mono:\ "{\isasymlbrakk}i\ dvd\ m;\ j\ dvd\ 

1193 
n\isasymrbrakk\ \isasymLongrightarrow\ i*j\ dvd\ (m*n\ ::\ nat)"\isanewline 

1194 
\isacommand{apply}\ (simp\ add:\ dvd_def) 

1195 
\end{isabelle} 

1196 
% 

1197 
Opening the definition of divides leaves this subgoal: 

1198 
\begin{isabelle} 

1199 
\ 1.\ \isasymlbrakk \isasymexists k.\ m\ =\ i\ *\ k;\ \isasymexists k.\ n\ 

1200 
=\ j\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ 

1201 
n\ =\ i\ *\ j\ *\ k% 

1202 
\isanewline 

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

1204 
\ 1.\ \isasymAnd k.\ \isasymlbrakk \isasymexists k.\ n\ =\ j\ *\ k;\ m\ =\ 

1205 
i\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\ 

1206 
=\ i\ *\ j\ *\ k% 

1207 
\isanewline 

1208 
\isacommand{apply}\ (erule\ exE) 

1209 
\end{isabelle} 

1210 
% 

1211 
Eliminating the two existential quantifiers in the assumptions leaves this 

1212 
subgoal: 

1213 
\begin{isabelle} 

1214 
\ 1.\ \isasymAnd k\ ka.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\ 

1215 
ka\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\ =\ i\ 

1216 
*\ j\ *\ k 

1217 
\end{isabelle} 

1218 
% 

1219 
The term needed to instantiate the remaining quantifier is~\isa{k*ka}: 

1220 
\begin{isabelle} 

1221 
\isacommand{apply}\ (rule_tac\ x="k*ka"\ \isakeyword{in}\ exI)\ \isanewline 

1222 
\ 1.\ \isasymAnd k\ ka.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\ 

1223 
ka\isasymrbrakk \ \isasymLongrightarrow \ m\ *\ n\ =\ i\ 

1224 
*\ j\ *\ (k\ *\ ka) 

1225 
\end{isabelle} 

1226 
% 

1227 
The rest is automatic, by arithmetic. 

1228 
\begin{isabelle} 

1229 
\isacommand{apply}\ simp\isanewline 

1230 
\isacommand{done}\isanewline 

1231 
\end{isabelle} 

1232 

1233 
\begin{warn} 

1234 
References to automaticallygenerated names like~\isa{ka} can make a proof 

1235 
brittle, especially if the proof is long. Small changes to your theory can 

1236 
cause these names to change. Robust proofs replace 

1237 
automaticallygenerated names by ones chosen using 

1238 
\isa{rename_tac} before giving them to \isa{rule_tac}. 

1239 
\end{warn} 

1240 

10295  1241 

1242 

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

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

1245 

11077  1246 
\index{Hilbert's epsilonoperator(}% 
1247 
HOL provides Hilbert's $\varepsilon$operator. The term $\varepsilon x. 

1248 
P(x)$ denotes some $x$ such that $P(x)$ is true, provided such a value 

1249 
exists. In \textsc{ascii}, we write \isa{SOME} for the Greek 

1250 
letter~$\varepsilon$. 

1251 

1252 
\begin{warn} 

1253 
Hilbert's $\varepsilon$operator can be hard to reason about. New users 

1254 
should try to avoid it. Fortunately, situations that require it are rare. 

1255 
\end{warn} 

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

1256 

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

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

1258 

11077  1259 
\index{descriptions!definite}% 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

1260 
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

1261 
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

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

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

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

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

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

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

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

1269 
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

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

1271 
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

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

1273 

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

1274 
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

1275 
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

1276 
\begin{isabelle} 
11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

1277 
(LEAST\ x.\ P\ x)\ = (SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

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

1279 
\end{isabelle} 
11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

1280 
% 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

1281 
Let us prove the counterpart of \isa{some_equality} for \isa{LEAST}\@. 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

1282 
The first step merely unfolds the definitions (\isa{LeastM} is a 
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

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

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

1285 
\isacommand{theorem}\ Least_equality:\isanewline 
11179
bee6673b020a
subst method and a new section on rule, rule_tac, etc
paulson
parents:
11159
diff
changeset

1286 
\ \ \ \ \ "\isasymlbrakk P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline 
11155  1287 
\isacommand{apply}\ (simp\ add:\ Least_def\ LeastM_def)\isanewline 
10848
7b3ee4695fe6
various changes including the SOME examples, rule_format and "by"
paulson
parents:
10792
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

1299 
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

1300 
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

1301 
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

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

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

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

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

1306 
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

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

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

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

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

1311 

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

1312 

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

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

1314 

11077  1315 
\index{descriptions!indefinite}% 
1316 
Occasionally, \hbox{\isa{SOME\ x.\ P\ x}} serves as an \emph{indefinite 

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

1317 
description}, when it makes an arbitrary selection from the values 
11077  1318 
satisfying~\isa{P}\@. Here is the definition 
1319 
of~\isa{inv},\index{*inv (constant)} which expresses inverses of functions: 

1320 
\begin{isabelle} 

1321 
inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y% 

1322 
\rulename{inv_def} 

