author  oheimb 
Wed, 12 Nov 1997 18:58:50 +0100  
changeset 4223  f60e3d2c81d3 
parent 3720  a5b9e0ade194 
child 4317  7264fa2ff2ec 
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 
7 
extension of classical firstorder logic. Isabelle's set theory~{\tt 

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

8 
ZF} is built upon theory~\texttt{FOL}, while higherorder logic 
3108  9 
conceptually contains firstorder logic as a fragment. 
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 
37 
set theory. To attempt to prove \emph{all} subgoals using a combination of 

38 
rewriting and classical reasoning, try 

3224  39 
\begin{ttbox} 
40 
by (Auto_tac()); 

41 
\end{ttbox} 

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

43 
subgoal, type one of the following: 
3716  44 
\begin{ttbox} 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

45 
by (Clarify_tac \(i\)); \emph{\textrm{applies to one subgoal}} 
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

46 
by Safe_tac; \emph{\textrm{applies to all subgoals}} 
3716  47 
\end{ttbox} 
48 
You need to know how the classical reasoner works in order to use it 

49 
effectively. There are many tactics to choose from, including {\tt 

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

50 
Fast_tac} and \texttt{Best_tac}. 
2479  51 

3108  52 
We shall first discuss the underlying principles, then present the 
53 
classical reasoner. Finally, we shall see how to instantiate it for 

54 
new logics. The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already 

55 
installed. 

104  56 

57 

58 
\section{The sequent calculus} 

59 
\index{sequent calculus} 

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

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

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

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

64 
generalization of natural deduction, is easier to automate. 

65 

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

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

69 
lists or multisets of formulae.} The sequent 

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

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

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

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

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

76 

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

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

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

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

82 
firstorder logic, 

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

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

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

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

88 
\eqno({\imp}R) 

89 
$$ 

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

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

93 
single rule 

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

96 
\eqno({\disj}R) 

97 
$$ 

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

100 

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

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

103 
reduce this formula to a basic sequent: 

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

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

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

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

108 
\] 

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

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

111 
surprisingly effective proof procedure. Quantifiers add few complications, 

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

113 
of {\em ML for the Working Programmer}~\cite{paulson91} for further 

114 
discussion. 

115 

116 

117 
\section{Simulating sequents by natural deduction} 

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

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

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

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

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

124 
Elimresolution plays a key role in simulating sequent proofs. 

125 

126 
We can easily handle reasoning on the left. 

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

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

131 
other connectives, we use sequentstyle elimination rules instead of 

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

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

136 
$$ 

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

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

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

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

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

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

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

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

151 
Swapped introduction rules are applied using elimresolution, which deletes 

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

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

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

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

156 

157 

158 
\section{Extra rules for the sequent calculus} 

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

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

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

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

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

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

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

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

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

172 
\qquad 

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

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

175 
\] 

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

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

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

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

104  181 

182 
Forgoing quantifier replication loses completeness, but gains decidability, 

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

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

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

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

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

188 
form: 

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

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

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

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

194 
\eqno(\forall E@3) 

195 
$$ 

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

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

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

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

205 
expensive to prove any but the simplest theorems. 

206 

207 

208 
\section{Classical rule sets} 

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

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

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

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

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

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

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

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

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

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

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

224 
above. 

104  225 

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

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

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

229 
exponentially many subgoals. Induction rules are unsafe because inductive 

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

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

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

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

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

235 

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

1099  241 
empty_cs : claset 
242 
print_cs : claset > unit 

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

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

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

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

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

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

1869  249 
delrules : claset * thm list > claset \hfill{\bf infix 4} 
104  250 
\end{ttbox} 
3089  251 
The add operations ignore any rule already present in the claset with the same 
252 
classification (such as Safe Introduction). They print a warning if the rule 

253 
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

254 
anyway. Calling \texttt{delrules} deletes all occurrences of a rule from the 
3089  255 
claset, but see the warning below concerning destruction rules. 
308  256 
\begin{ttdescription} 
104  257 
\item[\ttindexbold{empty_cs}] is the empty classical set. 
258 

1099  259 
\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$. 
260 

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

104  263 

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

104  266 

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

104  269 

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

104  272 

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

104  275 

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

1869  278 

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

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

308  282 
\end{ttdescription} 
283 

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

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

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

289 
\end{ttbox} 

290 
\par\noindent 

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

291 
This is necessary because the operators \texttt{addSDs} and \texttt{addDs} convert 
3089  292 
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

293 
and then insert them using \texttt{addSEs} and \texttt{addEs}, respectively. 
3089  294 
\end{warn} 
295 

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

