author  obua 
Fri, 16 Sep 2005 21:02:15 +0200  
changeset 17440  df77edc4f5d0 
parent 12366  f0fd3c4f2f49 
child 30184  37969710e61f 
permissions  rwrr 
104  1 
%% $Id$ 
319  2 
\chapter{The Classical Reasoner}\label{chap:classical} 
286  3 
\index{classical reasoner(} 
308  4 
\newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}} 
5 

9695  6 
Although Isabelle is generic, many users will be working in some extension of 
7 
classical firstorder logic. Isabelle's set theory~ZF is built upon 

8 
theory~FOL, while HOL conceptually contains firstorder logic as a fragment. 

9 
Theoremproving in predicate logic is undecidable, but many researchers have 

10 
developed strategies to assist in this task. 

104  11 

286  12 
Isabelle's classical reasoner is an \ML{} functor that accepts certain 
104  13 
information about a logic and delivers a suite of automatic tactics. Each 
14 
tactic takes a collection of rules and executes a simple, nonclausal proof 

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

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

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

18 
seconds: 

19 
\[ (\exists y. \forall x. J(y,x) \bimp \neg J(x,x)) 

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

21 
\[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x)) 

22 
\imp \neg (\exists z. \forall x. F(x,z)) 

23 
\] 

308  24 
% 
25 
The tactics are generic. They are not restricted to firstorder logic, and 

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

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

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

29 
any proof can be viewed interactively. 

104  30 

3716  31 
The simplest way to apply the classical reasoner (to subgoal~$i$) is to type 
2479  32 
\begin{ttbox} 
3089  33 
by (Blast_tac \(i\)); 
2479  34 
\end{ttbox} 
3716  35 
This command quickly proves most simple formulas of the predicate calculus or 
5550  36 
set theory. To attempt to prove subgoals using a combination of 
3716  37 
rewriting and classical reasoning, try 
3224  38 
\begin{ttbox} 
5550  39 
auto(); \emph{\textrm{applies to all subgoals}} 
40 
force i; \emph{\textrm{applies to one subgoal}} 

3224  41 
\end{ttbox} 
3716  42 
To do all obvious logical steps, even if they do not prove the 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

43 
subgoal, type one of the following: 
3716  44 
\begin{ttbox} 
5550  45 
by Safe_tac; \emph{\textrm{applies to all subgoals}} 
5576
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

46 
by (Clarify_tac \(i\)); \emph{\textrm{applies to one subgoal}} 
3716  47 
\end{ttbox} 
5550  48 

49 

3716  50 
You need to know how the classical reasoner works in order to use it 
5550  51 
effectively. There are many tactics to choose from, including 
52 
{\tt Fast_tac} and \texttt{Best_tac}. 

2479  53 

9695  54 
We shall first discuss the underlying principles, then present the classical 
55 
reasoner. Finally, we shall see how to instantiate it for new logics. The 

56 
logics FOL, ZF, HOL and HOLCF have it already installed. 

104  57 

58 

59 
\section{The sequent calculus} 

60 
\index{sequent calculus} 

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

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

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

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

65 
generalization of natural deduction, is easier to automate. 

66 

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

308  68 
and~$\Delta$ are sets of formulae.% 
69 
\footnote{For firstorder logic, sequents can equivalently be made from 

70 
lists or multisets of formulae.} The sequent 

104  71 
\[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \] 
72 
is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj 

73 
Q@n$. Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true, 

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

75 
basic} if its left and right sides have a common formula, as in $P,Q\turn 

76 
Q,R$; basic sequents are trivially valid. 

77 

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

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

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

308  81 
left rules are analogous to elimination rules. 
82 
Recall the natural deduction rules for 

83 
firstorder logic, 

84 
\iflabelundefined{folfig}{from {\it Introduction to Isabelle}}% 

85 
{Fig.\ts\ref{folfig}}. 

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

3108  87 
$$ 
88 
\ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q} 

89 
\eqno({\imp}R) 

90 
$$ 

104  91 
This breaks down some implication on the right side of a sequent; $\Gamma$ 
92 
and $\Delta$ stand for the sets of formulae that are unaffected by the 

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

94 
single rule 

3108  95 
$$ 
96 
\ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q} 

97 
\eqno({\disj}R) 

98 
$$ 

