doc-src/TutorialI/Rules/rules.tex

various changes including the SOME examples, rule_format and "by"

% $Id$
\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 programming.%
\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 
[for $\disj$ and $\exists$] 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.  

\medskip
\indexbold{by}
The \isacommand{by} command is useful for proofs like these that use
\isa{assumption} heavily.  It executes an
\isacommand{apply} command, then tries to prove all remaining subgoals using
\isa{assumption}.  Since (if successful) it ends the proof, it also replaces the 
\isacommand{done} symbol.  For example, the proof above can be shortened:
\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{by}\ (drule\ mp)
\end{isabelle}
We could use \isacommand{by} to replace the final \isacommand{apply} and
\isacommand{done} in any proof, but typically we use it
to eliminate calls to \isa{assumption}.  It is also a nice way of expressing a
one-line proof.


\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 if 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$.  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{by}\ (erule\ ssubst)
\end{isabelle}
%
The simplifier might loop, replacing \isa{x} by \isa{f x} and then by
\isa{f(f x)} and so forth. (Here \isa{simp} 
can see the danger and would re-orient the 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, so the \isacommand{by} command
proves it implicitly. 

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}

\noindent
The \isacommand{by} command works too, since it backtracks when
proving subgoals by assumption:
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\
\isasymrbrakk\
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
\isacommand{by}\ (erule\ ssubst)
\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{by}\ (erule_tac\ P="\isasymlambda u.\ P\ u\ u\ x"\ 
\isakeyword{in}\ ssubst)
\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.  With this instantiation, backtracking is neither necessary
nor possible.

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{by}\ (erule\ notE)
\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,
\isa{notE} will select the first negated assumption, which is useless.  
Instead, we invoke the rule using the
\isa{by} command.
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\isanewline
\isacommand{apply}\ (elim\ conjE\ disjE)\isanewline
\ \isacommand{apply}\ assumption
\isanewline
\isacommand{by}\ (erule\ contrapos_np,\ rule\ conjI)
\end{isabelle}
%
The first proof step applies the {\isa{intro}} method, which repeatedly  uses
built-in introduction rules.  Here it creates the negative assumption 
\hbox{\isa{\isasymnot(Q\ \isasymand\ R)}}.  That comes from \isa{disjCI},  a
disjunction introduction rule that combines the effects of 
\isa{disjI1} and \isa{disjI2}.
\begin{isabelle}
\ 1.\ \isasymlbrakk(P\ \isasymor\ Q)\ \isasymand\ R;\ \isasymnot\ (Q\ \isasymand\
R)\isasymrbrakk\ \isasymLongrightarrow\ P%
\end{isabelle}
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 applying
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}
They are proved by assumption, which is implicit in the \isacommand{by} command.


\section{Quantifiers}

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.

\subsection{The Universal Introduction Rule}

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{by}\ (rule\ impI)
\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}
This last subgoal is implicitly proved by assumption. 

\subsection{The Universal Elimination Rule}

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,\ rule\ allI)\isanewline
\isacommand{apply}\ (drule\ spec)\isanewline
\isacommand{by}\ (drule\ mp)
\end{isabelle}
First we apply implies introduction (\isa{impI}), 
which moves the \isa{P} from the conclusion to the assumptions. Then 
we apply universal introduction (\isa{allI}).  
\begin{isabelle}
\ 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 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, implicit in the
\isacommand{by} command, proves this subgoal.  The assumption need not
be identical to the conclusion, provided the two formulas are unifiable.  


\subsection{Re-using an Assumption: the {\tt\slshape frule} Method}

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 \emph{forward}.

