\chapter{The Rules of the Game}
\label{chap:rules}
Until now, we have proved everything using only induction and simplification.
Substantial proofs require more elaborate forms of inference. This chapter
outlines the concepts and techniques that underlie reasoning in Isabelle. The examples
are mainly drawn from predicate logic. The first examples in this
chapter will consist of detailed, low-level proof steps. Later, we shall
see how to automate such reasoning using the methods \isa{blast},
\isa{auto} and others.
\section{Natural deduction}
In Isabelle, proofs are constructed using inference rules. The
most familiar inference rule is probably \emph{modus ponens}:
\[ \infer{Q}{P\imp Q & P} \]
This rule says that from $P\imp Q$ and $P$
we may infer~$Q$.
%Early logical formalisms had this
%rule and at most one or two others, along with many complicated
%axioms. Any desired theorem could be obtained by applying \emph{modus
%ponens} or other rules to the axioms, but proofs were
%hard to find. For example, a standard inference system has
%these two axioms (amongst others):
%\begin{gather*}
% P\imp(Q\imp P) \tag{K}\\
% (P\imp(Q\imp R))\imp ((P\imp Q)\imp(P\imp R)) \tag{S}
%\end{gather*}
%Try proving the trivial fact $P\imp P$ using these axioms and \emph{modus
%ponens}!
\textbf{Natural deduction} is an attempt to formalize logic in a way
that mirrors human reasoning patterns.
%
%Instead of having a few
%inference rules and many axioms, it has many inference rules
%and few axioms.
%
For each logical symbol (say, $\conj$), there
are two kinds of rules: \textbf{introduction} and \textbf{elimination} rules.
The introduction rules allow us to infer this symbol (say, to
infer conjunctions). The elimination rules allow us to deduce
consequences from this symbol. Ideally each rule should mention
one symbol only. For predicate logic this can be
done, but when users define their own concepts they typically
have to refer to other symbols as well. It is best not be dogmatic.
Natural deduction generally deserves its name. It is easy to use. Each
proof step consists of identifying the outermost symbol of a formula and
applying the corresponding rule. It creates new subgoals in
an obvious way from parts of the chosen formula. Expanding the
definitions of constants can blow up the goal enormously. Deriving natural
deduction rules for such constants lets us reason in terms of their key
properties, which might otherwise be obscured by the technicalities of its
definition. Natural deduction rules also lend themselves to automation.
Isabelle's
\textbf{classical reasoner} accepts any suitable collection of natural deduction
rules and uses them to search for proofs automatically. Isabelle is designed around
natural deduction and many of its tools use the terminology of introduction and
elimination rules.
\section{Introduction rules}
An \textbf{introduction} rule tells us when we can infer a formula
containing a specific logical symbol. For example, the conjunction
introduction rule says that if we have $P$ and if we have $Q$ then
we have $P\conj Q$. In a mathematics text, it is typically shown
like this:
\[ \infer{P\conj Q}{P & Q} \]
The rule introduces the conjunction
symbol~($\conj$) in its conclusion. Of course, in Isabelle proofs we
mainly reason backwards. When we apply this rule, the subgoal already has
the form of a conjunction; the proof step makes this conjunction symbol
disappear.
In Isabelle notation, the rule looks like this:
\begin{isabelle}
\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulename{conjI}
\end{isabelle}
Carefully examine the syntax. The premises appear to the
left of the arrow and the conclusion to the right. The premises (if
more than one) are grouped using the fat brackets. The question marks
indicate \textbf{schematic variables} (also called \textbf{unknowns}): they may
be replaced by arbitrary formulas. If we use the rule backwards, Isabelle
tries to unify the current subgoal with the conclusion of the rule, which
has the form \isa{?P\ \isasymand\ ?Q}. (Unification is discussed below,
\S\ref{sec:unification}.) If successful,
it yields new subgoals given by the formulas assigned to
\isa{?P} and \isa{?Q}.
The following trivial proof illustrates this point.
\begin{isabelle}
\isacommand{lemma}\ conj_rule:\ "{\isasymlbrakk}P;\
Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\
(Q\ \isasymand\ P){"}\isanewline
\isacommand{apply}\ (rule\ conjI)\isanewline
\ \isacommand{apply}\ assumption\isanewline
\isacommand{apply}\ (rule\ conjI)\isanewline
\ \isacommand{apply}\ assumption\isanewline
\isacommand{apply}\ assumption
\end{isabelle}
At the start, Isabelle presents
us with the assumptions (\isa{P} and~\isa{Q}) and with the goal to be proved,
\isa{P\ \isasymand\
(Q\ \isasymand\ P)}. We are working backwards, so when we
apply conjunction introduction, the rule removes the outermost occurrence
of the \isa{\isasymand} symbol. To apply a rule to a subgoal, we apply
the proof method {\isa{rule}} --- here with {\isa{conjI}}, the conjunction
introduction rule.
\begin{isabelle}
%{\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\
%\isasymand\ P\isanewline
\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
\ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P
\end{isabelle}
Isabelle leaves two new subgoals: the two halves of the original conjunction.
The first is simply \isa{P}, which is trivial, since \isa{P} is among
the assumptions. We can apply the {\isa{assumption}}
method, which proves a subgoal by finding a matching assumption.
\begin{isabelle}
\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\
Q\ \isasymand\ P
\end{isabelle}
We are left with the subgoal of proving
\isa{Q\ \isasymand\ P} from the assumptions \isa{P} and~\isa{Q}. We apply
\isa{rule conjI} again.
\begin{isabelle}
\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline
\ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P
\end{isabelle}
We are left with two new subgoals, \isa{Q} and~\isa{P}, each of which can be proved
using the {\isa{assumption}} method.
\section{Elimination rules}
\textbf{Elimination} rules work in the opposite direction from introduction
rules. In the case of conjunction, there are two such rules.
From $P\conj Q$ we infer $P$. also, from $P\conj Q$
we infer $Q$:
\[ \infer{P}{P\conj Q} \qquad \infer{Q}{P\conj Q} \]
Now consider disjunction. There are two introduction rules, which resemble inverted forms of the
conjunction elimination rules:
\[ \infer{P\disj Q}{P} \qquad \infer{P\disj Q}{Q} \]
What is the disjunction elimination rule? The situation is rather different from
conjunction. From $P\disj Q$ we cannot conclude that $P$ is true and we
cannot conclude that $Q$ is true; there are no direct
elimination rules of the sort that we have seen for conjunction. Instead,
there is an elimination rule that works indirectly. If we are trying to prove
something else, say $R$, and we know that $P\disj Q$ holds, then we have to consider
two cases. We can assume that $P$ is true and prove $R$ and then assume that $Q$ is
true and prove $R$ a second time. Here we see a fundamental concept used in natural
deduction: that of the \textbf{assumptions}. We have to prove $R$ twice, under
different assumptions. The assumptions are local to these subproofs and are visible
nowhere else.
In a logic text, the disjunction elimination rule might be shown
like this:
\[ \infer{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}} \]
The assumptions $[P]$ and $[Q]$ are bracketed
to emphasize that they are local to their subproofs. In Isabelle
notation, the already-familiar \isa\isasymLongrightarrow syntax serves the
same purpose:
\begin{isabelle}
\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE}
\end{isabelle}
When we use this sort of elimination rule backwards, it produces
a case split. (We have this before, in proofs by induction.) The following proof
illustrates the use of disjunction elimination.
\begin{isabelle}
\isacommand{lemma}\ disj_swap:\ {"}P\ \isasymor\ Q\
\isasymLongrightarrow\ Q\ \isasymor\ P"\isanewline
\isacommand{apply}\ (erule\ disjE)\isanewline
\ \isacommand{apply}\ (rule\ disjI2)\isanewline
\ \isacommand{apply}\ assumption\isanewline
\isacommand{apply}\ (rule\ disjI1)\isanewline
\isacommand{apply}\ assumption
\end{isabelle}
We assume \isa{P\ \isasymor\ Q} and
must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction
elimination rule, \isa{disjE}. The method {\isa{erule}} applies an
elimination rule to the assumptions, searching for one that matches the
rule's first premise. Deleting that assumption, it
return the subgoals for the remaining premises. Most of the
time, this is the best way to use elimination rules; only rarely is there
any point in keeping the assumption.
\begin{isabelle}
%P\ \isasymor\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline
\ 1.\ P\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline
\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
\end{isabelle}
Here it leaves us with two subgoals. The first assumes \isa{P} and the
second assumes \isa{Q}. Tackling the first subgoal, we need to
show \isa{Q\ \isasymor\ P}\@. The second introduction rule (\isa{disjI2})
can reduce this to \isa{P}, which matches the assumption. So, we apply the
{\isa{rule}} method with \isa{disjI2} \ldots
\begin{isabelle}
\ 1.\ P\ \isasymLongrightarrow\ P\isanewline
\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
\end{isabelle}
\ldots and finish off with the {\isa{assumption}}
method. We are left with the other subgoal, which
assumes \isa{Q}.
\begin{isabelle}
\ 1.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
\end{isabelle}
Its proof is similar, using the introduction
rule \isa{disjI1}.
The result of this proof is a new inference rule \isa{disj_swap}, which is neither
an introduction nor an elimination rule, but which might
be useful. We can use it to replace any goal of the form $Q\disj P$
by a one of the form $P\disj Q$.
\section{Destruction rules: some examples}
Now let us examine the analogous proof for conjunction.
\begin{isabelle}
\isacommand{lemma}\ conj_swap:\ {"}P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P"\isanewline
\isacommand{apply}\ (rule\ conjI)\isanewline
\ \isacommand{apply}\ (drule\ conjunct2)\isanewline
\ \isacommand{apply}\ assumption\isanewline
\isacommand{apply}\ (drule\ conjunct1)\isanewline
\isacommand{apply}\ assumption
\end{isabelle}
Recall that the conjunction elimination rules --- whose Isabelle names are
\isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half
of a conjunction. Rules of this sort (where the conclusion is a subformula of a
premise) are called \textbf{destruction} rules, by analogy with the destructor
functions of functional pr§gramming.%
\footnote{This Isabelle terminology has no counterpart in standard logic texts,
although the distinction between the two forms of elimination rule is well known.
Girard \cite[page 74]{girard89}, for example, writes ``The elimination rules are very
bad. What is catastrophic about them is the parasitic presence of a formula [$R$]
which has no structural link with the formula which is eliminated.''}
The first proof step applies conjunction introduction, leaving
two subgoals:
\begin{isabelle}
%P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P\isanewline
\ 1.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\isanewline
\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P
\end{isabelle}
To invoke the elimination rule, we apply a new method, \isa{drule}.
Think of the \isa{d} as standing for \textbf{destruction} (or \textbf{direct}, if
you prefer). Applying the
second conjunction rule using \isa{drule} replaces the assumption
\isa{P\ \isasymand\ Q} by \isa{Q}.
\begin{isabelle}
\ 1.\ Q\ \isasymLongrightarrow\ Q\isanewline
\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P
\end{isabelle}
The resulting subgoal can be proved by applying \isa{assumption}.
The other subgoal is similarly proved, using the \isa{conjunct1} rule and the
\isa{assumption} method.
Choosing among the methods \isa{rule}, \isa{erule} and \isa{drule} is up to
you. Isabelle does not attempt to work out whether a rule
is an introduction rule or an elimination rule. The
method determines how the rule will be interpreted. Many rules
can be used in more than one way. For example, \isa{disj_swap} can
be applied to assumptions as well as to goals; it replaces any
assumption of the form
$P\disj Q$ by a one of the form $Q\disj P$.
Destruction rules are simpler in form than indirect rules such as \isa{disjE},
but they can be inconvenient. Each of the conjunction rules discards half
of the formula, when usually we want to take both parts of the conjunction as new
assumptions. The easiest way to do so is by using an
alternative conjunction elimination rule that resembles \isa{disjE}. It is seldom,
if ever, seen in logic books. In Isabelle syntax it looks like this:
\begin{isabelle}
\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{conjE}
\end{isabelle}
\begin{exercise}
Use the rule {\isa{conjE}} to shorten the proof above.
\end{exercise}
\section{Implication}
At the start of this chapter, we saw the rule \textit{modus ponens}. It is, in fact,
a destruction rule. The matching introduction rule looks like this
in Isabelle:
\begin{isabelle}
(?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\
\isasymlongrightarrow\ ?Q\rulename{impI}
\end{isabelle}
And this is \textit{modus ponens}:
\begin{isabelle}
\isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\
\isasymLongrightarrow\ ?Q
\rulename{mp}
\end{isabelle}
Here is a proof using the rules for implication. This
lemma performs a sort of uncurrying, replacing the two antecedents
of a nested implication by a conjunction.
\begin{isabelle}
\isacommand{lemma}\ imp_uncurry:\
{"}P\ \isasymlongrightarrow\ (Q\
\isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\
\isasymand\ Q\ \isasymlongrightarrow\
R"\isanewline
\isacommand{apply}\ (rule\ impI)\isanewline
\isacommand{apply}\ (erule\ conjE)\isanewline
\isacommand{apply}\ (drule\ mp)\isanewline
\ \isacommand{apply}\ assumption\isanewline
\isacommand{apply}\ (drule\ mp)\isanewline
\ \ \isacommand{apply}\ assumption\isanewline
\ \isacommand{apply}\ assumption
\end{isabelle}
First, we state the lemma and apply implication introduction (\isa{rule impI}),
which moves the conjunction to the assumptions.
\begin{isabelle}
%P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R\ \isasymLongrightarrow\ P\
%\isasymand\ Q\ \isasymlongrightarrow\ R\isanewline
\ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R
\end{isabelle}
Next, we apply conjunction elimination (\isa{erule conjE}), which splits this
conjunction into two parts.
\begin{isabelle}
\ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\
Q\isasymrbrakk\ \isasymLongrightarrow\ R
\end{isabelle}
Now, we work on the assumption \isa{P\ \isasymlongrightarrow\ (Q\
\isasymlongrightarrow\ R)}, where the parentheses have been inserted for
clarity. The nested implication requires two applications of
\textit{modus ponens}: \isa{drule mp}. The first use yields the
implication \isa{Q\
\isasymlongrightarrow\ R}, but first we must prove the extra subgoal
\isa{P}, which we do by assumption.
\begin{isabelle}
\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
\ 2.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R
\end{isabelle}
Repeating these steps for \isa{Q\
\isasymlongrightarrow\ R} yields the conclusion we seek, namely~\isa{R}.
\begin{isabelle}
\ 1.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\
\isasymLongrightarrow\ R
\end{isabelle}
The symbols \isa{\isasymLongrightarrow} and \isa{\isasymlongrightarrow}
both stand for implication, but they differ in many respects. Isabelle
uses \isa{\isasymLongrightarrow} to express inference rules; the symbol is
built-in and Isabelle's inference mechanisms treat it specially. On the
other hand, \isa{\isasymlongrightarrow} is just one of the many connectives
available in higher-order logic. We reason about it using inference rules
such as \isa{impI} and \isa{mp}, just as we reason about the other
connectives. You will have to use \isa{\isasymlongrightarrow} in any
context that requires a formula of higher-order logic. Use
\isa{\isasymLongrightarrow} to separate a theorem's preconditions from its
conclusion.
When using induction, often the desired theorem results in an induction
hypothesis that is too weak. In such cases you may have to invent a more
complicated induction formula, typically involving
\isa{\isasymlongrightarrow} and \isa{\isasymforall}. From this lemma you
derive the desired theorem , typically involving
\isa{\isasymLongrightarrow}. We shall see an example below,
\S\ref{sec:proving-euclid}.
\remark{negation: notI, notE, ccontr, swap, contrapos?}
\section{Unification and substitution}\label{sec:unification}
As we have seen, Isabelle rules involve variables that begin with a
question mark. These are called \textbf{schematic} variables and act as
placeholders for terms. \textbf{Unification} refers to the process of
making two terms identical, possibly by replacing their variables by
terms. The simplest case is when the two terms are already the same. Next
simplest is when the variables in only one of the term
are replaced; this is called \textbf{pattern-matching}. The
{\isa{rule}} method typically matches the rule's conclusion
against the current subgoal. In the most complex case, variables in both
terms are replaced; the {\isa{rule}} method can do this the goal
itself contains schematic variables. Other occurrences of the variables in
the rule or proof state are updated at the same time.
Schematic variables in goals are sometimes called \textbf{unknowns}. They
are useful because they let us proceed with a proof even when we do not
know what certain terms should be --- as when the goal is $\exists x.\,P$.
They can be filled in later, often automatically.
Unification is well known to Prolog programmers. Isabelle uses \textbf{higher-order}
unification, which is unification in the
typed $\lambda$-calculus. The general case is
undecidable, but for our purposes, the differences from ordinary
unification are straightforward. It handles bound variables
correctly, avoiding capture. The two terms \isa{{\isasymlambda}x.\ ?P} and
\isa{{\isasymlambda}x.\ t x} are not unifiable; replacing \isa{?P} by
\isa{t x} is forbidden because the free occurrence of~\isa{x} would become
bound. The two terms
\isa{{\isasymlambda}x.\ f(x,z)} and \isa{{\isasymlambda}y.\ f(y,z)} are
trivially unifiable because they differ only by a bound variable renaming.
Higher-order unification sometimes must invent
$\lambda$-terms to replace function variables,
which can lead to a combinatorial explosion. However, Isabelle proofs tend
to involve easy cases where there are few possibilities for the
$\lambda$-term being constructed. In the easiest case, the
function variable is applied only to bound variables,
as when we try to unify \isa{{\isasymlambda}x\ y.\ f(?h x y)} and
\isa{{\isasymlambda}x\ y.\ f(x+y+a)}. The only solution is to replace
\isa{?h} by \isa{{\isasymlambda}x\ y.\ x+y+a}. Such cases admit at most
one unifier, like ordinary unification. A harder case is
unifying \isa{?h a} with~\isa{a+b}; it admits two solutions for \isa{?h},
namely \isa{{\isasymlambda}x.~a+b} and \isa{{\isasymlambda}x.~x+b}.
Unifying \isa{?h a} with~\isa{a+a+b} admits four solutions; their number is
exponential in the number of occurrences of~\isa{a} in the second term.
Isabelle also uses function variables to express \textbf{substitution}.
A typical substitution rule allows us to replace one term by
another if we know that two terms are equal.
\[ \infer{P[t/x]}{s=t & P[s/x]} \]
The conclusion uses a notation for substitution: $P[t/x]$ is the result of
replacing $x$ by~$t$ in~$P$. The rule only substitutes in the positions
designated by~$x$, which gives it additional power. For example, it can
derive symmetry of equality from reflexivity. Using $x=s$ for~$P$
replaces just the first $s$ in $s=s$ by~$t$.
\[ \infer{t=s}{s=t & \infer{s=s}{}} \]
The Isabelle version of the substitution rule looks like this:
\begin{isabelle}
\isasymlbrakk?t\ =\ ?s;\ ?P\ ?s\isasymrbrakk\ \isasymLongrightarrow\ ?P\
?t
\rulename{ssubst}
\end{isabelle}
Crucially, \isa{?P} is a function
variable: it can be replaced by a $\lambda$-expression
involving one bound variable whose occurrences identify the places
in which $s$ will be replaced by~$t$. The proof above requires
\isa{{\isasymlambda}x.~x=s}.
The \isa{simp} method replaces equals by equals, but using the substitution
rule gives us more control. Consider this proof:
\begin{isabelle}
\isacommand{lemma}\
"{\isasymlbrakk}\ x\
=\ f\ x;\ odd(f\
x)\ \isasymrbrakk\ \isasymLongrightarrow\ odd\
x"\isanewline
\isacommand{apply}\ (erule\ ssubst)\isanewline
\isacommand{apply}\ assumption\isanewline
\isacommand{done}\end{isabelle}
%
The simplifier might loop, replacing \isa{x} by \isa{f x} and then by
\isa{f(f x)} and so forth. (Actually, \isa{simp}
sees the danger and re-orients this equality, but in more complicated cases
it can be fooled.) When we apply substitution, Isabelle replaces every
\isa{x} in the subgoal by \isa{f x} just once: it cannot loop. The
resulting subgoal is trivial by assumption.
We are using the \isa{erule} method it in a novel way. Hitherto,
the conclusion of the rule was just a variable such as~\isa{?R}, but it may
be any term. The conclusion is unified with the subgoal just as
it would be with the \isa{rule} method. At the same time \isa{erule} looks
for an assumption that matches the rule's first premise, as usual. With
\isa{ssubst} the effect is to find, use and delete an equality
assumption.
Higher-order unification can be tricky, as this example indicates:
\begin{isabelle}
\isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\
f\ x;\ triple\ (f\ x)\
(f\ x)\ x\ \isasymrbrakk\
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
\isacommand{apply}\ (erule\ ssubst)\isanewline
\isacommand{back}\isanewline
\isacommand{back}\isanewline
\isacommand{back}\isanewline
\isacommand{back}\isanewline
\isacommand{apply}\ assumption\isanewline
\isacommand{done}
\end{isabelle}
%
By default, Isabelle tries to substitute for all the
occurrences. Applying \isa{erule\ ssubst} yields this subgoal:
\begin{isabelle}
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ (f\ x)
\end{isabelle}
The substitution should have been done in the first two occurrences
of~\isa{x} only. Isabelle has gone too far. The \isa{back}
method allows us to reject this possibility and get a new one:
\begin{isabelle}
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ (f\ x)\ (f\ x)
\end{isabelle}
%
Now Isabelle has left the first occurrence of~\isa{x} alone. That is
promising but it is not the desired combination. So we use \isa{back}
again:
\begin{isabelle}
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ x\ (f\ x)
\end{isabelle}
%
This also is wrong, so we use \isa{back} again:
\begin{isabelle}
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ x\ (f\ x)
\end{isabelle}
%
And this one is wrong too. Looking carefully at the series
of alternatives, we see a binary countdown with reversed bits: 111,
011, 101, 001. Invoke \isa{back} again:
\begin{isabelle}
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ x%
\end{isabelle}
At last, we have the right combination! This goal follows by assumption.
Never use {\isa{back}} in the final version of a proof.
It should only be used for exploration. One way to get rid of {\isa{back}}
to combine two methods in a single \textbf{apply} command. Isabelle
applies the first method and then the second. If the second method
fails then Isabelle automatically backtracks. This process continues until
the first method produces an output that the second method can
use. We get a one-line proof of our example:
\begin{isabelle}
\isacommand{lemma}\
"{\isasymlbrakk}\ x\
=\ f\ x;\ triple\ (f\
x)\ (f\ x)\ x\
\isasymrbrakk\
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
\isacommand{apply}\ (erule\ ssubst,\ assumption)\isanewline
\isacommand{done}
\end{isabelle}
The most general way to get rid of the {\isa{back}} command is
to instantiate variables in the rule. The method {\isa{rule\_tac}} is
similar to \isa{rule}, but it
makes some of the rule's variables denote specified terms.
Also available are {\isa{drule\_tac}} and \isa{erule\_tac}. Here we need
\isa{erule\_tac} since above we used
\isa{erule}.
\begin{isabelle}
\isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
\isacommand{apply}\ (erule_tac\
P={"}{\isasymlambda}u.\ triple\ u\
u\ x"\ \isakeyword{in}\
ssubst)\isanewline
\isacommand{apply}\ assumption\isanewline
\isacommand{done}
\end{isabelle}
%
To specify a desired substitution
requires instantiating the variable \isa{?P} with a $\lambda$-expression.
The bound variable occurrences in \isa{{\isasymlambda}u.\ P\ u\
u\ x} indicate that the first two arguments have to be substituted, leaving
the third unchanged.
An alternative to {\isa{rule\_tac}} is to use \isa{rule} with the
{\isa{of}} directive, described in \S\ref{sec:forward} below. An
advantage of {\isa{rule\_tac}} is that the instantiations may refer to
variables bound in the current subgoal.
\section{Negation}
Negation causes surprising complexity in proofs. Its natural
deduction rules are straightforward, but additional rules seem
necessary in order to handle negated assumptions gracefully.
Negation introduction deduces $\neg P$ if assuming $P$ leads to a
contradiction. Negation elimination deduces any formula in the
presence of $\neg P$ together with~$P$:
\begin{isabelle}
(?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P%
\rulename{notI}\isanewline
\isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R%
\rulename{notE}
\end{isabelle}
%
Classical logic allows us to assume $\neg P$
when attempting to prove~$P$:
\begin{isabelle}
(\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P%
\rulename{classical}
\end{isabelle}
%
Three further rules are variations on the theme of contrapositive.
They differ in the placement of the negation symbols:
\begin{isabelle}
\isasymlbrakk?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
\rulename{contrapos_pp}\isanewline
\isasymlbrakk{\isasymnot}\ ?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
\rulename{contrapos_np}\isanewline
\isasymlbrakk{\isasymnot}\ ?Q;\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ \isasymnot\ ?P%
\rulename{contrapos_nn}
\end{isabelle}
%
These rules are typically applied using the {\isa{erule}} method, where
their effect is to form a contrapositive from an
assumption and the goal's conclusion.
The most important of these is \isa{contrapos_np}. It is useful
for applying introduction rules to negated assumptions. For instance,
the assumption $\neg(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we
might want to use conjunction introduction on it.
Before we can do so, we must move that assumption so that it
becomes the conclusion. The following proof demonstrates this
technique:
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\
\isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\
R"\isanewline
\isacommand{apply}\ (erule_tac\ Q="R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
contrapos_np)\isanewline
\isacommand{apply}\ intro\isanewline
\isacommand{apply}\ (erule\ notE,\ assumption)\isanewline
\isacommand{done}
\end{isabelle}
%
There are two negated assumptions and we need to exchange the conclusion with the
second one. The method \isa{erule contrapos_np} would select the first assumption,
which we do not want. So we specify the desired assumption explicitly, using
\isa{erule_tac}. This is the resulting subgoal:
\begin{isabelle}
\ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\
R\isasymrbrakk\ \isasymLongrightarrow\ R\ \isasymlongrightarrow\ Q%
\end{isabelle}
The former conclusion, namely \isa{R}, now appears negated among the assumptions,
while the negated formula \isa{R\ \isasymlongrightarrow\ Q} becomes the new
conclusion.
We can now apply introduction rules. We use the {\isa{intro}} method, which
repeatedly applies built-in introduction rules. Here its effect is equivalent
to \isa{rule impI}.\begin{isabelle}
\ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ R;\
R\isasymrbrakk\ \isasymLongrightarrow\ Q%
\end{isabelle}
We can see a contradiction in the form of assumptions \isa{\isasymnot\ R}
and~\isa{R}, which suggests using negation elimination. If applied on its own,
however, it will select the first negated assumption, which is useless. Instead,
we combine the rule with the
\isa{assumption} method:
\begin{isabelle}
\ \ \ \ \ (erule\ notE,\ assumption)
\end{isabelle}
Now when Isabelle selects the first assumption, it tries to prove \isa{P\
\isasymlongrightarrow\ Q} and fails; it then backtracks, finds the
assumption~\isa{\isasymnot\ R} and finally proves \isa{R} by assumption. That
concludes the proof.
\medskip
Here is another example.
\begin{isabelle}
\isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\
\isasymLongrightarrow\ P\ \isasymor\ Q\ \isasymand\ R"\isanewline
\isacommand{apply}\ intro%
\isacommand{apply}\ (elim\ conjE\ disjE)\isanewline
\ \isacommand{apply}\ assumption
\isanewline
\isacommand{apply}\ (erule\ contrapos_np,\ rule\ conjI)\isanewline
\ \ \isacommand{apply}\ assumption\isanewline
\ \isacommand{apply}\ assumption\isanewline
\isacommand{done}
\end{isabelle}
%
The first proof step applies the {\isa{intro}} method, which repeatedly
uses built-in introduction rules. Here it creates the negative assumption \isa{\isasymnot\ (Q\ \isasymand\
R)}.
\begin{isabelle}
\ 1.\ \isasymlbrakk(P\ \isasymor\ Q)\ \isasymand\ R;\ \isasymnot\ (Q\ \isasymand\
R)\isasymrbrakk\ \isasymLongrightarrow\ P%
\end{isabelle}
It comes from \isa{disjCI}, a disjunction introduction rule that is more
powerful than the separate rules \isa{disjI1} and \isa{disjI2}.
Next we apply the {\isa{elim}} method, which repeatedly applies
elimination rules; here, the elimination rules given
in the command. One of the subgoals is trivial, leaving us with one other:
\begin{isabelle}
\ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P%
\end{isabelle}
%
Now we must move the formula \isa{Q\ \isasymand\ R} to be the conclusion. The
combination
\begin{isabelle}
\ \ \ \ \ (erule\ contrapos_np,\ rule\ conjI)
\end{isabelle}
is robust: the \isa{conjI} forces the \isa{erule} to select a
conjunction. The two subgoals are the ones we would expect from appling
conjunction introduction to
\isa{Q\
\isasymand\ R}:
\begin{isabelle}
\ 1.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\
Q\isanewline
\ 2.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R%
\end{isabelle}
The rest of the proof is trivial.
\section{The universal quantifier}
Quantifiers require formalizing syntactic substitution and the notion of \textbf{arbitrary
value}. Consider the universal quantifier. In a logic book, its
introduction rule looks like this:
\[ \infer{\forall x.\,P}{P} \]
Typically, a proviso written in English says that $x$ must not
occur in the assumptions. This proviso guarantees that $x$ can be regarded as
arbitrary, since it has not been assumed to satisfy any special conditions.
Isabelle's underlying formalism, called the
\textbf{meta-logic}, eliminates the need for English. It provides its own universal
quantifier (\isasymAnd) to express the notion of an arbitrary value. We have
already seen another symbol of the meta-logic, namely
\isa\isasymLongrightarrow, which expresses inference rules and the treatment of
assumptions. The only other symbol in the meta-logic is \isa\isasymequiv, which
can be used to define constants.
Returning to the universal quantifier, we find that having a similar quantifier
as part of the meta-logic makes the introduction rule trivial to express:
\begin{isabelle}
({\isasymAnd}x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI}
\end{isabelle}
The following trivial proof demonstrates how the universal introduction
rule works.
\begin{isabelle}
\isacommand{lemma}\ "{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x"\isanewline
\isacommand{apply}\ (rule\ allI)\isanewline
\isacommand{apply}\ (rule\ impI)\isanewline
\isacommand{apply}\ assumption
\end{isabelle}
The first step invokes the rule by applying the method \isa{rule allI}.
\begin{isabelle}
%{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x\isanewline
\ 1.\ {\isasymAnd}x.\ P\ x\ \isasymlongrightarrow\ P\ x
\end{isabelle}
Note that the resulting proof state has a bound variable,
namely~\bigisa{x}. The rule has replaced the universal quantifier of
higher-order logic by Isabelle's meta-level quantifier. Our goal is to
prove
\isa{P\ x\ \isasymlongrightarrow\ P\ x} for arbitrary~\isa{x}; it is
an implication, so we apply the corresponding introduction rule (\isa{impI}).
\begin{isabelle}
\ 1.\ {\isasymAnd}x.\ P\ x\ \isasymLongrightarrow\ P\ x
\end{isabelle}
The {\isa{assumption}} method proves this last subgoal.
\medskip
Now consider universal elimination. In a logic text,
the rule looks like this:
\[ \infer{P[t/x]}{\forall x.\,P} \]
The conclusion is $P$ with $t$ substituted for the variable~$x$.
Isabelle expresses substitution using a function variable:
\begin{isabelle}
{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulename{spec}
\end{isabelle}
This destruction rule takes a
universally quantified formula and removes the quantifier, replacing
the bound variable \bigisa{x} by the schematic variable \bigisa{?x}. Recall that a
schematic variable starts with a question mark and acts as a
placeholder: it can be replaced by any term.
To see how this works, let us derive a rule about reducing
the scope of a universal quantifier. In mathematical notation we write
\[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \]
with the proviso `$x$ not free in~$P$.' Isabelle's treatment of
substitution makes the proviso unnecessary. The conclusion is expressed as
\isa{P\
\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the
variable \isa{P} can introduce a dependence upon~\isa{x}: that would be a
bound variable capture. Here is the isabelle proof in full:
\begin{isabelle}
\isacommand{lemma}\ "({\isasymforall}x.\ P\
\isasymlongrightarrow\ Q\ x)\ \isasymLongrightarrow\ P\
\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x){"}\isanewline
\isacommand{apply}\ (rule\ impI)\isanewline
\isacommand{apply}\ (rule\ allI)\isanewline
\isacommand{apply}\ (drule\ spec)\isanewline
\isacommand{apply}\ (drule\ mp)\isanewline
\ \ \isacommand{apply}\ assumption\isanewline
\ \isacommand{apply}\ assumption
\end{isabelle}
First we apply implies introduction (\isa{rule impI}),
which moves the \isa{P} from the conclusion to the assumptions. Then
we apply universal introduction (\isa{rule allI}).
\begin{isabelle}
%{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x\ \isasymLongrightarrow\ P\
%\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)\isanewline
\ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x
\end{isabelle}
As before, it replaces the HOL
quantifier by a meta-level quantifier, producing a subgoal that
binds the variable~\bigisa{x}. The leading bound variables
(here \isa{x}) and the assumptions (here \isa{{\isasymforall}x.\ P\
\isasymlongrightarrow\ Q\ x} and \isa{P}) form the \textbf{context} for the
conclusion, here \isa{Q\ x}. At each proof step, the subgoals inherit the
previous context, though some context elements may be added or deleted.
Applying \isa{erule} deletes an assumption, while many natural deduction
rules add bound variables or assumptions.
Now, to reason from the universally quantified
assumption, we apply the elimination rule using the {\isa{drule}}
method. This rule is called \isa{spec} because it specializes a universal formula
to a particular term.
\begin{isabelle}
\ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ P\ \isasymlongrightarrow\ Q\ (?x2\
x){\isasymrbrakk}\ \isasymLongrightarrow\ Q\ x
\end{isabelle}
Observe how the context has changed. The quantified formula is gone,
replaced by a new assumption derived from its body. Informally, we have
removed the quantifier. The quantified variable
has been replaced by the curious term
\bigisa{?x2~x}; it acts as a placeholder that may be replaced
by any term that can be built up from~\bigisa{x}. (Formally, \bigisa{?x2} is an
unknown of function type, applied to the argument~\bigisa{x}.) This new assumption is
an implication, so we can use \emph{modus ponens} on it. As before, it requires
proving the antecedent (in this case \isa{P}) and leaves us with the consequent.
\begin{isabelle}
\ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ Q\ (?x2\ x){\isasymrbrakk}\
\isasymLongrightarrow\ Q\ x
\end{isabelle}
The consequent is \isa{Q} applied to that placeholder. It may be replaced by any
term built from~\bigisa{x}, and here
it should simply be~\bigisa{x}. The \isa{assumption} method will do this.
The assumption need not be identical to the conclusion, provided the two formulas are
unifiable.
\medskip
Note that \isa{drule spec} removes the universal quantifier and --- as
usual with elimination rules --- discards the original formula. Sometimes, a
universal formula has to be kept so that it can be used again. Then we use a new
method: \isa{frule}. It acts like \isa{drule} but copies rather than replaces
the selected assumption. The \isa{f} is for `forward.'
In this example, we intuitively see that to go from \isa{P\ a} to \isa{P(f\ (f\
a))} requires two uses of the quantified assumption, one for each
additional~\isa{f}.
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x);
\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P(f\ (f\ a))"\isanewline
\isacommand{apply}\ (frule\ spec)\isanewline
\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
\isacommand{apply}\ (drule\ spec)\isanewline
\isacommand{apply}\ (drule\ mp,\ assumption,\ assumption)\isanewline
\isacommand{done}
\end{isabelle}
%
Applying \isa{frule\ spec} leaves this subgoal:
\begin{isabelle}
\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x);\ P\ a;\ P\ ?x\ \isasymlongrightarrow\ P\ (f\ ?x)\isasymrbrakk\ \isasymLongrightarrow\ P\ (f\ (f\ a))
\end{isabelle}
It is just what \isa{drule} would have left except that the quantified
assumption is still present. The next step is to apply \isa{mp} to the
implication and the assumption \isa{P\ a}, which leaves this subgoal:
\begin{isabelle}
\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x);\ P\ a;\ P\ (f\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (f\ (f\ a))
\end{isabelle}
%
We have created the assumption \isa{P(f\ a)}, which is progress. To finish the
proof, we apply \isa{spec} one last time, using \isa{drule}. One final trick: if
we then apply
\begin{isabelle}
\ \ \ \ \ (drule\ mp,\ assumption)
\end{isabelle}
it will add a second copy of \isa{P(f\ a)} instead of the desired \isa{P(f\
(f\ a))}. Bundling both \isa{assumption} calls with \isa{drule mp} causes
Isabelle to backtrack and find the correct one.
\section{The existential quantifier}
The concepts just presented also apply to the existential quantifier,
whose introduction rule looks like this in Isabelle:
\begin{isabelle}
?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulename{exI}
\end{isabelle}
If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
P(x)$ is also true. It is essentially a dual of the universal elimination rule, and
logic texts present it using the same notation for substitution. The existential
elimination rule looks like this
in a logic text:
\[ \infer{R}{\exists x.\,P & \infer*{R}{[P]}} \]
%
It looks like this in Isabelle:
\begin{isabelle}
\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ {\isasymAnd}x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE}
\end{isabelle}
%
Given an existentially quantified theorem and some
formula $Q$ to prove, it creates a new assumption by removing the quantifier. As with
the universal introduction rule, the textbook version imposes a proviso on the
quantified variable, which Isabelle expresses using its meta-logic. Note that it is
enough to have a universal quantifier in the meta-logic; we do not need an existential
quantifier to be built in as well.\remark{EX example needed?}
Isabelle/HOL also provides Hilbert's
$\epsilon$-operator. The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
true, provided such a value exists. Using this operator, we can express an
existential destruction rule:
\[ \infer{P[(\epsilon x. P) / \, x]}{\exists x.\,P} \]
This rule is seldom used, for it can cause exponential blow-up. The
main use of $\epsilon x. P(x)$ is in definitions when $P(x)$ characterizes $x$
uniquely. For instance, we can define the cardinality of a finite set~$A$ to be that
$n$ such that $A$ is in one-to-one correspondance with $\{1,\ldots,n\}$. We can then
prove that the cardinality of the empty set is zero (since $n=0$ satisfies the
description) and proceed to prove other facts.\remark{SOME theorems
and example}
\begin{exercise}
Prove the lemma
\[ \exists x.\, P\conj Q(x)\Imp P\conj(\exists x.\, Q(x)). \]
\emph{Hint}: the proof is similar
to the one just above for the universal quantifier.
\end{exercise}
\section{Some proofs that fail}
Most of the examples in this tutorial involve proving theorems. But not every
conjecture is true, and it can be instructive to see how
proofs fail. Here we attempt to prove a distributive law involving
the existential quantifier and conjunction.
\begin{isabelle}
\isacommand{lemma}\ "({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x"\isanewline
\isacommand{apply}\ (erule\ conjE)\isanewline
\isacommand{apply}\ (erule\ exE)\isanewline
\isacommand{apply}\ (erule\ exE)\isanewline
\isacommand{apply}\ (rule\ exI)\isanewline
\isacommand{apply}\ (rule\ conjI)\isanewline
\ \isacommand{apply}\ assumption\isanewline
\isacommand{oops}
\end{isabelle}
The first steps are routine. We apply conjunction elimination (\isa{erule
conjE}) to split the assumption in two, leaving two existentially quantified
assumptions. Applying existential elimination (\isa{erule exE}) removes one of
the quantifiers.
\begin{isabelle}
%({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\
%\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x\isanewline
\ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
\end{isabelle}
%
When we remove the other quantifier, we get a different bound
variable in the subgoal. (The name \isa{xa} is generated automatically.)
\begin{isabelle}
\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\
\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
\end{isabelle}
The proviso of the existential elimination rule has forced the variables to
differ: we can hardly expect two arbitrary values to be equal! There is
no way to prove this subgoal. Removing the
conclusion's existential quantifier yields two
identical placeholders, which can become any term involving the variables \bigisa{x}
and~\bigisa{xa}. We need one to become \bigisa{x}
and the other to become~\bigisa{xa}, but Isabelle requires all instances of a
placeholder to be identical.
\begin{isabelle}
\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\
\isasymLongrightarrow\ P\ (?x3\ x\ xa)\isanewline
\ 2.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa)
\end{isabelle}
We can prove either subgoal
using the \isa{assumption} method. If we prove the first one, the placeholder
changes into~\bigisa{x}.
\begin{isabelle}
\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\
\isasymLongrightarrow\ Q\ x
\end{isabelle}
We are left with a subgoal that cannot be proved,
because there is no way to prove that \bigisa{x}
equals~\bigisa{xa}. Applying the \isa{assumption} method results in an
error message:
\begin{isabelle}
*** empty result sequence -- proof command failed
\end{isabelle}
We can tell Isabelle to abandon a failed proof using the \isacommand{oops} command.
\medskip
Here is another abortive proof, illustrating the interaction between
bound variables and unknowns.
If $R$ is a reflexive relation,
is there an $x$ such that $R\,x\,y$ holds for all $y$? Let us see what happens when
we attempt to prove it.
\begin{isabelle}
\isacommand{lemma}\ "{\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\
{\isasymexists}x.\ {\isasymforall}y.\ R\ x\ y"\isanewline
\isacommand{apply}\ (rule\ exI)\isanewline
\isacommand{apply}\ (rule\ allI)\isanewline
\isacommand{apply}\ (drule\ spec)\isanewline
\isacommand{oops}
\end{isabelle}
First,
we remove the existential quantifier. The new proof state has
an unknown, namely~\bigisa{?x}.
\begin{isabelle}
%{\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymexists}x.\
%{\isasymforall}y.\ R\ x\ y\isanewline
\ 1.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymforall}y.\ R\ ?x\ y
\end{isabelle}
Next, we remove the universal quantifier
from the conclusion, putting the bound variable~\isa{y} into the subgoal.
\begin{isabelle}
\ 1.\ {\isasymAnd}y.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ R\ ?x\ y
\end{isabelle}
Finally, we try to apply our reflexivity assumption. We obtain a
new assumption whose identical placeholders may be replaced by
any term involving~\bigisa{y}.
\begin{isabelle}
\ 1.\ {\isasymAnd}y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y
\end{isabelle}
This subgoal can only be proved by putting \bigisa{y} for all the placeholders,
making the assumption and conclusion become \isa{R\ y\ y}.
But Isabelle refuses to substitute \bigisa{y}, a bound variable, for
\bigisa{?x}; that would be a bound variable capture. The proof fails.
Note that Isabelle can replace \bigisa{?z2~y} by \bigisa{y}; this involves
instantiating
\bigisa{?z2} to the identity function.
This example is typical of how Isabelle enforces sound quantifier reasoning.
\section{Proving theorems using the \emph{\texttt{blast}} method}
It is hard to prove substantial theorems using the methods
described above. A proof may be dozens or hundreds of steps long. You
may need to search among different ways of proving certain
subgoals. Often a choice that proves one subgoal renders another
impossible to prove. There are further complications that we have not
discussed, concerning negation and disjunction. Isabelle's
\textbf{classical reasoner} is a family of tools that perform such
proofs automatically. The most important of these is the
{\isa{blast}} method.
In this section, we shall first see how to use the classical
reasoner in its default mode and then how to insert additional
rules, enabling it to work in new problem domains.
We begin with examples from pure predicate logic. The following
example is known as Andrew's challenge. Peter Andrews designed
it to be hard to prove by automatic means.%
\footnote{Pelletier~\cite{pelletier86} describes it and many other
problems for automatic theorem provers.}
The nested biconditionals cause an exponential explosion: the formal
proof is enormous. However, the {\isa{blast}} method proves it in
a fraction of a second.
\begin{isabelle}
\isacommand{lemma}\
"(({\isasymexists}x.\
{\isasymforall}y.\
p(x){=}p(y){)}\
=\
(({\isasymexists}x.\
q(x){)}=({\isasymforall}y.\
p(y){)}){)}\
\ \ =\ \ \ \ \isanewline
\ \ \ \ \ \ \ \
(({\isasymexists}x.\
{\isasymforall}y.\
q(x){=}q(y){)}\
=\
(({\isasymexists}x.\
p(x){)}=({\isasymforall}y.\
q(y){)}){)}"\isanewline
\isacommand{apply}\ blast\isanewline
\isacommand{done}
\end{isabelle}
The next example is a logic problem composed by Lewis Carroll.
The {\isa{blast}} method finds it trivial. Moreover, it turns out
that not all of the assumptions are necessary. We can easily
experiment with variations of this formula and see which ones
can be proved.
\begin{isabelle}
\isacommand{lemma}\
"({\isasymforall}x.\
honest(x)\ \isasymand\
industrious(x)\ \isasymlongrightarrow\
healthy(x){)}\
\isasymand\ \ \isanewline
\ \ \ \ \ \ \ \ \isasymnot\ ({\isasymexists}x.\
grocer(x)\ \isasymand\
healthy(x){)}\
\isasymand\ \isanewline
\ \ \ \ \ \ \ \ ({\isasymforall}x.\
industrious(x)\ \isasymand\
grocer(x)\ \isasymlongrightarrow\
honest(x){)}\
\isasymand\ \isanewline
\ \ \ \ \ \ \ \ ({\isasymforall}x.\
cyclist(x)\ \isasymlongrightarrow\
industrious(x){)}\
\isasymand\ \isanewline
\ \ \ \ \ \ \ \ ({\isasymforall}x.\
{\isasymnot}healthy(x)\ \isasymand\
cyclist(x)\ \isasymlongrightarrow\
{\isasymnot}honest(x){)}\
\ \isanewline
\ \ \ \ \ \ \ \ \isasymlongrightarrow\
({\isasymforall}x.\
grocer(x)\ \isasymlongrightarrow\
{\isasymnot}cyclist(x){)}"\isanewline
\isacommand{apply}\ blast\isanewline
\isacommand{done}
\end{isabelle}
The {\isa{blast}} method is also effective for set theory, which is
described in the next chapter. This formula below may look horrible, but
the \isa{blast} method proves it easily.
\begin{isabelle}
\isacommand{lemma}\ "({\isasymUnion}i{\isasymin}I.\ A(i){)}\ \isasyminter\ ({\isasymUnion}j{\isasymin}J.\ B(j){)}\ =\isanewline
\ \ \ \ \ \ \ \ ({\isasymUnion}i{\isasymin}I.\ {\isasymUnion}j{\isasymin}J.\ A(i)\ \isasyminter\ B(j){)}"\isanewline
\isacommand{apply}\ blast\isanewline
\isacommand{done}
\end{isabelle}
Few subgoals are couched purely in predicate logic and set theory.
We can extend the scope of the classical reasoner by giving it new rules.
Extending it effectively requires understanding the notions of
introduction, elimination and destruction rules. Moreover, there is a
distinction between safe and unsafe rules. A \textbf{safe} rule is one
that can be applied backwards without losing information; an
\textbf{unsafe} rule loses information, perhaps transforming the subgoal
into one that cannot be proved. The safe/unsafe
distinction affects the proof search: if a proof attempt fails, the
classical reasoner backtracks to the most recent unsafe rule application
and makes another choice.
An important special case avoids all these complications. A logical
equivalence, which in higher-order logic is an equality between
formulas, can be given to the classical
reasoner and simplifier by using the attribute {\isa{iff}}. You
should do so if the right hand side of the equivalence is
simpler than the left-hand side.
For example, here is a simple fact about list concatenation.
The result of appending two lists is empty if and only if both
of the lists are themselves empty. Obviously, applying this equivalence
will result in a simpler goal. When stating this lemma, we include
the {\isa{iff}} attribute. Once we have proved the lemma, Isabelle
will make it known to the classical reasoner (and to the simplifier).
\begin{isabelle}
\isacommand{lemma}\
[iff]{:}\
"(xs{\isacharat}ys\ =\
\isacharbrackleft{]})\ =\
(xs=[]\
\isacharampersand\
ys=[]{)}"\isanewline
\isacommand{apply}\ (induct_tac\
xs)\isanewline
\isacommand{apply}\ (simp_all)
\isanewline
\isacommand{done}
\end{isabelle}
%
This fact about multiplication is also appropriate for
the {\isa{iff}} attribute:\remark{the ?s are ugly here but we need
them again when talking about \isa{of}; we need a consistent style}
\begin{isabelle}
(\mbox{?m}\ \isacharasterisk\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
\end{isabelle}
A product is zero if and only if one of the factors is zero. The
reasoning involves a logical \textsc{or}. Proving new rules for
disjunctive reasoning is hard, but translating to an actual disjunction
works: the classical reasoner handles disjunction properly.
In more detail, this is how the {\isa{iff}} attribute works. It converts
the equivalence $P=Q$ to a pair of rules: the introduction
rule $Q\Imp P$ and the destruction rule $P\Imp Q$. It gives both to the
classical reasoner as safe rules, ensuring that all occurrences of $P$ in
a subgoal are replaced by~$Q$. The simplifier performs the same
replacement, since \isa{iff} gives $P=Q$ to the
simplifier. But classical reasoning is different from
simplification. Simplification is deterministic: it applies rewrite rules
repeatedly, as long as possible, in order to \emph{transform} a goal. Classical
reasoning uses search and backtracking in order to \emph{prove} a goal.
\section{Proving the correctness of Euclid's algorithm}
\label{sec:proving-euclid}
A brief development will illustrate advanced use of
\isa{blast}. In \S\ref{sec:recdef-simplification}, we declared the
recursive function {\isa{gcd}}:
\begin{isabelle}
\isacommand{consts}\ gcd\ :{:}\ {"}nat{\isacharasterisk}nat={\isachargreater}nat"\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
\isacommand{recdef}\ gcd\ {"}measure\ ((\isasymlambda(m{,}n){.}n)\ :{:}nat{\isacharasterisk}nat={\isachargreater}nat){"}\isanewline
\ \ \ \ {"}gcd\ (m,\ n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n){)}"%
\end{isabelle}
Let us prove that it computes the greatest common
divisor of its two arguments.
%
%The declaration yields a recursion
%equation for {\isa{gcd}}. Simplifying with this equation can
%cause looping, expanding to ever-larger expressions of if-then-else
%and {\isa{gcd}} calls. To prevent this, we prove separate simplification rules
%for $n=0$\ldots
%\begin{isabelle}
%\isacommand{lemma}\ gcd_0\ [simp]{:}\ {"}gcd(m,0)\ =\ m"\isanewline
%\isacommand{apply}\ (simp)\isanewline
%\isacommand{done}
%\end{isabelle}
%\ldots{} and for $n>0$:
%\begin{isabelle}
%\isacommand{lemma}\ gcd_non_0:\ "0{\isacharless}n\ \isasymLongrightarrow\ gcd(m{,}n)\ =\ gcd\ (n,\ m\ mod\ n){"}\isanewline
%\isacommand{apply}\ (simp)\isanewline
%\isacommand{done}
%\end{isabelle}
%This second rule is similar to the original equation but
%does not loop because it is conditional. It can be applied only
%when the second argument is known to be non-zero.
%Armed with our two new simplification rules, we now delete the
%original {\isa{gcd}} recursion equation.
%\begin{isabelle}
%\isacommand{declare}\ gcd{.}simps\ [simp\ del]
%\end{isabelle}
%
%Now we can prove some interesting facts about the {\isa{gcd}} function,
%for exampe, that it computes a common divisor of its arguments.
%
The theorem is expressed in terms of the familiar
\textbf{divides} relation from number theory:
\begin{isabelle}
?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ \isacharasterisk\ k
\rulename{dvd_def}
\end{isabelle}
%
A simple induction proves the theorem. Here \isa{gcd.induct} refers to the
induction rule returned by \isa{recdef}. The proof relies on the simplification
rules proved in \S\ref{sec:recdef-simplification}, since rewriting by the
definition of \isa{gcd} can cause looping.
\begin{isabelle}
\isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m{,}n)\ dvd\ m)\ \isasymand\ (gcd(m{,}n)\ dvd\ n){"}\isanewline
\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd{.}induct)\isanewline
\isacommand{apply}\ (case_tac\ "n=0"{)}\isanewline
\isacommand{apply}\ (simp_all)\isanewline
\isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline
\isacommand{done}%
\end{isabelle}
Notice that the induction formula
is a conjunction. This is necessary: in the inductive step, each
half of the conjunction establishes the other. The first three proof steps
are applying induction, performing a case analysis on \isa{n},
and simplifying. Let us pass over these quickly and consider
the use of {\isa{blast}}. We have reached the following
subgoal:
\begin{isabelle}
%gcd\ (m,\ n)\ dvd\ m\ \isasymand\ gcd\ (m,\ n)\ dvd\ n\isanewline
\ 1.\ {\isasymAnd}m\ n.\ \isasymlbrakk0\ \isacharless\ n;\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand\ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n){\isasymrbrakk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ gcd\ (n,\ m\ mod\ n)\ dvd\ m
\end{isabelle}
%
One of the assumptions, the induction hypothesis, is a conjunction.
The two divides relationships it asserts are enough to prove
the conclusion, for we have the following theorem at our disposal:
\begin{isabelle}
\isasymlbrakk?k\ dvd\ (?m\ mod\ ?n){;}\ ?k\ dvd\ ?n\isasymrbrakk\ \isasymLongrightarrow\ ?k\ dvd\ ?m%
\rulename{dvd_mod_imp_dvd}
\end{isabelle}
%
This theorem can be applied in various ways. As an introduction rule, it
would cause backward chaining from the conclusion (namely
\isa{?k\ dvd\ ?m}) to the two premises, which
also involve the divides relation. This process does not look promising
and could easily loop. More sensible is to apply the rule in the forward
direction; each step would eliminate the \isa{mod} symboi from an
assumption, so the process must terminate.
So the final proof step applies the \isa{blast} method.
Attaching the {\isa{dest}} attribute to \isa{dvd_mod_imp_dvd} tells \isa{blast}
to use it as destruction rule: in the forward direction.
\medskip
We have proved a conjunction. Now, let us give names to each of the
two halves:
\begin{isabelle}
\isacommand{lemmas}\ gcd_dvd1\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct1]\isanewline
\isacommand{lemmas}\ gcd_dvd2\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct2]%
\end{isabelle}
Several things are happening here. The keyword \isacommand{lemmas}
tells Isabelle to transform a theorem in some way and to
give a name to the resulting theorem. Attributes can be given,
here \isa{iff}, which supplies the new theorems to the classical reasoner
and the simplifier. The directive {\isa{THEN}}, which will be explained
below, supplies the lemma
\isa{gcd_dvd_both} to the
destruction rule \isa{conjunct1} in order to extract the first part.
\begin{isabelle}
\ \ \ \ \ gcd\
(?m1,\
?n1)\ dvd\
?m1%
\end{isabelle}
The variable names \isa{?m1} and \isa{?n1} arise because
Isabelle renames schematic variables to prevent
clashes. The second \isacommand{lemmas} declaration yields
\begin{isabelle}
\ \ \ \ \ gcd\
(?m1,\
?n1)\ dvd\
?n1%
\end{isabelle}
Later, we shall explore this type of forward reasoning in detail.
To complete the verification of the {\isa{gcd}} function, we must
prove that it returns the greatest of all the common divisors
of its arguments. The proof is by induction and simplification.
\begin{isabelle}
\isacommand{lemma}\ gcd_greatest\
[rule_format]{:}\isanewline
\ \ \ \ \ \ \ "(k\ dvd\
m)\ \isasymlongrightarrow\ (k\ dvd\
n)\ \isasymlongrightarrow\ k\ dvd\
gcd(m{,}n)"\isanewline
\isacommand{apply}\ (induct_tac\ m\ n\
rule:\ gcd{.}induct)\isanewline
\isacommand{apply}\ (case_tac\ "n=0"{)}\isanewline
\isacommand{apply}\ (simp_all\ add:\ gcd_non_0\ dvd_mod)\isanewline
\isacommand{done}
\end{isabelle}
%
Note that the theorem has been expressed using HOL implication,
\isa{\isasymlongrightarrow}, because the induction affects the two
preconditions. The directive \isa{rule_format} tells Isabelle to replace
each \isa{\isasymlongrightarrow} by \isa{\isasymLongrightarrow} before
storing the theorem we have proved. This directive also removes outer
universal quantifiers, converting a theorem into the usual format for
inference rules.
The facts proved above can be summarized as a single logical
equivalence. This step gives us a chance to see another application
of \isa{blast}, and it is worth doing for sound logical reasons.
\begin{isabelle}
\isacommand{theorem}\ gcd_greatest_iff\ [iff]{:}\isanewline
\ \ \ \ \ \ \ \ \ "k\ dvd\ gcd(m{,}n)\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\ n)"\isanewline
\isacommand{apply}\ (blast\ intro!{:}\ gcd_greatest\ intro:\ dvd_trans)\isanewline
\isacommand{done}
\end{isabelle}
This theorem concisely expresses the correctness of the {\isa{gcd}}
function.
We state it with the {\isa{iff}} attribute so that
Isabelle can use it to remove some occurrences of {\isa{gcd}}.
The theorem has a one-line
proof using {\isa{blast}} supplied with four introduction
rules: note the {\isa{intro}} attribute. The exclamation mark
({\isa{intro}}{\isa{!}})\ signifies safe rules, which are
applied aggressively. Rules given without the exclamation mark
are applied reluctantly and their uses can be undone if
the search backtracks. Here the unsafe rule expresses transitivity
of the divides relation:
\begin{isabelle}
\isasymlbrakk?m\ dvd\ ?n;\ ?n\ dvd\ ?p\isasymrbrakk\ \isasymLongrightarrow\ ?m\ dvd\ ?p%
\rulename{dvd_trans}
\end{isabelle}
Applying \isa{dvd_trans} as
an introduction rule entails a risk of looping, for it multiplies
occurrences of the divides symbol. However, this proof relies
on transitivity reasoning. The rule {\isa{gcd\_greatest}} is safe to apply
aggressively because it yields simpler subgoals. The proof implicitly
uses \isa{gcd_dvd1} and \isa{gcd_dvd2} as safe rules, because they were
declared using \isa{iff}.
\section{Other classical reasoning methods}
The {\isa{blast}} method is our main workhorse for proving theorems
automatically. Other components of the classical reasoner interact
with the simplifier. Still others perform classical reasoning
to a limited extent, giving the user fine control over the proof.
Of the latter methods, the most useful is {\isa{clarify}}. It performs
all obvious reasoning steps without splitting the goal into multiple
parts. It does not apply rules that could render the
goal unprovable (so-called unsafe rules). By performing the obvious
steps, {\isa{clarify}} lays bare the difficult parts of the problem,
where human intervention is necessary.
For example, the following conjecture is false:
\begin{isabelle}
\isacommand{lemma}\ "({\isasymforall}x.\ P\ x)\ \isasymand\
({\isasymexists}x.\ Q\ x)\ \isasymlongrightarrow\ ({\isasymforall}x.\ P\ x\
\isasymand\ Q\ x)"\isanewline
\isacommand{apply}\ clarify
\end{isabelle}
The {\isa{blast}} method would simply fail, but {\isa{clarify}} presents
a subgoal that helps us see why we cannot continue the proof.
\begin{isabelle}
\ 1.\ {\isasymAnd}x\ xa.\ \isasymlbrakk{\isasymforall}x.\ P\ x;\ Q\
xa\isasymrbrakk\ \isasymLongrightarrow\ P\ x\ \isasymand\ Q\ x
\end{isabelle}
The proof must fail because the assumption \isa{Q\ xa} and conclusion \isa{Q\ x}
refer to distinct bound variables. To reach this state, \isa{clarify} applied
the introduction rules for \isa{\isasymlongrightarrow} and \isa{\isasymforall}
and the elimination rule for ~\isa{\isasymand}. It did not apply the introduction
rule for \isa{\isasymand} because of its policy never to split goals.
Also available is {\isa{clarsimp}}, a method that interleaves {\isa{clarify}}
and {\isa{simp}}. Also there is \isa{safe}, which like \isa{clarify} performs
obvious steps and even applies those that split goals.
The {\isa{force}} method applies the classical reasoner and simplifier
to one goal.
\remark{example needed? most
things done by blast, simp or auto can also be done by force, so why add a new
one?}
Unless it can prove the goal, it fails. Contrast
that with the auto method, which also combines classical reasoning
with simplification. The latter's purpose is to prove all the
easy subgoals and parts of subgoals. Unfortunately, it can produce
large numbers of new subgoals; also, since it proves some subgoals
and splits others, it obscures the structure of the proof tree.
The {\isa{force}} method does not have these drawbacks. Another
difference: {\isa{force}} tries harder than {\isa{auto}} to prove
its goal, so it can take much longer to terminate.
Older components of the classical reasoner have largely been
superseded by {\isa{blast}}, but they still have niche applications.
Most important among these are {\isa{fast}} and {\isa{best}}. While {\isa{blast}}
searches for proofs using a built-in first-order reasoner, these
earlier methods search for proofs using standard Isabelle inference.
That makes them slower but enables them to work correctly in the
presence of the more unusual features of Isabelle rules, such
as type classes and function unknowns. For example, the introduction rule
for Hilbert's epsilon-operator has the following form:
\begin{isabelle}
?P\ ?x\ \isasymLongrightarrow\ ?P\ (Eps\ ?P)
\rulename{someI}
\end{isabelle}
The repeated occurrence of the variable \isa{?P} makes this rule tricky
to apply. Consider this contrived example:
\begin{isabelle}
\isacommand{lemma}\ "{\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\isanewline
\ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ P\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)\
\isasymand\ Q\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)"\isanewline
\isacommand{apply}\ (rule\ someI)
\end{isabelle}
%
We can apply rule \isa{someI} explicitly. It yields the
following subgoal:
\begin{isabelle}
\ 1.\ {\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P\ ?x\
\isasymand\ Q\ ?x%
\end{isabelle}
The proof from this point is trivial. The question now arises, could we have
proved the theorem with a single command? Not using {\isa{blast}} method: it
cannot perform the higher-order unification that is necessary here. The
{\isa{fast}} method succeeds:
\begin{isabelle}
\isacommand{apply}\ (fast\ intro!:\ someI)
\end{isabelle}
The {\isa{best}} method is similar to {\isa{fast}} but it uses a
best-first search instead of depth-first search. Accordingly,
it is slower but is less susceptible to divergence. Transitivity
rules usually cause {\isa{fast}} to loop where often {\isa{best}}
can manage.
Here is a summary of the classical reasoning methods:
\begin{itemize}
\item \isa{blast} works automatically and is the fastest
\item \isa{clarify} and \isa{clarsimp} perform obvious steps without splitting the
goal; \isa{safe} even splits goals
\item \isa{force} uses classical reasoning and simplification to prove a goal;
\isa{auto} is similar but leaves what it cannot prove
\item \isa{fast} and \isa{best} are legacy methods that work well with rules involving
unusual features
\end{itemize}
A table illustrates the relationships among four of these methods.
\begin{center}
\begin{tabular}{r|l|l|}
& no split & split \\ \hline
no simp & \isa{clarify} & \isa{safe} \\ \hline
simp & \isa{clarsimp} & \isa{auto} \\ \hline
\end{tabular}
\end{center}
\section{Forward proof}\label{sec:forward}
Forward proof means deriving new facts from old ones. It is the
most fundamental type of proof. Backward proof, by working from goals to
subgoals, can help us find a difficult proof. But it is
not always the best way of presenting the proof so found. Forward
proof is particuarly good for reasoning from the general
to the specific. For example, consider the following distributive law for
the
\isa{gcd} function:
\[ k\times\gcd(m,n) = \gcd(k\times m,k\times n)\]
Putting $m=1$ we get (since $\gcd(1,n)=1$ and $k\times1=k$)
\[ k = \gcd(k,k\times n)\]
We have derived a new fact about \isa{gcd}; if re-oriented, it might be
useful for simplification. After re-orienting it and putting $n=1$, we
derive another useful law:
\[ \gcd(k,k)=k \]
Substituting values for variables --- instantiation --- is a forward step.
Re-orientation works by applying the symmetry of equality to
an equation, so it too is a forward step.
Now let us reproduce our examples in Isabelle. Here is the distributive
law:
\begin{isabelle}%
?k\ \isacharasterisk\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ \isacharasterisk\ ?m,\ ?k\ \isacharasterisk\ ?n)
\rulename{gcd_mult_distrib2}
\end{isabelle}%
The first step is to replace \isa{?m} by~1 in this law. We refer to the
variables not by name but by their position in the theorem, from left to
right. In this case, the variables are \isa{?k}, \isa{?m} and~\isa{?n}.
So, the expression
\hbox{\texttt{[of k 1]}} replaces \isa{?k} by~\isa{k} and \isa{?m}
by~\isa{1}.
\begin{isabelle}
\isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1]
\end{isabelle}
%
The command
\isa{thm gcd_mult_0}
displays the resulting theorem:
\begin{isabelle}
\ \ \ \ \ k\ \isacharasterisk\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ \isacharasterisk\ 1,\ k\ \isacharasterisk\ ?n)
\end{isabelle}
Something is odd: {\isa{k}} is an ordinary variable, while {\isa{?n}}
is schematic. We did not specify an instantiation
for {\isa{?n}}. In its present form, the theorem does not allow
substitution for {\isa{k}}. One solution is to avoid giving an instantiation for
\isa{?k}: instead of a term we can put an underscore~(\isa{_}). For example,
\begin{isabelle}
\ \ \ \ \ gcd_mult_distrib2\ [of\ _\ 1]
\end{isabelle}
replaces \isa{?m} by~\isa{1} but leaves \isa{?k} unchanged. Anyway, let us put
the theorem \isa{gcd_mult_0} into a simplified form:
\begin{isabelle}
\isacommand{lemmas}\
gcd_mult_1\ =\ gcd_mult_0\
[simplified]%
\end{isabelle}
%
Again, we display the resulting theorem:
\begin{isabelle}
\ \ \ \ \ k\ =\ gcd\ (k,\ k\ \isacharasterisk\ ?n)
\end{isabelle}
%
To re-orient the equation requires the symmetry rule:
\begin{isabelle}
?s\ =\ ?t\
\isasymLongrightarrow\ ?t\ =\
?s%
\rulename{sym}
\end{isabelle}
The following declaration gives our equation to \isa{sym}:
\begin{isabelle}
\ \ \ \isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_1\
[THEN\ sym]
\end{isabelle}
%
Here is the result:
\begin{isabelle}
\ \ \ \ \ gcd\ (k,\ k\ \isacharasterisk\
?n)\ =\ k%
\end{isabelle}
\isa{THEN~sym} gives the current theorem to the rule \isa{sym} and returns the
resulting conclusion.\remark{figure necessary?} The effect is to exchange the
two operands of the equality. Typically {\isa{THEN}} is used with destruction
rules. Above we have used
\isa{THEN~conjunct1} to extract the first part of the theorem
\isa{gcd_dvd_both}. Also useful is \isa{THEN~spec}, which removes the quantifier
from a theorem of the form $\forall x.\,P$, and \isa{THEN~mp}, which converts the
implication $P\imp Q$ into the rule $\vcenter{\infer{Q}{P}}$.
Similar to \isa{mp} are the following two rules, which extract
the two directions of reasoning about a boolean equivalence:
\begin{isabelle}
\isasymlbrakk?Q\ =\
?P;\ ?Q\isasymrbrakk\
\isasymLongrightarrow\ ?P%
\rulename{iffD1}%
\isanewline
\isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\
\isasymLongrightarrow\ ?P%
\rulename{iffD2}
\end{isabelle}
%
Normally we would never name the intermediate theorems
such as \isa{gcd_mult_0} and
\isa{gcd_mult_1} but would combine
the three forward steps:
\begin{isabelle}
\isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]%
\end{isabelle}
The directives, or attributes, are processed from left to right. This
declaration of \isa{gcd_mult} is equivalent to the
previous one.
Such declarations can make the proof script hard to read:
what is being proved? More legible
is to state the new lemma explicitly and to prove it using a single
\isa{rule} method whose operand is expressed using forward reasoning:
\begin{isabelle}
\isacommand{lemma}\ gcd_mult\
[simp]{:}\
"gcd(k,\
k{\isacharasterisk}n)\ =\
k"\isanewline
\isacommand{apply}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]{)}\isanewline
\isacommand{done}
\end{isabelle}
Compared with the previous proof of \isa{gcd_mult}, this
version shows the reader what has been proved. Also, it receives
the usual Isabelle treatment. In particular, Isabelle generalizes over all
variables: the resulting theorem will have {\isa{?k}} instead of {\isa{k}}.
At the start of this section, we also saw a proof of $\gcd(k,k)=k$. Here
is the Isabelle version:
\begin{isabelle}
\isacommand{lemma}\ gcd_self\
[simp]{:}\
"gcd(k{,}k)\
=\ k"\isanewline
\isacommand{apply}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified]{)}\isanewline
\isacommand{done}
\end{isabelle}
Recall that \isa{of} generates an instance of a rule by specifying
values for its variables. Analogous is \isa{OF}, which generates an
instance of a rule by specifying facts for its premises. Let us try
it with this rule:
\begin{isabelle}
{\isasymlbrakk}gcd(?k,?n){=}1;\ ?k\ dvd\ (?m * ?n){\isasymrbrakk}\
\isasymLongrightarrow\ ?k\ dvd\ ?m
\rulename{relprime_dvd_mult}
\end{isabelle}
First, we
prove an instance of its first premise:
\begin{isabelle}
\isacommand{lemma}\ relprime_20_81:\ "gcd(\#20,\#81)\ =\ 1"\isanewline
\isacommand{apply}\ (simp\ add:\ gcd{.}simps)\isanewline
\isacommand{done}%
\end{isabelle}
We have evaluated an application of the \isa{gcd} function by
simplification. Expression evaluation is not guaranteed to terminate, and
certainly is not efficient; Isabelle performs arithmetic operations by
rewriting symbolic bit strings. Here, however, the simplification takes
less than one second. We can specify this new lemma to {\isa{OF}},
generating an instance of \isa{relprime_dvd_mult}. The expression
\begin{isabelle}
\ \ \ \ \ relprime_dvd_mult [OF relprime_20_81]
\end{isabelle}
yields the theorem
\begin{isabelle}
\ \ \ \ \ \isacharhash20\ dvd\ (?m\ \isacharasterisk\ \isacharhash81)\ \isasymLongrightarrow\ \isacharhash20\ dvd\ ?m%
\end{isabelle}
%
{\isa{OF}} takes any number of operands. Consider
the following facts about the divides relation:
\begin{isabelle}
\isasymlbrakk?k\ dvd\ ?m;\
?k\ dvd\ ?n\isasymrbrakk\
\isasymLongrightarrow\ ?k\ dvd\
(?m\ \isacharplus\
?n)
\rulename{dvd_add}\isanewline
?m\ dvd\ ?m%
\rulename{dvd_refl}
\end{isabelle}
Let us supply \isa{dvd_refl} for each of the premises of \isa{dvd_add}:
\begin{isabelle}
\ \ \ \ \ dvd_add [OF dvd_refl dvd_refl]
\end{isabelle}
Here is the theorem that we have expressed:
\begin{isabelle}
\ \ \ \ \ ?k\ dvd\ (?k\ \isacharplus\ ?k)
\end{isabelle}
As with \isa{of}, we can use the \isa{_} symbol to leave some positions
unspecified:
\begin{isabelle}
\ \ \ \ \ dvd_add [OF _ dvd_refl]
\end{isabelle}
The result is
\begin{isabelle}
\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ \isacharplus\ ?k)
\end{isabelle}
You may have noticed that {\isa{THEN}} and {\isa{OF}} are based on
the same idea, namely to combine two rules. They differ in the
order of the combination and thus in their effect. We use \isa{THEN}
typically with a destruction rule to extract a subformula of the current
theorem. We use \isa{OF} with a list of facts to generate an instance of
the current theorem.
Here is a summary of the primitives for forward reasoning:
\begin{itemize}
\item {\isa{of}} instantiates the variables of a rule to a list of terms
\item {\isa{OF}} applies a rule to a list of theorems
\item {\isa{THEN}} gives a theorem to a named rule and returns the
conclusion
\end{itemize}
\section{Methods for forward proof}
We have seen that forward proof works well within a backward
proof. Also in that spirit is the \isa{insert} method, which inserts a
given theorem as a new assumption of the current subgoal. This already
is a forward step; moreover, we may (as always when using a theorem) apply
{\isa{of}}, {\isa{THEN}} and other directives. The new assumption can then
be used to help prove the subgoal.
For example, consider this theorem about the divides relation.
Only the first proof step is given; it inserts the distributive law for
\isa{gcd}. We specify its variables as shown.
\begin{isabelle}
\isacommand{lemma}\
relprime_dvd_mult:\isanewline
\ \ \ \ \ \ \ "{\isasymlbrakk}\ gcd(k,n){=}1;\
k\ dvd\ (m*n)\
{\isasymrbrakk}\
\isasymLongrightarrow\ k\ dvd\
m"\isanewline
\isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\
n])
\end{isabelle}
In the resulting subgoal, note how the equation has been
inserted:
\begin{isabelle}
{\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\
dvd\ (m\ \isacharasterisk\
n){\isasymrbrakk}\ \isasymLongrightarrow\ k\ dvd\
m\isanewline
\ 1.\ {\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ \isacharasterisk\ n){;}\isanewline
\ \ \ \ \ m\ \isacharasterisk\ gcd\
(k,\ n)\
=\ gcd\ (m\ \isacharasterisk\
k,\ m\ \isacharasterisk\
n){\isasymrbrakk}\isanewline
\ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
\end{isabelle}
The next proof step, \isa{\isacommand{apply}(simp)},
utilizes the assumption \isa{gcd(k,n)\ =\
1}. Here is the result:
\begin{isabelle}
{\isasymlbrakk}gcd\ (k,\
n)\ =\ 1;\ k\
dvd\ (m\ \isacharasterisk\
n){\isasymrbrakk}\ \isasymLongrightarrow\ k\ dvd\
m\isanewline
\ 1.\ {\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ \isacharasterisk\ n){;}\isanewline
\ \ \ \ \ m\ =\ gcd\ (m\
\isacharasterisk\ k,\ m\ \isacharasterisk\
n){\isasymrbrakk}\isanewline
\ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
\end{isabelle}
Simplification has yielded an equation for \isa{m} that will be used to
complete the proof.
\medskip
Here is another proof using \isa{insert}. \remark{Effect with unknowns?}
Division and remainder obey a well-known law:
\begin{isabelle}
(?m\ div\ ?n)\ \isacharasterisk\
?n\ \isacharplus\ ?m\ mod\ ?n\
=\ ?m
\rulename{mod_div_equality}
\end{isabelle}
We refer to this law explicitly in the following proof:
\begin{isabelle}
\isacommand{lemma}\ div_mult_self_is_m:\ \isanewline
\ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m{\isacharasterisk}n)\ div\ n\ =\ (m:{:}nat)"\isanewline
\isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m{\isacharasterisk}n"\ n]{)}\isanewline
\isacommand{apply}\ (simp)\isanewline
\isacommand{done}
\end{isabelle}
The first step inserts the law, specifying \isa{m*n} and
\isa{n} for its variables. Notice that nontrivial expressions must be
enclosed in quotation marks. Here is the resulting
subgoal, with its new assumption:
\begin{isabelle}
%0\ \isacharless\ n\ \isasymLongrightarrow\ (m\
%\isacharasterisk\ n)\ div\ n\ =\ m\isanewline
\ 1.\ \isasymlbrakk0\ \isacharless\
n;\ \ (m\ \isacharasterisk\ n)\ div\ n\
\isacharasterisk\ n\ \isacharplus\ (m\ \isacharasterisk\ n)\ mod\ n\
=\ m\ \isacharasterisk\ n\isasymrbrakk\isanewline
\ \ \ \ \isasymLongrightarrow\ (m\ \isacharasterisk\ n)\ div\ n\
=\ m
\end{isabelle}
Simplification reduces \isa{(m\ \isacharasterisk\ n)\ mod\ n} to zero.
Then it cancels the factor~\isa{n} on both
sides of the equation, proving the theorem.
\medskip
A similar method is {\isa{subgoal\_tac}}. Instead of inserting
a theorem as an assumption, it inserts an arbitrary formula.
This formula must be proved later as a separate subgoal. The
idea is to claim that the formula holds on the basis of the current
assumptions, to use this claim to complete the proof, and finally
to justify the claim. It is a valuable means of giving the proof
some structure. The explicit formula will be more readable than
proof commands that yield that formula indirectly.
Look at the following example.
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk(z::int)\ <\ \#37;\ \#66\ <\ \#2*z;\ z*z\
\isasymnoteq\ \#1225;\ Q(\#34);\ Q(\#36)\isasymrbrakk\isanewline
\ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ Q(z)"\isanewline
\isacommand{apply}\ (subgoal_tac\ "z\ =\ \#34\ \isasymor\ z\ =\
\#36")\isanewline
\isacommand{apply}\ blast\isanewline
\isacommand{apply}\ (subgoal_tac\ "z\ \isasymnoteq\ \#35")\isanewline
\isacommand{apply}\ arith\isanewline
\isacommand{apply}\ force\isanewline
\isacommand{done}
\end{isabelle}
Let us prove it informally. The first assumption tells us
that \isa{z} is no greater than 36. The second tells us that \isa{z}
is at least 34. The third assumption tells us that \isa{z} cannot be 35, since
$35\times35=1225$. So \isa{z} is either 34 or 36, and since \isa{Q} holds for
both of those values, we have the conclusion.
The Isabelle proof closely follows this reasoning. The first
step is to claim that \isa{z} is either 34 or 36. The resulting proof
state gives us two subgoals:
\begin{isabelle}
%{\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\
%Q\ \#34;\ Q\ \#36\isasymrbrakk\ \isasymLongrightarrow\ Q\ z\isanewline
\ 1.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
\ \ \ \ \ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isasymrbrakk\isanewline
\ \ \ \ \isasymLongrightarrow\ Q\ z\isanewline
\ 2.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
\ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36
\end{isabelle}
The first subgoal is trivial, but for the second Isabelle needs help to eliminate
the case
\isa{z}=35. The second invocation of {\isa{subgoal\_tac}} leaves two
subgoals:
\begin{isabelle}
\ 1.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\
\#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
\ \ \ \ \ z\ \isasymnoteq\ \#35\isasymrbrakk\isanewline
\ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isanewline
\ 2.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
\ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35
\end{isabelle}
Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic:
the method {\isa{arith}}. For the second subgoal we apply the method {\isa{force}},
which proceeds by assuming that \isa{z}=35 and arriving at a contradiction.
\medskip
Summary of these methods:
\begin{itemize}
\item {\isa{insert}} adds a theorem as a new assumption
\item {\isa{subgoal_tac}} adds a formula as a new assumption and leaves the
subgoal of proving that formula
\end{itemize}