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\


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


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}


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


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}


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


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


237 
functions of functional pr§gramming.%


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


310 
{"}P\ \isasymlongrightarrow\ (Q\


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 


375 
\remark{negation: notI, notE, ccontr, swap, contrapos?}


376 


377 


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


379 


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


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


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


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


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


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


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


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


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


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


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


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


392 


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


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


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


396 
They can be filled in later, often automatically.


397 


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


399 
unification, which is unification in the


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


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


402 
unification are straightforward. It handles bound variables


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


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


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


406 
bound. The two terms


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


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


409 


410 
Higherorder unification sometimes must invent


411 
$\lambda$terms to replace function variables,


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


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


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


415 
function variable is applied only to bound variables,


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


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


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


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


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


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


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


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


424 


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


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


427 
another if we know that two terms are equal.


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


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


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


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


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


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


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


435 


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


437 
\begin{isabelle}


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


439 
?t


440 
\rulename{ssubst}


441 
\end{isabelle}


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


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


444 
involving one bound variable whose occurrences identify the places


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


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


447 


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


449 
rule gives us more control. Consider this proof:


450 
\begin{isabelle}


451 
\isacommand{lemma}\


452 
"{\isasymlbrakk}\ x\


453 
=\ f\ x;\ odd(f\


454 
x)\ \isasymrbrakk\ \isasymLongrightarrow\ odd\


455 
x"\isanewline


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


457 
\isacommand{apply}\ assumption\isanewline


458 
\isacommand{done}\end{isabelle}


459 
%


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


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


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


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


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


465 
resulting subgoal is trivial by assumption.


466 


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


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


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


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


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


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


473 
assumption.


474 


475 


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


477 
\begin{isabelle}


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


479 
f\ x;\ triple\ (f\ x)\


480 
(f\ x)\ x\ \isasymrbrakk\


481 
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline


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


483 
\isacommand{back}\isanewline


484 
\isacommand{back}\isanewline


485 
\isacommand{back}\isanewline


486 
\isacommand{back}\isanewline


487 
\isacommand{apply}\ assumption\isanewline


488 
\isacommand{done}


489 
\end{isabelle}


490 
%


491 
By default, Isabelle tries to substitute for all the


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


493 
\begin{isabelle}


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


495 
\end{isabelle}


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


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


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


499 
\begin{isabelle}


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


501 
\end{isabelle}


502 
%


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


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


505 
again:


506 
\begin{isabelle}


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


508 
\end{isabelle}


509 
%


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


511 
\begin{isabelle}


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


513 
\end{isabelle}


514 
%


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


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


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


518 
\begin{isabelle}


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


520 
\end{isabelle}


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


522 


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


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


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


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


527 
fails then Isabelle automatically backtracks. This process continues until


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


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


530 
\begin{isabelle}


531 
\isacommand{lemma}\


532 
"{\isasymlbrakk}\ x\


533 
=\ f\ x;\ triple\ (f\


534 
x)\ (f\ x)\ x\


535 
\isasymrbrakk\


536 
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline


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


538 
\isacommand{done}


539 
\end{isabelle}


540 


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


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


543 
similar to \isa{rule}, but it


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


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


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


547 
\isa{erule}.


548 
\begin{isabelle}


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


550 
\isacommand{apply}\ (erule_tac\


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


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


553 
ssubst)\isanewline


554 
\isacommand{apply}\ assumption\isanewline


555 
\isacommand{done}


556 
\end{isabelle}


557 
%


558 
To specify a desired substitution


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


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


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


562 
the third unchanged.


563 


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


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


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


567 
variables bound in the current subgoal.


568 


569 


570 
\section{Negation}


571 


572 
Negation causes surprising complexity in proofs. Its natural


573 
deduction rules are straightforward, but additional rules seem


574 
necessary in order to handle negated assumptions gracefully.


575 


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


577 
contradiction. Negation elimination deduces any formula in the


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


579 
\begin{isabelle}


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


581 
\rulename{notI}\isanewline


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


583 
\rulename{notE}


584 
\end{isabelle}


585 
%


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


587 
when attempting to prove~$P$:


588 
\begin{isabelle}


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


590 
\rulename{classical}


591 
\end{isabelle}


592 
%


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


594 
They differ in the placement of the negation symbols:


595 
\begin{isabelle}


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


597 
\rulename{contrapos_pp}\isanewline


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


599 
\rulename{contrapos_np}\isanewline


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


601 
\rulename{contrapos_nn}


602 
\end{isabelle}


603 
%


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


605 
their effect is to form a contrapositive from an


606 
assumption and the goal's conclusion.


607 


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


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


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


611 
might want to use conjunction introduction on it.


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


613 
becomes the conclusion. The following proof demonstrates this


614 
technique:


615 
\begin{isabelle}


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


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


618 
R"\isanewline


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


620 
contrapos_np)\isanewline


