doc-src/TutorialI/Rules/rules.tex

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