doc-src/Intro/getting.tex
author aspinall
Sun Dec 31 15:34:21 2006 +0100 (2006-12-31)
changeset 21973 e7c9b0d3ce82
parent 14148 6580d374a509
child 42637 381fdcab0f36
permissions -rw-r--r--
Quote arguments in PGIP exceptions. Tune comment.
     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