author  nipkow 
Wed, 04 Aug 2004 11:25:08 +0200  
changeset 15106  e8cef6993701 
parent 13104  df7aac8543c9 
child 30184  37969710e61f 
permissions  rwrr 
104  1 
%% $Id$ 
2 
\chapter{Tacticals} 

3 
\index{tacticals(} 

4 
Tacticals are operations on tactics. Their implementation makes use of 

5 
functional programming techniques, especially for sequences. Most of the 

6 
time, you may forget about this and regard tacticals as highlevel control 

7 
structures. 

8 

9 
\section{The basic tacticals} 

10 
\subsection{Joining two tactics} 

323  11 
\index{tacticals!joining two tactics} 
104  12 
The tacticals {\tt THEN} and {\tt ORELSE}, which provide sequencing and 
13 
alternation, underlie most of the other control structures in Isabelle. 

14 
{\tt APPEND} and {\tt INTLEAVE} provide more sophisticated forms of 

15 
alternation. 

16 
\begin{ttbox} 

17 
THEN : tactic * tactic > tactic \hfill{\bf infix 1} 

18 
ORELSE : tactic * tactic > tactic \hfill{\bf infix} 

19 
APPEND : tactic * tactic > tactic \hfill{\bf infix} 

20 
INTLEAVE : tactic * tactic > tactic \hfill{\bf infix} 

21 
\end{ttbox} 

323  22 
\begin{ttdescription} 
23 
\item[$tac@1$ \ttindexbold{THEN} $tac@2$] 

104  24 
is the sequential composition of the two tactics. Applied to a proof 
25 
state, it returns all states reachable in two steps by applying $tac@1$ 

26 
followed by~$tac@2$. First, it applies $tac@1$ to the proof state, getting a 

27 
sequence of next states; then, it applies $tac@2$ to each of these and 

28 
concatenates the results. 

29 

323  30 
\item[$tac@1$ \ttindexbold{ORELSE} $tac@2$] 
104  31 
makes a choice between the two tactics. Applied to a state, it 
32 
tries~$tac@1$ and returns the result if nonempty; if $tac@1$ fails then it 

33 
uses~$tac@2$. This is a deterministic choice: if $tac@1$ succeeds then 

34 
$tac@2$ is excluded. 

35 

323  36 
\item[$tac@1$ \ttindexbold{APPEND} $tac@2$] 
104  37 
concatenates the results of $tac@1$ and~$tac@2$. By not making a commitment 
323  38 
to either tactic, {\tt APPEND} helps avoid incompleteness during 
39 
search.\index{search} 

104  40 

323  41 
\item[$tac@1$ \ttindexbold{INTLEAVE} $tac@2$] 
104  42 
interleaves the results of $tac@1$ and~$tac@2$. Thus, it includes all 
43 
possible next states, even if one of the tactics returns an infinite 

44 
sequence. 

323  45 
\end{ttdescription} 
104  46 

47 

48 
\subsection{Joining a list of tactics} 

323  49 
\index{tacticals!joining a list of tactics} 
104  50 
\begin{ttbox} 
51 
EVERY : tactic list > tactic 

52 
FIRST : tactic list > tactic 

53 
\end{ttbox} 

54 
{\tt EVERY} and {\tt FIRST} are block structured versions of {\tt THEN} and 

55 
{\tt ORELSE}\@. 

323  56 
\begin{ttdescription} 
104  57 
\item[\ttindexbold{EVERY} {$[tac@1,\ldots,tac@n]$}] 
58 
abbreviates \hbox{\tt$tac@1$ THEN \ldots{} THEN $tac@n$}. It is useful for 

59 
writing a series of tactics to be executed in sequence. 

60 

61 
\item[\ttindexbold{FIRST} {$[tac@1,\ldots,tac@n]$}] 

62 
abbreviates \hbox{\tt$tac@1$ ORELSE \ldots{} ORELSE $tac@n$}. It is useful for 

63 
writing a series of tactics to be attempted one after another. 

323  64 
\end{ttdescription} 
104  65 

66 

67 
\subsection{Repetition tacticals} 

323  68 
\index{tacticals!repetition} 
104  69 
\begin{ttbox} 
8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

70 
TRY : tactic > tactic 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

71 
REPEAT_DETERM : tactic > tactic 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

72 
REPEAT_DETERM_N : int > tactic > tactic 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

73 
REPEAT : tactic > tactic 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

74 
REPEAT1 : tactic > tactic 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

75 
DETERM_UNTIL : (thm > bool) > tactic > tactic 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

76 
trace_REPEAT : bool ref \hfill{\bf initially false} 
104  77 
\end{ttbox} 
323  78 
\begin{ttdescription} 
104  79 
\item[\ttindexbold{TRY} {\it tac}] 
80 
applies {\it tac\/} to the proof state and returns the resulting sequence, 

81 
if nonempty; otherwise it returns the original state. Thus, it applies 

82 
{\it tac\/} at most once. 

83 

84 
\item[\ttindexbold{REPEAT_DETERM} {\it tac}] 

85 
applies {\it tac\/} to the proof state and, recursively, to the head of the 

86 
resulting sequence. It returns the first state to make {\it tac\/} fail. 

87 
It is deterministic, discarding alternative outcomes. 

88 

8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

89 
\item[\ttindexbold{REPEAT_DETERM_N} {\it n} {\it tac}] 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

90 
is like \hbox{\tt REPEAT_DETERM {\it tac}} but the number of repititions 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

91 
is bound by {\it n} (unless negative). 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

92 

104  93 
\item[\ttindexbold{REPEAT} {\it tac}] 
94 
applies {\it tac\/} to the proof state and, recursively, to each element of 

95 
the resulting sequence. The resulting sequence consists of those states 

96 
that make {\it tac\/} fail. Thus, it applies {\it tac\/} as many times as 

97 
possible (including zero times), and allows backtracking over each 

98 
invocation of {\it tac}. It is more general than {\tt REPEAT_DETERM}, but 

99 
requires more space. 

100 

101 
\item[\ttindexbold{REPEAT1} {\it tac}] 

102 
is like \hbox{\tt REPEAT {\it tac}} but it always applies {\it tac\/} at 

103 
least once, failing if this is impossible. 

104 

8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

105 
\item[\ttindexbold{DETERM_UNTIL} {\it p} {\it tac}] 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

106 
applies {\it tac\/} to the proof state and, recursively, to the head of the 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

107 
resulting sequence, until the predicate {\it p} (applied on the proof state) 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

108 
yields {\it true}. It fails if {\it tac\/} fails on any of the intermediate 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

109 
states. It is deterministic, discarding alternative outcomes. 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

110 

4317  111 
\item[set \ttindexbold{trace_REPEAT};] 
286  112 
enables an interactive tracing mode for the tacticals {\tt REPEAT_DETERM} 
113 
and {\tt REPEAT}. To view the tracing options, type {\tt h} at the prompt. 

323  114 
\end{ttdescription} 
104  115 

116 

117 
\subsection{Identities for tacticals} 

323  118 
\index{tacticals!identities for} 
104  119 
\begin{ttbox} 
120 
all_tac : tactic 

121 
no_tac : tactic 

122 
\end{ttbox} 

323  123 
\begin{ttdescription} 
104  124 
\item[\ttindexbold{all_tac}] 
125 
maps any proof state to the oneelement sequence containing that state. 

126 
Thus, it succeeds for all states. It is the identity element of the 

127 
tactical \ttindex{THEN}\@. 

128 

129 
\item[\ttindexbold{no_tac}] 

130 
maps any proof state to the empty sequence. Thus it succeeds for no state. 

131 
It is the identity element of \ttindex{ORELSE}, \ttindex{APPEND}, and 

132 
\ttindex{INTLEAVE}\@. Also, it is a zero element for \ttindex{THEN}, which means that 

133 
\hbox{\tt$tac$ THEN no_tac} is equivalent to {\tt no_tac}. 

323  134 
\end{ttdescription} 
104  135 
These primitive tactics are useful when writing tacticals. For example, 
136 
\ttindexbold{TRY} and \ttindexbold{REPEAT} (ignoring tracing) can be coded 

137 
as follows: 

138 
\begin{ttbox} 

139 
fun TRY tac = tac ORELSE all_tac; 

140 

3108  141 
fun REPEAT tac = 
142 
(fn state => ((tac THEN REPEAT tac) ORELSE all_tac) state); 

104  143 
\end{ttbox} 
144 
If $tac$ can return multiple outcomes then so can \hbox{\tt REPEAT $tac$}. 

145 
Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND} or {\tt 

146 
INTLEAVE}, it applies $tac$ as many times as possible in each 

147 
outcome. 

148 

149 
\begin{warn} 

150 
Note {\tt REPEAT}'s explicit abstraction over the proof state. Recursive 

151 
tacticals must be coded in this awkward fashion to avoid infinite 

152 
recursion. With the following definition, \hbox{\tt REPEAT $tac$} would 

332  153 
loop due to \ML's eager evaluation strategy: 
104  154 
\begin{ttbox} 
155 
fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac; 

156 
\end{ttbox} 

157 
\par\noindent 

158 
The builtin {\tt REPEAT} avoids~{\tt THEN}, handling sequences explicitly 

159 
and using tail recursion. This sacrifices clarity, but saves much space by 

160 
discarding intermediate proof states. 

161 
\end{warn} 

162 

163 

164 
\section{Control and search tacticals} 

323  165 
\index{search!tacticals(} 
166 

104  167 
A predicate on theorems, namely a function of type \hbox{\tt thm>bool}, 
168 
can test whether a proof state enjoys some desirable property  such as 

169 
having no subgoals. Tactics that search for satisfactory states are easy 

170 
to express. The main search procedures, depthfirst, breadthfirst and 

171 
bestfirst, are provided as tacticals. They generate the search tree by 

172 
repeatedly applying a given tactic. 

173 

174 

175 
\subsection{Filtering a tactic's results} 

323  176 
\index{tacticals!for filtering} 
177 
\index{tactics!filtering results of} 

104  178 
\begin{ttbox} 
179 
FILTER : (thm > bool) > tactic > tactic 

180 
CHANGED : tactic > tactic 

181 
\end{ttbox} 

323  182 
\begin{ttdescription} 
1118  183 
\item[\ttindexbold{FILTER} {\it p} $tac$] 
104  184 
applies $tac$ to the proof state and returns a sequence consisting of those 
185 
result states that satisfy~$p$. 

186 

187 
\item[\ttindexbold{CHANGED} {\it tac}] 

188 
applies {\it tac\/} to the proof state and returns precisely those states 

189 
that differ from the original state. Thus, \hbox{\tt CHANGED {\it tac}} 

190 
always has some effect on the state. 

323  191 
\end{ttdescription} 
104  192 

193 

194 
\subsection{Depthfirst search} 

323  195 
\index{tacticals!searching} 
104  196 
\index{tracing!of searching tacticals} 
197 
\begin{ttbox} 

198 
DEPTH_FIRST : (thm>bool) > tactic > tactic 

332  199 
DEPTH_SOLVE : tactic > tactic 
200 
DEPTH_SOLVE_1 : tactic > tactic 

104  201 
trace_DEPTH_FIRST: bool ref \hfill{\bf initially false} 
202 
\end{ttbox} 

323  203 
\begin{ttdescription} 
104  204 
\item[\ttindexbold{DEPTH_FIRST} {\it satp} {\it tac}] 
205 
returns the proof state if {\it satp} returns true. Otherwise it applies 

206 
{\it tac}, then recursively searches from each element of the resulting 

207 
sequence. The code uses a stack for efficiency, in effect applying 

208 
\hbox{\tt {\it tac} THEN DEPTH_FIRST {\it satp} {\it tac}} to the state. 

209 

210 
\item[\ttindexbold{DEPTH_SOLVE} {\it tac}] 

211 
uses {\tt DEPTH_FIRST} to search for states having no subgoals. 

212 

213 
\item[\ttindexbold{DEPTH_SOLVE_1} {\it tac}] 

214 
uses {\tt DEPTH_FIRST} to search for states having fewer subgoals than the 

215 
given state. Thus, it insists upon solving at least one subgoal. 

216 

4317  217 
\item[set \ttindexbold{trace_DEPTH_FIRST};] 
104  218 
enables interactive tracing for {\tt DEPTH_FIRST}. To view the 
219 
tracing options, type {\tt h} at the prompt. 

323  220 
\end{ttdescription} 
104  221 

222 

223 
\subsection{Other search strategies} 

323  224 
\index{tacticals!searching} 
104  225 
\index{tracing!of searching tacticals} 
226 
\begin{ttbox} 

332  227 
BREADTH_FIRST : (thm>bool) > tactic > tactic 
104  228 
BEST_FIRST : (thm>bool)*(thm>int) > tactic > tactic 
229 
THEN_BEST_FIRST : tactic * ((thm>bool) * (thm>int) * tactic) 

230 
> tactic \hfill{\bf infix 1} 

231 
trace_BEST_FIRST: bool ref \hfill{\bf initially false} 

232 
\end{ttbox} 

233 
These search strategies will find a solution if one exists. However, they 

234 
do not enumerate all solutions; they terminate after the first satisfactory 

235 
result from {\it tac}. 

323  236 
\begin{ttdescription} 
104  237 
\item[\ttindexbold{BREADTH_FIRST} {\it satp} {\it tac}] 
238 
uses breadthfirst search to find states for which {\it satp\/} is true. 

239 
For most applications, it is too slow. 

240 

241 
\item[\ttindexbold{BEST_FIRST} $(satp,distf)$ {\it tac}] 

242 
does a heuristic search, using {\it distf\/} to estimate the distance from 

243 
a satisfactory state. It maintains a list of states ordered by distance. 

244 
It applies $tac$ to the head of this list; if the result contains any 

245 
satisfactory states, then it returns them. Otherwise, {\tt BEST_FIRST} 

246 
adds the new states to the list, and continues. 

247 

248 
The distance function is typically \ttindex{size_of_thm}, which computes 

249 
the size of the state. The smaller the state, the fewer and simpler 

250 
subgoals it has. 

251 

252 
\item[$tac@0$ \ttindexbold{THEN_BEST_FIRST} $(satp,distf,tac)$] 

253 
is like {\tt BEST_FIRST}, except that the priority queue initially 

254 
contains the result of applying $tac@0$ to the proof state. This tactical 

255 
permits separate tactics for starting the search and continuing the search. 

256 

4317  257 
\item[set \ttindexbold{trace_BEST_FIRST};] 
286  258 
enables an interactive tracing mode for the tactical {\tt BEST_FIRST}. To 
259 
view the tracing options, type {\tt h} at the prompt. 

323  260 
\end{ttdescription} 
104  261 

262 

263 
\subsection{Auxiliary tacticals for searching} 

264 
\index{tacticals!conditional} 

265 
\index{tacticals!deterministic} 

266 
\begin{ttbox} 

8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

267 
COND : (thm>bool) > tactic > tactic > tactic 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

268 
IF_UNSOLVED : tactic > tactic 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

269 
SOLVE : tactic > tactic 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

270 
DETERM : tactic > tactic 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

271 
DETERM_UNTIL_SOLVED : tactic > tactic 
104  272 
\end{ttbox} 
323  273 
\begin{ttdescription} 
1118  274 
\item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$] 
104  275 
applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$ 
276 
otherwise. It is a conditional tactical in that only one of $tac@1$ and 

277 
$tac@2$ is applied to a proof state. However, both $tac@1$ and $tac@2$ are 

278 
evaluated because \ML{} uses eager evaluation. 

279 

280 
\item[\ttindexbold{IF_UNSOLVED} {\it tac}] 

281 
applies {\it tac\/} to the proof state if it has any subgoals, and simply 

282 
returns the proof state otherwise. Many common tactics, such as {\tt 

283 
resolve_tac}, fail if applied to a proof state that has no subgoals. 

284 

5754  285 
\item[\ttindexbold{SOLVE} {\it tac}] 
286 
applies {\it tac\/} to the proof state and then fails iff there are subgoals 

287 
left. 

288 

104  289 
\item[\ttindexbold{DETERM} {\it tac}] 
290 
applies {\it tac\/} to the proof state and returns the head of the 

291 
resulting sequence. {\tt DETERM} limits the search space by making its 

292 
argument deterministic. 

8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

293 

941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

294 
\item[\ttindexbold{DETERM_UNTIL_SOLVED} {\it tac}] 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

295 
forces repeated deterministic application of {\it tac\/} to the proof state 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
6569
diff
changeset

296 
until the goal is solved completely. 
323  297 
\end{ttdescription} 
104  298 

299 

300 
\subsection{Predicates and functions useful for searching} 

301 
\index{theorems!size of} 

302 
\index{theorems!equality of} 

303 
\begin{ttbox} 

304 
has_fewer_prems : int > thm > bool 

305 
eq_thm : thm * thm > bool 

13104  306 
eq_thm_prop : thm * thm > bool 
104  307 
size_of_thm : thm > int 
308 
\end{ttbox} 

323  309 
\begin{ttdescription} 
104  310 
\item[\ttindexbold{has_fewer_prems} $n$ $thm$] 
311 
reports whether $thm$ has fewer than~$n$ premises. By currying, 

312 
\hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may 

313 
be given to the searching tacticals. 

314 

6569  315 
\item[\ttindexbold{eq_thm} ($thm@1$, $thm@2$)] reports whether $thm@1$ and 
13104  316 
$thm@2$ are equal. Both theorems must have compatible signatures. Both 
317 
theorems must have the same conclusions, the same hypotheses (in the same 

318 
order), and the same set of sort hypotheses. Names of bound variables are 

319 
ignored. 

320 

321 
\item[\ttindexbold{eq_thm_prop} ($thm@1$, $thm@2$)] reports whether the 

322 
propositions of $thm@1$ and $thm@2$ are equal. Names of bound variables are 

323 
ignored. 

104  324 

325 
\item[\ttindexbold{size_of_thm} $thm$] 

326 
computes the size of $thm$, namely the number of variables, constants and 

327 
abstractions in its conclusion. It may serve as a distance function for 

328 
\ttindex{BEST_FIRST}. 

323  329 
\end{ttdescription} 
330 

331 
\index{search!tacticals)} 

104  332 

333 

334 
\section{Tacticals for subgoal numbering} 

335 
When conducting a backward proof, we normally consider one goal at a time. 

336 
A tactic can affect the entire proof state, but many tactics  such as 

337 
{\tt resolve_tac} and {\tt assume_tac}  work on a single subgoal. 

338 
Subgoals are designated by a positive integer, so Isabelle provides 

339 
tacticals for combining values of type {\tt int>tactic}. 

340 

341 

342 
\subsection{Restricting a tactic to one subgoal} 

343 
\index{tactics!restricting to a subgoal} 

344 
\index{tacticals!for restriction to a subgoal} 

345 
\begin{ttbox} 

346 
SELECT_GOAL : tactic > int > tactic 

347 
METAHYPS : (thm list > tactic) > int > tactic 

348 
\end{ttbox} 

323  349 
\begin{ttdescription} 
104  350 
\item[\ttindexbold{SELECT_GOAL} {\it tac} $i$] 
351 
restricts the effect of {\it tac\/} to subgoal~$i$ of the proof state. It 

352 
fails if there is no subgoal~$i$, or if {\it tac\/} changes the main goal 

353 
(do not use {\tt rewrite_tac}). It applies {\it tac\/} to a dummy proof 

354 
state and uses the result to refine the original proof state at 

355 
subgoal~$i$. If {\it tac\/} returns multiple results then so does 

356 
\hbox{\tt SELECT_GOAL {\it tac} $i$}. 

357 

323  358 
{\tt SELECT_GOAL} works by creating a state of the form $\phi\Imp\phi$, 
332  359 
with the one subgoal~$\phi$. If subgoal~$i$ has the form $\psi\Imp\theta$ 
360 
then $(\psi\Imp\theta)\Imp(\psi\Imp\theta)$ is in fact 

361 
$\List{\psi\Imp\theta;\; \psi}\Imp\theta$, a proof state with two subgoals. 

362 
Such a proof state might cause tactics to go astray. Therefore {\tt 

363 
SELECT_GOAL} inserts a quantifier to create the state 

323  364 
\[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta). \] 
104  365 

323  366 
\item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{metaassumptions} 
104  367 
takes subgoal~$i$, of the form 
368 
\[ \Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta, \] 

369 
and creates the list $\theta'@1$, \ldots, $\theta'@k$ of metalevel 

370 
assumptions. In these theorems, the subgoal's parameters ($x@1$, 

371 
\ldots,~$x@l$) become free variables. It supplies the assumptions to 

372 
$tacf$ and applies the resulting tactic to the proof state 

373 
$\theta\Imp\theta$. 

