--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Intro/document/getting.tex Mon Aug 27 20:50:10 2012 +0200
@@ -0,0 +1,956 @@
+\part{Using Isabelle from the ML Top-Level}\label{chap:getting}
+
+Most Isabelle users write proof scripts using the Isar language, as described in the \emph{Tutorial}, and debug them through the Proof General user interface~\cite{proofgeneral}. Isabelle's original user interface --- based on the \ML{} top-level --- is still available, however.
+Proofs are conducted by
+applying certain \ML{} functions, which update a stored proof state.
+All syntax can be expressed using plain {\sc ascii}
+characters, but Isabelle can support
+alternative syntaxes, for example using mathematical symbols from a
+special screen font. The meta-logic and main object-logics already
+provide such fancy output as an option.
+
+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 \texttt{typ},
+\texttt{term}, \texttt{Sign.sg}, \texttt{thm}, \texttt{theory} and \texttt{tactic};
+tacticals have function types such as \texttt{tactic->tactic}. Isabelle
+users can operate on these data structures by writing \ML{} programs.
+
+
+\section{Forward proof}\label{sec:forward} \index{forward proof|(}
+This section describes the concrete syntax for types, terms and theorems,
+and demonstrates forward proof. The examples are set in first-order logic.
+The command to start Isabelle running first-order logic is
+\begin{ttbox}
+isabelle FOL
+\end{ttbox}
+Note that just typing \texttt{isabelle} usually brings up higher-order logic
+(HOL) by default.
+
+
+\subsection{Lexical matters}
+\index{identifiers}\index{reserved words}
+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 \texttt{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.
+
+Identifiers that are not reserved words may serve as free variables or
+constants. A {\bf type identifier} consists of an identifier prefixed by a
+prime, for example {\tt'a} and \hbox{\tt'hello}. Type identifiers stand
+for (free) type variables, which remain fixed during a proof.
+\index{type identifiers}
+
+An {\bf unknown}\index{unknowns} (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.%
+\footnote{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 {\tt"z6"} and subscript~0, while {\tt?a0.5}
+ has identifier {\tt"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 {\tt"hello"} and subscript
+ zero, while {\tt?z6} has identifier {\tt"z"} and subscript~6. The same
+ conventions apply to type unknowns. The question mark is {\it not\/}
+ part of the identifier!}
+
+
+\subsection{Syntax of types and terms}
+\index{classes!built-in|bold}\index{syntax!of types and terms}
+
+Classes are denoted by identifiers; the built-in class \cldx{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 of|bold}\index{sort constraints} Types are written
+with a syntax like \ML's. The built-in type \tydx{prop} is the type
+of propositions. Type variables can be constrained to particular
+classes or sorts, for example \texttt{'a::term} and \texttt{?'b::\ttlbrace
+ ord, arith\ttrbrace}.
+\[\dquotes
+\index{*:: symbol}\index{*=> symbol}
+\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
+\index{*[ symbol}\index{*] symbol}
+\begin{array}{ll}
+ \multicolumn{2}{c}{\hbox{ASCII Notation for Types}} \\ \hline
+ \alpha "::" C & \hbox{class constraint} \\
+ \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" &
+ \hbox{sort constraint} \\
+ \sigma " => " \tau & \hbox{function type } \sigma\To\tau \\
+ "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau
+ & \hbox{$n$-argument function type} \\
+ "(" \tau@1"," \ldots "," \tau@n ")" tycon & \hbox{type construction}
+\end{array}
+\]
+Terms are those of the typed $\lambda$-calculus.
+\index{terms!syntax of|bold}\index{type constraints}
+\[\dquotes
+\index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$-abstractions}
+\index{*:: symbol}
+\begin{array}{ll}
+ \multicolumn{2}{c}{\hbox{ASCII Notation for Terms}} \\ \hline
+ t "::" \sigma & \hbox{type constraint} \\
+ "\%" x "." t & \hbox{abstraction } \lambda x.t \\
+ "\%" x@1\ldots x@n "." t & \hbox{abstraction over several arguments} \\
+ t "(" u@1"," \ldots "," u@n ")" &
+ \hbox{application to several arguments (FOL and ZF)} \\
+ t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)}
+\end{array}
+\]
+Note that HOL uses its traditional ``higher-order'' syntax for application,
+which differs from that used in FOL.
+
+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~\texttt{prop}.
+\index{meta-implication}
+\index{meta-quantifiers}\index{meta-equality}
+\index{*"!"! symbol}
+
+\index{["!@{\tt[\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working
+\index{"!]@{\tt\char124]} symbol} % so these are [| and |]
+
+\index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
+\[\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 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 constraints}
+
+\index{*Trueprop constant}
+Most logics define the implicit coercion $Trueprop$ from object-formulae to
+propositions. 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~\tydx{prop} are seldom
+useful, but you can make a variable stand for a meta-formula by prefixing
+it with the symbol \texttt{PROP}:\index{*PROP symbol}
+\begin{ttbox}
+PROP ?psi ==> PROP ?theta
+\end{ttbox}
+
+Symbols of object-logics are typically rendered into {\sc ascii} 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) $$
+$({\conj}I)$ translates into {\sc ascii} characters as
+\begin{ttbox}
+[| ?P; ?Q |] ==> ?P & ?Q
+\end{ttbox}
+The schematic variables let unification instantiate the rule. To avoid
+cluttering logic definitions with question marks, Isabelle converts any
+free variables in a rule to schematic variables; we normally declare
+$({\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 system}
+Meta-level theorems have the \ML{} type \mltydx{thm}. They 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 \texttt{prth}, \texttt{prths} and~{\tt
+ prthq}. Of the other operations on theorems, most useful are \texttt{RS}
+and \texttt{RSN}, which perform resolution.
+
+\index{theorems!printing of}
+\begin{ttdescription}
+\item[\ttindex{prth} {\it thm};]
+ pretty-prints {\it thm\/} at the terminal.
+
+\item[\ttindex{prths} {\it thms};]
+ pretty-prints {\it thms}, a list of theorems.
+
+\item[\ttindex{prthq} {\it thmq};]
+ pretty-prints {\it thmq}, a sequence of theorems; this is useful for
+ inspecting the output of a tactic.
+
+\item[$thm1$ RS $thm2$] \index{*RS}
+ resolves the conclusion of $thm1$ with the first premise of~$thm2$.
+
+\item[$thm1$ RSN $(i,thm2)$] \index{*RSN}
+ resolves the conclusion of $thm1$ with the $i$th premise of~$thm2$.
+
+\item[\ttindex{standard} $thm$]
+ puts $thm$ into a standard format. It also renames schematic variables
+ to have subscript zero, improving readability and reducing subscript
+ growth.
+\end{ttdescription}
+The rules of a theory are normally bound to \ML\ identifiers. Suppose we are
+running an Isabelle session containing theory~FOL, natural deduction
+first-order logic.\footnote{For a listing of the FOL rules and their \ML{}
+ names, turn to
+\iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}%
+ {page~\pageref{fol-rules}}.}
+Let us try an example given in~\S\ref{joining}. We
+first print \tdx{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}
+User input appears in {\footnotesize\tt typewriter characters}, and output
+appears in{\out 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. Printing
+commands like \texttt{prth} omit the quotes and the surrounding \texttt{val
+ \ldots :\ thm}. Ignoring their side-effects, the printing commands are
+identity functions.
+
+To contrast \texttt{RS} with \texttt{RSN}, we resolve
+\tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{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}}
+\]
+%
+Rules can be derived by pasting other rules together. Let us join
+\tdx{spec}, which stands for~$(\forall E)$, with \texttt{mp} and {\tt
+ conjunct1}. In \ML{}, the identifier~\texttt{it} denotes the value just
+printed.
+\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) |] ==>}
+{\out ?Q2(?x1)" : thm}
+it RS conjunct1;
+{\out val it = "[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==>}
+{\out ?P6(?x2)" : thm}
+standard it;
+{\out val it = "[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==>}
+{\out ?Pa(?x)" : thm}
+\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.
+\index{assumptions!use of}
+
+\subsection{*Flex-flex constraints} \label{flexflex}
+\index{flex-flex constraints|bold}\index{unknowns!function}
+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 \texttt{RS} and~\texttt{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 = "EX x. ?a3(x) = ?a2(x)" [.] : thm}
+\end{ttbox}
+%
+The mysterious symbol \texttt{[.]} indicates that the result is subject to
+a meta-level hypothesis. We can make all such hypotheses visible by setting the
+\ttindexbold{show_hyps} flag:
+\begin{ttbox}
+set show_hyps;
+{\out val it = true : bool}
+refl RS exI;
+{\out val it = "EX x. ?a3(x) = ?a2(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 \texttt{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 \tdx{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}
+{\out THM ("RSN: multiple unifiers", 1,}
+{\out ["k = k", "?P(?x) ==> EX x. ?P(x)"])}
+\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}
+
+\index{forward proof|)}
+
+\section{Backward proof}
+Although \texttt{RS} and \texttt{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}
+The tactics \texttt{assume_tac}, {\tt
+resolve_tac}, \texttt{eresolve_tac}, and \texttt{dresolve_tac} suffice for most
+single-step proofs. Although \texttt{eresolve_tac} and \texttt{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{ttdescription}
+\item[\ttindex{assume_tac} {\it i}] \index{tactics!assumption}
+ 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[\ttindex{resolve_tac} {\it thms} {\it i}]\index{tactics!resolution}
+ 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[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elim-resolution}
+ performs elim-resolution. Like \texttt{resolve_tac~{\it thms}~{\it i\/}}
+ followed by \texttt{assume_tac~{\it i}}, it applies a rule then solves its
+ first premise by assumption. But \texttt{eresolve_tac} additionally deletes
+ that assumption from any subgoals arising from the resolution.
+
+\item[\ttindex{dresolve_tac} {\it thms} {\it i}]
+ \index{forward proof}\index{destruct-resolution}
+ performs destruct-resolution with the~$thms$, as described
+ in~\S\ref{destruct}. It is useful for forward reasoning from the
+ assumptions.
+\end{ttdescription}
+
+\subsection{Commands for backward proof}
+\index{proofs!commands for}
+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{ttdescription}
+\item[\ttindex{Goal} {\it formula}; ]
+begins a new proof, where the {\it formula\/} is written as an \ML\ string.
+
+\item[\ttindex{by} {\it tactic}; ]
+applies the {\it tactic\/} to the current proof
+state, raising an exception if the tactic fails.
+
+\item[\ttindex{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[\ttindex{result}();]
+returns the theorem just proved, in a standard format. It fails if
+unproved subgoals are left, etc.
+
+\item[\ttindex{qed} {\it name};] is the usual way of ending a proof.
+ It gets the theorem using \texttt{result}, stores it in Isabelle's
+ theorem database and binds it to an \ML{} identifier.
+
+\end{ttdescription}
+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
+\index{*br} \index{*be} \index{*bd} \index{*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 \texttt{FOL} of the Isabelle distribution defines 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 \texttt{FOL/ex/intro.ML}.}
+\begin{ttbox}
+Goal "P|P --> P";
+{\out Level 0}
+{\out P | P --> P}
+{\out 1. P | P --> P}
+\end{ttbox}\index{level of a proof}
+Isabelle responds by printing the initial proof state, which has $P\disj
+P\imp P$ as the main goal and the only subgoal. The {\bf level} of the
+state is the number of \texttt{by} commands that have been applied to reach
+it. We now use \ttindex{resolve_tac} to apply the rule \tdx{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
+\tdx{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 affects subgoal~1, updating {\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~\texttt{P} in subgoal~1.
+\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 \texttt{qed} stores the theorem.
+\begin{ttbox}
+qed "mythm";
+{\out val mythm = "?P | ?P --> ?P" : thm}
+\end{ttbox}
+Isabelle has replaced the free variable~\texttt{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.
+
+As an exercise, try doing the proof as in \S\ref{prop-proof}, observing how
+instantiations affect the proof state.
+
+
+\subsection{Part of a distributive law}
+\index{examples!propositional}
+To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac}
+and the tactical \texttt{REPEAT}, let us prove part of the distributive
+law
+\[ (P\conj Q)\disj R \,\bimp\, (P\disj R)\conj (Q\disj R). \]
+We begin by stating the goal to Isabelle and applying~$({\imp}I)$ to it:
+\begin{ttbox}
+Goal "(P & Q) | R --> (P | R)";
+{\out Level 0}
+{\out P & Q | R --> P | R}
+{\out 1. P & Q | R --> P | R}
+\ttbreak
+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 \texttt{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 \texttt{eresolve_tac}; it would replace $P\conj Q$ by the two
+assumptions~$P$ and~$Q$. Because the present example does not need~$Q$, we
+may try out \texttt{dresolve_tac}.
+\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 \texttt{assume_tac} can finish the proof. The
+tactical~\ttindex{REPEAT} here expresses a tactic that calls \texttt{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}\index{parameters}\index{unknowns}\index{unknowns!function}
+This section illustrates how Isabelle enforces quantifier provisos.
+Suppose that $x$, $y$ and~$z$ are parameters of a subgoal. Quantifier
+rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a function
+unknown. Instantiating $\Var{f}$ to $\lambda x\,z.t$ has the effect of
+replacing~$\Var{f}(x,z)$ by~$t$, where the term~$t$ may contain free
+occurrences of~$x$ and~$z$. On the other hand, no instantiation
+of~$\Var{f}$ can replace~$\Var{f}(x,z)$ by a term containing free
+occurrences of~$y$, since parameters are bound variables.
+
+\subsection{Two quantifier proofs: a success and a failure}
+\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{paulson-found}. 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.
+
+\paragraph{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 "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~\texttt{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~\texttt{x}.
+
+To remove the existential quantifier, 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 \texttt{y} has become {\tt?y1(x)}. This term consists of
+the function unknown~{\tt?y1} applied to the parameter~\texttt{x}.
+Instances of {\tt?y1(x)} may or may not contain~\texttt{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.
+
+\paragraph{The unsuccessful proof.}
+We state the goal $\exists y.\forall x.x=y$, which is not a theorem, and
+try~$(\exists I)$:
+\begin{ttbox}
+Goal "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 \texttt{?y} may be replaced by any term, but this can never
+introduce another bound occurrence of~\texttt{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~\texttt{x}.
+The reflexivity axiom does not unify with subgoal~1.
+\begin{ttbox}
+by (resolve_tac [refl] 1);
+{\out by: tactic failed}
+\end{ttbox}
+There can be no proof of $\exists y.\forall x.x=y$ by the soundness of
+first-order logic. I have elsewhere proved the faithfulness of Isabelle's
+encoding of first-order logic~\cite{paulson-found}; there could, of course, be
+faults in 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 \texttt{REPEAT}
+and~\texttt{ORELSE}.
+\begin{ttbox}
+Goal "(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}
+
+\paragraph{The wrong approach.}
+Using \texttt{dresolve_tac}, we apply the rule $(\forall E)$, bound to the
+\ML\ identifier \tdx{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 \texttt{?x1} and the parameter \texttt{z} have appeared. We again
+apply $(\forall E)$ and~$(\forall I)$.
+\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 \texttt{?y3} and the parameter \texttt{w} have appeared. Each
+unknown is applied to the parameters existing at the time of its creation;
+instances of~\texttt{?x1} cannot contain~\texttt{z} or~\texttt{w}, while instances
+of {\tt?y3(z)} can only contain~\texttt{z}. Due to the restriction on~\texttt{?x1},
+proof by assumption will fail.
+\begin{ttbox}
+by (assume_tac 1);
+{\out by: tactic failed}
+{\out uncaught exception ERROR}
+\end{ttbox}
+
+\paragraph{The right approach.}
+To do this proof, the rules must be applied in the correct order.
+Parameters 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)$ before $(\forall I)$.
+\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 \texttt{z} and~\texttt{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~\texttt{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}
+
+\paragraph{A one-step proof using tacticals.}
+\index{tacticals} \index{examples!of tacticals}
+
+Repeated application of rules can be effective, but the rules should be
+attempted in the correct order. 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}
+As we have just seen, \tdx{allI} should be attempted
+before~\tdx{spec}, while \ttindex{assume_tac} generally can be
+attempted first. Such priorities can easily be expressed
+using~\ttindex{ORELSE}, and repeated using~\ttindex{REPEAT}.
+\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}
+To see the practical use of parameters and unknowns, let us prove half of
+the equivalence
+\[ (\forall x. P(x) \imp Q) \,\bimp\, ((\exists x. P(x)) \imp Q). \]
+We state the left-to-right half to Isabelle in the normal way.
+Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we
+use \texttt{REPEAT}:
+\begin{ttbox}
+Goal "(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~\tdx{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 we applied $(\exists E)$ before $(\forall E)$, the unknown
+term~{\tt?x3(x)} may depend upon the parameter~\texttt{x}.
+
+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~\texttt{Q} to~\texttt{P(?x3(x))}, deleting the
+implication. The final step is trivial, thanks to the occurrence of~\texttt{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 reasoner}
+\index{classical reasoner}
+Isabelle provides enough automation to tackle substantial examples.
+The classical
+reasoner can be set up for any classical natural deduction logic;
+see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
+ {Chap.\ts\ref{chap:classical}}.
+It cannot compete with fully automatic theorem provers, but it is
+competitive with tools found in other interactive provers.
+
+Rules are packaged into {\bf classical sets}. The classical reasoner
+provides several tactics, which apply rules using naive algorithms.
+Unification handles quantifiers as shown above. The most useful tactic
+is~\ttindex{Blast_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 "(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}
+\ttindex{Blast_tac} proves subgoal~1 at a stroke.
+\begin{ttbox}
+by (Blast_tac 1);
+{\out Depth = 0}
+{\out Depth = 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~\texttt{step_tac}. This would take up much space, however,
+so let us proceed to the next example:
+\begin{ttbox}
+Goal "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)) <->}
+{\out (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
+\end{ttbox}
+Again, subgoal~1 succumbs immediately.
+\begin{ttbox}
+by (Blast_tac 1);
+{\out Depth = 0}
+{\out Depth = 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 reasoner is not restricted to the usual logical connectives.
+The natural deduction rules for unions and intersections resemble those for
+disjunction and conjunction. The rules for infinite unions and
+intersections resemble those for quantifiers. Given such rules, the classical
+reasoner is effective for reasoning in set theory.
+