%% $Id$

\chapter{The Classical Reasoner}\label{chap:classical}

\index{classical reasoner|(}

\newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}

Although Isabelle is generic, many users will be working in some

extension of classical first-order logic.  Isabelle's set theory~{\tt

  ZF} is built upon theory~{\tt FOL}, while higher-order logic

conceptually contains first-order logic as a fragment.

Theorem-proving in predicate logic is undecidable, but many

researchers have developed strategies to assist in this task.

Isabelle's classical reasoner is an \ML{} functor that accepts certain

information about a logic and delivers a suite of automatic tactics.  Each

tactic takes a collection of rules and executes a simple, non-clausal proof

procedure.  They are slow and simplistic compared with resolution theorem

provers, but they can save considerable time and effort.  They can prove

theorems such as Pelletier's~\cite{pelletier86} problems~40 and~41 in

seconds:

\[ (\exists y. \forall x. J(y,x) \bimp \neg J(x,x))  

   \imp  \neg (\forall x. \exists y. \forall z. J(z,y) \bimp \neg J(z,x)) \]

\[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x))

   \imp \neg (\exists z. \forall x. F(x,z))  

\]

%

The tactics are generic.  They are not restricted to first-order logic, and

have been heavily used in the development of Isabelle's set theory.  Few

interactive proof assistants provide this much automation.  The tactics can

be traced, and their components can be called directly; in this manner,

any proof can be viewed interactively.

The simplest way to apply the classical reasoner (to subgoal~$i$) is as

follows:

\begin{ttbox}

by (Blast_tac \(i\));

\end{ttbox}

If the subgoal is a simple formula of the predicate calculus or set theory,

then it should be proved quickly.  However, to use the classical reasoner

effectively, you need to know how it works and how to choose among the many

tactics available, including {\tt Fast_tac} and {\tt Best_tac}.

We shall first discuss the underlying principles, then present the

classical reasoner.  Finally, we shall see how to instantiate it for

new logics.  The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already

installed.

\section{The sequent calculus}

\index{sequent calculus}

Isabelle supports natural deduction, which is easy to use for interactive

proof.  But natural deduction does not easily lend itself to automation,

and has a bias towards intuitionism.  For certain proofs in classical

logic, it can not be called natural.  The {\bf sequent calculus}, a

generalization of natural deduction, is easier to automate.

A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$

and~$\Delta$ are sets of formulae.%

\footnote{For first-order logic, sequents can equivalently be made from

  lists or multisets of formulae.} The sequent

\[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \]

is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj

Q@n$.  Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true,

while $Q@1,\ldots,Q@n$ represent alternative goals.  A sequent is {\bf

basic} if its left and right sides have a common formula, as in $P,Q\turn

Q,R$; basic sequents are trivially valid.

Sequent rules are classified as {\bf right} or {\bf left}, indicating which

side of the $\turn$~symbol they operate on.  Rules that operate on the

right side are analogous to natural deduction's introduction rules, and

left rules are analogous to elimination rules.  

Recall the natural deduction rules for

  first-order logic, 

\iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%

                          {Fig.\ts\ref{fol-fig}}.

The sequent calculus analogue of~$({\imp}I)$ is the rule

$$

\ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}

\eqno({\imp}R)

$$

This breaks down some implication on the right side of a sequent; $\Gamma$

and $\Delta$ stand for the sets of formulae that are unaffected by the

inference.  The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the

single rule 

$$

\ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}

\eqno({\disj}R)

$$

This breaks down some disjunction on the right side, replacing it by both

disjuncts.  Thus, the sequent calculus is a kind of multiple-conclusion logic.

To illustrate the use of multiple formulae on the right, let us prove

the classical theorem $(P\imp Q)\disj(Q\imp P)$.  Working backwards, we

reduce this formula to a basic sequent:

\[ \infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)}

   {\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;}

    {\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad}

                    {P, Q \turn Q, P\qquad\qquad}}}

