author  paulson 
Tue, 18 Jan 2000 11:33:31 +0100  
changeset 8136  8c65f3ca13f2 
parent 7990  0a604b2fc2b1 
child 8284  95c022a866ca 
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 

3108  6 
Although Isabelle is generic, many users will be working in some 
5577  7 
extension of classical firstorder logic. 
8 
Isabelle's set theory~{\tt ZF} is built upon theory~\texttt{FOL}, 

9 
while {\HOL} conceptually contains firstorder logic as a fragment. 

3108  10 
Theoremproving in predicate logic is undecidable, but many 
308  11 
researchers have developed strategies to assist in this task. 
104  12 

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

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

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

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

19 
seconds: 

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

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

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

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

24 
\] 

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

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

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

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

30 
any proof can be viewed interactively. 

104  31 

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

3224  42 
\end{ttbox} 
3716  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  45 
\begin{ttbox} 
5550  46 
by Safe_tac; \emph{\textrm{applies to all subgoals}} 
5576
dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

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

50 

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

2479  54 

3108  55 
We shall first discuss the underlying principles, then present the 
5550  56 
classical reasoner. Finally, we shall see how to instantiate it for new logics. 
57 
The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already installed. 

104  58 

59 

60 
\section{The sequent calculus} 

61 
\index{sequent calculus} 

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

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

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

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

66 
generalization of natural deduction, is easier to automate. 

67 

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

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

71 
lists or multisets of formulae.} The sequent 

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

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

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

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

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

78 

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

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

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

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

84 
firstorder logic, 

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

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

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

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

90 
\eqno({\imp}R) 

91 
$$ 

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

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

95 
single rule 

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

98 
\eqno({\disj}R) 

99 
$$ 

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

102 

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

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

105 
reduce this formula to a basic sequent: 

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

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

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

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

110 
\] 

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

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

113 
surprisingly effective proof procedure. Quantifiers add few complications, 

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

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

118 

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 objectlogic~\texttt{LK}\@. 
104  121 
But natural deduction is easier to work with, and most objectlogics employ 
122 
it. Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn 

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

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

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

126 
Elimresolution plays a key role in simulating sequent proofs. 

127 

128 
We can easily handle reasoning on the left. 

308  129 
As discussed in 
130 
\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}}, 

104  131 
elimresolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$ 
132 
achieves a similar effect as the corresponding sequent rules. For the 

133 
other connectives, we use sequentstyle elimination rules instead of 

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

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

138 
$$ 

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

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

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

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

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

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

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

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

153 
Swapped introduction rules are applied using elimresolution, which deletes 

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

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

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

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

158 

159 

160 
\section{Extra rules for the sequent calculus} 

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

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

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

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

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

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

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

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

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

174 
\qquad 

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

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

177 
\] 

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

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

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

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

104  183 

184 
Forgoing quantifier replication loses completeness, but gains decidability, 

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

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

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

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

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

190 
form: 

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

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

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

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

196 
\eqno(\forall E@3) 

197 
$$ 

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

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

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

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

207 
expensive to prove any but the simplest theorems. 

208 

209 

210 
\section{Classical rule sets} 

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

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

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

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

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

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

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

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

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

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

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

226 
above. 

104  227 

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

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

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

231 
exponentially many subgoals. Induction rules are unsafe because inductive 

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

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

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

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

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

237 

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

8136  243 
empty_cs : claset 
244 
print_cs : claset > unit 

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

246 
hazEs: thm list, hazIs: thm list, 

247 
swrappers: (string * wrapper) list, 

248 
uwrappers: (string * wrapper) list, 

249 
safe0_netpair: netpair, safep_netpair: netpair, 

250 
haz_netpair: netpair, dup_netpair: netpair\} 

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

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

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

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

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

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

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

104  258 
\end{ttbox} 
3089  259 
The add operations ignore any rule already present in the claset with the same 
260 
classification (such as Safe Introduction). They print a warning if the rule 

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

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  263 
claset, but see the warning below concerning destruction rules. 
308  264 
\begin{ttdescription} 
104  265 
\item[\ttindexbold{empty_cs}] is the empty classical set. 
266 

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

269 

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

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

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

1099  274 

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

104  277 

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

104  280 

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

104  283 

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

104  286 

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

104  289 

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

1869  292 

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

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

308  296 
\end{ttdescription} 
297 

3089  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  300 
it as follows: 
301 
\begin{ttbox} 

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

303 
\end{ttbox} 

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  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  308 
\end{warn} 
309 

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

312 
be applied using elimresolution. Elimination rules are applied using 

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

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

104  316 

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

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

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

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

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

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

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

326 
\end{ttbox} 

327 
\begin{warn} 

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

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

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

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

332 
\end{warn} 

333 

1099  334 

335 
\subsection{Modifying the search step} 

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

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

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

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:classicalsetup} below). 
3716  342 
They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$ 
343 
and~$P$, then replace $P\imp Q$ by~$Q$. 

