10295

1 
\chapter{The Rules of the Game}


2 
\label{chap:rules}


3 


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


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


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


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


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


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


10 
\isa{auto} and others.


11 


12 
\section{Natural deduction}


13 


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


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


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


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


18 
we may infer~$Q$.


19 


20 
%Early logical formalisms had this


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


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


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


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


25 
%these two axioms (amongst others):


26 
%\begin{gather*}


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


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


29 
%\end{gather*}


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


31 
%ponens}!


32 


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


34 
that mirrors human reasoning patterns.


35 
%


36 
%Instead of having a few


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


38 
%and few axioms.


39 
%


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


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


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


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


44 
consequences from this symbol. Ideally each rule should mention


45 
one symbol only. For predicate logic this can be


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


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


48 


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


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


51 
applying the corresponding rule. It creates new subgoals in


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


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


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


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


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


57 
Isabelle's


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


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


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


61 
elimination rules.


62 


63 


64 
\section{Introduction rules}


65 


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


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


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


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


70 
like this:


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


72 
The rule introduces the conjunction


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


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


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


76 
disappear.


77 


78 
In Isabelle notation, the rule looks like this:


79 
\begin{isabelle}


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


81 
\end{isabelle}


82 
Carefully examine the syntax. The premises appear to the


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


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


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


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


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


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


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


90 
it yields new subgoals given by the formulas assigned to


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


92 


93 
The following trivial proof illustrates this point.


94 
\begin{isabelle}


95 
\isacommand{lemma}\ conj_rule:\ "{\isasymlbrakk}P;\


96 
Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\

10301

97 
(Q\ \isasymand\ P)"\isanewline

10295

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


99 
\ \isacommand{apply}\ assumption\isanewline


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


101 
\ \isacommand{apply}\ assumption\isanewline


102 
\isacommand{apply}\ assumption


103 
\end{isabelle}


104 
At the start, Isabelle presents


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