\]

This example is typical of the sequent calculus: start with the desired

theorem and apply rules backwards in a fairly arbitrary manner.  This yields a

surprisingly effective proof procedure.  Quantifiers add few complications,

since Isabelle handles parameters and schematic variables.  See Chapter~10

of {\em ML for the Working Programmer}~\cite{paulson91} for further

discussion.

\section{Simulating sequents by natural deduction}

Isabelle can represent sequents directly, as in the object-logic~{\tt LK}\@.

But natural deduction is easier to work with, and most object-logics employ

it.  Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn

Q@1,\ldots,Q@n$ by the Isabelle formula

\[ \List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1, \]

where the order of the assumptions and the choice of~$Q@1$ are arbitrary.

Elim-resolution plays a key role in simulating sequent proofs.

We can easily handle reasoning on the left.

As discussed in

\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}}, 

elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$

achieves a similar effect as the corresponding sequent rules.  For the

other connectives, we use sequent-style elimination rules instead of

destruction rules such as $({\conj}E1,2)$ and $(\forall E)$.  But note that

the rule $(\neg L)$ has no effect under our representation of sequents!

$$

\ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}\eqno({\neg}L)

$$

What about reasoning on the right?  Introduction rules can only affect the

formula in the conclusion, namely~$Q@1$.  The other right-side formulae are

represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.  

\index{assumptions!negated}

In order to operate on one of these, it must first be exchanged with~$Q@1$.

Elim-resolution with the {\bf swap} rule has this effect:

$$ \List{\neg P; \; \neg R\Imp P} \Imp R   \eqno(swap)  $$

To ensure that swaps occur only when necessary, each introduction rule is

converted into a swapped form: it is resolved with the second premise

of~$(swap)$.  The swapped form of~$({\conj}I)$, which might be

called~$({\neg\conj}E)$, is

\[ \List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R. \]

Similarly, the swapped form of~$({\imp}I)$ is

\[ \List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R  \]

Swapped introduction rules are applied using elim-resolution, which deletes

the negated formula.  Our representation of sequents also requires the use

of ordinary introduction rules.  If we had no regard for readability, we

could treat the right side more uniformly by representing sequents as

\[ \List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot. \]

\section{Extra rules for the sequent calculus}

As mentioned, destruction rules such as $({\conj}E1,2)$ and $(\forall E)$

must be replaced by sequent-style elimination rules.  In addition, we need

rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj

Q$.  The introduction rules~$({\disj}I1,2)$ are replaced by a rule that

simulates $({\disj}R)$:

\[ (\neg Q\Imp P) \Imp P\disj Q \]

The destruction rule $({\imp}E)$ is replaced by

\[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \]

Quantifier replication also requires special rules.  In classical logic,

$\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules

$(\exists R)$ and $(\forall L)$ are dual:

\[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P}

          {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R)

   \qquad

   \ainfer{\forall x{.}P, \Gamma &\turn \Delta}

          {P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L)

\]

Thus both kinds of quantifier may be replicated.  Theorems requiring

multiple uses of a universal formula are easy to invent; consider 

\[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \]

for any~$n>1$.  Natural examples of the multiple use of an existential

formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$.

Forgoing quantifier replication loses completeness, but gains decidability,

since the search space becomes finite.  Many useful theorems can be proved

without replication, and the search generally delivers its verdict in a

reasonable time.  To adopt this approach, represent the sequent rules

