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