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