104  99 
This breaks down some disjunction on the right side, replacing it by both 
100 
disjuncts. Thus, the sequent calculus is a kind of multipleconclusion logic. 

101 

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

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

104 
reduce this formula to a basic sequent: 

105 
\[ \infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)} 

106 
{\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;} 

107 
{\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad} 

108 
{P, Q \turn Q, P\qquad\qquad}}} 

109 
\] 

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

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

112 
surprisingly effective proof procedure. Quantifiers add few complications, 

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

6592  114 
of {\em ML for the Working Programmer}~\cite{paulsonml2} for further 
104  115 
discussion. 
116 

117 

118 
\section{Simulating sequents by natural deduction} 

3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

119 
Isabelle can represent sequents directly, as in the objectlogic~\texttt{LK}\@. 
104  120 
But natural deduction is easier to work with, and most objectlogics employ 
121 
it. Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn 

122 
Q@1,\ldots,Q@n$ by the Isabelle formula 

123 
\[ \List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1, \] 

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

125 
Elimresolution plays a key role in simulating sequent proofs. 

126 

127 
We can easily handle reasoning on the left. 

308  128 
As discussed in 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
9695
diff
changeset

129 
\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{{\S}\ref{destruct}}, 
104  130 
elimresolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$ 
131 
achieves a similar effect as the corresponding sequent rules. For the 

132 
other connectives, we use sequentstyle elimination rules instead of 

308  133 
destruction rules such as $({\conj}E1,2)$ and $(\forall E)$. But note that 
134 
the rule $(\neg L)$ has no effect under our representation of sequents! 

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

137 
$$ 

104  138 
What about reasoning on the right? Introduction rules can only affect the 
308  139 
formula in the conclusion, namely~$Q@1$. The other rightside formulae are 
319  140 
represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$. 
141 
\index{assumptions!negated} 

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

104  143 
Elimresolution with the {\bf swap} rule has this effect: 
3108  144 
$$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap) $$ 
104  145 
To ensure that swaps occur only when necessary, each introduction rule is 
146 
converted into a swapped form: it is resolved with the second premise 

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

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

149 
\[ \List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R. \] 

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

151 
\[ \List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R \] 

152 
Swapped introduction rules are applied using elimresolution, which deletes 

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

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

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

156 
\[ \List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot. \] 

157 

158 

159 
\section{Extra rules for the sequent calculus} 

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

161 
must be replaced by sequentstyle elimination rules. In addition, we need 

162 
rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj 

163 
Q$. The introduction rules~$({\disj}I1,2)$ are replaced by a rule that 

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

165 
\[ (\neg Q\Imp P) \Imp P\disj Q \] 

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

332  167 
\[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \] 
104  168 
Quantifier replication also requires special rules. In classical logic, 
308  169 
$\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules 
170 
$(\exists R)$ and $(\forall L)$ are dual: 

104  171 
\[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P} 
172 
{\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R) 

173 
\qquad 

174 
\ainfer{\forall x{.}P, \Gamma &\turn \Delta} 

175 
{P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L) 

176 
\] 

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

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

308  179 
\[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \] 
180 
for any~$n>1$. Natural examples of the multiple use of an existential 

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

104  182 

183 
Forgoing quantifier replication loses completeness, but gains decidability, 

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

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

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

