doc-src/Ref/classical.tex
author wenzelm
Sun Jul 23 12:01:05 2000 +0200 (2000-07-23)
changeset 9408 d3d56e1d2ec1
parent 8926 0c7f90147f5d
child 9439 a95343122ad0
permissions -rw-r--r--
classical atts now intro! / intro / intro?;
     1 %% $Id$
     2 \chapter{The Classical Reasoner}\label{chap:classical}
     3 \index{classical reasoner|(}
     4 \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
     5 
     6 Although Isabelle is generic, many users will be working in some
     7 extension of classical first-order logic.  
     8 Isabelle's set theory~{\tt ZF} is built upon theory~\texttt{FOL}, 
     9 while {\HOL} conceptually contains first-order logic as a fragment.
    10 Theorem-proving in predicate logic is undecidable, but many
    11 researchers have developed strategies to assist in this task.
    12 
    13 Isabelle's classical reasoner is an \ML{} functor that accepts certain
    14 information about a logic and delivers a suite of automatic tactics.  Each
    15 tactic takes a collection of rules and executes a simple, non-clausal proof
    16 procedure.  They are slow and simplistic compared with resolution theorem
    17 provers, but they can save considerable time and effort.  They can prove
    18 theorems such as Pelletier's~\cite{pelletier86} problems~40 and~41 in
    19 seconds:
    20 \[ (\exists y. \forall x. J(y,x) \bimp \neg J(x,x))  
    21    \imp  \neg (\forall x. \exists y. \forall z. J(z,y) \bimp \neg J(z,x)) \]
    22 \[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x))
    23    \imp \neg (\exists z. \forall x. F(x,z))  
    24 \]
    25 %
    26 The tactics are generic.  They are not restricted to first-order logic, and
    27 have been heavily used in the development of Isabelle's set theory.  Few
    28 interactive proof assistants provide this much automation.  The tactics can
    29 be traced, and their components can be called directly; in this manner,
    30 any proof can be viewed interactively.
    31 
    32 The simplest way to apply the classical reasoner (to subgoal~$i$) is to type
    33 \begin{ttbox}
    34 by (Blast_tac \(i\));
    35 \end{ttbox}
    36 This command quickly proves most simple formulas of the predicate calculus or
    37 set theory.  To attempt to prove subgoals using a combination of
    38 rewriting and classical reasoning, try
    39 \begin{ttbox}
    40 auto();                         \emph{\textrm{applies to all subgoals}}
    41 force i;                        \emph{\textrm{applies to one subgoal}}
    42 \end{ttbox}
    43 To do all obvious logical steps, even if they do not prove the
    44 subgoal, type one of the following:
    45 \begin{ttbox}
    46 by Safe_tac;                   \emph{\textrm{applies to all subgoals}}
    47 by (Clarify_tac \(i\));            \emph{\textrm{applies to one subgoal}}
    48 \end{ttbox}
    49 
    50 
    51 You need to know how the classical reasoner works in order to use it
    52 effectively.  There are many tactics to choose from, including 
    53 {\tt Fast_tac} and \texttt{Best_tac}.
    54 
    55 We shall first discuss the underlying principles, then present the
    56 classical reasoner.  Finally, we shall see how to instantiate it for new logics.
    57 The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already installed.
    58 
    59 
    60 \section{The sequent calculus}
    61 \index{sequent calculus}
    62 Isabelle supports natural deduction, which is easy to use for interactive
    63 proof.  But natural deduction does not easily lend itself to automation,
    64 and has a bias towards intuitionism.  For certain proofs in classical
    65 logic, it can not be called natural.  The {\bf sequent calculus}, a
    66 generalization of natural deduction, is easier to automate.
    67 
    68 A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$
    69 and~$\Delta$ are sets of formulae.%
    70 \footnote{For first-order logic, sequents can equivalently be made from
    71   lists or multisets of formulae.} The sequent
    72 \[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \]
    73 is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj
    74 Q@n$.  Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true,
    75 while $Q@1,\ldots,Q@n$ represent alternative goals.  A sequent is {\bf
    76 basic} if its left and right sides have a common formula, as in $P,Q\turn
    77 Q,R$; basic sequents are trivially valid.
    78 
    79 Sequent rules are classified as {\bf right} or {\bf left}, indicating which
    80 side of the $\turn$~symbol they operate on.  Rules that operate on the
    81 right side are analogous to natural deduction's introduction rules, and
    82 left rules are analogous to elimination rules.  
    83 Recall the natural deduction rules for
    84   first-order logic, 
    85 \iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%
    86                           {Fig.\ts\ref{fol-fig}}.
    87 The sequent calculus analogue of~$({\imp}I)$ is the rule
    88 $$
    89 \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
    90 \eqno({\imp}R)
    91 $$
    92 This breaks down some implication on the right side of a sequent; $\Gamma$
    93 and $\Delta$ stand for the sets of formulae that are unaffected by the
    94 inference.  The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the
    95 single rule 
    96 $$
    97 \ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}
    98 \eqno({\disj}R)
    99 $$
   100 This breaks down some disjunction on the right side, replacing it by both
   101 disjuncts.  Thus, the sequent calculus is a kind of multiple-conclusion logic.
   102 
   103 To illustrate the use of multiple formulae on the right, let us prove
   104 the classical theorem $(P\imp Q)\disj(Q\imp P)$.  Working backwards, we
   105 reduce this formula to a basic sequent:
   106 \[ \infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)}
   107    {\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;}
   108     {\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad}
   109                     {P, Q \turn Q, P\qquad\qquad}}}
   110 \]
   111 This example is typical of the sequent calculus: start with the desired
   112 theorem and apply rules backwards in a fairly arbitrary manner.  This yields a
   113 surprisingly effective proof procedure.  Quantifiers add few complications,
   114 since Isabelle handles parameters and schematic variables.  See Chapter~10
   115 of {\em ML for the Working Programmer}~\cite{paulson-ml2} for further
   116 discussion.
   117 
   118 
   119 \section{Simulating sequents by natural deduction}
   120 Isabelle can represent sequents directly, as in the object-logic~\texttt{LK}\@.
   121 But natural deduction is easier to work with, and most object-logics employ
   122 it.  Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn
   123 Q@1,\ldots,Q@n$ by the Isabelle formula
   124 \[ \List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1, \]
   125 where the order of the assumptions and the choice of~$Q@1$ are arbitrary.
   126 Elim-resolution plays a key role in simulating sequent proofs.
   127 
   128 We can easily handle reasoning on the left.
   129 As discussed in
   130 \iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}}, 
   131 elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$
   132 achieves a similar effect as the corresponding sequent rules.  For the
   133 other connectives, we use sequent-style elimination rules instead of
   134 destruction rules such as $({\conj}E1,2)$ and $(\forall E)$.  But note that
   135 the rule $(\neg L)$ has no effect under our representation of sequents!
   136 $$
   137 \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}\eqno({\neg}L)
   138 $$
   139 What about reasoning on the right?  Introduction rules can only affect the
   140 formula in the conclusion, namely~$Q@1$.  The other right-side formulae are
   141 represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.  
   142 \index{assumptions!negated}
   143 In order to operate on one of these, it must first be exchanged with~$Q@1$.
   144 Elim-resolution with the {\bf swap} rule has this effect:
   145 $$ \List{\neg P; \; \neg R\Imp P} \Imp R   \eqno(swap)  $$
   146 To ensure that swaps occur only when necessary, each introduction rule is
   147 converted into a swapped form: it is resolved with the second premise
   148 of~$(swap)$.  The swapped form of~$({\conj}I)$, which might be
   149 called~$({\neg\conj}E)$, is
   150 \[ \List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R. \]
   151 Similarly, the swapped form of~$({\imp}I)$ is
   152 \[ \List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R  \]
   153 Swapped introduction rules are applied using elim-resolution, which deletes
   154 the negated formula.  Our representation of sequents also requires the use
   155 of ordinary introduction rules.  If we had no regard for readability, we
   156 could treat the right side more uniformly by representing sequents as
   157 \[ \List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot. \]
   158 
   159 
   160 \section{Extra rules for the sequent calculus}
   161 As mentioned, destruction rules such as $({\conj}E1,2)$ and $(\forall E)$
   162 must be replaced by sequent-style elimination rules.  In addition, we need
   163 rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj
   164 Q$.  The introduction rules~$({\disj}I1,2)$ are replaced by a rule that
   165 simulates $({\disj}R)$:
   166 \[ (\neg Q\Imp P) \Imp P\disj Q \]
   167 The destruction rule $({\imp}E)$ is replaced by
   168 \[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \]
   169 Quantifier replication also requires special rules.  In classical logic,
   170 $\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules
   171 $(\exists R)$ and $(\forall L)$ are dual:
   172 \[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P}
   173           {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R)
   174    \qquad
   175    \ainfer{\forall x{.}P, \Gamma &\turn \Delta}
   176           {P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L)
   177 \]
   178 Thus both kinds of quantifier may be replicated.  Theorems requiring
   179 multiple uses of a universal formula are easy to invent; consider 
   180 \[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \]
   181 for any~$n>1$.  Natural examples of the multiple use of an existential
   182 formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$.
   183 
   184 Forgoing quantifier replication loses completeness, but gains decidability,
   185 since the search space becomes finite.  Many useful theorems can be proved
   186 without replication, and the search generally delivers its verdict in a
   187 reasonable time.  To adopt this approach, represent the sequent rules
   188 $(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists
   189 E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination
   190 form:
   191 $$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q    \eqno(\forall E@2) $$
   192 Elim-resolution with this rule will delete the universal formula after a
   193 single use.  To replicate universal quantifiers, replace the rule by
   194 $$
   195 \List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.
   196 \eqno(\forall E@3)
   197 $$
   198 To replicate existential quantifiers, replace $(\exists I)$ by
   199 \[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \]
   200 All introduction rules mentioned above are also useful in swapped form.
   201 
   202 Replication makes the search space infinite; we must apply the rules with
   203 care.  The classical reasoner distinguishes between safe and unsafe
   204 rules, applying the latter only when there is no alternative.  Depth-first
   205 search may well go down a blind alley; best-first search is better behaved
   206 in an infinite search space.  However, quantifier replication is too
   207 expensive to prove any but the simplest theorems.
   208 
   209 
   210 \section{Classical rule sets}
   211 \index{classical sets}
   212 Each automatic tactic takes a {\bf classical set} --- a collection of
   213 rules, classified as introduction or elimination and as {\bf safe} or {\bf
   214 unsafe}.  In general, safe rules can be attempted blindly, while unsafe
   215 rules must be used with care.  A safe rule must never reduce a provable
   216 goal to an unprovable set of subgoals.  
   217 
   218 The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$.  Any
   219 rule is unsafe whose premises contain new unknowns.  The elimination
   220 rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,
   221 which discards the assumption $\forall x{.}P(x)$ and replaces it by the
   222 weaker assumption~$P(\Var{t})$.  The rule $({\exists}I)$ is unsafe for
   223 similar reasons.  The rule~$(\forall E@3)$ is unsafe in a different sense:
   224 since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.
   225 In classical first-order logic, all rules are safe except those mentioned
   226 above.
   227 
   228 The safe/unsafe distinction is vague, and may be regarded merely as a way
   229 of giving some rules priority over others.  One could argue that
   230 $({\disj}E)$ is unsafe, because repeated application of it could generate
   231 exponentially many subgoals.  Induction rules are unsafe because inductive
   232 proofs are difficult to set up automatically.  Any inference is unsafe that
   233 instantiates an unknown in the proof state --- thus \ttindex{match_tac}
   234 must be used, rather than \ttindex{resolve_tac}.  Even proof by assumption
   235 is unsafe if it instantiates unknowns shared with other subgoals --- thus
   236 \ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.
   237 
   238 \subsection{Adding rules to classical sets}
   239 Classical rule sets belong to the abstract type \mltydx{claset}, which
   240 supports the following operations (provided the classical reasoner is
   241 installed!):
   242 \begin{ttbox} 
   243 empty_cs : claset
   244 print_cs : claset -> unit
   245 rep_cs : claset -> \{safeEs: thm list, safeIs: thm list,
   246                     hazEs: thm list,  hazIs: thm list, 
   247                     swrappers: (string * wrapper) list, 
   248                     uwrappers: (string * wrapper) list,
   249                     safe0_netpair: netpair, safep_netpair: netpair,
   250                     haz_netpair: netpair, dup_netpair: netpair\}
   251 addSIs   : claset * thm list -> claset                 \hfill{\bf infix 4}
   252 addSEs   : claset * thm list -> claset                 \hfill{\bf infix 4}
   253 addSDs   : claset * thm list -> claset                 \hfill{\bf infix 4}
   254 addIs    : claset * thm list -> claset                 \hfill{\bf infix 4}
   255 addEs    : claset * thm list -> claset                 \hfill{\bf infix 4}
   256 addDs    : claset * thm list -> claset                 \hfill{\bf infix 4}
   257 delrules : claset * thm list -> claset                 \hfill{\bf infix 4}
   258 \end{ttbox}
   259 The add operations ignore any rule already present in the claset with the same
   260 classification (such as safe introduction).  They print a warning if the rule
   261 has already been added with some other classification, but add the rule
   262 anyway.  Calling \texttt{delrules} deletes all occurrences of a rule from the
   263 claset, but see the warning below concerning destruction rules.
   264 \begin{ttdescription}
   265 \item[\ttindexbold{empty_cs}] is the empty classical set.
   266 
   267 \item[\ttindexbold{print_cs} $cs$] displays the printable contents of~$cs$,
   268   which is the rules. All other parts are non-printable.
   269 
   270 \item[\ttindexbold{rep_cs} $cs$] decomposes $cs$ as a record of its internal 
   271   components, namely the safe introduction and elimination rules, the unsafe
   272   introduction and elimination rules, the lists of safe and unsafe wrappers
   273   (see \ref{sec:modifying-search}), and the internalized forms of the rules.
   274 
   275 \item[$cs$ addSIs $rules$] \indexbold{*addSIs}
   276 adds safe introduction~$rules$ to~$cs$.
   277 
   278 \item[$cs$ addSEs $rules$] \indexbold{*addSEs}
   279 adds safe elimination~$rules$ to~$cs$.
   280 
   281 \item[$cs$ addSDs $rules$] \indexbold{*addSDs}
   282 adds safe destruction~$rules$ to~$cs$.
   283 
   284 \item[$cs$ addIs $rules$] \indexbold{*addIs}
   285 adds unsafe introduction~$rules$ to~$cs$.
   286 
   287 \item[$cs$ addEs $rules$] \indexbold{*addEs}
   288 adds unsafe elimination~$rules$ to~$cs$.
   289 
   290 \item[$cs$ addDs $rules$] \indexbold{*addDs}
   291 adds unsafe destruction~$rules$ to~$cs$.
   292 
   293 \item[$cs$ delrules $rules$] \indexbold{*delrules}
   294 deletes~$rules$ from~$cs$.  It prints a warning for those rules that are not
   295 in~$cs$.
   296 \end{ttdescription}
   297 
   298 \begin{warn}
   299   If you added $rule$ using \texttt{addSDs} or \texttt{addDs}, then you must delete
   300   it as follows:
   301 \begin{ttbox}
   302 \(cs\) delrules [make_elim \(rule\)]
   303 \end{ttbox}
   304 \par\noindent
   305 This is necessary because the operators \texttt{addSDs} and \texttt{addDs} convert
   306 the destruction rules to elimination rules by applying \ttindex{make_elim},
   307 and then insert them using \texttt{addSEs} and \texttt{addEs}, respectively.
   308 \end{warn}
   309 
   310 Introduction rules are those that can be applied using ordinary resolution.
   311 The classical set automatically generates their swapped forms, which will
   312 be applied using elim-resolution.  Elimination rules are applied using
   313 elim-resolution.  In a classical set, rules are sorted by the number of new
   314 subgoals they will yield; rules that generate the fewest subgoals will be
   315 tried first (see \S\ref{biresolve_tac}).
   316 
   317 For elimination and destruction rules there are variants of the add operations
   318 adding a rule in a way such that it is applied only if also its second premise
   319 can be unified with an assumption of the current proof state:
   320 \indexbold{*addSE2}\indexbold{*addSD2}\indexbold{*addE2}\indexbold{*addD2}
   321 \begin{ttbox}
   322 addSE2      : claset * (string * thm) -> claset           \hfill{\bf infix 4}
   323 addSD2      : claset * (string * thm) -> claset           \hfill{\bf infix 4}
   324 addE2       : claset * (string * thm) -> claset           \hfill{\bf infix 4}
   325 addD2       : claset * (string * thm) -> claset           \hfill{\bf infix 4}
   326 \end{ttbox}
   327 \begin{warn}
   328   A rule to be added in this special way must be given a name, which is used 
   329   to delete it again -- when desired -- using \texttt{delSWrappers} or 
   330   \texttt{delWrappers}, respectively. This is because these add operations
   331   are implemented as wrappers (see \ref{sec:modifying-search} below).
   332 \end{warn}
   333 
   334 
   335 \subsection{Modifying the search step}
   336 \label{sec:modifying-search}
   337 For a given classical set, the proof strategy is simple.  Perform as many safe
   338 inferences as possible; or else, apply certain safe rules, allowing
   339 instantiation of unknowns; or else, apply an unsafe rule.  The tactics also
   340 eliminate assumptions of the form $x=t$ by substitution if they have been set
   341 up to do so (see \texttt{hyp_subst_tacs} in~\S\ref{sec:classical-setup} below).
   342 They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$
   343 and~$P$, then replace $P\imp Q$ by~$Q$.
   344 
   345 The classical reasoning tactics --- except \texttt{blast_tac}! --- allow
   346 you to modify this basic proof strategy by applying two lists of arbitrary 
   347 {\bf wrapper tacticals} to it. 
   348 The first wrapper list, which is considered to contain safe wrappers only, 
   349 affects \ttindex{safe_step_tac} and all the tactics that call it.  
   350 The second one, which may contain unsafe wrappers, affects the unsafe parts
   351 of \ttindex{step_tac}, \ttindex{slow_step_tac}, and the tactics that call them.
   352 A wrapper transforms each step of the search, for example 
   353 by attempting other tactics before or after the original step tactic. 
   354 All members of a wrapper list are applied in turn to the respective step tactic.
   355 
   356 Initially the two wrapper lists are empty, which means no modification of the
   357 step tactics. Safe and unsafe wrappers are added to a claset 
   358 with the functions given below, supplying them with wrapper names. 
   359 These names may be used to selectively delete wrappers.
   360 
   361 \begin{ttbox} 
   362 type wrapper = (int -> tactic) -> (int -> tactic);
   363 
   364 addSWrapper  : claset * (string *  wrapper       ) -> claset \hfill{\bf infix 4}
   365 addSbefore   : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
   366 addSaltern   : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
   367 delSWrapper  : claset *  string                    -> claset \hfill{\bf infix 4}
   368 
   369 addWrapper   : claset * (string *  wrapper       ) -> claset \hfill{\bf infix 4}
   370 addbefore    : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
   371 addaltern    : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
   372 delWrapper   : claset *  string                    -> claset \hfill{\bf infix 4}
   373 
   374 addSss       : claset * simpset -> claset                 \hfill{\bf infix 4}
   375 addss        : claset * simpset -> claset                 \hfill{\bf infix 4}
   376 \end{ttbox}
   377 %
   378 
   379 \begin{ttdescription}
   380 \item[$cs$ addSWrapper $(name,wrapper)$] \indexbold{*addSWrapper}
   381 adds a new wrapper, which should yield a safe tactic, 
   382 to modify the existing safe step tactic.
   383 
   384 \item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore}
   385 adds the given tactic as a safe wrapper, such that it is tried 
   386 {\em before} each safe step of the search.
   387 
   388 \item[$cs$ addSaltern $(name,tac)$] \indexbold{*addSaltern}
   389 adds the given tactic as a safe wrapper, such that it is tried 
   390 when a safe step of the search would fail.
   391 
   392 \item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper}
   393 deletes the safe wrapper with the given name.
   394 
   395 \item[$cs$ addWrapper $(name,wrapper)$] \indexbold{*addWrapper}
   396 adds a new wrapper to modify the existing (unsafe) step tactic.
   397 
   398 \item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore}
   399 adds the given tactic as an unsafe wrapper, such that it its result is 
   400 concatenated {\em before} the result of each unsafe step.
   401 
   402 \item[$cs$ addaltern $(name,tac)$] \indexbold{*addaltern}
   403 adds the given tactic as an unsafe wrapper, such that it its result is 
   404 concatenated {\em after} the result of each unsafe step.
   405 
   406 \item[$cs$ delWrapper $name$] \indexbold{*delWrapper}
   407 deletes the unsafe wrapper with the given name.
   408 
   409 \item[$cs$ addSss $ss$] \indexbold{*addss}
   410 adds the simpset~$ss$ to the classical set.  The assumptions and goal will be
   411 simplified, in a rather safe way, after each safe step of the search.
   412 
   413 \item[$cs$ addss $ss$] \indexbold{*addss}
   414 adds the simpset~$ss$ to the classical set.  The assumptions and goal will be
   415 simplified, before the each unsafe step of the search.
   416 
   417 \end{ttdescription}
   418 
   419 \index{simplification!from classical reasoner} 
   420 Strictly speaking, the operators \texttt{addss} and \texttt{addSss}
   421 are not part of the classical reasoner.
   422 , which are used as primitives 
   423 for the automatic tactics described in \S\ref{sec:automatic-tactics}, are
   424 implemented as wrapper tacticals.
   425 they  
   426 \begin{warn}
   427 Being defined as wrappers, these operators are inappropriate for adding more 
   428 than one simpset at a time: the simpset added last overwrites any earlier ones.
   429 When a simpset combined with a claset is to be augmented, this should done 
   430 {\em before} combining it with the claset.
   431 \end{warn}
   432 
   433 
   434 \section{The classical tactics}
   435 \index{classical reasoner!tactics} If installed, the classical module provides
   436 powerful theorem-proving tactics.  Most of them have capitalized analogues
   437 that use the default claset; see \S\ref{sec:current-claset}.
   438 
   439 
   440 \subsection{The tableau prover}
   441 The tactic \texttt{blast_tac} searches for a proof using a fast tableau prover,
   442 coded directly in \ML.  It then reconstructs the proof using Isabelle
   443 tactics.  It is faster and more powerful than the other classical
   444 reasoning tactics, but has major limitations too.
   445 \begin{itemize}
   446 \item It does not use the wrapper tacticals described above, such as
   447   \ttindex{addss}.
   448 \item It ignores types, which can cause problems in \HOL.  If it applies a rule
   449   whose types are inappropriate, then proof reconstruction will fail.
   450 \item It does not perform higher-order unification, as needed by the rule {\tt
   451     rangeI} in {\HOL} and \texttt{RepFunI} in {\ZF}.  There are often
   452     alternatives to such rules, for example {\tt
   453     range_eqI} and \texttt{RepFun_eqI}.
   454 \item Function variables may only be applied to parameters of the subgoal.
   455 (This restriction arises because the prover does not use higher-order
   456 unification.)  If other function variables are present then the prover will
   457 fail with the message {\small\tt Function Var's argument not a bound variable}.
   458 \item Its proof strategy is more general than \texttt{fast_tac}'s but can be
   459   slower.  If \texttt{blast_tac} fails or seems to be running forever, try {\tt
   460   fast_tac} and the other tactics described below.
   461 \end{itemize}
   462 %
   463 \begin{ttbox} 
   464 blast_tac        : claset -> int -> tactic
   465 Blast.depth_tac  : claset -> int -> int -> tactic
   466 Blast.trace      : bool ref \hfill{\bf initially false}
   467 \end{ttbox}
   468 The two tactics differ on how they bound the number of unsafe steps used in a
   469 proof.  While \texttt{blast_tac} starts with a bound of zero and increases it
   470 successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound.
   471 \begin{ttdescription}
   472 \item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
   473   subgoal~$i$, increasing the search bound using iterative
   474   deepening~\cite{korf85}. 
   475   
   476 \item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
   477   to prove subgoal~$i$ using a search bound of $lim$.  Sometimes a slow
   478   proof using \texttt{blast_tac} can be made much faster by supplying the
   479   successful search bound to this tactic instead.
   480   
   481 \item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover}
   482   causes the tableau prover to print a trace of its search.  At each step it
   483   displays the formula currently being examined and reports whether the branch
   484   has been closed, extended or split.
   485 \end{ttdescription}
   486 
   487 
   488 \subsection{Automatic tactics}\label{sec:automatic-tactics}
   489 \begin{ttbox} 
   490 type clasimpset = claset * simpset;
   491 auto_tac        : clasimpset ->        tactic
   492 force_tac       : clasimpset -> int -> tactic
   493 auto            : unit -> unit
   494 force           : int  -> unit
   495 \end{ttbox}
   496 The automatic tactics attempt to prove goals using a combination of
   497 simplification and classical reasoning. 
   498 \begin{ttdescription}
   499 \item[\ttindexbold{auto_tac $(cs,ss)$}] is intended for situations where 
   500 there are a lot of mostly trivial subgoals; it proves all the easy ones, 
   501 leaving the ones it cannot prove.
   502 (Unfortunately, attempting to prove the hard ones may take a long time.)  
   503 \item[\ttindexbold{force_tac} $(cs,ss)$ $i$] is intended to prove subgoal~$i$ 
   504 completely. It tries to apply all fancy tactics it knows about, 
   505 performing a rather exhaustive search.
   506 \end{ttdescription}
   507 They must be supplied both a simpset and a claset; therefore 
   508 they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which 
   509 use the default claset and simpset (see \S\ref{sec:current-claset} below). 
   510 For interactive use, 
   511 the shorthand \texttt{auto();} abbreviates \texttt{by Auto_tac;} 
   512 while \texttt{force 1;} abbreviates \texttt{by (Force_tac 1);}
   513 
   514 
   515 \subsection{Semi-automatic tactics}
   516 \begin{ttbox} 
   517 clarify_tac      : claset -> int -> tactic
   518 clarify_step_tac : claset -> int -> tactic
   519 clarsimp_tac     : clasimpset -> int -> tactic
   520 \end{ttbox}
   521 Use these when the automatic tactics fail.  They perform all the obvious
   522 logical inferences that do not split the subgoal.  The result is a
   523 simpler subgoal that can be tackled by other means, such as by
   524 instantiating quantifiers yourself.
   525 \begin{ttdescription}
   526 \item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on
   527 subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}.
   528 \item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
   529   subgoal~$i$.  No splitting step is applied; for example, the subgoal $A\conj
   530   B$ is left as a conjunction.  Proof by assumption, Modus Ponens, etc., may be
   531   performed provided they do not instantiate unknowns.  Assumptions of the
   532   form $x=t$ may be eliminated.  The user-supplied safe wrapper tactical is
   533   applied.
   534 \item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but
   535 also does simplification with the given simpset. note that if the simpset 
   536 includes a splitter for the premises, the subgoal may still be split.
   537 \end{ttdescription}
   538 
   539 
   540 \subsection{Other classical tactics}
   541 \begin{ttbox} 
   542 fast_tac      : claset -> int -> tactic
   543 best_tac      : claset -> int -> tactic
   544 slow_tac      : claset -> int -> tactic
   545 slow_best_tac : claset -> int -> tactic
   546 \end{ttbox}
   547 These tactics attempt to prove a subgoal using sequent-style reasoning.
   548 Unlike \texttt{blast_tac}, they construct proofs directly in Isabelle.  Their
   549 effect is restricted (by \texttt{SELECT_GOAL}) to one subgoal; they either prove
   550 this subgoal or fail.  The \texttt{slow_} versions conduct a broader
   551 search.%
   552 \footnote{They may, when backtracking from a failed proof attempt, undo even
   553   the step of proving a subgoal by assumption.}
   554 
   555 The best-first tactics are guided by a heuristic function: typically, the
   556 total size of the proof state.  This function is supplied in the functor call
   557 that sets up the classical reasoner.
   558 \begin{ttdescription}
   559 \item[\ttindexbold{fast_tac} $cs$ $i$] applies \texttt{step_tac} using
   560 depth-first search to prove subgoal~$i$.
   561 
   562 \item[\ttindexbold{best_tac} $cs$ $i$] applies \texttt{step_tac} using
   563 best-first search to prove subgoal~$i$.
   564 
   565 \item[\ttindexbold{slow_tac} $cs$ $i$] applies \texttt{slow_step_tac} using
   566 depth-first search to prove subgoal~$i$.
   567 
   568 \item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with
   569 best-first search to prove subgoal~$i$.
   570 \end{ttdescription}
   571 
   572 
   573 \subsection{Depth-limited automatic tactics}
   574 \begin{ttbox} 
   575 depth_tac  : claset -> int -> int -> tactic
   576 deepen_tac : claset -> int -> int -> tactic
   577 \end{ttbox}
   578 These work by exhaustive search up to a specified depth.  Unsafe rules are
   579 modified to preserve the formula they act on, so that it be used repeatedly.
   580 They can prove more goals than \texttt{fast_tac} can but are much
   581 slower, for example if the assumptions have many universal quantifiers.
   582 
   583 The depth limits the number of unsafe steps.  If you can estimate the minimum
   584 number of unsafe steps needed, supply this value as~$m$ to save time.
   585 \begin{ttdescription}
   586 \item[\ttindexbold{depth_tac} $cs$ $m$ $i$] 
   587 tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.
   588 
   589 \item[\ttindexbold{deepen_tac} $cs$ $m$ $i$] 
   590 tries to prove subgoal~$i$ by iterative deepening.  It calls \texttt{depth_tac}
   591 repeatedly with increasing depths, starting with~$m$.
   592 \end{ttdescription}
   593 
   594 
   595 \subsection{Single-step tactics}
   596 \begin{ttbox} 
   597 safe_step_tac : claset -> int -> tactic
   598 safe_tac      : claset        -> tactic
   599 inst_step_tac : claset -> int -> tactic
   600 step_tac      : claset -> int -> tactic
   601 slow_step_tac : claset -> int -> tactic
   602 \end{ttbox}
   603 The automatic proof procedures call these tactics.  By calling them
   604 yourself, you can execute these procedures one step at a time.
   605 \begin{ttdescription}
   606 \item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
   607   subgoal~$i$.  The safe wrapper tacticals are applied to a tactic that may
   608   include proof by assumption or Modus Ponens (taking care not to instantiate
   609   unknowns), or substitution.
   610 
   611 \item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all 
   612 subgoals.  It is deterministic, with at most one outcome.  
   613 
   614 \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
   615 but allows unknowns to be instantiated.
   616 
   617 \item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
   618   procedure.  The unsafe wrapper tacticals are applied to a tactic that tries
   619   \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule
   620   from~$cs$.
   621 
   622 \item[\ttindexbold{slow_step_tac}] 
   623   resembles \texttt{step_tac}, but allows backtracking between using safe
   624   rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules.
   625   The resulting search space is larger.
   626 \end{ttdescription}
   627 
   628 
   629 \subsection{The current claset}\label{sec:current-claset}
   630 
   631 Each theory is equipped with an implicit \emph{current claset}
   632 \index{claset!current}.  This is a default set of classical
   633 rules.  The underlying idea is quite similar to that of a current
   634 simpset described in \S\ref{sec:simp-for-dummies}; please read that
   635 section, including its warnings.  
   636 
   637 The tactics
   638 \begin{ttbox}
   639 Blast_tac        : int -> tactic
   640 Auto_tac         :        tactic
   641 Force_tac        : int -> tactic
   642 Fast_tac         : int -> tactic
   643 Best_tac         : int -> tactic
   644 Deepen_tac       : int -> int -> tactic
   645 Clarify_tac      : int -> tactic
   646 Clarify_step_tac : int -> tactic
   647 Clarsimp_tac     : int -> tactic
   648 Safe_tac         :        tactic
   649 Safe_step_tac    : int -> tactic
   650 Step_tac         : int -> tactic
   651 \end{ttbox}
   652 \indexbold{*Blast_tac}\indexbold{*Auto_tac}\indexbold{*Force_tac}
   653 \indexbold{*Best_tac}\indexbold{*Fast_tac}%
   654 \indexbold{*Deepen_tac}
   655 \indexbold{*Clarify_tac}\indexbold{*Clarify_step_tac}\indexbold{*Clarsimp_tac}
   656 \indexbold{*Safe_tac}\indexbold{*Safe_step_tac}
   657 \indexbold{*Step_tac}
   658 make use of the current claset.  For example, \texttt{Blast_tac} is defined as 
   659 \begin{ttbox}
   660 fun Blast_tac i st = blast_tac (claset()) i st;
   661 \end{ttbox}
   662 and gets the current claset, only after it is applied to a proof state.  
   663 The functions
   664 \begin{ttbox}
   665 AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit
   666 \end{ttbox}
   667 \indexbold{*AddSIs} \indexbold{*AddSEs} \indexbold{*AddSDs}
   668 \indexbold{*AddIs} \indexbold{*AddEs} \indexbold{*AddDs}
   669 are used to add rules to the current claset.  They work exactly like their
   670 lower case counterparts, such as \texttt{addSIs}.  Calling
   671 \begin{ttbox}
   672 Delrules : thm list -> unit
   673 \end{ttbox}
   674 deletes rules from the current claset. 
   675 
   676 \medskip A few further functions are available as uppercase versions only:
   677 \begin{ttbox}
   678 AddXIs, AddXEs, AddXDs: thm list -> unit
   679 \end{ttbox}
   680 \indexbold{*AddXIs} \indexbold{*AddXEs} \indexbold{*AddXDs} augment the
   681 current claset by \emph{extra} introduction, elimination, or destruct rules.
   682 These provide additional hints for the basic non-automated proof methods of
   683 Isabelle/Isar \cite{isabelle-isar-ref}.  The corresponding Isar attributes are
   684 ``$intro?$'', ``$elim?$'', and ``$dest?$''.  Note that these extra rules do
   685 not have any effect on classic Isabelle tactics.
   686 
   687 
   688 \subsection{Accessing the current claset}
   689 \label{sec:access-current-claset}
   690 
   691 the functions to access the current claset are analogous to the functions 
   692 for the current simpset, so please see \ref{sec:access-current-simpset}
   693 for a description.
   694 \begin{ttbox}
   695 claset        : unit   -> claset
   696 claset_ref    : unit   -> claset ref
   697 claset_of     : theory -> claset
   698 claset_ref_of : theory -> claset ref
   699 print_claset  : theory -> unit
   700 CLASET        :(claset     ->       tactic) ->       tactic
   701 CLASET'       :(claset     -> 'a -> tactic) -> 'a -> tactic
   702 CLASIMPSET    :(clasimpset ->       tactic) ->       tactic
   703 CLASIMPSET'   :(clasimpset -> 'a -> tactic) -> 'a -> tactic
   704 \end{ttbox}
   705 
   706 
   707 \subsection{Other useful tactics}
   708 \index{tactics!for contradiction}
   709 \index{tactics!for Modus Ponens}
   710 \begin{ttbox} 
   711 contr_tac    :             int -> tactic
   712 mp_tac       :             int -> tactic
   713 eq_mp_tac    :             int -> tactic
   714 swap_res_tac : thm list -> int -> tactic
   715 \end{ttbox}
   716 These can be used in the body of a specialized search.
   717 \begin{ttdescription}
   718 \item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}
   719   solves subgoal~$i$ by detecting a contradiction among two assumptions of
   720   the form $P$ and~$\neg P$, or fail.  It may instantiate unknowns.  The
   721   tactic can produce multiple outcomes, enumerating all possible
   722   contradictions.
   723 
   724 \item[\ttindexbold{mp_tac} {\it i}] 
   725 is like \texttt{contr_tac}, but also attempts to perform Modus Ponens in
   726 subgoal~$i$.  If there are assumptions $P\imp Q$ and~$P$, then it replaces
   727 $P\imp Q$ by~$Q$.  It may instantiate unknowns.  It fails if it can do
   728 nothing.
   729 
   730 \item[\ttindexbold{eq_mp_tac} {\it i}] 
   731 is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
   732 is safe.
   733 
   734 \item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
   735 the proof state using {\it thms}, which should be a list of introduction
   736 rules.  First, it attempts to prove the goal using \texttt{assume_tac} or
   737 \texttt{contr_tac}.  It then attempts to apply each rule in turn, attempting
   738 resolution and also elim-resolution with the swapped form.
   739 \end{ttdescription}
   740 
   741 \subsection{Creating swapped rules}
   742 \begin{ttbox} 
   743 swapify   : thm list -> thm list
   744 joinrules : thm list * thm list -> (bool * thm) list
   745 \end{ttbox}
   746 \begin{ttdescription}
   747 \item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the
   748 swapped versions of~{\it thms}, regarded as introduction rules.
   749 
   750 \item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]
   751 joins introduction rules, their swapped versions, and elimination rules for
   752 use with \ttindex{biresolve_tac}.  Each rule is paired with~\texttt{false}
   753 (indicating ordinary resolution) or~\texttt{true} (indicating
   754 elim-resolution).
   755 \end{ttdescription}
   756 
   757 
   758 \section{Setting up the classical reasoner}\label{sec:classical-setup}
   759 \index{classical reasoner!setting up}
   760 Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL}, 
   761 have the classical reasoner already set up.  
   762 When defining a new classical logic, you should set up the reasoner yourself.  
   763 It consists of the \ML{} functor \ttindex{ClassicalFun}, which takes the 
   764 argument signature \texttt{CLASSICAL_DATA}:
   765 \begin{ttbox} 
   766 signature CLASSICAL_DATA =
   767   sig
   768   val mp             : thm
   769   val not_elim       : thm
   770   val swap           : thm
   771   val sizef          : thm -> int
   772   val hyp_subst_tacs : (int -> tactic) list
   773   end;
   774 \end{ttbox}
   775 Thus, the functor requires the following items:
   776 \begin{ttdescription}
   777 \item[\tdxbold{mp}] should be the Modus Ponens rule
   778 $\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
   779 
   780 \item[\tdxbold{not_elim}] should be the contradiction rule
   781 $\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.
   782 
   783 \item[\tdxbold{swap}] should be the swap rule
   784 $\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.
   785 
   786 \item[\ttindexbold{sizef}] is the heuristic function used for best-first
   787 search.  It should estimate the size of the remaining subgoals.  A good
   788 heuristic function is \ttindex{size_of_thm}, which measures the size of the
   789 proof state.  Another size function might ignore certain subgoals (say,
   790 those concerned with type-checking).  A heuristic function might simply
   791 count the subgoals.
   792 
   793 \item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
   794 the hypotheses, typically created by \ttindex{HypsubstFun} (see
   795 Chapter~\ref{substitution}).  This list can, of course, be empty.  The
   796 tactics are assumed to be safe!
   797 \end{ttdescription}
   798 The functor is not at all sensitive to the formalization of the
   799 object-logic.  It does not even examine the rules, but merely applies
   800 them according to its fixed strategy.  The functor resides in {\tt
   801   Provers/classical.ML} in the Isabelle sources.
   802 
   803 \index{classical reasoner|)}
   804 
   805 \section{Setting up the combination with the simplifier}
   806 \label{sec:clasimp-setup}
   807 
   808 To combine the classical reasoner and the simplifier, we simply call the 
   809 \ML{} functor \ttindex{ClasimpFun} that assembles the parts as required. 
   810 It takes a structure (of signature \texttt{CLASIMP_DATA}) as
   811 argment, which can be contructed on the fly:
   812 \begin{ttbox}
   813 structure Clasimp = ClasimpFun
   814  (structure Simplifier = Simplifier 
   815         and Classical  = Classical 
   816         and Blast      = Blast);
   817 \end{ttbox}
   818 %
   819 %%% Local Variables: 
   820 %%% mode: latex
   821 %%% TeX-master: "ref"
   822 %%% End: