104
|
1 |
%% $Id$
|
|
2 |
\chapter{Tactics} \label{tactics}
|
|
3 |
\index{tactics|(}
|
323
|
4 |
Tactics have type \mltydx{tactic}. They are essentially
|
104
|
5 |
functions from theorems to theorem sequences, where the theorems represent
|
|
6 |
states of a backward proof. Tactics seldom need to be coded from scratch,
|
323
|
7 |
as functions; instead they are expressed using basic tactics and tacticals.
|
104
|
8 |
|
|
9 |
\section{Resolution and assumption tactics}
|
|
10 |
{\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
|
|
11 |
a rule. {\bf Elim-resolution} is particularly suited for elimination
|
|
12 |
rules, while {\bf destruct-resolution} is particularly suited for
|
|
13 |
destruction rules. The {\tt r}, {\tt e}, {\tt d} naming convention is
|
|
14 |
maintained for several different kinds of resolution tactics, as well as
|
|
15 |
the shortcuts in the subgoal module.
|
|
16 |
|
|
17 |
All the tactics in this section act on a subgoal designated by a positive
|
|
18 |
integer~$i$. They fail (by returning the empty sequence) if~$i$ is out of
|
|
19 |
range.
|
|
20 |
|
|
21 |
\subsection{Resolution tactics}
|
323
|
22 |
\index{resolution!tactics}
|
104
|
23 |
\index{tactics!resolution|bold}
|
|
24 |
\begin{ttbox}
|
|
25 |
resolve_tac : thm list -> int -> tactic
|
|
26 |
eresolve_tac : thm list -> int -> tactic
|
|
27 |
dresolve_tac : thm list -> int -> tactic
|
|
28 |
forward_tac : thm list -> int -> tactic
|
|
29 |
\end{ttbox}
|
|
30 |
These perform resolution on a list of theorems, $thms$, representing a list
|
|
31 |
of object-rules. When generating next states, they take each of the rules
|
|
32 |
in the order given. Each rule may yield several next states, or none:
|
|
33 |
higher-order resolution may yield multiple resolvents.
|
323
|
34 |
\begin{ttdescription}
|
104
|
35 |
\item[\ttindexbold{resolve_tac} {\it thms} {\it i}]
|
323
|
36 |
refines the proof state using the rules, which should normally be
|
|
37 |
introduction rules. It resolves a rule's conclusion with
|
|
38 |
subgoal~$i$ of the proof state.
|
104
|
39 |
|
|
40 |
\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}]
|
323
|
41 |
\index{elim-resolution}
|
|
42 |
performs elim-resolution with the rules, which should normally be
|
|
43 |
elimination rules. It resolves with a rule, solves its first premise by
|
|
44 |
assumption, and finally {\em deletes\/} that assumption from any new
|
|
45 |
subgoals.
|
104
|
46 |
|
|
47 |
\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}]
|
323
|
48 |
\index{forward proof}\index{destruct-resolution}
|
|
49 |
performs destruct-resolution with the rules, which normally should
|
|
50 |
be destruction rules. This replaces an assumption by the result of
|
|
51 |
applying one of the rules.
|
104
|
52 |
|
323
|
53 |
\item[\ttindexbold{forward_tac}]\index{forward proof}
|
|
54 |
is like {\tt dresolve_tac} except that the selected assumption is not
|
|
55 |
deleted. It applies a rule to an assumption, adding the result as a new
|
|
56 |
assumption.
|
|
57 |
\end{ttdescription}
|
104
|
58 |
|
|
59 |
\subsection{Assumption tactics}
|
323
|
60 |
\index{tactics!assumption|bold}\index{assumptions!tactics for}
|
104
|
61 |
\begin{ttbox}
|
|
62 |
assume_tac : int -> tactic
|
|
63 |
eq_assume_tac : int -> tactic
|
|
64 |
\end{ttbox}
|
323
|
65 |
\begin{ttdescription}
|
104
|
66 |
\item[\ttindexbold{assume_tac} {\it i}]
|
|
67 |
attempts to solve subgoal~$i$ by assumption.
|
|
68 |
|
|
69 |
\item[\ttindexbold{eq_assume_tac}]
|
|
70 |
is like {\tt assume_tac} but does not use unification. It succeeds (with a
|
323
|
71 |
{\em unique\/} next state) if one of the assumptions is identical to the
|
104
|
72 |
subgoal's conclusion. Since it does not instantiate variables, it cannot
|
|
73 |
make other subgoals unprovable. It is intended to be called from proof
|
|
74 |
strategies, not interactively.
|
323
|
75 |
\end{ttdescription}
|
104
|
76 |
|
|
77 |
\subsection{Matching tactics} \label{match_tac}
|
323
|
78 |
\index{tactics!matching}
|
104
|
79 |
\begin{ttbox}
|
|
80 |
match_tac : thm list -> int -> tactic
|
|
81 |
ematch_tac : thm list -> int -> tactic
|
|
82 |
dmatch_tac : thm list -> int -> tactic
|
|
83 |
\end{ttbox}
|
|
84 |
These are just like the resolution tactics except that they never
|
|
85 |
instantiate unknowns in the proof state. Flexible subgoals are not updated
|
|
86 |
willy-nilly, but are left alone. Matching --- strictly speaking --- means
|
|
87 |
treating the unknowns in the proof state as constants; these tactics merely
|
|
88 |
discard unifiers that would update the proof state.
|
323
|
89 |
\begin{ttdescription}
|
104
|
90 |
\item[\ttindexbold{match_tac} {\it thms} {\it i}]
|
323
|
91 |
refines the proof state using the rules, matching a rule's
|
104
|
92 |
conclusion with subgoal~$i$ of the proof state.
|
|
93 |
|
|
94 |
\item[\ttindexbold{ematch_tac}]
|
|
95 |
is like {\tt match_tac}, but performs elim-resolution.
|
|
96 |
|
|
97 |
\item[\ttindexbold{dmatch_tac}]
|
|
98 |
is like {\tt match_tac}, but performs destruct-resolution.
|
323
|
99 |
\end{ttdescription}
|
104
|
100 |
|
|
101 |
|
|
102 |
\subsection{Resolution with instantiation} \label{res_inst_tac}
|
323
|
103 |
\index{tactics!instantiation}\index{instantiation}
|
104
|
104 |
\begin{ttbox}
|
|
105 |
res_inst_tac : (string*string)list -> thm -> int -> tactic
|
|
106 |
eres_inst_tac : (string*string)list -> thm -> int -> tactic
|
|
107 |
dres_inst_tac : (string*string)list -> thm -> int -> tactic
|
|
108 |
forw_inst_tac : (string*string)list -> thm -> int -> tactic
|
|
109 |
\end{ttbox}
|
|
110 |
These tactics are designed for applying rules such as substitution and
|
|
111 |
induction, which cause difficulties for higher-order unification. The
|
332
|
112 |
tactics accept explicit instantiations for unknowns in the rule ---
|
|
113 |
typically, in the rule's conclusion. Each instantiation is a pair
|
|
114 |
{\tt($v$,$e$)}, where $v$ is an unknown {\em without\/} its leading
|
|
115 |
question mark!
|
104
|
116 |
\begin{itemize}
|
332
|
117 |
\item If $v$ is the type unknown {\tt'a}, then
|
|
118 |
the rule must contain a type unknown \verb$?'a$ of some
|
104
|
119 |
sort~$s$, and $e$ should be a type of sort $s$.
|
|
120 |
|
332
|
121 |
\item If $v$ is the unknown {\tt P}, then
|
|
122 |
the rule must contain an unknown \verb$?P$ of some type~$\tau$,
|
104
|
123 |
and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
|
|
124 |
$\sigma$ are unifiable. If the unification of $\tau$ and $\sigma$
|
332
|
125 |
instantiates any type unknowns in $\tau$, these instantiations
|
104
|
126 |
are recorded for application to the rule.
|
|
127 |
\end{itemize}
|
|
128 |
Types are instantiated before terms. Because type instantiations are
|
|
129 |
inferred from term instantiations, explicit type instantiations are seldom
|
|
130 |
necessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list
|
|
131 |
\verb$[("'a","bool"),("t","True")]$ may be simplified to
|
|
132 |
\verb$[("t","True")]$. Type unknowns in the proof state may cause
|
|
133 |
failure because the tactics cannot instantiate them.
|
|
134 |
|
|
135 |
The instantiation tactics act on a given subgoal. Terms in the
|
|
136 |
instantiations are type-checked in the context of that subgoal --- in
|
|
137 |
particular, they may refer to that subgoal's parameters. Any unknowns in
|
|
138 |
the terms receive subscripts and are lifted over the parameters; thus, you
|
|
139 |
may not refer to unknowns in the subgoal.
|
|
140 |
|
323
|
141 |
\begin{ttdescription}
|
104
|
142 |
\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
|
|
143 |
instantiates the rule {\it thm} with the instantiations {\it insts}, as
|
|
144 |
described above, and then performs resolution on subgoal~$i$. Resolution
|
|
145 |
typically causes further instantiations; you need not give explicit
|
332
|
146 |
instantiations for every unknown in the rule.
|
104
|
147 |
|
|
148 |
\item[\ttindexbold{eres_inst_tac}]
|
|
149 |
is like {\tt res_inst_tac}, but performs elim-resolution.
|
|
150 |
|
|
151 |
\item[\ttindexbold{dres_inst_tac}]
|
|
152 |
is like {\tt res_inst_tac}, but performs destruct-resolution.
|
|
153 |
|
|
154 |
\item[\ttindexbold{forw_inst_tac}]
|
|
155 |
is like {\tt dres_inst_tac} except that the selected assumption is not
|
|
156 |
deleted. It applies the instantiated rule to an assumption, adding the
|
|
157 |
result as a new assumption.
|
323
|
158 |
\end{ttdescription}
|
104
|
159 |
|
|
160 |
|
|
161 |
\section{Other basic tactics}
|
|
162 |
\subsection{Definitions and meta-level rewriting}
|
323
|
163 |
\index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
|
|
164 |
\index{definitions}
|
|
165 |
|
332
|
166 |
Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
|
104
|
167 |
constant or a constant applied to a list of variables, for example $\it
|
|
168 |
sqr(n)\equiv n\times n$. (Conditional definitions, $\phi\Imp t\equiv u$,
|
332
|
169 |
are not supported.) {\bf Unfolding} the definition ${t\equiv u}$ means using
|
104
|
170 |
it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem. {\bf
|
|
171 |
Folding} $t\equiv u$ means replacing~$u$ by~$t$. Rewriting continues until
|
|
172 |
no rewrites are applicable to any subterm.
|
|
173 |
|
|
174 |
There are rules for unfolding and folding definitions; Isabelle does not do
|
|
175 |
this automatically. The corresponding tactics rewrite the proof state,
|
332
|
176 |
yielding a single next state. See also the {\tt goalw} command, which is the
|
104
|
177 |
easiest way of handling definitions.
|
|
178 |
\begin{ttbox}
|
|
179 |
rewrite_goals_tac : thm list -> tactic
|
|
180 |
rewrite_tac : thm list -> tactic
|
|
181 |
fold_goals_tac : thm list -> tactic
|
|
182 |
fold_tac : thm list -> tactic
|
|
183 |
\end{ttbox}
|
323
|
184 |
\begin{ttdescription}
|
104
|
185 |
\item[\ttindexbold{rewrite_goals_tac} {\it defs}]
|
|
186 |
unfolds the {\it defs} throughout the subgoals of the proof state, while
|
|
187 |
leaving the main goal unchanged. Use \ttindex{SELECT_GOAL} to restrict it to a
|
|
188 |
particular subgoal.
|
|
189 |
|
|
190 |
\item[\ttindexbold{rewrite_tac} {\it defs}]
|
|
191 |
unfolds the {\it defs} throughout the proof state, including the main goal
|
|
192 |
--- not normally desirable!
|
|
193 |
|
|
194 |
\item[\ttindexbold{fold_goals_tac} {\it defs}]
|
|
195 |
folds the {\it defs} throughout the subgoals of the proof state, while
|
|
196 |
leaving the main goal unchanged.
|
|
197 |
|
|
198 |
\item[\ttindexbold{fold_tac} {\it defs}]
|
|
199 |
folds the {\it defs} throughout the proof state.
|
323
|
200 |
\end{ttdescription}
|
104
|
201 |
|
|
202 |
|
|
203 |
\subsection{Tactic shortcuts}
|
323
|
204 |
\index{shortcuts!for tactics}
|
104
|
205 |
\index{tactics!resolution}\index{tactics!assumption}
|
|
206 |
\index{tactics!meta-rewriting}
|
|
207 |
\begin{ttbox}
|
332
|
208 |
rtac : thm -> int -> tactic
|
|
209 |
etac : thm -> int -> tactic
|
|
210 |
dtac : thm -> int -> tactic
|
|
211 |
atac : int -> tactic
|
104
|
212 |
ares_tac : thm list -> int -> tactic
|
332
|
213 |
rewtac : thm -> tactic
|
104
|
214 |
\end{ttbox}
|
|
215 |
These abbreviate common uses of tactics.
|
323
|
216 |
\begin{ttdescription}
|
104
|
217 |
\item[\ttindexbold{rtac} {\it thm} {\it i}]
|
|
218 |
abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.
|
|
219 |
|
|
220 |
\item[\ttindexbold{etac} {\it thm} {\it i}]
|
|
221 |
abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.
|
|
222 |
|
|
223 |
\item[\ttindexbold{dtac} {\it thm} {\it i}]
|
|
224 |
abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
|
|
225 |
destruct-resolution.
|
|
226 |
|
|
227 |
\item[\ttindexbold{atac} {\it i}]
|
332
|
228 |
abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
|
104
|
229 |
|
|
230 |
\item[\ttindexbold{ares_tac} {\it thms} {\it i}]
|
|
231 |
tries proof by assumption and resolution; it abbreviates
|
|
232 |
\begin{ttbox}
|
|
233 |
assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}
|
|
234 |
\end{ttbox}
|
|
235 |
|
|
236 |
\item[\ttindexbold{rewtac} {\it def}]
|
|
237 |
abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.
|
323
|
238 |
\end{ttdescription}
|
104
|
239 |
|
|
240 |
|
|
241 |
\subsection{Inserting premises and facts}\label{cut_facts_tac}
|
323
|
242 |
\index{tactics!for inserting facts}\index{assumptions!inserting}
|
104
|
243 |
\begin{ttbox}
|
|
244 |
cut_facts_tac : thm list -> int -> tactic
|
286
|
245 |
cut_inst_tac : (string*string)list -> thm -> int -> tactic
|
|
246 |
subgoal_tac : string -> int -> tactic
|
104
|
247 |
\end{ttbox}
|
332
|
248 |
These tactics add assumptions to a given subgoal.
|
323
|
249 |
\begin{ttdescription}
|
104
|
250 |
\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}]
|
|
251 |
adds the {\it thms} as new assumptions to subgoal~$i$. Once they have
|
286
|
252 |
been inserted as assumptions, they become subject to tactics such as {\tt
|
|
253 |
eresolve_tac} and {\tt rewrite_goals_tac}. Only rules with no premises
|
|
254 |
are inserted: Isabelle cannot use assumptions that contain $\Imp$
|
|
255 |
or~$\Forall$. Sometimes the theorems are premises of a rule being
|
|
256 |
derived, returned by~{\tt goal}; instead of calling this tactic, you
|
|
257 |
could state the goal with an outermost meta-quantifier.
|
|
258 |
|
|
259 |
\item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
|
|
260 |
instantiates the {\it thm} with the instantiations {\it insts}, as
|
|
261 |
described in \S\ref{res_inst_tac}. It adds the resulting theorem as a
|
|
262 |
new assumption to subgoal~$i$.
|
104
|
263 |
|
|
264 |
\item[\ttindexbold{subgoal_tac} {\it formula} {\it i}]
|
|
265 |
adds the {\it formula} as a assumption to subgoal~$i$, and inserts the same
|
|
266 |
{\it formula} as a new subgoal, $i+1$.
|
323
|
267 |
\end{ttdescription}
|
104
|
268 |
|
|
269 |
|
|
270 |
\subsection{Theorems useful with tactics}
|
323
|
271 |
\index{theorems!of pure theory}
|
104
|
272 |
\begin{ttbox}
|
|
273 |
asm_rl: thm
|
|
274 |
cut_rl: thm
|
|
275 |
\end{ttbox}
|
323
|
276 |
\begin{ttdescription}
|
|
277 |
\item[\tdx{asm_rl}]
|
104
|
278 |
is $\psi\Imp\psi$. Under elim-resolution it does proof by assumption, and
|
|
279 |
\hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to
|
|
280 |
\begin{ttbox}
|
|
281 |
assume_tac {\it i} ORELSE eresolve_tac {\it thms} {\it i}
|
|
282 |
\end{ttbox}
|
|
283 |
|
323
|
284 |
\item[\tdx{cut_rl}]
|
104
|
285 |
is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting
|
323
|
286 |
assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}
|
|
287 |
and {\tt subgoal_tac}.
|
|
288 |
\end{ttdescription}
|
104
|
289 |
|
|
290 |
|
|
291 |
\section{Obscure tactics}
|
|
292 |
\subsection{Tidying the proof state}
|
323
|
293 |
\index{parameters!removing unused}
|
104
|
294 |
\index{flex-flex constraints}
|
|
295 |
\begin{ttbox}
|
|
296 |
prune_params_tac : tactic
|
|
297 |
flexflex_tac : tactic
|
|
298 |
\end{ttbox}
|
323
|
299 |
\begin{ttdescription}
|
104
|
300 |
\item[\ttindexbold{prune_params_tac}]
|
|
301 |
removes unused parameters from all subgoals of the proof state. It works
|
|
302 |
by rewriting with the theorem $(\Forall x. V)\equiv V$. This tactic can
|
|
303 |
make the proof state more readable. It is used with
|
|
304 |
\ttindex{rule_by_tactic} to simplify the resulting theorem.
|
|
305 |
|
|
306 |
\item[\ttindexbold{flexflex_tac}]
|
|
307 |
removes all flex-flex pairs from the proof state by applying the trivial
|
|
308 |
unifier. This drastic step loses information, and should only be done as
|
|
309 |
the last step of a proof.
|
|
310 |
|
|
311 |
Flex-flex constraints arise from difficult cases of higher-order
|
|
312 |
unification. To prevent this, use \ttindex{res_inst_tac} to instantiate
|
|
313 |
some variables in a rule~(\S\ref{res_inst_tac}). Normally flex-flex
|
|
314 |
constraints can be ignored; they often disappear as unknowns get
|
|
315 |
instantiated.
|
323
|
316 |
\end{ttdescription}
|
104
|
317 |
|
|
318 |
|
323
|
319 |
\subsection{Renaming parameters in a goal} \index{parameters!renaming}
|
104
|
320 |
\begin{ttbox}
|
|
321 |
rename_tac : string -> int -> tactic
|
|
322 |
rename_last_tac : string -> string list -> int -> tactic
|
|
323 |
Logic.set_rename_prefix : string -> unit
|
|
324 |
Logic.auto_rename : bool ref \hfill{\bf initially false}
|
|
325 |
\end{ttbox}
|
|
326 |
When creating a parameter, Isabelle chooses its name by matching variable
|
|
327 |
names via the object-rule. Given the rule $(\forall I)$ formalized as
|
|
328 |
$\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note that
|
|
329 |
the $\Forall$-bound variable in the premise has the same name as the
|
|
330 |
$\forall$-bound variable in the conclusion.
|
|
331 |
|
|
332 |
Sometimes there is insufficient information and Isabelle chooses an
|
|
333 |
arbitrary name. The renaming tactics let you override Isabelle's choice.
|
|
334 |
Because renaming parameters has no logical effect on the proof state, the
|
323
|
335 |
{\tt by} command prints the message {\tt Warning:\ same as previous
|
104
|
336 |
level}.
|
|
337 |
|
|
338 |
Alternatively, you can suppress the naming mechanism described above and
|
|
339 |
have Isabelle generate uniform names for parameters. These names have the
|
|
340 |
form $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desired
|
|
341 |
prefix. They are ugly but predictable.
|
|
342 |
|
323
|
343 |
\begin{ttdescription}
|
104
|
344 |
\item[\ttindexbold{rename_tac} {\it str} {\it i}]
|
|
345 |
interprets the string {\it str} as a series of blank-separated variable
|
|
346 |
names, and uses them to rename the parameters of subgoal~$i$. The names
|
|
347 |
must be distinct. If there are fewer names than parameters, then the
|
|
348 |
tactic renames the innermost parameters and may modify the remaining ones
|
|
349 |
to ensure that all the parameters are distinct.
|
|
350 |
|
|
351 |
\item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}]
|
|
352 |
generates a list of names by attaching each of the {\it suffixes\/} to the
|
|
353 |
{\it prefix}. It is intended for coding structural induction tactics,
|
|
354 |
where several of the new parameters should have related names.
|
|
355 |
|
|
356 |
\item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};]
|
|
357 |
sets the prefix for uniform renaming to~{\it prefix}. The default prefix
|
|
358 |
is {\tt"k"}.
|
|
359 |
|
323
|
360 |
\item[\ttindexbold{Logic.auto_rename} := true;]
|
104
|
361 |
makes Isabelle generate uniform names for parameters.
|
323
|
362 |
\end{ttdescription}
|
104
|
363 |
|
|
364 |
|
|
365 |
\subsection{Composition: resolution without lifting}
|
323
|
366 |
\index{tactics!for composition}
|
104
|
367 |
\begin{ttbox}
|
|
368 |
compose_tac: (bool * thm * int) -> int -> tactic
|
|
369 |
\end{ttbox}
|
332
|
370 |
{\bf Composing} two rules means resolving them without prior lifting or
|
104
|
371 |
renaming of unknowns. This low-level operation, which underlies the
|
|
372 |
resolution tactics, may occasionally be useful for special effects.
|
|
373 |
A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
|
|
374 |
rule, then passes the result to {\tt compose_tac}.
|
323
|
375 |
\begin{ttdescription}
|
104
|
376 |
\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$]
|
|
377 |
refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to
|
|
378 |
have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
|
323
|
379 |
not be atomic; thus $m$ determines the number of new subgoals. If
|
104
|
380 |
$flag$ is {\tt true} then it performs elim-resolution --- it solves the
|
|
381 |
first premise of~$rule$ by assumption and deletes that assumption.
|
323
|
382 |
\end{ttdescription}
|
104
|
383 |
|
|
384 |
|
|
385 |
\section{Managing lots of rules}
|
|
386 |
These operations are not intended for interactive use. They are concerned
|
|
387 |
with the processing of large numbers of rules in automatic proof
|
|
388 |
strategies. Higher-order resolution involving a long list of rules is
|
|
389 |
slow. Filtering techniques can shorten the list of rules given to
|
|
390 |
resolution, and can also detect whether a given subgoal is too flexible,
|
|
391 |
with too many rules applicable.
|
|
392 |
|
|
393 |
\subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
|
|
394 |
\index{tactics!resolution}
|
|
395 |
\begin{ttbox}
|
|
396 |
biresolve_tac : (bool*thm)list -> int -> tactic
|
|
397 |
bimatch_tac : (bool*thm)list -> int -> tactic
|
|
398 |
subgoals_of_brl : bool*thm -> int
|
|
399 |
lessb : (bool*thm) * (bool*thm) -> bool
|
|
400 |
\end{ttbox}
|
|
401 |
{\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs. For each
|
|
402 |
pair, it applies resolution if the flag is~{\tt false} and
|
|
403 |
elim-resolution if the flag is~{\tt true}. A single tactic call handles a
|
|
404 |
mixture of introduction and elimination rules.
|
|
405 |
|
323
|
406 |
\begin{ttdescription}
|
104
|
407 |
\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}]
|
|
408 |
refines the proof state by resolution or elim-resolution on each rule, as
|
|
409 |
indicated by its flag. It affects subgoal~$i$ of the proof state.
|
|
410 |
|
|
411 |
\item[\ttindexbold{bimatch_tac}]
|
|
412 |
is like {\tt biresolve_tac}, but performs matching: unknowns in the
|
|
413 |
proof state are never updated (see~\S\ref{match_tac}).
|
|
414 |
|
|
415 |
\item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})]
|
|
416 |
returns the number of new subgoals that bi-resolution would yield for the
|
|
417 |
pair (if applied to a suitable subgoal). This is $n$ if the flag is
|
|
418 |
{\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
|
|
419 |
of premises of the rule. Elim-resolution yields one fewer subgoal than
|
|
420 |
ordinary resolution because it solves the major premise by assumption.
|
|
421 |
|
|
422 |
\item[\ttindexbold{lessb} ({\it brl1},{\it brl2})]
|
|
423 |
returns the result of
|
|
424 |
\begin{ttbox}
|
332
|
425 |
subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
|
104
|
426 |
\end{ttbox}
|
323
|
427 |
\end{ttdescription}
|
104
|
428 |
Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
|
|
429 |
(flag,rule)$ pairs by the number of new subgoals they will yield. Thus,
|
|
430 |
those that yield the fewest subgoals should be tried first.
|
|
431 |
|
|
432 |
|
323
|
433 |
\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}
|
104
|
434 |
\index{discrimination nets|bold}
|
|
435 |
\index{tactics!resolution}
|
|
436 |
\begin{ttbox}
|
|
437 |
net_resolve_tac : thm list -> int -> tactic
|
|
438 |
net_match_tac : thm list -> int -> tactic
|
|
439 |
net_biresolve_tac: (bool*thm) list -> int -> tactic
|
|
440 |
net_bimatch_tac : (bool*thm) list -> int -> tactic
|
|
441 |
filt_resolve_tac : thm list -> int -> int -> tactic
|
|
442 |
could_unify : term*term->bool
|
|
443 |
filter_thms : (term*term->bool) -> int*term*thm list -> thm list
|
|
444 |
\end{ttbox}
|
323
|
445 |
The module {\tt Net} implements a discrimination net data structure for
|
104
|
446 |
fast selection of rules \cite[Chapter 14]{charniak80}. A term is
|
|
447 |
classified by the symbol list obtained by flattening it in preorder.
|
|
448 |
The flattening takes account of function applications, constants, and free
|
|
449 |
and bound variables; it identifies all unknowns and also regards
|
323
|
450 |
\index{lambda abs@$\lambda$-abstractions}
|
104
|
451 |
$\lambda$-abstractions as unknowns, since they could $\eta$-contract to
|
|
452 |
anything.
|
|
453 |
|
|
454 |
A discrimination net serves as a polymorphic dictionary indexed by terms.
|
|
455 |
The module provides various functions for inserting and removing items from
|
|
456 |
nets. It provides functions for returning all items whose term could match
|
|
457 |
or unify with a target term. The matching and unification tests are
|
|
458 |
overly lax (due to the identifications mentioned above) but they serve as
|
|
459 |
useful filters.
|
|
460 |
|
|
461 |
A net can store introduction rules indexed by their conclusion, and
|
|
462 |
elimination rules indexed by their major premise. Isabelle provides
|
323
|
463 |
several functions for `compiling' long lists of rules into fast
|
104
|
464 |
resolution tactics. When supplied with a list of theorems, these functions
|
|
465 |
build a discrimination net; the net is used when the tactic is applied to a
|
332
|
466 |
goal. To avoid repeatedly constructing the nets, use currying: bind the
|
104
|
467 |
resulting tactics to \ML{} identifiers.
|
|
468 |
|
323
|
469 |
\begin{ttdescription}
|
104
|
470 |
\item[\ttindexbold{net_resolve_tac} {\it thms}]
|
|
471 |
builds a discrimination net to obtain the effect of a similar call to {\tt
|
|
472 |
resolve_tac}.
|
|
473 |
|
|
474 |
\item[\ttindexbold{net_match_tac} {\it thms}]
|
|
475 |
builds a discrimination net to obtain the effect of a similar call to {\tt
|
|
476 |
match_tac}.
|
|
477 |
|
|
478 |
\item[\ttindexbold{net_biresolve_tac} {\it brls}]
|
|
479 |
builds a discrimination net to obtain the effect of a similar call to {\tt
|
|
480 |
biresolve_tac}.
|
|
481 |
|
|
482 |
\item[\ttindexbold{net_bimatch_tac} {\it brls}]
|
|
483 |
builds a discrimination net to obtain the effect of a similar call to {\tt
|
|
484 |
bimatch_tac}.
|
|
485 |
|
|
486 |
\item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}]
|
|
487 |
uses discrimination nets to extract the {\it thms} that are applicable to
|
|
488 |
subgoal~$i$. If more than {\it maxr\/} theorems are applicable then the
|
|
489 |
tactic fails. Otherwise it calls {\tt resolve_tac}.
|
|
490 |
|
|
491 |
This tactic helps avoid runaway instantiation of unknowns, for example in
|
|
492 |
type inference.
|
|
493 |
|
|
494 |
\item[\ttindexbold{could_unify} ({\it t},{\it u})]
|
323
|
495 |
returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and
|
104
|
496 |
otherwise returns~{\tt true}. It assumes all variables are distinct,
|
|
497 |
reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
|
|
498 |
|
|
499 |
\item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$]
|
|
500 |
returns the list of potentially resolvable rules (in {\it thms\/}) for the
|
|
501 |
subgoal {\it prem}, using the predicate {\it could\/} to compare the
|
|
502 |
conclusion of the subgoal with the conclusion of each rule. The resulting list
|
|
503 |
is no longer than {\it limit}.
|
323
|
504 |
\end{ttdescription}
|
104
|
505 |
|
|
506 |
|
|
507 |
\section{Programming tools for proof strategies}
|
|
508 |
Do not consider using the primitives discussed in this section unless you
|
323
|
509 |
really need to code tactics from scratch.
|
104
|
510 |
|
|
511 |
\subsection{Operations on type {\tt tactic}}
|
323
|
512 |
\index{tactics!primitives for coding}
|
104
|
513 |
A tactic maps theorems to theorem sequences (lazy lists). The type
|
323
|
514 |
constructor for sequences is called \mltydx{Sequence.seq}. To simplify the
|
104
|
515 |
types of tactics and tacticals, Isabelle defines a type of tactics:
|
|
516 |
\begin{ttbox}
|
|
517 |
datatype tactic = Tactic of thm -> thm Sequence.seq
|
|
518 |
\end{ttbox}
|
|
519 |
{\tt Tactic} and {\tt tapply} convert between tactics and functions. The
|
|
520 |
other operations provide means for coding tactics in a clean style.
|
|
521 |
\begin{ttbox}
|
|
522 |
tapply : tactic * thm -> thm Sequence.seq
|
|
523 |
Tactic : (thm -> thm Sequence.seq) -> tactic
|
|
524 |
PRIMITIVE : (thm -> thm) -> tactic
|
|
525 |
STATE : (thm -> tactic) -> tactic
|
|
526 |
SUBGOAL : ((term*int) -> tactic) -> int -> tactic
|
|
527 |
\end{ttbox}
|
323
|
528 |
\begin{ttdescription}
|
|
529 |
\item[\ttindexbold{tapply}({\it tac}, {\it thm})]
|
104
|
530 |
returns the result of applying the tactic, as a function, to {\it thm}.
|
|
531 |
|
|
532 |
\item[\ttindexbold{Tactic} {\it f}]
|
|
533 |
packages {\it f} as a tactic.
|
|
534 |
|
|
535 |
\item[\ttindexbold{PRIMITIVE} $f$]
|
|
536 |
applies $f$ to the proof state and returns the result as a
|
|
537 |
one-element sequence. This packages the meta-rule~$f$ as a tactic.
|
|
538 |
|
|
539 |
\item[\ttindexbold{STATE} $f$]
|
|
540 |
applies $f$ to the proof state and then applies the resulting tactic to the
|
|
541 |
same state. It supports the following style, where the tactic body is
|
323
|
542 |
expressed using tactics and tacticals, but may peek at the proof state:
|
104
|
543 |
\begin{ttbox}
|
323
|
544 |
STATE (fn state => {\it tactic-valued expression})
|
104
|
545 |
\end{ttbox}
|
|
546 |
|
|
547 |
\item[\ttindexbold{SUBGOAL} $f$ $i$]
|
|
548 |
extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
|
|
549 |
tactic by calling~$f(t,i)$. It applies the resulting tactic to the same
|
323
|
550 |
state. The tactic body is expressed using tactics and tacticals, but may
|
|
551 |
peek at a particular subgoal:
|
104
|
552 |
\begin{ttbox}
|
323
|
553 |
SUBGOAL (fn (t,i) => {\it tactic-valued expression})
|
104
|
554 |
\end{ttbox}
|
323
|
555 |
\end{ttdescription}
|
104
|
556 |
|
|
557 |
|
|
558 |
\subsection{Tracing}
|
323
|
559 |
\index{tactics!tracing}
|
104
|
560 |
\index{tracing!of tactics}
|
|
561 |
\begin{ttbox}
|
|
562 |
pause_tac: tactic
|
|
563 |
print_tac: tactic
|
|
564 |
\end{ttbox}
|
332
|
565 |
These tactics print tracing information when they are applied to a proof
|
|
566 |
state. Their output may be difficult to interpret. Note that certain of
|
|
567 |
the searching tacticals, such as {\tt REPEAT}, have built-in tracing
|
|
568 |
options.
|
323
|
569 |
\begin{ttdescription}
|
104
|
570 |
\item[\ttindexbold{pause_tac}]
|
332
|
571 |
prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line
|
|
572 |
from the terminal. If this line is blank then it returns the proof state
|
|
573 |
unchanged; otherwise it fails (which may terminate a repetition).
|
104
|
574 |
|
|
575 |
\item[\ttindexbold{print_tac}]
|
|
576 |
returns the proof state unchanged, with the side effect of printing it at
|
|
577 |
the terminal.
|
323
|
578 |
\end{ttdescription}
|
104
|
579 |
|
|
580 |
|
323
|
581 |
\section{Sequences}
|
104
|
582 |
\index{sequences (lazy lists)|bold}
|
323
|
583 |
The module {\tt Sequence} declares a type of lazy lists. It uses
|
|
584 |
Isabelle's type \mltydx{option} to represent the possible presence
|
104
|
585 |
(\ttindexbold{Some}) or absence (\ttindexbold{None}) of
|
|
586 |
a value:
|
|
587 |
\begin{ttbox}
|
|
588 |
datatype 'a option = None | Some of 'a;
|
|
589 |
\end{ttbox}
|
286
|
590 |
For clarity, the module name {\tt Sequence} is omitted from the signature
|
|
591 |
specifications below; for instance, {\tt null} appears instead of {\tt
|
|
592 |
Sequence.null}.
|
104
|
593 |
|
323
|
594 |
\subsection{Basic operations on sequences}
|
104
|
595 |
\begin{ttbox}
|
286
|
596 |
null : 'a seq
|
|
597 |
seqof : (unit -> ('a * 'a seq) option) -> 'a seq
|
|
598 |
single : 'a -> 'a seq
|
|
599 |
pull : 'a seq -> ('a * 'a seq) option
|
104
|
600 |
\end{ttbox}
|
323
|
601 |
\begin{ttdescription}
|
|
602 |
\item[Sequence.null]
|
104
|
603 |
is the empty sequence.
|
|
604 |
|
|
605 |
\item[\tt Sequence.seqof (fn()=> Some($x$,$s$))]
|
|
606 |
constructs the sequence with head~$x$ and tail~$s$, neither of which is
|
|
607 |
evaluated.
|
|
608 |
|
323
|
609 |
\item[Sequence.single $x$]
|
104
|
610 |
constructs the sequence containing the single element~$x$.
|
|
611 |
|
323
|
612 |
\item[Sequence.pull $s$]
|
104
|
613 |
returns {\tt None} if the sequence is empty and {\tt Some($x$,$s'$)} if the
|
|
614 |
sequence has head~$x$ and tail~$s'$. Warning: calling \hbox{Sequence.pull
|
332
|
615 |
$s$} again will {\it recompute\/} the value of~$x$; it is not stored!
|
323
|
616 |
\end{ttdescription}
|
104
|
617 |
|
|
618 |
|
323
|
619 |
\subsection{Converting between sequences and lists}
|
104
|
620 |
\begin{ttbox}
|
286
|
621 |
chop : int * 'a seq -> 'a list * 'a seq
|
|
622 |
list_of_s : 'a seq -> 'a list
|
|
623 |
s_of_list : 'a list -> 'a seq
|
104
|
624 |
\end{ttbox}
|
323
|
625 |
\begin{ttdescription}
|
332
|
626 |
\item[Sequence.chop($n$,$s$)]
|
104
|
627 |
returns the first~$n$ elements of~$s$ as a list, paired with the remaining
|
|
628 |
elements of~$s$. If $s$ has fewer than~$n$ elements, then so will the
|
|
629 |
list.
|
|
630 |
|
323
|
631 |
\item[Sequence.list_of_s $s$]
|
104
|
632 |
returns the elements of~$s$, which must be finite, as a list.
|
|
633 |
|
323
|
634 |
\item[Sequence.s_of_list $l$]
|
104
|
635 |
creates a sequence containing the elements of~$l$.
|
323
|
636 |
\end{ttdescription}
|
104
|
637 |
|
|
638 |
|
323
|
639 |
\subsection{Combining sequences}
|
104
|
640 |
\begin{ttbox}
|
286
|
641 |
append : 'a seq * 'a seq -> 'a seq
|
|
642 |
interleave : 'a seq * 'a seq -> 'a seq
|
|
643 |
flats : 'a seq seq -> 'a seq
|
|
644 |
maps : ('a -> 'b) -> 'a seq -> 'b seq
|
|
645 |
filters : ('a -> bool) -> 'a seq -> 'a seq
|
104
|
646 |
\end{ttbox}
|
323
|
647 |
\begin{ttdescription}
|
332
|
648 |
\item[Sequence.append($s@1$,$s@2$)]
|
104
|
649 |
concatenates $s@1$ to $s@2$.
|
|
650 |
|
332
|
651 |
\item[Sequence.interleave($s@1$,$s@2$)]
|
104
|
652 |
joins $s@1$ with $s@2$ by interleaving their elements. The result contains
|
|
653 |
all the elements of the sequences, even if both are infinite.
|
|
654 |
|
323
|
655 |
\item[Sequence.flats $ss$]
|
104
|
656 |
concatenates a sequence of sequences.
|
|
657 |
|
323
|
658 |
\item[Sequence.maps $f$ $s$]
|
104
|
659 |
applies $f$ to every element of~$s=x@1,x@2,\ldots$, yielding the sequence
|
|
660 |
$f(x@1),f(x@2),\ldots$.
|
|
661 |
|
323
|
662 |
\item[Sequence.filters $p$ $s$]
|
104
|
663 |
returns the sequence consisting of all elements~$x$ of~$s$ such that $p(x)$
|
|
664 |
is {\tt true}.
|
323
|
665 |
\end{ttdescription}
|
104
|
666 |
|
|
667 |
\index{tactics|)}
|