187 
$(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists 

188 
E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination 

189 
form: 

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

191 
Elimresolution with this rule will delete the universal formula after a 

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

3108  193 
$$ 
194 
\List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q. 

195 
\eqno(\forall E@3) 

196 
$$ 

104  197 
To replicate existential quantifiers, replace $(\exists I)$ by 
332  198 
\[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \] 
104  199 
All introduction rules mentioned above are also useful in swapped form. 
200 

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

286  202 
care. The classical reasoner distinguishes between safe and unsafe 
104  203 
rules, applying the latter only when there is no alternative. Depthfirst 
204 
search may well go down a blind alley; bestfirst search is better behaved 

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

206 
expensive to prove any but the simplest theorems. 

207 

208 

209 
\section{Classical rule sets} 

319  210 
\index{classical sets} 
211 
Each automatic tactic takes a {\bf classical set}  a collection of 

104  212 
rules, classified as introduction or elimination and as {\bf safe} or {\bf 
213 
unsafe}. In general, safe rules can be attempted blindly, while unsafe 

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

308  215 
goal to an unprovable set of subgoals. 
104  216 

308  217 
The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$. Any 
218 
rule is unsafe whose premises contain new unknowns. The elimination 

219 
rule~$(\forall E@2)$ is unsafe, since it is applied via elimresolution, 

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

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

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

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

224 
In classical firstorder logic, all rules are safe except those mentioned 

225 
above. 

104  226 

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

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

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

230 
exponentially many subgoals. Induction rules are unsafe because inductive 

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

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

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

234 
is unsafe if it instantiates unknowns shared with other subgoals  thus 

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

236 

1099  237 
\subsection{Adding rules to classical sets} 
319  238 
Classical rule sets belong to the abstract type \mltydx{claset}, which 
286  239 
supports the following operations (provided the classical reasoner is 
104  240 
installed!): 
241 
\begin{ttbox} 

8136  242 
empty_cs : claset 
243 
print_cs : claset > unit 

244 
rep_cs : claset > \{safeEs: thm list, safeIs: thm list, 

245 
hazEs: thm list, hazIs: thm list, 

246 
swrappers: (string * wrapper) list, 

247 
uwrappers: (string * wrapper) list, 

248 
safe0_netpair: netpair, safep_netpair: netpair, 

249 
haz_netpair: netpair, dup_netpair: netpair\} 

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

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

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

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

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

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

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

104  257 
\end{ttbox} 
3089  258 
The add operations ignore any rule already present in the claset with the same 
8926  259 
classification (such as safe introduction). They print a warning if the rule 
3089  260 
has already been added with some other classification, but add the rule 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

261 
anyway. Calling \texttt{delrules} deletes all occurrences of a rule from the 
3089  262 
claset, but see the warning below concerning destruction rules. 
308  263 
\begin{ttdescription} 
104  264 
\item[\ttindexbold{empty_cs}] is the empty classical set. 
265 

4665  266 
\item[\ttindexbold{print_cs} $cs$] displays the printable contents of~$cs$, 
267 
which is the rules. All other parts are nonprintable. 

268 

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

4666  270 
components, namely the safe introduction and elimination rules, the unsafe 
271 
introduction and elimination rules, the lists of safe and unsafe wrappers 

272 
(see \ref{sec:modifyingsearch}), and the internalized forms of the rules. 

1099  273 

308  274 
\item[$cs$ addSIs $rules$] \indexbold{*addSIs} 
275 
adds safe introduction~$rules$ to~$cs$. 

104  276 

308  277 
\item[$cs$ addSEs $rules$] \indexbold{*addSEs} 
278 
adds safe elimination~$rules$ to~$cs$. 

104  279 

308  280 
\item[$cs$ addSDs $rules$] \indexbold{*addSDs} 
281 
adds safe destruction~$rules$ to~$cs$. 

104  282 

308  283 
\item[$cs$ addIs $rules$] \indexbold{*addIs} 
284 
adds unsafe introduction~$rules$ to~$cs$. 

104  285 

308  286 
\item[$cs$ addEs $rules$] \indexbold{*addEs} 
287 
adds unsafe elimination~$rules$ to~$cs$. 

104  288 

308  289 
\item[$cs$ addDs $rules$] \indexbold{*addDs} 
290 
adds unsafe destruction~$rules$ to~$cs$. 

1869  291 

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

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

308  295 
\end{ttdescription} 
296 

3089  297 
\begin{warn} 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

298 
If you added $rule$ using \texttt{addSDs} or \texttt{addDs}, then you must delete 
3089  299 
it as follows: 
300 
\begin{ttbox} 

301 
\(cs\) delrules [make_elim \(rule\)] 

302 
\end{ttbox} 

303 
\par\noindent 

3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

304 
This is necessary because the operators \texttt{addSDs} and \texttt{addDs} convert 
3089  305 
the destruction rules to elimination rules by applying \ttindex{make_elim}, 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

306 
and then insert them using \texttt{addSEs} and \texttt{addEs}, respectively. 
3089  307 
\end{warn} 
308 

104  309 
Introduction rules are those that can be applied using ordinary resolution. 
310 
The classical set automatically generates their swapped forms, which will 

311 
be applied using elimresolution. Elimination rules are applied using 

286  312 
elimresolution. In a classical set, rules are sorted by the number of new 
313 
subgoals they will yield; rules that generate the fewest subgoals will be 

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
9695
diff
changeset

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

5550  316 
For elimination and destruction rules there are variants of the add operations 
317 
adding a rule in a way such that it is applied only if also its second premise 

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

5576
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

319 
\indexbold{*addSE2}\indexbold{*addSD2}\indexbold{*addE2}\indexbold{*addD2} 
5550  320 
\begin{ttbox} 
321 
addSE2 : claset * (string * thm) > claset \hfill{\bf infix 4} 

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

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

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

325 
\end{ttbox} 

326 
\begin{warn} 

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

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

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

330 
are implemented as wrappers (see \ref{sec:modifyingsearch} below). 

331 
\end{warn} 

332 

1099  333 

334 
\subsection{Modifying the search step} 

4665  335 
\label{sec:modifyingsearch} 
3716  336 
For a given classical set, the proof strategy is simple. Perform as many safe 
337 
inferences as possible; or else, apply certain safe rules, allowing 

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

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

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
9695
diff
changeset

340 
up to do so (see \texttt{hyp_subst_tacs} in~{\S}\ref{sec:classicalsetup} below). 
3716  341 
They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$ 
342 
and~$P$, then replace $P\imp Q$ by~$Q$. 

104  343 

3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

344 
The classical reasoning tactics  except \texttt{blast_tac}!  allow 
4649  345 
you to modify this basic proof strategy by applying two lists of arbitrary 
346 
{\bf wrapper tacticals} to it. 

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

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

5550  349 
The second one, which may contain unsafe wrappers, affects the unsafe parts 
350 
of \ttindex{step_tac}, \ttindex{slow_step_tac}, and the tactics that call them. 

4649  351 
A wrapper transforms each step of the search, for example 
5550  352 
by attempting other tactics before or after the original step tactic. 
4649  353 
All members of a wrapper list are applied in turn to the respective step tactic. 
354 

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

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

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

358 
These names may be used to selectively delete wrappers. 

1099  359 

360 
\begin{ttbox} 

4649  361 
type wrapper = (int > tactic) > (int > tactic); 
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

362 

d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

363 
addSWrapper : claset * (string * wrapper ) > claset \hfill{\bf infix 4} 
4649  364 
addSbefore : claset * (string * (int > tactic)) > claset \hfill{\bf infix 4} 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
9695
diff
changeset

365 
addSafter : claset * (string * (int > tactic)) > claset \hfill{\bf infix 4} 
4649  366 
delSWrapper : claset * string > claset \hfill{\bf infix 4} 
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

367 

d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

368 
addWrapper : claset * (string * wrapper ) > claset \hfill{\bf infix 4} 
4649  369 
addbefore : claset * (string * (int > tactic)) > claset \hfill{\bf infix 4} 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
9695
diff
changeset

370 
addafter : claset * (string * (int > tactic)) > claset \hfill{\bf infix 4} 
4649  371 
delWrapper : claset * string > claset \hfill{\bf infix 4} 
372 

4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

373 
addSss : claset * simpset > claset \hfill{\bf infix 4} 
2632  374 
addss : claset * simpset > claset \hfill{\bf infix 4} 
1099  375 
\end{ttbox} 
376 
% 

377 

378 
\begin{ttdescription} 

4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

379 
\item[$cs$ addSWrapper $(name,wrapper)$] \indexbold{*addSWrapper} 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

380 
adds a new wrapper, which should yield a safe tactic, 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

381 
to modify the existing safe step tactic. 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

382 

d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

383 
\item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore} 
5550  384 
adds the given tactic as a safe wrapper, such that it is tried 
385 
{\em before} each safe step of the search. 