$(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists

E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination

form:

$$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q    \eqno(\forall E@2) $$

Elim-resolution with this rule will delete the universal formula after a

single use.  To replicate universal quantifiers, replace the rule by

$$

\List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.

\eqno(\forall E@3)

$$

To replicate existential quantifiers, replace $(\exists I)$ by

\[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \]

All introduction rules mentioned above are also useful in swapped form.

Replication makes the search space infinite; we must apply the rules with

care.  The classical reasoner distinguishes between safe and unsafe

rules, applying the latter only when there is no alternative.  Depth-first

search may well go down a blind alley; best-first search is better behaved

in an infinite search space.  However, quantifier replication is too

expensive to prove any but the simplest theorems.

\section{Classical rule sets}

\index{classical sets}

Each automatic tactic takes a {\bf classical set} --- a collection of

rules, classified as introduction or elimination and as {\bf safe} or {\bf

unsafe}.  In general, safe rules can be attempted blindly, while unsafe

rules must be used with care.  A safe rule must never reduce a provable

goal to an unprovable set of subgoals.  

The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$.  Any

rule is unsafe whose premises contain new unknowns.  The elimination

rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,

which discards the assumption $\forall x{.}P(x)$ and replaces it by the

weaker assumption~$P(\Var{t})$.  The rule $({\exists}I)$ is unsafe for

similar reasons.  The rule~$(\forall E@3)$ is unsafe in a different sense:

since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.

In classical first-order logic, all rules are safe except those mentioned

above.

The safe/unsafe distinction is vague, and may be regarded merely as a way

of giving some rules priority over others.  One could argue that

$({\disj}E)$ is unsafe, because repeated application of it could generate

exponentially many subgoals.  Induction rules are unsafe because inductive

proofs are difficult to set up automatically.  Any inference is unsafe that

instantiates an unknown in the proof state --- thus \ttindex{match_tac}

must be used, rather than \ttindex{resolve_tac}.  Even proof by assumption

is unsafe if it instantiates unknowns shared with other subgoals --- thus

\ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.

\subsection{Adding rules to classical sets}

Classical rule sets belong to the abstract type \mltydx{claset}, which

supports the following operations (provided the classical reasoner is

installed!):

\begin{ttbox} 

empty_cs    : claset

print_cs    : claset -> unit

addSIs      : claset * thm list -> claset                 \hfill{\bf infix 4}

addSEs      : claset * thm list -> claset                 \hfill{\bf infix 4}

addSDs      : claset * thm list -> claset                 \hfill{\bf infix 4}

addIs       : claset * thm list -> claset                 \hfill{\bf infix 4}

addEs       : claset * thm list -> claset                 \hfill{\bf infix 4}

addDs       : claset * thm list -> claset                 \hfill{\bf infix 4}

delrules    : claset * thm list -> claset                 \hfill{\bf infix 4}

\end{ttbox}

The add operations ignore any rule already present in the claset with the same

classification (such as Safe Introduction).  They print a warning if the rule

has already been added with some other classification, but add the rule

anyway.  Calling {\tt delrules} deletes all occurrences of a rule from the

claset, but see the warning below concerning destruction rules.

\begin{ttdescription}

\item[\ttindexbold{empty_cs}] is the empty classical set.

\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.

\item[$cs$ addSIs $rules$] \indexbold{*addSIs}

adds safe introduction~$rules$ to~$cs$.

\item[$cs$ addSEs $rules$] \indexbold{*addSEs}

adds safe elimination~$rules$ to~$cs$.

\item[$cs$ addSDs $rules$] \indexbold{*addSDs}

adds safe destruction~$rules$ to~$cs$.

\item[$cs$ addIs $rules$] \indexbold{*addIs}

adds unsafe introduction~$rules$ to~$cs$.

\item[$cs$ addEs $rules$] \indexbold{*addEs}

adds unsafe elimination~$rules$ to~$cs$.

\item[$cs$ addDs $rules$] \indexbold{*addDs}

adds unsafe destruction~$rules$ to~$cs$.

\item[$cs$ delrules $rules$] \indexbold{*delrules}

deletes~$rules$ from~$cs$.  It prints a warning for those rules that are not

in~$cs$.

\end{ttdescription}

\begin{warn}

  If you added $rule$ using {\tt addSDs} or {\tt addDs}, then you must delete

  it as follows:

\begin{ttbox}

\(cs\) delrules [make_elim \(rule\)]

\end{ttbox}

\par\noindent

This is necessary because the operators {\tt addSDs} and {\tt addDs} convert

the destruction rules to elimination rules by applying \ttindex{make_elim},

and then insert them using {\tt addSEs} and {\tt addEs}, respectively.

\end{warn}

Introduction rules are those that can be applied using ordinary resolution.

The classical set automatically generates their swapped forms, which will

be applied using elim-resolution.  Elimination rules are applied using

elim-resolution.  In a classical set, rules are sorted by the number of new

subgoals they will yield; rules that generate the fewest subgoals will be

tried first (see \S\ref{biresolve_tac}).

\subsection{Modifying the search step}

For a given classical set, the proof strategy is simple.  Perform as many

safe inferences as possible; or else, apply certain safe rules, allowing

instantiation of unknowns; or else, apply an unsafe rule.  The tactics may

also apply {\tt hyp_subst_tac}, if they have been set up to do so (see

below).  They may perform a form of Modus Ponens: if there are assumptions

$P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$.

The classical reasoning tactics --- except {\tt blast_tac}! --- allow

you to modify this basic proof strategy by applying two arbitrary {\bf

  wrapper tacticals} to it. This affects each step of the search.

Usually they are the identity tacticals, but they could apply another

tactic before or after the step tactic. The first one, which is

considered to be safe, affects \ttindex{safe_step_tac} and all the

tactics that call it. The the second one, which may be unsafe, affects

\ttindex{step_tac}, \ttindex{slow_step_tac} and the tactics that call

them.

\begin{ttbox} 

addss        : claset * simpset -> claset                 \hfill{\bf infix 4}

addSbefore   : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}

