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