298 
be applied using elimresolution. Elimination rules are applied using 

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

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

104  302 

1099  303 

304 
\subsection{Modifying the search step} 

3716  305 
For a given classical set, the proof strategy is simple. Perform as many safe 
306 
inferences as possible; or else, apply certain safe rules, allowing 

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

308 
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

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

104  312 

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

313 
The classical reasoning tactics  except \texttt{blast_tac}!  allow 
3108  314 
you to modify this basic proof strategy by applying two arbitrary {\bf 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3224
diff
changeset

315 
wrapper tacticals} to it. This affects each step of the search. 
3108  316 
Usually they are the identity tacticals, but they could apply another 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3224
diff
changeset

317 
tactic before or after the step tactic. The first one, which is 
3108  318 
considered to be safe, affects \ttindex{safe_step_tac} and all the 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3224
diff
changeset

319 
tactics that call it. The the second one, which may be unsafe, affects 
3108  320 
\ttindex{step_tac}, \ttindex{slow_step_tac} and the tactics that call 
321 
them. 

1099  322 

323 
\begin{ttbox} 

2632  324 
addss : claset * simpset > claset \hfill{\bf infix 4} 
325 
addSbefore : claset * (int > tactic) > claset \hfill{\bf infix 4} 

326 
addSaltern : claset * (int > tactic) > claset \hfill{\bf infix 4} 

327 
setSWrapper : claset * ((int > tactic) > 

328 
(int > tactic)) > claset \hfill{\bf infix 4} 

329 
compSWrapper : claset * ((int > tactic) > 

330 
(int > tactic)) > claset \hfill{\bf infix 4} 

331 
addbefore : claset * (int > tactic) > claset \hfill{\bf infix 4} 

332 
addaltern : claset * (int > tactic) > claset \hfill{\bf infix 4} 

333 
setWrapper : claset * ((int > tactic) > 

334 
(int > tactic)) > claset \hfill{\bf infix 4} 

335 
compWrapper : claset * ((int > tactic) > 

336 
(int > tactic)) > claset \hfill{\bf infix 4} 

1099  337 
\end{ttbox} 
338 
% 

3108  339 
\index{simplification!from classical reasoner} The wrapper tacticals 
340 
underly the operator addss, which combines each search step by 

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

341 
simplification. Strictly speaking, \texttt{addss} is not part of the 
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

342 
classical reasoner. It should be defined (using \texttt{addSaltern 
3108  343 
(CHANGED o (safe_asm_more_full_simp_tac ss)}) when the simplifier is 
344 
installed. 

1099  345 

346 
\begin{ttdescription} 

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

348 
adds the simpset~$ss$ to the classical set. The assumptions and goal will be 
2631
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

349 
simplified, in a safe way, after the safe steps of the search. 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

350 

5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

351 
\item[$cs$ addSbefore $tac$] \indexbold{*addSbefore} 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

352 
changes the safe wrapper tactical to apply the given tactic {\em before} 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

353 
each safe step of the search. 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

354 

5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

355 
\item[$cs$ addSaltern $tac$] \indexbold{*addSaltern} 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

356 
changes the safe wrapper tactical to apply the given tactic when a safe step 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

357 
of the search would fail. 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

358 

5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

359 
\item[$cs$ setSWrapper $tactical$] \indexbold{*setSWrapper} 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

360 
specifies a new safe wrapper tactical. 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

361 

5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

362 
\item[$cs$ compSWrapper $tactical$] \indexbold{*compSWrapper} 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

363 
composes the $tactical$ with the existing safe wrapper tactical, 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

364 
to combine their effects. 
1099  365 

366 
\item[$cs$ addbefore $tac$] \indexbold{*addbefore} 

2631
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

367 
changes the (unsafe) wrapper tactical to apply the given tactic, which should 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

368 
be safe, {\em before} each step of the search. 
1099  369 

2631
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

370 
\item[$cs$ addaltern $tac$] \indexbold{*addaltern} 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

371 
changes the (unsafe) wrapper tactical to apply the given tactic 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

372 
{\em alternatively} after each step of the search. 
1099  373 

2631
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

374 
\item[$cs$ setWrapper $tactical$] \indexbold{*setWrapper} 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

375 
specifies a new (unsafe) wrapper tactical. 
1099  376 

2631
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

377 
\item[$cs$ compWrapper $tactical$] \indexbold{*compWrapper} 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

378 
composes the $tactical$ with the existing (unsafe) wrapper tactical, 
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

379 
to combine their effects. 
1099  380 
\end{ttdescription} 
381 

104  382 

383 
\section{The classical tactics} 

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

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

387 

388 
\subsection{Semiautomatic tactics} 

389 
\begin{ttbox} 

390 
clarify_tac : claset > int > tactic 

391 
clarify_step_tac : claset > int > tactic 

392 
\end{ttbox} 

393 
Use these when the automatic tactics fail. They perform all the obvious 

394 
logical inferences that do not split the subgoal. The result is a 

395 
simpler subgoal that can be tackled by other means, such as by 

396 
instantiating quantifiers yourself. 

397 
\begin{ttdescription} 

398 
\item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on 

399 
subgoal~$i$, using \texttt{clarify_step_tac}. 

400 

401 
\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on 

402 
subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj 

403 
B$ is left as a conjunction. Proof by assumption, Modus Ponens, etc., may be 

404 
performed provided they do not instantiate unknowns. Assumptions of the 

405 
form $x=t$ may be eliminated. The usersupplied safe wrapper tactical is 

406 
applied. 

407 
\end{ttdescription} 

408 

104  409 

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

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

414 
reasoning tactics, but has major limitations too. 

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

417 
\ttindex{addss}. 

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

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

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

421 
rangeI} in {\HOL} and \texttt{RepFunI} in {\ZF}. There are often 
3089  422 
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