addSaltern   : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}

setSWrapper  : claset * ((int -> tactic) -> 

                         (int -> tactic)) -> claset       \hfill{\bf infix 4}

compSWrapper : claset * ((int -> tactic) -> 

                         (int -> tactic)) -> claset       \hfill{\bf infix 4}

addbefore    : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}

addaltern    : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}

setWrapper   : claset * ((int -> tactic) -> 

                         (int -> tactic)) -> claset       \hfill{\bf infix 4}

compWrapper  : claset * ((int -> tactic) -> 

                         (int -> tactic)) -> claset       \hfill{\bf infix 4}

\end{ttbox}

%

\index{simplification!from classical reasoner} The wrapper tacticals

underly the operator addss, which combines each search step by

simplification.  Strictly speaking, {\tt addss} is not part of the

classical reasoner.  It should be defined (using {\tt addSaltern

  (CHANGED o (safe_asm_more_full_simp_tac ss)}) when the simplifier is

installed.

\begin{ttdescription}

\item[$cs$ addss $ss$] \indexbold{*addss}

adds the simpset~$ss$ to the classical set. The assumptions and goal will be

simplified, in a safe way, after the safe steps of the search.

\item[$cs$ addSbefore $tac$] \indexbold{*addSbefore}

changes the safe wrapper tactical to apply the given tactic {\em before}

each safe step of the search.

\item[$cs$ addSaltern $tac$] \indexbold{*addSaltern}

changes the safe wrapper tactical to apply the given tactic when a safe step 

of the search would fail.

\item[$cs$ setSWrapper $tactical$] \indexbold{*setSWrapper}

specifies a new safe wrapper tactical.  

\item[$cs$ compSWrapper $tactical$] \indexbold{*compSWrapper}

composes the $tactical$ with the existing safe wrapper tactical, 

to combine their effects. 

\item[$cs$ addbefore $tac$] \indexbold{*addbefore}

changes the (unsafe) wrapper tactical to apply the given tactic, which should

be safe, {\em before} each step of the search.

\item[$cs$ addaltern $tac$] \indexbold{*addaltern}

changes the (unsafe) wrapper tactical to apply the given tactic 

{\em alternatively} after each step of the search.

\item[$cs$ setWrapper $tactical$] \indexbold{*setWrapper}

specifies a new (unsafe) wrapper tactical.  

\item[$cs$ compWrapper $tactical$] \indexbold{*compWrapper}

composes the $tactical$ with the existing (unsafe) wrapper tactical, 

to combine their effects. 

\end{ttdescription}

\section{The classical tactics}

\index{classical reasoner!tactics}

If installed, the classical module provides several tactics (and other

operations) for simulating the classical sequent calculus.

\subsection{The automatic tableau prover}

The tactic {\tt blast_tac} finds a proof rapidly using a separate tableau

prover and then reconstructs the proof using Isabelle tactics.  It is much

faster and more powerful than the other classical reasoning tactics, but has

major limitations too.  

\begin{itemize}

\item It does not use the wrapper tacticals described above, such as

  \ttindex{addss}.

\item It ignores types, which can cause problems in \HOL.  If it applies a rule

  whose types are inappropriate, then proof reconstruction will fail.

\item It does not perform higher-order unification, as needed by the rule {\tt

    rangeI} in {\HOL} and {\tt RepFunI} in {\ZF}.  There are often

    alternatives to such rules, for example {\tt

    range_eqI} and {\tt RepFun_eqI}.

\item The message {\small\tt Function Var's argument not a bound variable\ }

relates to the lack of higher-order unification.  Function variables

may only be applied to parameters of the subgoal.

\item Its proof strategy is more general than {\tt fast_tac}'s but can be

  slower.  If {\tt blast_tac} fails or seems to be running forever, try {\tt

  fast_tac} and the other tactics described below.

\end{itemize}

%

\begin{ttbox} 

blast_tac        : claset -> int -> tactic

Blast.depth_tac  : claset -> int -> int -> tactic

Blast.trace      : bool ref \hfill{\bf initially false}

\end{ttbox}

The two tactics differ on how they bound the number of unsafe steps used in a

proof.  While {\tt blast_tac} starts with a bound of zero and increases it

successively to~20, {\tt Blast.depth_tac} applies a user-supplied search bound.

\begin{ttdescription}

\item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove

  subgoal~$i$ using iterative deepening to increase the search bound.

\item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries

  to prove subgoal~$i$ using a search bound of $lim$.  Often a slow

  proof using {\tt blast_tac} can be made much faster by supplying the

  successful search bound to this tactic instead.

\item[\ttindexbold{Blast.trace} := true;] \index{tracing!of classical prover}

  causes the tableau prover to print a trace of its search.  At each step it

  displays the formula currently being examined and reports whether the branch

  has been closed, extended or split.

\end{ttdescription}

\subsection{The automatic tactics}

\begin{ttbox} 

fast_tac      : claset -> int -> tactic

best_tac      : claset -> int -> tactic

slow_tac      : claset -> int -> tactic

slow_best_tac : claset -> int -> tactic

\end{ttbox}

These tactics work by applying {\tt step_tac} or {\tt slow_step_tac}

repeatedly.  Their effect is restricted (by {\tt SELECT_GOAL}) to one subgoal;

they either prove this subgoal or fail.  The {\tt slow_} versions are more

powerful but can be much slower.  

The best-first tactics are guided by a heuristic function: typically, the

total size of the proof state.  This function is supplied in the functor call

that sets up the classical reasoner.

\begin{ttdescription}

\item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using

depth-first search, to prove subgoal~$i$.

\item[\ttindexbold{best_tac} $cs$ $i$] applies {\tt step_tac} using

best-first search, to prove subgoal~$i$.

\item[\ttindexbold{slow_tac} $cs$ $i$] applies {\tt slow_step_tac} using

depth-first search, to prove subgoal~$i$.

\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies {\tt slow_step_tac} using

best-first search, to prove subgoal~$i$.

\end{ttdescription}

\subsection{Depth-limited tactics}

\begin{ttbox} 

depth_tac  : claset -> int -> int -> tactic

deepen_tac : claset -> int -> int -> tactic

\end{ttbox}

These work by exhaustive search up to a specified depth.  Unsafe rules are

modified to preserve the formula they act on, so that it be used repeatedly.

They can prove more goals than {\tt fast_tac} can but are much

slower, for example if the assumptions have many universal quantifiers.

The depth limits the number of unsafe steps.  If you can estimate the minimum

number of unsafe steps needed, supply this value as~$m$ to save time.

\begin{ttdescription}

\item[\ttindexbold{depth_tac} $cs$ $m$ $i$] 

tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.

\item[\ttindexbold{deepen_tac} $cs$ $m$ $i$] 

tries to prove subgoal~$i$ by iterative deepening.  It calls {\tt depth_tac}

repeatedly with increasing depths, starting with~$m$.

\end{ttdescription}

\subsection{Single-step tactics}

\begin{ttbox} 

safe_step_tac : claset -> int -> tactic

safe_tac      : claset        -> tactic

inst_step_tac : claset -> int -> tactic

step_tac      : claset -> int -> tactic

slow_step_tac : claset -> int -> tactic

\end{ttbox}

The automatic proof procedures call these tactics.  By calling them

yourself, you can execute these procedures one step at a time.

\begin{ttdescription}

\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on

subgoal~$i$. The safe wrapper tactical is applied to a tactic that may include 

proof by assumption or Modus Ponens (taking care not to instantiate unknowns), 

or {\tt hyp_subst_tac}.

\item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all 

subgoals.  It is deterministic, with at most one outcome.  If the automatic

tactics fail, try using {\tt safe_tac} to open up your formula; then you

can replicate certain quantifiers explicitly by applying appropriate rules.

\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like {\tt safe_step_tac},

but allows unknowns to be instantiated.

\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof

  procedure.  The (unsafe) wrapper tactical is applied to a tactic that tries

 {\tt safe_tac}, {\tt inst_step_tac}, or applies an unsafe rule from~$cs$.

\item[\ttindexbold{slow_step_tac}] 

  resembles {\tt step_tac}, but allows backtracking between using safe

  rules with instantiation ({\tt inst_step_tac}) and using unsafe rules.

  The resulting search space is larger.

\end{ttdescription}

\subsection{The current claset}

Some logics (\FOL, {\HOL} and \ZF) support the concept of a current

claset\index{claset!current}.  This is a default set of classical rules.  The

underlying idea is quite similar to that of a current simpset described in

\S\ref{sec:simp-for-dummies}; please read that section, including its

warnings.  Just like simpsets, clasets can be associated with theories.  The

tactics

\begin{ttbox}

Blast_tac    : int -> tactic

Fast_tac     : int -> tactic

Best_tac     : int -> tactic

Deepen_tac   : int -> int -> tactic

Step_tac     : int -> tactic

\end{ttbox}

\indexbold{*Blast_tac}\indexbold{*Best_tac}\indexbold{*Fast_tac}%

\indexbold{*Deepen_tac}\indexbold{*Step_tac}

make use of the current claset. E.g. {\tt Blast_tac} is defined as follows:

\begin{ttbox}

fun Blast_tac i = fast_tac (!claset) i;

\end{ttbox}

where \ttindex{!claset} is the current claset.

The functions

\begin{ttbox}

AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit

\end{ttbox}

\indexbold{*AddSIs} \indexbold{*AddSEs} \indexbold{*AddSDs}

\indexbold{*AddIs} \indexbold{*AddEs} \indexbold{*AddDs}

are used to add rules to the current claset. They work exactly like their

lower case counterparts {\tt addSIs} etc.

\begin{ttbox}

Delrules : thm list -> unit

\end{ttbox}

deletes rules from the current claset. You do not need to worry via which of

the above {\tt Add} functions the rule was initially added.

\subsection{Other useful tactics}

\index{tactics!for contradiction}

\index{tactics!for Modus Ponens}

\begin{ttbox} 

contr_tac    :             int -> tactic

mp_tac       :             int -> tactic

eq_mp_tac    :             int -> tactic

swap_res_tac : thm list -> int -> tactic

\end{ttbox}

These can be used in the body of a specialized search.

\begin{ttdescription}

\item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}

  solves subgoal~$i$ by detecting a contradiction among two assumptions of

  the form $P$ and~$\neg P$, or fail.  It may instantiate unknowns.  The

  tactic can produce multiple outcomes, enumerating all possible

  contradictions.

\item[\ttindexbold{mp_tac} {\it i}] 

is like {\tt contr_tac}, but also attempts to perform Modus Ponens in

subgoal~$i$.  If there are assumptions $P\imp Q$ and~$P$, then it replaces

$P\imp Q$ by~$Q$.  It may instantiate unknowns.  It fails if it can do

nothing.

\item[\ttindexbold{eq_mp_tac} {\it i}] 

is like {\tt mp_tac} {\it i}, but may not instantiate unknowns --- thus, it

is safe.

\item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of

the proof state using {\it thms}, which should be a list of introduction

rules.  First, it attempts to prove the goal using {\tt assume_tac} or

{\tt contr_tac}.  It then attempts to apply each rule in turn, attempting

resolution and also elim-resolution with the swapped form.

\end{ttdescription}

\subsection{Creating swapped rules}

\begin{ttbox} 

swapify   : thm list -> thm list

joinrules : thm list * thm list -> (bool * thm) list

\end{ttbox}

\begin{ttdescription}

\item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the

swapped versions of~{\it thms}, regarded as introduction rules.

\item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]

