doc-src/Ref/classical.tex
author oheimb
Sat, 15 Feb 1997 17:35:53 +0100
changeset 2632 1612b99395d4
parent 2631 5e5c78ba955e
child 3089 32dad29d4666
permissions -rw-r--r--
corrected minor mistakes
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
     2
\chapter{The Classical Reasoner}\label{chap:classical}
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
     3
\index{classical reasoner|(}
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
     4
\newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
     5
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
Although Isabelle is generic, many users will be working in some extension
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
     7
of classical first-order logic.  Isabelle's set theory~{\tt ZF} is built
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
     8
upon theory~{\tt FOL}, while higher-order logic contains first-order logic
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
     9
as a fragment.  Theorem-proving in predicate logic is undecidable, but many
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    10
researchers have developed strategies to assist in this task.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    12
Isabelle's classical reasoner is an \ML{} functor that accepts certain
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
information about a logic and delivers a suite of automatic tactics.  Each
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
tactic takes a collection of rules and executes a simple, non-clausal proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
procedure.  They are slow and simplistic compared with resolution theorem
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
provers, but they can save considerable time and effort.  They can prove
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
theorems such as Pelletier's~\cite{pelletier86} problems~40 and~41 in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
seconds:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
\[ (\exists y. \forall x. J(y,x) \bimp \neg J(x,x))  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
   \imp  \neg (\forall x. \exists y. \forall z. J(z,y) \bimp \neg J(z,x)) \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
\[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
   \imp \neg (\exists z. \forall x. F(x,z))  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
\]
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    24
%
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    25
The tactics are generic.  They are not restricted to first-order logic, and
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    26
have been heavily used in the development of Isabelle's set theory.  Few
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    27
interactive proof assistants provide this much automation.  The tactics can
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    28
be traced, and their components can be called directly; in this manner,
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    29
any proof can be viewed interactively.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
2479
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    31
The simplest way to apply the classical reasoner (to subgoal~$i$) is as
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    32
follows:
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    33
\begin{ttbox}
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    34
by (Fast_tac \(i\));
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    35
\end{ttbox}
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    36
If the subgoal is a simple formula of the predicate calculus or set theory,
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    37
then it should be proved quickly.  However, to use the classical reasoner
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    38
effectively, you need to know how it works.
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    39
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    40
We shall first discuss the underlying principles, then present the classical
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    41
reasoner.  Finally, we shall see how to instantiate it for new logics.  The
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    42
logics {\tt FOL}, {\tt HOL} and {\tt ZF} have it already installed.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
\section{The sequent calculus}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
\index{sequent calculus}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
Isabelle supports natural deduction, which is easy to use for interactive
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
proof.  But natural deduction does not easily lend itself to automation,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
and has a bias towards intuitionism.  For certain proofs in classical
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
logic, it can not be called natural.  The {\bf sequent calculus}, a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
generalization of natural deduction, is easier to automate.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    54
and~$\Delta$ are sets of formulae.%
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    55
\footnote{For first-order logic, sequents can equivalently be made from
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    56
  lists or multisets of formulae.} The sequent
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
\[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
Q@n$.  Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
while $Q@1,\ldots,Q@n$ represent alternative goals.  A sequent is {\bf
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
basic} if its left and right sides have a common formula, as in $P,Q\turn
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
Q,R$; basic sequents are trivially valid.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
Sequent rules are classified as {\bf right} or {\bf left}, indicating which
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
side of the $\turn$~symbol they operate on.  Rules that operate on the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
right side are analogous to natural deduction's introduction rules, and
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    67
left rules are analogous to elimination rules.  
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    68
Recall the natural deduction rules for
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    69
  first-order logic, 
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    70
\iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    71
                          {Fig.\ts\ref{fol-fig}}.
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    72
The sequent calculus analogue of~$({\imp}I)$ is the rule
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
$$ \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
   \eqno({\imp}R) $$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
This breaks down some implication on the right side of a sequent; $\Gamma$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
and $\Delta$ stand for the sets of formulae that are unaffected by the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
inference.  The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
single rule 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
$$ \ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
   \eqno({\disj}R) $$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
This breaks down some disjunction on the right side, replacing it by both
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
disjuncts.  Thus, the sequent calculus is a kind of multiple-conclusion logic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
To illustrate the use of multiple formulae on the right, let us prove
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
the classical theorem $(P\imp Q)\disj(Q\imp P)$.  Working backwards, we
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
reduce this formula to a basic sequent:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
\[ \infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
   {\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
    {\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
                    {P, Q \turn Q, P\qquad\qquad}}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
This example is typical of the sequent calculus: start with the desired
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
theorem and apply rules backwards in a fairly arbitrary manner.  This yields a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
surprisingly effective proof procedure.  Quantifiers add few complications,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
since Isabelle handles parameters and schematic variables.  See Chapter~10
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
of {\em ML for the Working Programmer}~\cite{paulson91} for further
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
discussion.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
\section{Simulating sequents by natural deduction}
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   101
Isabelle can represent sequents directly, as in the object-logic~{\tt LK}\@.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
But natural deduction is easier to work with, and most object-logics employ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
it.  Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
Q@1,\ldots,Q@n$ by the Isabelle formula
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
\[ \List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1, \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
where the order of the assumptions and the choice of~$Q@1$ are arbitrary.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
Elim-resolution plays a key role in simulating sequent proofs.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
We can easily handle reasoning on the left.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   110
As discussed in
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   111
\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}}, 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
achieves a similar effect as the corresponding sequent rules.  For the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
other connectives, we use sequent-style elimination rules instead of
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   115
destruction rules such as $({\conj}E1,2)$ and $(\forall E)$.  But note that
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   116
the rule $(\neg L)$ has no effect under our representation of sequents!
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
$$ \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
   \eqno({\neg}L) $$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
What about reasoning on the right?  Introduction rules can only affect the
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   120
formula in the conclusion, namely~$Q@1$.  The other right-side formulae are
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   121
represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.  
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   122
\index{assumptions!negated}
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   123
In order to operate on one of these, it must first be exchanged with~$Q@1$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
Elim-resolution with the {\bf swap} rule has this effect:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
$$ \List{\neg P; \; \neg R\Imp P} \Imp R   \eqno(swap)$$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
To ensure that swaps occur only when necessary, each introduction rule is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
converted into a swapped form: it is resolved with the second premise
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
of~$(swap)$.  The swapped form of~$({\conj}I)$, which might be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
called~$({\neg\conj}E)$, is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
\[ \List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R. \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
Similarly, the swapped form of~$({\imp}I)$ is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
\[ \List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R  \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
Swapped introduction rules are applied using elim-resolution, which deletes
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
the negated formula.  Our representation of sequents also requires the use
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
of ordinary introduction rules.  If we had no regard for readability, we
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
could treat the right side more uniformly by representing sequents as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
\[ \List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot. \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
\section{Extra rules for the sequent calculus}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
As mentioned, destruction rules such as $({\conj}E1,2)$ and $(\forall E)$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
must be replaced by sequent-style elimination rules.  In addition, we need
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
Q$.  The introduction rules~$({\disj}I1,2)$ are replaced by a rule that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
simulates $({\disj}R)$:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
\[ (\neg Q\Imp P) \Imp P\disj Q \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
The destruction rule $({\imp}E)$ is replaced by
332
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   148
\[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
Quantifier replication also requires special rules.  In classical logic,
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   150
$\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   151
$(\exists R)$ and $(\forall L)$ are dual:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
\[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
          {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
   \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
   \ainfer{\forall x{.}P, \Gamma &\turn \Delta}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
          {P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
Thus both kinds of quantifier may be replicated.  Theorems requiring
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
multiple uses of a universal formula are easy to invent; consider 
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   160
\[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \]
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   161
for any~$n>1$.  Natural examples of the multiple use of an existential
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   162
formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
Forgoing quantifier replication loses completeness, but gains decidability,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
since the search space becomes finite.  Many useful theorems can be proved
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
without replication, and the search generally delivers its verdict in a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
reasonable time.  To adopt this approach, represent the sequent rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
$(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
form:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
$$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q    \eqno(\forall E@2) $$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
Elim-resolution with this rule will delete the universal formula after a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
single use.  To replicate universal quantifiers, replace the rule by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
$$ \List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
   \eqno(\forall E@3) $$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
To replicate existential quantifiers, replace $(\exists I)$ by
332
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   177
\[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
All introduction rules mentioned above are also useful in swapped form.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
Replication makes the search space infinite; we must apply the rules with
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   181
care.  The classical reasoner distinguishes between safe and unsafe
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
rules, applying the latter only when there is no alternative.  Depth-first
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
search may well go down a blind alley; best-first search is better behaved
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
in an infinite search space.  However, quantifier replication is too
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
expensive to prove any but the simplest theorems.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
\section{Classical rule sets}
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   189
\index{classical sets}
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   190
Each automatic tactic takes a {\bf classical set} --- a collection of
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
rules, classified as introduction or elimination and as {\bf safe} or {\bf
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
unsafe}.  In general, safe rules can be attempted blindly, while unsafe
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
rules must be used with care.  A safe rule must never reduce a provable
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   194
goal to an unprovable set of subgoals.  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   196
The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$.  Any
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   197
rule is unsafe whose premises contain new unknowns.  The elimination
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   198
rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   199
which discards the assumption $\forall x{.}P(x)$ and replaces it by the
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   200
weaker assumption~$P(\Var{t})$.  The rule $({\exists}I)$ is unsafe for
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   201
similar reasons.  The rule~$(\forall E@3)$ is unsafe in a different sense:
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   202
since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   203
In classical first-order logic, all rules are safe except those mentioned
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   204
above.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
The safe/unsafe distinction is vague, and may be regarded merely as a way
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
of giving some rules priority over others.  One could argue that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
$({\disj}E)$ is unsafe, because repeated application of it could generate
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
exponentially many subgoals.  Induction rules are unsafe because inductive
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
proofs are difficult to set up automatically.  Any inference is unsafe that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
instantiates an unknown in the proof state --- thus \ttindex{match_tac}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
must be used, rather than \ttindex{resolve_tac}.  Even proof by assumption
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
is unsafe if it instantiates unknowns shared with other subgoals --- thus
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
\ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   216
\subsection{Adding rules to classical sets}
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   217
Classical rule sets belong to the abstract type \mltydx{claset}, which
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   218
supports the following operations (provided the classical reasoner is
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
installed!):
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
\begin{ttbox} 
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   221
empty_cs    : claset
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   222
print_cs    : claset -> unit
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   223
addSIs      : claset * thm list -> claset                 \hfill{\bf infix 4}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   224
addSEs      : claset * thm list -> claset                 \hfill{\bf infix 4}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   225
addSDs      : claset * thm list -> claset                 \hfill{\bf infix 4}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   226
addIs       : claset * thm list -> claset                 \hfill{\bf infix 4}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   227
addEs       : claset * thm list -> claset                 \hfill{\bf infix 4}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   228
addDs       : claset * thm list -> claset                 \hfill{\bf infix 4}
1869
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   229
delrules    : claset * thm list -> claset                 \hfill{\bf infix 4}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
\end{ttbox}
1869
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   231
The add operations do not check for repetitions.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   232
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
\item[\ttindexbold{empty_cs}] is the empty classical set.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   235
\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   236
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   237
\item[$cs$ addSIs $rules$] \indexbold{*addSIs}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   238
adds safe introduction~$rules$ to~$cs$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   240
\item[$cs$ addSEs $rules$] \indexbold{*addSEs}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   241
adds safe elimination~$rules$ to~$cs$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   243
\item[$cs$ addSDs $rules$] \indexbold{*addSDs}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   244
adds safe destruction~$rules$ to~$cs$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   246
\item[$cs$ addIs $rules$] \indexbold{*addIs}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   247
adds unsafe introduction~$rules$ to~$cs$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   249
\item[$cs$ addEs $rules$] \indexbold{*addEs}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   250
adds unsafe elimination~$rules$ to~$cs$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   252
\item[$cs$ addDs $rules$] \indexbold{*addDs}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   253
adds unsafe destruction~$rules$ to~$cs$.
1869
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   254
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   255
\item[$cs$ delrules $rules$] \indexbold{*delrules}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   256
deletes~$rules$ from~$cs$.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   257
\end{ttdescription}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   258
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
Introduction rules are those that can be applied using ordinary resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
The classical set automatically generates their swapped forms, which will
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
be applied using elim-resolution.  Elimination rules are applied using
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   262
elim-resolution.  In a classical set, rules are sorted by the number of new
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   263
subgoals they will yield; rules that generate the fewest subgoals will be
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   264
tried first (see \S\ref{biresolve_tac}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   266
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   267
\subsection{Modifying the search step}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
For a given classical set, the proof strategy is simple.  Perform as many
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
safe inferences as possible; or else, apply certain safe rules, allowing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
instantiation of unknowns; or else, apply an unsafe rule.  The tactics may
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   271
also apply {\tt hyp_subst_tac}, if they have been set up to do so (see
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
below).  They may perform a form of Modus Ponens: if there are assumptions
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
$P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   275
The classical reasoner allows you to modify this basic proof strategy by
2632
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   276
applying two arbitrary {\bf wrapper tacticals} to it. This affects each step of
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   277
the search.  Usually they are the identity tacticals, but they could apply 
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   278
another tactic before or after the step tactic. The first one, which is
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   279
considered to be safe, affects \ttindex{safe_step_tac} and all the tactics that
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   280
call it. The the second one, which may be unsafe, affects 
2632
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   281
\ttindex{step_tac}, \ttindex{slow_step_tac} and the tactics that call them.
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   282
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   283
\begin{ttbox} 
2632
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   284
addss        : claset * simpset -> claset                 \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   285
addSbefore   : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   286
addSaltern   : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   287
setSWrapper  : claset * ((int -> tactic) -> 
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   288
                         (int -> tactic)) -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   289
compSWrapper : claset * ((int -> tactic) -> 
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   290
                         (int -> tactic)) -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   291
addbefore    : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   292
addaltern    : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   293
setWrapper   : claset * ((int -> tactic) -> 
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   294
                         (int -> tactic)) -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   295
compWrapper  : claset * ((int -> tactic) -> 
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   296
                         (int -> tactic)) -> claset       \hfill{\bf infix 4}
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   297
\end{ttbox}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   298
%
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   299
\index{simplification!from classical reasoner} 
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   300
The wrapper tacticals underly the operator \ttindex{addss}, which combines
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   301
each search step by simplification.  Strictly speaking, {\tt addss} is not
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   302
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.
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   303
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   304
\begin{ttdescription}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   305
\item[$cs$ addss $ss$] \indexbold{*addss}
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   306
adds the simpset~$ss$ to the classical set. The assumptions and goal will be
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   307
simplified, in a safe way, after the safe steps of the search.
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   308
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   309
\item[$cs$ addSbefore $tac$] \indexbold{*addSbefore}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   310
changes the safe wrapper tactical to apply the given tactic {\em before}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   311
each safe step of the search.
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   312
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   313
\item[$cs$ addSaltern $tac$] \indexbold{*addSaltern}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   314
changes the safe wrapper tactical to apply the given tactic when a safe step 
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   315
of the search would fail.
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   316
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   317
\item[$cs$ setSWrapper $tactical$] \indexbold{*setSWrapper}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   318
specifies a new safe wrapper tactical.  
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   319
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   320
\item[$cs$ compSWrapper $tactical$] \indexbold{*compSWrapper}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   321
composes the $tactical$ with the existing safe wrapper tactical, 
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   322
to combine their effects. 
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   323
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   324
\item[$cs$ addbefore $tac$] \indexbold{*addbefore}
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   325
changes the (unsafe) wrapper tactical to apply the given tactic, which should
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   326
be safe, {\em before} each step of the search.
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   327
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   328
\item[$cs$ addaltern $tac$] \indexbold{*addaltern}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   329
changes the (unsafe) wrapper tactical to apply the given tactic 
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   330
{\em alternatively} after each step of the search.
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   331
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   332
\item[$cs$ setWrapper $tactical$] \indexbold{*setWrapper}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   333
specifies a new (unsafe) wrapper tactical.  
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   334
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   335
\item[$cs$ compWrapper $tactical$] \indexbold{*compWrapper}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   336
composes the $tactical$ with the existing (unsafe) wrapper tactical, 
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   337
to combine their effects. 
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   338
\end{ttdescription}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   339
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
\section{The classical tactics}
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   342
\index{classical reasoner!tactics}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
If installed, the classical module provides several tactics (and other
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
operations) for simulating the classical sequent calculus.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
332
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   346
\subsection{The automatic tactics}
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   347
\begin{ttbox} 
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   348
fast_tac      : claset -> int -> tactic
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   349
best_tac      : claset -> int -> tactic
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   350
slow_tac      : claset -> int -> tactic
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   351
slow_best_tac : claset -> int -> tactic
332
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   352
\end{ttbox}
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   353
These tactics work by applying {\tt step_tac} or {\tt slow_step_tac}
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   354
repeatedly.  Their effect is restricted (by {\tt SELECT_GOAL}) to one subgoal;
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   355
they either solve this subgoal or fail.  The {\tt slow_} versions are more
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   356
powerful but can be much slower.  
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   357
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   358
The best-first tactics are guided by a heuristic function: typically, the
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   359
total size of the proof state.  This function is supplied in the functor call
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   360
that sets up the classical reasoner.
332
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   361
\begin{ttdescription}
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   362
\item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   363
depth-first search, to solve subgoal~$i$.
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   364
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   365
\item[\ttindexbold{best_tac} $cs$ $i$] applies {\tt step_tac} using
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   366
best-first search, to solve subgoal~$i$.
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   367
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   368
\item[\ttindexbold{slow_tac} $cs$ $i$] applies {\tt slow_step_tac} using
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   369
depth-first search, to solve subgoal~$i$.
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   370
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   371
\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies {\tt slow_step_tac} using
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   372
best-first search, to solve subgoal~$i$.
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   373
\end{ttdescription}
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   374
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   375
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   376
\subsection{Depth-limited tactics}
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   377
\begin{ttbox} 
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   378
depth_tac  : claset -> int -> int -> tactic
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   379
deepen_tac : claset -> int -> int -> tactic
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   380
\end{ttbox}
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   381
These work by exhaustive search up to a specified depth.  Unsafe rules are
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   382
modified to preserve the formula they act on, so that it be used repeatedly.
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   383
They can prove more goals than {\tt fast_tac} can but are much
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   384
slower, for example if the assumptions have many universal quantifiers.
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   385
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   386
The depth limits the number of unsafe steps.  If you can estimate the minimum
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   387
number of unsafe steps needed, supply this value as~$m$ to save time.
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   388
\begin{ttdescription}
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   389
\item[\ttindexbold{depth_tac} $cs$ $m$ $i$] 
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   390
tries to solve subgoal~$i$ by exhaustive search up to depth~$m$.
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   391
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   392
\item[\ttindexbold{deepen_tac} $cs$ $m$ $i$] 
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   393
tries to solve subgoal~$i$ by iterative deepening.  It calls {\tt depth_tac}
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   394
repeatedly with increasing depths, starting with~$m$.
332
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   395
\end{ttdescription}
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   396
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   397
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
\subsection{Single-step tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
safe_step_tac : claset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
safe_tac      : claset        -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
inst_step_tac : claset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
step_tac      : claset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
slow_step_tac : claset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   406
The automatic proof procedures call these tactics.  By calling them
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
yourself, you can execute these procedures one step at a time.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   408
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   410
subgoal~$i$. The safe wrapper tactical is applied to a tactic that may include 
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   411
proof by assumption or Modus Ponens (taking care not to instantiate unknowns), 
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   412
or {\tt hyp_subst_tac}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
\item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   415
subgoals.  It is deterministic, with at most one outcome.  If the automatic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
tactics fail, try using {\tt safe_tac} to open up your formula; then you
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
can replicate certain quantifiers explicitly by applying appropriate rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like {\tt safe_step_tac},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
but allows unknowns to be instantiated.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   422
\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   423
  procedure.  The (unsafe) wrapper tactical is applied to a tactic that tries
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   424
 {\tt safe_tac}, {\tt inst_step_tac}, or applies an unsafe rule from~$cs$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
\item[\ttindexbold{slow_step_tac}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
  resembles {\tt step_tac}, but allows backtracking between using safe
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
  rules with instantiation ({\tt inst_step_tac}) and using unsafe rules.
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   429
  The resulting search space is larger.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   430
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
1869
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   432
\subsection{The current claset}
2479
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
   433
Some logics (\FOL, {\HOL} and \ZF) support the concept of a current
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
   434
claset\index{claset!current}.  This is a default set of classical rules.  The
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
   435
underlying idea is quite similar to that of a current simpset described in
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
   436
\S\ref{sec:simp-for-dummies}; please read that section, including its
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
   437
warnings.  Just like simpsets, clasets can be associated with theories.  The
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
   438
tactics
1869
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   439
\begin{ttbox}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   440
Step_tac     : int -> tactic
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   441
Fast_tac     : int -> tactic
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   442
Best_tac     : int -> tactic
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   443
Deepen_tac   : int -> int -> tactic
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   444
\end{ttbox}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   445
\indexbold{*Step_tac} \indexbold{*Best_tac} \indexbold{*Fast_tac}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   446
\indexbold{*Deepen_tac} 
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   447
make use of the current claset. E.g.~{\tt Fast_tac} is defined as follows:
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   448
\begin{ttbox}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   449
fun Fast_tac i = fast_tac (!claset) i;
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   450
\end{ttbox}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   451
where \ttindex{!claset} is the current claset.
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   452
The functions
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   453
\begin{ttbox}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   454
AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   455
\end{ttbox}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   456
\indexbold{*AddSIs} \indexbold{*AddSEs} \indexbold{*AddSDs}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   457
\indexbold{*AddIs} \indexbold{*AddEs} \indexbold{*AddDs}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   458
are used to add rules to the current claset. They work exactly like their
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   459
lower case counterparts {\tt addSIs} etc.
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   460
\begin{ttbox}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   461
Delrules : thm list -> unit
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   462
\end{ttbox}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   463
deletes rules from the current claset. You do not need to worry via which of
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   464
the above {\tt Add} functions the rule was initially added.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   466
\subsection{Other useful tactics}
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   467
\index{tactics!for contradiction}
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   468
\index{tactics!for Modus Ponens}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   469
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
contr_tac    :             int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
mp_tac       :             int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
eq_mp_tac    :             int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
swap_res_tac : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   474
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   475
These can be used in the body of a specialized search.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   476
\begin{ttdescription}
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   477
\item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   478
  solves subgoal~$i$ by detecting a contradiction among two assumptions of
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   479
  the form $P$ and~$\neg P$, or fail.  It may instantiate unknowns.  The
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   480
  tactic can produce multiple outcomes, enumerating all possible
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   481
  contradictions.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   482
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   483
\item[\ttindexbold{mp_tac} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
is like {\tt contr_tac}, but also attempts to perform Modus Ponens in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   485
subgoal~$i$.  If there are assumptions $P\imp Q$ and~$P$, then it replaces
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
$P\imp Q$ by~$Q$.  It may instantiate unknowns.  It fails if it can do
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
nothing.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
\item[\ttindexbold{eq_mp_tac} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
is like {\tt mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
is safe.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
\item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
the proof state using {\it thms}, which should be a list of introduction
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   495
rules.  First, it attempts to solve the goal using {\tt assume_tac} or
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
{\tt contr_tac}.  It then attempts to apply each rule in turn, attempting
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   497
resolution and also elim-resolution with the swapped form.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   498
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   500
\subsection{Creating swapped rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
swapify   : thm list -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   503
joinrules : thm list * thm list -> (bool * thm) list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
\end{ttbox}
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   505
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   506
\item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   507
swapped versions of~{\it thms}, regarded as introduction rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   509
\item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
joins introduction rules, their swapped versions, and elimination rules for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
use with \ttindex{biresolve_tac}.  Each rule is paired with~{\tt false}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
(indicating ordinary resolution) or~{\tt true} (indicating
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
elim-resolution).
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   514
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   517
\section{Setting up the classical reasoner}
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   518
\index{classical reasoner!setting up}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
Isabelle's classical object-logics, including {\tt FOL} and {\tt HOL}, have
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   520
the classical reasoner already set up.  When defining a new classical logic,
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   521
you should set up the reasoner yourself.  It consists of the \ML{} functor
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
\ttindex{ClassicalFun}, which takes the argument
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   523
signature {\tt CLASSICAL_DATA}:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   525
signature CLASSICAL_DATA =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
  sig
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   527
  val mp             : thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
  val not_elim       : thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
  val swap           : thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
  val sizef          : thm -> int
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
  val hyp_subst_tacs : (int -> tactic) list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
  end;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
Thus, the functor requires the following items:
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   535
\begin{ttdescription}
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   536
\item[\tdxbold{mp}] should be the Modus Ponens rule
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   538
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   539
\item[\tdxbold{not_elim}] should be the contradiction rule
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   540
$\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   541
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   542
\item[\tdxbold{swap}] should be the swap rule
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
$\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   544
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   545
\item[\ttindexbold{sizef}] is the heuristic function used for best-first
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   546
search.  It should estimate the size of the remaining subgoals.  A good
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   547
heuristic function is \ttindex{size_of_thm}, which measures the size of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   548
proof state.  Another size function might ignore certain subgoals (say,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   549
those concerned with type checking).  A heuristic function might simply
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
count the subgoals.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   551
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   552
\item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   553
the hypotheses, typically created by \ttindex{HypsubstFun} (see
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   554
Chapter~\ref{substitution}).  This list can, of course, be empty.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   555
tactics are assumed to be safe!
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   556
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   557
The functor is not at all sensitive to the formalization of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   558
object-logic.  It does not even examine the rules, but merely applies them
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   559
according to its fixed strategy.  The functor resides in {\tt
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   560
Provers/classical.ML} in the Isabelle distribution directory.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   561
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   562
\index{classical reasoner|)}