4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

386 

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
9695
diff
changeset

387 
\item[$cs$ addSafter $(name,tac)$] \indexbold{*addSafter} 
5550  388 
adds the given tactic as a safe wrapper, such that it is tried 
389 
when a safe step of the search would fail. 

4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

390 

d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

391 
\item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper} 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

392 
deletes the safe wrapper with the given name. 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

393 

d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

394 
\item[$cs$ addWrapper $(name,wrapper)$] \indexbold{*addWrapper} 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

395 
adds a new wrapper to modify the existing (unsafe) step tactic. 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

396 

d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

397 
\item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore} 
5550  398 
adds the given tactic as an unsafe wrapper, such that it its result is 
399 
concatenated {\em before} the result of each unsafe step. 

4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

400 

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
9695
diff
changeset

401 
\item[$cs$ addafter $(name,tac)$] \indexbold{*addafter} 
5550  402 
adds the given tactic as an unsafe wrapper, such that it its result is 
403 
concatenated {\em after} the result of each unsafe step. 

4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

404 

d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

405 
\item[$cs$ delWrapper $name$] \indexbold{*delWrapper} 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

406 
deletes the unsafe wrapper with the given name. 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

407 

d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

408 
\item[$cs$ addSss $ss$] \indexbold{*addss} 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

