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