%% $Id$

 \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{*"["| symbol}\index{*"|"] symbol}

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