409 
adds the simpset~$ss$ to the classical set. The assumptions and goal will be 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

410 
simplified, in a rather safe way, after each safe step of the search. 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

411 

1099  412 
\item[$cs$ addss $ss$] \indexbold{*addss} 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3224
diff
changeset

413 
adds the simpset~$ss$ to the classical set. The assumptions and goal will be 
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

414 
simplified, before the each unsafe step of the search. 
2631
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

415 

4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

416 
\end{ttdescription} 
2631
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

417 

5550  418 
\index{simplification!from classical reasoner} 
419 
Strictly speaking, the operators \texttt{addss} and \texttt{addSss} 

420 
are not part of the classical reasoner. 

421 
, which are used as primitives 

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
9695
diff
changeset

422 
for the automatic tactics described in {\S}\ref{sec:automatictactics}, are 
5550  423 
implemented as wrapper tacticals. 
424 
they 

4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

425 
\begin{warn} 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

426 
Being defined as wrappers, these operators are inappropriate for adding more 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

427 
than one simpset at a time: the simpset added last overwrites any earlier ones. 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

428 
When a simpset combined with a claset is to be augmented, this should done 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

429 
{\em before} combining it with the claset. 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

430 
\end{warn} 
1099  431 

104  432 

433 
\section{The classical tactics} 

3716  434 
\index{classical reasoner!tactics} If installed, the classical module provides 
435 
powerful theoremproving tactics. Most of them have capitalized analogues 

11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
9695
diff
changeset

436 
that use the default claset; see {\S}\ref{sec:currentclaset}. 
3716  437 

104  438 

3224  439 
\subsection{The tableau prover} 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

440 
The tactic \texttt{blast_tac} searches for a proof using a fast tableau prover, 
3224  441 
coded directly in \ML. It then reconstructs the proof using Isabelle 
442 
tactics. It is faster and more powerful than the other classical 

443 
reasoning tactics, but has major limitations too. 

3089  444 
\begin{itemize} 
445 
\item It does not use the wrapper tacticals described above, such as 

446 
\ttindex{addss}. 

9695  447 
\item It ignores types, which can cause problems in HOL. If it applies a rule 
3089  448 
whose types are inappropriate, then proof reconstruction will fail. 
449 
\item It does not perform higherorder unification, as needed by the rule {\tt 

9695  450 
rangeI} in HOL and \texttt{RepFunI} in ZF. There are often alternatives 
451 
to such rules, for example {\tt range_eqI} and \texttt{RepFun_eqI}. 

8136  452 
\item Function variables may only be applied to parameters of the subgoal. 
453 
(This restriction arises because the prover does not use higherorder 

454 
unification.) If other function variables are present then the prover will 

455 
fail with the message {\small\tt Function Var's argument not a bound variable}. 

3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

456 
\item Its proof strategy is more general than \texttt{fast_tac}'s but can be 
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

457 
slower. If \texttt{blast_tac} fails or seems to be running forever, try {\tt 
3089  458 
fast_tac} and the other tactics described below. 
459 
\end{itemize} 

460 
% 

461 
\begin{ttbox} 

462 
blast_tac : claset > int > tactic 

463 
Blast.depth_tac : claset > int > int > tactic 

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

465 
\end{ttbox} 

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

3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

467 
proof. While \texttt{blast_tac} starts with a bound of zero and increases it 
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

468 
successively to~20, \texttt{Blast.depth_tac} applies a usersupplied search bound. 
3089  469 
\begin{ttdescription} 
470 
\item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove 

8284  471 
subgoal~$i$, increasing the search bound using iterative 
472 
deepening~\cite{korf85}. 

3089  473 

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

8284  475 
to prove subgoal~$i$ using a search bound of $lim$. Sometimes a slow 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

476 
proof using \texttt{blast_tac} can be made much faster by supplying the 
3089  477 
successful search bound to this tactic instead. 
478 

4317  479 
\item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover} 
3089  480 
causes the tableau prover to print a trace of its search. At each step it 
481 
displays the formula currently being examined and reports whether the branch 

