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: