1.1 --- a/doc-src/Ref/classical.tex Mon May 05 21:18:01 1997 +0200
1.2 +++ b/doc-src/Ref/classical.tex Tue May 06 12:50:16 1997 +0200
1.3 @@ -3,10 +3,11 @@
1.4 \index{classical reasoner|(}
1.5 \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
1.6
1.7 -Although Isabelle is generic, many users will be working in some extension
1.8 -of classical first-order logic. Isabelle's set theory~{\tt ZF} is built
1.9 -upon theory~{\tt FOL}, while higher-order logic contains first-order logic
1.10 -as a fragment. Theorem-proving in predicate logic is undecidable, but many
1.11 +Although Isabelle is generic, many users will be working in some
1.12 +extension of classical first-order logic. Isabelle's set theory~{\tt
1.13 + ZF} is built upon theory~{\tt FOL}, while higher-order logic
1.14 +conceptually contains first-order logic as a fragment.
1.15 +Theorem-proving in predicate logic is undecidable, but many
1.16 researchers have developed strategies to assist in this task.
1.17
1.18 Isabelle's classical reasoner is an \ML{} functor that accepts certain
1.19 @@ -38,9 +39,10 @@
1.20 effectively, you need to know how it works and how to choose among the many
1.21 tactics available, including {\tt Fast_tac} and {\tt Best_tac}.
1.22
1.23 -We shall first discuss the underlying principles, then present the classical
1.24 -reasoner. Finally, we shall see how to instantiate it for new logics. The
1.25 -logics {\tt FOL}, {\tt HOL} and {\tt ZF} have it already installed.
1.26 +We shall first discuss the underlying principles, then present the
1.27 +classical reasoner. Finally, we shall see how to instantiate it for
1.28 +new logics. The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already
1.29 +installed.
1.30
1.31
1.32 \section{The sequent calculus}
1.33 @@ -71,14 +73,18 @@
1.34 \iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%
1.35 {Fig.\ts\ref{fol-fig}}.
1.36 The sequent calculus analogue of~$({\imp}I)$ is the rule
1.37 -$$ \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
1.38 - \eqno({\imp}R) $$
1.39 +$$
1.40 +\ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
1.41 +\eqno({\imp}R)
1.42 +$$
1.43 This breaks down some implication on the right side of a sequent; $\Gamma$
1.44 and $\Delta$ stand for the sets of formulae that are unaffected by the
1.45 inference. The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the
1.46 single rule
1.47 -$$ \ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}
1.48 - \eqno({\disj}R) $$
1.49 +$$
1.50 +\ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}
1.51 +\eqno({\disj}R)
1.52 +$$
1.53 This breaks down some disjunction on the right side, replacing it by both
1.54 disjuncts. Thus, the sequent calculus is a kind of multiple-conclusion logic.
1.55
1.56 @@ -115,15 +121,16 @@
1.57 other connectives, we use sequent-style elimination rules instead of
1.58 destruction rules such as $({\conj}E1,2)$ and $(\forall E)$. But note that
1.59 the rule $(\neg L)$ has no effect under our representation of sequents!
1.60 -$$ \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}
1.61 - \eqno({\neg}L) $$
1.62 +$$
1.63 +\ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}\eqno({\neg}L)
1.64 +$$
1.65 What about reasoning on the right? Introduction rules can only affect the
1.66 formula in the conclusion, namely~$Q@1$. The other right-side formulae are
1.67 represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.
1.68 \index{assumptions!negated}
1.69 In order to operate on one of these, it must first be exchanged with~$Q@1$.
1.70 Elim-resolution with the {\bf swap} rule has this effect:
1.71 -$$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap)$$
1.72 +$$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap) $$
1.73 To ensure that swaps occur only when necessary, each introduction rule is
1.74 converted into a swapped form: it is resolved with the second premise
1.75 of~$(swap)$. The swapped form of~$({\conj}I)$, which might be
1.76 @@ -172,8 +179,10 @@
1.77 $$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q \eqno(\forall E@2) $$
1.78 Elim-resolution with this rule will delete the universal formula after a
1.79 single use. To replicate universal quantifiers, replace the rule by
1.80 -$$ \List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.
1.81 - \eqno(\forall E@3) $$
1.82 +$$
1.83 +\List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.
1.84 +\eqno(\forall E@3)
1.85 +$$
1.86 To replicate existential quantifiers, replace $(\exists I)$ by
1.87 \[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \]
1.88 All introduction rules mentioned above are also useful in swapped form.
1.89 @@ -290,14 +299,15 @@
1.90 below). They may perform a form of Modus Ponens: if there are assumptions
1.91 $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$.
1.92
1.93 -The classical reasoning tactics---except {\tt blast_tac}!---allow you to
1.94 -modify this basic proof strategy by
1.95 -applying two arbitrary {\bf wrapper tacticals} to it. This affects each step of
1.96 -the search. Usually they are the identity tacticals, but they could apply
1.97 -another tactic before or after the step tactic. The first one, which is
1.98 -considered to be safe, affects \ttindex{safe_step_tac} and all the tactics that
1.99 -call it. The the second one, which may be unsafe, affects
1.100 -\ttindex{step_tac}, \ttindex{slow_step_tac} and the tactics that call them.
1.101 +The classical reasoning tactics --- except {\tt blast_tac}! --- allow
1.102 +you to modify this basic proof strategy by applying two arbitrary {\bf
1.103 + wrapper tacticals} to it. This affects each step of the search.
1.104 +Usually they are the identity tacticals, but they could apply another
1.105 +tactic before or after the step tactic. The first one, which is
1.106 +considered to be safe, affects \ttindex{safe_step_tac} and all the
1.107 +tactics that call it. The the second one, which may be unsafe, affects
1.108 +\ttindex{step_tac}, \ttindex{slow_step_tac} and the tactics that call
1.109 +them.
1.110
1.111 \begin{ttbox}
1.112 addss : claset * simpset -> claset \hfill{\bf infix 4}
1.113 @@ -315,10 +325,12 @@
1.114 (int -> tactic)) -> claset \hfill{\bf infix 4}
1.115 \end{ttbox}
1.116 %
1.117 -\index{simplification!from classical reasoner}
1.118 -The wrapper tacticals underly the operator \ttindex{addss}, which combines
1.119 -each search step by simplification. Strictly speaking, {\tt addss} is not
1.120 -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.
1.121 +\index{simplification!from classical reasoner} The wrapper tacticals
1.122 +underly the operator addss, which combines each search step by
1.123 +simplification. Strictly speaking, {\tt addss} is not part of the
1.124 +classical reasoner. It should be defined (using {\tt addSaltern
1.125 + (CHANGED o (safe_asm_more_full_simp_tac ss)}) when the simplifier is
1.126 +installed.
1.127
1.128 \begin{ttdescription}
1.129 \item[$cs$ addss $ss$] \indexbold{*addss}
1.130 @@ -501,7 +513,7 @@
1.131 warnings. Just like simpsets, clasets can be associated with theories. The
1.132 tactics
1.133 \begin{ttbox}
1.134 -Blast_tac : int -> tactic
1.135 +Blast_tac : int -> tactic
1.136 Fast_tac : int -> tactic
1.137 Best_tac : int -> tactic
1.138 Deepen_tac : int -> int -> tactic
1.139 @@ -620,8 +632,8 @@
1.140 tactics are assumed to be safe!
1.141 \end{ttdescription}
1.142 The functor is not at all sensitive to the formalization of the
1.143 -object-logic. It does not even examine the rules, but merely applies them
1.144 -according to its fixed strategy. The functor resides in {\tt
1.145 -Provers/classical.ML} in the Isabelle distribution directory.
1.146 +object-logic. It does not even examine the rules, but merely applies
1.147 +them according to its fixed strategy. The functor resides in {\tt
1.148 + Provers/classical.ML} in the Isabelle sources.
1.149
1.150 \index{classical reasoner|)}