621 
\isacommand{apply}\ intro\isanewline


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


623 
\isacommand{done}


624 
\end{isabelle}


625 
%


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


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


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


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


630 
\begin{isabelle}


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


632 
R\isasymrbrakk\ \isasymLongrightarrow\ R\ \isasymlongrightarrow\ Q%


633 
\end{isabelle}


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


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


636 
conclusion.


637 


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


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


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


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


642 
R\isasymrbrakk\ \isasymLongrightarrow\ Q%


643 
\end{isabelle}


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


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


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


647 
we combine the rule with the


648 
\isa{assumption} method:


649 
\begin{isabelle}


650 
\ \ \ \ \ (erule\ notE,\ assumption)


651 
\end{isabelle}


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


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


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


655 
concludes the proof.


656 


657 
\medskip


658 


659 
Here is another example.


660 
\begin{isabelle}


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


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


663 
\isacommand{apply}\ intro%


664 


665 


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


667 
\ \isacommand{apply}\ assumption


668 
\isanewline


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


670 
\ \ \isacommand{apply}\ assumption\isanewline


671 
\ \isacommand{apply}\ assumption\isanewline


672 
\isacommand{done}


673 
\end{isabelle}


674 
%


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


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


677 
R)}.


678 
\begin{isabelle}


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


680 
R)\isasymrbrakk\ \isasymLongrightarrow\ P%


681 
\end{isabelle}


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


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


684 


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


686 
elimination rules; here, the elimination rules given


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


688 
\begin{isabelle}


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


690 
\end{isabelle}


691 
%


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


693 
combination


694 
\begin{isabelle}


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


696 
\end{isabelle}


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


698 
conjunction. The two subgoals are the ones we would expect from appling


699 
conjunction introduction to


700 
\isa{Q\


701 
\isasymand\ R}:


702 
\begin{isabelle}


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


704 
Q\isanewline


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


706 
\end{isabelle}


707 
The rest of the proof is trivial.


708 


709 


710 
\section{The universal quantifier}


711 


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


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


714 
introduction rule looks like this:


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


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


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


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


719 
Isabelle's underlying formalism, called the


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


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


722 
already seen another symbol of the metalogic, namely


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


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


725 
can be used to define constants.


726 


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


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


729 
\begin{isabelle}


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


731 
\end{isabelle}


732 


733 


734 
The following trivial proof demonstrates how the universal introduction


735 
rule works.


736 
\begin{isabelle}


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


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


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


740 
\isacommand{apply}\ assumption


741 
\end{isabelle}


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


743 
\begin{isabelle}


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


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


746 
\end{isabelle}


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


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


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


750 
prove


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


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


753 
\begin{isabelle}


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


755 
\end{isabelle}


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


757 


758 
\medskip


759 
Now consider universal elimination. In a logic text,


760 
the rule looks like this:


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


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


763 
Isabelle expresses substitution using a function variable:


764 
\begin{isabelle}


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


766 
\end{isabelle}


767 
This destruction rule takes a


768 
universally quantified formula and removes the quantifier, replacing


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


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


771 
placeholder: it can be replaced by any term.


772 


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


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


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


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


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


778 
\isa{P\


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


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


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


782 
\begin{isabelle}


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


784 
\isasymlongrightarrow\ Q\ x)\ \isasymLongrightarrow\ P\


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


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


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


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


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


790 
\ \ \isacommand{apply}\ assumption\isanewline


791 
\ \isacommand{apply}\ assumption


792 
\end{isabelle}


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


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


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


796 
\begin{isabelle}


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


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


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


800 
\end{isabelle}


801 
As before, it replaces the HOL


802 
quantifier by a metalevel quantifier, producing a subgoal that


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


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


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


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


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


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


809 
rules add bound variables or assumptions.


810 


811 
Now, to reason from the universally quantified


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


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


814 
to a particular term.


815 
\begin{isabelle}


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


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


818 
\end{isabelle}


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


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


821 
removed the quantifier. The quantified variable


822 
has been replaced by the curious term


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


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


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


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


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


828 
\begin{isabelle}


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


830 
\isasymLongrightarrow\ Q\ x


831 
\end{isabelle}


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


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


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


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


836 
unifiable.


837 


838 
\medskip


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


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


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


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


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


844 


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


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


847 
additional~\isa{f}.


848 
\begin{isabelle}


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


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


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


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


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


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


855 
\isacommand{done}


856 
\end{isabelle}


857 
%


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


859 
\begin{isabelle}


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


861 
\end{isabelle}


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


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


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


865 
\begin{isabelle}


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


867 
\end{isabelle}


868 
%


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


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


871 
we then apply


