doc-src/Ref/classical.tex
 author wenzelm Sun Oct 31 20:11:23 1999 +0100 (1999-10-31) changeset 7990 0a604b2fc2b1 parent 6592 c120262044b6 child 8136 8c65f3ca13f2 permissions -rw-r--r--
updated;
     1 %% $Id$

     2 \chapter{The Classical Reasoner}\label{chap:classical}

     3 \index{classical reasoner|(}

     4 \newcommand\ainfer{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}

     5

     6 Although Isabelle is generic, many users will be working in some

     7 extension of classical first-order logic.

     8 Isabelle's set theory~{\tt ZF} is built upon theory~\texttt{FOL},

     9 while {\HOL} conceptually contains first-order logic as a fragment.

    10 Theorem-proving in predicate logic is undecidable, but many

    11 researchers have developed strategies to assist in this task.

    12

    13 Isabelle's classical reasoner is an \ML{} functor that accepts certain

    14 information about a logic and delivers a suite of automatic tactics.  Each

    15 tactic takes a collection of rules and executes a simple, non-clausal proof

    16 procedure.  They are slow and simplistic compared with resolution theorem

    17 provers, but they can save considerable time and effort.  They can prove

    18 theorems such as Pelletier's~\cite{pelletier86} problems~40 and~41 in

    19 seconds:

    20 $(\exists y. \forall x. J(y,x) \bimp \neg J(x,x))   21 \imp \neg (\forall x. \exists y. \forall z. J(z,y) \bimp \neg J(z,x))$

    22 $(\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x))   23 \imp \neg (\exists z. \forall x. F(x,z))   24$

    25 %

    26 The tactics are generic.  They are not restricted to first-order logic, and

    27 have been heavily used in the development of Isabelle's set theory.  Few

    28 interactive proof assistants provide this much automation.  The tactics can

    29 be traced, and their components can be called directly; in this manner,

    30 any proof can be viewed interactively.

    31

    32 The simplest way to apply the classical reasoner (to subgoal~$i$) is to type

    33 \begin{ttbox}

    34 by (Blast_tac $$i$$);

    35 \end{ttbox}

    36 This command quickly proves most simple formulas of the predicate calculus or

    37 set theory.  To attempt to prove subgoals using a combination of

    38 rewriting and classical reasoning, try

    39 \begin{ttbox}

    40 auto();                         \emph{\textrm{applies to all subgoals}}

    41 force i;                        \emph{\textrm{applies to one subgoal}}

    42 \end{ttbox}

    43 To do all obvious logical steps, even if they do not prove the

    44 subgoal, type one of the following:

    45 \begin{ttbox}

    46 by Safe_tac;                   \emph{\textrm{applies to all subgoals}}

    47 by (Clarify_tac $$i$$);            \emph{\textrm{applies to one subgoal}}

    48 \end{ttbox}

    49

    50

    51 You need to know how the classical reasoner works in order to use it

    52 effectively.  There are many tactics to choose from, including

    53 {\tt Fast_tac} and \texttt{Best_tac}.

    54

    55 We shall first discuss the underlying principles, then present the

    56 classical reasoner.  Finally, we shall see how to instantiate it for new logics.

    57 The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already installed.

    58

    59

    60 \section{The sequent calculus}

    61 \index{sequent calculus}

    62 Isabelle supports natural deduction, which is easy to use for interactive

    63 proof.  But natural deduction does not easily lend itself to automation,

    64 and has a bias towards intuitionism.  For certain proofs in classical

    65 logic, it can not be called natural.  The {\bf sequent calculus}, a

    66 generalization of natural deduction, is easier to automate.

    67

    68 A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$

    69 and~$\Delta$ are sets of formulae.%

    70 \footnote{For first-order logic, sequents can equivalently be made from

    71   lists or multisets of formulae.} The sequent

    72 $P@1,\ldots,P@m\turn Q@1,\ldots,Q@n$

    73 is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj   74 Q@n$.  Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true,

    75 while $Q@1,\ldots,Q@n$ represent alternative goals.  A sequent is {\bf

    76 basic} if its left and right sides have a common formula, as in $P,Q\turn   77 Q,R$; basic sequents are trivially valid.

    78

    79 Sequent rules are classified as {\bf right} or {\bf left}, indicating which

    80 side of the $\turn$~symbol they operate on.  Rules that operate on the

    81 right side are analogous to natural deduction's introduction rules, and

    82 left rules are analogous to elimination rules.

    83 Recall the natural deduction rules for

    84   first-order logic,

    85 \iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%

    86                           {Fig.\ts\ref{fol-fig}}.

    87 The sequent calculus analogue of~$({\imp}I)$ is the rule

    88 $$  89 \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}   90 \eqno({\imp}R)   91$$

    92 This breaks down some implication on the right side of a sequent; $\Gamma$

    93 and $\Delta$ stand for the sets of formulae that are unaffected by the

    94 inference.  The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the

    95 single rule

    96 $$  97 \ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}   98 \eqno({\disj}R)   99$$

   100 This breaks down some disjunction on the right side, replacing it by both

   101 disjuncts.  Thus, the sequent calculus is a kind of multiple-conclusion logic.

   102

   103 To illustrate the use of multiple formulae on the right, let us prove

   104 the classical theorem $(P\imp Q)\disj(Q\imp P)$.  Working backwards, we

   105 reduce this formula to a basic sequent:

   106 $\infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)}   107 {\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;}   108 {\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad}   109 {P, Q \turn Q, P\qquad\qquad}}}   110$

   111 This example is typical of the sequent calculus: start with the desired

   112 theorem and apply rules backwards in a fairly arbitrary manner.  This yields a

   113 surprisingly effective proof procedure.  Quantifiers add few complications,

   114 since Isabelle handles parameters and schematic variables.  See Chapter~10

   115 of {\em ML for the Working Programmer}~\cite{paulson-ml2} for further

   116 discussion.

   117

   118

   119 \section{Simulating sequents by natural deduction}

   120 Isabelle can represent sequents directly, as in the object-logic~\texttt{LK}\@.

   121 But natural deduction is easier to work with, and most object-logics employ

   122 it.  Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn   123 Q@1,\ldots,Q@n$ by the Isabelle formula

   124 $\List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1,$

   125 where the order of the assumptions and the choice of~$Q@1$ are arbitrary.

   126 Elim-resolution plays a key role in simulating sequent proofs.

   127

   128 We can easily handle reasoning on the left.

   129 As discussed in

   130 \iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}},

   131 elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$

   132 achieves a similar effect as the corresponding sequent rules.  For the

   133 other connectives, we use sequent-style elimination rules instead of

   134 destruction rules such as $({\conj}E1,2)$ and $(\forall E)$.  But note that

   135 the rule $(\neg L)$ has no effect under our representation of sequents!

   136 $$  137 \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}\eqno({\neg}L)   138$$

   139 What about reasoning on the right?  Introduction rules can only affect the

   140 formula in the conclusion, namely~$Q@1$.  The other right-side formulae are

   141 represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.

   142 \index{assumptions!negated}

   143 In order to operate on one of these, it must first be exchanged with~$Q@1$.

   144 Elim-resolution with the {\bf swap} rule has this effect:

   145 $$\List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap)$$

   146 To ensure that swaps occur only when necessary, each introduction rule is

   147 converted into a swapped form: it is resolved with the second premise

   148 of~$(swap)$.  The swapped form of~$({\conj}I)$, which might be

   149 called~$({\neg\conj}E)$, is

   150 $\List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R.$

   151 Similarly, the swapped form of~$({\imp}I)$ is

   152 $\List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R$

   153 Swapped introduction rules are applied using elim-resolution, which deletes

   154 the negated formula.  Our representation of sequents also requires the use

   155 of ordinary introduction rules.  If we had no regard for readability, we

   156 could treat the right side more uniformly by representing sequents as

   157 $\List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot.$

   158

   159

   160 \section{Extra rules for the sequent calculus}

   161 As mentioned, destruction rules such as $({\conj}E1,2)$ and $(\forall E)$

   162 must be replaced by sequent-style elimination rules.  In addition, we need

   163 rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj   164 Q$.  The introduction rules~$({\disj}I1,2)$ are replaced by a rule that

   165 simulates $({\disj}R)$:

   166 $(\neg Q\Imp P) \Imp P\disj Q$

   167 The destruction rule $({\imp}E)$ is replaced by

   168 $\List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R.$

   169 Quantifier replication also requires special rules.  In classical logic,

   170 $\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules

   171 $(\exists R)$ and $(\forall L)$ are dual:

   172 $\ainfer{\Gamma &\turn \Delta, \exists x{.}P}   173 {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R)   174 \qquad   175 \ainfer{\forall x{.}P, \Gamma &\turn \Delta}   176 {P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L)   177$

   178 Thus both kinds of quantifier may be replicated.  Theorems requiring

   179 multiple uses of a universal formula are easy to invent; consider

   180 $(\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)),$

   181 for any~$n>1$.  Natural examples of the multiple use of an existential

   182 formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$.

   183

   184 Forgoing quantifier replication loses completeness, but gains decidability,

   185 since the search space becomes finite.  Many useful theorems can be proved

   186 without replication, and the search generally delivers its verdict in a

   187 reasonable time.  To adopt this approach, represent the sequent rules

   188 $(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists   189 E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination

   190 form:

   191 $$\List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q \eqno(\forall E@2)$$

   192 Elim-resolution with this rule will delete the universal formula after a

   193 single use.  To replicate universal quantifiers, replace the rule by

   194 $$  195 \List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.   196 \eqno(\forall E@3)   197$$

   198 To replicate existential quantifiers, replace $(\exists I)$ by

   199 $\List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x).$

   200 All introduction rules mentioned above are also useful in swapped form.

   201

   202 Replication makes the search space infinite; we must apply the rules with

   203 care.  The classical reasoner distinguishes between safe and unsafe

   204 rules, applying the latter only when there is no alternative.  Depth-first

   205 search may well go down a blind alley; best-first search is better behaved

   206 in an infinite search space.  However, quantifier replication is too

   207 expensive to prove any but the simplest theorems.

   208

   209

   210 \section{Classical rule sets}

   211 \index{classical sets}

   212 Each automatic tactic takes a {\bf classical set} --- a collection of

   213 rules, classified as introduction or elimination and as {\bf safe} or {\bf

   214 unsafe}.  In general, safe rules can be attempted blindly, while unsafe

   215 rules must be used with care.  A safe rule must never reduce a provable

   216 goal to an unprovable set of subgoals.

   217

   218 The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$.  Any

   219 rule is unsafe whose premises contain new unknowns.  The elimination

   220 rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,

   221 which discards the assumption $\forall x{.}P(x)$ and replaces it by the

   222 weaker assumption~$P(\Var{t})$.  The rule $({\exists}I)$ is unsafe for

   223 similar reasons.  The rule~$(\forall E@3)$ is unsafe in a different sense:

   224 since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.

   225 In classical first-order logic, all rules are safe except those mentioned

   226 above.

   227

   228 The safe/unsafe distinction is vague, and may be regarded merely as a way

   229 of giving some rules priority over others.  One could argue that

   230 $({\disj}E)$ is unsafe, because repeated application of it could generate

   231 exponentially many subgoals.  Induction rules are unsafe because inductive

   232 proofs are difficult to set up automatically.  Any inference is unsafe that

   233 instantiates an unknown in the proof state --- thus \ttindex{match_tac}

   234 must be used, rather than \ttindex{resolve_tac}.  Even proof by assumption

   235 is unsafe if it instantiates unknowns shared with other subgoals --- thus

   236 \ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.

   237

   238 \subsection{Adding rules to classical sets}

   239 Classical rule sets belong to the abstract type \mltydx{claset}, which

   240 supports the following operations (provided the classical reasoner is

   241 installed!):

   242 \begin{ttbox}

   243 empty_cs    : claset

   244 print_cs    : claset -> unit

   245 rep_cs      : claset -> {safeEs: thm list, safeIs: thm list,

   246                          hazEs: thm list,  hazIs: thm list,

   247                          swrappers: (string * wrapper) list,

   248                          uwrappers: (string * wrapper) list,

   249                          safe0_netpair: netpair, safep_netpair: netpair,

   250                            haz_netpair: netpair,   dup_netpair: netpair}

   251 addSIs      : claset * thm list -> claset                 \hfill{\bf infix 4}

   252 addSEs      : claset * thm list -> claset                 \hfill{\bf infix 4}

   253 addSDs      : claset * thm list -> claset                 \hfill{\bf infix 4}

   254 addIs       : claset * thm list -> claset                 \hfill{\bf infix 4}

   255 addEs       : claset * thm list -> claset                 \hfill{\bf infix 4}

   256 addDs       : claset * thm list -> claset                 \hfill{\bf infix 4}

   257 delrules    : claset * thm list -> claset                 \hfill{\bf infix 4}

   258 \end{ttbox}

   259 The add operations ignore any rule already present in the claset with the same

   260 classification (such as Safe Introduction).  They print a warning if the rule

   261 has already been added with some other classification, but add the rule

   262 anyway.  Calling \texttt{delrules} deletes all occurrences of a rule from the

   263 claset, but see the warning below concerning destruction rules.

   264 \begin{ttdescription}

   265 \item[\ttindexbold{empty_cs}] is the empty classical set.

   266

   267 \item[\ttindexbold{print_cs} $cs$] displays the printable contents of~$cs$,

   268   which is the rules. All other parts are non-printable.

   269

   270 \item[\ttindexbold{rep_cs} $cs$] decomposes $cs$ as a record of its internal

   271   components, namely the safe introduction and elimination rules, the unsafe

   272   introduction and elimination rules, the lists of safe and unsafe wrappers

   273   (see \ref{sec:modifying-search}), and the internalized forms of the rules.

   274

   275 \item[$cs$ addSIs $rules$] \indexbold{*addSIs}

   276 adds safe introduction~$rules$ to~$cs$.

   277

   278 \item[$cs$ addSEs $rules$] \indexbold{*addSEs}

   279 adds safe elimination~$rules$ to~$cs$.

   280

   281 \item[$cs$ addSDs $rules$] \indexbold{*addSDs}

   282 adds safe destruction~$rules$ to~$cs$.

   283

   284 \item[$cs$ addIs $rules$] \indexbold{*addIs}

   285 adds unsafe introduction~$rules$ to~$cs$.

   286

   287 \item[$cs$ addEs $rules$] \indexbold{*addEs}

   288 adds unsafe elimination~$rules$ to~$cs$.

   289

   290 \item[$cs$ addDs $rules$] \indexbold{*addDs}

   291 adds unsafe destruction~$rules$ to~$cs$.

   292

   293 \item[$cs$ delrules $rules$] \indexbold{*delrules}

   294 deletes~$rules$ from~$cs$.  It prints a warning for those rules that are not

   295 in~$cs$.

   296 \end{ttdescription}

   297

   298 \begin{warn}

   299   If you added $rule$ using \texttt{addSDs} or \texttt{addDs}, then you must delete

   300   it as follows:

   301 \begin{ttbox}

   302 $$cs$$ delrules [make_elim $$rule$$]

   303 \end{ttbox}

   304 \par\noindent

   305 This is necessary because the operators \texttt{addSDs} and \texttt{addDs} convert

   306 the destruction rules to elimination rules by applying \ttindex{make_elim},

   307 and then insert them using \texttt{addSEs} and \texttt{addEs}, respectively.

   308 \end{warn}

   309

   310 Introduction rules are those that can be applied using ordinary resolution.

   311 The classical set automatically generates their swapped forms, which will

   312 be applied using elim-resolution.  Elimination rules are applied using

   313 elim-resolution.  In a classical set, rules are sorted by the number of new

   314 subgoals they will yield; rules that generate the fewest subgoals will be

   315 tried first (see \S\ref{biresolve_tac}).

   316

   317 For elimination and destruction rules there are variants of the add operations

   318 adding a rule in a way such that it is applied only if also its second premise

   319 can be unified with an assumption of the current proof state:

   320 \indexbold{*addSE2}\indexbold{*addSD2}\indexbold{*addE2}\indexbold{*addD2}

   321 \begin{ttbox}

   322 addSE2      : claset * (string * thm) -> claset           \hfill{\bf infix 4}

   323 addSD2      : claset * (string * thm) -> claset           \hfill{\bf infix 4}

   324 addE2       : claset * (string * thm) -> claset           \hfill{\bf infix 4}

   325 addD2       : claset * (string * thm) -> claset           \hfill{\bf infix 4}

   326 \end{ttbox}

   327 \begin{warn}

   328   A rule to be added in this special way must be given a name, which is used

   329   to delete it again -- when desired -- using \texttt{delSWrappers} or

   330   \texttt{delWrappers}, respectively. This is because these add operations

   331   are implemented as wrappers (see \ref{sec:modifying-search} below).

   332 \end{warn}

   333

   334

   335 \subsection{Modifying the search step}

   336 \label{sec:modifying-search}

   337 For a given classical set, the proof strategy is simple.  Perform as many safe

   338 inferences as possible; or else, apply certain safe rules, allowing

   339 instantiation of unknowns; or else, apply an unsafe rule.  The tactics also

   340 eliminate assumptions of the form $x=t$ by substitution if they have been set

   341 up to do so (see \texttt{hyp_subst_tacs} in~\S\ref{sec:classical-setup} below).

   342 They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$

   343 and~$P$, then replace $P\imp Q$ by~$Q$.

   344

   345 The classical reasoning tactics --- except \texttt{blast_tac}! --- allow

   346 you to modify this basic proof strategy by applying two lists of arbitrary

   347 {\bf wrapper tacticals} to it.

   348 The first wrapper list, which is considered to contain safe wrappers only,

   349 affects \ttindex{safe_step_tac} and all the tactics that call it.

   350 The second one, which may contain unsafe wrappers, affects the unsafe parts

   351 of \ttindex{step_tac}, \ttindex{slow_step_tac}, and the tactics that call them.

   352 A wrapper transforms each step of the search, for example

   353 by attempting other tactics before or after the original step tactic.

   354 All members of a wrapper list are applied in turn to the respective step tactic.

   355

   356 Initially the two wrapper lists are empty, which means no modification of the

   357 step tactics. Safe and unsafe wrappers are added to a claset

   358 with the functions given below, supplying them with wrapper names.

   359 These names may be used to selectively delete wrappers.

   360

   361 \begin{ttbox}

   362 type wrapper = (int -> tactic) -> (int -> tactic);

   363

   364 addSWrapper  : claset * (string *  wrapper       ) -> claset \hfill{\bf infix 4}

   365 addSbefore   : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}

   366 addSaltern   : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}

   367 delSWrapper  : claset *  string                    -> claset \hfill{\bf infix 4}

   368

   369 addWrapper   : claset * (string *  wrapper       ) -> claset \hfill{\bf infix 4}

   370 addbefore    : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}

   371 addaltern    : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}

   372 delWrapper   : claset *  string                    -> claset \hfill{\bf infix 4}

   373

   374 addSss       : claset * simpset -> claset                 \hfill{\bf infix 4}

   375 addss        : claset * simpset -> claset                 \hfill{\bf infix 4}

   376 \end{ttbox}

   377 %

   378

   379 \begin{ttdescription}

   380 \item[$cs$ addSWrapper $(name,wrapper)$] \indexbold{*addSWrapper}

   381 adds a new wrapper, which should yield a safe tactic,

   382 to modify the existing safe step tactic.

   383

   384 \item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore}

   385 adds the given tactic as a safe wrapper, such that it is tried

   386 {\em before} each safe step of the search.

   387

   388 \item[$cs$ addSaltern $(name,tac)$] \indexbold{*addSaltern}

   389 adds the given tactic as a safe wrapper, such that it is tried

   390 when a safe step of the search would fail.

   391

   392 \item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper}

   393 deletes the safe wrapper with the given name.

   394

   395 \item[$cs$ addWrapper $(name,wrapper)$] \indexbold{*addWrapper}

   396 adds a new wrapper to modify the existing (unsafe) step tactic.

   397

   398 \item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore}

   399 adds the given tactic as an unsafe wrapper, such that it its result is

   400 concatenated {\em before} the result of each unsafe step.

   401

   402 \item[$cs$ addaltern $(name,tac)$] \indexbold{*addaltern}

   403 adds the given tactic as an unsafe wrapper, such that it its result is

   404 concatenated {\em after} the result of each unsafe step.

   405

   406 \item[$cs$ delWrapper $name$] \indexbold{*delWrapper}

   407 deletes the unsafe wrapper with the given name.

   408

   409 \item[$cs$ addSss $ss$] \indexbold{*addss}

   410 adds the simpset~$ss$ to the classical set.  The assumptions and goal will be

   411 simplified, in a rather safe way, after each safe step of the search.

   412

   413 \item[$cs$ addss $ss$] \indexbold{*addss}

   414 adds the simpset~$ss$ to the classical set.  The assumptions and goal will be

   415 simplified, before the each unsafe step of the search.

   416

   417 \end{ttdescription}

   418

   419 \index{simplification!from classical reasoner}

   420 Strictly speaking, the operators \texttt{addss} and \texttt{addSss}

   421 are not part of the classical reasoner.

   422 , which are used as primitives

   423 for the automatic tactics described in \S\ref{sec:automatic-tactics}, are

   424 implemented as wrapper tacticals.

   425 they

   426 \begin{warn}

   427 Being defined as wrappers, these operators are inappropriate for adding more

   428 than one simpset at a time: the simpset added last overwrites any earlier ones.

   429 When a simpset combined with a claset is to be augmented, this should done

   430 {\em before} combining it with the claset.

   431 \end{warn}

   432

   433

   434 \section{The classical tactics}

   435 \index{classical reasoner!tactics} If installed, the classical module provides

   436 powerful theorem-proving tactics.  Most of them have capitalized analogues

   437 that use the default claset; see \S\ref{sec:current-claset}.

   438

   439

   440 \subsection{The tableau prover}

   441 The tactic \texttt{blast_tac} searches for a proof using a fast tableau prover,

   442 coded directly in \ML.  It then reconstructs the proof using Isabelle

   443 tactics.  It is faster and more powerful than the other classical

   444 reasoning tactics, but has major limitations too.

   445 \begin{itemize}

   446 \item It does not use the wrapper tacticals described above, such as

   447   \ttindex{addss}.

   448 \item It ignores types, which can cause problems in \HOL.  If it applies a rule

   449   whose types are inappropriate, then proof reconstruction will fail.

   450 \item It does not perform higher-order unification, as needed by the rule {\tt

   451     rangeI} in {\HOL} and \texttt{RepFunI} in {\ZF}.  There are often

   452     alternatives to such rules, for example {\tt

   453     range_eqI} and \texttt{RepFun_eqI}.

   454 \item The message {\small\tt Function Var's argument not a bound variable\ }

   455 relates to the lack of higher-order unification.  Function variables

   456 may only be applied to parameters of the subgoal.

   457 \item Its proof strategy is more general than \texttt{fast_tac}'s but can be

   458   slower.  If \texttt{blast_tac} fails or seems to be running forever, try {\tt

   459   fast_tac} and the other tactics described below.

   460 \end{itemize}

   461 %

   462 \begin{ttbox}

   463 blast_tac        : claset -> int -> tactic

   464 Blast.depth_tac  : claset -> int -> int -> tactic

   465 Blast.trace      : bool ref \hfill{\bf initially false}

   466 \end{ttbox}

   467 The two tactics differ on how they bound the number of unsafe steps used in a

   468 proof.  While \texttt{blast_tac} starts with a bound of zero and increases it

   469 successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound.

   470 \begin{ttdescription}

   471 \item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove

   472   subgoal~$i$ using iterative deepening to increase the search bound.

   473

   474 \item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries

   475   to prove subgoal~$i$ using a search bound of $lim$.  Often a slow

   476   proof using \texttt{blast_tac} can be made much faster by supplying the

   477   successful search bound to this tactic instead.

   478

   479 \item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover}

   480   causes the tableau prover to print a trace of its search.  At each step it

   481   displays the formula currently being examined and reports whether the branch

   482   has been closed, extended or split.

   483 \end{ttdescription}

   484

   485

   486 \subsection{Automatic tactics}\label{sec:automatic-tactics}

   487 \begin{ttbox}

   488 type clasimpset = claset * simpset;

   489 auto_tac        : clasimpset ->        tactic

   490 force_tac       : clasimpset -> int -> tactic

   491 auto            : unit -> unit

   492 force           : int  -> unit

   493 \end{ttbox}

   494 The automatic tactics attempt to prove goals using a combination of

   495 simplification and classical reasoning.

   496 \begin{ttdescription}

   497 \item[\ttindexbold{auto_tac $(cs,ss)$}] is intended for situations where

   498 there are a lot of mostly trivial subgoals; it proves all the easy ones,

   499 leaving the ones it cannot prove.

   500 (Unfortunately, attempting to prove the hard ones may take a long time.)

   501 \item[\ttindexbold{force_tac} $(cs,ss)$ $i$] is intended to prove subgoal~$i$

   502 completely. It tries to apply all fancy tactics it knows about,

   503 performing a rather exhaustive search.

   504 \end{ttdescription}

   505 They must be supplied both a simpset and a claset; therefore

   506 they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which

   507 use the default claset and simpset (see \S\ref{sec:current-claset} below).

   508 For interactive use,

   509 the shorthand \texttt{auto();} abbreviates \texttt{by Auto_tac;}

   510 while \texttt{force 1;} abbreviates \texttt{by (Force_tac 1);}

   511

   512

   513 \subsection{Semi-automatic tactics}

   514 \begin{ttbox}

   515 clarify_tac      : claset -> int -> tactic

   516 clarify_step_tac : claset -> int -> tactic

   517 clarsimp_tac     : clasimpset -> int -> tactic

   518 \end{ttbox}

   519 Use these when the automatic tactics fail.  They perform all the obvious

   520 logical inferences that do not split the subgoal.  The result is a

   521 simpler subgoal that can be tackled by other means, such as by

   522 instantiating quantifiers yourself.

   523 \begin{ttdescription}

   524 \item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on

   525 subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}.

   526 \item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on

   527   subgoal~$i$.  No splitting step is applied; for example, the subgoal $A\conj   528 B$ is left as a conjunction.  Proof by assumption, Modus Ponens, etc., may be

   529   performed provided they do not instantiate unknowns.  Assumptions of the

   530   form $x=t$ may be eliminated.  The user-supplied safe wrapper tactical is

   531   applied.

   532 \item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but

   533 also does simplification with the given simpset. note that if the simpset

   534 includes a splitter for the premises, the subgoal may still be split.

   535 \end{ttdescription}

   536

   537

   538 \subsection{Other classical tactics}

   539 \begin{ttbox}

   540 fast_tac      : claset -> int -> tactic

   541 best_tac      : claset -> int -> tactic

   542 slow_tac      : claset -> int -> tactic

   543 slow_best_tac : claset -> int -> tactic

   544 \end{ttbox}

   545 These tactics attempt to prove a subgoal using sequent-style reasoning.

   546 Unlike \texttt{blast_tac}, they construct proofs directly in Isabelle.  Their

   547 effect is restricted (by \texttt{SELECT_GOAL}) to one subgoal; they either prove

   548 this subgoal or fail.  The \texttt{slow_} versions conduct a broader

   549 search.%

   550 \footnote{They may, when backtracking from a failed proof attempt, undo even

   551   the step of proving a subgoal by assumption.}

   552

   553 The best-first tactics are guided by a heuristic function: typically, the

   554 total size of the proof state.  This function is supplied in the functor call

   555 that sets up the classical reasoner.

   556 \begin{ttdescription}

   557 \item[\ttindexbold{fast_tac} $cs$ $i$] applies \texttt{step_tac} using

   558 depth-first search, to prove subgoal~$i$.

   559

   560 \item[\ttindexbold{best_tac} $cs$ $i$] applies \texttt{step_tac} using

   561 best-first search, to prove subgoal~$i$.

   562

   563 \item[\ttindexbold{slow_tac} $cs$ $i$] applies \texttt{slow_step_tac} using

   564 depth-first search, to prove subgoal~$i$.

   565

   566 \item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} using

   567 best-first search, to prove subgoal~$i$.

   568 \end{ttdescription}

   569

   570

   571 \subsection{Depth-limited automatic tactics}

   572 \begin{ttbox}

   573 depth_tac  : claset -> int -> int -> tactic

   574 deepen_tac : claset -> int -> int -> tactic

   575 \end{ttbox}

   576 These work by exhaustive search up to a specified depth.  Unsafe rules are

   577 modified to preserve the formula they act on, so that it be used repeatedly.

   578 They can prove more goals than \texttt{fast_tac} can but are much

   579 slower, for example if the assumptions have many universal quantifiers.

   580

   581 The depth limits the number of unsafe steps.  If you can estimate the minimum

   582 number of unsafe steps needed, supply this value as~$m$ to save time.

   583 \begin{ttdescription}

   584 \item[\ttindexbold{depth_tac} $cs$ $m$ $i$]

   585 tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.

   586

   587 \item[\ttindexbold{deepen_tac} $cs$ $m$ $i$]

   588 tries to prove subgoal~$i$ by iterative deepening.  It calls \texttt{depth_tac}

   589 repeatedly with increasing depths, starting with~$m$.

   590 \end{ttdescription}

   591

   592

   593 \subsection{Single-step tactics}

   594 \begin{ttbox}

   595 safe_step_tac : claset -> int -> tactic

   596 safe_tac      : claset        -> tactic

   597 inst_step_tac : claset -> int -> tactic

   598 step_tac      : claset -> int -> tactic

   599 slow_step_tac : claset -> int -> tactic

   600 \end{ttbox}

   601 The automatic proof procedures call these tactics.  By calling them

   602 yourself, you can execute these procedures one step at a time.

   603 \begin{ttdescription}

   604 \item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on

   605   subgoal~$i$.  The safe wrapper tacticals are applied to a tactic that may

   606   include proof by assumption or Modus Ponens (taking care not to instantiate

   607   unknowns), or substitution.

   608

   609 \item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all

   610 subgoals.  It is deterministic, with at most one outcome.

   611

   612 \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},

   613 but allows unknowns to be instantiated.

   614

   615 \item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof

   616   procedure.  The (unsafe) wrapper tacticals are applied to a tactic that tries

   617  \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule from~$cs$.

   618

   619 \item[\ttindexbold{slow_step_tac}]

   620   resembles \texttt{step_tac}, but allows backtracking between using safe

   621   rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules.

   622   The resulting search space is larger.

   623 \end{ttdescription}

   624

   625

   626 \subsection{The current claset}\label{sec:current-claset}

   627

   628 Each theory is equipped with an implicit \emph{current claset}

   629 \index{claset!current}.  This is a default set of classical

   630 rules.  The underlying idea is quite similar to that of a current

   631 simpset described in \S\ref{sec:simp-for-dummies}; please read that

   632 section, including its warnings.

   633

   634 The tactics

   635 \begin{ttbox}

   636 Blast_tac        : int -> tactic

   637 Auto_tac         :        tactic

   638 Force_tac        : int -> tactic

   639 Fast_tac         : int -> tactic

   640 Best_tac         : int -> tactic

   641 Deepen_tac       : int -> int -> tactic

   642 Clarify_tac      : int -> tactic

   643 Clarify_step_tac : int -> tactic

   644 Clarsimp_tac     : int -> tactic

   645 Safe_tac         :        tactic

   646 Safe_step_tac    : int -> tactic

   647 Step_tac         : int -> tactic

   648 \end{ttbox}

   649 \indexbold{*Blast_tac}\indexbold{*Auto_tac}\indexbold{*Force_tac}

   650 \indexbold{*Best_tac}\indexbold{*Fast_tac}%

   651 \indexbold{*Deepen_tac}

   652 \indexbold{*Clarify_tac}\indexbold{*Clarify_step_tac}\indexbold{*Clarsimp_tac}

   653 \indexbold{*Safe_tac}\indexbold{*Safe_step_tac}

   654 \indexbold{*Step_tac}

   655 make use of the current claset.  For example, \texttt{Blast_tac} is defined as

   656 \begin{ttbox}

   657 fun Blast_tac i st = blast_tac (claset()) i st;

   658 \end{ttbox}

   659 and gets the current claset, only after it is applied to a proof state.

   660 The functions

   661 \begin{ttbox}

   662 AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit

   663 \end{ttbox}

   664 \indexbold{*AddSIs} \indexbold{*AddSEs} \indexbold{*AddSDs}

   665 \indexbold{*AddIs} \indexbold{*AddEs} \indexbold{*AddDs}

   666 are used to add rules to the current claset.  They work exactly like their

   667 lower case counterparts, such as \texttt{addSIs}.  Calling

   668 \begin{ttbox}

   669 Delrules : thm list -> unit

   670 \end{ttbox}

   671 deletes rules from the current claset.

   672

   673 \medskip A few further functions are available as uppercase versions only:

   674 \begin{ttbox}

   675 AddXIs, AddXEs, AddXDs: thm list -> unit

   676 \end{ttbox}

   677 \indexbold{*AddXIs} \indexbold{*AddXEs} \indexbold{*AddXDs} augment the

   678 current claset by \emph{extra} introduction, elimination, or destruct rules.

   679 These provide additional hints for the basic non-automated proof methods of

   680 Isabelle/Isar \cite{isabelle-isar-ref}.  The corresponding Isar attributes are

   681 $intro!!$'', $elim!!$'', and $dest!!$''.  Note that these extra rules do

   682 not have any effect on classic Isabelle tactics.

   683

   684

   685 \subsection{Accessing the current claset}

   686 \label{sec:access-current-claset}

   687

   688 the functions to access the current claset are analogous to the functions

   689 for the current simpset, so please see \ref{sec:access-current-simpset}

   690 for a description.

   691 \begin{ttbox}

   692 claset        : unit   -> claset

   693 claset_ref    : unit   -> claset ref

   694 claset_of     : theory -> claset

   695 claset_ref_of : theory -> claset ref

   696 print_claset  : theory -> unit

   697 CLASET        :(claset     ->       tactic) ->       tactic

   698 CLASET'       :(claset     -> 'a -> tactic) -> 'a -> tactic

   699 CLASIMPSET    :(clasimpset ->       tactic) ->       tactic

   700 CLASIMPSET'   :(clasimpset -> 'a -> tactic) -> 'a -> tactic

   701 \end{ttbox}

   702

   703

   704 \subsection{Other useful tactics}

   705 \index{tactics!for contradiction}

   706 \index{tactics!for Modus Ponens}

   707 \begin{ttbox}

   708 contr_tac    :             int -> tactic

   709 mp_tac       :             int -> tactic

   710 eq_mp_tac    :             int -> tactic

   711 swap_res_tac : thm list -> int -> tactic

   712 \end{ttbox}

   713 These can be used in the body of a specialized search.

   714 \begin{ttdescription}

   715 \item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}

   716   solves subgoal~$i$ by detecting a contradiction among two assumptions of

   717   the form $P$ and~$\neg P$, or fail.  It may instantiate unknowns.  The

   718   tactic can produce multiple outcomes, enumerating all possible

   719   contradictions.

   720

   721 \item[\ttindexbold{mp_tac} {\it i}]

   722 is like \texttt{contr_tac}, but also attempts to perform Modus Ponens in

   723 subgoal~$i$.  If there are assumptions $P\imp Q$ and~$P$, then it replaces

   724 $P\imp Q$ by~$Q$.  It may instantiate unknowns.  It fails if it can do

   725 nothing.

   726

   727 \item[\ttindexbold{eq_mp_tac} {\it i}]

   728 is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it

   729 is safe.

   730

   731 \item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of

   732 the proof state using {\it thms}, which should be a list of introduction

   733 rules.  First, it attempts to prove the goal using \texttt{assume_tac} or

   734 \texttt{contr_tac}.  It then attempts to apply each rule in turn, attempting

   735 resolution and also elim-resolution with the swapped form.

   736 \end{ttdescription}

   737

   738 \subsection{Creating swapped rules}

   739 \begin{ttbox}

   740 swapify   : thm list -> thm list

   741 joinrules : thm list * thm list -> (bool * thm) list

   742 \end{ttbox}

   743 \begin{ttdescription}

   744 \item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the

   745 swapped versions of~{\it thms}, regarded as introduction rules.

   746

   747 \item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]

   748 joins introduction rules, their swapped versions, and elimination rules for

   749 use with \ttindex{biresolve_tac}.  Each rule is paired with~\texttt{false}

   750 (indicating ordinary resolution) or~\texttt{true} (indicating

   751 elim-resolution).

   752 \end{ttdescription}

   753

   754

   755 \section{Setting up the classical reasoner}\label{sec:classical-setup}

   756 \index{classical reasoner!setting up}

   757 Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL},

   758 have the classical reasoner already set up.

   759 When defining a new classical logic, you should set up the reasoner yourself.

   760 It consists of the \ML{} functor \ttindex{ClassicalFun}, which takes the

   761 argument signature \texttt{CLASSICAL_DATA}:

   762 \begin{ttbox}

   763 signature CLASSICAL_DATA =

   764   sig

   765   val mp             : thm

   766   val not_elim       : thm

   767   val swap           : thm

   768   val sizef          : thm -> int

   769   val hyp_subst_tacs : (int -> tactic) list

   770   end;

   771 \end{ttbox}

   772 Thus, the functor requires the following items:

   773 \begin{ttdescription}

   774 \item[\tdxbold{mp}] should be the Modus Ponens rule

   775 $\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.

   776

   777 \item[\tdxbold{not_elim}] should be the contradiction rule

   778 $\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.

   779

   780 \item[\tdxbold{swap}] should be the swap rule

   781 $\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.

   782

   783 \item[\ttindexbold{sizef}] is the heuristic function used for best-first

   784 search.  It should estimate the size of the remaining subgoals.  A good

   785 heuristic function is \ttindex{size_of_thm}, which measures the size of the

   786 proof state.  Another size function might ignore certain subgoals (say,

   787 those concerned with type-checking).  A heuristic function might simply

   788 count the subgoals.

   789

   790 \item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in

   791 the hypotheses, typically created by \ttindex{HypsubstFun} (see

   792 Chapter~\ref{substitution}).  This list can, of course, be empty.  The

   793 tactics are assumed to be safe!

   794 \end{ttdescription}

   795 The functor is not at all sensitive to the formalization of the

   796 object-logic.  It does not even examine the rules, but merely applies

   797 them according to its fixed strategy.  The functor resides in {\tt

   798   Provers/classical.ML} in the Isabelle sources.

   799

   800 \index{classical reasoner|)}

   801

   802 \section{Setting up the combination with the simplifier}

   803 \label{sec:clasimp-setup}

   804

   805 To combine the classical reasoner and the simplifier, we simply call the

   806 \ML{} functor \ttindex{ClasimpFun} that assembles the parts as required.

   807 It takes a structure (of signature \texttt{CLASIMP_DATA}) as

   808 argment, which can be contructed on the fly:

   809 \begin{ttbox}

   810 structure Clasimp = ClasimpFun

   811  (structure Simplifier = Simplifier

   812         and Classical  = Classical

   813         and Blast      = Blast);

   814 \end{ttbox}

   815 %

   816 %%% Local Variables:

   817 %%% mode: latex

   818 %%% TeX-master: "ref"

   819 %%% End: