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