1.1 --- a/doc-src/Ref/classical.tex Mon Apr 04 17:09:45 1994 +0200
1.2 +++ b/doc-src/Ref/classical.tex Mon Apr 04 17:20:15 1994 +0200
1.3 @@ -1,12 +1,13 @@
1.4 %% $Id$
1.5 \chapter{The Classical Reasoner}
1.6 \index{classical reasoner|(}
1.7 -\newcommand\ainfer[2]{\begin{array}{r@{}l}#2\\ \hline#1\end{array}}
1.8 +\newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
1.9 +
1.10 Although Isabelle is generic, many users will be working in some extension
1.11 -of classical first-order logic (FOL). Isabelle's set theory is built upon
1.12 -FOL, while higher-order logic contains FOL as a fragment. Theorem-proving
1.13 -in FOL is of course undecidable, but many researchers have developed
1.14 -strategies to assist in this task.
1.15 +of classical first-order logic. Isabelle's set theory~{\tt ZF} is built
1.16 +upon theory~{\tt FOL}, while higher-order logic contains first-order logic
1.17 +as a fragment. Theorem-proving in predicate logic is undecidable, but many
1.18 +researchers have developed strategies to assist in this task.
1.19
1.20 Isabelle's classical reasoner is an \ML{} functor that accepts certain
1.21 information about a logic and delivers a suite of automatic tactics. Each
1.22 @@ -20,15 +21,16 @@
1.23 \[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x))
1.24 \imp \neg (\exists z. \forall x. F(x,z))
1.25 \]
1.26 -The tactics are generic. They are not restricted to~FOL, and have been
1.27 -heavily used in the development of Isabelle's set theory. Few interactive
1.28 -proof assistants provide this much automation. Isabelle does not record
1.29 -proofs, but the tactics can be traced, and their components can be called
1.30 -directly. In this manner, any proof can be viewed interactively.
1.31 +%
1.32 +The tactics are generic. They are not restricted to first-order logic, and
1.33 +have been heavily used in the development of Isabelle's set theory. Few
1.34 +interactive proof assistants provide this much automation. The tactics can
1.35 +be traced, and their components can be called directly; in this manner,
1.36 +any proof can be viewed interactively.
1.37
1.38 -The logics FOL, HOL and ZF have the classical reasoner already installed. We
1.39 -shall first consider how to use it, then see how to instantiate it for new
1.40 -logics.
1.41 +The logics {\tt FOL}, {\tt HOL} and {\tt ZF} have the classical reasoner
1.42 +already installed. We shall first consider how to use it, then see how to
1.43 +instantiate it for new logics.
1.44
1.45
1.46 \section{The sequent calculus}
1.47 @@ -40,8 +42,9 @@
1.48 generalization of natural deduction, is easier to automate.
1.49
1.50 A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$
1.51 -and~$\Delta$ are sets of formulae.\footnote{For FOL, sequents can
1.52 -equivalently be made from lists or multisets of formulae.} The sequent
1.53 +and~$\Delta$ are sets of formulae.%
1.54 +\footnote{For first-order logic, sequents can equivalently be made from
1.55 + lists or multisets of formulae.} The sequent
1.56 \[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \]
1.57 is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj
1.58 Q@n$. Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true,
1.59 @@ -52,8 +55,12 @@
1.60 Sequent rules are classified as {\bf right} or {\bf left}, indicating which
1.61 side of the $\turn$~symbol they operate on. Rules that operate on the
1.62 right side are analogous to natural deduction's introduction rules, and
1.63 -left rules are analogous to elimination rules. The sequent calculus
1.64 -analogue of~$({\imp}I)$ is the rule
1.65 +left rules are analogous to elimination rules.
1.66 +Recall the natural deduction rules for
1.67 + first-order logic,
1.68 +\iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%
1.69 + {Fig.\ts\ref{fol-fig}}.
1.70 +The sequent calculus analogue of~$({\imp}I)$ is the rule
1.71 $$ \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
1.72 \eqno({\imp}R) $$
1.73 This breaks down some implication on the right side of a sequent; $\Gamma$
1.74 @@ -82,7 +89,7 @@
1.75
1.76
1.77 \section{Simulating sequents by natural deduction}
1.78 -Isabelle can represent sequents directly, as in the object-logic~{\sc lk}.
1.79 +Isabelle can represent sequents directly, as in the object-logic~{\tt LK}\@.
1.80 But natural deduction is easier to work with, and most object-logics employ
1.81 it. Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn
1.82 Q@1,\ldots,Q@n$ by the Isabelle formula
1.83 @@ -91,16 +98,17 @@
1.84 Elim-resolution plays a key role in simulating sequent proofs.
1.85
1.86 We can easily handle reasoning on the left.
1.87 -As discussed in the {\em Introduction to Isabelle},
1.88 +As discussed in
1.89 +\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}},
1.90 elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$
1.91 achieves a similar effect as the corresponding sequent rules. For the
1.92 other connectives, we use sequent-style elimination rules instead of
1.93 -destruction rules. But note that the rule $(\neg L)$ has no effect
1.94 -under our representation of sequents!
1.95 +destruction rules such as $({\conj}E1,2)$ and $(\forall E)$. But note that
1.96 +the rule $(\neg L)$ has no effect under our representation of sequents!
1.97 $$ \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}
1.98 \eqno({\neg}L) $$
1.99 What about reasoning on the right? Introduction rules can only affect the
1.100 -formula in the conclusion, namely~$Q@1$. The other right-side formula are
1.101 +formula in the conclusion, namely~$Q@1$. The other right-side formulae are
1.102 represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$. In
1.103 order to operate on one of these, it must first be exchanged with~$Q@1$.
1.104 Elim-resolution with the {\bf swap} rule has this effect:
1.105 @@ -129,8 +137,8 @@
1.106 The destruction rule $({\imp}E)$ is replaced by
1.107 \[ \List{P\imp Q;\; \neg P\imp R;\; Q\imp R} \Imp R. \]
1.108 Quantifier replication also requires special rules. In classical logic,
1.109 -$\exists x{.}P$ is equivalent to $\forall x{.}P$, and the rules $(\exists R)$
1.110 -and $(\forall L)$ are dual:
1.111 +$\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules
1.112 +$(\exists R)$ and $(\forall L)$ are dual:
1.113 \[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P}
1.114 {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R)
1.115 \qquad
1.116 @@ -139,9 +147,9 @@
1.117 \]
1.118 Thus both kinds of quantifier may be replicated. Theorems requiring
1.119 multiple uses of a universal formula are easy to invent; consider
1.120 -$(\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(x))$, for any~$n>1$.
1.121 -Natural examples of the multiple use of an existential formula are rare; a
1.122 -standard one is $\exists x.\forall y. P(x)\imp P(y)$.
1.123 +\[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \]
1.124 +for any~$n>1$. Natural examples of the multiple use of an existential
1.125 +formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$.
1.126
1.127 Forgoing quantifier replication loses completeness, but gains decidability,
1.128 since the search space becomes finite. Many useful theorems can be proved
1.129 @@ -169,22 +177,21 @@
1.130
1.131 \section{Classical rule sets}
1.132 \index{classical sets|bold}
1.133 -Each automatic tactic takes a {\bf classical rule set} -- a collection of
1.134 +Each automatic tactic takes a {\bf classical rule set} --- a collection of
1.135 rules, classified as introduction or elimination and as {\bf safe} or {\bf
1.136 unsafe}. In general, safe rules can be attempted blindly, while unsafe
1.137 rules must be used with care. A safe rule must never reduce a provable
1.138 -goal to an unprovable set of subgoals. The rule~$({\disj}I1)$ is obviously
1.139 -unsafe, since it reduces $P\disj Q$ to~$P$; fortunately, we do not require
1.140 -this rule.
1.141 +goal to an unprovable set of subgoals.
1.142
1.143 -In general, any rule is unsafe whose premises contain new unknowns. The
1.144 -elimination rule~$(\forall E@2)$ is unsafe, since it is applied via
1.145 -elim-resolution, which discards the assumption $\forall x{.}P(x)$ and
1.146 -replaces it by the weaker assumption~$P(\Var{t})$. The rule $({\exists}I)$
1.147 -is unsafe for similar reasons. The rule~$(\forall E@3)$ is unsafe in a
1.148 -different sense: since it keeps the assumption $\forall x{.}P(x)$, it is
1.149 -prone to looping. In classical first-order logic, all rules are safe
1.150 -except those mentioned above.
1.151 +The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$. Any
1.152 +rule is unsafe whose premises contain new unknowns. The elimination
1.153 +rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,
1.154 +which discards the assumption $\forall x{.}P(x)$ and replaces it by the
1.155 +weaker assumption~$P(\Var{t})$. The rule $({\exists}I)$ is unsafe for
1.156 +similar reasons. The rule~$(\forall E@3)$ is unsafe in a different sense:
1.157 +since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.
1.158 +In classical first-order logic, all rules are safe except those mentioned
1.159 +above.
1.160
1.161 The safe/unsafe distinction is vague, and may be regarded merely as a way
1.162 of giving some rules priority over others. One could argue that
1.163 @@ -211,29 +218,30 @@
1.164 \end{ttbox}
1.165 There are no operations for deletion from a classical set. The add
1.166 operations do not check for repetitions.
1.167 -\begin{description}
1.168 +\begin{ttdescription}
1.169 \item[\ttindexbold{empty_cs}] is the empty classical set.
1.170
1.171 -\item[\tt $cs$ addSIs $rules$] \indexbold{*addSIs}
1.172 -adds some safe introduction~$rules$ to the classical set~$cs$.
1.173 +\item[$cs$ addSIs $rules$] \indexbold{*addSIs}
1.174 +adds safe introduction~$rules$ to~$cs$.
1.175
1.176 -\item[\tt $cs$ addSEs $rules$] \indexbold{*addSEs}
1.177 -adds some safe elimination~$rules$ to the classical set~$cs$.
1.178 +\item[$cs$ addSEs $rules$] \indexbold{*addSEs}
1.179 +adds safe elimination~$rules$ to~$cs$.
1.180
1.181 -\item[\tt $cs$ addSDs $rules$] \indexbold{*addSDs}
1.182 -adds some safe destruction~$rules$ to the classical set~$cs$.
1.183 +\item[$cs$ addSDs $rules$] \indexbold{*addSDs}
1.184 +adds safe destruction~$rules$ to~$cs$.
1.185
1.186 -\item[\tt $cs$ addIs $rules$] \indexbold{*addIs}
1.187 -adds some unsafe introduction~$rules$ to the classical set~$cs$.
1.188 +\item[$cs$ addIs $rules$] \indexbold{*addIs}
1.189 +adds unsafe introduction~$rules$ to~$cs$.
1.190
1.191 -\item[\tt $cs$ addEs $rules$] \indexbold{*addEs}
1.192 -adds some unsafe elimination~$rules$ to the classical set~$cs$.
1.193 +\item[$cs$ addEs $rules$] \indexbold{*addEs}
1.194 +adds unsafe elimination~$rules$ to~$cs$.
1.195
1.196 -\item[\tt $cs$ addDs $rules$] \indexbold{*addDs}
1.197 -adds some unsafe destruction~$rules$ to the classical set~$cs$.
1.198 +\item[$cs$ addDs $rules$] \indexbold{*addDs}
1.199 +adds unsafe destruction~$rules$ to~$cs$.
1.200
1.201 -\item[\ttindexbold{print_cs} $cs$] prints the rules of the classical set~$cs$.
1.202 -\end{description}
1.203 +\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.
1.204 +\end{ttdescription}
1.205 +
1.206 Introduction rules are those that can be applied using ordinary resolution.
1.207 The classical set automatically generates their swapped forms, which will
1.208 be applied using elim-resolution. Elimination rules are applied using
1.209 @@ -265,7 +273,7 @@
1.210 \end{ttbox}
1.211 The automatic proof procedures call these tactics. By calling them
1.212 yourself, you can execute these procedures one step at a time.
1.213 -\begin{description}
1.214 +\begin{ttdescription}
1.215 \item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
1.216 subgoal~$i$. This may include proof by assumption or Modus Ponens, taking
1.217 care not to instantiate unknowns, or \ttindex{hyp_subst_tac}.
1.218 @@ -288,7 +296,7 @@
1.219 The resulting search space is too large for use in the standard proof
1.220 procedures, but {\tt slow_step_tac} is worth considering in special
1.221 situations.
1.222 -\end{description}
1.223 +\end{ttdescription}
1.224
1.225
1.226 \subsection{The automatic tactics}
1.227 @@ -299,7 +307,7 @@
1.228 Both of these tactics work by applying {\tt step_tac} repeatedly. Their
1.229 effect is restricted (by {\tt SELECT_GOAL}) to one subgoal; they either
1.230 solve this subgoal or fail.
1.231 -\begin{description}
1.232 +\begin{ttdescription}
1.233 \item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using
1.234 depth-first search, to solve subgoal~$i$.
1.235
1.236 @@ -307,7 +315,7 @@
1.237 best-first search, to solve subgoal~$i$. A heuristic function ---
1.238 typically, the total size of the proof state --- guides the search. This
1.239 function is supplied when the classical reasoner is set up.
1.240 -\end{description}
1.241 +\end{ttdescription}
1.242
1.243
1.244 \subsection{Other useful tactics}
1.245 @@ -320,7 +328,7 @@
1.246 swap_res_tac : thm list -> int -> tactic
1.247 \end{ttbox}
1.248 These can be used in the body of a specialized search.
1.249 -\begin{description}
1.250 +\begin{ttdescription}
1.251 \item[\ttindexbold{contr_tac} {\it i}] solves subgoal~$i$ by detecting a
1.252 contradiction among two assumptions of the form $P$ and~$\neg P$, or fail.
1.253 It may instantiate unknowns. The tactic can produce multiple outcomes,
1.254 @@ -341,23 +349,23 @@
1.255 rules. First, it attempts to solve the goal using \ttindex{assume_tac} or
1.256 {\tt contr_tac}. It then attempts to apply each rule in turn, attempting
1.257 resolution and also elim-resolution with the swapped form.
1.258 -\end{description}
1.259 +\end{ttdescription}
1.260
1.261 \subsection{Creating swapped rules}
1.262 \begin{ttbox}
1.263 swapify : thm list -> thm list
1.264 joinrules : thm list * thm list -> (bool * thm) list
1.265 \end{ttbox}
1.266 -\begin{description}
1.267 +\begin{ttdescription}
1.268 \item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the
1.269 swapped versions of~{\it thms}, regarded as introduction rules.
1.270
1.271 -\item[\ttindexbold{joinrules} \tt({\it intrs}, {\it elims})]
1.272 +\item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]
1.273 joins introduction rules, their swapped versions, and elimination rules for
1.274 use with \ttindex{biresolve_tac}. Each rule is paired with~{\tt false}
1.275 (indicating ordinary resolution) or~{\tt true} (indicating
1.276 elim-resolution).
1.277 -\end{description}
1.278 +\end{ttdescription}
1.279
1.280
1.281 \section{Setting up the classical reasoner}
1.282 @@ -378,7 +386,7 @@
1.283 end;
1.284 \end{ttbox}
1.285 Thus, the functor requires the following items:
1.286 -\begin{description}
1.287 +\begin{ttdescription}
1.288 \item[\ttindexbold{mp}] should be the Modus Ponens rule
1.289 $\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
1.290
1.291 @@ -399,7 +407,7 @@
1.292 the hypotheses, typically created by \ttindex{HypsubstFun} (see
1.293 Chapter~\ref{substitution}). This list can, of course, be empty. The
1.294 tactics are assumed to be safe!
1.295 -\end{description}
1.296 +\end{ttdescription}
1.297 The functor is not at all sensitive to the formalization of the
1.298 object-logic. It does not even examine the rules, but merely applies them
1.299 according to its fixed strategy. The functor resides in {\tt