In this example, going from \isa{P\ a} to \isa{P(h(h~a))}
requires two uses of the quantified assumption, one for each~\isa{h} being
affixed to the term~\isa{a}.
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);
\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P(h\ (h\ a))"\isanewline
\isacommand{apply}\ (frule\ spec)\isanewline
\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
\isacommand{apply}\ (drule\ spec)\isanewline
\isacommand{by}\ (drule\ mp)
\end{isabelle}
%
Applying \isa{frule\ spec} leaves this subgoal:
\begin{isabelle}
\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);\ P\ a;\ P\ ?x\ \isasymlongrightarrow\ P\ (h\ ?x)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ 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\ (h\ x);\ P\ a;\ P\ (h\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a))
\end{isabelle}
%
We have created the assumption \isa{P(h\ a)}, which is progress.  To finish the
proof, we apply \isa{spec} one last time, using \isa{drule}.
One final remark: applying \isa{spec} by the command
\begin{isabelle}
\isacommand{apply}\ (drule\ mp,\ assumption)
\end{isabelle}
does not work the second time.  It adds a second copy of \isa{P(h\ a)} instead of
the desired assumption, \isa{P(h(h\ a))}.  We have used the \isacommand{by}
command, which causes Isabelle to backtrack until it finds the correct one.
Equivalently, we could have used the \isacommand{apply} command and bundled the
\isa{drule mp} with two \isa{assumption} calls.


\subsection{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 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.
 

\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{Hilbert's $\epsilon$-Operator}

Isabelle/HOL 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.  

\subsection{Definite Descriptions}

In ASCII, we write \isa{SOME} for $\epsilon$.
\REMARK{the internal constant is \isa{Eps}}
The main use of \hbox{\isa{SOME\ x.\ P\ x}} is as a \textbf{definite
description}: when \isa{P} is satisfied by a unique value,~\isa{a}. 
We reason using this rule:
\begin{isabelle}
\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \ 
\isasymLongrightarrow \ (SOME\ x.\ P\ x)\ =\ a%
\rulename{some_equality}
\end{isabelle}
For instance, we can define the
cardinality of a finite set~$A$ to be that
$n$ such that $A$ is in one-to-one correspondence 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.

Here is an example.  HOL defines \isa{inv},\indexbold{*inv (constant)}
which expresses inverses of functions, as a definite
description:
\begin{isabelle}
inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%
\rulename{inv_def}
\end{isabelle}
The inverse of \isa{f}, when applied to \isa{y}, returns some {x} such that
\isa{f~x~=~y}.  For example, we can prove \isa{inv~Suc} really is the inverse
of the \isa{Suc} function 
\begin{isabelle}
\isacommand{lemma}\ "inv\ Suc\ (Suc\ x)\ =\ x"\isanewline
\isacommand{by}\ (simp\ add:\ inv_def)
\end{isabelle}

\noindent
The proof is a one-liner: the subgoal simplifies to a degenerate application of
\isa{SOME}, which is then erased.  The definition says nothing about what
\isa{inv~Suc} returns when applied to zero.


A more challenging example illustrates how Isabelle/HOL defines the least-number
operator, which denotes the least \isa{x} satisfying~\isa{P}:
\begin{isabelle}
(LEAST\ x.\ P\ x)\ \isasymequiv \ SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)
\rulename{Least_def}
\end{isabelle}

Let us prove the counterpart of \isa{some_equality} for this operator.
The first step merely unfolds the definition:
\begin{isabelle}
\isacommand{theorem}\ Least_equality:\isanewline
\ \ \ \ \ "\isasymlbrakk \ P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\ \isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline
\isacommand{apply}\ (simp\ add:\ Least_def)\isanewline
%\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\
%\isasymle \ x\isasymrbrakk \isanewline
%\ \ \ \ \isasymLongrightarrow \ (SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))\ =\ k%
\isacommand{apply}\ (rule\ some_equality)\isanewline
\isanewline
\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\
\isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ P\ k\ \isasymand \
(\isasymforall y.\ P\ y\ \isasymlongrightarrow \ k\ \isasymle \ y)\isanewline
\ 2.\ \isasymAnd x.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x;\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)\isasymrbrakk \isanewline
\ \ \ \ \ \ \ \ \isasymLongrightarrow \ x\ =\ k%
\end{isabelle}

