--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Intro/getting.tex Wed Nov 10 05:06:55 1993 +0100
@@ -0,0 +1,896 @@
+%% $Id$
+\part{Getting started with Isabelle}
+This Part describes how to perform simple proofs using Isabelle. Although
+it frequently refers to concepts from the previous Part, a user can get
+started without understanding them in detail.
+
+As of this writing, Isabelle's user interface is \ML. Proofs are conducted
+by applying certain \ML{} functions, which update a stored proof state.
+Logics are combined and extended by calling \ML{} functions. All syntax
+must be expressed using {\sc ascii} characters. Menu-driven graphical
+interfaces are under construction, but Isabelle users will always need to
+know some \ML, at least to use tacticals.
+
+Object-logics are built upon Pure Isabelle, which implements the meta-logic
+and provides certain fundamental data structures: types, terms, signatures,
+theorems and theories, tactics and tacticals. These data structures have
+the corresponding \ML{} types {\tt typ}, {\tt term}, {\tt Sign.sg}, {\tt thm},
+{\tt theory} and {\tt tactic}; tacticals have function types such as {\tt
+tactic->tactic}. Isabelle users can operate on these data structures by
+writing \ML{} programs.
+
+\section{Forward proof}
+\index{Isabelle!getting started}\index{ML}
+This section describes the concrete syntax for types, terms and theorems,
+and demonstrates forward proof.
+
+\subsection{Lexical matters}
+\index{identifiers|bold}\index{reserved words|bold}
+An {\bf identifier} is a string of letters, digits, underscores~(\verb|_|)
+and single quotes~({\tt'}), beginning with a letter. Single quotes are
+regarded as primes; for instance {\tt x'} is read as~$x'$. Identifiers are
+separated by white space and special characters. {\bf Reserved words} are
+identifiers that appear in Isabelle syntax definitions.
+
+An Isabelle theory can declare symbols composed of special characters, such
+as {\tt=}, {\tt==}, {\tt=>} and {\tt==>}. (The latter three are part of
+the syntax of the meta-logic.) Such symbols may be run together; thus if
+\verb|}| and \verb|{| are used for set brackets then \verb|{{a},{a,b}}| is
+valid notation for a set of sets --- but only if \verb|}}| and \verb|{{|
+have not been declared as symbols! The parser resolves any ambiguity by
+taking the longest possible symbol that has been declared. Thus the string
+{\tt==>} is read as a single symbol. But \hbox{\tt= =>} is read as two
+symbols, as is \verb|}}|, as discussed above.
+
+Identifiers that are not reserved words may serve as free variables or
+constants. A type identifier consists of an identifier prefixed by a
+prime, for example {\tt'a} and \hbox{\tt'hello}. An unknown (or type
+unknown) consists of a question mark, an identifier (or type identifier),
+and a subscript. The subscript, a non-negative integer, allows the
+renaming of unknowns prior to unification.
+
+The subscript may appear after the identifier, separated by a dot; this
+prevents ambiguity when the identifier ends with a digit. Thus {\tt?z6.0}
+has identifier \verb|"z6"| and subscript~0, while {\tt?a0.5} has identifier
+\verb|"a0"| and subscript~5. If the identifier does not end with a digit,
+then no dot appears and a subscript of~0 is omitted; for example,
+{\tt?hello} has identifier \verb|"hello"| and subscript zero, while
+{\tt?z6} has identifier \verb|"z"| and subscript~6. The same conventions
+apply to type unknowns. Note that the question mark is {\bf not} part of the
+identifier!
+
+
+\subsection{Syntax of types and terms}
+\index{Isabelle!syntax of}
+\index{classes!built-in|bold}
+Classes are denoted by identifiers; the built-in class \ttindex{logic}
+contains the `logical' types. Sorts are lists of classes enclosed in
+braces~\{ and \}; singleton sorts may be abbreviated by dropping the braces.
+
+\index{types!syntax|bold}
+Types are written with a syntax like \ML's. The built-in type \ttindex{prop}
+is the type of propositions. Type variables can be constrained to particular
+classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\{ord,arith\}}.
+\[\dquotes
+\begin{array}{lll}
+ \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline
+ t "::" C & t :: C & \hbox{class constraint} \\
+ t "::" "\{" C@1 "," \ldots "," C@n "\}" &
+ t :: \{C@1,\dots,C@n\} & \hbox{sort constraint} \\
+ \sigma"=>"\tau & \sigma\To\tau & \hbox{function type} \\
+ "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau &
+ [\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\
+ "(" \tau@1"," \ldots "," \tau@n ")" tycon &
+ (\tau@1, \ldots, \tau@n)tycon & \hbox{type construction}
+\end{array}
+\]
+Terms are those of the typed $\lambda$-calculus.
+\index{terms!syntax|bold}
+\[\dquotes
+\begin{array}{lll}
+ \multicolumn{3}{c}{\hbox{ASCII Notation for Terms}} \\ \hline
+ t "::" \sigma & t :: \sigma & \hbox{type constraint} \\
+ "\%" x "." t & \lambda x.t & \hbox{abstraction} \\
+ "\%" x@1\ldots x@n "." t & \lambda x@1\ldots x@n.t &
+ \hbox{curried abstraction} \\
+ t "(" u@1"," \ldots "," u@n ")" &
+ t (u@1, \ldots, u@n) & \hbox{curried application}
+\end{array}
+\]
+The theorems and rules of an object-logic are represented by theorems in
+the meta-logic, which are expressed using meta-formulae. Since the
+meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{}
+are just terms of type~\ttindex{prop}.
+\index{meta-formulae!syntax|bold}
+\[\dquotes
+ \begin{array}{l@{\quad}l@{\quad}l}
+ \multicolumn{3}{c}{\hbox{ASCII Notation for Meta-Formulae}} \\ \hline
+ a " == " b & a\equiv b & \hbox{meta-equality} \\
+ a " =?= " b & a\qeq b & \hbox{flex-flex constraint} \\
+ \phi " ==> " \psi & \phi\Imp \psi & \hbox{meta-implication} \\
+ "[|" \phi@1 ";" \ldots ";" \phi@n "|] ==> " \psi &
+ \List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\
+ "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\
+ "!!" x@1\ldots x@n "." \phi &
+ \Forall x@1. \ldots \Forall x@n.\phi & \hbox{nested quantification}
+ \end{array}
+\]
+Flex-flex constraints are meta-equalities arising from unification; they
+require special treatment. See~\S\ref{flexflex}.
+\index{flex-flex equations}
+
+Most logics define the implicit coercion $Trueprop$ from object-formulae to
+propositions.
+\index{Trueprop@{$Trueprop$}}
+This could cause an ambiguity: in $P\Imp Q$, do the variables $P$ and $Q$
+stand for meta-formulae or object-formulae? If the latter, $P\Imp Q$
+really abbreviates $Trueprop(P)\Imp Trueprop(Q)$. To prevent such
+ambiguities, Isabelle's syntax does not allow a meta-formula to consist of
+a variable. Variables of type~\ttindex{prop} are seldom useful, but you
+can make a variable stand for a meta-formula by prefixing it with the
+keyword \ttindex{PROP}:
+\begin{ttbox}
+PROP ?psi ==> PROP ?theta
+\end{ttbox}
+
+Symbols of object-logics also must be rendered into {\sc ascii}, typically
+as follows:
+\[ \begin{tabular}{l@{\quad}l@{\quad}l}
+ \tt True & $\top$ & true \\
+ \tt False & $\bot$ & false \\
+ \tt $P$ \& $Q$ & $P\conj Q$ & conjunction \\
+ \tt $P$ | $Q$ & $P\disj Q$ & disjunction \\
+ \verb'~' $P$ & $\neg P$ & negation \\
+ \tt $P$ --> $Q$ & $P\imp Q$ & implication \\
+ \tt $P$ <-> $Q$ & $P\bimp Q$ & bi-implication \\
+ \tt ALL $x\,y\,z$ .\ $P$ & $\forall x\,y\,z.P$ & for all \\
+ \tt EX $x\,y\,z$ .\ $P$ & $\exists x\,y\,z.P$ & there exists
+ \end{tabular}
+\]
+To illustrate the notation, consider two axioms for first-order logic:
+$$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$
+$$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$
+Using the {\tt [|\ldots|]} shorthand, $({\conj}I)$ translates literally into
+{\sc ascii} characters as
+\begin{ttbox}
+[| ?P; ?Q |] ==> ?P & ?Q
+\end{ttbox}
+The schematic variables let unification instantiate the rule. To
+avoid cluttering rules with question marks, Isabelle converts any free
+variables in a rule to schematic variables; we normally write $({\conj}I)$ as
+\begin{ttbox}
+[| P; Q |] ==> P & Q
+\end{ttbox}
+This variables convention agrees with the treatment of variables in goals.
+Free variables in a goal remain fixed throughout the proof. After the
+proof is finished, Isabelle converts them to scheme variables in the
+resulting theorem. Scheme variables in a goal may be replaced by terms
+during the proof, supporting answer extraction, program synthesis, and so
+forth.
+
+For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as
+\begin{ttbox}
+[| EX x.P(x); !!x. P(x) ==> Q |] ==> Q
+\end{ttbox}
+
+
+\subsection{Basic operations on theorems}
+\index{theorems!basic operations on|bold}
+\index{LCF}
+Meta-level theorems have type \ttindex{thm} and represent the theorems and
+inference rules of object-logics. Isabelle's meta-logic is implemented
+using the {\sc lcf} approach: each meta-level inference rule is represented by
+a function from theorems to theorems. Object-level rules are taken as
+axioms.
+
+The main theorem printing commands are {\tt prth}, {\tt prths} and~{\tt
+ prthq}. Of the other operations on theorems, most useful are {\tt RS}
+and {\tt RSN}, which perform resolution.
+
+\index{printing commands|bold}
+\begin{description}
+\item[\ttindexbold{prth} {\it thm}] pretty-prints {\it thm\/} at the terminal.
+
+\item[\ttindexbold{prths} {\it thms}] pretty-prints {\it thms}, a list of
+theorems.
+
+\item[\ttindexbold{prthq} {\it thmq}] pretty-prints {\it thmq}, a sequence of
+theorems; this is useful for inspecting the output of a tactic.
+
+\item[\tt$thm1$ RS $thm2$] \indexbold{*RS} resolves the conclusion of $thm1$
+with the first premise of~$thm2$.
+
+\item[\tt$thm1$ RSN $(i,thm2)$] \indexbold{*RSN} resolves the conclusion of $thm1$
+with the $i$th premise of~$thm2$.
+
+\item[\ttindexbold{standard} $thm$] puts $thm$ into a standard
+format. It also renames schematic variables to have subscript zero,
+improving readability and reducing subscript growth.
+\end{description}
+\index{ML}
+The rules of a theory are normally bound to \ML\ identifiers. Suppose we
+are running an Isabelle session containing natural deduction first-order
+logic. Let us try an example given in~\S\ref{joining}. We first print
+\ttindex{mp}, which is the rule~$({\imp}E)$, then resolve it with itself.
+\begin{ttbox}
+prth mp;
+{\out [| ?P --> ?Q; ?P |] ==> ?Q}
+{\out val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm}
+prth (mp RS mp);
+{\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q}
+{\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm}
+\end{ttbox}
+In the Isabelle documentation, user's input appears in {\tt typewriter
+ characters}, and output appears in {\sltt slanted typewriter characters}.
+\ML's response {\out val }~\ldots{} is compiler-dependent and will
+sometimes be suppressed. This session illustrates two formats for the
+display of theorems. Isabelle's top-level displays theorems as ML values,
+enclosed in quotes.\footnote{This works under both Poly/ML and Standard ML
+ of New Jersey.} Printing functions like {\tt prth} omit the quotes and
+the surrounding {\tt val \ldots :\ thm}.
+
+To contrast {\tt RS} with {\tt RSN}, we resolve
+\ttindex{conjunct1}, which stands for~$(\conj E1)$, with~\ttindex{mp}.
+\begin{ttbox}
+conjunct1 RS mp;
+{\out val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm}
+conjunct1 RSN (2,mp);
+{\out val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm}
+\end{ttbox}
+These correspond to the following proofs:
+\[ \infer[({\imp}E)]{Q}{\infer[({\conj}E1)]{P\imp Q}{(P\imp Q)\conj Q@1} & P}
+ \qquad
+ \infer[({\imp}E)]{Q}{P\imp Q & \infer[({\conj}E1)]{P}{P\conj Q@1}}
+\]
+The printing commands return their argument; the \ML{} identifier~{\tt it}
+denotes the value just printed. You may derive a rule by pasting other
+rules together. Below, \ttindex{spec} stands for~$(\forall E)$:
+\begin{ttbox}
+spec;
+{\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm}
+it RS mp;
+{\out val it = "[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==> ?Q2(?x1)" : thm}
+it RS conjunct1;
+{\out val it = "[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==> ?P6(?x2)"}
+standard it;
+{\out val it = "[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==> ?Pa(?x)"}
+\end{ttbox}
+By resolving $(\forall E)$ with (${\imp}E)$ and (${\conj}E1)$, we have
+derived a destruction rule for formulae of the form $\forall x.
+P(x)\imp(Q(x)\conj R(x))$. Used with destruct-resolution, such specialized
+rules provide a way of referring to particular assumptions.
+
+\subsection{Flex-flex equations} \label{flexflex}
+\index{flex-flex equations|bold}\index{unknowns!of function type}
+In higher-order unification, {\bf flex-flex} equations are those where both
+sides begin with a function unknown, such as $\Var{f}(0)\qeq\Var{g}(0)$.
+They admit a trivial unifier, here $\Var{f}\equiv \lambda x.\Var{a}$ and
+$\Var{g}\equiv \lambda y.\Var{a}$, where $\Var{a}$ is a new unknown. They
+admit many other unifiers, such as $\Var{f} \equiv \lambda x.\Var{g}(0)$
+and $\{\Var{f} \equiv \lambda x.x,\, \Var{g} \equiv \lambda x.0\}$. Huet's
+procedure does not enumerate the unifiers; instead, it retains flex-flex
+equations as constraints on future unifications. Flex-flex constraints
+occasionally become attached to a proof state; more frequently, they appear
+during use of {\tt RS} and~{\tt RSN}:
+\begin{ttbox}
+refl;
+{\out val it = "?a = ?a" : thm}
+exI;
+{\out val it = "?P(?x) ==> EX x. ?P(x)" : thm}
+refl RS exI;
+{\out val it = "?a3(?x) =?= ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)" : thm}
+\end{ttbox}
+
+\noindent
+Renaming variables, this is $\exists x.\Var{f}(x)=\Var{g}(x)$ with
+the constraint ${\Var{f}(\Var{u})\qeq\Var{g}(\Var{u})}$. Instances
+satisfying the constraint include $\exists x.\Var{f}(x)=\Var{f}(x)$ and
+$\exists x.x=\Var{u}$. Calling \ttindex{flexflex_rule} removes all
+constraints by applying the trivial unifier:\index{*prthq}
+\begin{ttbox}
+prthq (flexflex_rule it);
+{\out EX x. ?a4 = ?a4}
+\end{ttbox}
+Isabelle simplifies flex-flex equations to eliminate redundant bound
+variables. In $\lambda x\,y.\Var{f}(k(y),x) \qeq \lambda x\,y.\Var{g}(y)$,
+there is no bound occurrence of~$x$ on the right side; thus, there will be
+none on the left, in a common instance of these terms. Choosing a new
+variable~$\Var{h}$, Isabelle assigns $\Var{f}\equiv \lambda u\,v.?h(u)$,
+simplifying the left side to $\lambda x\,y.\Var{h}(k(y))$. Dropping $x$
+from the equation leaves $\lambda y.\Var{h}(k(y)) \qeq \lambda
+y.\Var{g}(y)$. By $\eta$-conversion, this simplifies to the assignment
+$\Var{g}\equiv\lambda y.?h(k(y))$.
+
+\begin{warn}
+\ttindex{RS} and \ttindex{RSN} fail (by raising exception {\tt THM}) unless
+the resolution delivers {\bf exactly one} resolvent. For multiple results,
+use \ttindex{RL} and \ttindex{RLN}, which operate on theorem lists. The
+following example uses \ttindex{read_instantiate} to create an instance
+of \ttindex{refl} containing no schematic variables.
+\begin{ttbox}
+val reflk = read_instantiate [("a","k")] refl;
+{\out val reflk = "k = k" : thm}
+\end{ttbox}
+
+\noindent
+A flex-flex constraint is no longer possible; resolution does not find a
+unique unifier:
+\begin{ttbox}
+reflk RS exI;
+{\out uncaught exception THM}
+\end{ttbox}
+Using \ttindex{RL} this time, we discover that there are four unifiers, and
+four resolvents:
+\begin{ttbox}
+[reflk] RL [exI];
+{\out val it = ["EX x. x = x", "EX x. k = x",}
+{\out "EX x. x = k", "EX x. k = k"] : thm list}
+\end{ttbox}
+\end{warn}
+
+
+\section{Backward proof}
+Although {\tt RS} and {\tt RSN} are fine for simple forward reasoning,
+large proofs require tactics. Isabelle provides a suite of commands for
+conducting a backward proof using tactics.
+
+\subsection{The basic tactics}
+\index{tactics!basic|bold}
+The tactics {\tt assume_tac}, {\tt
+resolve_tac}, {\tt eresolve_tac}, and {\tt dresolve_tac} suffice for most
+single-step proofs. Although {\tt eresolve_tac} and {\tt dresolve_tac} are
+not strictly necessary, they simplify proofs involving elimination and
+destruction rules. All the tactics act on a subgoal designated by a
+positive integer~$i$, failing if~$i$ is out of range. The resolution
+tactics try their list of theorems in left-to-right order.
+
+\begin{description}
+\item[\ttindexbold{assume_tac} {\it i}] is the tactic that attempts to solve
+subgoal~$i$ by assumption. Proof by assumption is not a trivial step; it
+can falsify other subgoals by instantiating shared variables. There may be
+several ways of solving the subgoal by assumption.
+
+\item[\ttindexbold{resolve_tac} {\it thms} {\it i}]
+is the basic resolution tactic, used for most proof steps. The $thms$
+represent object-rules, which are resolved against subgoal~$i$ of the proof
+state. For each rule, resolution forms next states by unifying the
+conclusion with the subgoal and inserting instantiated premises in its
+place. A rule can admit many higher-order unifiers. The tactic fails if
+none of the rules generates next states.
+
+\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}]
+performs elim-resolution. Like
+\hbox{\tt resolve_tac {\it thms} {\it i}} followed by \hbox{\tt assume_tac
+{\it i}}, it applies a rule then solves its first premise by assumption.
+But {\tt eresolve_tac} additionally deletes that assumption from any
+subgoals arising from the resolution.
+
+
+\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}]
+performs destruct-resolution with the~$thms$, as described
+in~\S\ref{destruct}. It is useful for forward reasoning from the
+assumptions.
+\end{description}
+
+\subsection{Commands for backward proof}
+\index{proof!commands for|bold}
+Tactics are normally applied using the subgoal module, which maintains a
+proof state and manages the proof construction. It allows interactive
+backtracking through the proof space, going away to prove lemmas, etc.; of
+its many commands, most important are the following:
+\begin{description}
+\item[\ttindexbold{goal} {\it theory} {\it formula}; ]
+begins a new proof, where $theory$ is usually an \ML\ identifier
+and the {\it formula\/} is written as an \ML\ string.
+
+\item[\ttindexbold{by} {\it tactic}; ]
+applies the {\it tactic\/} to the current proof
+state, raising an exception if the tactic fails.
+
+\item[\ttindexbold{undo}(); ]
+reverts to the previous proof state. Undo can be repeated but cannot be
+undone. Do not omit the parentheses; typing {\tt undo;} merely causes \ML\
+to echo the value of that function.
+
+\item[\ttindexbold{result}()]
+returns the theorem just proved, in a standard format. It fails if
+unproved subgoals are left or if the main goal does not match the one you
+started with.
+\end{description}
+The commands and tactics given above are cumbersome for interactive use.
+Although our examples will use the full commands, you may prefer Isabelle's
+shortcuts:
+\begin{center} \tt
+\indexbold{*br} \indexbold{*be} \indexbold{*bd} \indexbold{*ba}
+\begin{tabular}{l@{\qquad\rm abbreviates\qquad}l}
+ ba {\it i}; & by (assume_tac {\it i}); \\
+
+ br {\it thm} {\it i}; & by (resolve_tac [{\it thm}] {\it i}); \\
+
+ be {\it thm} {\it i}; & by (eresolve_tac [{\it thm}] {\it i}); \\
+
+ bd {\it thm} {\it i}; & by (dresolve_tac [{\it thm}] {\it i});
+\end{tabular}
+\end{center}
+
+\subsection{A trivial example in propositional logic}
+\index{examples!propositional}
+Directory {\tt FOL} of the Isabelle distribution defines the \ML\
+identifier~\ttindex{FOL.thy}, which denotes the theory of first-order
+logic. Let us try the example from~\S\ref{prop-proof}, entering the goal
+$P\disj P\imp P$ in that theory.\footnote{To run these examples, see the
+file {\tt FOL/ex/intro.ML}.}
+\begin{ttbox}
+goal FOL.thy "P|P --> P";
+{\out Level 0}
+{\out P | P --> P}
+{\out 1. P | P --> P}
+\end{ttbox}
+Isabelle responds by printing the initial proof state, which has $P\disj
+P\imp P$ as the main goal and the only subgoal. The \bfindex{level} of the
+state is the number of {\tt by} commands that have been applied to reach
+it. We now use \ttindex{resolve_tac} to apply the rule \ttindex{impI},
+or~$({\imp}I)$, to subgoal~1:
+\begin{ttbox}
+by (resolve_tac [impI] 1);
+{\out Level 1}
+{\out P | P --> P}
+{\out 1. P | P ==> P}
+\end{ttbox}
+In the new proof state, subgoal~1 is $P$ under the assumption $P\disj P$.
+(The meta-implication {\tt==>} indicates assumptions.) We apply
+\ttindex{disjE}, or~(${\disj}E)$, to that subgoal:
+\begin{ttbox}
+by (resolve_tac [disjE] 1);
+{\out Level 2}
+{\out P | P --> P}
+{\out 1. P | P ==> ?P1 | ?Q1}
+{\out 2. [| P | P; ?P1 |] ==> P}
+{\out 3. [| P | P; ?Q1 |] ==> P}
+\end{ttbox}
+At Level~2 there are three subgoals, each provable by
+assumption. We deviate from~\S\ref{prop-proof} by tackling subgoal~3
+first, using \ttindex{assume_tac}. This updates {\tt?Q1} to~{\tt P}.
+\begin{ttbox}
+by (assume_tac 3);
+{\out Level 3}
+{\out P | P --> P}
+{\out 1. P | P ==> ?P1 | P}
+{\out 2. [| P | P; ?P1 |] ==> P}
+\end{ttbox}
+Next we tackle subgoal~2, instantiating {\tt?P1} to~{\tt P}.
+\begin{ttbox}
+by (assume_tac 2);
+{\out Level 4}
+{\out P | P --> P}
+{\out 1. P | P ==> P | P}
+\end{ttbox}
+Lastly we prove the remaining subgoal by assumption:
+\begin{ttbox}
+by (assume_tac 1);
+{\out Level 5}
+{\out P | P --> P}
+{\out No subgoals!}
+\end{ttbox}
+Isabelle tells us that there are no longer any subgoals: the proof is
+complete. Calling \ttindex{result} returns the theorem.
+\begin{ttbox}
+val mythm = result();
+{\out val mythm = "?P | ?P --> ?P" : thm}
+\end{ttbox}
+Isabelle has replaced the free variable~{\tt P} by the scheme
+variable~{\tt?P}\@. Free variables in the proof state remain fixed
+throughout the proof. Isabelle finally converts them to scheme variables
+so that the resulting theorem can be instantiated with any formula.
+
+
+\subsection{Proving a distributive law}
+\index{examples!propositional}
+To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac}
+and the tactical \ttindex{REPEAT}, we shall prove part of the distributive
+law $(P\conj Q)\disj R \iff (P\disj R)\conj (Q\disj R)$.
+
+We begin by stating the goal to Isabelle and applying~$({\imp}I)$ to it:
+\begin{ttbox}
+goal FOL.thy "(P & Q) | R --> (P | R)";
+{\out Level 0}
+{\out P & Q | R --> P | R}
+{\out 1. P & Q | R --> P | R}
+by (resolve_tac [impI] 1);
+{\out Level 1}
+{\out P & Q | R --> P | R}
+{\out 1. P & Q | R ==> P | R}
+\end{ttbox}
+Previously we applied~(${\disj}E)$ using {\tt resolve_tac}, but
+\ttindex{eresolve_tac} deletes the assumption after use. The resulting proof
+state is simpler.
+\begin{ttbox}
+by (eresolve_tac [disjE] 1);
+{\out Level 2}
+{\out P & Q | R --> P | R}
+{\out 1. P & Q ==> P | R}
+{\out 2. R ==> P | R}
+\end{ttbox}
+Using \ttindex{dresolve_tac}, we can apply~(${\conj}E1)$ to subgoal~1,
+replacing the assumption $P\conj Q$ by~$P$. Normally we should apply the
+rule~(${\conj}E)$, given in~\S\ref{destruct}. That is an elimination rule
+and requires {\tt eresolve_tac}; it would replace $P\conj Q$ by the two
+assumptions~$P$ and~$Q$. The present example does not need~$Q$.
+\begin{ttbox}
+by (dresolve_tac [conjunct1] 1);
+{\out Level 3}
+{\out P & Q | R --> P | R}
+{\out 1. P ==> P | R}
+{\out 2. R ==> P | R}
+\end{ttbox}
+The next two steps apply~(${\disj}I1$) and~(${\disj}I2$) in an obvious manner.
+\begin{ttbox}
+by (resolve_tac [disjI1] 1);
+{\out Level 4}
+{\out P & Q | R --> P | R}
+{\out 1. P ==> P}
+{\out 2. R ==> P | R}
+\ttbreak
+by (resolve_tac [disjI2] 2);
+{\out Level 5}
+{\out P & Q | R --> P | R}
+{\out 1. P ==> P}
+{\out 2. R ==> R}
+\end{ttbox}
+Two calls of~\ttindex{assume_tac} can finish the proof. The
+tactical~\ttindex{REPEAT} expresses a tactic that calls {\tt assume_tac~1}
+as many times as possible. We can restrict attention to subgoal~1 because
+the other subgoals move up after subgoal~1 disappears.
+\begin{ttbox}
+by (REPEAT (assume_tac 1));
+{\out Level 6}
+{\out P & Q | R --> P | R}
+{\out No subgoals!}
+\end{ttbox}
+
+
+\section{Quantifier reasoning}
+\index{quantifiers!reasoning about}\index{parameters}\index{unknowns}
+This section illustrates how Isabelle enforces quantifier provisos.
+Quantifier rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a
+function unknown and $x$ and~$z$ are parameters. This may be replaced by
+any term, possibly containing free occurrences of $x$ and~$z$.
+
+\subsection{Two quantifier proofs, successful and not}
+\index{examples!with quantifiers}
+Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an
+attempted proof of the non-theorem $\exists y.\forall x.x=y$. The former
+proof succeeds, and the latter fails, because of the scope of quantified
+variables~\cite{paulson89}. Unification helps even in these trivial
+proofs. In $\forall x.\exists y.x=y$ the $y$ that `exists' is simply $x$,
+but we need never say so. This choice is forced by the reflexive law for
+equality, and happens automatically.
+
+\subsubsection{The successful proof}
+The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules
+$(\forall I)$ and~$(\exists I)$. We state the goal and apply $(\forall I)$:
+\begin{ttbox}
+goal FOL.thy "ALL x. EX y. x=y";
+{\out Level 0}
+{\out ALL x. EX y. x = y}
+{\out 1. ALL x. EX y. x = y}
+\ttbreak
+by (resolve_tac [allI] 1);
+{\out Level 1}
+{\out ALL x. EX y. x = y}
+{\out 1. !!x. EX y. x = y}
+\end{ttbox}
+The variable~{\tt x} is no longer universally quantified, but is a
+parameter in the subgoal; thus, it is universally quantified at the
+meta-level. The subgoal must be proved for all possible values of~{\tt x}.
+We apply the rule $(\exists I)$:
+\begin{ttbox}
+by (resolve_tac [exI] 1);
+{\out Level 2}
+{\out ALL x. EX y. x = y}
+{\out 1. !!x. x = ?y1(x)}
+\end{ttbox}
+The bound variable {\tt y} has become {\tt?y1(x)}. This term consists of
+the function unknown~{\tt?y1} applied to the parameter~{\tt x}.
+Instances of {\tt?y1(x)} may or may not contain~{\tt x}. We resolve the
+subgoal with the reflexivity axiom.
+\begin{ttbox}
+by (resolve_tac [refl] 1);
+{\out Level 3}
+{\out ALL x. EX y. x = y}
+{\out No subgoals!}
+\end{ttbox}
+Let us consider what has happened in detail. The reflexivity axiom is
+lifted over~$x$ to become $\Forall x.\Var{f}(x)=\Var{f}(x)$, which is
+unified with $\Forall x.x=\Var{y@1}(x)$. The function unknowns $\Var{f}$
+and~$\Var{y@1}$ are both instantiated to the identity function, and
+$x=\Var{y@1}(x)$ collapses to~$x=x$ by $\beta$-reduction.
+
+\subsubsection{The unsuccessful proof}
+We state the goal $\exists y.\forall x.x=y$, which is {\bf not} a theorem, and
+try~$(\exists I)$:
+\begin{ttbox}
+goal FOL.thy "EX y. ALL x. x=y";
+{\out Level 0}
+{\out EX y. ALL x. x = y}
+{\out 1. EX y. ALL x. x = y}
+\ttbreak
+by (resolve_tac [exI] 1);
+{\out Level 1}
+{\out EX y. ALL x. x = y}
+{\out 1. ALL x. x = ?y}
+\end{ttbox}
+The unknown {\tt ?y} may be replaced by any term, but this can never
+introduce another bound occurrence of~{\tt x}. We now apply~$(\forall I)$:
+\begin{ttbox}
+by (resolve_tac [allI] 1);
+{\out Level 2}
+{\out EX y. ALL x. x = y}
+{\out 1. !!x. x = ?y}
+\end{ttbox}
+Compare our position with the previous Level~2. Instead of {\tt?y1(x)} we
+have~{\tt?y}, whose instances may not contain the bound variable~{\tt x}.
+The reflexivity axiom does not unify with subgoal~1.
+\begin{ttbox}
+by (resolve_tac [refl] 1);
+{\out by: tactic returned no results}
+\end{ttbox}
+No other choice of rules seems likely to complete the proof. Of course,
+this is no guarantee that Isabelle cannot prove $\exists y.\forall x.x=y$
+or other invalid assertions. We must appeal to the soundness of
+first-order logic and the faithfulness of its encoding in
+Isabelle~\cite{paulson89}, and must trust the implementation.
+
+
+\subsection{Nested quantifiers}
+\index{examples!with quantifiers}
+Multiple quantifiers create complex terms. Proving $(\forall x\,y.P(x,y))
+\imp (\forall z\,w.P(w,z))$, will demonstrate how parameters and
+unknowns develop. If they appear in the wrong order, the proof will fail.
+This section concludes with a demonstration of {\tt REPEAT}
+and~{\tt ORELSE}.
+
+The start of the proof is routine.
+\begin{ttbox}
+goal FOL.thy "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))";
+{\out Level 0}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+\ttbreak
+by (resolve_tac [impI] 1);
+{\out Level 1}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}
+\end{ttbox}
+
+\subsubsection{The wrong approach}
+Using \ttindex{dresolve_tac}, we apply the rule $(\forall E)$, bound to the
+\ML\ identifier \ttindex{spec}. Then we apply $(\forall I)$.
+\begin{ttbox}
+by (dresolve_tac [spec] 1);
+{\out Level 2}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out 1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)}
+\ttbreak
+by (resolve_tac [allI] 1);
+{\out Level 3}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out 1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)}
+\end{ttbox}
+The unknown {\tt ?u} and the parameter {\tt z} have appeared. We again
+apply $(\forall I)$ and~$(\forall E)$.
+\begin{ttbox}
+by (dresolve_tac [spec] 1);
+{\out Level 4}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out 1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)}
+\ttbreak
+by (resolve_tac [allI] 1);
+{\out Level 5}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out 1. !!z w. P(?x1,?y3(z)) ==> P(w,z)}
+\end{ttbox}
+The unknown {\tt ?y3} and the parameter {\tt w} have appeared. Each
+unknown is applied to the parameters existing at the time of its creation;
+instances of {\tt ?x1} cannot contain~{\tt z} or~{\tt w}, while instances
+of {\tt?y3(z)} can only contain~{\tt z}. Because of these restrictions,
+proof by assumption will fail.
+\begin{ttbox}
+by (assume_tac 1);
+{\out by: tactic returned no results}
+{\out uncaught exception ERROR}
+\end{ttbox}
+
+\subsubsection{The right approach}
+To do this proof, the rules must be applied in the correct order.
+Eigenvariables should be created before unknowns. The
+\ttindex{choplev} command returns to an earlier stage of the proof;
+let us return to the result of applying~$({\imp}I)$:
+\begin{ttbox}
+choplev 1;
+{\out Level 1}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}
+\end{ttbox}
+Previously, we made the mistake of applying $(\forall E)$; this time, we
+apply $(\forall I)$ twice.
+\begin{ttbox}
+by (resolve_tac [allI] 1);
+{\out Level 2}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out 1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)}
+\ttbreak
+by (resolve_tac [allI] 1);
+{\out Level 3}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out 1. !!z w. ALL x y. P(x,y) ==> P(w,z)}
+\end{ttbox}
+The parameters {\tt z} and~{\tt w} have appeared. We now create the
+unknowns:
+\begin{ttbox}
+by (dresolve_tac [spec] 1);
+{\out Level 4}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out 1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)}
+\ttbreak
+by (dresolve_tac [spec] 1);
+{\out Level 5}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out 1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)}
+\end{ttbox}
+Both {\tt?x3(z,w)} and~{\tt?y4(z,w)} could become any terms containing {\tt
+z} and~{\tt w}:
+\begin{ttbox}
+by (assume_tac 1);
+{\out Level 6}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out No subgoals!}
+\end{ttbox}
+
+\subsubsection{A one-step proof using tacticals}
+\index{tacticals}
+\index{examples!of tacticals}
+Repeated application of rules can be an effective theorem-proving
+procedure, but the rules should be attempted in an order that delays the
+creation of unknowns. As we have just seen, \ttindex{allI} should be
+attempted before~\ttindex{spec}, while \ttindex{assume_tac} generally can
+be attempted first. Such priorities can easily be expressed
+using~\ttindex{ORELSE}, and repeated using~\ttindex{REPEAT}. Let us return
+to the original goal using \ttindex{choplev}:
+\begin{ttbox}
+choplev 0;
+{\out Level 0}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+\end{ttbox}
+A repetitive procedure proves it:
+\begin{ttbox}
+by (REPEAT (assume_tac 1
+ ORELSE resolve_tac [impI,allI] 1
+ ORELSE dresolve_tac [spec] 1));
+{\out Level 1}
+{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
+{\out No subgoals!}
+\end{ttbox}
+
+
+\subsection{A realistic quantifier proof}
+\index{examples!with quantifiers}
+A proof of $(\forall x. P(x) \imp Q) \imp (\exists x. P(x)) \imp Q$
+demonstrates the practical use of parameters and unknowns.
+Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we
+use \ttindex{REPEAT}:
+\begin{ttbox}
+goal FOL.thy "(ALL x.P(x) --> Q) --> (EX x.P(x)) --> Q";
+{\out Level 0}
+{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
+{\out 1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
+\ttbreak
+by (REPEAT (resolve_tac [impI] 1));
+{\out Level 1}
+{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
+{\out 1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q}
+\end{ttbox}
+We can eliminate the universal or the existential quantifier. The
+existential quantifier should be eliminated first, since this creates a
+parameter. The rule~$(\exists E)$ is bound to the
+identifier~\ttindex{exE}.
+\begin{ttbox}
+by (eresolve_tac [exE] 1);
+{\out Level 2}
+{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
+{\out 1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q}
+\end{ttbox}
+The only possibility now is $(\forall E)$, a destruction rule. We use
+\ttindex{dresolve_tac}, which discards the quantified assumption; it is
+only needed once.
+\begin{ttbox}
+by (dresolve_tac [spec] 1);
+{\out Level 3}
+{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
+{\out 1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q}
+\end{ttbox}
+Because the parameter~{\tt x} appeared first, the unknown
+term~{\tt?x3(x)} may depend upon it. Had we eliminated the universal
+quantifier before the existential, this would not be so.
+
+Although $({\imp}E)$ is a destruction rule, it works with
+\ttindex{eresolve_tac} to perform backward chaining. This technique is
+frequently useful.
+\begin{ttbox}
+by (eresolve_tac [mp] 1);
+{\out Level 4}
+{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
+{\out 1. !!x. P(x) ==> P(?x3(x))}
+\end{ttbox}
+The tactic has reduced~{\tt Q} to~{\tt P(?x3(x))}, deleting the
+implication. The final step is trivial, thanks to the occurrence of~{\tt x}.
+\begin{ttbox}
+by (assume_tac 1);
+{\out Level 5}
+{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
+{\out No subgoals!}
+\end{ttbox}
+
+
+\subsection{The classical reasoning package}
+\index{classical reasoning package}
+Although Isabelle cannot compete with fully automatic theorem provers, it
+provides enough automation to tackle substantial examples. The classical
+reasoning package can be set up for any classical natural deduction logic
+--- see the {\em Reference Manual}.
+
+Rules are packaged into bundles called \bfindex{classical sets}. The package
+provides several tactics, which apply rules using naive algorithms, using
+unification to handle quantifiers. The most useful tactic
+is~\ttindex{fast_tac}.
+
+Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}. (The
+backslashes~\hbox{\verb|\|\ldots\verb|\|} are an \ML{} string escape
+sequence, to break the long string over two lines.)
+\begin{ttbox}
+goal FOL.thy "(EX y. ALL x. J(y,x) <-> ~J(x,x)) \ttback
+\ttback --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
+{\out Level 0}
+{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
+{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
+{\out 1. (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
+{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
+\end{ttbox}
+The rules of classical logic are bundled as {\tt FOL_cs}. We may solve
+subgoal~1 at a stroke, using~\ttindex{fast_tac}.
+\begin{ttbox}
+by (fast_tac FOL_cs 1);
+{\out Level 1}
+{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
+{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
+{\out No subgoals!}
+\end{ttbox}
+Sceptics may examine the proof by calling the package's single-step
+tactics, such as~{\tt step_tac}. This would take up much space, however,
+so let us proceed to the next example:
+\begin{ttbox}
+goal FOL.thy "ALL x. P(x,f(x)) <-> \ttback
+\ttback (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
+{\out Level 0}
+{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
+{\out 1. ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
+\end{ttbox}
+Again, subgoal~1 succumbs immediately.
+\begin{ttbox}
+by (fast_tac FOL_cs 1);
+{\out Level 1}
+{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
+{\out No subgoals!}
+\end{ttbox}
+The classical reasoning package is not restricted to the usual logical
+connectives. The natural deduction rules for unions and intersections in
+set theory resemble those for disjunction and conjunction, and in the
+infinitary case, for quantifiers. The package is valuable for reasoning in
+set theory.
+
+
+% Local Variables:
+% mode: latex
+% TeX-master: t
+% End: