%% $Id$
\chapter{The classical theorem prover}
\index{classical prover|(}
\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 (FOL). Isabelle's set theory is built upon
FOL, while higher-order logic contains FOL as a fragment. Theorem-proving
in FOL is of course undecidable, but many researchers have developed
strategies to assist in this task.
Isabelle's classical module 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~FOL, and have been
heavily used in the development of Isabelle's set theory. Few interactive
proof assistants provide this much automation. Isabelle does not record
proofs, but the tactics can be traced, and their components can be called
directly. In this manner, any proof can be viewed interactively.
The logics FOL, HOL and ZF have the classical prover already installed. We
shall first consider how to use it, then see how to instantiate it for new
logics.
\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 FOL, 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. 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~{\sc 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 the {\em Introduction to Isabelle},
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. 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 formula are
represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$. 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 $\forall x{.}P$, and 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(x))$, 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
\[ \Bigl(\neg(\exists x{.}P(x)) \Imp P(t)\Bigr) \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 package 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|bold}
Each automatic tactic takes a {\bf classical rule 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 obviously
unsafe, since it reduces $P\disj Q$ to~$P$; fortunately, we do not require
this rule.
In general, 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}.
Classical rule sets belong to the abstract type \ttindexbold{claset}, which
supports the following operations (provided the classical prover is
installed!):
\begin{ttbox}
empty_cs : claset
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}
print_cs : claset -> unit
\end{ttbox}
There are no operations for deletion from a classical set. The add
operations do not check for repetitions.
\begin{description}
\item[\ttindexbold{empty_cs}] is the empty classical set.
\item[\tt $cs$ addSIs $rules$] \indexbold{*addSIs}
adds some safe introduction~$rules$ to the classical set~$cs$.
\item[\tt $cs$ addSEs $rules$] \indexbold{*addSEs}
adds some safe elimination~$rules$ to the classical set~$cs$.
\item[\tt $cs$ addSDs $rules$] \indexbold{*addSDs}
adds some safe destruction~$rules$ to the classical set~$cs$.
\item[\tt $cs$ addIs $rules$] \indexbold{*addIs}
adds some unsafe introduction~$rules$ to the classical set~$cs$.
\item[\tt $cs$ addEs $rules$] \indexbold{*addEs}
adds some unsafe elimination~$rules$ to the classical set~$cs$.
\item[\tt $cs$ addDs $rules$] \indexbold{*addDs}
adds some unsafe destruction~$rules$ to the classical set~$cs$.
\item[\ttindexbold{print_cs} $cs$] prints the rules of the classical set~$cs$.
\end{description}
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 the number of new
subgoals they will yield, so that rules that generate the fewest subgoals
will be tried first (see \S\ref{biresolve_tac}).
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 \ttindex{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$.
\section{The classical tactics}
\index{classical prover!tactics|bold}
\index{tactics!for classical proof|bold}
If installed, the classical module provides several tactics (and other
operations) for simulating the classical sequent calculus.
\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{description}
\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
subgoal~$i$. This may include proof by assumption or Modus Ponens, taking
care not to instantiate unknowns, or \ttindex{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$] tries {\tt safe_tac}. IF this
fails, it tries {\tt inst_step_tac}, or applies an unsafe rule from~$cs$.
This is the basic step of the proof procedure.
\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 too large for use in the standard proof
procedures, but {\tt slow_step_tac} is worth considering in special
situations.
\end{description}
\subsection{The automatic tactics}
\begin{ttbox}
fast_tac : claset -> int -> tactic
best_tac : claset -> int -> tactic
\end{ttbox}
Both of these tactics work by applying {\tt step_tac} repeatedly. Their
effect is restricted (by {\tt SELECT_GOAL}) to one subgoal; they either
solve this subgoal or fail.
\begin{description}
\item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using
depth-first search, to solve subgoal~$i$.
\item[\ttindexbold{best_tac} $cs$ $i$] applies {\tt step_tac} using
best-first search, to solve subgoal~$i$. A heuristic function ---
typically, the total size of the proof state --- guides the search. This
function is supplied when the classical module is set up.
\end{description}
\subsection{Other useful tactics}
\index{tactics!for contradiction|bold}
\index{tactics!for Modus Ponens|bold}
\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{description}
\item[\ttindexbold{contr_tac} {\it i}] 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 solve the goal using \ttindex{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{description}
\subsection{Creating swapped rules}
\begin{ttbox}
swapify : thm list -> thm list
joinrules : thm list * thm list -> (bool * thm) list
\end{ttbox}
\begin{description}
\item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the
swapped versions of~{\it thms}, regarded as introduction rules.
\item[\ttindexbold{joinrules} \tt({\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{description}
\section{Setting up the classical prover}
\index{classical prover!setting up|bold}
Isabelle's classical object-logics, including {\tt FOL} and {\tt HOL}, have
the classical prover already set up. When defining a new classical logic,
you should set up the prover yourself. It consists of the \ML{} functor
\ttindex{ClassicalFun}, which takes the argument
signature\indexbold{*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{description}
\item[\ttindexbold{mp}] should be the Modus Ponens rule
$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
\item[\ttindexbold{not_elim}] should be the contradiction rule
$\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.
\item[\ttindexbold{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_tac}] 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{description}
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} on the Isabelle distribution directory.
\index{classical prover|)}