104  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  346 
you to modify this basic proof strategy by applying two lists of arbitrary 
347 
{\bf wrapper tacticals} to it. 

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

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

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

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

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

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

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

359 
These names may be used to selectively delete wrappers. 

1099  360 

361 
\begin{ttbox} 

4649  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  365 
addSbefore : claset * (string * (int > tactic)) > claset \hfill{\bf infix 4} 
366 
addSaltern : claset * (string * (int > tactic)) > claset \hfill{\bf infix 4} 

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

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  370 
addbefore : claset * (string * (int > tactic)) > claset \hfill{\bf infix 4} 
371 
addaltern : claset * (string * (int > tactic)) > claset \hfill{\bf infix 4} 

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

373 

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  375 
addss : claset * simpset > claset \hfill{\bf infix 4} 
1099  376 
\end{ttbox} 
377 
% 

378 

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  385 
adds the given tactic as a safe wrapper, such that it is tried 
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  389 
adds the given tactic as a safe wrapper, such that it is tried 
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  399 
adds the given tactic as an unsafe wrapper, such that it its result is 
400 
concatenated {\em before} the result of each unsafe step. 

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  403 
adds the given tactic as an unsafe wrapper, such that it its result is 
404 
concatenated {\em after} the result of each unsafe step. 

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  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  419 
\index{simplification!from classical reasoner} 
420 
Strictly speaking, the operators \texttt{addss} and \texttt{addSss} 

421 
are not part of the classical reasoner. 

422 
, which are used as primitives 

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

424 
implemented as wrapper tacticals. 

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  432 

104  433 

434 
\section{The classical tactics} 

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

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

438 

104  439 

3224  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  442 
coded directly in \ML. It then reconstructs the proof using Isabelle 
443 
tactics. It is faster and more powerful than the other classical 

444 
reasoning tactics, but has major limitations too. 

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

447 
\ttindex{addss}. 

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

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