joins introduction rules, their swapped versions, and elimination rules for

use with \ttindex{biresolve_tac}.  Each rule is paired with~{\tt false}

(indicating ordinary resolution) or~{\tt true} (indicating

elim-resolution).

\end{ttdescription}

\section{Setting up the classical reasoner}

\index{classical reasoner!setting up}

Isabelle's classical object-logics, including {\tt FOL} and {\tt HOL}, have

the classical reasoner already set up.  When defining a new classical logic,

you should set up the reasoner yourself.  It consists of the \ML{} functor

\ttindex{ClassicalFun}, which takes the argument

signature {\tt CLASSICAL_DATA}:

\begin{ttbox} 

signature CLASSICAL_DATA =

  sig

  val mp             : thm

  val not_elim       : thm

  val swap           : thm

  val sizef          : thm -> int

  val hyp_subst_tacs : (int -> tactic) list

  end;

\end{ttbox}

Thus, the functor requires the following items:

\begin{ttdescription}

\item[\tdxbold{mp}] should be the Modus Ponens rule

$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.

\item[\tdxbold{not_elim}] should be the contradiction rule

$\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.

\item[\tdxbold{swap}] should be the swap rule

$\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.

\item[\ttindexbold{sizef}] is the heuristic function used for best-first

search.  It should estimate the size of the remaining subgoals.  A good

heuristic function is \ttindex{size_of_thm}, which measures the size of the

proof state.  Another size function might ignore certain subgoals (say,

those concerned with type checking).  A heuristic function might simply

count the subgoals.

\item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in

the hypotheses, typically created by \ttindex{HypsubstFun} (see

Chapter~\ref{substitution}).  This list can, of course, be empty.  The

tactics are assumed to be safe!

\end{ttdescription}

The functor is not at all sensitive to the formalization of the

object-logic.  It does not even examine the rules, but merely applies

them according to its fixed strategy.  The functor resides in {\tt

  Provers/classical.ML} in the Isabelle sources.

\index{classical reasoner|)}