doc-src/TutorialI/Rules/rules.tex

fixed the pr example

% $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.  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 seen 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, searching for an assumption 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 because they take apart and destroy
a premise.%
\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 schematic 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 rule 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 
\isasymAnd-bound variables 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 (\isa{\isacommand{apply} assumption}),
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}
\ 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{Renaming an Assumption: {\tt\slshape rename_tac}}

When you apply a rule such as \isa{allI}, the quantified variable becomes a new
bound variable of the new subgoal.  Isabelle tries to avoid changing its name, but
sometimes it has to choose a new name in order to avoid a clash.  Here is a
contrived example:
\begin{isabelle}
\isacommand{lemma}\ "x\ <\ y\ \isasymLongrightarrow \ \isasymforall x\ y.\ P\ x\
(f\ y)"\isanewline
\isacommand{apply}\ intro\isanewline
\ 1.\ \isasymAnd xa\ ya.\ x\ <\ y\ \isasymLongrightarrow \ P\ xa\ (f\ ya)
\end{isabelle}
%
The names \isa{x} and \isa{y} were already in use, so the new bound variables are
called \isa{xa} and~\isa{ya}.  You can rename them by invoking \isa{rename_tac}:

\begin{isabelle}
\isacommand{apply}\ (rename_tac\ v\ w)\isanewline
\ 1.\ \isasymAnd v\ w.\ x\ <\ y\ \isasymLongrightarrow \ P\ v\ (f\ w)
\end{isabelle}
Recall that \isa{rule_tac}\index{*rule_tac!and renaming} instantiates a
theorem with specified terms.  These terms may involve the goal's bound
variables, but beware of referring to  variables
like~\isa{xa}.  A future change to your theories could change the set of names
produced at top level, so that \isa{xa} changes to~\isa{xb} or reverts to~\isa{x}.
It is safer to rename automatically-generated variables before mentioning them.

If the subgoal has more bound variables than there are names given to
\isa{rename_tac}, the rightmost ones are renamed.


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

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}.

\medskip
\emph{A final remark}.  Applying \isa{spec} by the command
\begin{isabelle}
\isacommand{apply}\ (drule\ mp,\ assumption)
\end{isabelle}
would not work a second time: it would add a second copy of \isa{P(h~a)} instead
of the desired assumption, \isa{P(h(h~a))}.  The \isacommand{by}
command forces Isabelle to backtrack until it finds the correct one.
Alternatively, we could have used the \isacommand{apply} command and bundled the
\isa{drule mp} with \emph{two} calls of \isa{assumption}.


\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{Q}{\exists x.\,P & \infer*{Q}{[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}
\label{sec:SOME}

HOL provides Hilbert's
$\varepsilon$-operator.  The term $\varepsilon 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[(\varepsilon x. P) / \, x]}{\exists x.\,P} \]
This rule is seldom used, for it can cause exponential blow-up.  

\subsection{Definite Descriptions}

In \textsc{ascii}, we write \isa{SOME} for $\varepsilon$.
\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 another example.  Isabelle/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}
If we interact with Isabelle via the shell interface,
we abandon a failed proof with 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\ =\ [])\ =\
(xs=[]\ \isasymand\ 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 disjunction.  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}.  We shall also see \isa{case_tac} used to perform a Boolean
case split.

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 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}
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 --- we shall discuss
\isa{case_tac} below --- 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 an occurrence of the \isa{mod} symbol, 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}, described in
\S\ref{sec:forward} below, supplies the lemma 
\isa{gcd_dvd_both} to the
destruction rule \isa{conjunct1}.  The effect is 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}

\medskip
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, case analysis 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}

The case analysis is performed by \isa{case_tac~"n=0"}: the operand has type
\isa{bool}.  Until now, we have used \isa{case_tac} only with datatypes, and since
\isa{nat} is a datatype, we could have written
\isa{case_tac~"n"} with a similar effect.  However, the definition of \isa{gcd}
makes a Boolean decision:
\begin{isabelle}
\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))"
\end{isabelle}
Proofs about a function frequently follow the function's definition, so we perform
case analysis over the same formula.

\begingroup\samepage
\begin{isabelle}
\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
\ \ \ \ \ \ \ \ \ \ \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ n\ =\ 0\isasymrbrakk \isanewline
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n)
\pagebreak[0]\isanewline
\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
\ \ \ \ \ \ \ \ \ \ \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ n\ \isasymnoteq \ 0\isasymrbrakk \isanewline
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n)
\end{isabelle}
\endgroup