872 
\begin{isabelle}


873 
\ \ \ \ \ (drule\ mp,\ assumption)


874 
\end{isabelle}


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


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


877 
Isabelle to backtrack and find the correct one.


878 


879 


880 
\section{The existential quantifier}


881 


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


883 
whose introduction rule looks like this in Isabelle:


884 
\begin{isabelle}


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


886 
\end{isabelle}


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


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


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


890 
elimination rule looks like this


891 
in a logic text:


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


893 
%


894 
It looks like this in Isabelle:


895 
\begin{isabelle}


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


897 
\end{isabelle}


898 
%


899 
Given an existentially quantified theorem and some


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


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


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


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


904 
quantifier to be built in as well.\remark{EX example needed?}


905 


906 
Isabelle/HOL also provides Hilbert's


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


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


909 
existential destruction rule:


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


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


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


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


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


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


916 
description) and proceed to prove other facts.\remark{SOME theorems


917 
and example}


918 


919 
\begin{exercise}


920 
Prove the lemma


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


922 
\emph{Hint}: the proof is similar


923 
to the one just above for the universal quantifier.


924 
\end{exercise}


925 


926 


927 
\section{Some proofs that fail}


928 


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


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


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


932 
the existential quantifier and conjunction.


933 
\begin{isabelle}


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


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


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


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


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


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


940 
\ \isacommand{apply}\ assumption\isanewline


941 
\isacommand{oops}


942 
\end{isabelle}


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


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


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


946 
the quantifiers.


947 
\begin{isabelle}


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


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


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


951 
\end{isabelle}


952 
%


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


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


955 
\begin{isabelle}


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


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


958 
\end{isabelle}


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


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


961 
no way to prove this subgoal. Removing the


962 
conclusion's existential quantifier yields two


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


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


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


966 
placeholder to be identical.


967 
\begin{isabelle}


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


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


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


971 
\end{isabelle}


972 
We can prove either subgoal


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


974 
changes into~\bigisa{x}.


975 
\begin{isabelle}


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


977 
\isasymLongrightarrow\ Q\ x


978 
\end{isabelle}


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


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


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


982 
error message:


983 
\begin{isabelle}


984 
*** empty result sequence  proof command failed


985 
\end{isabelle}


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


987 


988 
\medskip


989 


990 
Here is another abortive proof, illustrating the interaction between


991 
bound variables and unknowns.


992 
If $R$ is a reflexive relation,


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


994 
we attempt to prove it.


995 
\begin{isabelle}


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


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


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


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


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


1001 
\isacommand{oops}


1002 
\end{isabelle}


1003 
First,


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


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


1006 
\begin{isabelle}


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


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


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


1010 
\end{isabelle}


1011 
Next, we remove the universal quantifier


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


1013 
\begin{isabelle}


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


1015 
\end{isabelle}


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


1017 
new assumption whose identical placeholders may be replaced by


1018 
any term involving~\bigisa{y}.


1019 
\begin{isabelle}


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


1021 
\end{isabelle}


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


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


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


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


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


1027 
instantiating


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


1029 


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


1031 


1032 


1033 
\section{Proving theorems using the \emph{\texttt{blast}} method}


1034 


1035 
It is hard to prove substantial theorems using the methods


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


1037 
may need to search among different ways of proving certain


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


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


1040 
discussed, concerning negation and disjunction. Isabelle's


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


1042 
proofs automatically. The most important of these is the


1043 
{\isa{blast}} method.


1044 


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


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


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


1048 


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


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


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


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


1053 
problems for automatic theorem provers.}


1054 
The nested biconditionals cause an exponential explosion: the formal


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


1056 
a fraction of a second.


1057 
\begin{isabelle}


1058 
\isacommand{lemma}\


1059 
"(({\isasymexists}x.\


1060 
{\isasymforall}y.\


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


1062 
=\


1063 
(({\isasymexists}x.\


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


1065 
p(y){)}){)}\


1066 
\ \ =\ \ \ \ \isanewline


1067 
\ \ \ \ \ \ \ \


1068 
(({\isasymexists}x.\


1069 
{\isasymforall}y.\


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


1071 
=\


1072 
(({\isasymexists}x.\


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


1074 
q(y){)}){)}"\isanewline


1075 
\isacommand{apply}\ blast\isanewline


1076 
\isacommand{done}


1077 
\end{isabelle}


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


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


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


1081 
experiment with variations of this formula and see which ones


1082 
can be proved.


1083 
\begin{isabelle}


1084 
\isacommand{lemma}\


1085 
"({\isasymforall}x.\


1086 
honest(x)\ \isasymand\


1087 
industrious(x)\ \isasymlongrightarrow\


1088 
healthy(x){)}\


1089 
\isasymand\ \ \isanewline


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


