author lcp Mon, 04 Apr 1994 17:20:15 +0200 changeset 308 f4cecad9b6a0 parent 307 994dbab40849 child 309 3751567696bf
modifications towards final draft
 doc-src/Ref/classical.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/classical.tex	Mon Apr 04 17:09:45 1994 +0200
+++ b/doc-src/Ref/classical.tex	Mon Apr 04 17:20:15 1994 +0200
@@ -1,12 +1,13 @@
%% $Id$
\chapter{The Classical Reasoner}
\index{classical reasoner|(}
-\newcommand\ainfer{\begin{array}{r@{}l}#2\\ \hline#1\end{array}}
+\newcommand\ainfer{\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.
+of classical first-order logic.  Isabelle's set theory~{\tt ZF} is built
+upon theory~{\tt FOL}, while higher-order logic 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
@@ -20,15 +21,16 @@
$(\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 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 logics FOL, HOL and ZF have the classical reasoner already installed.  We
-shall first consider how to use it, then see how to instantiate it for new
-logics.
+The logics {\tt FOL}, {\tt HOL} and {\tt ZF} have the classical reasoner
+already installed.  We shall first consider how to use it, then see how to
+instantiate it for new logics.

\section{The sequent calculus}
@@ -40,8 +42,9 @@
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
+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,
@@ -52,8 +55,12 @@
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
+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$
@@ -82,7 +89,7 @@

\section{Simulating sequents by natural deduction}
-Isabelle can represent sequents directly, as in the object-logic~{\sc lk}.
+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
@@ -91,16 +98,17 @@
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},
+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.  But note that the rule $(\neg L)$ has no effect
-under our representation of sequents!
+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 formula are
+formula in the conclusion, namely~$Q@1$.  The other right-side formulae 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:
@@ -129,8 +137,8 @@
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:
+$\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 @@ -139,9 +147,9 @@$
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)$.
+$(\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
@@ -169,22 +177,21 @@

\section{Classical rule sets}
\index{classical sets|bold}
-Each automatic tactic takes a {\bf classical rule set} -- a collection of
+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.
+goal to an unprovable set of subgoals.

-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 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
@@ -211,29 +218,30 @@
\end{ttbox}
There are no operations for deletion from a classical set.  The add
operations do not check for repetitions.
-\begin{description}
+\begin{ttdescription}
\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[$cs$ addSIs $rules$] \indexbold{*addSIs}
+adds safe introduction~$rules$ to~$cs$.

-\item[\tt $cs$ addSEs $rules$] \indexbold{*addSEs}
-adds some safe elimination~$rules$ to the classical set~$cs$.
+\item[$cs$ addSEs $rules$] \indexbold{*addSEs}
+adds safe elimination~$rules$ to~$cs$.

-\item[\tt $cs$ addSDs $rules$] \indexbold{*addSDs}
-adds some safe destruction~$rules$ to the classical set~$cs$.
+\item[$cs$ addSDs $rules$] \indexbold{*addSDs}
+adds safe destruction~$rules$ to~$cs$.

-\item[\tt $cs$ addIs $rules$] \indexbold{*addIs}
-adds some unsafe introduction~$rules$ to the classical set~$cs$.
+\item[$cs$ addIs $rules$] \indexbold{*addIs}
+adds unsafe introduction~$rules$ to~$cs$.

-\item[\tt $cs$ addEs $rules$] \indexbold{*addEs}
-adds some unsafe elimination~$rules$ to the classical set~$cs$.
+\item[$cs$ addEs $rules$] \indexbold{*addEs}
+adds unsafe elimination~$rules$ to~$cs$.

-\item[\tt $cs$ addDs $rules$] \indexbold{*addDs}
-adds some unsafe destruction~$rules$ to the classical set~$cs$.
+\item[$cs$ addDs $rules$] \indexbold{*addDs}
+adds unsafe destruction~$rules$ to~$cs$.

-\item[\ttindexbold{print_cs} $cs$] prints the rules of the classical set~$cs$.
-\end{description}
+\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.
+\end{ttdescription}
+
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
@@ -265,7 +273,7 @@
\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}
+\begin{ttdescription}
\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}.
@@ -288,7 +296,7 @@
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}
+\end{ttdescription}

\subsection{The automatic tactics}
@@ -299,7 +307,7 @@
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}
+\begin{ttdescription}
\item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using
depth-first search, to solve subgoal~$i$.

@@ -307,7 +315,7 @@
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 reasoner is set up.
-\end{description}
+\end{ttdescription}

\subsection{Other useful tactics}
@@ -320,7 +328,7 @@
swap_res_tac : thm list -> int -> tactic
\end{ttbox}
These can be used in the body of a specialized search.
-\begin{description}
+\begin{ttdescription}
\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,
@@ -341,23 +349,23 @@
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}
+\end{ttdescription}

\subsection{Creating swapped rules}
\begin{ttbox}
swapify   : thm list -> thm list
joinrules : thm list * thm list -> (bool * thm) list
\end{ttbox}
-\begin{description}
+\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} \tt({\it intrs}, {\it elims})]
+\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{description}
+\end{ttdescription}

\section{Setting up the classical reasoner}
@@ -378,7 +386,7 @@
end;
\end{ttbox}
Thus, the functor requires the following items:
-\begin{description}
+\begin{ttdescription}
\item[\ttindexbold{mp}] should be the Modus Ponens rule
$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.

@@ -399,7 +407,7 @@
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}
+\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