482 
has been closed, extended or split. 

483 
\end{ttdescription} 

484 

3224  485 

4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

486 
\subsection{Automatic tactics}\label{sec:automatictactics} 
3224  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  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  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  504 
\end{ttdescription} 
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

505 
They must be supplied both a simpset and a claset; therefore 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

506 
they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
9695
diff
changeset

507 
use the default claset and simpset (see {\S}\ref{sec:currentclaset} below). 
4885  508 
For interactive use, 
509 
the shorthand \texttt{auto();} abbreviates \texttt{by Auto_tac;} 

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

3224  511 

5576
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

512 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

513 
\subsection{Semiautomatic tactics} 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

514 
\begin{ttbox} 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

515 
clarify_tac : claset > int > tactic 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

516 
clarify_step_tac : claset > int > tactic 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

517 
clarsimp_tac : clasimpset > int > tactic 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

518 
\end{ttbox} 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

519 
Use these when the automatic tactics fail. They perform all the obvious 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

520 
logical inferences that do not split the subgoal. The result is a 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

521 
simpler subgoal that can be tackled by other means, such as by 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

522 
instantiating quantifiers yourself. 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

523 
\begin{ttdescription} 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

524 
\item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

525 
subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}. 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

526 
\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

527 
subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

528 
B$ is left as a conjunction. Proof by assumption, Modus Ponens, etc., may be 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

529 
performed provided they do not instantiate unknowns. Assumptions of the 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

530 
form $x=t$ may be eliminated. The usersupplied safe wrapper tactical is 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

531 
applied. 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

532 
\item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but 
9439  533 
also does simplification with the given simpset. Note that if the simpset 
5577  534 
includes a splitter for the premises, the subgoal may still be split. 
5576
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

535 
\end{ttdescription} 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

536 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

537 

