author | wenzelm |
Wed, 25 Jan 2012 16:16:20 +0100 | |
changeset 46257 | 3ba3681d8930 |
parent 30184 | 37969710e61f |
child 46271 | e1b5460f1725 |
permissions | -rw-r--r-- |
30184
37969710e61f
removed parts of the manual that are clearly obsolete, or covered by
wenzelm
parents:
17818
diff
changeset
|
1 |
|
104 | 2 |
\chapter{Tactics} \label{tactics} |
30184
37969710e61f
removed parts of the manual that are clearly obsolete, or covered by
wenzelm
parents:
17818
diff
changeset
|
3 |
\index{tactics|(} |
104 | 4 |
|
5 |
\section{Other basic tactics} |
|
6 |
||
7 |
\subsection{Inserting premises and facts}\label{cut_facts_tac} |
|
323 | 8 |
\index{tactics!for inserting facts}\index{assumptions!inserting} |
104 | 9 |
\begin{ttbox} |
10 |
cut_facts_tac : thm list -> int -> tactic |
|
286 | 11 |
cut_inst_tac : (string*string)list -> thm -> int -> tactic |
12 |
subgoal_tac : string -> int -> tactic |
|
9523 | 13 |
subgoals_tac : string list -> int -> tactic |
104 | 14 |
\end{ttbox} |
2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
15 |
These tactics add assumptions to a subgoal. |
323 | 16 |
\begin{ttdescription} |
104 | 17 |
\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] |
18 |
adds the {\it thms} as new assumptions to subgoal~$i$. Once they have |
|
286 | 19 |
been inserted as assumptions, they become subject to tactics such as {\tt |
20 |
eresolve_tac} and {\tt rewrite_goals_tac}. Only rules with no premises |
|
21 |
are inserted: Isabelle cannot use assumptions that contain $\Imp$ |
|
22 |
or~$\Forall$. Sometimes the theorems are premises of a rule being |
|
23 |
derived, returned by~{\tt goal}; instead of calling this tactic, you |
|
24 |
could state the goal with an outermost meta-quantifier. |
|
25 |
||
26 |
\item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}] |
|
27 |
instantiates the {\it thm} with the instantiations {\it insts}, as |
|
7491 | 28 |
described in {\S}\ref{res_inst_tac}. It adds the resulting theorem as a |
286 | 29 |
new assumption to subgoal~$i$. |
104 | 30 |
|
31 |
\item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] |
|
9568 | 32 |
adds the {\it formula} as an assumption to subgoal~$i$, and inserts the same |
104 | 33 |
{\it formula} as a new subgoal, $i+1$. |
457 | 34 |
|
35 |
\item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}] |
|
36 |
uses {\tt subgoal_tac} to add the members of the list of {\it |
|
37 |
formulae} as assumptions to subgoal~$i$. |
|
323 | 38 |
\end{ttdescription} |
104 | 39 |
|
40 |
||
4317 | 41 |
\subsection{Definitions and meta-level rewriting} \label{sec:rewrite_goals} |
2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
42 |
\index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold} |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
43 |
\index{definitions} |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
44 |
|
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
45 |
Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
46 |
constant or a constant applied to a list of variables, for example $\it |
4317 | 47 |
sqr(n)\equiv n\times n$. Conditional definitions, $\phi\Imp t\equiv u$, |
48 |
are also supported. {\bf Unfolding} the definition ${t\equiv u}$ means using |
|
2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
49 |
it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem. {\bf |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
50 |
Folding} $t\equiv u$ means replacing~$u$ by~$t$. Rewriting continues until |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
51 |
no rewrites are applicable to any subterm. |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
52 |
|
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
53 |
There are rules for unfolding and folding definitions; Isabelle does not do |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
54 |
this automatically. The corresponding tactics rewrite the proof state, |
46257 | 55 |
yielding a single next state. |
2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
56 |
\begin{ttbox} |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
57 |
rewrite_goals_tac : thm list -> tactic |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
58 |
fold_goals_tac : thm list -> tactic |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
59 |
\end{ttbox} |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
60 |
\begin{ttdescription} |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
61 |
\item[\ttindexbold{rewrite_goals_tac} {\it defs}] |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
62 |
unfolds the {\it defs} throughout the subgoals of the proof state, while |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
63 |
leaving the main goal unchanged. Use \ttindex{SELECT_GOAL} to restrict it to a |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
64 |
particular subgoal. |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
65 |
|
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
66 |
\item[\ttindexbold{fold_goals_tac} {\it defs}] |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
67 |
folds the {\it defs} throughout the subgoals of the proof state, while |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
68 |
leaving the main goal unchanged. |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
69 |
\end{ttdescription} |
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
70 |
|
4317 | 71 |
\begin{warn} |
72 |
These tactics only cope with definitions expressed as meta-level |
|
73 |
equalities ($\equiv$). More general equivalences are handled by the |
|
74 |
simplifier, provided that it is set up appropriately for your logic |
|
75 |
(see Chapter~\ref{chap:simplification}). |
|
76 |
\end{warn} |
|
2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
77 |
|
104 | 78 |
\subsection{Theorems useful with tactics} |
323 | 79 |
\index{theorems!of pure theory} |
104 | 80 |
\begin{ttbox} |
81 |
asm_rl: thm |
|
82 |
cut_rl: thm |
|
83 |
\end{ttbox} |
|
323 | 84 |
\begin{ttdescription} |
85 |
\item[\tdx{asm_rl}] |
|
104 | 86 |
is $\psi\Imp\psi$. Under elim-resolution it does proof by assumption, and |
87 |
\hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to |
|
88 |
\begin{ttbox} |
|
89 |
assume_tac {\it i} ORELSE eresolve_tac {\it thms} {\it i} |
|
90 |
\end{ttbox} |
|
91 |
||
323 | 92 |
\item[\tdx{cut_rl}] |
104 | 93 |
is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting |
323 | 94 |
assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac} |
95 |
and {\tt subgoal_tac}. |
|
96 |
\end{ttdescription} |
|
104 | 97 |
|
98 |
||
99 |
\section{Obscure tactics} |
|
1212 | 100 |
|
2612 | 101 |
\subsection{Manipulating assumptions} |
102 |
\index{assumptions!rotating} |
|
103 |
\begin{ttbox} |
|
104 |
thin_tac : string -> int -> tactic |
|
105 |
rotate_tac : int -> int -> tactic |
|
106 |
\end{ttbox} |
|
107 |
\begin{ttdescription} |
|
108 |
\item[\ttindexbold{thin_tac} {\it formula} $i$] |
|
109 |
\index{assumptions!deleting} |
|
110 |
deletes the specified assumption from subgoal $i$. Often the assumption |
|
111 |
can be abbreviated, replacing subformul{\ae} by unknowns; the first matching |
|
112 |
assumption will be deleted. Removing useless assumptions from a subgoal |
|
113 |
increases its readability and can make search tactics run faster. |
|
114 |
||
115 |
\item[\ttindexbold{rotate_tac} $n$ $i$] |
|
116 |
\index{assumptions!rotating} |
|
117 |
rotates the assumptions of subgoal $i$ by $n$ positions: from right to left |
|
118 |
if $n$ is positive, and from left to right if $n$ is negative. This is |
|
119 |
sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which |
|
120 |
processes assumptions from left to right. |
|
121 |
\end{ttdescription} |
|
122 |
||
123 |
||
124 |
\subsection{Tidying the proof state} |
|
3400 | 125 |
\index{duplicate subgoals!removing} |
2612 | 126 |
\index{parameters!removing unused} |
127 |
\index{flex-flex constraints} |
|
128 |
\begin{ttbox} |
|
3400 | 129 |
distinct_subgoals_tac : tactic |
130 |
prune_params_tac : tactic |
|
131 |
flexflex_tac : tactic |
|
2612 | 132 |
\end{ttbox} |
133 |
\begin{ttdescription} |
|
9695 | 134 |
\item[\ttindexbold{distinct_subgoals_tac}] removes duplicate subgoals from a |
135 |
proof state. (These arise especially in ZF, where the subgoals are |
|
136 |
essentially type constraints.) |
|
3400 | 137 |
|
2612 | 138 |
\item[\ttindexbold{prune_params_tac}] |
139 |
removes unused parameters from all subgoals of the proof state. It works |
|
140 |
by rewriting with the theorem $(\Forall x. V)\equiv V$. This tactic can |
|
141 |
make the proof state more readable. It is used with |
|
142 |
\ttindex{rule_by_tactic} to simplify the resulting theorem. |
|
143 |
||
144 |
\item[\ttindexbold{flexflex_tac}] |
|
145 |
removes all flex-flex pairs from the proof state by applying the trivial |
|
146 |
unifier. This drastic step loses information, and should only be done as |
|
147 |
the last step of a proof. |
|
148 |
||
149 |
Flex-flex constraints arise from difficult cases of higher-order |
|
150 |
unification. To prevent this, use \ttindex{res_inst_tac} to instantiate |
|
7491 | 151 |
some variables in a rule~({\S}\ref{res_inst_tac}). Normally flex-flex |
2612 | 152 |
constraints can be ignored; they often disappear as unknowns get |
153 |
instantiated. |
|
154 |
\end{ttdescription} |
|
155 |
||
156 |
||
104 | 157 |
\subsection{Composition: resolution without lifting} |
323 | 158 |
\index{tactics!for composition} |
104 | 159 |
\begin{ttbox} |
160 |
compose_tac: (bool * thm * int) -> int -> tactic |
|
161 |
\end{ttbox} |
|
332 | 162 |
{\bf Composing} two rules means resolving them without prior lifting or |
104 | 163 |
renaming of unknowns. This low-level operation, which underlies the |
164 |
resolution tactics, may occasionally be useful for special effects. |
|
165 |
A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a |
|
166 |
rule, then passes the result to {\tt compose_tac}. |
|
323 | 167 |
\begin{ttdescription} |
104 | 168 |
\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$] |
169 |
refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to |
|
170 |
have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need |
|
323 | 171 |
not be atomic; thus $m$ determines the number of new subgoals. If |
104 | 172 |
$flag$ is {\tt true} then it performs elim-resolution --- it solves the |
173 |
first premise of~$rule$ by assumption and deletes that assumption. |
|
323 | 174 |
\end{ttdescription} |
104 | 175 |
|
176 |
||
4276 | 177 |
\section{*Managing lots of rules} |
104 | 178 |
These operations are not intended for interactive use. They are concerned |
179 |
with the processing of large numbers of rules in automatic proof |
|
180 |
strategies. Higher-order resolution involving a long list of rules is |
|
181 |
slow. Filtering techniques can shorten the list of rules given to |
|
2039
79c86b966257
Documented defer_tac and moved back the obsolete tactics like fold_tac
paulson
parents:
1212
diff
changeset
|
182 |
resolution, and can also detect whether a subgoal is too flexible, |
104 | 183 |
with too many rules applicable. |
184 |
||
185 |
\subsection{Combined resolution and elim-resolution} \label{biresolve_tac} |
|
186 |
\index{tactics!resolution} |
|
187 |
\begin{ttbox} |
|
188 |
biresolve_tac : (bool*thm)list -> int -> tactic |
|
189 |
bimatch_tac : (bool*thm)list -> int -> tactic |
|
190 |
subgoals_of_brl : bool*thm -> int |
|
191 |
lessb : (bool*thm) * (bool*thm) -> bool |
|
192 |
\end{ttbox} |
|
193 |
{\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs. For each |
|
194 |
pair, it applies resolution if the flag is~{\tt false} and |
|
195 |
elim-resolution if the flag is~{\tt true}. A single tactic call handles a |
|
196 |
mixture of introduction and elimination rules. |
|
197 |
||
323 | 198 |
\begin{ttdescription} |
104 | 199 |
\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}] |
200 |
refines the proof state by resolution or elim-resolution on each rule, as |
|
201 |
indicated by its flag. It affects subgoal~$i$ of the proof state. |
|
202 |
||
203 |
\item[\ttindexbold{bimatch_tac}] |
|
204 |
is like {\tt biresolve_tac}, but performs matching: unknowns in the |
|
7491 | 205 |
proof state are never updated (see~{\S}\ref{match_tac}). |
104 | 206 |
|
207 |
\item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})] |
|
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4317
diff
changeset
|
208 |
returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the |
104 | 209 |
pair (if applied to a suitable subgoal). This is $n$ if the flag is |
210 |
{\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number |
|
211 |
of premises of the rule. Elim-resolution yields one fewer subgoal than |
|
212 |
ordinary resolution because it solves the major premise by assumption. |
|
213 |
||
214 |
\item[\ttindexbold{lessb} ({\it brl1},{\it brl2})] |
|
215 |
returns the result of |
|
216 |
\begin{ttbox} |
|
332 | 217 |
subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2} |
104 | 218 |
\end{ttbox} |
323 | 219 |
\end{ttdescription} |
104 | 220 |
Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it |
221 |
(flag,rule)$ pairs by the number of new subgoals they will yield. Thus, |
|
222 |
those that yield the fewest subgoals should be tried first. |
|
223 |
||
224 |
||
323 | 225 |
\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac} |
104 | 226 |
\index{discrimination nets|bold} |
227 |
\index{tactics!resolution} |
|
228 |
\begin{ttbox} |
|
229 |
net_resolve_tac : thm list -> int -> tactic |
|
230 |
net_match_tac : thm list -> int -> tactic |
|
231 |
net_biresolve_tac: (bool*thm) list -> int -> tactic |
|
232 |
net_bimatch_tac : (bool*thm) list -> int -> tactic |
|
233 |
filt_resolve_tac : thm list -> int -> int -> tactic |
|
234 |
could_unify : term*term->bool |
|
8136 | 235 |
filter_thms : (term*term->bool) -> int*term*thm list -> thm{\ts}list |
104 | 236 |
\end{ttbox} |
323 | 237 |
The module {\tt Net} implements a discrimination net data structure for |
104 | 238 |
fast selection of rules \cite[Chapter 14]{charniak80}. A term is |
239 |
classified by the symbol list obtained by flattening it in preorder. |
|
240 |
The flattening takes account of function applications, constants, and free |
|
241 |
and bound variables; it identifies all unknowns and also regards |
|
323 | 242 |
\index{lambda abs@$\lambda$-abstractions} |
104 | 243 |
$\lambda$-abstractions as unknowns, since they could $\eta$-contract to |
244 |
anything. |
|
245 |
||
246 |
A discrimination net serves as a polymorphic dictionary indexed by terms. |
|
247 |
The module provides various functions for inserting and removing items from |
|
248 |
nets. It provides functions for returning all items whose term could match |
|
249 |
or unify with a target term. The matching and unification tests are |
|
250 |
overly lax (due to the identifications mentioned above) but they serve as |
|
251 |
useful filters. |
|
252 |
||
253 |
A net can store introduction rules indexed by their conclusion, and |
|
254 |
elimination rules indexed by their major premise. Isabelle provides |
|
323 | 255 |
several functions for `compiling' long lists of rules into fast |
104 | 256 |
resolution tactics. When supplied with a list of theorems, these functions |
257 |
build a discrimination net; the net is used when the tactic is applied to a |
|
332 | 258 |
goal. To avoid repeatedly constructing the nets, use currying: bind the |
104 | 259 |
resulting tactics to \ML{} identifiers. |
260 |
||
323 | 261 |
\begin{ttdescription} |
104 | 262 |
\item[\ttindexbold{net_resolve_tac} {\it thms}] |
263 |
builds a discrimination net to obtain the effect of a similar call to {\tt |
|
264 |
resolve_tac}. |
|
265 |
||
266 |
\item[\ttindexbold{net_match_tac} {\it thms}] |
|
267 |
builds a discrimination net to obtain the effect of a similar call to {\tt |
|
268 |
match_tac}. |
|
269 |
||
270 |
\item[\ttindexbold{net_biresolve_tac} {\it brls}] |
|
271 |
builds a discrimination net to obtain the effect of a similar call to {\tt |
|
272 |
biresolve_tac}. |
|
273 |
||
274 |
\item[\ttindexbold{net_bimatch_tac} {\it brls}] |
|
275 |
builds a discrimination net to obtain the effect of a similar call to {\tt |
|
276 |
bimatch_tac}. |
|
277 |
||
278 |
\item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}] |
|
279 |
uses discrimination nets to extract the {\it thms} that are applicable to |
|
280 |
subgoal~$i$. If more than {\it maxr\/} theorems are applicable then the |
|
281 |
tactic fails. Otherwise it calls {\tt resolve_tac}. |
|
282 |
||
283 |
This tactic helps avoid runaway instantiation of unknowns, for example in |
|
284 |
type inference. |
|
285 |
||
286 |
\item[\ttindexbold{could_unify} ({\it t},{\it u})] |
|
323 | 287 |
returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and |
104 | 288 |
otherwise returns~{\tt true}. It assumes all variables are distinct, |
289 |
reporting that {\tt ?a=?a} may unify with {\tt 0=1}. |
|
290 |
||
291 |
\item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$] |
|
292 |
returns the list of potentially resolvable rules (in {\it thms\/}) for the |
|
293 |
subgoal {\it prem}, using the predicate {\it could\/} to compare the |
|
294 |
conclusion of the subgoal with the conclusion of each rule. The resulting list |
|
295 |
is no longer than {\it limit}. |
|
323 | 296 |
\end{ttdescription} |
104 | 297 |
|
298 |
\index{tactics|)} |
|
5371 | 299 |
|
300 |
||
301 |
%%% Local Variables: |
|
302 |
%%% mode: latex |
|
303 |
%%% TeX-master: "ref" |
|
304 |
%%% End: |