\begin{warn}
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 can also remove outer
universal quantifiers, converting a theorem into the usual format for
inference rules.  (See \S\ref{sec:forward}.)
\end{warn}

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{by}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans)
\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 two additional introduction 
rules. 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 unsafe rules that could render the 
goal unprovable. 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 of \isa{force}?}
Unless it can prove the goal, it fails. Contrast 
that with the \isa{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, recall the introduction rule
for Hilbert's $\varepsilon$-operator: 
\begin{isabelle}
?P\ ?x\ \isasymLongrightarrow\ ?P\ (SOME\ x.\ ?P x)
\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.  Could we have
proved the theorem with a single command? Not using \isa{blast}: it
cannot perform  the higher-order unification needed 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{Directives for 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 particularly 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.  

\subsection{The {\tt\slshape of} and {\tt\slshape THEN} Directives}

Now let us reproduce our examples in Isabelle.  Here is the distributive
law:
\begin{isabelle}%
?k\ *\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ *\ ?m,\ ?k\ *\ ?n)
\rulename{gcd_mult_distrib2}
\end{isabelle}%
The first step is to replace \isa{?m} by~1 in this law.  The \isa{of} directive
refers to variables not by name but by their order of occurrence in the theorem. 
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\ *\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ *\ 1,\ k\ *\ ?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.  

The next step is to put
the theorem \isa{gcd_mult_0} into a simplified form, performing the steps 
$\gcd(1,n)=1$ and $k\times1=k$.  The \isaindexbold{simplified}
attribute takes a theorem
and returns the result of simplifying it, with respect to the default
simplification rules:
\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\ *\ ?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\ *\ ?n)\ =\ k%
\end{isabelle}
\isa{THEN~sym} gives the current theorem to the rule \isa{sym} and returns the
resulting conclusion.  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.  Better   
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*n)\ =\ k"\isanewline
\isacommand{by}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym])
\end{isabelle}
Compared with the previous proof of \isa{gcd_mult}, this
version shows the reader what has been proved.  Also, the result will be processed
in the normal way.  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{by}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified])
\end{isabelle}

\medskip
The \isaindexbold{rule_format} directive replaces a common usage
of \isa{THEN}\@.  It is needed in proofs by induction when the induction formula must be
expressed using
\isa{\isasymlongrightarrow} and \isa{\isasymforall}.  For example, in 
Sect.\ts\ref{sec:proving-euclid} above we were able to write just this:
\begin{isabelle}
\isacommand{lemma}\ gcd_greatest\
[rule_format]:\isanewline
\ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ \isasymlongrightarrow\
k\ dvd\ gcd(m,n)"
\end{isabelle}
%
It replaces a clumsy use of \isa{THEN}:
\begin{isabelle}
\isacommand{lemma}\ gcd_greatest\
[THEN mp, THEN mp]:\isanewline
\ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ \isasymlongrightarrow\
k\ dvd\ gcd(m,n)"
\end{isabelle}
%
Through \isa{rule_format} we can replace any number of applications of \isa{THEN}
with the rules \isa{mp} and \isa{spec}, eliminating the outermost occurrences of
\isa{\isasymlongrightarrow} and \isa{\isasymforall}.


\subsection{The {\tt\slshape OF} Directive}

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{by}\ (simp\ add:\ gcd.simps)
\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 above 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}
\ \ \ \ \ \#20\ dvd\ (?m\ *\ \#81)\ \isasymLongrightarrow\ \#20\ 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\ +\ ?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\ +\ ?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\ +\ ?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 some 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 
\item \isa{rule_format} puts a theorem into standard form
  by removing \isa{\isasymlongrightarrow} and~\isa{\isasymforall}
\item \isa{simplified} applies the simplifier to a theorem
\end{itemize}


\section{Methods for Forward Proof}

We have seen that the forward proof directives work well within a backward 
proof.  There are many ways to achieve a forward style, using our existing
proof methods and some additional ones that we introduce below.  

The methods \isa{drule}, \isa{frule}, \isa{drule_tac}, etc.,
reason forward from a subgoal.  We have seen them already, using rules such as
\isa{mp} and
\isa{spec} to operate on formulae.  They can also operate on terms, using rules
such as these:
\begin{isabelle}
x\ =\ y\ \isasymLongrightarrow \ f\ x\ =\ f\ y%
\rulename{arg_cong}\isanewline
i\ \isasymle \ j\ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ k%
\rulename{mult_le_mono1}
\end{isabelle}

For example, let us prove a fact about divisibility in the natural numbers:
\begin{isabelle}
\isacommand{lemma}\ "\#2\ \isasymle \ u\ \isasymLongrightarrow \ u*m\ \isasymnoteq
\ Suc(u*n)"\isanewline
\isacommand{apply}\ intro\isanewline
\ 1.\ \isasymlbrakk \#2\ \isasymle \ u;\ u\ *\ m\ =\ Suc\ (u\ *\ n)\isasymrbrakk \ \isasymLongrightarrow \ False%
\end{isabelle}
%
The key step is to apply the function \ldots\isa{mod\ u} to both sides of the
equation
\isa{u*m\ =\ Suc(u*n)}:

