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