--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/rules.tex Tue Aug 28 14:37:57 2012 +0200
@@ -0,0 +1,2641 @@
+%!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{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|)}