1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{tactic}% |
|
4 % |
|
5 \isadelimtheory |
|
6 \isanewline |
|
7 \isanewline |
|
8 \isanewline |
|
9 % |
|
10 \endisadelimtheory |
|
11 % |
|
12 \isatagtheory |
|
13 \isacommand{theory}\isamarkupfalse% |
|
14 \ tactic\ \isakeyword{imports}\ base\ \isakeyword{begin}% |
|
15 \endisatagtheory |
|
16 {\isafoldtheory}% |
|
17 % |
|
18 \isadelimtheory |
|
19 % |
|
20 \endisadelimtheory |
|
21 % |
|
22 \isamarkupchapter{Tactical reasoning% |
|
23 } |
|
24 \isamarkuptrue% |
|
25 % |
|
26 \begin{isamarkuptext}% |
|
27 Tactical reasoning works by refining the initial claim in a |
|
28 backwards fashion, until a solved form is reached. A \isa{goal} |
|
29 consists of several subgoals that need to be solved in order to |
|
30 achieve the main statement; zero subgoals means that the proof may |
|
31 be finished. A \isa{tactic} is a refinement operation that maps |
|
32 a goal to a lazy sequence of potential successors. A \isa{tactical} is a combinator for composing tactics.% |
|
33 \end{isamarkuptext}% |
|
34 \isamarkuptrue% |
|
35 % |
|
36 \isamarkupsection{Goals \label{sec:tactical-goals}% |
|
37 } |
|
38 \isamarkuptrue% |
|
39 % |
|
40 \begin{isamarkuptext}% |
|
41 Isabelle/Pure represents a goal\glossary{Tactical goal}{A theorem of |
|
42 \seeglossary{Horn Clause} form stating that a number of subgoals |
|
43 imply the main conclusion, which is marked as a protected |
|
44 proposition.} as a theorem stating that the subgoals imply the main |
|
45 goal: \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}. The outermost goal |
|
46 structure is that of a Horn Clause\glossary{Horn Clause}{An iterated |
|
47 implication \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}, without any |
|
48 outermost quantifiers. Strictly speaking, propositions \isa{A\isactrlsub i} need to be atomic in Horn Clauses, but Isabelle admits |
|
49 arbitrary substructure here (nested \isa{{\isasymLongrightarrow}} and \isa{{\isasymAnd}} |
|
50 connectives).}: i.e.\ an iterated implication without any |
|
51 quantifiers\footnote{Recall that outermost \isa{{\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} is |
|
52 always represented via schematic variables in the body: \isa{{\isasymphi}{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}. These variables may get instantiated during the course of |
|
53 reasoning.}. For \isa{n\ {\isacharequal}\ {\isadigit{0}}} a goal is called ``solved''. |
|
54 |
|
55 The structure of each subgoal \isa{A\isactrlsub i} is that of a general |
|
56 Hereditary Harrop Formula \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymAnd}x\isactrlsub k{\isachardot}\ H\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ H\isactrlsub m\ {\isasymLongrightarrow}\ B} in |
|
57 normal form. Here \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub k} are goal parameters, i.e.\ |
|
58 arbitrary-but-fixed entities of certain types, and \isa{H\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ H\isactrlsub m} are goal hypotheses, i.e.\ facts that may be assumed locally. |
|
59 Together, this forms the goal context of the conclusion \isa{B} to |
|
60 be established. The goal hypotheses may be again arbitrary |
|
61 Hereditary Harrop Formulas, although the level of nesting rarely |
|
62 exceeds 1--2 in practice. |
|
63 |
|
64 The main conclusion \isa{C} is internally marked as a protected |
|
65 proposition\glossary{Protected proposition}{An arbitrarily |
|
66 structured proposition \isa{C} which is forced to appear as |
|
67 atomic by wrapping it into a propositional identity operator; |
|
68 notation \isa{{\isacharhash}C}. Protecting a proposition prevents basic |
|
69 inferences from entering into that structure for the time being.}, |
|
70 which is represented explicitly by the notation \isa{{\isacharhash}C}. This |
|
71 ensures that the decomposition into subgoals and main conclusion is |
|
72 well-defined for arbitrarily structured claims. |
|
73 |
|
74 \medskip Basic goal management is performed via the following |
|
75 Isabelle/Pure rules: |
|
76 |
|
77 \[ |
|
78 \infer[\isa{{\isacharparenleft}init{\isacharparenright}}]{\isa{C\ {\isasymLongrightarrow}\ {\isacharhash}C}}{} \qquad |
|
79 \infer[\isa{{\isacharparenleft}finish{\isacharparenright}}]{\isa{C}}{\isa{{\isacharhash}C}} |
|
80 \] |
|
81 |
|
82 \medskip The following low-level variants admit general reasoning |
|
83 with protected propositions: |
|
84 |
|
85 \[ |
|
86 \infer[\isa{{\isacharparenleft}protect{\isacharparenright}}]{\isa{{\isacharhash}C}}{\isa{C}} \qquad |
|
87 \infer[\isa{{\isacharparenleft}conclude{\isacharparenright}}]{\isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}}{\isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ {\isacharhash}C}} |
|
88 \]% |
|
89 \end{isamarkuptext}% |
|
90 \isamarkuptrue% |
|
91 % |
|
92 \isadelimmlref |
|
93 % |
|
94 \endisadelimmlref |
|
95 % |
|
96 \isatagmlref |
|
97 % |
|
98 \begin{isamarkuptext}% |
|
99 \begin{mldecls} |
|
100 \indexml{Goal.init}\verb|Goal.init: cterm -> thm| \\ |
|
101 \indexml{Goal.finish}\verb|Goal.finish: thm -> thm| \\ |
|
102 \indexml{Goal.protect}\verb|Goal.protect: thm -> thm| \\ |
|
103 \indexml{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\ |
|
104 \end{mldecls} |
|
105 |
|
106 \begin{description} |
|
107 |
|
108 \item \verb|Goal.init|~\isa{C} initializes a tactical goal from |
|
109 the well-formed proposition \isa{C}. |
|
110 |
|
111 \item \verb|Goal.finish|~\isa{thm} checks whether theorem |
|
112 \isa{thm} is a solved goal (no subgoals), and concludes the |
|
113 result by removing the goal protection. |
|
114 |
|
115 \item \verb|Goal.protect|~\isa{thm} protects the full statement |
|
116 of theorem \isa{thm}. |
|
117 |
|
118 \item \verb|Goal.conclude|~\isa{thm} removes the goal |
|
119 protection, even if there are pending subgoals. |
|
120 |
|
121 \end{description}% |
|
122 \end{isamarkuptext}% |
|
123 \isamarkuptrue% |
|
124 % |
|
125 \endisatagmlref |
|
126 {\isafoldmlref}% |
|
127 % |
|
128 \isadelimmlref |
|
129 % |
|
130 \endisadelimmlref |
|
131 % |
|
132 \isamarkupsection{Tactics% |
|
133 } |
|
134 \isamarkuptrue% |
|
135 % |
|
136 \begin{isamarkuptext}% |
|
137 A \isa{tactic} is a function \isa{goal\ {\isasymrightarrow}\ goal\isactrlsup {\isacharasterisk}\isactrlsup {\isacharasterisk}} that |
|
138 maps a given goal state (represented as a theorem, cf.\ |
|
139 \secref{sec:tactical-goals}) to a lazy sequence of potential |
|
140 successor states. The underlying sequence implementation is lazy |
|
141 both in head and tail, and is purely functional in \emph{not} |
|
142 supporting memoing.\footnote{The lack of memoing and the strict |
|
143 nature of SML requires some care when working with low-level |
|
144 sequence operations, to avoid duplicate or premature evaluation of |
|
145 results.} |
|
146 |
|
147 An \emph{empty result sequence} means that the tactic has failed: in |
|
148 a compound tactic expressions other tactics might be tried instead, |
|
149 or the whole refinement step might fail outright, producing a |
|
150 toplevel error message. When implementing tactics from scratch, one |
|
151 should take care to observe the basic protocol of mapping regular |
|
152 error conditions to an empty result; only serious faults should |
|
153 emerge as exceptions. |
|
154 |
|
155 By enumerating \emph{multiple results}, a tactic can easily express |
|
156 the potential outcome of an internal search process. There are also |
|
157 combinators for building proof tools that involve search |
|
158 systematically, see also \secref{sec:tacticals}. |
|
159 |
|
160 \medskip As explained in \secref{sec:tactical-goals}, a goal state |
|
161 essentially consists of a list of subgoals that imply the main goal |
|
162 (conclusion). Tactics may operate on all subgoals or on a |
|
163 particularly specified subgoal, but must not change the main |
|
164 conclusion (apart from instantiating schematic goal variables). |
|
165 |
|
166 Tactics with explicit \emph{subgoal addressing} are of the form |
|
167 \isa{int\ {\isasymrightarrow}\ tactic} and may be applied to a particular subgoal |
|
168 (counting from 1). If the subgoal number is out of range, the |
|
169 tactic should fail with an empty result sequence, but must not raise |
|
170 an exception! |
|
171 |
|
172 Operating on a particular subgoal means to replace it by an interval |
|
173 of zero or more subgoals in the same place; other subgoals must not |
|
174 be affected, apart from instantiating schematic variables ranging |
|
175 over the whole goal state. |
|
176 |
|
177 A common pattern of composing tactics with subgoal addressing is to |
|
178 try the first one, and then the second one only if the subgoal has |
|
179 not been solved yet. Special care is required here to avoid bumping |
|
180 into unrelated subgoals that happen to come after the original |
|
181 subgoal. Assuming that there is only a single initial subgoal is a |
|
182 very common error when implementing tactics! |
|
183 |
|
184 Tactics with internal subgoal addressing should expose the subgoal |
|
185 index as \isa{int} argument in full generality; a hardwired |
|
186 subgoal 1 inappropriate. |
|
187 |
|
188 \medskip The main well-formedness conditions for proper tactics are |
|
189 summarized as follows. |
|
190 |
|
191 \begin{itemize} |
|
192 |
|
193 \item General tactic failure is indicated by an empty result, only |
|
194 serious faults may produce an exception. |
|
195 |
|
196 \item The main conclusion must not be changed, apart from |
|
197 instantiating schematic variables. |
|
198 |
|
199 \item A tactic operates either uniformly on all subgoals, or |
|
200 specifically on a selected subgoal (without bumping into unrelated |
|
201 subgoals). |
|
202 |
|
203 \item Range errors in subgoal addressing produce an empty result. |
|
204 |
|
205 \end{itemize} |
|
206 |
|
207 Some of these conditions are checked by higher-level goal |
|
208 infrastructure (\secref{sec:results}); others are not checked |
|
209 explicitly, and violating them merely results in ill-behaved tactics |
|
210 experienced by the user (e.g.\ tactics that insist in being |
|
211 applicable only to singleton goals, or disallow composition with |
|
212 basic tacticals).% |
|
213 \end{isamarkuptext}% |
|
214 \isamarkuptrue% |
|
215 % |
|
216 \isadelimmlref |
|
217 % |
|
218 \endisadelimmlref |
|
219 % |
|
220 \isatagmlref |
|
221 % |
|
222 \begin{isamarkuptext}% |
|
223 \begin{mldecls} |
|
224 \indexmltype{tactic}\verb|type tactic = thm -> thm Seq.seq| \\ |
|
225 \indexml{no\_tac}\verb|no_tac: tactic| \\ |
|
226 \indexml{all\_tac}\verb|all_tac: tactic| \\ |
|
227 \indexml{print\_tac}\verb|print_tac: string -> tactic| \\[1ex] |
|
228 \indexml{PRIMITIVE}\verb|PRIMITIVE: (thm -> thm) -> tactic| \\[1ex] |
|
229 \indexml{SUBGOAL}\verb|SUBGOAL: (term * int -> tactic) -> int -> tactic| \\ |
|
230 \indexml{CSUBGOAL}\verb|CSUBGOAL: (cterm * int -> tactic) -> int -> tactic| \\ |
|
231 \end{mldecls} |
|
232 |
|
233 \begin{description} |
|
234 |
|
235 \item \verb|tactic| represents tactics. The well-formedness |
|
236 conditions described above need to be observed. See also \hyperlink{file.~~/src/Pure/General/seq.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}General{\isacharslash}seq{\isachardot}ML}}}} for the underlying implementation of |
|
237 lazy sequences. |
|
238 |
|
239 \item \verb|int -> tactic| represents tactics with explicit |
|
240 subgoal addressing, with well-formedness conditions as described |
|
241 above. |
|
242 |
|
243 \item \verb|no_tac| is a tactic that always fails, returning the |
|
244 empty sequence. |
|
245 |
|
246 \item \verb|all_tac| is a tactic that always succeeds, returning a |
|
247 singleton sequence with unchanged goal state. |
|
248 |
|
249 \item \verb|print_tac|~\isa{message} is like \verb|all_tac|, but |
|
250 prints a message together with the goal state on the tracing |
|
251 channel. |
|
252 |
|
253 \item \verb|PRIMITIVE|~\isa{rule} turns a primitive inference rule |
|
254 into a tactic with unique result. Exception \verb|THM| is considered |
|
255 a regular tactic failure and produces an empty result; other |
|
256 exceptions are passed through. |
|
257 |
|
258 \item \verb|SUBGOAL|~\isa{{\isacharparenleft}fn\ {\isacharparenleft}subgoal{\isacharcomma}\ i{\isacharparenright}\ {\isacharequal}{\isachargreater}\ tactic{\isacharparenright}} is the |
|
259 most basic form to produce a tactic with subgoal addressing. The |
|
260 given abstraction over the subgoal term and subgoal number allows to |
|
261 peek at the relevant information of the full goal state. The |
|
262 subgoal range is checked as required above. |
|
263 |
|
264 \item \verb|CSUBGOAL| is similar to \verb|SUBGOAL|, but passes the |
|
265 subgoal as \verb|cterm| instead of raw \verb|term|. This |
|
266 avoids expensive re-certification in situations where the subgoal is |
|
267 used directly for primitive inferences. |
|
268 |
|
269 \end{description}% |
|
270 \end{isamarkuptext}% |
|
271 \isamarkuptrue% |
|
272 % |
|
273 \endisatagmlref |
|
274 {\isafoldmlref}% |
|
275 % |
|
276 \isadelimmlref |
|
277 % |
|
278 \endisadelimmlref |
|
279 % |
|
280 \isamarkupsubsection{Resolution and assumption tactics \label{sec:resolve-assume-tac}% |
|
281 } |
|
282 \isamarkuptrue% |
|
283 % |
|
284 \begin{isamarkuptext}% |
|
285 \emph{Resolution} is the most basic mechanism for refining a |
|
286 subgoal using a theorem as object-level rule. |
|
287 \emph{Elim-resolution} is particularly suited for elimination rules: |
|
288 it resolves with a rule, proves its first premise by assumption, and |
|
289 finally deletes that assumption from any new subgoals. |
|
290 \emph{Destruct-resolution} is like elim-resolution, but the given |
|
291 destruction rules are first turned into canonical elimination |
|
292 format. \emph{Forward-resolution} is like destruct-resolution, but |
|
293 without deleting the selected assumption. The \isa{r{\isacharslash}e{\isacharslash}d{\isacharslash}f} |
|
294 naming convention is maintained for several different kinds of |
|
295 resolution rules and tactics. |
|
296 |
|
297 Assumption tactics close a subgoal by unifying some of its premises |
|
298 against its conclusion. |
|
299 |
|
300 \medskip All the tactics in this section operate on a subgoal |
|
301 designated by a positive integer. Other subgoals might be affected |
|
302 indirectly, due to instantiation of schematic variables. |
|
303 |
|
304 There are various sources of non-determinism, the tactic result |
|
305 sequence enumerates all possibilities of the following choices (if |
|
306 applicable): |
|
307 |
|
308 \begin{enumerate} |
|
309 |
|
310 \item selecting one of the rules given as argument to the tactic; |
|
311 |
|
312 \item selecting a subgoal premise to eliminate, unifying it against |
|
313 the first premise of the rule; |
|
314 |
|
315 \item unifying the conclusion of the subgoal to the conclusion of |
|
316 the rule. |
|
317 |
|
318 \end{enumerate} |
|
319 |
|
320 Recall that higher-order unification may produce multiple results |
|
321 that are enumerated here.% |
|
322 \end{isamarkuptext}% |
|
323 \isamarkuptrue% |
|
324 % |
|
325 \isadelimmlref |
|
326 % |
|
327 \endisadelimmlref |
|
328 % |
|
329 \isatagmlref |
|
330 % |
|
331 \begin{isamarkuptext}% |
|
332 \begin{mldecls} |
|
333 \indexml{resolve\_tac}\verb|resolve_tac: thm list -> int -> tactic| \\ |
|
334 \indexml{eresolve\_tac}\verb|eresolve_tac: thm list -> int -> tactic| \\ |
|
335 \indexml{dresolve\_tac}\verb|dresolve_tac: thm list -> int -> tactic| \\ |
|
336 \indexml{forward\_tac}\verb|forward_tac: thm list -> int -> tactic| \\[1ex] |
|
337 \indexml{assume\_tac}\verb|assume_tac: int -> tactic| \\ |
|
338 \indexml{eq\_assume\_tac}\verb|eq_assume_tac: int -> tactic| \\[1ex] |
|
339 \indexml{match\_tac}\verb|match_tac: thm list -> int -> tactic| \\ |
|
340 \indexml{ematch\_tac}\verb|ematch_tac: thm list -> int -> tactic| \\ |
|
341 \indexml{dmatch\_tac}\verb|dmatch_tac: thm list -> int -> tactic| \\ |
|
342 \end{mldecls} |
|
343 |
|
344 \begin{description} |
|
345 |
|
346 \item \verb|resolve_tac|~\isa{thms\ i} refines the goal state |
|
347 using the given theorems, which should normally be introduction |
|
348 rules. The tactic resolves a rule's conclusion with subgoal \isa{i}, replacing it by the corresponding versions of the rule's |
|
349 premises. |
|
350 |
|
351 \item \verb|eresolve_tac|~\isa{thms\ i} performs elim-resolution |
|
352 with the given theorems, which should normally be elimination rules. |
|
353 |
|
354 \item \verb|dresolve_tac|~\isa{thms\ i} performs |
|
355 destruct-resolution with the given theorems, which should normally |
|
356 be destruction rules. This replaces an assumption by the result of |
|
357 applying one of the rules. |
|
358 |
|
359 \item \verb|forward_tac| is like \verb|dresolve_tac| except that the |
|
360 selected assumption is not deleted. It applies a rule to an |
|
361 assumption, adding the result as a new assumption. |
|
362 |
|
363 \item \verb|assume_tac|~\isa{i} attempts to solve subgoal \isa{i} |
|
364 by assumption (modulo higher-order unification). |
|
365 |
|
366 \item \verb|eq_assume_tac| is similar to \verb|assume_tac|, but checks |
|
367 only for immediate \isa{{\isasymalpha}}-convertibility instead of using |
|
368 unification. It succeeds (with a unique next state) if one of the |
|
369 assumptions is equal to the subgoal's conclusion. Since it does not |
|
370 instantiate variables, it cannot make other subgoals unprovable. |
|
371 |
|
372 \item \verb|match_tac|, \verb|ematch_tac|, and \verb|dmatch_tac| are |
|
373 similar to \verb|resolve_tac|, \verb|eresolve_tac|, and \verb|dresolve_tac|, respectively, but do not instantiate schematic |
|
374 variables in the goal state. |
|
375 |
|
376 Flexible subgoals are not updated at will, but are left alone. |
|
377 Strictly speaking, matching means to treat the unknowns in the goal |
|
378 state as constants; these tactics merely discard unifiers that would |
|
379 update the goal state. |
|
380 |
|
381 \end{description}% |
|
382 \end{isamarkuptext}% |
|
383 \isamarkuptrue% |
|
384 % |
|
385 \endisatagmlref |
|
386 {\isafoldmlref}% |
|
387 % |
|
388 \isadelimmlref |
|
389 % |
|
390 \endisadelimmlref |
|
391 % |
|
392 \isamarkupsubsection{Explicit instantiation within a subgoal context% |
|
393 } |
|
394 \isamarkuptrue% |
|
395 % |
|
396 \begin{isamarkuptext}% |
|
397 The main resolution tactics (\secref{sec:resolve-assume-tac}) |
|
398 use higher-order unification, which works well in many practical |
|
399 situations despite its daunting theoretical properties. |
|
400 Nonetheless, there are important problem classes where unguided |
|
401 higher-order unification is not so useful. This typically involves |
|
402 rules like universal elimination, existential introduction, or |
|
403 equational substitution. Here the unification problem involves |
|
404 fully flexible \isa{{\isacharquery}P\ {\isacharquery}x} schemes, which are hard to manage |
|
405 without further hints. |
|
406 |
|
407 By providing a (small) rigid term for \isa{{\isacharquery}x} explicitly, the |
|
408 remaining unification problem is to assign a (large) term to \isa{{\isacharquery}P}, according to the shape of the given subgoal. This is |
|
409 sufficiently well-behaved in most practical situations. |
|
410 |
|
411 \medskip Isabelle provides separate versions of the standard \isa{r{\isacharslash}e{\isacharslash}d{\isacharslash}f} resolution tactics that allow to provide explicit |
|
412 instantiations of unknowns of the given rule, wrt.\ terms that refer |
|
413 to the implicit context of the selected subgoal. |
|
414 |
|
415 An instantiation consists of a list of pairs of the form \isa{{\isacharparenleft}{\isacharquery}x{\isacharcomma}\ t{\isacharparenright}}, where \isa{{\isacharquery}x} is a schematic variable occurring in |
|
416 the given rule, and \isa{t} is a term from the current proof |
|
417 context, augmented by the local goal parameters of the selected |
|
418 subgoal; cf.\ the \isa{focus} operation described in |
|
419 \secref{sec:variables}. |
|
420 |
|
421 Entering the syntactic context of a subgoal is a brittle operation, |
|
422 because its exact form is somewhat accidental, and the choice of |
|
423 bound variable names depends on the presence of other local and |
|
424 global names. Explicit renaming of subgoal parameters prior to |
|
425 explicit instantiation might help to achieve a bit more robustness. |
|
426 |
|
427 Type instantiations may be given as well, via pairs like \isa{{\isacharparenleft}{\isacharquery}{\isacharprime}a{\isacharcomma}\ {\isasymtau}{\isacharparenright}}. Type instantiations are distinguished from term |
|
428 instantiations by the syntactic form of the schematic variable. |
|
429 Types are instantiated before terms are. Since term instantiation |
|
430 already performs type-inference as expected, explicit type |
|
431 instantiations are seldom necessary.% |
|
432 \end{isamarkuptext}% |
|
433 \isamarkuptrue% |
|
434 % |
|
435 \isadelimmlref |
|
436 % |
|
437 \endisadelimmlref |
|
438 % |
|
439 \isatagmlref |
|
440 % |
|
441 \begin{isamarkuptext}% |
|
442 \begin{mldecls} |
|
443 \indexml{res\_inst\_tac}\verb|res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\ |
|
444 \indexml{eres\_inst\_tac}\verb|eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\ |
|
445 \indexml{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\ |
|
446 \indexml{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\[1ex] |
|
447 \indexml{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\ |
|
448 \end{mldecls} |
|
449 |
|
450 \begin{description} |
|
451 |
|
452 \item \verb|res_inst_tac|~\isa{ctxt\ insts\ thm\ i} instantiates the |
|
453 rule \isa{thm} with the instantiations \isa{insts}, as described |
|
454 above, and then performs resolution on subgoal \isa{i}. |
|
455 |
|
456 \item \verb|eres_inst_tac| is like \verb|res_inst_tac|, but performs |
|
457 elim-resolution. |
|
458 |
|
459 \item \verb|dres_inst_tac| is like \verb|res_inst_tac|, but performs |
|
460 destruct-resolution. |
|
461 |
|
462 \item \verb|forw_inst_tac| is like \verb|dres_inst_tac| except that |
|
463 the selected assumption is not deleted. |
|
464 |
|
465 \item \verb|rename_tac|~\isa{names\ i} renames the innermost |
|
466 parameters of subgoal \isa{i} according to the provided \isa{names} (which need to be distinct indentifiers). |
|
467 |
|
468 \end{description}% |
|
469 \end{isamarkuptext}% |
|
470 \isamarkuptrue% |
|
471 % |
|
472 \endisatagmlref |
|
473 {\isafoldmlref}% |
|
474 % |
|
475 \isadelimmlref |
|
476 % |
|
477 \endisadelimmlref |
|
478 % |
|
479 \isamarkupsection{Tacticals \label{sec:tacticals}% |
|
480 } |
|
481 \isamarkuptrue% |
|
482 % |
|
483 \begin{isamarkuptext}% |
|
484 FIXME |
|
485 |
|
486 \glossary{Tactical}{A functional combinator for building up complex |
|
487 tactics from simpler ones. Typical tactical perform sequential |
|
488 composition, disjunction (choice), iteration, or goal addressing. |
|
489 Various search strategies may be expressed via tacticals.}% |
|
490 \end{isamarkuptext}% |
|
491 \isamarkuptrue% |
|
492 % |
|
493 \isadelimtheory |
|
494 % |
|
495 \endisadelimtheory |
|
496 % |
|
497 \isatagtheory |
|
498 \isacommand{end}\isamarkupfalse% |
|
499 % |
|
500 \endisatagtheory |
|
501 {\isafoldtheory}% |
|
502 % |
|
503 \isadelimtheory |
|
504 % |
|
505 \endisadelimtheory |
|
506 \isanewline |
|
507 \isanewline |
|
508 \end{isabellebody}% |
|
509 %%% Local Variables: |
|
510 %%% mode: latex |
|
511 %%% TeX-master: "root" |
|
512 %%% End: |
|