423 
range_eqI} and \texttt{RepFun_eqI}. 
3089  424 
\item The message {\small\tt Function Var's argument not a bound variable\ } 
425 
relates to the lack of higherorder unification. Function variables 

426 
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

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

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

431 
% 

432 
\begin{ttbox} 

433 
blast_tac : claset > int > tactic 

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

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

436 
\end{ttbox} 

437 
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

438 
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

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

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

443 

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

445 
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

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

449 
\item[\ttindexbold{Blast.trace} := true;] \index{tracing!of classical prover} 

450 
causes the tableau prover to print a trace of its search. At each step it 

451 
displays the formula currently being examined and reports whether the branch 

452 
has been closed, extended or split. 

453 
\end{ttdescription} 

454 

3224  455 

456 
\subsection{An automatic tactic} 

457 
\begin{ttbox} 

458 
auto_tac : claset * simpset > tactic 

459 
auto : unit > unit 

460 
\end{ttbox} 

461 
The autotactic attempts to prove all subgoals using a combination of 

462 
simplification and classical reasoning. It is intended for situations where 

463 
there are a lot of mostly trivial subgoals; it proves all the easy ones, 

464 
leaving the ones it cannot prove. (Unfortunately, attempting to prove the 

465 
hard ones may take a long time.) It must be supplied both a simpset and a 

466 
claset; therefore it is most easily called as \texttt{Auto_tac}, which uses 

467 
the default claset and simpset (see \S\ref{sec:currentclaset} below). For 

468 
interactive use, the shorthand \texttt{auto();} abbreviates 

469 
\begin{ttbox} 

470 
by (Auto_tac()); 

471 
\end{ttbox} 

472 

473 
\subsection{Other classical tactics} 

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

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

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

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

478 
slow_best_tac : claset > int > tactic 
332  479 
\end{ttbox} 
3224  480 
These tactics attempt to prove a subgoal using sequentstyle reasoning. 
481 
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

482 
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

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

486 
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

487 

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

488 
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

489 
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

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

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

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

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

497 

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

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

500 

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

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

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

504 

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

505 

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

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

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

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

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

511 
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

512 
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

513 
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

514 
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

515 

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

516 
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

517 
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

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

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

521 

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

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

523 
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

524 
repeatedly with increasing depths, starting with~$m$. 
332  525 
\end{ttdescription} 
526 

527 

104  528 
\subsection{Singlestep tactics} 
529 
\begin{ttbox} 

530 
safe_step_tac : claset > int > tactic 

531 
safe_tac : claset > tactic 

532 
inst_step_tac : claset > int > tactic 

533 
step_tac : claset > int > tactic 

534 
slow_step_tac : claset > int > tactic 

535 
\end{ttbox} 

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

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

308  538 
\begin{ttdescription} 
104  539 
\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on 
3716  540 
subgoal~$i$. The safe wrapper tactical is applied to a tactic that may 
541 
include proof by assumption or Modus Ponens (taking care not to instantiate 

542 
unknowns), or substitution. 

104  543 

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

3716  545 
subgoals. It is deterministic, with at most one outcome. 
104  546 

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

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

1099  550 
\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof 
2631
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset

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

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

554 
\item[\ttindexbold{slow_step_tac}] 

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

555 
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

556 
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

557 
The resulting search space is larger. 
308  558 
\end{ttdescription} 
104  559 

3224  560 
\subsection{The current claset}\label{sec:currentclaset} 
2479  561 
Some logics (\FOL, {\HOL} and \ZF) support the concept of a current 
562 
claset\index{claset!current}. This is a default set of classical rules. The 

563 
underlying idea is quite similar to that of a current simpset described in 

564 
\S\ref{sec:simpfordummies}; please read that section, including its 

565 
warnings. Just like simpsets, clasets can be associated with theories. The 

566 
tactics 

1869  567 
\begin{ttbox} 
3716  568 
Blast_tac : int > tactic 
569 
Auto_tac : unit > tactic 

570 
Fast_tac : int > tactic 

571 
Best_tac : int > tactic 

572 
Deepen_tac : int > int > tactic 

573 
Clarify_tac : int > tactic 

574 
Clarify_step_tac : int > tactic 

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

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

576 
Safe_step_tac : int > tactic 
3716  577 
Step_tac : int > tactic 
1869  578 
\end{ttbox} 
3224  579 
\indexbold{*Blast_tac}\indexbold{*Auto_tac} 
580 
\indexbold{*Best_tac}\indexbold{*Fast_tac}% 

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

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

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

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

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

585 
make use of the current claset. For example, \texttt{Blast_tac} is defined as 
1869  586 
\begin{ttbox} 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

587 
fun Blast_tac i st = blast_tac (!claset) i st; 
1869  588 
\end{ttbox} 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

589 
and gets the current claset, \ttindex{!claset}, only after it is applied to a 
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

590 
proof state. The functions 
1869  591 
\begin{ttbox} 
592 
AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list > unit 

593 
\end{ttbox} 

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

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

596 
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

597 
lower case counterparts, such as \texttt{addSIs}. Calling 
1869  598 
\begin{ttbox} 
599 
Delrules : thm list > unit 

600 
\end{ttbox} 

3224  601 
deletes rules from the current claset. 
104  602 

603 
\subsection{Other useful tactics} 

319  604 
\index{tactics!for contradiction} 
605 
\index{tactics!for Modus Ponens} 

104  606 
\begin{ttbox} 
607 
contr_tac : int > tactic 

608 
mp_tac : int > tactic 

609 
eq_mp_tac : int > tactic 

610 
swap_res_tac : thm list > int > tactic 

611 
\end{ttbox} 

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

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

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

617 
tactic can produce multiple outcomes, enumerating all possible 

618 
contradictions. 

104  619 

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

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

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

624 
nothing. 

625 

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

627 
is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns  thus, it 
104  628 
is safe. 
629 

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

631 
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

632 
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

633 
\texttt{contr_tac}. It then attempts to apply each rule in turn, attempting 
104  634 
resolution and also elimresolution with the swapped form. 
308  635 
\end{ttdescription} 
104  636 

637 
\subsection{Creating swapped rules} 

638 
\begin{ttbox} 

639 
swapify : thm list > thm list 

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

641 
\end{ttbox} 

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

645 

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

648 
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

649 
(indicating ordinary resolution) or~\texttt{true} (indicating 
104  650 
elimresolution). 
308  651 
\end{ttdescription} 
104  652 

653 

3716  654 
\section{Setting up the classical reasoner}\label{sec:classicalsetup} 
319  655 
\index{classical reasoner!setting up} 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

656 
Isabelle's classical objectlogics, including \texttt{FOL} and \texttt{HOL}, have 
286  657 
the classical reasoner already set up. When defining a new classical logic, 
658 
you should set up the reasoner yourself. It consists of the \ML{} functor 

104  659 
\ttindex{ClassicalFun}, which takes the argument 
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt > \texttt
paulson
parents:
3716
diff
changeset

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

661 
CLASSICAL_DATA}: 
104  662 
\begin{ttbox} 
663 
signature CLASSICAL_DATA = 

664 
sig 

665 
val mp : thm 

666 
val not_elim : thm 

667 
val swap : thm 

668 
val sizef : thm > int 

669 
val hyp_subst_tacs : (int > tactic) list 

670 
end; 

671 
\end{ttbox} 

672 
Thus, the functor requires the following items: 

308  673 
\begin{ttdescription} 
319  674 
\item[\tdxbold{mp}] should be the Modus Ponens rule 
104  675 
$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$. 
676 

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

319  680 
\item[\tdxbold{swap}] should be the swap rule 
104  681 
$\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$. 
682 

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

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

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

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

687 
those concerned with type checking). A heuristic function might simply 

688 
count the subgoals. 

689 

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

693 
tactics are assumed to be safe! 

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

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

104  699 

319  700 
\index{classical reasoner)} 