author  wenzelm 
Fri, 16 Jul 1999 22:24:42 +0200  
changeset 7024  44bd3c094fd6 
parent 6592  c120262044b6 
child 7990  0a604b2fc2b1 
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} 

1099  243 
empty_cs : claset 
244 
print_cs : claset > unit 

4665  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} 

1099  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} 

1869  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}. 
3089  454 
\item The message {\small\tt Function Var's argument not a bound variable\ } 
455 
relates to the lack of higherorder unification. Function variables 

456 
may only be applied to parameters of the subgoal. 

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

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

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

461 
% 

462 
\begin{ttbox} 

463 
blast_tac : claset > int > tactic 

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

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

466 
\end{ttbox} 

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

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

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

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

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

473 

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

475 
to prove subgoal~$i$ using a search bound of $lim$. Often a slow 

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

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

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

482 
has been closed, extended or split. 

483 
\end{ttdescription} 

484 

3224  485 

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

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

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

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

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

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

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

494 
The automatic tactics attempt to prove goals using a combination of 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

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

497 
\item[\ttindexbold{auto_tac $(cs,ss)$}] is intended for situations where 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

498 
there are a lot of mostly trivial subgoals; it proves all the easy ones, 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

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

500 
(Unfortunately, attempting to prove the hard ones may take a long time.) 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

501 
\item[\ttindexbold{force_tac} $(cs,ss)$ $i$] is intended to prove subgoal~$i$ 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

502 
completely. It tries to apply all fancy tactics it knows about, 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

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

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

506 
they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which 
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

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

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

3224  511 

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

512 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

536 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

537 

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

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

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

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

543 
slow_best_tac : claset > int > tactic 
332  544 
\end{ttbox} 
3224  545 
These tactics attempt to prove a subgoal using sequentstyle reasoning. 
546 
Unlike \texttt{blast_tac}, they construct proofs directly in Isabelle. Their 

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

547 
effect is restricted (by \texttt{SELECT_GOAL}) to one subgoal; they either prove 
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

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

551 
the step of proving a subgoal by assumption.} 

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

552 

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

553 
The bestfirst tactics are guided by a heuristic function: typically, the 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

554 
total size of the proof state. This function is supplied in the functor call 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

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

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

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

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

562 

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

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

565 

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

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

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

569 

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

570 

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

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

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

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

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

576 
These work by exhaustive search up to a specified depth. Unsafe rules are 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

577 
modified to preserve the formula they act on, so that it be used repeatedly. 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

578 
They can prove more goals than \texttt{fast_tac} can but are much 
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

579 
slower, for example if the assumptions have many universal quantifiers. 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

580 

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

581 
The depth limits the number of unsafe steps. If you can estimate the minimum 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

582 
number of unsafe steps needed, supply this value as~$m$ to save time. 
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

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

584 
\item[\ttindexbold{depth_tac} $cs$ $m$ $i$] 
3089  585 
tries to prove subgoal~$i$ by exhaustive search up to depth~$m$. 
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

586 

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

587 
\item[\ttindexbold{deepen_tac} $cs$ $m$ $i$] 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

588 
tries to prove subgoal~$i$ by iterative deepening. It calls \texttt{depth_tac} 
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset

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

592 

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

595 
safe_step_tac : claset > int > tactic 

596 
safe_tac : claset > tactic 

597 
inst_step_tac : claset > int > tactic 

598 
step_tac : claset > int > tactic 

599 
slow_step_tac : claset > int > tactic 

600 
\end{ttbox} 

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

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

308  603 
\begin{ttdescription} 
104  604 
\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on 
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

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

104  608 

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

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

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

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

1099  615 
\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof 
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset

616 
procedure. The (unsafe) wrapper tacticals are applied to a tactic that tries 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

617 
\texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule from~$cs$. 
104  618 

619 
\item[\ttindexbold{slow_step_tac}] 

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

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

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

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

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

625 

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

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

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

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

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

632 
section, including its warnings. 
4561  633 

634 
The tactics 

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

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

641 
Deepen_tac : int > int > tactic 

642 
Clarify_tac : int > tactic 

643 
Clarify_step_tac : int > tactic 

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

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

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

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

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

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

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

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

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

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

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

663 
\end{ttbox} 

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

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

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

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

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

670 
\end{ttbox} 

3224  671 
deletes rules from the current claset. 
104  672 

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

673 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

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

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

676 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

691 

dc6ee60d2be8
exchanged automatictactics and semiautomatictactics
oheimb
parents:
5550
diff
changeset

692 

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

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

698 
mp_tac : int > tactic 

699 
eq_mp_tac : int > tactic 

700 
swap_res_tac : thm list > int > tactic 

701 
\end{ttbox} 

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

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

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

707 
tactic can produce multiple outcomes, enumerating all possible 

708 
contradictions. 

104  709 

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

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

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

714 
nothing. 

715 

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

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

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

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

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

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

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

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

727 
\subsection{Creating swapped rules} 

728 
\begin{ttbox} 

729 
swapify : thm list > thm list 

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

731 
\end{ttbox} 

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

735 

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

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

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

743 

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

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

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

750 
argument signature \texttt{CLASSICAL_DATA}: 

104  751 
\begin{ttbox} 
752 
signature CLASSICAL_DATA = 

753 
sig 

754 
val mp : thm 

755 
val not_elim : thm 

756 
val swap : thm 

757 
val sizef : thm > int 

758 
val hyp_subst_tacs : (int > tactic) list 

759 
end; 

760 
\end{ttbox} 

761 
Thus, the functor requires the following items: 

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

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

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

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

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

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

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

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

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

782 
tactics are assumed to be safe! 

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

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

104  788 

319  789 
\index{classical reasoner)} 
5371  790 

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

5371  793 

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

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

797 
argment, which can be contructed on the fly: 

798 
\begin{ttbox} 

799 
structure Clasimp = ClasimpFun 

800 
(structure Simplifier = Simplifier 

801 
and Classical = Classical 

802 
and Blast = Blast); 

803 
\end{ttbox} 

804 
% 

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

807 
%%% TeXmaster: "ref" 

808 
%%% End: 