doc-src/TutorialI/Rules/rules.tex

added warning about inconsistent context to Metis;
it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent

% $Id$
%!TEX root = ../tutorial.tex
\chapter{The Rules of the Game}
\label{chap:rules}
 
This chapter outlines the concepts and techniques that underlie reasoning
in Isabelle.  Until now, we have proved everything using only induction and
simplification, but any serious verification project requires more elaborate
forms of inference.  The chapter also introduces the fundamentals of
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.  Backward or goal-directed proof is our usual style,
but the chapter also introduces forward reasoning, where one theorem is
transformed to yield another.

\section{Natural Deduction}

\index{natural deduction|(}%
In Isabelle, proofs are constructed using inference rules. The 
most familiar inference rule is probably \emph{modus ponens}:%
\index{modus ponens@\emph{modus ponens}} 
\[ \infer{Q}{P\imp Q & P} \]
This rule says that from $P\imp Q$ and $P$ we may infer~$Q$.  

\textbf{Natural deduction} is an attempt to formalize logic in a way 
that mirrors human reasoning patterns. 
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 to 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.%
\index{natural deduction|)}


\section{Introduction Rules}

\index{introduction rules|(}%
An 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\rulenamedx{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}):\index{unknowns|bold} 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 how rules work.  It also introduces a
style of indentation.  If a command adds a new subgoal, then the next
command's indentation is increased by one space; if it proves a subgoal, then
the indentation is reduced.  This provides the reader with hints about the
subgoal structure.
\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 \methdx{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.%
\index{introduction rules|)}


\section{Elimination Rules}

\index{elimination rules|(}%
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\rulenamedx{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}\@.  We invoke it using \methdx{erule}, a
method designed to work with elimination rules.  It looks for an assumption that
matches the rule's first premise.  It deletes the matching assumption,
regards the first premise as proved and returns subgoals corresponding to
the remaining premises.  When we apply \isa{erule} to \isa{disjE}, only two
subgoals result.  This is better than applying it using \isa{rule}
to get three subgoals, then proving the first by assumption: the other
subgoals would have the redundant assumption 
\hbox{\isa{P\ \isasymor\ Q}}.
Most of the time, \isa{erule} is  the best way to use elimination rules, since it
replaces an assumption by its subformulas; only rarely does the original
assumption remain useful.

\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}
These are the two subgoals returned by \isa{erule}.  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 one of the form $P\disj Q$.%
\index{elimination rules|)}


\section{Destruction Rules: Some Examples}

\index{destruction rules|(}%
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},\index{Girard, Jean-Yves|fnote}
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\rulenamedx{conjE}
\end{isabelle}
\index{destruction rules|)}

\begin{exercise}
Use the rule \isa{conjE} to shorten the proof above. 
\end{exercise}


\section{Implication}