1091 
grocer(x)\ \isasymand\


1092 
healthy(x){)}\


1093 
\isasymand\ \isanewline


1094 
\ \ \ \ \ \ \ \ ({\isasymforall}x.\


1095 
industrious(x)\ \isasymand\


1096 
grocer(x)\ \isasymlongrightarrow\


1097 
honest(x){)}\


1098 
\isasymand\ \isanewline


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


1100 
cyclist(x)\ \isasymlongrightarrow\


1101 
industrious(x){)}\


1102 
\isasymand\ \isanewline


1103 
\ \ \ \ \ \ \ \ ({\isasymforall}x.\


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


1105 
cyclist(x)\ \isasymlongrightarrow\


1106 
{\isasymnot}honest(x){)}\


1107 
\ \isanewline


1108 
\ \ \ \ \ \ \ \ \isasymlongrightarrow\


1109 
({\isasymforall}x.\


1110 
grocer(x)\ \isasymlongrightarrow\


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


1112 
\isacommand{apply}\ blast\isanewline


1113 
\isacommand{done}


1114 
\end{isabelle}


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


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


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


1118 
\begin{isabelle}


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


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


1121 
\isacommand{apply}\ blast\isanewline


1122 
\isacommand{done}


1123 
\end{isabelle}


1124 


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


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


1127 
Extending it effectively requires understanding the notions of


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


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


1130 
that can be applied backwards without losing information; an


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


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


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


1134 
classical reasoner backtracks to the most recent unsafe rule application


1135 
and makes another choice.


1136 


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


1138 
equivalence, which in higherorder logic is an equality between


1139 
formulas, can be given to the classical


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


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


1142 
simpler than the lefthand side.


1143 


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


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


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


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


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


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


1150 
\begin{isabelle}


1151 
\isacommand{lemma}\


1152 
[iff]{:}\


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


1154 
\isacharbrackleft{]})\ =\


1155 
(xs=[]\


1156 
\isacharampersand\


1157 
ys=[]{)}"\isanewline


1158 
\isacommand{apply}\ (induct_tac\


1159 
xs)\isanewline


1160 
\isacommand{apply}\ (simp_all)


1161 
\isanewline


1162 
\isacommand{done}


1163 
\end{isabelle}


1164 
%


1165 
This fact about multiplication is also appropriate for


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


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


1168 
\begin{isabelle}


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


1170 
\end{isabelle}


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


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


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


1174 
works: the classical reasoner handles disjunction properly.


1175 


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


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


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


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


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


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


1182 
simplifier. But classical reasoning is different from


1183 
simplification. Simplification is deterministic: it applies rewrite rules


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


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


1186 


1187 


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


1189 
\label{sec:provingeuclid}


1190 


1191 
A brief development will illustrate advanced use of


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


1193 
recursive function {\isa{gcd}}:


1194 
\begin{isabelle}


1195 
\isacommand{consts}\ gcd\ :{:}\ {"}nat{\isacharasterisk}nat={\isachargreater}nat"\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline


1196 
\isacommand{recdef}\ gcd\ {"}measure\ ((\isasymlambda(m{,}n){.}n)\ :{:}nat{\isacharasterisk}nat={\isachargreater}nat){"}\isanewline


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


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}


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


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


1210 
%\isacommand{done}


1211 
%\end{isabelle}


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


1213 
%\begin{isabelle}


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


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}


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


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}


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


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


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


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


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


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\


1321 
[rule_format]{:}\isanewline


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


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


1324 
n)\ \isasymlongrightarrow\ k\ dvd\


1325 
gcd(m{,}n)"\isanewline


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


1327 
rule:\ gcd{.}induct)\isanewline


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


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}


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


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 


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


1413 
to one goal.


1414 
\remark{example needed? most


1415 
things done by blast, simp or auto can also be done by force, so why add a new


1416 
one?}


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


1418 
that with the auto method, which also combines classical reasoning


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


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


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


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


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


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


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


1426 


1427 
Older components of the classical reasoner have largely been


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


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


1430 
searches for proofs using a builtin firstorder reasoner, these


1431 
earlier methods search for proofs using standard Isabelle inference.


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


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


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


1435 
for Hilbert's epsilonoperator has the following form:


1436 
\begin{isabelle}


1437 
?P\ ?x\ \isasymLongrightarrow\ ?P\ (Eps\ ?P)


1438 
\rulename{someI}


1439 
\end{isabelle}


1440 


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


1442 
to apply. Consider this contrived example:


1443 
\begin{isabelle}


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


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


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


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


1448 
\end{isabelle}


1449 
%


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


1451 
following subgoal:


1452 
\begin{isabelle}


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


1454 
\isasymand\ Q\ ?x%


1455 
\end{isabelle}


1456 