\begin{isabelle}
\isacommand{apply}\ (drule_tac\ f="\isasymlambda x.\ x\ mod\ u"\ \isakeyword{in}\
arg_cong)\isanewline
\ 1.\ \isasymlbrakk \#2\ \isasymle \ u;\ u\ *\ m\ mod\ u\ =\ Suc\ (u\ *\ n)\ mod\
u\isasymrbrakk \ \isasymLongrightarrow \ False
\end{isabelle}
%
Simplification reduces the left side to 0 and the right side to~1, yielding the
required contradiction.
\begin{isabelle}
\isacommand{apply}\ (simp\ add:\ mod_Suc)\isanewline
\isacommand{done}
\end{isabelle}

Our proof has used a fact about remainder:
\begin{isabelle}
Suc\ m\ mod\ n\ =\isanewline
(if\ Suc\ (m\ mod\ n)\ =\ n\ then\ 0\ else\ Suc\ (m\ mod\ n))
\rulename{mod_Suc}
\end{isabelle}

\medskip
The methods designed for supporting forward reasoning are \isa{insert} and
\isa{subgoal_tac}.  The \isa{insert} method 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}
\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ m\ *\ n{;}\ m\ *\ gcd\
(k,\ n)\
=\ gcd\ (m\ *\ k,\ m\ *\ 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}
\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}
\ m\ =\ gcd\ (m\ *\ k,\ m\ *\ 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)\ *\ ?n\ +\ ?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*n)\ div\ n\ =\
(m::nat)"\isanewline
\isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m*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 non-trivial expressions must be
enclosed in quotation marks.  Here is the resulting 
subgoal, with its new assumption: 
\begin{isabelle}
%0\ \isacharless\ n\ \isasymLongrightarrow\ (m\
%*\ n)\ div\ n\ =\ m\isanewline
\ 1.\ \isasymlbrakk0\ \isacharless\
n;\ \ (m\ *\ n)\ div\ n\ *\ n\ +\ (m\ *\ n)\ mod\ n\
=\ m\ *\ n\isasymrbrakk\isanewline
\ \ \ \ \isasymLongrightarrow\ (m\ *\ n)\ div\ n\
=\ m
\end{isabelle}
Simplification reduces \isa{(m\ *\ 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 (\isa{blast}), 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
(\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}


\section{Managing Large Proofs}

Naturally you should try to divide proofs into manageable parts.  Look for lemmas
that can be proved separately.  Sometimes you will observe that they are
instances of much simpler facts.  On other occasions, no lemmas suggest themselves
and you are forced to cope with a long proof involving many subgoals.  

\subsection{Tacticals, or Control Structures}

If the proof is long, perhaps it at least has some regularity.  Then you can
express it more concisely using \textbf{tacticals}, which provide control
structures.  Here is a proof (it would be a one-liner using
\isa{blast}, but forget that) that contains a series of repeated
commands:
%
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk P\isasymlongrightarrow Q;\
Q\isasymlongrightarrow R;\ R\isasymlongrightarrow S;\ P\isasymrbrakk \
\isasymLongrightarrow \ S"\isanewline
\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
\isacommand{apply}\ (assumption)\isanewline
\isacommand{done}
\end{isabelle}
%
Each of the three identical commands finds an implication and proves its
antecedent by assumption.  The first one finds \isa{P\isasymlongrightarrow Q} and
\isa{P}, concluding~\isa{Q}; the second one concludes~\isa{R} and the third one
concludes~\isa{S}.  The final step matches the assumption \isa{S} with the goal to
be proved.

Suffixing a method with a plus sign~(\isa+)
expresses one or more repetitions:
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk P\isasymlongrightarrow Q;\ Q\isasymlongrightarrow R;\ R\isasymlongrightarrow S;\ P\isasymrbrakk \ \isasymLongrightarrow \ S"\isanewline
\isacommand{by}\ (drule\ mp,\ assumption)+
\end{isabelle}
%
Using \isacommand{by} takes care of the final use of \isa{assumption}.  The new
proof is more concise.  It is also more general: the repetitive method works
for a chain of implications having any length, not just three.

Choice is another control structure.  Separating two methods by a vertical
bar~(\isa|) gives the effect of applying the first method, and if that fails,
trying the second.  It can be combined with repetition, when the choice must be
made over and over again.  Here is a chain of implications in which most of the
antecedents are proved by assumption, but one is proved by arithmetic:
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ x<\#5\isasymlongrightarrow P;\
Suc\ x\ <\ \#5\isasymrbrakk \ \isasymLongrightarrow \ R"\ \isanewline
\isacommand{by}\ (drule\ mp,\ (assumption|arith))+
\end{isabelle}
The \isa{arith}
method can prove $x<5$ from $x+1<5$, but it cannot duplicate the effect of
\isa{assumption}.  Therefore, we combine these methods using the choice
operator.

A postfixed question mark~(\isa?) expresses zero or one repetitions of a method. 
It can also be viewed as the choice between executing a method and doing nothing. 
It is useless at top level but may be valuable within other control structures. 


\subsection{Subgoal Numbering}

Another problem in large proofs is contending with huge
subgoals or many subgoals.  Induction can produce a proof state that looks
like this:
\begin{isabelle}
\ 1.\ bigsubgoal1\isanewline
\ 2.\ bigsubgoal2\isanewline
\ 3.\ bigsubgoal3\isanewline
\ 4.\ bigsubgoal4\isanewline
\ 5.\ bigsubgoal5\isanewline
\ 6.\ bigsubgoal6
\end{isabelle}
If each \isa{bigsubgoal} is 15 lines or so, the proof state will be too big to
scroll through.  By default, Isabelle displays at most 10 subgoals.  The 
\isacommand{pr} command lets you change this limit:
\begin{isabelle}
\isacommand{pr}\ 2\isanewline
\ 1.\ bigsubgoal1\isanewline
\ 2.\ bigsubgoal2\isanewline
A total of 6 subgoals...
\end{isabelle}

\medskip
All methods apply to the first subgoal.
Sometimes, not only in a large proof, you may want to focus on some other
subgoal.  Then you should try the commands \isacommand{defer} or \isacommand{prefer}.

In the following example, the first subgoal looks hard, while the others
look as if \isa{blast} alone could prove them:
%\begin{isabelle}
%\isacommand{lemma}\ "hard\ \isasymand \ (P\ \isasymor \ \isachartilde P)\ \isasymand \ (Q\isasymlongrightarrow Q)"\isanewline
%\isacommand{apply}\ intro
%\end{isabelle}
\begin{isabelle}
\ 1.\ hard\isanewline
\ 2.\ \isasymnot \ \isasymnot \ P\ \isasymLongrightarrow \ P\isanewline
\ 3.\ Q\ \isasymLongrightarrow \ Q%
\end{isabelle}
%
The \isacommand{defer} command moves the first subgoal into the last position.
\begin{isabelle}
\isacommand{defer}\ 1\isanewline
\ 1.\ \isasymnot \ \isasymnot \ P\ \isasymLongrightarrow \ P\isanewline
\ 2.\ Q\ \isasymLongrightarrow \ Q\isanewline
\ 3.\ hard%
\end{isabelle}
%
Now we apply \isa{blast} repeatedly to the easy subgoals:
\begin{isabelle}
\isacommand{apply}\ blast+\isanewline
\ 1.\ hard%
\end{isabelle}
Using \isacommand{defer}, we have cleared away the trivial parts of the proof so
that we can devote attention to the difficult part.

\medskip
The \isacommand{prefer} command moves the specified subgoal into the
first position.  For example, if you suspect that one of your subgoals is
invalid (not a theorem), then you should investigate that subgoal first.  If it
cannot be proved, then there is no point in proving the other subgoals.
\begin{isabelle}
\ 1.\ ok1\isanewline
\ 2.\ ok2\isanewline
\ 3.\ doubtful%
\end{isabelle}
%
We decide to work on the third subgoal.
\begin{isabelle}
\isacommand{prefer}\ 3\isanewline
\ 1.\ doubtful\isanewline
\ 2.\ ok1\isanewline
\ 3.\ ok2
\end{isabelle}
If we manage to prove \isa{doubtful}, then we can work on the other
subgoals, confident that we are not wasting our time.  Finally we revise the
proof script to remove the \isacommand{prefer} command, since we needed it only to
focus our exploration.  The previous example is different: its use of
\isacommand{defer} stops trivial subgoals from cluttering the rest of the
proof.  Even there, we should consider proving \isa{hard} as a preliminary
lemma.  Always seek ways to streamline your proofs.
 

\medskip
Summary:
\begin{itemize}
\item the control structures \isa+, \isa? and \isa| help express complicated proofs
\item the \isacommand{pr} command can limit the number of subgoals to display
\item the \isacommand{defer} and \isacommand{prefer} commands move a 
subgoal to the last or first position
\end{itemize}

\begin{exercise}
This proof uses \isa? and \isa+ to \ldots{} can you explain?
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk P\isasymand Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ R"\isanewline
\isacommand{by}\ (drule\ mp,\ intro?,\ assumption+)+
\end{isabelle}
\end{exercise}