As always with \isa{some_equality}, we must show existence and
uniqueness of the claimed solution,~\isa{k}.  Existence, the first
subgoal, is trivial.  Uniqueness, the second subgoal, follows by antisymmetry:
\begin{isabelle}
\isasymlbrakk x\ \isasymle \ y;\ y\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ x\ =\ y%
\rulename{order_antisym}
\end{isabelle}
The assumptions imply both \isa{k~\isasymle~x} and \isa{x~\isasymle~k}.  One call
to \isa{auto} does it all:
\begin{isabelle}
\isacommand{by}\ (auto\ intro:\ order_antisym)
\end{isabelle}


\subsection{Indefinite Descriptions}

Occasionally, \hbox{\isa{SOME\ x.\ P\ x}} serves as an \textbf{indefinite
description}, when it makes an arbitrary selection from the values
satisfying~\isa{P}\@.  
\begin{isabelle}
P\ x\ \isasymLongrightarrow \ P\ (SOME\ x.\ P\ x)
\rulename{someI}\isanewline
\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ Q\
x\isasymrbrakk \ \isasymLongrightarrow \ Q\ (SOME\ x.\ P\ x)
\rulename{someI2}
\end{isabelle}
Rule \isa{someI} is basic (if anything satisfies \isa{P} then so does
\hbox{\isa{SOME\ x.\ P\ x}}).  Rule \isa{someI2} is easier to apply in a backward
proof.

\medskip
For example, let us prove the Axiom of Choice:
\begin{isabelle}
\isacommand{theorem}\ axiom_of_choice:
\ "(\isasymforall x.\ \isasymexists \ y.\ P\ x\ y)\ \isasymLongrightarrow \
\isasymexists f.\ \isasymforall x.\ P\ x\ (f\ x)"\isanewline
\isacommand{apply}\ (rule\ exI,\ rule\ allI)\isanewline
\ 1.\ \isasymAnd x.\ \isasymforall x.\ \isasymexists y.\ P\ x\ y\
\isasymLongrightarrow \ P\ x\ (?f\ x)
\end{isabelle}
%
We have applied the introduction rules; now it is time to apply the elimination
rules.

\begin{isabelle}
\isacommand{apply}\ (drule\ spec,\ erule\ exE)\isanewline
\ 1.\ \isasymAnd x\ y.\ P\ (?x2\ x)\ y\ \isasymLongrightarrow \ P\ x\ (?f\ x)
\end{isabelle}

\noindent
The rule \isa{someI} automatically instantiates
\isa{f} to \hbox{\isa{\isasymlambda x.\ SOME y.\ P\ x\ y}}, which is the choice
function.  It also instantiates \isa{?x2\ x} to \isa{x}.
\begin{isabelle}
\isacommand{by}\ (rule\ someI)\isanewline
\end{isabelle}


\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 \isa{x}
and~\isa{xa}.  We need one to become \isa{x}
and the other to become~\isa{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~\isa{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.  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~\isa{?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~\isa{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 \isa{y} for all the placeholders,
making the assumption and conclusion become \isa{R\ y\ y}. 
But Isabelle refuses to substitute \isa{y}, a bound variable, for
\isa{?x}; that would be a bound variable capture.  The proof fails.
Note that Isabelle can replace \isa{?z2~y} by \isa{y}; this involves
instantiating
\isa{?z2} to the identity function.

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


\section{Proving Theorems Using the {\tt\slshape 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{by}\ blast
\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{by}\ blast
\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{by}\ blast
\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}\ *\ \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 the advanced use of  
\isa{blast}.  In \S\ref{sec:recdef-simplification}, we declared the
recursive function \isa{gcd}:
\begin{isabelle}
\isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline
\isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n)\
::nat*nat\ \isasymRightarrow\ 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\ *\ 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}