374 

375 
If the resulting proof state is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, 

376 
possibly containing $\theta'@1,\ldots,\theta'@k$ as assumptions, then it is 

377 
lifted back into the original context, yielding $n$ subgoals. 

378 

286  379 
Metalevel assumptions may not contain unknowns. Unknowns in the 
380 
hypotheses $\theta@1,\ldots,\theta@k$ become free variables in $\theta'@1$, 

381 
\ldots, $\theta'@k$, and are restored afterwards; the {\tt METAHYPS} call 

382 
cannot instantiate them. Unknowns in $\theta$ may be instantiated. New 

323  383 
unknowns in $\phi@1$, \ldots, $\phi@n$ are lifted over the parameters. 
104  384 

385 
Here is a typical application. Calling {\tt hyp_res_tac}~$i$ resolves 

386 
subgoal~$i$ with one of its own assumptions, which may itself have the form 

387 
of an inference rule (these are called {\bf higherlevel assumptions}). 

388 
\begin{ttbox} 

389 
val hyp_res_tac = METAHYPS (fn prems => resolve_tac prems 1); 

390 
\end{ttbox} 

332  391 
The function \ttindex{gethyps} is useful for debugging applications of {\tt 
392 
METAHYPS}. 

323  393 
\end{ttdescription} 
104  394 