450 
\item It does not perform higherorder 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  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}. 
8136  454 
\item Function variables may only be applied to parameters of the subgoal. 
455 
(This restriction arises because the prover does not use higherorder 

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

457 
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

458 
\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

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

462 
% 

463 
\begin{ttbox} 

464 
blast_tac : claset > int > tactic 

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

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

467 
\end{ttbox} 

468 
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

469 
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

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

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

474 

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

476 
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

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

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

483 
has been closed, extended or split. 

484 
\end{ttdescription} 

485 

3224  486 

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

487 
\subsection{Automatic tactics}\label{sec:automatictactics} 
3224  488 
\begin{ttbox} 
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

489 
type clasimpset = claset * simpset; 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

490 
auto_tac : clasimpset > tactic 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

491 
force_tac : clasimpset > int > tactic 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

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

493 
force : int > unit 
3224  494 
\end{ttbox} 
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

495 
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

496 
simplification and classical reasoning. 
4885  497 
\begin{ttdescription} 
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

498 
\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

499 
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

500 
leaving the ones it cannot prove. 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

501 
(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

502 
\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

503 
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

504 
performing a rather exhaustive search. 
4885  505 
\end{ttdescription} 
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

506 
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

507 
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

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

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

3224  512 

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

513 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

533 
\item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but 
5577  534 
also does simplification with the given simpset. note that if the simpset 
535 
includes a splitter for the premises, the subgoal may still be split. 

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

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

537 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

538 

3224  539 
\subsection{Other classical tactics} 
332  540 
\begin{ttbox} 
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

541 
fast_tac : claset > int > tactic 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

542 
best_tac : claset > int > tactic 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

543 
slow_tac : claset > int > tactic 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

544 
slow_best_tac : claset > int > tactic 
332  545 
\end{ttbox} 
3224  546 
These tactics attempt to prove a subgoal using sequentstyle reasoning. 
547 
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

548 
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

549 
this subgoal or fail. The \texttt{slow_} versions conduct a broader 
3224  550 
search.% 
551 
\footnote{They may, when backtracking from a failed proof attempt, undo even 

552 
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

553 

a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

554 
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

555 
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

556 
that sets up the classical reasoner. 
332  557 
\begin{ttdescription} 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

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

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

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

563 

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

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

566 

8136  567 
\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with 
568 
bestfirst search to prove subgoal~$i$. 

875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

569 
\end{ttdescription} 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

570 

a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

571 

3716  572 
\subsection{Depthlimited automatic tactics} 
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

573 
\begin{ttbox} 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

574 
depth_tac : claset > int > int > tactic 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

575 
deepen_tac : claset > int > int > tactic 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

576 
\end{ttbox} 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

577 
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

578 
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

579 
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

580 
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

581 

a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

582 
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

583 
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

584 
\begin{ttdescription} 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

585 
\item[\ttindexbold{depth_tac} $cs$ $m$ $i$] 
3089  586 
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

587 

a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

588 
\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

589 
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

590 
repeatedly with increasing depths, starting with~$m$. 
332  591 
\end{ttdescription} 
592 

593 

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

596 
safe_step_tac : claset > int > tactic 

597 
safe_tac : claset > tactic 

598 
inst_step_tac : claset > int > tactic 

599 
step_tac : claset > int > tactic 

600 
slow_step_tac : claset > int > tactic 

601 
\end{ttbox} 

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

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

308  604 
\begin{ttdescription} 
104  605 
\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

606 
subgoal~$i$. The safe wrapper tacticals are applied to a tactic that may 
3716  607 
include proof by assumption or Modus Ponens (taking care not to instantiate 
608 
unknowns), or substitution. 

104  609 

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

3716  611 
subgoals. It is deterministic, with at most one outcome. 
104  612 

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

613 
\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac}, 
104  614 
but allows unknowns to be instantiated. 
615 

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

619 
from~$cs$. 

104  620 

621 
\item[\ttindexbold{slow_step_tac}] 

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

622 
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

623 
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

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

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

627 

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

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

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

631 
\index{claset!current}. This is a default set of classical 
4561  632 
rules. The underlying idea is quite similar to that of a current 
633 
simpset described in \S\ref{sec:simpfordummies}; please read that 

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

634 
section, including its warnings. 
4561  635 

636 
The tactics 

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

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

643 
Deepen_tac : int > int > tactic 

644 
Clarify_tac : int > tactic 

645 
Clarify_step_tac : int > tactic 

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

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

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

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

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

654 
\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

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

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

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

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

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

665 
\end{ttbox} 

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

667 
\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

668 
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

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

672 
\end{ttbox} 

3224  673 
deletes rules from the current claset. 
104  674 

7990  675 
\medskip A few further functions are available as uppercase versions only: 
676 
\begin{ttbox} 

677 
AddXIs, AddXEs, AddXDs: thm list > unit 

678 
\end{ttbox} 

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

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

681 
These provide additional hints for the basic nonautomated proof methods of 

682 
Isabelle/Isar \cite{isabelleisarref}. The corresponding Isar attributes are 

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

684 
not have any effect on classic Isabelle tactics. 

685 

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

686 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

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

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

689 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

704 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

705 

104  706 
\subsection{Other useful tactics} 
319  707 
\index{tactics!for contradiction} 
708 
\index{tactics!for Modus Ponens} 

104  709 
\begin{ttbox} 
710 
contr_tac : int > tactic 

711 
mp_tac : int > tactic 

712 
eq_mp_tac : int > tactic 

713 
swap_res_tac : thm list > int > tactic 

714 
\end{ttbox} 

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

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

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

720 
tactic can produce multiple outcomes, enumerating all possible 

721 
contradictions. 

104  722 

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

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

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

727 
nothing. 

728 

729 
\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

730 
is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns  thus, it 
104  731 
is safe. 
732 

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

734 
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

735 
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

736 
\texttt{contr_tac}. It then attempts to apply each rule in turn, attempting 
104  737 
resolution and also elimresolution with the swapped form. 
308  738 
\end{ttdescription} 
104  739 

740 
\subsection{Creating swapped rules} 

741 
\begin{ttbox} 

742 
swapify : thm list > thm list 

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

744 
\end{ttbox} 

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

748 

308  749 
\item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})] 
104  750 
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

751 
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

752 
(indicating ordinary resolution) or~\texttt{true} (indicating 
104  753 
elimresolution). 
308  754 
\end{ttdescription} 
104  755 

756 

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

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

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

763 
argument signature \texttt{CLASSICAL_DATA}: 

104  764 
\begin{ttbox} 
765 
signature CLASSICAL_DATA = 

766 
sig 

767 
val mp : thm 

768 
val not_elim : thm 

769 
val swap : thm 

770 
val sizef : thm > int 

771 
val hyp_subst_tacs : (int > tactic) list 

772 
end; 

773 
\end{ttbox} 

774 
Thus, the functor requires the following items: 

308  775 
\begin{ttdescription} 
319  776 
\item[\tdxbold{mp}] should be the Modus Ponens rule 
104  777 
$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$. 
778 

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

319  782 
\item[\tdxbold{swap}] should be the swap rule 
104  783 
$\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$. 
784 

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

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

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

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

6170  789 
those concerned with typechecking). A heuristic function might simply 
104  790 
count the subgoals. 
791 

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

795 
tactics are assumed to be safe! 

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

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

104  801 

319  802 
\index{classical reasoner)} 
5371  803 

5550  804 
\section{Setting up the combination with the simplifier} 
805 
\label{sec:clasimpsetup} 

5371  806 

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

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

810 
argment, which can be contructed on the fly: 

811 
\begin{ttbox} 

812 
structure Clasimp = ClasimpFun 

813 
(structure Simplifier = Simplifier 

814 
and Classical = Classical 

815 
and Blast = Blast); 

816 
\end{ttbox} 

817 
% 

5371  818 
%%% Local Variables: 
819 
%%% mode: latex 

820 
%%% TeXmaster: "ref" 

821 
%%% End: 