author  paulson 
Wed, 23 Feb 2000 10:41:37 +0100  
changeset 8284  95c022a866ca 
parent 8136  8c65f3ca13f2 
child 8702  78b7010db847 
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 

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

3089  475 

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

8284  477 
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

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

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

484 
has been closed, extended or split. 

485 
\end{ttdescription} 

486 

3224  487 

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

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

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

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

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

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

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

496 
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

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

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

500 
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

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

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

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

504 
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

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

507 
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

508 
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

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

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

3224  513 

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

514 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

538 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

539 

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

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

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

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

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

549 
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

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

553 
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

554 

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

555 
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

556 
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

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

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

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

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

564 

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

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

567 

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

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

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

571 

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

572 

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

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

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

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

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

578 
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

579 
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

580 
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

581 
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

582 

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

583 
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

584 
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

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

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

588 

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

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

590 
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

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

594 

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

597 
safe_step_tac : claset > int > tactic 

598 
safe_tac : claset > tactic 

599 
inst_step_tac : claset > int > tactic 

600 
step_tac : claset > int > tactic 

601 
slow_step_tac : claset > int > tactic 

602 
\end{ttbox} 

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

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

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

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

104  610 

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

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

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

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

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

620 
from~$cs$. 

104  621 

622 
\item[\ttindexbold{slow_step_tac}] 

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

623 
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

624 
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

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

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

628 

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

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

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

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

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

635 
section, including its warnings. 
4561  636 

637 
The tactics 

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

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

644 
Deepen_tac : int > int > tactic 

645 
Clarify_tac : int > tactic 

646 
Clarify_step_tac : int > tactic 

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

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

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

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

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

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

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

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

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

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

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

666 
\end{ttbox} 

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

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

669 
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

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

673 
\end{ttbox} 

3224  674 
deletes rules from the current claset. 
104  675 

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

678 
AddXIs, AddXEs, AddXDs: thm list > unit 

679 
\end{ttbox} 

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

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

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

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

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

685 
not have any effect on classic Isabelle tactics. 

686 

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

687 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

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

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

690 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

705 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

706 

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

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

712 
mp_tac : int > tactic 

713 
eq_mp_tac : int > tactic 

714 
swap_res_tac : thm list > int > tactic 

715 
\end{ttbox} 

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

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

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

721 
tactic can produce multiple outcomes, enumerating all possible 

722 
contradictions. 

104  723 

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

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

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

728 
nothing. 

729 

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

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

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

735 
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

736 
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

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

741 
\subsection{Creating swapped rules} 

742 
\begin{ttbox} 

743 
swapify : thm list > thm list 

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

745 
\end{ttbox} 

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

749 

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

752 
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

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

757 

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

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

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

764 
argument signature \texttt{CLASSICAL_DATA}: 

104  765 
\begin{ttbox} 
766 
signature CLASSICAL_DATA = 

767 
sig 

768 
val mp : thm 

769 
val not_elim : thm 

770 
val swap : thm 

771 
val sizef : thm > int 

772 
val hyp_subst_tacs : (int > tactic) list 

773 
end; 

774 
\end{ttbox} 

775 
Thus, the functor requires the following items: 

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

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

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

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

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

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

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

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

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

796 
tactics are assumed to be safe! 

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

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

104  802 

319  803 
\index{classical reasoner)} 
5371  804 

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

5371  807 

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

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

811 
argment, which can be contructed on the fly: 

812 
\begin{ttbox} 

813 
structure Clasimp = ClasimpFun 

814 
(structure Simplifier = Simplifier 

815 
and Classical = Classical 

816 
and Blast = Blast); 

817 
\end{ttbox} 

818 
% 

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

821 
%%% TeXmaster: "ref" 

822 
%%% End: 