395 
\begin{warn} 

396 
{\tt METAHYPS} fails if the context or new subgoals contain type unknowns. 

397 
In principle, the tactical could treat these like ordinary unknowns. 

398 
\end{warn} 

399 

400 

401 
\subsection{Scanning for a subgoal by number} 

323  402 
\index{tacticals!scanning for subgoals} 
104  403 
\begin{ttbox} 
404 
ALLGOALS : (int > tactic) > tactic 

405 
TRYALL : (int > tactic) > tactic 

406 
SOMEGOAL : (int > tactic) > tactic 

407 
FIRSTGOAL : (int > tactic) > tactic 

408 
REPEAT_SOME : (int > tactic) > tactic 

409 
REPEAT_FIRST : (int > tactic) > tactic 

410 
trace_goalno_tac : (int > tactic) > int > tactic 

411 
\end{ttbox} 

412 
These apply a tactic function of type {\tt int > tactic} to all the 

413 
subgoal numbers of a proof state, and join the resulting tactics using 

414 
\ttindex{THEN} or \ttindex{ORELSE}\@. Thus, they apply the tactic to all the 

415 
subgoals, or to one subgoal. 

416 

417 
Suppose that the original proof state has $n$ subgoals. 

418 

323  419 
\begin{ttdescription} 
104  420 
\item[\ttindexbold{ALLGOALS} {\it tacf}] 
421 
is equivalent to 

