doc-src/Intro/getting.tex
 author wenzelm Mon Oct 01 21:19:50 2007 +0200 (2007-10-01) changeset 24803 38577b4b1fde parent 14148 6580d374a509 child 42637 381fdcab0f36 permissions -rw-r--r--
Norbert Schirmer: record improvements;
     1 %% $Id$

     2 \part{Using Isabelle from the ML Top-Level}\label{chap:getting}

     3

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

     5 Proofs are conducted by

     6 applying certain \ML{} functions, which update a stored proof state.

     7 All syntax can be expressed using plain {\sc ascii}

     8 characters, but Isabelle can support

     9 alternative syntaxes, for example using mathematical symbols from a

    10 special screen font.  The meta-logic and main object-logics already

    11 provide such fancy output as an option.

    12

    13 Object-logics are built upon Pure Isabelle, which implements the

    14 meta-logic and provides certain fundamental data structures: types,

    15 terms, signatures, theorems and theories, tactics and tacticals.

    16 These data structures have the corresponding \ML{} types \texttt{typ},

    17 \texttt{term}, \texttt{Sign.sg}, \texttt{thm}, \texttt{theory} and \texttt{tactic};

    18 tacticals have function types such as \texttt{tactic->tactic}.  Isabelle

    19 users can operate on these data structures by writing \ML{} programs.

    20

    21

    22 \section{Forward proof}\label{sec:forward} \index{forward proof|(}

    23 This section describes the concrete syntax for types, terms and theorems,

    24 and demonstrates forward proof.  The examples are set in first-order logic.

    25 The command to start Isabelle running first-order logic is

    26 \begin{ttbox}

    27 isabelle FOL

    28 \end{ttbox}

    29 Note that just typing \texttt{isabelle} usually brings up higher-order logic

    30 (HOL) by default.

    31

    32

    33 \subsection{Lexical matters}

    34 \index{identifiers}\index{reserved words}

    35 An {\bf identifier} is a string of letters, digits, underscores~(\verb|_|)

    36 and single quotes~({\tt'}), beginning with a letter.  Single quotes are

    37 regarded as primes; for instance \texttt{x'} is read as~$x'$.  Identifiers are

    38 separated by white space and special characters.  {\bf Reserved words} are

    39 identifiers that appear in Isabelle syntax definitions.

    40

    41 An Isabelle theory can declare symbols composed of special characters, such

    42 as {\tt=}, {\tt==}, {\tt=>} and {\tt==>}.  (The latter three are part of

    43 the syntax of the meta-logic.)  Such symbols may be run together; thus if

    44 \verb|}| and \verb|{| are used for set brackets then \verb|{{a},{a,b}}| is

    45 valid notation for a set of sets --- but only if \verb|}}| and \verb|{{|

    46 have not been declared as symbols!  The parser resolves any ambiguity by

    47 taking the longest possible symbol that has been declared.  Thus the string

    48 {\tt==>} is read as a single symbol.  But \hbox{\tt= =>} is read as two

    49 symbols.

    50

    51 Identifiers that are not reserved words may serve as free variables or

    52 constants.  A {\bf type identifier} consists of an identifier prefixed by a

    53 prime, for example {\tt'a} and \hbox{\tt'hello}.  Type identifiers stand

    54 for (free) type variables, which remain fixed during a proof.

    55 \index{type identifiers}

    56

    57 An {\bf unknown}\index{unknowns} (or type unknown) consists of a question

    58 mark, an identifier (or type identifier), and a subscript.  The subscript,

    59 a non-negative integer,

    60 allows the renaming of unknowns prior to unification.%

    61 \footnote{The subscript may appear after the identifier, separated by a

    62   dot; this prevents ambiguity when the identifier ends with a digit.  Thus

    63   {\tt?z6.0} has identifier {\tt"z6"} and subscript~0, while {\tt?a0.5}

    64   has identifier {\tt"a0"} and subscript~5.  If the identifier does not

    65   end with a digit, then no dot appears and a subscript of~0 is omitted;

    66   for example, {\tt?hello} has identifier {\tt"hello"} and subscript

    67   zero, while {\tt?z6} has identifier {\tt"z"} and subscript~6.  The same

    68   conventions apply to type unknowns.  The question mark is {\it not\/}

    69   part of the identifier!}

    70

    71

    72 \subsection{Syntax of types and terms}

    73 \index{classes!built-in|bold}\index{syntax!of types and terms}

    74

    75 Classes are denoted by identifiers; the built-in class \cldx{logic}

    76 contains the logical' types.  Sorts are lists of classes enclosed in

    77 braces~\} and \{; singleton sorts may be abbreviated by dropping the braces.

    78

    79 \index{types!syntax of|bold}\index{sort constraints} Types are written

    80 with a syntax like \ML's.  The built-in type \tydx{prop} is the type

    81 of propositions.  Type variables can be constrained to particular

    82 classes or sorts, for example \texttt{'a::term} and \texttt{?'b::\ttlbrace

    83   ord, arith\ttrbrace}.

    84 $\dquotes   85 \index{*:: symbol}\index{*=> symbol}   86 \index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}   87 \index{*[ symbol}\index{*] symbol}   88 \begin{array}{ll}   89 \multicolumn{2}{c}{\hbox{ASCII Notation for Types}} \\ \hline   90 \alpha "::" C & \hbox{class constraint} \\   91 \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" &   92 \hbox{sort constraint} \\   93 \sigma " => " \tau & \hbox{function type } \sigma\To\tau \\   94 "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau   95 & \hbox{n-argument function type} \\   96 "(" \tau@1"," \ldots "," \tau@n ")" tycon & \hbox{type construction}   97 \end{array}   98$

    99 Terms are those of the typed $\lambda$-calculus.

   100 \index{terms!syntax of|bold}\index{type constraints}

   101 $\dquotes   102 \index{%@{\tt\%} symbol}\index{lambda abs@\lambda-abstractions}   103 \index{*:: symbol}   104 \begin{array}{ll}   105 \multicolumn{2}{c}{\hbox{ASCII Notation for Terms}} \\ \hline   106 t "::" \sigma & \hbox{type constraint} \\   107 "\%" x "." t & \hbox{abstraction } \lambda x.t \\   108 "\%" x@1\ldots x@n "." t & \hbox{abstraction over several arguments} \\   109 t "(" u@1"," \ldots "," u@n ")" &   110 \hbox{application to several arguments (FOL and ZF)} \\   111 t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)}   112 \end{array}   113$

   114 Note that HOL uses its traditional higher-order'' syntax for application,

   115 which differs from that used in FOL.

   116

   117 The theorems and rules of an object-logic are represented by theorems in

   118 the meta-logic, which are expressed using meta-formulae.  Since the

   119 meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{}

   120 are just terms of type~\texttt{prop}.

   121 \index{meta-implication}

   122 \index{meta-quantifiers}\index{meta-equality}

   123 \index{*"!"! symbol}\index{*"["| symbol}\index{*"|"] symbol}

   124 \index{*== symbol}\index{*=?= symbol}\index{*==> symbol}

   125 $\dquotes   126 \begin{array}{l@{\quad}l@{\quad}l}   127 \multicolumn{3}{c}{\hbox{ASCII Notation for Meta-Formulae}} \\ \hline   128 a " == " b & a\equiv b & \hbox{meta-equality} \\   129 a " =?= " b & a\qeq b & \hbox{flex-flex constraint} \\   130 \phi " ==> " \psi & \phi\Imp \psi & \hbox{meta-implication} \\   131 "[|" \phi@1 ";" \ldots ";" \phi@n "|] ==> " \psi &   132 \List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\   133 "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\   134 "!!" x@1\ldots x@n "." \phi &   135 \Forall x@1. \ldots x@n.\phi & \hbox{nested quantification}   136 \end{array}   137$

   138 Flex-flex constraints are meta-equalities arising from unification; they

   139 require special treatment.  See~\S\ref{flexflex}.

   140 \index{flex-flex constraints}

   141

   142 \index{*Trueprop constant}

   143 Most logics define the implicit coercion $Trueprop$ from object-formulae to

   144 propositions.  This could cause an ambiguity: in $P\Imp Q$, do the

   145 variables $P$ and $Q$ stand for meta-formulae or object-formulae?  If the

   146 latter, $P\Imp Q$ really abbreviates $Trueprop(P)\Imp Trueprop(Q)$.  To

   147 prevent such ambiguities, Isabelle's syntax does not allow a meta-formula

   148 to consist of a variable.  Variables of type~\tydx{prop} are seldom

   149 useful, but you can make a variable stand for a meta-formula by prefixing

   150 it with the symbol \texttt{PROP}:\index{*PROP symbol}

   151 \begin{ttbox}

   152 PROP ?psi ==> PROP ?theta

   153 \end{ttbox}

   154

   155 Symbols of object-logics are typically rendered into {\sc ascii} as

   156 follows:

   157 $\begin{tabular}{l@{\quad}l@{\quad}l}   158 \tt True & \top & true \\   159 \tt False & \bot & false \\   160 \tt P \& Q & P\conj Q & conjunction \\   161 \tt P | Q & P\disj Q & disjunction \\   162 \verb'~' P & \neg P & negation \\   163 \tt P --> Q & P\imp Q & implication \\   164 \tt P <-> Q & P\bimp Q & bi-implication \\   165 \tt ALL x\,y\,z .\ P & \forall x\,y\,z.P & for all \\   166 \tt EX x\,y\,z .\ P & \exists x\,y\,z.P & there exists   167 \end{tabular}   168$

   169 To illustrate the notation, consider two axioms for first-order logic:

   170 $$\List{P; Q} \Imp P\conj Q \eqno(\conj I)$$

   171 $$\List{\exists x. P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E)$$

   172 $({\conj}I)$ translates into {\sc ascii} characters as

   173 \begin{ttbox}

   174 [| ?P; ?Q |] ==> ?P & ?Q

   175 \end{ttbox}

   176 The schematic variables let unification instantiate the rule.  To avoid

   177 cluttering logic definitions with question marks, Isabelle converts any

   178 free variables in a rule to schematic variables; we normally declare

   179 $({\conj}I)$ as

   180 \begin{ttbox}

   181 [| P; Q |] ==> P & Q

   182 \end{ttbox}

   183 This variables convention agrees with the treatment of variables in goals.

   184 Free variables in a goal remain fixed throughout the proof.  After the

   185 proof is finished, Isabelle converts them to scheme variables in the

   186 resulting theorem.  Scheme variables in a goal may be replaced by terms

   187 during the proof, supporting answer extraction, program synthesis, and so

   188 forth.

   189

   190 For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as

   191 \begin{ttbox}

   192 [| EX x. P(x);  !!x. P(x) ==> Q |] ==> Q

   193 \end{ttbox}

   194

   195

   196 \subsection{Basic operations on theorems}

   197 \index{theorems!basic operations on|bold}

   198 \index{LCF system}

   199 Meta-level theorems have the \ML{} type \mltydx{thm}.  They represent the

   200 theorems and inference rules of object-logics.  Isabelle's meta-logic is

   201 implemented using the {\sc lcf} approach: each meta-level inference rule is

   202 represented by a function from theorems to theorems.  Object-level rules

   203 are taken as axioms.

   204

   205 The main theorem printing commands are \texttt{prth}, \texttt{prths} and~{\tt

   206   prthq}.  Of the other operations on theorems, most useful are \texttt{RS}

   207 and \texttt{RSN}, which perform resolution.

   208

   209 \index{theorems!printing of}

   210 \begin{ttdescription}

   211 \item[\ttindex{prth} {\it thm};]

   212   pretty-prints {\it thm\/} at the terminal.

   213

   214 \item[\ttindex{prths} {\it thms};]

   215   pretty-prints {\it thms}, a list of theorems.

   216

   217 \item[\ttindex{prthq} {\it thmq};]

   218   pretty-prints {\it thmq}, a sequence of theorems; this is useful for

   219   inspecting the output of a tactic.

   220

   221 \item[$thm1$ RS $thm2$] \index{*RS}

   222   resolves the conclusion of $thm1$ with the first premise of~$thm2$.

   223

   224 \item[$thm1$ RSN $(i,thm2)$] \index{*RSN}

   225   resolves the conclusion of $thm1$ with the $i$th premise of~$thm2$.

   226

   227 \item[\ttindex{standard} $thm$]

   228   puts $thm$ into a standard format.  It also renames schematic variables

   229   to have subscript zero, improving readability and reducing subscript

   230   growth.

   231 \end{ttdescription}

   232 The rules of a theory are normally bound to \ML\ identifiers.  Suppose we are

   233 running an Isabelle session containing theory~FOL, natural deduction

   234 first-order logic.\footnote{For a listing of the FOL rules and their \ML{}

   235   names, turn to

   236 \iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}%

   237            {page~\pageref{fol-rules}}.}

   238 Let us try an example given in~\S\ref{joining}.  We

   239 first print \tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with

   240 itself.

   241 \begin{ttbox}

   242 prth mp;

   243 {\out [| ?P --> ?Q; ?P |] ==> ?Q}

   244 {\out val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm}

   245 prth (mp RS mp);

   246 {\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q}

   247 {\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm}

   248 \end{ttbox}

   249 User input appears in {\footnotesize\tt typewriter characters}, and output

   250 appears in{\out slanted typewriter characters}.  \ML's response {\out val

   251   }~\ldots{} is compiler-dependent and will sometimes be suppressed.  This

   252 session illustrates two formats for the display of theorems.  Isabelle's

   253 top-level displays theorems as \ML{} values, enclosed in quotes.  Printing

   254 commands like \texttt{prth} omit the quotes and the surrounding \texttt{val

   255   \ldots :\ thm}.  Ignoring their side-effects, the printing commands are

   256 identity functions.

   257

   258 To contrast \texttt{RS} with \texttt{RSN}, we resolve

   259 \tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}.

   260 \begin{ttbox}

   261 conjunct1 RS mp;

   262 {\out val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm}

   263 conjunct1 RSN (2,mp);

   264 {\out val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm}

   265 \end{ttbox}

   266 These correspond to the following proofs:

   267 $\infer[({\imp}E)]{Q}{\infer[({\conj}E1)]{P\imp Q}{(P\imp Q)\conj Q@1} & P}   268 \qquad   269 \infer[({\imp}E)]{Q}{P\imp Q & \infer[({\conj}E1)]{P}{P\conj Q@1}}   270$

   271 %

   272 Rules can be derived by pasting other rules together.  Let us join

   273 \tdx{spec}, which stands for~$(\forall E)$, with \texttt{mp} and {\tt

   274   conjunct1}.  In \ML{}, the identifier~\texttt{it} denotes the value just

   275 printed.

   276 \begin{ttbox}

   277 spec;

   278 {\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm}

   279 it RS mp;

   280 {\out val it = "[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==>}

   281 {\out           ?Q2(?x1)" : thm}

   282 it RS conjunct1;

   283 {\out val it = "[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==>}

   284 {\out           ?P6(?x2)" : thm}

   285 standard it;

   286 {\out val it = "[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==>}

   287 {\out           ?Pa(?x)" : thm}

   288 \end{ttbox}

   289 By resolving $(\forall E)$ with (${\imp}E)$ and (${\conj}E1)$, we have

   290 derived a destruction rule for formulae of the form $\forall x.   291 P(x)\imp(Q(x)\conj R(x))$.  Used with destruct-resolution, such specialized

   292 rules provide a way of referring to particular assumptions.

   293 \index{assumptions!use of}

   294

   295 \subsection{*Flex-flex constraints} \label{flexflex}

   296 \index{flex-flex constraints|bold}\index{unknowns!function}

   297 In higher-order unification, {\bf flex-flex} equations are those where both

   298 sides begin with a function unknown, such as $\Var{f}(0)\qeq\Var{g}(0)$.

   299 They admit a trivial unifier, here $\Var{f}\equiv \lambda x.\Var{a}$ and

   300 $\Var{g}\equiv \lambda y.\Var{a}$, where $\Var{a}$ is a new unknown.  They

   301 admit many other unifiers, such as $\Var{f} \equiv \lambda x.\Var{g}(0)$

   302 and $\{\Var{f} \equiv \lambda x.x,\, \Var{g} \equiv \lambda x.0\}$.  Huet's

   303 procedure does not enumerate the unifiers; instead, it retains flex-flex

   304 equations as constraints on future unifications.  Flex-flex constraints

   305 occasionally become attached to a proof state; more frequently, they appear

   306 during use of \texttt{RS} and~\texttt{RSN}:

   307 \begin{ttbox}

   308 refl;

   309 {\out val it = "?a = ?a" : thm}

   310 exI;

   311 {\out val it = "?P(?x) ==> EX x. ?P(x)" : thm}

   312 refl RS exI;

   313 {\out val it = "EX x. ?a3(x) = ?a2(x)"  [.] : thm}

   314 \end{ttbox}

   315 %

   316 The mysterious symbol \texttt{[.]} indicates that the result is subject to

   317 a meta-level hypothesis. We can make all such hypotheses visible by setting the

   318 \ttindexbold{show_hyps} flag:

   319 \begin{ttbox}

   320 set show_hyps;

   321 {\out val it = true : bool}

   322 refl RS exI;

   323 {\out val it = "EX x. ?a3(x) = ?a2(x)"  ["?a3(?x) =?= ?a2(?x)"] : thm}

   324 \end{ttbox}

   325

   326 \noindent

   327 Renaming variables, this is $\exists x.\Var{f}(x)=\Var{g}(x)$ with

   328 the constraint ${\Var{f}(\Var{u})\qeq\Var{g}(\Var{u})}$.  Instances

   329 satisfying the constraint include $\exists x.\Var{f}(x)=\Var{f}(x)$ and

   330 $\exists x.x=\Var{u}$.  Calling \ttindex{flexflex_rule} removes all

   331 constraints by applying the trivial unifier:\index{*prthq}

   332 \begin{ttbox}

   333 prthq (flexflex_rule it);

   334 {\out EX x. ?a4 = ?a4}

   335 \end{ttbox}

   336 Isabelle simplifies flex-flex equations to eliminate redundant bound

   337 variables.  In $\lambda x\,y.\Var{f}(k(y),x) \qeq \lambda x\,y.\Var{g}(y)$,

   338 there is no bound occurrence of~$x$ on the right side; thus, there will be

   339 none on the left in a common instance of these terms.  Choosing a new

   340 variable~$\Var{h}$, Isabelle assigns $\Var{f}\equiv \lambda u\,v.?h(u)$,

   341 simplifying the left side to $\lambda x\,y.\Var{h}(k(y))$.  Dropping $x$

   342 from the equation leaves $\lambda y.\Var{h}(k(y)) \qeq \lambda   343 y.\Var{g}(y)$.  By $\eta$-conversion, this simplifies to the assignment

   344 $\Var{g}\equiv\lambda y.?h(k(y))$.

   345

   346 \begin{warn}

   347 \ttindex{RS} and \ttindex{RSN} fail (by raising exception \texttt{THM}) unless

   348 the resolution delivers {\bf exactly one} resolvent.  For multiple results,

   349 use \ttindex{RL} and \ttindex{RLN}, which operate on theorem lists.  The

   350 following example uses \ttindex{read_instantiate} to create an instance

   351 of \tdx{refl} containing no schematic variables.

   352 \begin{ttbox}

   353 val reflk = read_instantiate [("a","k")] refl;

   354 {\out val reflk = "k = k" : thm}

   355 \end{ttbox}

   356

   357 \noindent

   358 A flex-flex constraint is no longer possible; resolution does not find a

   359 unique unifier:

   360 \begin{ttbox}

   361 reflk RS exI;

   362 {\out uncaught exception}

   363 {\out    THM ("RSN: multiple unifiers", 1,}

   364 {\out         ["k = k", "?P(?x) ==> EX x. ?P(x)"])}

   365 \end{ttbox}

   366 Using \ttindex{RL} this time, we discover that there are four unifiers, and

   367 four resolvents:

   368 \begin{ttbox}

   369 [reflk] RL [exI];

   370 {\out val it = ["EX x. x = x", "EX x. k = x",}

   371 {\out           "EX x. x = k", "EX x. k = k"] : thm list}

   372 \end{ttbox}

   373 \end{warn}

   374

   375 \index{forward proof|)}

   376

   377 \section{Backward proof}

   378 Although \texttt{RS} and \texttt{RSN} are fine for simple forward reasoning,

   379 large proofs require tactics.  Isabelle provides a suite of commands for

   380 conducting a backward proof using tactics.

   381

   382 \subsection{The basic tactics}

   383 The tactics \texttt{assume_tac}, {\tt

   384 resolve_tac}, \texttt{eresolve_tac}, and \texttt{dresolve_tac} suffice for most

   385 single-step proofs.  Although \texttt{eresolve_tac} and \texttt{dresolve_tac} are

   386 not strictly necessary, they simplify proofs involving elimination and

   387 destruction rules.  All the tactics act on a subgoal designated by a

   388 positive integer~$i$, failing if~$i$ is out of range.  The resolution

   389 tactics try their list of theorems in left-to-right order.

   390

   391 \begin{ttdescription}

   392 \item[\ttindex{assume_tac} {\it i}] \index{tactics!assumption}

   393   is the tactic that attempts to solve subgoal~$i$ by assumption.  Proof by

   394   assumption is not a trivial step; it can falsify other subgoals by

   395   instantiating shared variables.  There may be several ways of solving the

   396   subgoal by assumption.

   397

   398 \item[\ttindex{resolve_tac} {\it thms} {\it i}]\index{tactics!resolution}

   399   is the basic resolution tactic, used for most proof steps.  The $thms$

   400   represent object-rules, which are resolved against subgoal~$i$ of the

   401   proof state.  For each rule, resolution forms next states by unifying the

   402   conclusion with the subgoal and inserting instantiated premises in its

   403   place.  A rule can admit many higher-order unifiers.  The tactic fails if

   404   none of the rules generates next states.

   405

   406 \item[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elim-resolution}

   407   performs elim-resolution.  Like \texttt{resolve_tac~{\it thms}~{\it i\/}}

   408   followed by \texttt{assume_tac~{\it i}}, it applies a rule then solves its

   409   first premise by assumption.  But \texttt{eresolve_tac} additionally deletes

   410   that assumption from any subgoals arising from the resolution.

   411

   412 \item[\ttindex{dresolve_tac} {\it thms} {\it i}]

   413   \index{forward proof}\index{destruct-resolution}

   414   performs destruct-resolution with the~$thms$, as described

   415   in~\S\ref{destruct}.  It is useful for forward reasoning from the

   416   assumptions.

   417 \end{ttdescription}

   418

   419 \subsection{Commands for backward proof}

   420 \index{proofs!commands for}

   421 Tactics are normally applied using the subgoal module, which maintains a

   422 proof state and manages the proof construction.  It allows interactive

   423 backtracking through the proof space, going away to prove lemmas, etc.; of

   424 its many commands, most important are the following:

   425 \begin{ttdescription}

   426 \item[\ttindex{Goal} {\it formula}; ]

   427 begins a new proof, where the {\it formula\/} is written as an \ML\ string.

   428

   429 \item[\ttindex{by} {\it tactic}; ]

   430 applies the {\it tactic\/} to the current proof

   431 state, raising an exception if the tactic fails.

   432

   433 \item[\ttindex{undo}(); ]

   434   reverts to the previous proof state.  Undo can be repeated but cannot be

   435   undone.  Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely

   436   causes \ML\ to echo the value of that function.

   437

   438 \item[\ttindex{result}();]

   439 returns the theorem just proved, in a standard format.  It fails if

   440 unproved subgoals are left, etc.

   441

   442 \item[\ttindex{qed} {\it name};] is the usual way of ending a proof.

   443   It gets the theorem using \texttt{result}, stores it in Isabelle's

   444   theorem database and binds it to an \ML{} identifier.

   445

   446 \end{ttdescription}

   447 The commands and tactics given above are cumbersome for interactive use.

   448 Although our examples will use the full commands, you may prefer Isabelle's

   449 shortcuts:

   450 \begin{center} \tt

   451 \index{*br} \index{*be} \index{*bd} \index{*ba}

   452 \begin{tabular}{l@{\qquad\rm abbreviates\qquad}l}

   453     ba {\it i};           & by (assume_tac {\it i}); \\

   454

   455     br {\it thm} {\it i}; & by (resolve_tac [{\it thm}] {\it i}); \\

   456

   457     be {\it thm} {\it i}; & by (eresolve_tac [{\it thm}] {\it i}); \\

   458

   459     bd {\it thm} {\it i}; & by (dresolve_tac [{\it thm}] {\it i});

   460 \end{tabular}

   461 \end{center}

   462

   463 \subsection{A trivial example in propositional logic}

   464 \index{examples!propositional}

   465

   466 Directory \texttt{FOL} of the Isabelle distribution defines the theory of

   467 first-order logic.  Let us try the example from \S\ref{prop-proof},

   468 entering the goal $P\disj P\imp P$ in that theory.\footnote{To run these

   469   examples, see the file \texttt{FOL/ex/intro.ML}.}

   470 \begin{ttbox}

   471 Goal "P|P --> P";

   472 {\out Level 0}

   473 {\out P | P --> P}

   474 {\out 1. P | P --> P}

   475 \end{ttbox}\index{level of a proof}

   476 Isabelle responds by printing the initial proof state, which has $P\disj   477 P\imp P$ as the main goal and the only subgoal.  The {\bf level} of the

   478 state is the number of \texttt{by} commands that have been applied to reach

   479 it.  We now use \ttindex{resolve_tac} to apply the rule \tdx{impI},

   480 or~$({\imp}I)$, to subgoal~1:

   481 \begin{ttbox}

   482 by (resolve_tac [impI] 1);

   483 {\out Level 1}

   484 {\out P | P --> P}

   485 {\out 1. P | P ==> P}

   486 \end{ttbox}

   487 In the new proof state, subgoal~1 is $P$ under the assumption $P\disj P$.

   488 (The meta-implication {\tt==>} indicates assumptions.)  We apply

   489 \tdx{disjE}, or~(${\disj}E)$, to that subgoal:

   490 \begin{ttbox}

   491 by (resolve_tac [disjE] 1);

   492 {\out Level 2}

   493 {\out P | P --> P}

   494 {\out 1. P | P ==> ?P1 | ?Q1}

   495 {\out 2. [| P | P; ?P1 |] ==> P}

   496 {\out 3. [| P | P; ?Q1 |] ==> P}

   497 \end{ttbox}

   498 At Level~2 there are three subgoals, each provable by assumption.  We

   499 deviate from~\S\ref{prop-proof} by tackling subgoal~3 first, using

   500 \ttindex{assume_tac}.  This affects subgoal~1, updating {\tt?Q1} to~{\tt

   501   P}.

   502 \begin{ttbox}

   503 by (assume_tac 3);

   504 {\out Level 3}

   505 {\out P | P --> P}

   506 {\out 1. P | P ==> ?P1 | P}

   507 {\out 2. [| P | P; ?P1 |] ==> P}

   508 \end{ttbox}

   509 Next we tackle subgoal~2, instantiating {\tt?P1} to~\texttt{P} in subgoal~1.

   510 \begin{ttbox}

   511 by (assume_tac 2);

   512 {\out Level 4}

   513 {\out P | P --> P}

   514 {\out 1. P | P ==> P | P}

   515 \end{ttbox}

   516 Lastly we prove the remaining subgoal by assumption:

   517 \begin{ttbox}

   518 by (assume_tac 1);

   519 {\out Level 5}

   520 {\out P | P --> P}

   521 {\out No subgoals!}

   522 \end{ttbox}

   523 Isabelle tells us that there are no longer any subgoals: the proof is

   524 complete.  Calling \texttt{qed} stores the theorem.

   525 \begin{ttbox}

   526 qed "mythm";

   527 {\out val mythm = "?P | ?P --> ?P" : thm}

   528 \end{ttbox}

   529 Isabelle has replaced the free variable~\texttt{P} by the scheme

   530 variable~{\tt?P}\@.  Free variables in the proof state remain fixed

   531 throughout the proof.  Isabelle finally converts them to scheme variables

   532 so that the resulting theorem can be instantiated with any formula.

   533

   534 As an exercise, try doing the proof as in \S\ref{prop-proof}, observing how

   535 instantiations affect the proof state.

   536

   537

   538 \subsection{Part of a distributive law}

   539 \index{examples!propositional}

   540 To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac}

   541 and the tactical \texttt{REPEAT}, let us prove part of the distributive

   542 law

   543 $(P\conj Q)\disj R \,\bimp\, (P\disj R)\conj (Q\disj R).$

   544 We begin by stating the goal to Isabelle and applying~$({\imp}I)$ to it:

   545 \begin{ttbox}

   546 Goal "(P & Q) | R  --> (P | R)";

   547 {\out Level 0}

   548 {\out P & Q | R --> P | R}

   549 {\out  1. P & Q | R --> P | R}

   550 \ttbreak

   551 by (resolve_tac [impI] 1);

   552 {\out Level 1}

   553 {\out P & Q | R --> P | R}

   554 {\out  1. P & Q | R ==> P | R}

   555 \end{ttbox}

   556 Previously we applied~(${\disj}E)$ using \texttt{resolve_tac}, but

   557 \ttindex{eresolve_tac} deletes the assumption after use.  The resulting proof

   558 state is simpler.

   559 \begin{ttbox}

   560 by (eresolve_tac [disjE] 1);

   561 {\out Level 2}

   562 {\out P & Q | R --> P | R}

   563 {\out  1. P & Q ==> P | R}

   564 {\out  2. R ==> P | R}

   565 \end{ttbox}

   566 Using \ttindex{dresolve_tac}, we can apply~(${\conj}E1)$ to subgoal~1,

   567 replacing the assumption $P\conj Q$ by~$P$.  Normally we should apply the

   568 rule~(${\conj}E)$, given in~\S\ref{destruct}.  That is an elimination rule

   569 and requires \texttt{eresolve_tac}; it would replace $P\conj Q$ by the two

   570 assumptions~$P$ and~$Q$.  Because the present example does not need~$Q$, we

   571 may try out \texttt{dresolve_tac}.

   572 \begin{ttbox}

   573 by (dresolve_tac [conjunct1] 1);

   574 {\out Level 3}

   575 {\out P & Q | R --> P | R}

   576 {\out  1. P ==> P | R}

   577 {\out  2. R ==> P | R}

   578 \end{ttbox}

   579 The next two steps apply~(${\disj}I1$) and~(${\disj}I2$) in an obvious manner.

   580 \begin{ttbox}

   581 by (resolve_tac [disjI1] 1);

   582 {\out Level 4}

   583 {\out P & Q | R --> P | R}

   584 {\out  1. P ==> P}

   585 {\out  2. R ==> P | R}

   586 \ttbreak

   587 by (resolve_tac [disjI2] 2);

   588 {\out Level 5}

   589 {\out P & Q | R --> P | R}

   590 {\out  1. P ==> P}

   591 {\out  2. R ==> R}

   592 \end{ttbox}

   593 Two calls of \texttt{assume_tac} can finish the proof.  The

   594 tactical~\ttindex{REPEAT} here expresses a tactic that calls \texttt{assume_tac~1}

   595 as many times as possible.  We can restrict attention to subgoal~1 because

   596 the other subgoals move up after subgoal~1 disappears.

   597 \begin{ttbox}

   598 by (REPEAT (assume_tac 1));

   599 {\out Level 6}

   600 {\out P & Q | R --> P | R}

   601 {\out No subgoals!}

   602 \end{ttbox}

   603

   604

   605 \section{Quantifier reasoning}

   606 \index{quantifiers}\index{parameters}\index{unknowns}\index{unknowns!function}

   607 This section illustrates how Isabelle enforces quantifier provisos.

   608 Suppose that $x$, $y$ and~$z$ are parameters of a subgoal.  Quantifier

   609 rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a function

   610 unknown.  Instantiating $\Var{f}$ to $\lambda x\,z.t$ has the effect of

   611 replacing~$\Var{f}(x,z)$ by~$t$, where the term~$t$ may contain free

   612 occurrences of~$x$ and~$z$.  On the other hand, no instantiation

   613 of~$\Var{f}$ can replace~$\Var{f}(x,z)$ by a term containing free

   614 occurrences of~$y$, since parameters are bound variables.

   615

   616 \subsection{Two quantifier proofs: a success and a failure}

   617 \index{examples!with quantifiers}

   618 Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an

   619 attempted proof of the non-theorem $\exists y.\forall x.x=y$.  The former

   620 proof succeeds, and the latter fails, because of the scope of quantified

   621 variables~\cite{paulson-found}.  Unification helps even in these trivial

   622 proofs.  In $\forall x.\exists y.x=y$ the $y$ that exists' is simply $x$,

   623 but we need never say so.  This choice is forced by the reflexive law for

   624 equality, and happens automatically.

   625

   626 \paragraph{The successful proof.}

   627 The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules

   628 $(\forall I)$ and~$(\exists I)$.  We state the goal and apply $(\forall I)$:

   629 \begin{ttbox}

   630 Goal "ALL x. EX y. x=y";

   631 {\out Level 0}

   632 {\out ALL x. EX y. x = y}

   633 {\out  1. ALL x. EX y. x = y}

   634 \ttbreak

   635 by (resolve_tac [allI] 1);

   636 {\out Level 1}

   637 {\out ALL x. EX y. x = y}

   638 {\out  1. !!x. EX y. x = y}

   639 \end{ttbox}

   640 The variable~\texttt{x} is no longer universally quantified, but is a

   641 parameter in the subgoal; thus, it is universally quantified at the

   642 meta-level.  The subgoal must be proved for all possible values of~\texttt{x}.

   643

   644 To remove the existential quantifier, we apply the rule $(\exists I)$:

   645 \begin{ttbox}

   646 by (resolve_tac [exI] 1);

   647 {\out Level 2}

   648 {\out ALL x. EX y. x = y}

   649 {\out  1. !!x. x = ?y1(x)}

   650 \end{ttbox}

   651 The bound variable \texttt{y} has become {\tt?y1(x)}.  This term consists of

   652 the function unknown~{\tt?y1} applied to the parameter~\texttt{x}.

   653 Instances of {\tt?y1(x)} may or may not contain~\texttt{x}.  We resolve the

   654 subgoal with the reflexivity axiom.

   655 \begin{ttbox}

   656 by (resolve_tac [refl] 1);

   657 {\out Level 3}

   658 {\out ALL x. EX y. x = y}

   659 {\out No subgoals!}

   660 \end{ttbox}

   661 Let us consider what has happened in detail.  The reflexivity axiom is

   662 lifted over~$x$ to become $\Forall x.\Var{f}(x)=\Var{f}(x)$, which is

   663 unified with $\Forall x.x=\Var{y@1}(x)$.  The function unknowns $\Var{f}$

   664 and~$\Var{y@1}$ are both instantiated to the identity function, and

   665 $x=\Var{y@1}(x)$ collapses to~$x=x$ by $\beta$-reduction.

   666

   667 \paragraph{The unsuccessful proof.}

   668 We state the goal $\exists y.\forall x.x=y$, which is not a theorem, and

   669 try~$(\exists I)$:

   670 \begin{ttbox}

   671 Goal "EX y. ALL x. x=y";

   672 {\out Level 0}

   673 {\out EX y. ALL x. x = y}

   674 {\out  1. EX y. ALL x. x = y}

   675 \ttbreak

   676 by (resolve_tac [exI] 1);

   677 {\out Level 1}

   678 {\out EX y. ALL x. x = y}

   679 {\out  1. ALL x. x = ?y}

   680 \end{ttbox}

   681 The unknown \texttt{?y} may be replaced by any term, but this can never

   682 introduce another bound occurrence of~\texttt{x}.  We now apply~$(\forall I)$:

   683 \begin{ttbox}

   684 by (resolve_tac [allI] 1);

   685 {\out Level 2}

   686 {\out EX y. ALL x. x = y}

   687 {\out  1. !!x. x = ?y}

   688 \end{ttbox}

   689 Compare our position with the previous Level~2.  Instead of {\tt?y1(x)} we

   690 have~{\tt?y}, whose instances may not contain the bound variable~\texttt{x}.

   691 The reflexivity axiom does not unify with subgoal~1.

   692 \begin{ttbox}

   693 by (resolve_tac [refl] 1);

   694 {\out by: tactic failed}

   695 \end{ttbox}

   696 There can be no proof of $\exists y.\forall x.x=y$ by the soundness of

   697 first-order logic.  I have elsewhere proved the faithfulness of Isabelle's

   698 encoding of first-order logic~\cite{paulson-found}; there could, of course, be

   699 faults in the implementation.

   700

   701

   702 \subsection{Nested quantifiers}

   703 \index{examples!with quantifiers}

   704 Multiple quantifiers create complex terms.  Proving

   705 $(\forall x\,y.P(x,y)) \imp (\forall z\,w.P(w,z))$

   706 will demonstrate how parameters and unknowns develop.  If they appear in

   707 the wrong order, the proof will fail.

   708

   709 This section concludes with a demonstration of \texttt{REPEAT}

   710 and~\texttt{ORELSE}.

   711 \begin{ttbox}

   712 Goal "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";

   713 {\out Level 0}

   714 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   715 {\out  1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   716 \ttbreak

   717 by (resolve_tac [impI] 1);

   718 {\out Level 1}

   719 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   720 {\out  1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}

   721 \end{ttbox}

   722

   723 \paragraph{The wrong approach.}

   724 Using \texttt{dresolve_tac}, we apply the rule $(\forall E)$, bound to the

   725 \ML\ identifier \tdx{spec}.  Then we apply $(\forall I)$.

   726 \begin{ttbox}

   727 by (dresolve_tac [spec] 1);

   728 {\out Level 2}

   729 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   730 {\out  1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)}

   731 \ttbreak

   732 by (resolve_tac [allI] 1);

   733 {\out Level 3}

   734 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   735 {\out  1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)}

   736 \end{ttbox}

   737 The unknown \texttt{?x1} and the parameter \texttt{z} have appeared.  We again

   738 apply $(\forall E)$ and~$(\forall I)$.

   739 \begin{ttbox}

   740 by (dresolve_tac [spec] 1);

   741 {\out Level 4}

   742 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   743 {\out  1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)}

   744 \ttbreak

   745 by (resolve_tac [allI] 1);

   746 {\out Level 5}

   747 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   748 {\out  1. !!z w. P(?x1,?y3(z)) ==> P(w,z)}

   749 \end{ttbox}

   750 The unknown \texttt{?y3} and the parameter \texttt{w} have appeared.  Each

   751 unknown is applied to the parameters existing at the time of its creation;

   752 instances of~\texttt{?x1} cannot contain~\texttt{z} or~\texttt{w}, while instances

   753 of {\tt?y3(z)} can only contain~\texttt{z}.  Due to the restriction on~\texttt{?x1},

   754 proof by assumption will fail.

   755 \begin{ttbox}

   756 by (assume_tac 1);

   757 {\out by: tactic failed}

   758 {\out uncaught exception ERROR}

   759 \end{ttbox}

   760

   761 \paragraph{The right approach.}

   762 To do this proof, the rules must be applied in the correct order.

   763 Parameters should be created before unknowns.  The

   764 \ttindex{choplev} command returns to an earlier stage of the proof;

   765 let us return to the result of applying~$({\imp}I)$:

   766 \begin{ttbox}

   767 choplev 1;

   768 {\out Level 1}

   769 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   770 {\out  1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}

   771 \end{ttbox}

   772 Previously we made the mistake of applying $(\forall E)$ before $(\forall I)$.

   773 \begin{ttbox}

   774 by (resolve_tac [allI] 1);

   775 {\out Level 2}

   776 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   777 {\out  1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)}

   778 \ttbreak

   779 by (resolve_tac [allI] 1);

   780 {\out Level 3}

   781 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   782 {\out  1. !!z w. ALL x y. P(x,y) ==> P(w,z)}

   783 \end{ttbox}

   784 The parameters \texttt{z} and~\texttt{w} have appeared.  We now create the

   785 unknowns:

   786 \begin{ttbox}

   787 by (dresolve_tac [spec] 1);

   788 {\out Level 4}

   789 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   790 {\out  1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)}

   791 \ttbreak

   792 by (dresolve_tac [spec] 1);

   793 {\out Level 5}

   794 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   795 {\out  1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)}

   796 \end{ttbox}

   797 Both {\tt?x3(z,w)} and~{\tt?y4(z,w)} could become any terms containing {\tt

   798 z} and~\texttt{w}:

   799 \begin{ttbox}

   800 by (assume_tac 1);

   801 {\out Level 6}

   802 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   803 {\out No subgoals!}

   804 \end{ttbox}

   805

   806 \paragraph{A one-step proof using tacticals.}

   807 \index{tacticals} \index{examples!of tacticals}

   808

   809 Repeated application of rules can be effective, but the rules should be

   810 attempted in the correct order.  Let us return to the original goal using

   811 \ttindex{choplev}:

   812 \begin{ttbox}

   813 choplev 0;

   814 {\out Level 0}

   815 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   816 {\out  1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   817 \end{ttbox}

   818 As we have just seen, \tdx{allI} should be attempted

   819 before~\tdx{spec}, while \ttindex{assume_tac} generally can be

   820 attempted first.  Such priorities can easily be expressed

   821 using~\ttindex{ORELSE}, and repeated using~\ttindex{REPEAT}.

   822 \begin{ttbox}

   823 by (REPEAT (assume_tac 1 ORELSE resolve_tac [impI,allI] 1

   824      ORELSE dresolve_tac [spec] 1));

   825 {\out Level 1}

   826 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}

   827 {\out No subgoals!}

   828 \end{ttbox}

   829

   830

   831 \subsection{A realistic quantifier proof}

   832 \index{examples!with quantifiers}

   833 To see the practical use of parameters and unknowns, let us prove half of

   834 the equivalence

   835 $(\forall x. P(x) \imp Q) \,\bimp\, ((\exists x. P(x)) \imp Q).$

   836 We state the left-to-right half to Isabelle in the normal way.

   837 Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we

   838 use \texttt{REPEAT}:

   839 \begin{ttbox}

   840 Goal "(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q";

   841 {\out Level 0}

   842 {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}

   843 {\out  1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}

   844 \ttbreak

   845 by (REPEAT (resolve_tac [impI] 1));

   846 {\out Level 1}

   847 {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}

   848 {\out  1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q}

   849 \end{ttbox}

   850 We can eliminate the universal or the existential quantifier.  The

   851 existential quantifier should be eliminated first, since this creates a

   852 parameter.  The rule~$(\exists E)$ is bound to the

   853 identifier~\tdx{exE}.

   854 \begin{ttbox}

   855 by (eresolve_tac [exE] 1);

   856 {\out Level 2}

   857 {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}

   858 {\out  1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q}

   859 \end{ttbox}

   860 The only possibility now is $(\forall E)$, a destruction rule.  We use

   861 \ttindex{dresolve_tac}, which discards the quantified assumption; it is

   862 only needed once.

   863 \begin{ttbox}

   864 by (dresolve_tac [spec] 1);

   865 {\out Level 3}

   866 {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}

   867 {\out  1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q}

   868 \end{ttbox}

   869 Because we applied $(\exists E)$ before $(\forall E)$, the unknown

   870 term~{\tt?x3(x)} may depend upon the parameter~\texttt{x}.

   871

   872 Although $({\imp}E)$ is a destruction rule, it works with

   873 \ttindex{eresolve_tac} to perform backward chaining.  This technique is

   874 frequently useful.

   875 \begin{ttbox}

   876 by (eresolve_tac [mp] 1);

   877 {\out Level 4}

   878 {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}

   879 {\out  1. !!x. P(x) ==> P(?x3(x))}

   880 \end{ttbox}

   881 The tactic has reduced~\texttt{Q} to~\texttt{P(?x3(x))}, deleting the

   882 implication.  The final step is trivial, thanks to the occurrence of~\texttt{x}.

   883 \begin{ttbox}

   884 by (assume_tac 1);

   885 {\out Level 5}

   886 {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}

   887 {\out No subgoals!}

   888 \end{ttbox}

   889

   890

   891 \subsection{The classical reasoner}

   892 \index{classical reasoner}

   893 Isabelle provides enough automation to tackle substantial examples.

   894 The classical

   895 reasoner can be set up for any classical natural deduction logic;

   896 see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%

   897         {Chap.\ts\ref{chap:classical}}.

   898 It cannot compete with fully automatic theorem provers, but it is

   899 competitive with tools found in other interactive provers.

   900

   901 Rules are packaged into {\bf classical sets}.  The classical reasoner

   902 provides several tactics, which apply rules using naive algorithms.

   903 Unification handles quantifiers as shown above.  The most useful tactic

   904 is~\ttindex{Blast_tac}.

   905

   906 Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}.  (The

   907 backslashes~\hbox{\verb|\|\ldots\verb|\|} are an \ML{} string escape

   908 sequence, to break the long string over two lines.)

   909 \begin{ttbox}

   910 Goal "(EX y. ALL x. J(y,x) <-> ~J(x,x))  \ttback

   911 \ttback       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";

   912 {\out Level 0}

   913 {\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}

   914 {\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}

   915 {\out  1. (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}

   916 {\out     ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}

   917 \end{ttbox}

   918 \ttindex{Blast_tac} proves subgoal~1 at a stroke.

   919 \begin{ttbox}

   920 by (Blast_tac 1);

   921 {\out Depth = 0}

   922 {\out Depth = 1}

   923 {\out Level 1}

   924 {\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}

   925 {\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}

   926 {\out No subgoals!}

   927 \end{ttbox}

   928 Sceptics may examine the proof by calling the package's single-step

   929 tactics, such as~\texttt{step_tac}.  This would take up much space, however,

   930 so let us proceed to the next example:

   931 \begin{ttbox}

   932 Goal "ALL x. P(x,f(x)) <-> \ttback

   933 \ttback       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";

   934 {\out Level 0}

   935 {\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}

   936 {\out  1. ALL x. P(x,f(x)) <->}

   937 {\out     (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}

   938 \end{ttbox}

   939 Again, subgoal~1 succumbs immediately.

   940 \begin{ttbox}

   941 by (Blast_tac 1);

   942 {\out Depth = 0}

   943 {\out Depth = 1}

   944 {\out Level 1}

   945 {\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}

   946 {\out No subgoals!}

   947 \end{ttbox}

   948 The classical reasoner is not restricted to the usual logical connectives.

   949 The natural deduction rules for unions and intersections resemble those for

   950 disjunction and conjunction.  The rules for infinite unions and

   951 intersections resemble those for quantifiers.  Given such rules, the classical

   952 reasoner is effective for reasoning in set theory.

   953