--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Ref/classical.tex Wed Nov 10 05:00:57 1993 +0100
@@ -0,0 +1,408 @@
+%% $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|)}