422 
\hbox{\tt$tacf(n)$ THEN \ldots{} THEN $tacf(1)$}. 

423 

323  424 
It applies {\it tacf} to all the subgoals, counting downwards (to 
104  425 
avoid problems when subgoals are added or deleted). 
426 

427 
\item[\ttindexbold{TRYALL} {\it tacf}] 

428 
is equivalent to 

323  429 
\hbox{\tt TRY$(tacf(n))$ THEN \ldots{} THEN TRY$(tacf(1))$}. 
104  430 

431 
It attempts to apply {\it tacf} to all the subgoals. For instance, 

286  432 
the tactic \hbox{\tt TRYALL assume_tac} attempts to solve all the subgoals by 
104  433 
assumption. 
434 

435 
\item[\ttindexbold{SOMEGOAL} {\it tacf}] 

436 
is equivalent to 

437 
\hbox{\tt$tacf(n)$ ORELSE \ldots{} ORELSE $tacf(1)$}. 

438 

323  439 
It applies {\it tacf} to one subgoal, counting downwards. For instance, 
286  440 
the tactic \hbox{\tt SOMEGOAL assume_tac} solves one subgoal by assumption, 
441 
failing if this is impossible. 

104  442 

443 
\item[\ttindexbold{FIRSTGOAL} {\it tacf}] 

444 
is equivalent to 

445 
\hbox{\tt$tacf(1)$ ORELSE \ldots{} ORELSE $tacf(n)$}. 

446 

323  447 
It applies {\it tacf} to one subgoal, counting upwards. 
104  448 

449 
\item[\ttindexbold{REPEAT_SOME} {\it tacf}] 

323  450 
applies {\it tacf} once or more to a subgoal, counting downwards. 
104  451 

452 
\item[\ttindexbold{REPEAT_FIRST} {\it tacf}] 

323  453 
applies {\it tacf} once or more to a subgoal, counting upwards. 
104  454 

455 
\item[\ttindexbold{trace_goalno_tac} {\it tac} {\it i}] 

456 
applies \hbox{\it tac i\/} to the proof state. If the resulting sequence 

457 
is nonempty, then it is returned, with the sideeffect of printing {\tt 

458 
Subgoal~$i$ selected}. Otherwise, {\tt trace_goalno_tac} returns the empty 

459 
sequence and prints nothing. 

460 