\index{implication|(}%
At the start of this chapter, we saw the rule \emph{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\rulenamedx{impI}
\end{isabelle}
And this is \emph{modus ponens}\index{modus ponens@\emph{modus ponens}}:
\begin{isabelle}
\isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\
\isasymLongrightarrow\ ?Q
\rulenamedx{mp}
\end{isabelle}

Here is a proof using the implication rules.  This 
lemma performs a sort of uncurrying, replacing the two antecedents 
of a nested implication by a conjunction.  The proof illustrates
how assumptions work.  At each proof step, the subgoals inherit the previous
assumptions, perhaps with additions or deletions.  Rules such as
\isa{impI} and \isa{disjE} add assumptions, while applying \isa{erule} or
\isa{drule} deletes the matching assumption.
\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.%
\index{implication|)}

\medskip
\index{by@\isacommand{by} (command)|(}%
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.%
\index{by@\isacommand{by} (command)|)}



\section{Negation}
 
\index{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.  This section
also illustrates the \isa{intro} method: a convenient way of
applying introduction rules.

Negation introduction deduces $\lnot P$ if assuming $P$ leads to a 
contradiction. Negation elimination deduces any formula in the 
presence of $\lnot P$ together with~$P$: 
\begin{isabelle}
(?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P%
\rulenamedx{notI}\isanewline
\isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R%
\rulenamedx{notE}
\end{isabelle}
%
Classical logic allows us to assume $\lnot P$ 
when attempting to prove~$P$: 
\begin{isabelle}
(\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P%
\rulenamedx{classical}
\end{isabelle}

\index{contrapositives|(}%
The implications $P\imp Q$ and $\lnot Q\imp\lnot P$ are logically
equivalent, and each is called the
\textbf{contrapositive} of the other.  Four further rules support
reasoning about contrapositives.  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?Q;\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\
\isasymnot\ ?P%
\rulename{contrapos_pn}\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.%
\index{contrapositives|)}

The most important of these is \isa{contrapos_np}.  It is useful
for applying introduction rules to negated assumptions.  For instance, 
the assumption $\lnot(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\ impI)\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 a new method, \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 \methdx{intro} method, which
repeatedly applies the given 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

The following example may be skipped on a first reading.  It involves a
peculiar but important rule, a form of disjunction introduction:
\begin{isabelle}
(\isasymnot \ ?Q\ \isasymLongrightarrow \ ?P)\ \isasymLongrightarrow \ ?P\ \isasymor \ ?Q%
\rulenamedx{disjCI}
\end{isabelle}
This rule combines the effects of \isa{disjI1} and \isa{disjI2}.  Its great
advantage is that we can remove the disjunction symbol without deciding
which disjunction to prove.  This treatment of disjunction is standard in sequent
and tableau calculi.

\begin{isabelle}
\isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\
\isasymLongrightarrow\ P\ \isasymor\ (Q\ \isasymand\ R)"\isanewline
\isacommand{apply}\ (rule\ disjCI)\isanewline
\isacommand{apply}\ (elim\ conjE\ disjE)\isanewline
\ \isacommand{apply}\ assumption
\isanewline
\isacommand{by}\ (erule\ contrapos_np,\ rule\ conjI)
\end{isabelle}
%
The first proof step to applies the introduction rules \isa{disjCI}.
The resulting subgoal has the negative assumption 
\hbox{\isa{\isasymnot(Q\ \isasymand\ R)}}.  

\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.%
\index{negation|)}


\section{Interlude: the Basic Methods for Rules}

We have seen examples of many tactics that operate on individual rules.  It
may be helpful to review how they work given an arbitrary rule such as this:
\[ \infer{Q}{P@1 & \ldots & P@n} \]
Below, we refer to $P@1$ as the \bfindex{major premise}.  This concept
applies only to elimination and destruction rules.  These rules act upon an
instance of their major premise, typically to replace it by subformulas of itself.

Suppose that the rule above is called~\isa{R}\@.  Here are the basic rule
methods, most of which we have already seen:
\begin{itemize}
\item 
Method \isa{rule\ R} unifies~$Q$ with the current subgoal, replacing it
by $n$ new subgoals: instances of $P@1$, \ldots,~$P@n$. 
This is backward reasoning and is appropriate for introduction rules.
\item 
Method \isa{erule\ R} unifies~$Q$ with the current subgoal and
simultaneously unifies $P@1$ with some assumption.  The subgoal is 
replaced by the $n-1$ new subgoals of proving
instances of $P@2$,
\ldots,~$P@n$, with the matching assumption deleted.  It is appropriate for
elimination rules.  The method
\isa{(rule\ R,\ assumption)} is similar, but it does not delete an
assumption.
\item 
Method \isa{drule\ R} unifies $P@1$ with some assumption, which it
then deletes.  The subgoal is 
replaced by the $n-1$ new subgoals of proving $P@2$, \ldots,~$P@n$; an
$n$th subgoal is like the original one but has an additional assumption: an
instance of~$Q$.  It is appropriate for destruction rules. 
\item 
Method \isa{frule\ R} is like \isa{drule\ R} except that the matching
assumption is not deleted.  (See {\S}\ref{sec:frule} below.)
\end{itemize}

Other methods apply a rule while constraining some of its
variables.  The typical form is
\begin{isabelle}
\ \ \ \ \ \methdx{rule_tac}\ $v@1$ = $t@1$ \isakeyword{and} \ldots \isakeyword{and}
$v@k$ =
$t@k$ \isakeyword{in} R
\end{isabelle}
This method behaves like \isa{rule R}, while instantiating the variables
$v@1$, \ldots,
$v@k$ as specified.  We similarly have \methdx{erule_tac}, \methdx{drule_tac} and
\methdx{frule_tac}.  These methods also let us specify which subgoal to
operate on.  By default it is the first subgoal, as with nearly all
methods, but we can specify that rule \isa{R} should be applied to subgoal
number~$i$:
\begin{isabelle}
\ \ \ \ \ rule_tac\ [$i$] R
\end{isabelle}



\section{Unification and Substitution}\label{sec:unification}

\index{unification|(}%
As we have seen, Isabelle rules involve schematic variables, which begin with
a question mark and act as
placeholders for terms.  \textbf{Unification} --- well known to Prolog programmers --- is the act of
making two terms identical, possibly replacing their schematic variables by
terms.  The simplest case is when the two terms are already the same. Next
simplest is \textbf{pattern-matching}, which replaces variables in only one of the
terms.  The
\isa{rule} method typically  matches the rule's conclusion
against the current subgoal.  The
\isa{assumption} method matches the current subgoal's conclusion
against each of its assumptions.   Unification can instantiate variables in both terms; 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 represent unknown terms.  Given a goal such
as $\exists x.\,P$, they let us proceed with a proof.  They can be 
filled in later, sometimes in stages and often automatically. 

\begin{pgnote}
If unification fails when you think it should succeed, try setting the Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$
\pgmenu{Trace Unification},
which makes Isabelle show the cause of unification failures (in Proof
General's \pgmenu{Trace} buffer).
\end{pgnote}
\noindent
For example, suppose we are trying to prove this subgoal by assumption:
\begin{isabelle}
\ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a)
\end{isabelle}
The \isa{assumption} method having failed, we try again with the flag set:
\begin{isabelle}
\isacommand{apply} assumption
\end{isabelle}
In this trivial case, the output clearly shows that \isa{e} clashes with \isa{c}:
\begin{isabelle}
Clash: e =/= c
\end{isabelle}

Isabelle uses
\textbf{higher-order} unification, which works in the
typed $\lambda$-calculus.  The procedure requires search and is potentially
undecidable.  For our purposes, however, the differences from ordinary
unification are straightforward.  It handles bound variables
correctly, avoiding capture.  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.  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.  Unfortunately, even if \isa{trace_unify_fail} is set, Isabelle displays no information about this type of failure.

\begin{warn}
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.
\end{warn}



\subsection{Substitution and the {\tt\slshape subst} Method}
\label{sec:subst}

\index{substitution|(}%
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
\rulenamedx{ssubst}
\end{isabelle}
Crucially, \isa{?P} is a function 
variable.  It can be replaced by a $\lambda$-term 
with one bound variable, whose occurrences identify the places 
in which $s$ will be replaced by~$t$.  The proof above requires \isa{?P}
to be replaced by \isa{{\isasymlambda}x.~x=s}; the second premise will then
be \isa{s=s} and the conclusion will be \isa{t=s}.

The \isa{simp} method also replaces equals by equals, but 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 assumption \isa{x\ =\ f\ x}, if used for rewriting, would loop, 
replacing \isa{x} by \isa{f x} and then by
\isa{f(f x)} and so forth. (Here \isa{simp} 
would see the danger and would re-orient the equality, but in more complicated
cases it can be fooled.) When we apply the substitution rule,  
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 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.

The \methdx{subst} method performs individual substitutions. In simple cases,
it closely resembles a use of the substitution rule.  Suppose a
proof has reached this point:
\begin{isabelle}
\ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \ \isasymLongrightarrow \ f\ z\ =\ x\ *\ y%
\end{isabelle}
Now we wish to apply a commutative law:
\begin{isabelle}
?m\ *\ ?n\ =\ ?n\ *\ ?m%
\rulename{mult_commute}
\end{isabelle}
Isabelle rejects our first attempt:
\begin{isabelle}
apply (simp add: mult_commute)
\end{isabelle}
The simplifier notices the danger of looping and refuses to apply the
rule.%
\footnote{More precisely, it only applies such a rule if the new term is
smaller under a specified ordering; here, \isa{x\ *\ y}
is already smaller than
\isa{y\ *\ x}.}
%
The \isa{subst} method applies \isa{mult_commute} exactly once.  
\begin{isabelle}
\isacommand{apply}\ (subst\ mult_commute)\isanewline
\ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \
\isasymLongrightarrow \ f\ z\ =\ y\ *\ x%
\end{isabelle}
As we wanted, \isa{x\ *\ y} has become \isa{y\ *\ x}.

\medskip
This use of the \methdx{subst} method has the same effect as the command
\begin{isabelle}
\isacommand{apply}\ (rule\ mult_commute [THEN ssubst])
\end{isabelle}
The attribute \isa{THEN}, which combines two rules, is described in 
{\S}\ref{sec:THEN} below. The \methdx{subst} method is more powerful than
applying the substitution rule. It can perform substitutions in a subgoal's
assumptions. Moreover, if the subgoal contains more than one occurrence of
the left-hand side of the equality, the \methdx{subst} method lets us specify which occurrence should be replaced.


\subsection{Unification and Its Pitfalls}

Higher-order unification can be tricky.  Here is an example, which you may
want to skip on your first reading:
\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 \commdx{back}
command allows us to reject this possibility and demand 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 \isacommand{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 \isacommand{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 \isacommand{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.%
\index{unification|)}

\medskip
This example shows that unification can do strange things with
function variables.  We were forced to select the right unifier using the
\isacommand{back} command.  That is all right during exploration, but \isacommand{back}
should never appear in the final version of a proof.  You can eliminate the
need for \isacommand{back} by giving Isabelle less freedom when you apply a rule.

One way to constrain the inference is by joining two methods in a 
\isacommand{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 constrain unification is 
by instantiating 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.\ triple\ 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 a theorem
modified using~\isa{of}, described in
{\S}\ref{sec:forward} below.   But \isa{rule_tac}, unlike \isa{of}, can 
express instantiations that refer to 
\isasymAnd-bound variables in the current subgoal.%
\index{substitution|)}


\section{Quantifiers}

\index{quantifiers!universal|(}%
Quantifiers require formalizing syntactic substitution and the notion of 
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
\bfindex{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 operator of the meta-logic, namely
\isa\isasymLongrightarrow, which expresses  inference rules and the treatment
of assumptions. The only other operator 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\rulenamedx{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~\isa{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\rulenamedx{spec}
\end{isabelle}
This destruction rule takes a 
universally quantified formula and removes the quantifier, replacing 
the bound variable \isa{x} by the schematic variable \isa{?x}.  Recall that a
schematic variable starts with a question mark and acts as a
placeholder: it can be replaced by any term.  

The universal elimination rule is also
available in the standard elimination format.  Like \isa{conjE}, it never
appears in logic books:
\begin{isabelle}
\isasymlbrakk \isasymforall x.\ ?P\ x;\ ?P\ ?x\ \isasymLongrightarrow \ ?R\isasymrbrakk \ \isasymLongrightarrow \ ?R%
\rulenamedx{allE}
\end{isabelle}
The methods \isa{drule~spec} and \isa{erule~allE} do precisely the
same inference.

To see how $\forall$-elimination 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.  Let us walk through the proof.
\begin{isabelle}
\isacommand{lemma}\ "(\isasymforall x.\ P\ \isasymlongrightarrow \ Q\ x)\
\isasymLongrightarrow \ P\ \isasymlongrightarrow \ (\isasymforall x.\ Q\
x)"
\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}
\isacommand{apply}\ (rule\ impI,\ rule\ allI)\isanewline
\ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\
x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x
\end{isabelle}
As before, it replaces the HOL 
quantifier by a meta-level quantifier, producing a subgoal that 
binds the variable~\isa{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}.  Subgoals inherit the context,
although assumptions can be added or deleted (as we saw
earlier), while rules such as \isa{allI} add bound variables.

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}
\isacommand{apply}\ (drule\ spec)\isanewline
\ 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.  We have
removed the quantifier and replaced the bound variable
by the curious term 
\isa{?x2~x}.  This term is a placeholder: it may become any term that can be
built from~\isa{x}.  (Formally, \isa{?x2} is an unknown of function type, applied
to the argument~\isa{x}.)  This new assumption is an implication, so we can  use
\emph{modus ponens} on it, which concludes the proof. 
\begin{isabelle}
\isacommand{by}\ (drule\ mp)
\end{isabelle}
Let us take a closer look at this last step.  \emph{Modus ponens} yields
two subgoals: one where we prove the antecedent (in this case \isa{P}) and
one where we may assume the consequent.  Both of these subgoals are proved
by the
\isa{assumption} method, which is implicit in the
\isacommand{by} command.  Replacing the \isacommand{by} command by 
\isa{\isacommand{apply} (drule\ mp, assumption)} would have left one last
subgoal:
\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~\isa{x}, and here 
it should simply be~\isa{x}.  The assumption need not
be identical to the conclusion, provided the two formulas are unifiable.%
\index{quantifiers!universal|)}  


\subsection{The Existential Quantifier}

\index{quantifiers!existential|(}%
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\rulenamedx{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\rulenamedx{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.  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}
\index{quantifiers!existential|)}


\subsection{Renaming a Bound Variable: {\tt\slshape rename_tac}}

\index{assumptions!renaming|(}\index{*rename_tac (method)|(}%
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.  The result may not be ideal:
\begin{isabelle}
\isacommand{lemma}\ "x\ <\ y\ \isasymLongrightarrow \ \isasymforall x\ y.\ P\ x\
(f\ y)"\isanewline
\isacommand{apply}\ (intro allI)\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 (method)!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.%
\index{assumptions!renaming|)}\index{*rename_tac (method)|)}


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

\index{assumptions!reusing|(}\index{*frule (method)|(}%
Note that \isa{drule spec} removes the universal quantifier and --- as
usual with elimination rules --- discards the original formula.  Sometimes, a
universal formula has to be kept so that it can be used again.  Then we use a new
method: \isa{frule}.  It acts like \isa{drule} but copies rather than replaces
the selected assumption.  The \isa{f} is for \emph{forward}.

In this example, going from \isa{P\ a} to \isa{P(h(h~a))}
requires two uses of the quantified assumption, one for each~\isa{h}
in~\isa{h(h~a)}.
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);
\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P(h\ (h\ a))"
\end{isabelle}
%
Examine the subgoal left by \isa{frule}:
\begin{isabelle}
\isacommand{apply}\ (frule\ spec)\isanewline
\ 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 what \isa{drule} would have left except that the quantified
assumption is still present.  Next we apply \isa{mp} to the
implication and the assumption~\isa{P\ a}:
\begin{isabelle}
\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
\ 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
continue the proof, we apply \isa{spec} again.  We shall not need it
again, so we can use
\isa{drule}.
\begin{isabelle}
\isacommand{apply}\ (drule\ spec)\isanewline
\ 1.\ \isasymlbrakk P\ a;\ P\ (h\ a);\ P\ ?x2\ 
\isasymlongrightarrow \ P\ (h\ ?x2)\isasymrbrakk \ \isasymLongrightarrow \
P\ (h\ (h\ a))
\end{isabelle}
%
The new assumption bridges the gap between \isa{P(h\ a)} and \isa{P(h(h\ a))}.
\begin{isabelle}
\isacommand{by}\ (drule\ mp)
\end{isabelle}

\medskip
\emph{A final remark}.  Replacing this \isacommand{by} command with
\begin{isabelle}
\isacommand{apply}\ (drule\ mp,\ assumption)
\end{isabelle}
would not work: 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}.  Or, of course,
we could have given the entire proof to \isa{auto}.%
\index{assumptions!reusing|)}\index{*frule (method)|)}



\subsection{Instantiating a Quantifier Explicitly}
\index{quantifiers!instantiating}

We can prove a theorem of the form $\exists x.\,P\, x$ by exhibiting a
suitable term~$t$ such that $P\,t$ is true.  Dually, we can use an
assumption of the form $\forall x.\,P\, x$ to generate a new assumption $P\,t$ for
a suitable term~$t$.  In many cases, 
Isabelle makes the correct choice automatically, constructing the term by
unification.  In other cases, the required term is not obvious and we must
specify it ourselves.  Suitable methods are \isa{rule_tac}, \isa{drule_tac}
and \isa{erule_tac}.

We have seen (just above, {\S}\ref{sec:frule}) a proof of this lemma:
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk \isasymforall x.\ P\ x\
\isasymlongrightarrow \ P\ (h\ x);\ P\ a\isasymrbrakk \
\isasymLongrightarrow \ P(h\ (h\ a))"
\end{isabelle}
We had reached 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}
%
The proof requires instantiating the quantified assumption with the
term~\isa{h~a}.
\begin{isabelle}
\isacommand{apply}\ (drule_tac\ x\ =\ "h\ a"\ \isakeyword{in}\
spec)\isanewline
\ 1.\ \isasymlbrakk P\ a;\ P\ (h\ a);\ P\ (h\ a)\ \isasymlongrightarrow \
P\ (h\ (h\ a))\isasymrbrakk \ \isasymLongrightarrow \ P\ (h\ (h\ a))
\end{isabelle}
We have forced the desired instantiation.

\medskip
Existential formulas can be instantiated too.  The next example uses the 
\textbf{divides} relation\index{divides relation}
of number theory: 
\begin{isabelle}
?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
\rulename{dvd_def}
\end{isabelle}

Let us prove that multiplication of natural numbers is monotone with
respect to the divides relation:
\begin{isabelle}
\isacommand{lemma}\ mult_dvd_mono:\ "{\isasymlbrakk}i\ dvd\ m;\ j\ dvd\
n\isasymrbrakk\ \isasymLongrightarrow\ i*j\ dvd\ (m*n\ ::\ nat)"\isanewline
\isacommand{apply}\ (simp\ add:\ dvd_def)
\end{isabelle}
%
Unfolding the definition of divides has left this subgoal:
\begin{isabelle}
\ 1.\ \isasymlbrakk \isasymexists k.\ m\ =\ i\ *\ k;\ \isasymexists k.\ n\
=\ j\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\
n\ =\ i\ *\ j\ *\ k
\end{isabelle}
%
Next, we eliminate the two existential quantifiers in the assumptions:
\begin{isabelle}
\isacommand{apply}\ (erule\ exE)\isanewline
\ 1.\ \isasymAnd k.\ \isasymlbrakk \isasymexists k.\ n\ =\ j\ *\ k;\ m\ =\
i\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\
=\ i\ *\ j\ *\ k%
\isanewline
\isacommand{apply}\ (erule\ exE)
\isanewline
\ 1.\ \isasymAnd k\ ka.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\
ka\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\ =\ i\
*\ j\ *\ k
\end{isabelle}
%
The term needed to instantiate the remaining quantifier is~\isa{k*ka}.  But
\isa{ka} is an automatically-generated name.  As noted above, references to
such variable names makes a proof less resilient to future changes.  So,
first we rename the most recent variable to~\isa{l}:
\begin{isabelle}
\isacommand{apply}\ (rename_tac\ l)\isanewline
\ 1.\ \isasymAnd k\ l.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\ l\isasymrbrakk \
\isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\ =\ i\ *\ j\ *\ k%
\end{isabelle}

We instantiate the quantifier with~\isa{k*l}:
\begin{isabelle}
\isacommand{apply}\ (rule_tac\ x="k*l"\ \isakeyword{in}\ exI)\ \isanewline
\ 1.\ \isasymAnd k\ ka.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\
ka\isasymrbrakk \ \isasymLongrightarrow \ m\ *\ n\ =\ i\
*\ j\ *\ (k\ *\ ka)
\end{isabelle}
%
The rest is automatic, by arithmetic.
\begin{isabelle}
\isacommand{apply}\ simp\isanewline
\isacommand{done}\isanewline
\end{isabelle}



\section{Description Operators}
\label{sec:SOME}

\index{description operators|(}%
HOL provides two description operators.
A \textbf{definite description} formalizes the word ``the,'' as in
``the greatest divisior of~$n$.''
It returns an arbitrary value unless the formula has a unique solution.
An \textbf{indefinite description} formalizes the word ``some,'' as in
``some member of~$S$.''  It differs from a definite description in not
requiring the solution to be unique: it uses the axiom of choice to pick any
solution. 

\begin{warn}
Description operators can be hard to reason about.  Novices
should try to avoid them.  Fortunately, descriptions are seldom required.
\end{warn}

\subsection{Definite Descriptions}

\index{descriptions!definite}%
A definite description is traditionally written $\iota x.  P(x)$.  It denotes
the $x$ such that $P(x)$ is true, provided there exists a unique such~$x$;
otherwise, it returns an arbitrary value of the expected type.
Isabelle uses \sdx{THE} for the Greek letter~$\iota$.  

%(The traditional notation could be provided, but it is not legible on screen.)

We reason using this rule, where \isa{a} is the unique solution:
\begin{isabelle}
\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \ 
\isasymLongrightarrow \ (THE\ x.\ P\ x)\ =\ a%
\rulenamedx{the_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.

A more challenging example illustrates how Isabelle/HOL defines the least number
operator, which denotes the least \isa{x} satisfying~\isa{P}:%
\index{least number operator|see{\protect\isa{LEAST}}}
\begin{isabelle}
(LEAST\ x.\ P\ x)\ = (THE\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))
\end{isabelle}
%
Let us prove the analogue of \isa{the_equality} for \sdx{LEAST}\@.
\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
\isanewline
\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\isasymrbrakk \isanewline
\isaindent{\ 1.\ }\isasymLongrightarrow \ (THE\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))\ =\ k%
\end{isabelle}
The first step has merely unfolded the definition.
\begin{isabelle}
\isacommand{apply}\ (rule\ the_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{the_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}

\index{Hilbert's $\varepsilon$-operator}%
\index{descriptions!indefinite}%
An indefinite description is traditionally written $\varepsilon x. P(x)$ and is
known as Hilbert's $\varepsilon$-operator.  It denotes
some $x$ such that $P(x)$ is true, provided one exists.
Isabelle uses \sdx{SOME} for the Greek letter~$\varepsilon$.

Here is the definition of~\cdx{inv},\footnote{In fact, \isa{inv} is defined via a second constant \isa{inv_into}, which we ignore here.} which expresses inverses of
functions:
\begin{isabelle}
inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%
\rulename{inv_def}
\end{isabelle}
Using \isa{SOME} rather than \isa{THE} makes \isa{inv~f} behave well
even if \isa{f} is not injective.  As it happens, most useful theorems about
\isa{inv} do assume the function to be injective.

The inverse of \isa{f}, when applied to \isa{y}, returns some~\isa{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\ n)\ =\ n"\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.  In detail, the left-hand side simplifies
to \isa{SOME\ x.\ Suc\ x\ =\ Suc\ n}, then to \isa{SOME\ x.\ x\ =\ n} and
finally to~\isa{n}.  

We know nothing about what
\isa{inv~Suc} returns when applied to zero.  The proof above still treats
\isa{SOME} as a definite description, since it only reasons about
situations in which the value is described uniquely.  Indeed, \isa{SOME}
satisfies this rule:
\begin{isabelle}
\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \ 
\isasymLongrightarrow \ (SOME\ x.\ P\ x)\ =\ a%
\rulenamedx{some_equality}
\end{isabelle}
To go further is
tricky and requires rules such as these:
\begin{isabelle}
P\ x\ \isasymLongrightarrow \ P\ (SOME\ x.\ P\ x)
\rulenamedx{someI}\isanewline
\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ Q\
x\isasymrbrakk \ \isasymLongrightarrow \ Q\ (SOME\ x.\ P\ x)
\rulenamedx{someI2}
\end{isabelle}
Rule \isa{someI} is basic: if anything satisfies \isa{P} then so does
\hbox{\isa{SOME\ x.\ P\ x}}.  The repetition of~\isa{P} in the conclusion makes it
difficult to apply in a backward proof, so the derived rule \isa{someI2} is
also provided. 

\medskip
For example, let us prove the \rmindex{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}

\subsubsection{Historical Note}
The original purpose of Hilbert's $\varepsilon$-operator was to express an
existential destruction rule:
\[ \infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P} \]
This rule is seldom used for that purpose --- it can cause exponential
blow-up --- but it is occasionally used as an introduction rule
for the~$\varepsilon$-operator.  Its name in HOL is \tdxbold{someI_ex}.%%
\index{description operators|)}


\section{Some Proofs That Fail}

\index{proofs!examples of failing|(}%
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"
\end{isabelle}
The first steps are  routine.  We apply conjunction elimination to break
the assumption into two existentially quantified assumptions. 
Applying existential elimination removes one of the quantifiers. 
\begin{isabelle}
\isacommand{apply}\ (erule\ conjE)\isanewline
\isacommand{apply}\ (erule\ exE)\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}
\isacommand{apply}\ (erule\ exE)\isanewline
\ 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}
\isacommand{apply}\ (rule\ exI)\isanewline
\isacommand{apply}\ (rule\ conjI)\isanewline
\ 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}
\ \isacommand{apply}\ assumption\isanewline
\ 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}
When interacting with Isabelle via the shell interface,
you can abandon a proof using the \isacommand{oops} command.

\medskip 

Here is another abortive proof, illustrating the interaction between 
bound variables and unknowns.  
If $R$ is a reflexive relation, 
is there an $x$ such that $R\,x\,y$ holds for all $y$?  Let us see what happens when
we attempt to prove it. 
\begin{isabelle}
\isacommand{lemma}\ "\isasymforall y.\ R\ y\ y\ \isasymLongrightarrow 
\ \isasymexists x.\ \isasymforall y.\ R\ x\ y"
\end{isabelle}
First,  we remove the existential quantifier. The new proof state has  an
unknown, namely~\isa{?x}. 
\begin{isabelle}
\isacommand{apply}\ (rule\ exI)\isanewline
\ 1.\ \isasymforall y.\ R\ y\ y\ \isasymLongrightarrow \ \isasymforall y.\ R\ ?x\ y%
\end{isabelle}
It looks like we can just apply \isa{assumption}, but it fails.  Isabelle
refuses to substitute \isa{y}, a bound variable, for~\isa{?x}; that would be
a bound variable capture.  We can still try to finish the proof in some
other way. We remove the universal quantifier  from the conclusion, moving
the bound variable~\isa{y} into the subgoal.  But note that it is still
bound!
\begin{isabelle}
\isacommand{apply}\ (rule\ allI)\isanewline
\ 1.\ \isasymAnd y.\ \isasymforall y.\ R\ y\ y\ \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}
\isacommand{apply}\ (drule\ spec)\isanewline
\ 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}.  Isabelle can
replace \isa{?z2~y} by \isa{y}; this involves instantiating
\isa{?z2} to the identity function.  But, just as two steps earlier,
Isabelle refuses to substitute~\isa{y} for~\isa{?x}.
This example is typical of how Isabelle enforces sound quantifier reasoning. 
\index{proofs!examples of failing|)}

