doc-src/Ref/classical.tex
author oheimb
Wed, 12 Nov 1997 18:58:50 +0100
changeset 4223 f60e3d2c81d3
parent 3720 a5b9e0ade194
child 4317 7264fa2ff2ec
permissions -rw-r--r--
added thin_refl to hyp_subst_tac
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
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
     6
Although Isabelle is generic, many users will be working in some
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
     7
extension of classical first-order logic.  Isabelle's set theory~{\tt
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
     8
  ZF} is built upon theory~\texttt{FOL}, while higher-order logic
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
     9
conceptually contains first-order logic as a fragment.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
    10
Theorem-proving in predicate logic is undecidable, but many
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    11
researchers have developed strategies to assist in this task.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    13
Isabelle's classical reasoner is an \ML{} functor that accepts certain
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
information about a logic and delivers a suite of automatic tactics.  Each
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
tactic takes a collection of rules and executes a simple, non-clausal proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
procedure.  They are slow and simplistic compared with resolution theorem
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
provers, but they can save considerable time and effort.  They can prove
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
theorems such as Pelletier's~\cite{pelletier86} problems~40 and~41 in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
seconds:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
\[ (\exists y. \forall x. J(y,x) \bimp \neg J(x,x))  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
   \imp  \neg (\forall x. \exists y. \forall z. J(z,y) \bimp \neg J(z,x)) \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
\[ (\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
    23
   \imp \neg (\exists z. \forall x. F(x,z))  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
\]
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    25
%
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    26
The tactics are generic.  They are not restricted to first-order logic, and
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    27
have been heavily used in the development of Isabelle's set theory.  Few
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    28
interactive proof assistants provide this much automation.  The tactics can
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    29
be traced, and their components can be called directly; in this manner,
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    30
any proof can be viewed interactively.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
    32
The simplest way to apply the classical reasoner (to subgoal~$i$) is to type
2479
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    33
\begin{ttbox}
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
    34
by (Blast_tac \(i\));
2479
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    35
\end{ttbox}
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
    36
This command quickly proves most simple formulas of the predicate calculus or
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
    37
set theory.  To attempt to prove \emph{all} subgoals using a combination of
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
    38
rewriting and classical reasoning, try
3224
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
    39
\begin{ttbox}
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
    40
by (Auto_tac());
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
    41
\end{ttbox}
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
    42
To do all obvious logical steps, even if they do not prove the
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
    43
subgoal, type one of the following:
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
    44
\begin{ttbox}
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
    45
by (Clarify_tac \(i\));        \emph{\textrm{applies to one subgoal}}
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
    46
by Safe_tac;               \emph{\textrm{applies to all subgoals}}
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
    47
\end{ttbox}
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
    48
You need to know how the classical reasoner works in order to use it
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
    49
effectively.  There are many tactics to choose from, including {\tt
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
    50
  Fast_tac} and \texttt{Best_tac}.
2479
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
    51
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
    52
We shall first discuss the underlying principles, then present the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
    53
classical reasoner.  Finally, we shall see how to instantiate it for
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
    54
new logics.  The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
    55
installed.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
\section{The sequent calculus}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
\index{sequent calculus}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
Isabelle supports natural deduction, which is easy to use for interactive
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
proof.  But natural deduction does not easily lend itself to automation,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
and has a bias towards intuitionism.  For certain proofs in classical
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
logic, it can not be called natural.  The {\bf sequent calculus}, a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
generalization of natural deduction, is easier to automate.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    67
and~$\Delta$ are sets of formulae.%
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    68
\footnote{For first-order logic, sequents can equivalently be made from
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    69
  lists or multisets of formulae.} The sequent
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
\[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
Q@n$.  Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
while $Q@1,\ldots,Q@n$ represent alternative goals.  A sequent is {\bf
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
basic} if its left and right sides have a common formula, as in $P,Q\turn
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
Q,R$; basic sequents are trivially valid.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
Sequent rules are classified as {\bf right} or {\bf left}, indicating which
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
side of the $\turn$~symbol they operate on.  Rules that operate on the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
right side are analogous to natural deduction's introduction rules, and
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    80
left rules are analogous to elimination rules.  
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    81
Recall the natural deduction rules for
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    82
  first-order logic, 
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    83
\iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    84
                          {Fig.\ts\ref{fol-fig}}.
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
    85
The sequent calculus analogue of~$({\imp}I)$ is the rule
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
    86
$$
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
    87
\ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
    88
\eqno({\imp}R)
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
    89
$$
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
This breaks down some implication on the right side of a sequent; $\Gamma$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
and $\Delta$ stand for the sets of formulae that are unaffected by the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
inference.  The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
single rule 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
    94
$$
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
    95
\ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
    96
\eqno({\disj}R)
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
    97
$$
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
This breaks down some disjunction on the right side, replacing it by both
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
disjuncts.  Thus, the sequent calculus is a kind of multiple-conclusion logic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
To illustrate the use of multiple formulae on the right, let us prove
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
the classical theorem $(P\imp Q)\disj(Q\imp P)$.  Working backwards, we
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
reduce this formula to a basic sequent:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
\[ \infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
   {\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
    {\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
                    {P, Q \turn Q, P\qquad\qquad}}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
This example is typical of the sequent calculus: start with the desired
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
theorem and apply rules backwards in a fairly arbitrary manner.  This yields a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
surprisingly effective proof procedure.  Quantifiers add few complications,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
since Isabelle handles parameters and schematic variables.  See Chapter~10
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
of {\em ML for the Working Programmer}~\cite{paulson91} for further
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
discussion.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
\section{Simulating sequents by natural deduction}
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   118
Isabelle can represent sequents directly, as in the object-logic~\texttt{LK}\@.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
But natural deduction is easier to work with, and most object-logics employ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
it.  Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
Q@1,\ldots,Q@n$ by the Isabelle formula
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
\[ \List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1, \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
where the order of the assumptions and the choice of~$Q@1$ are arbitrary.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
Elim-resolution plays a key role in simulating sequent proofs.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
We can easily handle reasoning on the left.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   127
As discussed in
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   128
\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}}, 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
achieves a similar effect as the corresponding sequent rules.  For the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
other connectives, we use sequent-style elimination rules instead of
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   132
destruction rules such as $({\conj}E1,2)$ and $(\forall E)$.  But note that
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   133
the rule $(\neg L)$ has no effect under our representation of sequents!
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   134
$$
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   135
\ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}\eqno({\neg}L)
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   136
$$
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
What about reasoning on the right?  Introduction rules can only affect the
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   138
formula in the conclusion, namely~$Q@1$.  The other right-side formulae are
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   139
represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.  
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   140
\index{assumptions!negated}
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   141
In order to operate on one of these, it must first be exchanged with~$Q@1$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
Elim-resolution with the {\bf swap} rule has this effect:
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   143
$$ \List{\neg P; \; \neg R\Imp P} \Imp R   \eqno(swap)  $$
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
To ensure that swaps occur only when necessary, each introduction rule is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
converted into a swapped form: it is resolved with the second premise
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
of~$(swap)$.  The swapped form of~$({\conj}I)$, which might be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
called~$({\neg\conj}E)$, is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
\[ \List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R. \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
Similarly, the swapped form of~$({\imp}I)$ is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
\[ \List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R  \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
Swapped introduction rules are applied using elim-resolution, which deletes
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
the negated formula.  Our representation of sequents also requires the use
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
of ordinary introduction rules.  If we had no regard for readability, we
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
could treat the right side more uniformly by representing sequents as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
\[ \List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot. \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
\section{Extra rules for the sequent calculus}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
As mentioned, destruction rules such as $({\conj}E1,2)$ and $(\forall E)$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
must be replaced by sequent-style elimination rules.  In addition, we need
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
Q$.  The introduction rules~$({\disj}I1,2)$ are replaced by a rule that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
simulates $({\disj}R)$:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
\[ (\neg Q\Imp P) \Imp P\disj Q \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
The destruction rule $({\imp}E)$ is replaced by
332
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   166
\[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
Quantifier replication also requires special rules.  In classical logic,
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   168
$\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   169
$(\exists R)$ and $(\forall L)$ are dual:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
\[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
          {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
   \qquad
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
   \ainfer{\forall x{.}P, \Gamma &\turn \Delta}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
          {P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
Thus both kinds of quantifier may be replicated.  Theorems requiring
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
multiple uses of a universal formula are easy to invent; consider 
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   178
\[ (\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
   179
for any~$n>1$.  Natural examples of the multiple use of an existential
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   180
formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
Forgoing quantifier replication loses completeness, but gains decidability,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
since the search space becomes finite.  Many useful theorems can be proved
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
without replication, and the search generally delivers its verdict in a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
reasonable time.  To adopt this approach, represent the sequent rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
$(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
form:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
$$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q    \eqno(\forall E@2) $$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
Elim-resolution with this rule will delete the universal formula after a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
single use.  To replicate universal quantifiers, replace the rule by
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   192
$$
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   193
\List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   194
\eqno(\forall E@3)
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   195
$$
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
To replicate existential quantifiers, replace $(\exists I)$ by
332
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   197
\[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
All introduction rules mentioned above are also useful in swapped form.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
Replication makes the search space infinite; we must apply the rules with
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   201
care.  The classical reasoner distinguishes between safe and unsafe
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
rules, applying the latter only when there is no alternative.  Depth-first
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
search may well go down a blind alley; best-first search is better behaved
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
in an infinite search space.  However, quantifier replication is too
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
expensive to prove any but the simplest theorems.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
\section{Classical rule sets}
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   209
\index{classical sets}
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   210
Each automatic tactic takes a {\bf classical set} --- a collection of
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
rules, classified as introduction or elimination and as {\bf safe} or {\bf
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
unsafe}.  In general, safe rules can be attempted blindly, while unsafe
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
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
   214
goal to an unprovable set of subgoals.  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   216
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
   217
rule is unsafe whose premises contain new unknowns.  The elimination
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   218
rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   219
which discards the assumption $\forall x{.}P(x)$ and replaces it by the
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   220
weaker assumption~$P(\Var{t})$.  The rule $({\exists}I)$ is unsafe for
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   221
similar reasons.  The rule~$(\forall E@3)$ is unsafe in a different sense:
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   222
since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   223
In classical first-order logic, all rules are safe except those mentioned
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   224
above.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
The safe/unsafe distinction is vague, and may be regarded merely as a way
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
of giving some rules priority over others.  One could argue that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
$({\disj}E)$ is unsafe, because repeated application of it could generate
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
exponentially many subgoals.  Induction rules are unsafe because inductive
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
proofs are difficult to set up automatically.  Any inference is unsafe that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
instantiates an unknown in the proof state --- thus \ttindex{match_tac}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
must be used, rather than \ttindex{resolve_tac}.  Even proof by assumption
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
is unsafe if it instantiates unknowns shared with other subgoals --- thus
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
\ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   236
\subsection{Adding rules to classical sets}
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   237
Classical rule sets belong to the abstract type \mltydx{claset}, which
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   238
supports the following operations (provided the classical reasoner is
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
installed!):
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
\begin{ttbox} 
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   241
empty_cs    : claset
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   242
print_cs    : claset -> unit
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   243
addSIs      : claset * thm list -> claset                 \hfill{\bf infix 4}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   244
addSEs      : claset * thm list -> claset                 \hfill{\bf infix 4}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   245
addSDs      : claset * thm list -> claset                 \hfill{\bf infix 4}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   246
addIs       : claset * thm list -> claset                 \hfill{\bf infix 4}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   247
addEs       : claset * thm list -> claset                 \hfill{\bf infix 4}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   248
addDs       : claset * thm list -> claset                 \hfill{\bf infix 4}
1869
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   249
delrules    : claset * thm list -> claset                 \hfill{\bf infix 4}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
\end{ttbox}
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   251
The add operations ignore any rule already present in the claset with the same
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   252
classification (such as Safe Introduction).  They print a warning if the rule
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   253
has already been added with some other classification, but add the rule
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   254
anyway.  Calling \texttt{delrules} deletes all occurrences of a rule from the
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   255
claset, but see the warning below concerning destruction rules.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   256
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
\item[\ttindexbold{empty_cs}] is the empty classical set.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   259
\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   260
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   261
\item[$cs$ addSIs $rules$] \indexbold{*addSIs}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   262
adds safe introduction~$rules$ to~$cs$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   264
\item[$cs$ addSEs $rules$] \indexbold{*addSEs}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   265
adds safe elimination~$rules$ to~$cs$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   267
\item[$cs$ addSDs $rules$] \indexbold{*addSDs}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   268
adds safe destruction~$rules$ to~$cs$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   270
\item[$cs$ addIs $rules$] \indexbold{*addIs}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   271
adds unsafe introduction~$rules$ to~$cs$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   273
\item[$cs$ addEs $rules$] \indexbold{*addEs}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   274
adds unsafe elimination~$rules$ to~$cs$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   276
\item[$cs$ addDs $rules$] \indexbold{*addDs}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   277
adds unsafe destruction~$rules$ to~$cs$.
1869
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   278
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   279
\item[$cs$ delrules $rules$] \indexbold{*delrules}
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   280
deletes~$rules$ from~$cs$.  It prints a warning for those rules that are not
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   281
in~$cs$.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   282
\end{ttdescription}
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   283
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   284
\begin{warn}
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   285
  If you added $rule$ using \texttt{addSDs} or \texttt{addDs}, then you must delete
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   286
  it as follows:
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   287
\begin{ttbox}
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   288
\(cs\) delrules [make_elim \(rule\)]
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   289
\end{ttbox}
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   290
\par\noindent
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   291
This is necessary because the operators \texttt{addSDs} and \texttt{addDs} convert
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   292
the destruction rules to elimination rules by applying \ttindex{make_elim},
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   293
and then insert them using \texttt{addSEs} and \texttt{addEs}, respectively.
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   294
\end{warn}
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   295
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
Introduction rules are those that can be applied using ordinary resolution.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
The classical set automatically generates their swapped forms, which will
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
be applied using elim-resolution.  Elimination rules are applied using
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   299
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
   300
subgoals they will yield; rules that generate the fewest subgoals will be
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   301
tried first (see \S\ref{biresolve_tac}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
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
\subsection{Modifying the search step}
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   305
For a given classical set, the proof strategy is simple.  Perform as many safe
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   306
inferences as possible; or else, apply certain safe rules, allowing
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   307
instantiation of unknowns; or else, apply an unsafe rule.  The tactics also
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   308
eliminate assumptions of the form $x=t$ by substitution if they have been set
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   309
up to do so (see \texttt{hyp_subst_tacs} in~\S\ref{sec:classical-setup} below).
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   310
They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   311
and~$P$, then replace $P\imp Q$ by~$Q$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   313
The classical reasoning tactics --- except \texttt{blast_tac}! --- allow
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   314
you to modify this basic proof strategy by applying two arbitrary {\bf
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3224
diff changeset
   315
  wrapper tacticals} to it.  This affects each step of the search.
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   316
Usually they are the identity tacticals, but they could apply another
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3224
diff changeset
   317
tactic before or after the step tactic.  The first one, which is
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   318
considered to be safe, affects \ttindex{safe_step_tac} and all the
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3224
diff changeset
   319
tactics that call it.  The the second one, which may be unsafe, affects
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   320
\ttindex{step_tac}, \ttindex{slow_step_tac} and the tactics that call
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   321
them.
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   322
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   323
\begin{ttbox} 
2632
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   324
addss        : claset * simpset -> claset                 \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   325
addSbefore   : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   326
addSaltern   : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   327
setSWrapper  : claset * ((int -> tactic) -> 
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   328
                         (int -> tactic)) -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   329
compSWrapper : claset * ((int -> tactic) -> 
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   330
                         (int -> tactic)) -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   331
addbefore    : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   332
addaltern    : claset *  (int -> tactic)  -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   333
setWrapper   : claset * ((int -> tactic) -> 
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   334
                         (int -> tactic)) -> claset       \hfill{\bf infix 4}
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   335
compWrapper  : claset * ((int -> tactic) -> 
1612b99395d4 corrected minor mistakes
oheimb
parents: 2631
diff changeset
   336
                         (int -> tactic)) -> claset       \hfill{\bf infix 4}
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   337
\end{ttbox}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   338
%
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   339
\index{simplification!from classical reasoner} The wrapper tacticals
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   340
underly the operator addss, which combines each search step by
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   341
simplification.  Strictly speaking, \texttt{addss} is not part of the
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   342
classical reasoner.  It should be defined (using \texttt{addSaltern
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   343
  (CHANGED o (safe_asm_more_full_simp_tac ss)}) when the simplifier is
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   344
installed.
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   345
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   346
\begin{ttdescription}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   347
\item[$cs$ addss $ss$] \indexbold{*addss}
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3224
diff changeset
   348
adds the simpset~$ss$ to the classical set.  The assumptions and goal will be
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   349
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
   350
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   351
\item[$cs$ addSbefore $tac$] \indexbold{*addSbefore}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   352
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
   353
each safe step of the search.
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   354
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   355
\item[$cs$ addSaltern $tac$] \indexbold{*addSaltern}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   356
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
   357
of the search would fail.
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   358
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   359
\item[$cs$ setSWrapper $tactical$] \indexbold{*setSWrapper}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   360
specifies a new safe wrapper tactical.  
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   361
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   362
\item[$cs$ compSWrapper $tactical$] \indexbold{*compSWrapper}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   363
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
   364
to combine their effects. 
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   365
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   366
\item[$cs$ addbefore $tac$] \indexbold{*addbefore}
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   367
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
   368
be safe, {\em before} each step of the search.
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   369
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   370
\item[$cs$ addaltern $tac$] \indexbold{*addaltern}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   371
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
   372
{\em alternatively} after each step of the search.
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   373
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   374
\item[$cs$ setWrapper $tactical$] \indexbold{*setWrapper}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   375
specifies a new (unsafe) wrapper tactical.  
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   376
2631
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   377
\item[$cs$ compWrapper $tactical$] \indexbold{*compWrapper}
5e5c78ba955e description of safe vs. unsafe wrapper and the functions involved
oheimb
parents: 2479
diff changeset
   378
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
   379
to combine their effects. 
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   380
\end{ttdescription}
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   381
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
\section{The classical tactics}
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   384
\index{classical reasoner!tactics} If installed, the classical module provides
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   385
powerful theorem-proving tactics.  Most of them have capitalized analogues
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   386
that use the default claset; see \S\ref{sec:current-claset}.
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   387
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   388
\subsection{Semi-automatic tactics}
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   389
\begin{ttbox} 
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   390
clarify_tac      : claset -> int -> tactic
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   391
clarify_step_tac : claset -> int -> tactic
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   392
\end{ttbox}
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   393
Use these when the automatic tactics fail.  They perform all the obvious
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   394
logical inferences that do not split the subgoal.  The result is a
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   395
simpler subgoal that can be tackled by other means, such as by
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   396
instantiating quantifiers yourself.
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   397
\begin{ttdescription}
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   398
\item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   399
subgoal~$i$, using \texttt{clarify_step_tac}.
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   400
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   401
\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   402
  subgoal~$i$.  No splitting step is applied; for example, the subgoal $A\conj
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   403
  B$ is left as a conjunction.  Proof by assumption, Modus Ponens, etc., may be
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   404
  performed provided they do not instantiate unknowns.  Assumptions of the
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   405
  form $x=t$ may be eliminated.  The user-supplied safe wrapper tactical is
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   406
  applied.
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   407
\end{ttdescription}
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   408
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
3224
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   410
\subsection{The tableau prover}
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   411
The tactic \texttt{blast_tac} searches for a proof using a fast tableau prover,
3224
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   412
coded directly in \ML.  It then reconstructs the proof using Isabelle
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   413
tactics.  It is faster and more powerful than the other classical
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   414
reasoning tactics, but has major limitations too.
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   415
\begin{itemize}
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   416
\item It does not use the wrapper tacticals described above, such as
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   417
  \ttindex{addss}.
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   418
\item It ignores types, which can cause problems in \HOL.  If it applies a rule
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   419
  whose types are inappropriate, then proof reconstruction will fail.
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   420
\item It does not perform higher-order unification, as needed by the rule {\tt
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   421
    rangeI} in {\HOL} and \texttt{RepFunI} in {\ZF}.  There are often
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   422
    alternatives to such rules, for example {\tt
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   423
    range_eqI} and \texttt{RepFun_eqI}.
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   424
\item The message {\small\tt Function Var's argument not a bound variable\ }
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   425
relates to the lack of higher-order unification.  Function variables
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   426
may only be applied to parameters of the subgoal.
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   427
\item Its proof strategy is more general than \texttt{fast_tac}'s but can be
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   428
  slower.  If \texttt{blast_tac} fails or seems to be running forever, try {\tt
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   429
  fast_tac} and the other tactics described below.
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   430
\end{itemize}
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   431
%
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   432
\begin{ttbox} 
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   433
blast_tac        : claset -> int -> tactic
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   434
Blast.depth_tac  : claset -> int -> int -> tactic
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   435
Blast.trace      : bool ref \hfill{\bf initially false}
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   436
\end{ttbox}
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   437
The two tactics differ on how they bound the number of unsafe steps used in a
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   438
proof.  While \texttt{blast_tac} starts with a bound of zero and increases it
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   439
successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound.
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   440
\begin{ttdescription}
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   441
\item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   442
  subgoal~$i$ using iterative deepening to increase the search bound.
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   443
  
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   444
\item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   445
  to prove subgoal~$i$ using a search bound of $lim$.  Often a slow
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   446
  proof using \texttt{blast_tac} can be made much faster by supplying the
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   447
  successful search bound to this tactic instead.
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   448
  
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   449
\item[\ttindexbold{Blast.trace} := true;] \index{tracing!of classical prover}
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   450
  causes the tableau prover to print a trace of its search.  At each step it
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   451
  displays the formula currently being examined and reports whether the branch
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   452
  has been closed, extended or split.
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   453
\end{ttdescription}
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   454
3224
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   455
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   456
\subsection{An automatic tactic}
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   457
\begin{ttbox} 
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   458
auto_tac      : claset * simpset -> tactic
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   459
auto          : unit -> unit
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   460
\end{ttbox}
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   461
The auto-tactic attempts to prove all subgoals using a combination of
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   462
simplification and classical reasoning.  It is intended for situations where
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   463
there are a lot of mostly trivial subgoals; it proves all the easy ones,
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   464
leaving the ones it cannot prove.  (Unfortunately, attempting to prove the
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   465
hard ones may take a long time.)  It must be supplied both a simpset and a
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   466
claset; therefore it is most easily called as \texttt{Auto_tac}, which uses
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   467
the default claset and simpset (see \S\ref{sec:current-claset} below).  For
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   468
interactive use, the shorthand \texttt{auto();} abbreviates 
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   469
\begin{ttbox}
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   470
by (Auto_tac());
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   471
\end{ttbox}
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   472
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   473
\subsection{Other classical tactics}
332
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   474
\begin{ttbox} 
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   475
fast_tac      : claset -> int -> tactic
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   476
best_tac      : claset -> int -> tactic
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   477
slow_tac      : claset -> int -> tactic
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   478
slow_best_tac : claset -> int -> tactic
332
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   479
\end{ttbox}
3224
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   480
These tactics attempt to prove a subgoal using sequent-style reasoning.
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   481
Unlike \texttt{blast_tac}, they construct proofs directly in Isabelle.  Their
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   482
effect is restricted (by \texttt{SELECT_GOAL}) to one subgoal; they either prove
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   483
this subgoal or fail.  The \texttt{slow_} versions conduct a broader
3224
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   484
search.%
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   485
\footnote{They may, when backtracking from a failed proof attempt, undo even
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   486
  the step of proving a subgoal by assumption.}
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   487
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   488
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
   489
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
   490
that sets up the classical reasoner.
332
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   491
\begin{ttdescription}
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   492
\item[\ttindexbold{fast_tac} $cs$ $i$] applies \texttt{step_tac} using
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   493
depth-first search, to prove subgoal~$i$.
332
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   494
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   495
\item[\ttindexbold{best_tac} $cs$ $i$] applies \texttt{step_tac} using
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   496
best-first search, to prove subgoal~$i$.
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   497
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   498
\item[\ttindexbold{slow_tac} $cs$ $i$] applies \texttt{slow_step_tac} using
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   499
depth-first search, to prove subgoal~$i$.
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   500
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   501
\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} using
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   502
best-first search, to prove subgoal~$i$.
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   503
\end{ttdescription}
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   504
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   505
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   506
\subsection{Depth-limited automatic tactics}
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   507
\begin{ttbox} 
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   508
depth_tac  : claset -> int -> int -> tactic
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   509
deepen_tac : claset -> int -> int -> tactic
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   510
\end{ttbox}
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   511
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
   512
modified to preserve the formula they act on, so that it be used repeatedly.
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   513
They can prove more goals than \texttt{fast_tac} can but are much
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   514
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
   515
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   516
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
   517
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
   518
\begin{ttdescription}
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   519
\item[\ttindexbold{depth_tac} $cs$ $m$ $i$] 
3089
32dad29d4666 Documented blast_tac
paulson
parents: 2632
diff changeset
   520
tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   521
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   522
\item[\ttindexbold{deepen_tac} $cs$ $m$ $i$] 
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   523
tries to prove subgoal~$i$ by iterative deepening.  It calls \texttt{depth_tac}
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   524
repeatedly with increasing depths, starting with~$m$.
332
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   525
\end{ttdescription}
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   526
01b87a921967 final Springer copy
lcp
parents: 319
diff changeset
   527
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
\subsection{Single-step tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
safe_step_tac : claset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
safe_tac      : claset        -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
inst_step_tac : claset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
step_tac      : claset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
slow_step_tac : claset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   535
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   536
The automatic proof procedures call these tactics.  By calling them
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
yourself, you can execute these procedures one step at a time.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   538
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   539
\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   540
  subgoal~$i$.  The safe wrapper tactical is applied to a tactic that may
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   541
  include proof by assumption or Modus Ponens (taking care not to instantiate
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   542
  unknowns), or substitution.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   544
\item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all 
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   545
subgoals.  It is deterministic, with at most one outcome.  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   546
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   547
\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   548
but allows unknowns to be instantiated.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   549
1099
f4335b56f772 Covers wrapper tacticals: setwrapper, ..., addss
lcp
parents: 875
diff changeset
   550
\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
   551
  procedure.  The (unsafe) wrapper tactical is applied to a tactic that tries
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   552
 \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule from~$cs$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   553
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   554
\item[\ttindexbold{slow_step_tac}] 
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   555
  resembles \texttt{step_tac}, but allows backtracking between using safe
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   556
  rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules.
875
a0b71a4bbe5e documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents: 332
diff changeset
   557
  The resulting search space is larger.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   558
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   559
3224
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   560
\subsection{The current claset}\label{sec:current-claset}
2479
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
   561
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
   562
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
   563
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
   564
\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
   565
warnings.  Just like simpsets, clasets can be associated with theories.  The
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 1869
diff changeset
   566
tactics
1869
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   567
\begin{ttbox}
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   568
Blast_tac        : int -> tactic
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   569
Auto_tac         : unit -> tactic
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   570
Fast_tac         : int -> tactic
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   571
Best_tac         : int -> tactic
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   572
Deepen_tac       : int -> int -> tactic
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   573
Clarify_tac      : int -> tactic
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   574
Clarify_step_tac : int -> tactic
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   575
Safe_tac         :        tactic
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   576
Safe_step_tac    : int -> tactic
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   577
Step_tac         : int -> tactic
1869
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   578
\end{ttbox}
3224
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   579
\indexbold{*Blast_tac}\indexbold{*Auto_tac}
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   580
\indexbold{*Best_tac}\indexbold{*Fast_tac}%
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   581
\indexbold{*Deepen_tac}
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   582
\indexbold{*Clarify_tac}\indexbold{*Clarify_step_tac}
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   583
\indexbold{*Safe_tac}\indexbold{*Safe_step_tac}
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   584
\indexbold{*Step_tac}
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   585
make use of the current claset.  For example, \texttt{Blast_tac} is defined as 
1869
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   586
\begin{ttbox}
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   587
fun Blast_tac i st = blast_tac (!claset) i st;
1869
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   588
\end{ttbox}
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   589
and gets the current claset, \ttindex{!claset}, only after it is applied to a
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   590
proof state.  The functions
1869
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   591
\begin{ttbox}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   592
AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   593
\end{ttbox}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   594
\indexbold{*AddSIs} \indexbold{*AddSEs} \indexbold{*AddSDs}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   595
\indexbold{*AddIs} \indexbold{*AddEs} \indexbold{*AddDs}
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3224
diff changeset
   596
are used to add rules to the current claset.  They work exactly like their
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   597
lower case counterparts, such as \texttt{addSIs}.  Calling
1869
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   598
\begin{ttbox}
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   599
Delrules : thm list -> unit
065bd29adc7a Added section about current claset.
berghofe
parents: 1099
diff changeset
   600
\end{ttbox}
3224
4ea2aa9f93a5 Documented auto_tac
paulson
parents: 3108
diff changeset
   601
deletes rules from the current claset. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   602
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   603
\subsection{Other useful tactics}
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   604
\index{tactics!for contradiction}
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   605
\index{tactics!for Modus Ponens}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   606
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   607
contr_tac    :             int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   608
mp_tac       :             int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   609
eq_mp_tac    :             int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   610
swap_res_tac : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   611
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   612
These can be used in the body of a specialized search.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   613
\begin{ttdescription}
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   614
\item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   615
  solves subgoal~$i$ by detecting a contradiction among two assumptions of
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   616
  the form $P$ and~$\neg P$, or fail.  It may instantiate unknowns.  The
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   617
  tactic can produce multiple outcomes, enumerating all possible
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   618
  contradictions.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   619
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   620
\item[\ttindexbold{mp_tac} {\it i}] 
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   621
is like \texttt{contr_tac}, but also attempts to perform Modus Ponens in
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   622
subgoal~$i$.  If there are assumptions $P\imp Q$ and~$P$, then it replaces
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   623
$P\imp Q$ by~$Q$.  It may instantiate unknowns.  It fails if it can do
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   624
nothing.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   625
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   626
\item[\ttindexbold{eq_mp_tac} {\it i}] 
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   627
is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   628
is safe.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   629
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   630
\item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   631
the proof state using {\it thms}, which should be a list of introduction
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   632
rules.  First, it attempts to prove the goal using \texttt{assume_tac} or
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   633
\texttt{contr_tac}.  It then attempts to apply each rule in turn, attempting
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   634
resolution and also elim-resolution with the swapped form.
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   635
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   636
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   637
\subsection{Creating swapped rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   638
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   639
swapify   : thm list -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   640
joinrules : thm list * thm list -> (bool * thm) list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   641
\end{ttbox}
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   642
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   643
\item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   644
swapped versions of~{\it thms}, regarded as introduction rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   645
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   646
\item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   647
joins introduction rules, their swapped versions, and elimination rules for
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   648
use with \ttindex{biresolve_tac}.  Each rule is paired with~\texttt{false}
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   649
(indicating ordinary resolution) or~\texttt{true} (indicating
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   650
elim-resolution).
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   651
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   652
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   653
3716
2885b760a4b4 Clarify_tac and some textual improvements
paulson
parents: 3485
diff changeset
   654
\section{Setting up the classical reasoner}\label{sec:classical-setup}
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   655
\index{classical reasoner!setting up}
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   656
Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL}, have
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   657
the classical reasoner already set up.  When defining a new classical logic,
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
   658
you should set up the reasoner yourself.  It consists of the \ML{} functor
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   659
\ttindex{ClassicalFun}, which takes the argument
3720
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   660
signature \texttt{
a5b9e0ade194 Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents: 3716
diff changeset
   661
                  CLASSICAL_DATA}:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   662
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   663
signature CLASSICAL_DATA =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   664
  sig
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   665
  val mp             : thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   666
  val not_elim       : thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   667
  val swap           : thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   668
  val sizef          : thm -> int
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   669
  val hyp_subst_tacs : (int -> tactic) list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   670
  end;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   671
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   672
Thus, the functor requires the following items:
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   673
\begin{ttdescription}
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   674
\item[\tdxbold{mp}] should be the Modus Ponens rule
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   675
$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   676
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   677
\item[\tdxbold{not_elim}] should be the contradiction rule
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   678
$\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   679
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   680
\item[\tdxbold{swap}] should be the swap rule
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   681
$\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   682
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   683
\item[\ttindexbold{sizef}] is the heuristic function used for best-first
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   684
search.  It should estimate the size of the remaining subgoals.  A good
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   685
heuristic function is \ttindex{size_of_thm}, which measures the size of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   686
proof state.  Another size function might ignore certain subgoals (say,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   687
those concerned with type checking).  A heuristic function might simply
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   688
count the subgoals.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   689
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   690
\item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   691
the hypotheses, typically created by \ttindex{HypsubstFun} (see
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   692
Chapter~\ref{substitution}).  This list can, of course, be empty.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   693
tactics are assumed to be safe!
308
f4cecad9b6a0 modifications towards final draft
lcp
parents: 286
diff changeset
   694
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   695
The functor is not at all sensitive to the formalization of the
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   696
object-logic.  It does not even examine the rules, but merely applies
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   697
them according to its fixed strategy.  The functor resides in {\tt
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3089
diff changeset
   698
  Provers/classical.ML} in the Isabelle sources.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   699
319
f143f7686cd6 penultimate Springer draft
lcp
parents: 308
diff changeset
   700
\index{classical reasoner|)}