3224  538 
\subsection{Other classical tactics} 
332  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  544 
\end{ttbox} 
3224  545 
These tactics attempt to prove a subgoal using sequentstyle reasoning. 
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  549 
search.% 
550 
\footnote{They may, when backtracking from a failed proof attempt, undo even 

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 bestfirst 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  556 
\begin{ttdescription} 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

557 
\item[\ttindexbold{fast_tac} $cs$ $i$] applies \texttt{step_tac} using 
8136  558 
depthfirst search to prove subgoal~$i$. 
332  559 

3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

560 
\item[\ttindexbold{best_tac} $cs$ $i$] applies \texttt{step_tac} using 
8136  561 
bestfirst search to prove subgoal~$i$. 
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

562 

3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

563 
\item[\ttindexbold{slow_tac} $cs$ $i$] applies \texttt{slow_step_tac} using 
8136  564 
depthfirst search to prove subgoal~$i$. 
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

565 

8136  566 
\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with 
567 
bestfirst 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  571 
\subsection{Depthlimited 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  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  590 
\end{ttdescription} 
591 

592 

104  593 
\subsection{Singlestep tactics} 
594 
\begin{ttbox} 

595 
safe_step_tac : claset > int > tactic 

596 
safe_tac : claset > tactic 

597 
inst_step_tac : claset > int > tactic 

598 
step_tac : claset > int > tactic 

599 
slow_step_tac : claset > int > tactic 

600 
\end{ttbox} 

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

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

308  603 
\begin{ttdescription} 
104  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  606 
include proof by assumption or Modus Ponens (taking care not to instantiate 
607 
unknowns), or substitution. 

104  608 

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

3716  610 
subgoals. It is deterministic, with at most one outcome. 
104  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  613 
but allows unknowns to be instantiated. 
614 

1099  615 
\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof 
8136  616 
procedure. The unsafe wrapper tacticals are applied to a tactic that tries 
617 
\texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule 

618 
from~$cs$. 

104  619 

620 
\item[\ttindexbold{slow_step_tac}] 

3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

621 
resembles \texttt{step_tac}, but allows backtracking between using safe 
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

622 
rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules. 
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

623 
The resulting search space is larger. 
308  624 
\end{ttdescription} 
104  625 

5576
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

626 

3224  627 
\subsection{The current claset}\label{sec:currentclaset} 
4561  628 

5576
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

629 
Each theory is equipped with an implicit \emph{current claset} 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

630 
\index{claset!current}. This is a default set of classical 
4561  631 
rules. The underlying idea is quite similar to that of a current 
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
9695
diff
changeset

632 
simpset described in {\S}\ref{sec:simpfordummies}; please read that 
5576
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

633 
section, including its warnings. 
4561  634 

635 
The tactics 

1869  636 
\begin{ttbox} 
3716  637 
Blast_tac : int > tactic 
4507  638 
Auto_tac : tactic 
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

639 
Force_tac : int > tactic 
3716  640 
Fast_tac : int > tactic 
641 
Best_tac : int > tactic 

642 
Deepen_tac : int > int > tactic 

643 
Clarify_tac : int > tactic 

644 
Clarify_step_tac : int > tactic 

5550  645 
Clarsimp_tac : int > tactic 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

646 
Safe_tac : tactic 
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

647 
Safe_step_tac : int > tactic 
3716  648 
Step_tac : int > tactic 
1869  649 
\end{ttbox} 
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

650 
\indexbold{*Blast_tac}\indexbold{*Auto_tac}\indexbold{*Force_tac} 
3224  651 
\indexbold{*Best_tac}\indexbold{*Fast_tac}% 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

652 
\indexbold{*Deepen_tac} 
5576
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

653 
\indexbold{*Clarify_tac}\indexbold{*Clarify_step_tac}\indexbold{*Clarsimp_tac} 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

654 
\indexbold{*Safe_tac}\indexbold{*Safe_step_tac} 
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

655 
\indexbold{*Step_tac} 
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

656 
make use of the current claset. For example, \texttt{Blast_tac} is defined as 
1869  657 
\begin{ttbox} 
4561  658 
fun Blast_tac i st = blast_tac (claset()) i st; 
1869  659 
\end{ttbox} 
5576
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

660 
and gets the current claset, only after it is applied to a proof state. 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

661 
The functions 
1869  662 
\begin{ttbox} 
663 
AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list > unit 

664 
\end{ttbox} 

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

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

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3224
diff
changeset

667 
are used to add rules to the current claset. They work exactly like their 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

668 
lower case counterparts, such as \texttt{addSIs}. Calling 
1869  669 
\begin{ttbox} 
670 
Delrules : thm list > unit 

671 
\end{ttbox} 

3224  672 
deletes rules from the current claset. 
104  673 

5576
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

674 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

675 
\subsection{Accessing the current claset} 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

676 
\label{sec:accesscurrentclaset} 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

677 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

678 
the functions to access the current claset are analogous to the functions 
5577  679 
for the current simpset, so please see \ref{sec:accesscurrentsimpset} 
5576
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

680 
for a description. 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

681 
\begin{ttbox} 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

682 
claset : unit > claset 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

683 
claset_ref : unit > claset ref 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

684 
claset_of : theory > claset 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

685 
claset_ref_of : theory > claset ref 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

686 
print_claset : theory > unit 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

687 
CLASET :(claset > tactic) > tactic 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

688 
CLASET' :(claset > 'a > tactic) > 'a > tactic 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

689 
CLASIMPSET :(clasimpset > tactic) > tactic 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

690 
CLASIMPSET' :(clasimpset > 'a > tactic) > 'a > tactic 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

691 
\end{ttbox} 
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

692 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

693 

104  694 
\subsection{Other useful tactics} 
319  695 
\index{tactics!for contradiction} 
696 
\index{tactics!for Modus Ponens} 

104  697 
\begin{ttbox} 
698 
contr_tac : int > tactic 

699 
mp_tac : int > tactic 

700 
eq_mp_tac : int > tactic 

701 
swap_res_tac : thm list > int > tactic 

702 
\end{ttbox} 

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

308  704 
\begin{ttdescription} 
319  705 
\item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory} 
706 
solves subgoal~$i$ by detecting a contradiction among two assumptions of 

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