\section{Proving Theorems Using the {\tt\slshape blast} Method}

\index{*blast (method)|(}%
It is hard to prove many theorems using the methods 
described above. A proof may be 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.
It is particularly hard for a resolution prover, where 
converting the nested biconditionals to
clause form produces a combinatorial
explosion~\cite{pelletier86}. 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  
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.  The formula below may look horrible, but
the \isa{blast} method proves it in milliseconds. 
\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}\indexbold{safe rules} rule is one that can be applied 
backwards without losing information; an
\textbf{unsafe}\indexbold{unsafe rules} 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 \attrdx{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 \attrdx{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 \attrdx{iff} attribute:
\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 \attrdx{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.  

Classical reasoning is different from
simplification.  Simplification is deterministic.  It applies rewrite rules
repeatedly, as long as possible, transforming a goal into another goal.  Classical
reasoning uses search and backtracking in order to prove a goal outright.%
\index{*blast (method)|)}%


\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 
\methdx{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 \methdx{clarsimp}, a method
that interleaves \isa{clarify} and \isa{simp}.  Also there is  \methdx{safe},
which like \isa{clarify} performs obvious steps but even applies those that
split goals.

The \methdx{force} method applies the classical
reasoner and simplifier  to one goal. 
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 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
\methdx{fast} method succeeds: 
\begin{isabelle}
\isacommand{apply}\ (fast\ intro!:\ someI)
\end{isabelle}

The \methdx{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 \isa{best} 
can often manage.

Here is a summary of the classical reasoning methods:
\begin{itemize}
\item \methdx{blast} works automatically and is the fastest

\item \methdx{clarify} and \methdx{clarsimp} perform obvious steps without
splitting the goal;  \methdx{safe} even splits goals

\item \methdx{force} uses classical reasoning and simplification to prove a goal;
 \methdx{auto} is similar but leaves what it cannot prove

\item \methdx{fast} and \methdx{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  & \methdx{clarify}    & \methdx{safe} \\ \hline
     simp  & \methdx{clarsimp}   & \methdx{auto} \\ \hline
\end{tabular}
\end{center}

\section{Finding More Theorems}
\label{sec:find2}
\input{Rules/document/find2.tex}


\section{Forward Proof: Transforming Theorems}\label{sec:forward}

\index{forward proof|(}%
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 thus found.  Forward
proof is particularly good for reasoning from the general
to the specific.  For example, consider this distributive law for
the greatest common divisor:
\[ 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; 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{Modifying a Theorem using {\tt\slshape of},  {\tt\slshape where}
 and {\tt\slshape THEN}}

\label{sec:THEN}

Let us reproduce our examples in Isabelle.  Recall that in
{\S}\ref{sec:fun-simplification} we declared the recursive function
\isa{gcd}:\index{*gcd (constant)|(}
\begin{isabelle}
\isacommand{fun}\ gcd\ ::\ "nat\ \isasymRightarrow \ nat\ \isasymRightarrow \ nat"\ \isakeyword{where}\isanewline
\ \ "gcd\ m\ n\ =\ (if\ n=0\ then\ m\ else\ gcd\ n\ (m\ mod\ n))"
\end{isabelle}
%
From this definition, it is possible to prove the distributive law.  
That takes us to the starting point for our example.
\begin{isabelle}
?k\ *\ gcd\ ?m\ ?n\ =\ gcd\ (?k\ *\ ?m)\ (?k\ *\ ?n)
\rulename{gcd_mult_distrib2}
\end{isabelle}
%
The first step in our derivation is to replace \isa{?m} by~1.  We instantiate the
theorem using~\attrdx{of}, which identifies variables in order of their
appearance from left to right.  In this case, the variables  are \isa{?k}, \isa{?m}
and~\isa{?n}. So, the expression
\hbox{\texttt{[of k 1]}} replaces \isa{?k} by~\isa{k} and \isa{?m}
by~\isa{1}.
\begin{isabelle}
\isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1]
\end{isabelle}
%
The keyword \commdx{lemmas} declares a new theorem, which can be derived
from an existing one using attributes such as \isa{[of~k~1]}.
The command 
\isa{thm gcd_mult_0}
displays the result:
\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.  

An equivalent solution is to use the attribute \isa{where}. 
\begin{isabelle}
\ \ \ \ \ gcd\_mult\_distrib2\ [where\ m=1]
\end{isabelle}
While \isa{of} refers to
variables by their position, \isa{where} refers to variables by name. Multiple
instantiations are separated by~\isa{and}, as in this example:
\begin{isabelle}
\ \ \ \ \ gcd\_mult\_distrib2\ [where\ m=1\ and\ k=1]
\end{isabelle}

We now continue the present example with the version of \isa{gcd_mult_0}
shown above, which has \isa{k} instead of \isa{?k}.
Once we have replaced \isa{?m} by~1, we must next simplify
the theorem \isa{gcd_mult_0}, performing the steps 
$\gcd(1,n)=1$ and $k\times1=k$.  The \attrdx{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%
\rulenamedx{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}\indexbold{*THEN (attribute)} 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.  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%
\rulenamedx{iffD1}%
\isanewline
\isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
\rulenamedx{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:\index{*gcd (constant)|)}
\begin{isabelle}
\isacommand{lemma}\ gcd\_self\ [simp]:\ "gcd\ k\ k\ =\ k"\isanewline
\isacommand{by}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified])
\end{isabelle}

\begin{warn}
To give~\isa{of} a nonatomic term, enclose it in quotation marks, as in
\isa{[of "k*m"]}.  The term must not contain unknowns: an
attribute such as 
\isa{[of "?k*m"]} will be rejected.
\end{warn}

%Answer is now included in that section! Is a modified version of this
%  exercise worth including? E.g. find a difference between the two ways
%  of substituting.
%\begin{exercise}
%In {\S}\ref{sec:subst} the method \isa{subst\ mult_commute} was applied.  How
%can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}?
%% answer  rule (mult_commute [THEN ssubst])
%\end{exercise}

\subsection{Modifying a Theorem using {\tt\slshape OF}}

\index{*OF (attribute)|(}%
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.  

We again need the divides relation\index{divides relation} of number theory, which
as we recall is defined by 
\begin{isabelle}
?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
\rulename{dvd_def}
\end{isabelle}
%
Suppose, for example, that we have proved the following rule.  
It states that if $k$ and $n$ are relatively prime
and if $k$ divides $m\times n$ then $k$ divides $m$.
\begin{isabelle}
\isasymlbrakk gcd ?k ?n {=} 1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\
\isasymLongrightarrow\ ?k\ dvd\ ?m
\rulename{relprime_dvd_mult}
\end{isabelle}
We can use \isa{OF} to create an instance of this rule.
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 involving recursive functions is not
guaranteed to terminate, and it can be slow; Isabelle
performs arithmetic by  rewriting symbolic bit strings.  Here,
however, the simplification takes less than one second.  We can
give this new lemma to \isa{OF}.  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.%
\index{*OF (attribute)|)}

Here is a summary of some primitives for forward reasoning:
\begin{itemize}
\item \attrdx{of} instantiates the variables of a rule to a list of terms
\item \attrdx{OF} applies a rule to a list of theorems
\item \attrdx{THEN} gives a theorem to a named rule and returns the
conclusion 
%\item \attrdx{rule_format} puts a theorem into standard form
%  by removing \isa{\isasymlongrightarrow} and~\isa{\isasymforall}
\item \attrdx{simplified} applies the simplifier to a theorem
\item \isacommand{lemmas} assigns a name to the theorem produced by the
attributes above
\end{itemize}


\section{Forward Reasoning in a Backward 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.  We shall also meet some new methods that perform forward
reasoning.  

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%
\rulenamedx{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\ notI)\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)}:\index{*drule_tac (method)}
\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}

\subsection{The Method {\tt\slshape insert}}

\index{*insert (method)|(}%
The \isa{insert} method
inserts a given theorem as a new assumption of all subgoals.  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 subgoals.

For example, consider this theorem about the divides relation.  The first
proof step 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
\isaindent{\ 1.\ }\isasymLongrightarrow \ k\ dvd\ m%
\end{isabelle}
The next proof step utilizes the assumption \isa{gcd\ k\ n\ =\ 1}
(note that \isa{Suc\ 0} is another expression for 1):
\begin{isabelle}
\isacommand{apply}(simp)\isanewline
\ 1.\ \isasymlbrakk gcd\ k\ n\ =\ Suc\ 0;\ k\ dvd\ m\ *\ n;\ m\ =\ gcd\ (m\ *\ k)\ (m\ *\ n)\isasymrbrakk \isanewline
\isaindent{\ 1.\ }\isasymLongrightarrow \ k\ dvd\ m%
\end{isabelle}
Simplification has yielded an equation for~\isa{m}.  The rest of the proof
is omitted.

\medskip
Here is another demonstration of \isa{insert}.  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 \isa{(m\ *\ n)\ div\ n\ *\ n\ =\ m\ *\ n}, proving the
theorem.

\begin{warn}
Any unknowns in the theorem given to \methdx{insert} will be universally
quantified in the new assumption.
\end{warn}%
\index{*insert (method)|)}

\subsection{The Method {\tt\slshape subgoal_tac}}

\index{*subgoal_tac (method)}%
A related method is \isa{subgoal_tac}, but 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 gives the proof 
some structure.  If you find yourself generating a complex assumption by a
long series of forward steps, consider using \isa{subgoal_tac} instead: you can
state the formula you are aiming for, and perhaps prove it automatically.

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}
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 \methdx{insert} adds a theorem as a new assumption
\item \methdx{subgoal_tac} adds a formula as a new assumption and leaves the
subgoal of proving that formula
\end{itemize}
\index{forward proof|)}


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

\index{tacticals|(}%
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+)\index{*"+ (tactical)}
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
% we must use ?? rather than "| as the sorting item because somehow the presence
% of | (even quoted) stops hyperref from putting |hyperpage at the end of the index
% entry.
bar~(\isa|)\index{??@\texttt{"|} (tactical)}  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?)\index{*"? (tactical)} 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 can be valuable
within other control structures; for example, 
\isa{($m$+)?} performs zero or more repetitions of method~$m$.%
\index{tacticals|)}


\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 
\commdx{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}
\ 1.\ hard\isanewline
\ 2.\ \isasymnot \ \isasymnot \ P\ \isasymLongrightarrow \ P\isanewline
\ 3.\ Q\ \isasymLongrightarrow \ Q%
\end{isabelle}
%
The \commdx{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 \commdx{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}
Explain the use of \isa? and \isa+ in this proof.
\begin{isabelle}
\isacommand{lemma}\ "\isasymlbrakk P\isasymand Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ R"\isanewline
\isacommand{by}\ (drule\ mp,\ (intro conjI)?,\ assumption+)+
\end{isabelle}
\end{exercise}



\section{Proving the Correctness of Euclid's Algorithm}
\label{sec:proving-euclid}

\index{Euclid's algorithm|(}\index{*gcd (constant)|(}\index{divides relation|(}%
A brief development will demonstrate the techniques of this chapter,
including \isa{blast} applied with additional rules.  We shall also see
\isa{case_tac} used to perform a Boolean case split.

Let us prove that \isa{gcd} computes the greatest common
divisor of its two arguments.  
%
We use induction: \isa{gcd.induct} is the
induction rule returned by \isa{fun}.  We simplify using
rules proved in {\S}\ref{sec:fun-simplification}, since rewriting by the
definition of \isa{gcd} can loop.
\begin{isabelle}
\isacommand{lemma}\ gcd\_dvd\_both:\ "(gcd\ m\ n\ dvd\ m)\ \isasymand \ (gcd\ m\ n\ dvd\ n)"
\end{isabelle}
The induction formula must be a conjunction.  In the
inductive step, each conjunct establishes the other. 
\begin{isabelle}
\ 1.\ \isasymAnd m\ n.\ (n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
\isaindent{\ 1.\ \isasymAnd m\ n.\ (}gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \isanewline
\isaindent{\ 1.\ \isasymAnd m\ n.\ (}gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n)\ \isasymLongrightarrow \isanewline
\isaindent{\ 1.\ \isasymAnd m\ n.\ }gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n%
\end{isabelle}

The conditional induction hypothesis suggests doing a case
analysis on \isa{n=0}.  We apply \methdx{case_tac} with type
\isa{bool} --- and not with a datatype, as we have done until now.  Since
\isa{nat} is a datatype, we could have written
\isa{case_tac~n} instead of \isa{case_tac~"n=0"}.  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.
\begin{isabelle}
\isacommand{apply}\ (case_tac\ "n=0")\isanewline
\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
\isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline
\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n\isanewline
\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk \isanewline
\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n%
\end{isabelle}
%
Simplification leaves one subgoal: 
\begin{isabelle}
\isacommand{apply}\ (simp_all)\isanewline
\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
\isaindent{\ 1.\ \isasymAnd m\ n.\ \ }0\ <\ n\isasymrbrakk \isanewline
\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ n\ (m\ mod\ n)\ dvd\ m%
\end{isabelle}
%
Here, we can use \isa{blast}.  
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.  
\begin{isabelle}
\isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline
\isacommand{done}
\end{isabelle}
Attaching the \attrdx{dest} attribute to \isa{dvd_mod_imp_dvd} tells
\isa{blast} to use it as destruction rule; that is, 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}
Here we see \commdx{lemmas}
used with the \attrdx{iff} attribute, which supplies the new theorems to the
classical reasoner and the simplifier.  Recall that \attrdx{THEN} is
frequently used with destruction rules; \isa{THEN conjunct1} extracts the
first half of a conjunctive theorem.  Given \isa{gcd_dvd_both} it yields
\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"
\end{isabelle}
%
The goal is 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 eventual theorem.  This directive can also remove outer
universal quantifiers, converting the theorem into the usual format for
inference rules.  It can replace any series of applications of
\isa{THEN} to the rules \isa{mp} and \isa{spec}.  We did not have to
write this:
\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}

Because we are again reasoning about \isa{gcd}, we perform the same
induction and case analysis as in the previous proof:
\begingroup\samepage
\begin{isabelle}
\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ n\ (m\ mod\ n);\isanewline
\isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline
\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n\isanewline
\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ n\ (m\ mod\ n);\isanewline
\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk \isanewline
\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n%
\end{isabelle}
\endgroup

\noindent Simplification proves both subgoals. 
\begin{isabelle}
\isacommand{apply}\ (simp_all\ add:\ dvd_mod)\isanewline
\isacommand{done}
\end{isabelle}
In the first, where \isa{n=0}, the implication becomes trivial: \isa{k\ dvd\
gcd\ m\ n} goes to~\isa{k\ dvd\ m}.  The second subgoal is proved by
an unfolding of \isa{gcd}, using this rule about divides:
\begin{isabelle}
\isasymlbrakk ?f\ dvd\ ?m;\ ?f\ dvd\ ?n\isasymrbrakk \
\isasymLongrightarrow \ ?f\ dvd\ ?m\ mod\ ?n%
\rulename{dvd_mod}
\end{isabelle}


\medskip
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}.
\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}.%
\index{Euclid's algorithm|)}\index{*gcd (constant)|)}\index{divides relation|)}