106 
\isa{P\ \isasymand\


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


108 
apply conjunction introduction, the rule removes the outermost occurrence


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


110 
the proof method {\isa{rule}}  here with {\isa{conjI}}, the conjunction


111 
introduction rule.


112 
\begin{isabelle}


113 
%{\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\


114 
%\isasymand\ P\isanewline


115 
\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline


116 
\ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P


117 
\end{isabelle}


118 
Isabelle leaves two new subgoals: the two halves of the original conjunction.


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


120 
the assumptions. We can apply the {\isa{assumption}}


121 
method, which proves a subgoal by finding a matching assumption.


122 
\begin{isabelle}


123 
\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\


124 
Q\ \isasymand\ P


125 
\end{isabelle}


126 
We are left with the subgoal of proving


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


128 
\isa{rule conjI} again.


129 
\begin{isabelle}


130 
\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline


131 
\ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P


132 
\end{isabelle}


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


134 
using the {\isa{assumption}} method.


135 


136 


137 
\section{Elimination rules}


138 


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


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


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


142 
we infer $Q$:


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


144 


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


146 
conjunction elimination rules:


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


148 


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


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


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


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


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


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


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


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


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


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


159 
nowhere else.


160 


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


162 
like this:


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


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


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


166 
notation, the alreadyfamiliar \isa\isasymLongrightarrow syntax serves the


167 
same purpose:


168 
\begin{isabelle}


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


170 
\end{isabelle}


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


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


173 
illustrates the use of disjunction elimination.


174 
\begin{isabelle}

10301

175 
\isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\

10295

176 
\isasymLongrightarrow\ Q\ \isasymor\ P"\isanewline


177 
\isacommand{apply}\ (erule\ disjE)\isanewline


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


179 
\ \isacommand{apply}\ assumption\isanewline


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


181 
\isacommand{apply}\ assumption


182 
\end{isabelle}


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


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


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


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


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


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


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


190 
any point in keeping the assumption.


191 


192 
\begin{isabelle}


193 
%P\ \isasymor\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline


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


195 
\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P


196 
\end{isabelle}


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


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


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


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


201 
{\isa{rule}} method with \isa{disjI2} \ldots


202 
\begin{isabelle}


203 
\ 1.\ P\ \isasymLongrightarrow\ P\isanewline


204 
\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P


205 
\end{isabelle}


206 
\ldots and finish off with the {\isa{assumption}}


207 
method. We are left with the other subgoal, which


208 
assumes \isa{Q}.


209 
\begin{isabelle}


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


211 
\end{isabelle}


212 
Its proof is similar, using the introduction


213 
rule \isa{disjI1}.


214 


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


216 
an introduction nor an elimination rule, but which might


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


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


219 


220 


221 


222 
\section{Destruction rules: some examples}


223 


224 
Now let us examine the analogous proof for conjunction.


225 
\begin{isabelle}

10301

226 
\isacommand{lemma}\ conj_swap:\ "P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P"\isanewline

10295

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


228 
\ \isacommand{apply}\ (drule\ conjunct2)\isanewline


229 
\ \isacommand{apply}\ assumption\isanewline


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


231 
\isacommand{apply}\ assumption


232 
\end{isabelle}


233 
Recall that the conjunction elimination rules  whose Isabelle names are


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


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


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

10301

237 
functions of functional programming.%

10295

238 
\footnote{This Isabelle terminology has no counterpart in standard logic texts,


239 
although the distinction between the two forms of elimination rule is well known.


240 
Girard \cite[page 74]{girard89}, for example, writes ``The elimination rules are very


241 
bad. What is catastrophic about them is the parasitic presence of a formula [$R$]


242 
which has no structural link with the formula which is eliminated.''}


243 


244 
The first proof step applies conjunction introduction, leaving


245 
two subgoals:


246 
\begin{isabelle}


247 
%P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P\isanewline


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


249 
\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P


250 
\end{isabelle}


251 


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


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


254 
you prefer). Applying the


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


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


257 
\begin{isabelle}


258 
\ 1.\ Q\ \isasymLongrightarrow\ Q\isanewline


259 
\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P


260 
\end{isabelle}


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


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


263 
\isa{assumption} method.


264 


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


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


267 
is an introduction rule or an elimination rule. The


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


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


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


271 
assumption of the form


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


273 


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


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


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


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


278 
alternative conjunction elimination rule that resembles \isa{disjE}. It is seldom,


279 
if ever, seen in logic books. In Isabelle syntax it looks like this:


280 
\begin{isabelle}


281 
\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{conjE}


282 
\end{isabelle}


283 


284 
\begin{exercise}


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


286 
\end{exercise}


287 


288 


289 
\section{Implication}


290 


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


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


293 
in Isabelle:


294 
\begin{isabelle}


295 
(?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\


296 
\isasymlongrightarrow\ ?Q\rulename{impI}


297 
\end{isabelle}


298 
And this is \textit{modus ponens}:


299 
\begin{isabelle}


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


301 
\isasymLongrightarrow\ ?Q


302 
\rulename{mp}


303 
\end{isabelle}


304 


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


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


307 
of a nested implication by a conjunction.


308 
\begin{isabelle}


309 
\isacommand{lemma}\ imp_uncurry:\

10301

310 
"P\ \isasymlongrightarrow\ (Q\

10295

311 
\isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\


312 
\isasymand\ Q\ \isasymlongrightarrow\


313 
R"\isanewline


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


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


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


317 
\ \isacommand{apply}\ assumption\isanewline


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


319 
\ \ \isacommand{apply}\ assumption\isanewline


320 
\ \isacommand{apply}\ assumption


321 
\end{isabelle}


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


323 
which moves the conjunction to the assumptions.


324 
\begin{isabelle}


325 
%P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R\ \isasymLongrightarrow\ P\


326 
%\isasymand\ Q\ \isasymlongrightarrow\ R\isanewline


327 
\ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R


328 
\end{isabelle}


329 
Next, we apply conjunction elimination (\isa{erule conjE}), which splits this


330 
conjunction into two parts.


331 
\begin{isabelle}


332 
\ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\


333 
Q\isasymrbrakk\ \isasymLongrightarrow\ R


334 
\end{isabelle}


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


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


337 
clarity. The nested implication requires two applications of


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


339 
implication \isa{Q\


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


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


342 
\begin{isabelle}


343 
\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline


344 
\ 2.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R


345 
\end{isabelle}


346 
Repeating these steps for \isa{Q\


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


348 
\begin{isabelle}


349 
\ 1.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\


350 
\isasymLongrightarrow\ R


351 
\end{isabelle}


352 


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


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


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


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


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


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


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


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


361 
context that requires a formula of higherorder logic. Use


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


363 
conclusion.


364 


365 
When using induction, often the desired theorem results in an induction


366 
hypothesis that is too weak. In such cases you may have to invent a more


367 
complicated induction formula, typically involving


368 
\isa{\isasymlongrightarrow} and \isa{\isasymforall}. From this lemma you


369 
derive the desired theorem , typically involving


370 
\isa{\isasymLongrightarrow}. We shall see an example below,


371 
\S\ref{sec:provingeuclid}.


372 


373 


374 
\section{Unification and substitution}\label{sec:unification}


375 


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


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


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


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


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


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


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


383 
{\isa{rule}} method typically matches the rule's conclusion


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


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


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


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


388 


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


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


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


392 
They can be filled in later, often automatically.


393 


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


395 
unification, which is unification in the


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


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


398 
unification are straightforward. It handles bound variables


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


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


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


402 
bound. The two terms


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


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


405 


406 
Higherorder unification sometimes must invent


407 
$\lambda$terms to replace function variables,


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


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


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


411 
function variable is applied only to bound variables,


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


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


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


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


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


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


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


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


420 


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


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


423 
another if we know that two terms are equal.


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


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


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


427 
designated by~$x$, which gives it additional power. For example, it can


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


429 
replaces just the first $s$ in $s=s$ by~$t$.


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


431 


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


433 
\begin{isabelle}


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


435 
?t


436 
\rulename{ssubst}


437 
\end{isabelle}


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


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


440 
involving one bound variable whose occurrences identify the places


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


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


443 


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


445 
rule gives us more control. Consider this proof:


446 
\begin{isabelle}


447 
\isacommand{lemma}\


448 
"{\isasymlbrakk}\ x\


449 
=\ f\ x;\ odd(f\


450 
x)\ \isasymrbrakk\ \isasymLongrightarrow\ odd\


451 
x"\isanewline


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


453 
\isacommand{apply}\ assumption\isanewline


454 
\isacommand{done}\end{isabelle}


455 
%


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


457 
\isa{f(f x)} and so forth. (Actually, \isa{simp}


458 
sees the danger and reorients this equality, but in more complicated cases


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


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


461 
resulting subgoal is trivial by assumption.


462 


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


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


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


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


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


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


469 
assumption.


470 


471 


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


473 
\begin{isabelle}


474 
\isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\


475 
f\ x;\ triple\ (f\ x)\


476 
(f\ x)\ x\ \isasymrbrakk\


477 
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline


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


479 
\isacommand{back}\isanewline


480 
\isacommand{back}\isanewline


481 
\isacommand{back}\isanewline


482 
\isacommand{back}\isanewline


483 
\isacommand{apply}\ assumption\isanewline


484 
\isacommand{done}


485 
\end{isabelle}


486 
%


487 
By default, Isabelle tries to substitute for all the


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


489 
\begin{isabelle}


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


491 
\end{isabelle}


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


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


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


495 
\begin{isabelle}


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


497 
\end{isabelle}


498 
%


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


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


501 
again:


502 
\begin{isabelle}


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


504 
\end{isabelle}


505 
%


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


507 
\begin{isabelle}


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


509 
\end{isabelle}


510 
%


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


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


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


514 
\begin{isabelle}


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


516 
\end{isabelle}


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


518 


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


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


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


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


523 
fails then Isabelle automatically backtracks. This process continues until


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


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


526 
\begin{isabelle}


527 
\isacommand{lemma}\


528 
"{\isasymlbrakk}\ x\


529 
=\ f\ x;\ triple\ (f\


530 
x)\ (f\ x)\ x\


531 
\isasymrbrakk\


532 
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline


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


534 
\isacommand{done}


535 
\end{isabelle}


536 


537 
The most general way to get rid of the {\isa{back}} command is


538 
to instantiate variables in the rule. The method {\isa{rule\_tac}} is


539 
similar to \isa{rule}, but it


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


541 
Also available are {\isa{drule\_tac}} and \isa{erule\_tac}. Here we need


542 
\isa{erule\_tac} since above we used


543 
\isa{erule}.


544 
\begin{isabelle}


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


546 
\isacommand{apply}\ (erule_tac\

10301

547 
P="{\isasymlambda}u.\ triple\ u\

10295

548 
u\ x"\ \isakeyword{in}\


549 
ssubst)\isanewline


550 
\isacommand{apply}\ assumption\isanewline


551 
\isacommand{done}


552 
\end{isabelle}


553 
%


554 
To specify a desired substitution


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


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


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


558 
the third unchanged.


559 


560 
An alternative to {\isa{rule\_tac}} is to use \isa{rule} with the


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


562 
advantage of {\isa{rule\_tac}} is that the instantiations may refer to


563 
variables bound in the current subgoal.


564 


565 


566 
\section{Negation}


567 


568 
Negation causes surprising complexity in proofs. Its natural


569 
deduction rules are straightforward, but additional rules seem


570 
necessary in order to handle negated assumptions gracefully.


571 


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


573 
contradiction. Negation elimination deduces any formula in the


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


575 
\begin{isabelle}


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


577 
\rulename{notI}\isanewline


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


579 
\rulename{notE}


580 
\end{isabelle}


581 
%


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


583 
when attempting to prove~$P$:


584 
\begin{isabelle}


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


586 
\rulename{classical}


587 
\end{isabelle}


588 
%


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


590 
They differ in the placement of the negation symbols:


591 
\begin{isabelle}


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


593 
\rulename{contrapos_pp}\isanewline


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


595 
\rulename{contrapos_np}\isanewline


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


597 
\rulename{contrapos_nn}


598 
\end{isabelle}


599 
%


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


601 
their effect is to form a contrapositive from an


602 
assumption and the goal's conclusion.


603 


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


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


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


607 
might want to use conjunction introduction on it.


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


609 
becomes the conclusion. The following proof demonstrates this


610 
technique:


611 
\begin{isabelle}


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


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


614 
R"\isanewline


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


616 
contrapos_np)\isanewline


617 
\isacommand{apply}\ intro\isanewline


618 
\isacommand{apply}\ (erule\ notE,\ assumption)\isanewline


619 
\isacommand{done}


620 
\end{isabelle}


621 
%


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


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


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


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


626 
\begin{isabelle}


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


628 
R\isasymrbrakk\ \isasymLongrightarrow\ R\ \isasymlongrightarrow\ Q%


629 
\end{isabelle}


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


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


632 
conclusion.


633 


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


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


636 
to \isa{rule impI}.\begin{isabelle}


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


638 
R\isasymrbrakk\ \isasymLongrightarrow\ Q%


639 
\end{isabelle}


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


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


642 
however, it will select the first negated assumption, which is useless. Instead,


643 
we combine the rule with the


644 
\isa{assumption} method:


645 
\begin{isabelle}


646 
\ \ \ \ \ (erule\ notE,\ assumption)


647 
\end{isabelle}


648 
Now when Isabelle selects the first assumption, it tries to prove \isa{P\


649 
\isasymlongrightarrow\ Q} and fails; it then backtracks, finds the


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


651 
concludes the proof.


652 


653 
\medskip


654 


655 
Here is another example.


656 
\begin{isabelle}


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


658 
\isasymLongrightarrow\ P\ \isasymor\ Q\ \isasymand\ R"\isanewline


659 
\isacommand{apply}\ intro%


660 


661 


662 
\isacommand{apply}\ (elim\ conjE\ disjE)\isanewline


663 
\ \isacommand{apply}\ assumption


664 
\isanewline


665 
\isacommand{apply}\ (erule\ contrapos_np,\ rule\ conjI)\isanewline


666 
\ \ \isacommand{apply}\ assumption\isanewline


667 
\ \isacommand{apply}\ assumption\isanewline


668 
\isacommand{done}


669 
\end{isabelle}


670 
%


671 
The first proof step applies the {\isa{intro}} method, which repeatedly


672 
uses builtin introduction rules. Here it creates the negative assumption \isa{\isasymnot\ (Q\ \isasymand\


673 
R)}.


674 
\begin{isabelle}


675 
\ 1.\ \isasymlbrakk(P\ \isasymor\ Q)\ \isasymand\ R;\ \isasymnot\ (Q\ \isasymand\


676 
R)\isasymrbrakk\ \isasymLongrightarrow\ P%


677 
\end{isabelle}


678 
It comes from \isa{disjCI}, a disjunction introduction rule that is more


679 
powerful than the separate rules \isa{disjI1} and \isa{disjI2}.


680 


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


682 
elimination rules; here, the elimination rules given


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


684 
\begin{isabelle}


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


686 
\end{isabelle}


687 
%


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


689 
combination


690 
\begin{isabelle}


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


692 
\end{isabelle}


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

10301

694 
conjunction. The two subgoals are the ones we would expect from applying

10295

695 
conjunction introduction to


696 
\isa{Q\


697 
\isasymand\ R}:


698 
\begin{isabelle}


699 
\ 1.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\


700 
Q\isanewline


701 
\ 2.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R%


702 
\end{isabelle}


703 
The rest of the proof is trivial.


704 


705 


706 
\section{The universal quantifier}


707 


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


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


710 
introduction rule looks like this:


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


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


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


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


715 
Isabelle's underlying formalism, called the


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


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


718 
already seen another symbol of the metalogic, namely


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


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


721 
can be used to define constants.


722 


723 
Returning to the universal quantifier, we find that having a similar quantifier


724 
as part of the metalogic makes the introduction rule trivial to express:


725 
\begin{isabelle}


726 
({\isasymAnd}x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI}


727 
\end{isabelle}


728 


729 


730 
The following trivial proof demonstrates how the universal introduction


731 
rule works.


732 
\begin{isabelle}


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


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


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


736 
\isacommand{apply}\ assumption


737 
\end{isabelle}


738 
The first step invokes the rule by applying the method \isa{rule allI}.


739 
\begin{isabelle}


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


741 
\ 1.\ {\isasymAnd}x.\ P\ x\ \isasymlongrightarrow\ P\ x


742 
\end{isabelle}


743 
Note that the resulting proof state has a bound variable,


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


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


746 
prove


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


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


749 
\begin{isabelle}


750 
\ 1.\ {\isasymAnd}x.\ P\ x\ \isasymLongrightarrow\ P\ x


751 
\end{isabelle}


752 
The {\isa{assumption}} method proves this last subgoal.


753 


754 
\medskip


755 
Now consider universal elimination. In a logic text,


756 
the rule looks like this:


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


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


759 
Isabelle expresses substitution using a function variable:


760 
\begin{isabelle}


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


762 
\end{isabelle}


763 
This destruction rule takes a


764 
universally quantified formula and removes the quantifier, replacing


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


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


767 
placeholder: it can be replaced by any term.


768 


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


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


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


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


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


774 
\isa{P\


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


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


777 
bound variable capture. Here is the isabelle proof in full:


778 
\begin{isabelle}


779 
\isacommand{lemma}\ "({\isasymforall}x.\ P\


780 
\isasymlongrightarrow\ Q\ x)\ \isasymLongrightarrow\ P\

10301

781 
\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)"\isanewline

10295

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


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


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


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


786 
\ \ \isacommand{apply}\ assumption\isanewline


787 
\ \isacommand{apply}\ assumption


788 
\end{isabelle}


789 
First we apply implies introduction (\isa{rule impI}),


790 
which moves the \isa{P} from the conclusion to the assumptions. Then


791 
we apply universal introduction (\isa{rule allI}).


792 
\begin{isabelle}


793 
%{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x\ \isasymLongrightarrow\ P\


794 
%\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)\isanewline


795 
\ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x


796 
\end{isabelle}


797 
As before, it replaces the HOL


798 
quantifier by a metalevel quantifier, producing a subgoal that


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


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


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


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


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


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


805 
rules add bound variables or assumptions.


806 


807 
Now, to reason from the universally quantified


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


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


810 
to a particular term.


811 
\begin{isabelle}


812 
\ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ P\ \isasymlongrightarrow\ Q\ (?x2\


813 
x){\isasymrbrakk}\ \isasymLongrightarrow\ Q\ x


814 
\end{isabelle}


815 
Observe how the context has changed. The quantified formula is gone,


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


817 
removed the quantifier. The quantified variable


818 
has been replaced by the curious term


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


820 
by any term that can be built up from~\bigisa{x}. (Formally, \bigisa{?x2} is an


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


822 
an implication, so we can use \emph{modus ponens} on it. As before, it requires


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


824 
\begin{isabelle}


825 
\ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ Q\ (?x2\ x){\isasymrbrakk}\


826 
\isasymLongrightarrow\ Q\ x


827 
\end{isabelle}


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


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


830 
it should simply be~\bigisa{x}. The \isa{assumption} method will do this.


831 
The assumption need not be identical to the conclusion, provided the two formulas are


832 
unifiable.


833 


834 
\medskip


835 
Note that \isa{drule spec} removes the universal quantifier and  as


836 
usual with elimination rules  discards the original formula. Sometimes, a


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


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


839 
the selected assumption. The \isa{f} is for `forward.'


840 


841 
In this example, we intuitively see that to go from \isa{P\ a} to \isa{P(f\ (f\


842 
a))} requires two uses of the quantified assumption, one for each


843 
additional~\isa{f}.


844 
\begin{isabelle}


845 
\isacommand{lemma}\ "\isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x);


846 
\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P(f\ (f\ a))"\isanewline


847 
\isacommand{apply}\ (frule\ spec)\isanewline


848 
\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline


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


850 
\isacommand{apply}\ (drule\ mp,\ assumption,\ assumption)\isanewline


851 
\isacommand{done}


852 
\end{isabelle}


853 
%


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


855 
\begin{isabelle}


856 
\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x);\ P\ a;\ P\ ?x\ \isasymlongrightarrow\ P\ (f\ ?x)\isasymrbrakk\ \isasymLongrightarrow\ P\ (f\ (f\ a))


857 
\end{isabelle}


858 
It is just what \isa{drule} would have left except that the quantified


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


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


861 
\begin{isabelle}


862 
\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x);\ P\ a;\ P\ (f\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (f\ (f\ a))


863 
\end{isabelle}


864 
%


865 
We have created the assumption \isa{P(f\ a)}, which is progress. To finish the


866 
proof, we apply \isa{spec} one last time, using \isa{drule}. One final trick: if


867 
we then apply


868 
\begin{isabelle}


869 
\ \ \ \ \ (drule\ mp,\ assumption)


870 
\end{isabelle}


871 
it will add a second copy of \isa{P(f\ a)} instead of the desired \isa{P(f\


872 
(f\ a))}. Bundling both \isa{assumption} calls with \isa{drule mp} causes


873 
Isabelle to backtrack and find the correct one.


874 


875 


876 
\section{The existential quantifier}


877 


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


879 
whose introduction rule looks like this in Isabelle:


880 
\begin{isabelle}


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


882 
\end{isabelle}


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


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


885 
logic texts present it using the same notation for substitution. The existential


886 
elimination rule looks like this


887 
in a logic text:


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


889 
%


890 
It looks like this in Isabelle:


891 
\begin{isabelle}


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


893 
\end{isabelle}


894 
%


895 
Given an existentially quantified theorem and some


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


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


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


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

10399

900 
quantifier to be built in as well.\REMARK{EX example needed?}

10295

901 


902 
Isabelle/HOL also provides Hilbert's


903 
$\epsilon$operator. The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is


904 
true, provided such a value exists. Using this operator, we can express an


905 
existential destruction rule:


906 
\[ \infer{P[(\epsilon x. P) / \, x]}{\exists x.\,P} \]


907 
This rule is seldom used, for it can cause exponential blowup. The


908 
main use of $\epsilon x. P(x)$ is in definitions when $P(x)$ characterizes $x$


909 
uniquely. For instance, we can define the cardinality of a finite set~$A$ to be that

10301

910 
$n$ such that $A$ is in onetoone correspondence with $\{1,\ldots,n\}$. We can then

10295

911 
prove that the cardinality of the empty set is zero (since $n=0$ satisfies the

10399

912 
description) and proceed to prove other facts.\REMARK{SOME theorems

10295

913 
and example}


914 


915 
\begin{exercise}


916 
Prove the lemma


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


918 
\emph{Hint}: the proof is similar


919 
to the one just above for the universal quantifier.


920 
\end{exercise}


921 


922 


923 
\section{Some proofs that fail}


924 


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


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


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


928 
the existential quantifier and conjunction.


929 
\begin{isabelle}


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


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


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


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


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


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


936 
\ \isacommand{apply}\ assumption\isanewline


937 
\isacommand{oops}


938 
\end{isabelle}


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


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


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


942 
the quantifiers.


943 
\begin{isabelle}


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


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


946 
\ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x


947 
\end{isabelle}


948 
%


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


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


951 
\begin{isabelle}


952 
\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\


953 
\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x


954 
\end{isabelle}


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


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


957 
no way to prove this subgoal. Removing the


958 
conclusion's existential quantifier yields two


959 
identical placeholders, which can become any term involving the variables \bigisa{x}


960 
and~\bigisa{xa}. We need one to become \bigisa{x}


961 
and the other to become~\bigisa{xa}, but Isabelle requires all instances of a


962 
placeholder to be identical.


963 
\begin{isabelle}


964 
\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\


965 
\isasymLongrightarrow\ P\ (?x3\ x\ xa)\isanewline


966 
\ 2.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa)


967 
\end{isabelle}


968 
We can prove either subgoal


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


970 
changes into~\bigisa{x}.


971 
\begin{isabelle}


972 
\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\


973 
\isasymLongrightarrow\ Q\ x


974 
\end{isabelle}


975 
We are left with a subgoal that cannot be proved,


976 
because there is no way to prove that \bigisa{x}


977 
equals~\bigisa{xa}. Applying the \isa{assumption} method results in an


978 
error message:


979 
\begin{isabelle}


980 
*** empty result sequence  proof command failed


981 
\end{isabelle}


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


983 


984 
\medskip


985 


986 
Here is another abortive proof, illustrating the interaction between


987 
bound variables and unknowns.


988 
If $R$ is a reflexive relation,


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


990 
we attempt to prove it.


991 
\begin{isabelle}


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


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


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


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


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


997 
\isacommand{oops}


998 
\end{isabelle}


999 
First,


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


1001 
an unknown, namely~\bigisa{?x}.


1002 
\begin{isabelle}


1003 
%{\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymexists}x.\


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


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


1006 
\end{isabelle}


1007 
Next, we remove the universal quantifier


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


1009 
\begin{isabelle}


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


1011 
\end{isabelle}


1012 
Finally, we try to apply our reflexivity assumption. We obtain a


1013 
new assumption whose identical placeholders may be replaced by


1014 
any term involving~\bigisa{y}.


1015 
\begin{isabelle}


1016 
\ 1.\ {\isasymAnd}y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y


1017 
\end{isabelle}


1018 
This subgoal can only be proved by putting \bigisa{y} for all the placeholders,


1019 
making the assumption and conclusion become \isa{R\ y\ y}.


1020 
But Isabelle refuses to substitute \bigisa{y}, a bound variable, for


1021 
\bigisa{?x}; that would be a bound variable capture. The proof fails.


1022 
Note that Isabelle can replace \bigisa{?z2~y} by \bigisa{y}; this involves


1023 
instantiating


1024 
\bigisa{?z2} to the identity function.


1025 


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


1027 


1028 

10578

1029 
\section{Proving theorems using the {\tt\slshape blast} method}

10295

1030 


1031 
It is hard to prove substantial theorems using the methods


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


1033 
may need to search among different ways of proving certain


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


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


1036 
discussed, concerning negation and disjunction. Isabelle's


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


1038 
proofs automatically. The most important of these is the


1039 
{\isa{blast}} method.


1040 


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


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


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


1044 


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


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


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


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


1049 
problems for automatic theorem provers.}


1050 
The nested biconditionals cause an exponential explosion: the formal


1051 
proof is enormous. However, the {\isa{blast}} method proves it in


1052 
a fraction of a second.


1053 
\begin{isabelle}


1054 
\isacommand{lemma}\


1055 
"(({\isasymexists}x.\


1056 
{\isasymforall}y.\

10301

1057 
p(x){=}p(y))\

10295

1058 
=\


1059 
(({\isasymexists}x.\

10301

1060 
q(x))=({\isasymforall}y.\


1061 
p(y))))\

10295

1062 
\ \ =\ \ \ \ \isanewline


1063 
\ \ \ \ \ \ \ \


1064 
(({\isasymexists}x.\


1065 
{\isasymforall}y.\

10301

1066 
q(x){=}q(y))\

10295

1067 
=\


1068 
(({\isasymexists}x.\

10301

1069 
p(x))=({\isasymforall}y.\


1070 
q(y))))"\isanewline

10295

1071 
\isacommand{apply}\ blast\isanewline


1072 
\isacommand{done}


1073 
\end{isabelle}


1074 
The next example is a logic problem composed by Lewis Carroll.


1075 
The {\isa{blast}} method finds it trivial. Moreover, it turns out


1076 
that not all of the assumptions are necessary. We can easily


1077 
experiment with variations of this formula and see which ones


1078 
can be proved.


1079 
\begin{isabelle}


1080 
\isacommand{lemma}\


1081 
"({\isasymforall}x.\


1082 
honest(x)\ \isasymand\


1083 
industrious(x)\ \isasymlongrightarrow\

10301

1084 
healthy(x))\

10295

1085 
\isasymand\ \ \isanewline


1086 
\ \ \ \ \ \ \ \ \isasymnot\ ({\isasymexists}x.\


1087 
grocer(x)\ \isasymand\

10301

1088 
healthy(x))\

10295

1089 
\isasymand\ \isanewline


1090 
\ \ \ \ \ \ \ \ ({\isasymforall}x.\


1091 
industrious(x)\ \isasymand\


1092 
grocer(x)\ \isasymlongrightarrow\

10301

1093 
honest(x))\

10295

1094 
\isasymand\ \isanewline


1095 
\ \ \ \ \ \ \ \ ({\isasymforall}x.\


1096 
cyclist(x)\ \isasymlongrightarrow\

10301

1097 
industrious(x))\

10295

1098 
\isasymand\ \isanewline


1099 
\ \ \ \ \ \ \ \ ({\isasymforall}x.\


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


1101 
cyclist(x)\ \isasymlongrightarrow\

10301

1102 
{\isasymnot}honest(x))\

10295

1103 
\ \isanewline


1104 
\ \ \ \ \ \ \ \ \isasymlongrightarrow\


1105 
({\isasymforall}x.\


1106 
grocer(x)\ \isasymlongrightarrow\

10301

1107 
{\isasymnot}cyclist(x))"\isanewline

10295

1108 
\isacommand{apply}\ blast\isanewline


1109 
\isacommand{done}


1110 
\end{isabelle}


1111 
The {\isa{blast}} method is also effective for set theory, which is


1112 
described in the next chapter. This formula below may look horrible, but


1113 
the \isa{blast} method proves it easily.


1114 
\begin{isabelle}

10301

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


1116 
\ \ \ \ \ \ \ \ ({\isasymUnion}i{\isasymin}I.\ {\isasymUnion}j{\isasymin}J.\ A(i)\ \isasyminter\ B(j))"\isanewline

10295

1117 
\isacommand{apply}\ blast\isanewline


1118 
\isacommand{done}


1119 
\end{isabelle}


1120 


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


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


1123 
Extending it effectively requires understanding the notions of


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


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


1126 
that can be applied backwards without losing information; an


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


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


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


1130 
classical reasoner backtracks to the most recent unsafe rule application


1131 
and makes another choice.


1132 


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


1134 
equivalence, which in higherorder logic is an equality between


1135 
formulas, can be given to the classical


1136 
reasoner and simplifier by using the attribute {\isa{iff}}. You


1137 
should do so if the right hand side of the equivalence is


1138 
simpler than the lefthand side.


1139 


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


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


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


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


1144 
the {\isa{iff}} attribute. Once we have proved the lemma, Isabelle


1145 
will make it known to the classical reasoner (and to the simplifier).


1146 
\begin{isabelle}


1147 
\isacommand{lemma}\

10301

1148 
[iff]:\

10295

1149 
"(xs{\isacharat}ys\ =\


1150 
\isacharbrackleft{]})\ =\


1151 
(xs=[]\


1152 
\isacharampersand\

10301

1153 
ys=[])"\isanewline

10295

1154 
\isacommand{apply}\ (induct_tac\


1155 
xs)\isanewline


1156 
\isacommand{apply}\ (simp_all)


1157 
\isanewline


1158 
\isacommand{done}


1159 
\end{isabelle}


1160 
%


1161 
This fact about multiplication is also appropriate for

10399

1162 
the {\isa{iff}} attribute:\REMARK{the ?s are ugly here but we need

10295

1163 
them again when talking about \isa{of}; we need a consistent style}


1164 
\begin{isabelle}


1165 
(\mbox{?m}\ \isacharasterisk\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)


1166 
\end{isabelle}


1167 
A product is zero if and only if one of the factors is zero. The


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


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


1170 
works: the classical reasoner handles disjunction properly.


1171 


1172 
In more detail, this is how the {\isa{iff}} attribute works. It converts


1173 
the equivalence $P=Q$ to a pair of rules: the introduction


1174 
rule $Q\Imp P$ and the destruction rule $P\Imp Q$. It gives both to the


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


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


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


1178 
simplifier. But classical reasoning is different from


1179 
simplification. Simplification is deterministic: it applies rewrite rules


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


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


1182 


1183 


1184 
\section{Proving the correctness of Euclid's algorithm}


1185 
\label{sec:provingeuclid}


1186 


1187 
A brief development will illustrate advanced use of


1188 
\isa{blast}. In \S\ref{sec:recdefsimplification}, we declared the


1189 
recursive function {\isa{gcd}}:


1190 
\begin{isabelle}

10301

1191 
\isacommand{consts}\ gcd\ ::\ "nat{\isacharasterisk}nat\ \isasymRightarrow\ nat"\


1192 
\


1193 
\


1194 
\ \ \ \ \ \ \ \ \ \ \ \ \isanewline


1195 
\isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n)\


1196 
::nat{\isacharasterisk}nat\ \isasymRightarrow\ nat)"\isanewline


1197 
\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))"

10295

1198 
\end{isabelle}


1199 
Let us prove that it computes the greatest common


1200 
divisor of its two arguments.


1201 
%


1202 
%The declaration yields a recursion


1203 
%equation for {\isa{gcd}}. Simplifying with this equation can


1204 
%cause looping, expanding to everlarger expressions of ifthenelse


1205 
%and {\isa{gcd}} calls. To prevent this, we prove separate simplification rules


1206 
%for $n=0$\ldots


1207 
%\begin{isabelle}

10301

1208 
%\isacommand{lemma}\ gcd_0\ [simp]:\ "gcd(m,0)\ =\ m"\isanewline

10295

1209 
%\isacommand{apply}\ (simp)\isanewline


1210 
%\isacommand{done}


1211 
%\end{isabelle}


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


1213 
%\begin{isabelle}

10301

1214 
%\isacommand{lemma}\ gcd_non_0:\ "0{\isacharless}n\ \isasymLongrightarrow\ gcd(m,n)\ =\ gcd\ (n,\ m\ mod\ n)"\isanewline

10295

1215 
%\isacommand{apply}\ (simp)\isanewline


1216 
%\isacommand{done}


1217 
%\end{isabelle}


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


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


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


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


1222 
%original {\isa{gcd}} recursion equation.


1223 
%\begin{isabelle}

10301

1224 
%\isacommand{declare}\ gcd.simps\ [simp\ del]

10295

1225 
%\end{isabelle}


1226 
%


1227 
%Now we can prove some interesting facts about the {\isa{gcd}} function,


1228 
%for exampe, that it computes a common divisor of its arguments.


1229 
%


1230 
The theorem is expressed in terms of the familiar


1231 
\textbf{divides} relation from number theory:


1232 
\begin{isabelle}


1233 
?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ \isacharasterisk\ k


1234 
\rulename{dvd_def}


1235 
\end{isabelle}


1236 
%


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


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


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


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


1241 
\begin{isabelle}

10301

1242 
\isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\ n)"\isanewline


1243 
\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline


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

10295

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


1246 
\isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline


1247 
\isacommand{done}%


1248 
\end{isabelle}


1249 
Notice that the induction formula


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


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


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


1253 
and simplifying. Let us pass over these quickly and consider


1254 
the use of {\isa{blast}}. We have reached the following


1255 
subgoal:


1256 
\begin{isabelle}


1257 
%gcd\ (m,\ n)\ dvd\ m\ \isasymand\ gcd\ (m,\ n)\ dvd\ n\isanewline


1258 
\ 1.\ {\isasymAnd}m\ n.\ \isasymlbrakk0\ \isacharless\ n;\isanewline


1259 
\ \ \ \ \ \ \ \ \ \ \ \ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand\ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n){\isasymrbrakk}\isanewline

10546

1260 
\ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ gcd\ (n,\ m\ mod\ n)\ dvd\ m

10295

1261 
\end{isabelle}


1262 
%


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


1264 
The two divides relationships it asserts are enough to prove


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


1266 
\begin{isabelle}


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


1268 
\rulename{dvd_mod_imp_dvd}


1269 
\end{isabelle}


1270 
%


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


1272 
would cause backward chaining from the conclusion (namely


1273 
\isa{?k\ dvd\ ?m}) to the two premises, which


1274 
also involve the divides relation. This process does not look promising


1275 
and could easily loop. More sensible is to apply the rule in the forward

10301

1276 
direction; each step would eliminate the \isa{mod} symbol from an

10295

1277 
assumption, so the process must terminate.


1278 


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


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


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


1282 


1283 
\medskip


1284 
We have proved a conjunction. Now, let us give names to each of the


1285 
two halves:


1286 
\begin{isabelle}


1287 
\isacommand{lemmas}\ gcd_dvd1\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct1]\isanewline


1288 
\isacommand{lemmas}\ gcd_dvd2\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct2]%


1289 
\end{isabelle}


1290 


1291 
Several things are happening here. The keyword \isacommand{lemmas}


1292 
tells Isabelle to transform a theorem in some way and to


1293 
give a name to the resulting theorem. Attributes can be given,


1294 
here \isa{iff}, which supplies the new theorems to the classical reasoner


1295 
and the simplifier. The directive {\isa{THEN}}, which will be explained


1296 
below, supplies the lemma


1297 
\isa{gcd_dvd_both} to the


1298 
destruction rule \isa{conjunct1} in order to extract the first part.


1299 
\begin{isabelle}


1300 
\ \ \ \ \ gcd\


1301 
(?m1,\


1302 
?n1)\ dvd\


1303 
?m1%


1304 
\end{isabelle}


1305 
The variable names \isa{?m1} and \isa{?n1} arise because


1306 
Isabelle renames schematic variables to prevent


1307 
clashes. The second \isacommand{lemmas} declaration yields


1308 
\begin{isabelle}


1309 
\ \ \ \ \ gcd\


1310 
(?m1,\


1311 
?n1)\ dvd\


1312 
?n1%


1313 
\end{isabelle}


1314 
Later, we shall explore this type of forward reasoning in detail.


1315 


1316 
To complete the verification of the {\isa{gcd}} function, we must


1317 
prove that it returns the greatest of all the common divisors


1318 
of its arguments. The proof is by induction and simplification.


1319 
\begin{isabelle}


1320 
\isacommand{lemma}\ gcd_greatest\

10301

1321 
[rule_format]:\isanewline

10295

1322 
\ \ \ \ \ \ \ "(k\ dvd\


1323 
m)\ \isasymlongrightarrow\ (k\ dvd\


1324 
n)\ \isasymlongrightarrow\ k\ dvd\

10301

1325 
gcd(m,n)"\isanewline

10295

1326 
\isacommand{apply}\ (induct_tac\ m\ n\

10301

1327 
rule:\ gcd.induct)\isanewline


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

10295

1329 
\isacommand{apply}\ (simp_all\ add:\ gcd_non_0\ dvd_mod)\isanewline


1330 
\isacommand{done}


1331 
\end{isabelle}


1332 
%


1333 
Note that the theorem has been expressed using HOL implication,


1334 
\isa{\isasymlongrightarrow}, because the induction affects the two


1335 
preconditions. The directive \isa{rule_format} tells Isabelle to replace


1336 
each \isa{\isasymlongrightarrow} by \isa{\isasymLongrightarrow} before


1337 
storing the theorem we have proved. This directive also removes outer


1338 
universal quantifiers, converting a theorem into the usual format for


1339 
inference rules.


1340 


1341 
The facts proved above can be summarized as a single logical


1342 
equivalence. This step gives us a chance to see another application


1343 
of \isa{blast}, and it is worth doing for sound logical reasons.


1344 
\begin{isabelle}

10301

1345 
\isacommand{theorem}\ gcd_greatest_iff\ [iff]:\isanewline


1346 
\ \ \ \ \ \ \ \ \ "k\ dvd\ gcd(m,n)\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\ n)"\isanewline


1347 
\isacommand{apply}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans)\isanewline

10295

1348 
\isacommand{done}


1349 
\end{isabelle}


1350 
This theorem concisely expresses the correctness of the {\isa{gcd}}


1351 
function.


1352 
We state it with the {\isa{iff}} attribute so that


1353 
Isabelle can use it to remove some occurrences of {\isa{gcd}}.


1354 
The theorem has a oneline


1355 
proof using {\isa{blast}} supplied with four introduction


1356 
rules: note the {\isa{intro}} attribute. The exclamation mark


1357 
({\isa{intro}}{\isa{!}})\ signifies safe rules, which are


1358 
applied aggressively. Rules given without the exclamation mark


1359 
are applied reluctantly and their uses can be undone if


1360 
the search backtracks. Here the unsafe rule expresses transitivity


1361 
of the divides relation:


1362 
\begin{isabelle}


1363 
\isasymlbrakk?m\ dvd\ ?n;\ ?n\ dvd\ ?p\isasymrbrakk\ \isasymLongrightarrow\ ?m\ dvd\ ?p%


1364 
\rulename{dvd_trans}


1365 
\end{isabelle}


1366 
Applying \isa{dvd_trans} as


1367 
an introduction rule entails a risk of looping, for it multiplies


1368 
occurrences of the divides symbol. However, this proof relies


1369 
on transitivity reasoning. The rule {\isa{gcd\_greatest}} is safe to apply


1370 
aggressively because it yields simpler subgoals. The proof implicitly


1371 
uses \isa{gcd_dvd1} and \isa{gcd_dvd2} as safe rules, because they were


1372 
declared using \isa{iff}.


1373 


1374 


1375 
\section{Other classical reasoning methods}


1376 


1377 
The {\isa{blast}} method is our main workhorse for proving theorems


1378 
automatically. Other components of the classical reasoner interact


1379 
with the simplifier. Still others perform classical reasoning


1380 
to a limited extent, giving the user fine control over the proof.


1381 


1382 
Of the latter methods, the most useful is {\isa{clarify}}. It performs


1383 
all obvious reasoning steps without splitting the goal into multiple


1384 
parts. It does not apply rules that could render the


1385 
goal unprovable (socalled unsafe rules). By performing the obvious


1386 
steps, {\isa{clarify}} lays bare the difficult parts of the problem,


1387 
where human intervention is necessary.


1388 


1389 
For example, the following conjecture is false:


1390 
\begin{isabelle}


1391 
\isacommand{lemma}\ "({\isasymforall}x.\ P\ x)\ \isasymand\


1392 
({\isasymexists}x.\ Q\ x)\ \isasymlongrightarrow\ ({\isasymforall}x.\ P\ x\


1393 
\isasymand\ Q\ x)"\isanewline


1394 
\isacommand{apply}\ clarify


1395 
\end{isabelle}


1396 
The {\isa{blast}} method would simply fail, but {\isa{clarify}} presents


1397 
a subgoal that helps us see why we cannot continue the proof.


1398 
\begin{isabelle}


1399 
\ 1.\ {\isasymAnd}x\ xa.\ \isasymlbrakk{\isasymforall}x.\ P\ x;\ Q\


1400 
xa\isasymrbrakk\ \isasymLongrightarrow\ P\ x\ \isasymand\ Q\ x


1401 
\end{isabelle}


1402 
The proof must fail because the assumption \isa{Q\ xa} and conclusion \isa{Q\ x}


1403 
refer to distinct bound variables. To reach this state, \isa{clarify} applied


1404 
the introduction rules for \isa{\isasymlongrightarrow} and \isa{\isasymforall}


1405 
and the elimination rule for ~\isa{\isasymand}. It did not apply the introduction


1406 
rule for \isa{\isasymand} because of its policy never to split goals.


1407 


1408 
Also available is {\isa{clarsimp}}, a method that interleaves {\isa{clarify}}


1409 
and {\isa{simp}}. Also there is \isa{safe}, which like \isa{clarify} performs


1410 
obvious steps and even applies those that split goals.


1411 

10546

1412 
The \isa{force} method applies the classical reasoner and simplifier

10295

1413 
to one goal.

10546

1414 
\REMARK{example needed of \isa{force}?}

10295

1415 
Unless it can prove the goal, it fails. Contrast

10546

1416 
that with the \isa{auto} method, which also combines classical reasoning

10295

1417 
with simplification. The latter's purpose is to prove all the


1418 
easy subgoals and parts of subgoals. Unfortunately, it can produce


1419 
large numbers of new subgoals; also, since it proves some subgoals


1420 
and splits others, it obscures the structure of the proof tree.

10546

1421 
The \isa{force} method does not have these drawbacks. Another


1422 
difference: \isa{force} tries harder than {\isa{auto}} to prove

10295

1423 
its goal, so it can take much longer to terminate.


1424 


1425 
Older components of the classical reasoner have largely been


1426 
superseded by {\isa{blast}}, but they still have niche applications.


1427 
Most important among these are {\isa{fast}} and {\isa{best}}. While {\isa{blast}}


1428 
searches for proofs using a builtin firstorder reasoner, these


1429 
earlier methods search for proofs using standard Isabelle inference.


1430 
That makes them slower but enables them to work correctly in the


1431 
presence of the more unusual features of Isabelle rules, such


1432 
as type classes and function unknowns. For example, the introduction rule


1433 
for Hilbert's epsilonoperator has the following form:


1434 
\begin{isabelle}

10546

1435 
?P\ ?x\ \isasymLongrightarrow\ ?P\ (SOME\ x.\ ?P x)

10295

1436 
\rulename{someI}


1437 
\end{isabelle}


1438 


1439 
The repeated occurrence of the variable \isa{?P} makes this rule tricky


1440 
to apply. Consider this contrived example:


1441 
\begin{isabelle}


1442 
\isacommand{lemma}\ "{\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\isanewline


1443 
\ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ P\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)\


1444 
\isasymand\ Q\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)"\isanewline


1445 
\isacommand{apply}\ (rule\ someI)


1446 
\end{isabelle}


1447 
%


1448 
We can apply rule \isa{someI} explicitly. It yields the


1449 
following subgoal:


1450 
\begin{isabelle}


1451 
\ 1.\ {\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P\ ?x\


1452 
\isasymand\ Q\ ?x%


1453 
\end{isabelle}


1454 
The proof from this point is trivial. The question now arises, could we have