708 
tactic can produce multiple outcomes, enumerating all possible 

709 
contradictions. 

104  710 

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

3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

712 
is like \texttt{contr_tac}, but also attempts to perform Modus Ponens in 
104  713 
subgoal~$i$. If there are assumptions $P\imp Q$ and~$P$, then it replaces 
714 
$P\imp Q$ by~$Q$. It may instantiate unknowns. It fails if it can do 

715 
nothing. 

716 

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

3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

718 
is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns  thus, it 
104  719 
is safe. 
720 

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

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

3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

723 
rules. First, it attempts to prove the goal using \texttt{assume_tac} or 
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

724 
\texttt{contr_tac}. It then attempts to apply each rule in turn, attempting 
104  725 
resolution and also elimresolution with the swapped form. 
308  726 
\end{ttdescription} 
104  727 

728 
\subsection{Creating swapped rules} 

729 
\begin{ttbox} 

730 
swapify : thm list > thm list 

731 
joinrules : thm list * thm list > (bool * thm) list 

732 
\end{ttbox} 

308  733 
\begin{ttdescription} 
104  734 
\item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the 
735 
swapped versions of~{\it thms}, regarded as introduction rules. 

736 

308  737 
\item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})] 
104  738 
joins introduction rules, their swapped versions, and elimination rules for 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

739 
use with \ttindex{biresolve_tac}. Each rule is paired with~\texttt{false} 
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

740 
(indicating ordinary resolution) or~\texttt{true} (indicating 
104  741 
elimresolution). 
308  742 
\end{ttdescription} 
104  743 

744 

3716  745 
\section{Setting up the classical reasoner}\label{sec:classicalsetup} 
319  746 
\index{classical reasoner!setting up} 
5550  747 
Isabelle's classical objectlogics, including \texttt{FOL} and \texttt{HOL}, 
748 
have the classical reasoner already set up. 

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

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

751 
argument signature \texttt{CLASSICAL_DATA}: 

104  752 
\begin{ttbox} 
753 
signature CLASSICAL_DATA = 

754 
sig 

755 
val mp : thm 

756 
val not_elim : thm 

757 
val swap : thm 

758 
val sizef : thm > int 

759 
val hyp_subst_tacs : (int > tactic) list 

760 
end; 

761 
\end{ttbox} 

762 
Thus, the functor requires the following items: 

308  763 
\begin{ttdescription} 
319  764 
\item[\tdxbold{mp}] should be the Modus Ponens rule 
104  765 
$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$. 
766 

319  767 
\item[\tdxbold{not_elim}] should be the contradiction rule 
104  768 
$\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$. 
769 

319  770 
\item[\tdxbold{swap}] should be the swap rule 
104  771 
$\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$. 
772 

773 
\item[\ttindexbold{sizef}] is the heuristic function used for bestfirst 

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

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

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

6170  777 
those concerned with typechecking). A heuristic function might simply 
104  778 
count the subgoals. 
779 

319  780 
\item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in 
104  781 
the hypotheses, typically created by \ttindex{HypsubstFun} (see 
782 
Chapter~\ref{substitution}). This list can, of course, be empty. The 

783 
tactics are assumed to be safe! 

308  784 
\end{ttdescription} 
104  785 
The functor is not at all sensitive to the formalization of the 
3108  786 
objectlogic. It does not even examine the rules, but merely applies 
787 
them according to its fixed strategy. The functor resides in {\tt 

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

104  789 

319  790 
\index{classical reasoner)} 
5371  791 

5550  792 
\section{Setting up the combination with the simplifier} 
793 
\label{sec:clasimpsetup} 

5371  794 

5550  795 
To combine the classical reasoner and the simplifier, we simply call the 
796 
\ML{} functor \ttindex{ClasimpFun} that assembles the parts as required. 

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

798 
argment, which can be contructed on the fly: 

799 
\begin{ttbox} 

800 
structure Clasimp = ClasimpFun 

801 
(structure Simplifier = Simplifier 

802 
and Classical = Classical 

803 
and Blast = Blast); 

804 
\end{ttbox} 

805 
% 

5371  806 
%%% Local Variables: 
807 
%%% mode: latex 

808 
%%% TeXmaster: "ref" 

809 
%%% End: 