323  461 
It indicates that `the tactic worked for subgoal~$i$' and is mainly used 
104  462 
with {\tt SOMEGOAL} and {\tt FIRSTGOAL}. 
323  463 
\end{ttdescription} 
104  464 

465 

466 
\subsection{Joining tactic functions} 

323  467 
\index{tacticals!joining tactic functions} 
104  468 
\begin{ttbox} 
469 
THEN' : ('a > tactic) * ('a > tactic) > 'a > tactic \hfill{\bf infix 1} 

470 
ORELSE' : ('a > tactic) * ('a > tactic) > 'a > tactic \hfill{\bf infix} 

471 
APPEND' : ('a > tactic) * ('a > tactic) > 'a > tactic \hfill{\bf infix} 

472 
INTLEAVE' : ('a > tactic) * ('a > tactic) > 'a > tactic \hfill{\bf infix} 

473 
EVERY' : ('a > tactic) list > 'a > tactic 

474 
FIRST' : ('a > tactic) list > 'a > tactic 

475 
\end{ttbox} 

476 
These help to express tactics that specify subgoal numbers. The tactic 

477 
\begin{ttbox} 

478 
SOMEGOAL (fn i => resolve_tac rls i ORELSE eresolve_tac erls i) 

479 
\end{ttbox} 

480 
can be simplified to 

481 
\begin{ttbox} 

482 
SOMEGOAL (resolve_tac rls ORELSE' eresolve_tac erls) 

483 
\end{ttbox} 

484 
Note that {\tt TRY'}, {\tt REPEAT'}, {\tt DEPTH_FIRST'}, etc.\ are not 

485 
provided, because function composition accomplishes the same purpose. 

486 
The tactic 

487 
\begin{ttbox} 

488 
ALLGOALS (fn i => REPEAT (etac exE i ORELSE atac i)) 

489 
\end{ttbox} 

490 
can be simplified to 

491 
\begin{ttbox} 

492 
ALLGOALS (REPEAT o (etac exE ORELSE' atac)) 

493 
\end{ttbox} 

494 
These tacticals are polymorphic; $x$ need not be an integer. 

495 
\begin{center} \tt 

496 
\begin{tabular}{r@{\rm\ \ yields\ \ }l} 

323  497 
$(tacf@1$~~THEN'~~$tacf@2)(x)$ \index{*THEN'} & 
104  498 
$tacf@1(x)$~~THEN~~$tacf@2(x)$ \\ 
499 

323  500 
$(tacf@1$ ORELSE' $tacf@2)(x)$ \index{*ORELSE'} & 
104  501 
$tacf@1(x)$ ORELSE $tacf@2(x)$ \\ 
502 

323  503 
$(tacf@1$ APPEND' $tacf@2)(x)$ \index{*APPEND'} & 
104  504 
$tacf@1(x)$ APPEND $tacf@2(x)$ \\ 
505 

323  506 
$(tacf@1$ INTLEAVE' $tacf@2)(x)$ \index{*INTLEAVE'} & 
104  507 
$tacf@1(x)$ INTLEAVE $tacf@2(x)$ \\ 
508 

509 
EVERY' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*EVERY'} & 

510 
EVERY $[tacf@1(x),\ldots,tacf@n(x)]$ \\ 

511 

512 
FIRST' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*FIRST'} & 

513 
FIRST $[tacf@1(x),\ldots,tacf@n(x)]$ 

514 
\end{tabular} 

515 
\end{center} 

516 

517 

518 
\subsection{Applying a list of tactics to 1} 

323  519 
\index{tacticals!joining tactic functions} 
104  520 
\begin{ttbox} 
521 
EVERY1: (int > tactic) list > tactic 

522 
FIRST1: (int > tactic) list > tactic 

523 
\end{ttbox} 

524 
A common proof style is to treat the subgoals as a stack, always 

525 
restricting attention to the first subgoal. Such proofs contain long lists 

526 
of tactics, each applied to~1. These can be simplified using {\tt EVERY1} 

527 
and {\tt FIRST1}: 

528 
\begin{center} \tt 

529 
\begin{tabular}{r@{\rm\ \ abbreviates\ \ }l} 

530 
EVERY1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*EVERY1} & 

531 
EVERY $[tacf@1(1),\ldots,tacf@n(1)]$ \\ 

532 

533 
FIRST1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*FIRST1} & 

534 
FIRST $[tacf@1(1),\ldots,tacf@n(1)]$ 

535 
\end{tabular} 

536 
\end{center} 

537 

538 
\index{tacticals)} 

5371  539 

540 

541 
%%% Local Variables: 

542 
%%% mode: latex 

543 
%%% TeXmaster: "ref" 

544 
%%% End: 