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