author | wenzelm |
Wed, 25 Jan 2012 19:04:38 +0100 | |
changeset 46259 | 6fab37137dcb |
parent 46258 | 89ee3bc580a8 |
child 46260 | 9be4ff2dd91e |
permissions | -rw-r--r-- |
29755 | 1 |
theory Tactic |
2 |
imports Base |
|
3 |
begin |
|
18537 | 4 |
|
20452 | 5 |
chapter {* Tactical reasoning *} |
18537 | 6 |
|
34930 | 7 |
text {* Tactical reasoning works by refining an initial claim in a |
20474 | 8 |
backwards fashion, until a solved form is reached. A @{text "goal"} |
9 |
consists of several subgoals that need to be solved in order to |
|
10 |
achieve the main statement; zero subgoals means that the proof may |
|
11 |
be finished. A @{text "tactic"} is a refinement operation that maps |
|
12 |
a goal to a lazy sequence of potential successors. A @{text |
|
34930 | 13 |
"tactical"} is a combinator for composing tactics. *} |
18537 | 14 |
|
15 |
||
16 |
section {* Goals \label{sec:tactical-goals} *} |
|
17 |
||
20451 | 18 |
text {* |
29758 | 19 |
Isabelle/Pure represents a goal as a theorem stating that the |
20 |
subgoals imply the main goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> |
|
21 |
C"}. The outermost goal structure is that of a Horn Clause: i.e.\ |
|
22 |
an iterated implication without any quantifiers\footnote{Recall that |
|
23 |
outermost @{text "\<And>x. \<phi>[x]"} is always represented via schematic |
|
24 |
variables in the body: @{text "\<phi>[?x]"}. These variables may get |
|
25 |
instantiated during the course of reasoning.}. For @{text "n = 0"} |
|
26 |
a goal is called ``solved''. |
|
18537 | 27 |
|
29761 | 28 |
The structure of each subgoal @{text "A\<^sub>i"} is that of a |
29 |
general Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots> |
|
30 |
\<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"}. Here @{text |
|
31 |
"x\<^sub>1, \<dots>, x\<^sub>k"} are goal parameters, i.e.\ |
|
32 |
arbitrary-but-fixed entities of certain types, and @{text |
|
33 |
"H\<^sub>1, \<dots>, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may |
|
34 |
be assumed locally. Together, this forms the goal context of the |
|
35 |
conclusion @{text B} to be established. The goal hypotheses may be |
|
36 |
again arbitrary Hereditary Harrop Formulas, although the level of |
|
37 |
nesting rarely exceeds 1--2 in practice. |
|
18537 | 38 |
|
20451 | 39 |
The main conclusion @{text C} is internally marked as a protected |
29758 | 40 |
proposition, which is represented explicitly by the notation @{text |
34930 | 41 |
"#C"} here. This ensures that the decomposition into subgoals and |
42 |
main conclusion is well-defined for arbitrarily structured claims. |
|
18537 | 43 |
|
20451 | 44 |
\medskip Basic goal management is performed via the following |
45 |
Isabelle/Pure rules: |
|
18537 | 46 |
|
47 |
\[ |
|
48 |
\infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad |
|
20547 | 49 |
\infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}} |
18537 | 50 |
\] |
51 |
||
52 |
\medskip The following low-level variants admit general reasoning |
|
53 |
with protected propositions: |
|
54 |
||
55 |
\[ |
|
56 |
\infer[@{text "(protect)"}]{@{text "#C"}}{@{text "C"}} \qquad |
|
57 |
\infer[@{text "(conclude)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}} |
|
58 |
\] |
|
59 |
*} |
|
60 |
||
61 |
text %mlref {* |
|
62 |
\begin{mldecls} |
|
63 |
@{index_ML Goal.init: "cterm -> thm"} \\ |
|
32201
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30272
diff
changeset
|
64 |
@{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\ |
18537 | 65 |
@{index_ML Goal.protect: "thm -> thm"} \\ |
66 |
@{index_ML Goal.conclude: "thm -> thm"} \\ |
|
67 |
\end{mldecls} |
|
68 |
||
69 |
\begin{description} |
|
70 |
||
20474 | 71 |
\item @{ML "Goal.init"}~@{text C} initializes a tactical goal from |
72 |
the well-formed proposition @{text C}. |
|
18537 | 73 |
|
32201
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30272
diff
changeset
|
74 |
\item @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem |
20474 | 75 |
@{text "thm"} is a solved goal (no subgoals), and concludes the |
32201
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30272
diff
changeset
|
76 |
result by removing the goal protection. The context is only |
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30272
diff
changeset
|
77 |
required for printing error messages. |
18537 | 78 |
|
20474 | 79 |
\item @{ML "Goal.protect"}~@{text "thm"} protects the full statement |
80 |
of theorem @{text "thm"}. |
|
18537 | 81 |
|
20474 | 82 |
\item @{ML "Goal.conclude"}~@{text "thm"} removes the goal |
83 |
protection, even if there are pending subgoals. |
|
18537 | 84 |
|
85 |
\end{description} |
|
86 |
*} |
|
87 |
||
88 |
||
39847 | 89 |
section {* Tactics\label{sec:tactics} *} |
18537 | 90 |
|
28781 | 91 |
text {* A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that |
92 |
maps a given goal state (represented as a theorem, cf.\ |
|
93 |
\secref{sec:tactical-goals}) to a lazy sequence of potential |
|
94 |
successor states. The underlying sequence implementation is lazy |
|
95 |
both in head and tail, and is purely functional in \emph{not} |
|
96 |
supporting memoing.\footnote{The lack of memoing and the strict |
|
97 |
nature of SML requires some care when working with low-level |
|
98 |
sequence operations, to avoid duplicate or premature evaluation of |
|
34930 | 99 |
results. It also means that modified runtime behavior, such as |
100 |
timeout, is very hard to achieve for general tactics.} |
|
18537 | 101 |
|
28781 | 102 |
An \emph{empty result sequence} means that the tactic has failed: in |
34930 | 103 |
a compound tactic expression other tactics might be tried instead, |
28781 | 104 |
or the whole refinement step might fail outright, producing a |
34930 | 105 |
toplevel error message in the end. When implementing tactics from |
106 |
scratch, one should take care to observe the basic protocol of |
|
107 |
mapping regular error conditions to an empty result; only serious |
|
108 |
faults should emerge as exceptions. |
|
28781 | 109 |
|
110 |
By enumerating \emph{multiple results}, a tactic can easily express |
|
111 |
the potential outcome of an internal search process. There are also |
|
112 |
combinators for building proof tools that involve search |
|
113 |
systematically, see also \secref{sec:tacticals}. |
|
114 |
||
34930 | 115 |
\medskip As explained before, a goal state essentially consists of a |
116 |
list of subgoals that imply the main goal (conclusion). Tactics may |
|
117 |
operate on all subgoals or on a particularly specified subgoal, but |
|
118 |
must not change the main conclusion (apart from instantiating |
|
119 |
schematic goal variables). |
|
18537 | 120 |
|
28781 | 121 |
Tactics with explicit \emph{subgoal addressing} are of the form |
122 |
@{text "int \<rightarrow> tactic"} and may be applied to a particular subgoal |
|
123 |
(counting from 1). If the subgoal number is out of range, the |
|
124 |
tactic should fail with an empty result sequence, but must not raise |
|
125 |
an exception! |
|
126 |
||
127 |
Operating on a particular subgoal means to replace it by an interval |
|
128 |
of zero or more subgoals in the same place; other subgoals must not |
|
129 |
be affected, apart from instantiating schematic variables ranging |
|
130 |
over the whole goal state. |
|
131 |
||
132 |
A common pattern of composing tactics with subgoal addressing is to |
|
133 |
try the first one, and then the second one only if the subgoal has |
|
134 |
not been solved yet. Special care is required here to avoid bumping |
|
28782 | 135 |
into unrelated subgoals that happen to come after the original |
136 |
subgoal. Assuming that there is only a single initial subgoal is a |
|
137 |
very common error when implementing tactics! |
|
138 |
||
139 |
Tactics with internal subgoal addressing should expose the subgoal |
|
140 |
index as @{text "int"} argument in full generality; a hardwired |
|
34930 | 141 |
subgoal 1 is not acceptable. |
28781 | 142 |
|
143 |
\medskip The main well-formedness conditions for proper tactics are |
|
144 |
summarized as follows. |
|
145 |
||
146 |
\begin{itemize} |
|
147 |
||
148 |
\item General tactic failure is indicated by an empty result, only |
|
149 |
serious faults may produce an exception. |
|
150 |
||
151 |
\item The main conclusion must not be changed, apart from |
|
152 |
instantiating schematic variables. |
|
153 |
||
154 |
\item A tactic operates either uniformly on all subgoals, or |
|
155 |
specifically on a selected subgoal (without bumping into unrelated |
|
156 |
subgoals). |
|
157 |
||
158 |
\item Range errors in subgoal addressing produce an empty result. |
|
159 |
||
160 |
\end{itemize} |
|
28782 | 161 |
|
162 |
Some of these conditions are checked by higher-level goal |
|
34930 | 163 |
infrastructure (\secref{sec:struct-goals}); others are not checked |
28782 | 164 |
explicitly, and violating them merely results in ill-behaved tactics |
165 |
experienced by the user (e.g.\ tactics that insist in being |
|
34930 | 166 |
applicable only to singleton goals, or prevent composition via |
167 |
standard tacticals). |
|
28782 | 168 |
*} |
169 |
||
170 |
text %mlref {* |
|
171 |
\begin{mldecls} |
|
172 |
@{index_ML_type tactic: "thm -> thm Seq.seq"} \\ |
|
28783 | 173 |
@{index_ML no_tac: tactic} \\ |
174 |
@{index_ML all_tac: tactic} \\ |
|
175 |
@{index_ML print_tac: "string -> tactic"} \\[1ex] |
|
176 |
@{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex] |
|
28782 | 177 |
@{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\ |
178 |
@{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\ |
|
179 |
\end{mldecls} |
|
180 |
||
181 |
\begin{description} |
|
182 |
||
39864 | 183 |
\item Type @{ML_type tactic} represents tactics. The |
184 |
well-formedness conditions described above need to be observed. See |
|
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
39864
diff
changeset
|
185 |
also @{file "~~/src/Pure/General/seq.ML"} for the underlying |
39864 | 186 |
implementation of lazy sequences. |
28782 | 187 |
|
39864 | 188 |
\item Type @{ML_type "int -> tactic"} represents tactics with |
189 |
explicit subgoal addressing, with well-formedness conditions as |
|
190 |
described above. |
|
28782 | 191 |
|
28783 | 192 |
\item @{ML no_tac} is a tactic that always fails, returning the |
193 |
empty sequence. |
|
194 |
||
195 |
\item @{ML all_tac} is a tactic that always succeeds, returning a |
|
196 |
singleton sequence with unchanged goal state. |
|
197 |
||
198 |
\item @{ML print_tac}~@{text "message"} is like @{ML all_tac}, but |
|
199 |
prints a message together with the goal state on the tracing |
|
200 |
channel. |
|
201 |
||
28782 | 202 |
\item @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule |
203 |
into a tactic with unique result. Exception @{ML THM} is considered |
|
204 |
a regular tactic failure and produces an empty result; other |
|
205 |
exceptions are passed through. |
|
206 |
||
207 |
\item @{ML SUBGOAL}~@{text "(fn (subgoal, i) => tactic)"} is the |
|
28783 | 208 |
most basic form to produce a tactic with subgoal addressing. The |
28782 | 209 |
given abstraction over the subgoal term and subgoal number allows to |
210 |
peek at the relevant information of the full goal state. The |
|
211 |
subgoal range is checked as required above. |
|
212 |
||
213 |
\item @{ML CSUBGOAL} is similar to @{ML SUBGOAL}, but passes the |
|
28783 | 214 |
subgoal as @{ML_type cterm} instead of raw @{ML_type term}. This |
28782 | 215 |
avoids expensive re-certification in situations where the subgoal is |
216 |
used directly for primitive inferences. |
|
217 |
||
218 |
\end{description} |
|
28781 | 219 |
*} |
18537 | 220 |
|
221 |
||
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
222 |
subsection {* Resolution and assumption tactics \label{sec:resolve-assume-tac} *} |
28783 | 223 |
|
224 |
text {* \emph{Resolution} is the most basic mechanism for refining a |
|
225 |
subgoal using a theorem as object-level rule. |
|
226 |
\emph{Elim-resolution} is particularly suited for elimination rules: |
|
227 |
it resolves with a rule, proves its first premise by assumption, and |
|
228 |
finally deletes that assumption from any new subgoals. |
|
229 |
\emph{Destruct-resolution} is like elim-resolution, but the given |
|
230 |
destruction rules are first turned into canonical elimination |
|
231 |
format. \emph{Forward-resolution} is like destruct-resolution, but |
|
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
232 |
without deleting the selected assumption. The @{text "r/e/d/f"} |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
233 |
naming convention is maintained for several different kinds of |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
234 |
resolution rules and tactics. |
28783 | 235 |
|
236 |
Assumption tactics close a subgoal by unifying some of its premises |
|
237 |
against its conclusion. |
|
238 |
||
239 |
\medskip All the tactics in this section operate on a subgoal |
|
240 |
designated by a positive integer. Other subgoals might be affected |
|
241 |
indirectly, due to instantiation of schematic variables. |
|
242 |
||
243 |
There are various sources of non-determinism, the tactic result |
|
244 |
sequence enumerates all possibilities of the following choices (if |
|
245 |
applicable): |
|
246 |
||
247 |
\begin{enumerate} |
|
248 |
||
249 |
\item selecting one of the rules given as argument to the tactic; |
|
250 |
||
251 |
\item selecting a subgoal premise to eliminate, unifying it against |
|
252 |
the first premise of the rule; |
|
253 |
||
254 |
\item unifying the conclusion of the subgoal to the conclusion of |
|
255 |
the rule. |
|
256 |
||
257 |
\end{enumerate} |
|
258 |
||
259 |
Recall that higher-order unification may produce multiple results |
|
260 |
that are enumerated here. |
|
261 |
*} |
|
262 |
||
263 |
text %mlref {* |
|
264 |
\begin{mldecls} |
|
265 |
@{index_ML resolve_tac: "thm list -> int -> tactic"} \\ |
|
266 |
@{index_ML eresolve_tac: "thm list -> int -> tactic"} \\ |
|
267 |
@{index_ML dresolve_tac: "thm list -> int -> tactic"} \\ |
|
268 |
@{index_ML forward_tac: "thm list -> int -> tactic"} \\[1ex] |
|
269 |
@{index_ML assume_tac: "int -> tactic"} \\ |
|
270 |
@{index_ML eq_assume_tac: "int -> tactic"} \\[1ex] |
|
271 |
@{index_ML match_tac: "thm list -> int -> tactic"} \\ |
|
272 |
@{index_ML ematch_tac: "thm list -> int -> tactic"} \\ |
|
273 |
@{index_ML dmatch_tac: "thm list -> int -> tactic"} \\ |
|
274 |
\end{mldecls} |
|
275 |
||
276 |
\begin{description} |
|
277 |
||
278 |
\item @{ML resolve_tac}~@{text "thms i"} refines the goal state |
|
279 |
using the given theorems, which should normally be introduction |
|
280 |
rules. The tactic resolves a rule's conclusion with subgoal @{text |
|
281 |
i}, replacing it by the corresponding versions of the rule's |
|
282 |
premises. |
|
283 |
||
284 |
\item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution |
|
285 |
with the given theorems, which should normally be elimination rules. |
|
286 |
||
287 |
\item @{ML dresolve_tac}~@{text "thms i"} performs |
|
288 |
destruct-resolution with the given theorems, which should normally |
|
289 |
be destruction rules. This replaces an assumption by the result of |
|
290 |
applying one of the rules. |
|
291 |
||
292 |
\item @{ML forward_tac} is like @{ML dresolve_tac} except that the |
|
293 |
selected assumption is not deleted. It applies a rule to an |
|
294 |
assumption, adding the result as a new assumption. |
|
295 |
||
296 |
\item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i} |
|
297 |
by assumption (modulo higher-order unification). |
|
298 |
||
299 |
\item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks |
|
300 |
only for immediate @{text "\<alpha>"}-convertibility instead of using |
|
301 |
unification. It succeeds (with a unique next state) if one of the |
|
302 |
assumptions is equal to the subgoal's conclusion. Since it does not |
|
303 |
instantiate variables, it cannot make other subgoals unprovable. |
|
304 |
||
305 |
\item @{ML match_tac}, @{ML ematch_tac}, and @{ML dmatch_tac} are |
|
306 |
similar to @{ML resolve_tac}, @{ML eresolve_tac}, and @{ML |
|
307 |
dresolve_tac}, respectively, but do not instantiate schematic |
|
308 |
variables in the goal state. |
|
309 |
||
310 |
Flexible subgoals are not updated at will, but are left alone. |
|
311 |
Strictly speaking, matching means to treat the unknowns in the goal |
|
312 |
state as constants; these tactics merely discard unifiers that would |
|
313 |
update the goal state. |
|
314 |
||
315 |
\end{description} |
|
316 |
*} |
|
317 |
||
318 |
||
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
319 |
subsection {* Explicit instantiation within a subgoal context *} |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
320 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
321 |
text {* The main resolution tactics (\secref{sec:resolve-assume-tac}) |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
322 |
use higher-order unification, which works well in many practical |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
323 |
situations despite its daunting theoretical properties. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
324 |
Nonetheless, there are important problem classes where unguided |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
325 |
higher-order unification is not so useful. This typically involves |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
326 |
rules like universal elimination, existential introduction, or |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
327 |
equational substitution. Here the unification problem involves |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
328 |
fully flexible @{text "?P ?x"} schemes, which are hard to manage |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
329 |
without further hints. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
330 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
331 |
By providing a (small) rigid term for @{text "?x"} explicitly, the |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
332 |
remaining unification problem is to assign a (large) term to @{text |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
333 |
"?P"}, according to the shape of the given subgoal. This is |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
334 |
sufficiently well-behaved in most practical situations. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
335 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
336 |
\medskip Isabelle provides separate versions of the standard @{text |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
337 |
"r/e/d/f"} resolution tactics that allow to provide explicit |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
338 |
instantiations of unknowns of the given rule, wrt.\ terms that refer |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
339 |
to the implicit context of the selected subgoal. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
340 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
341 |
An instantiation consists of a list of pairs of the form @{text |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
342 |
"(?x, t)"}, where @{text ?x} is a schematic variable occurring in |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
343 |
the given rule, and @{text t} is a term from the current proof |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
344 |
context, augmented by the local goal parameters of the selected |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
345 |
subgoal; cf.\ the @{text "focus"} operation described in |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
346 |
\secref{sec:variables}. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
347 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
348 |
Entering the syntactic context of a subgoal is a brittle operation, |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
349 |
because its exact form is somewhat accidental, and the choice of |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
350 |
bound variable names depends on the presence of other local and |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
351 |
global names. Explicit renaming of subgoal parameters prior to |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
352 |
explicit instantiation might help to achieve a bit more robustness. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
353 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
354 |
Type instantiations may be given as well, via pairs like @{text |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
355 |
"(?'a, \<tau>)"}. Type instantiations are distinguished from term |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
356 |
instantiations by the syntactic form of the schematic variable. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
357 |
Types are instantiated before terms are. Since term instantiation |
34930 | 358 |
already performs simple type-inference, so explicit type |
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
359 |
instantiations are seldom necessary. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
360 |
*} |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
361 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
362 |
text %mlref {* |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
363 |
\begin{mldecls} |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
364 |
@{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
365 |
@{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
366 |
@{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
367 |
@{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\[1ex] |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
368 |
@{index_ML rename_tac: "string list -> int -> tactic"} \\ |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
369 |
\end{mldecls} |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
370 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
371 |
\begin{description} |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
372 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
373 |
\item @{ML res_inst_tac}~@{text "ctxt insts thm i"} instantiates the |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
374 |
rule @{text thm} with the instantiations @{text insts}, as described |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
375 |
above, and then performs resolution on subgoal @{text i}. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
376 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
377 |
\item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
378 |
elim-resolution. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
379 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
380 |
\item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
381 |
destruct-resolution. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
382 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
383 |
\item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
384 |
the selected assumption is not deleted. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
385 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
386 |
\item @{ML rename_tac}~@{text "names i"} renames the innermost |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
387 |
parameters of subgoal @{text i} according to the provided @{text |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
388 |
names} (which need to be distinct indentifiers). |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
389 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
390 |
\end{description} |
34930 | 391 |
|
392 |
For historical reasons, the above instantiation tactics take |
|
393 |
unparsed string arguments, which makes them hard to use in general |
|
394 |
ML code. The slightly more advanced @{ML Subgoal.FOCUS} combinator |
|
395 |
of \secref{sec:struct-goals} allows to refer to internal goal |
|
396 |
structure with explicit context management. |
|
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
397 |
*} |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
398 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
399 |
|
28781 | 400 |
section {* Tacticals \label{sec:tacticals} *} |
18537 | 401 |
|
46258 | 402 |
text {* A \emph{tactical} is a functional combinator for building up |
403 |
complex tactics from simpler ones. Common tacticals perform |
|
404 |
sequential composition, disjunctive choice, iteration, or goal |
|
405 |
addressing. Various search strategies may be expressed via |
|
406 |
tacticals. |
|
407 |
||
408 |
\medskip The chapter on tacticals in old \cite{isabelle-ref} is |
|
409 |
still applicable for further details. *} |
|
410 |
||
411 |
||
412 |
subsection {* Combining tactics *} |
|
413 |
||
414 |
text {* Sequential composition and alternative choices are the most |
|
415 |
basic ways to combine tactics, similarly to ``@{verbatim ","}'' and |
|
416 |
``@{verbatim "|"}'' in Isar method notation. This corresponds to |
|
417 |
@{text "THEN"} and @{text "ORELSE"} in ML, but there are further |
|
418 |
possibilities for fine-tuning alternation of tactics such as @{text |
|
419 |
"APPEND"}. Further details become visible in ML due to explicit |
|
420 |
subgoal addressing. *} |
|
421 |
||
422 |
text %mlref {* |
|
423 |
\begin{mldecls} |
|
424 |
@{index_ML "op THEN": "tactic * tactic -> tactic"} \\ |
|
425 |
@{index_ML "op ORELSE": "tactic * tactic -> tactic"} \\ |
|
426 |
@{index_ML "op APPEND": "tactic * tactic -> tactic"} \\ |
|
427 |
@{index_ML "EVERY": "tactic list -> tactic"} \\ |
|
428 |
@{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex] |
|
429 |
||
430 |
@{index_ML "op THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ |
|
431 |
@{index_ML "op ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ |
|
432 |
@{index_ML "op APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ |
|
433 |
@{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\ |
|
434 |
@{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\ |
|
435 |
@{index_ML "EVERY1": "(int -> tactic) list -> tactic"} \\ |
|
436 |
@{index_ML "FIRST1": "(int -> tactic) list -> tactic"} \\[0.5ex] |
|
437 |
\end{mldecls} |
|
438 |
||
439 |
\begin{description} |
|
18537 | 440 |
|
46258 | 441 |
\item @{text "tac\<^sub>1 THEN tac\<^sub>2"} is the sequential composition of |
442 |
@{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a proof state, it |
|
443 |
returns all states reachable in two steps by applying @{text "tac\<^sub>1"} |
|
444 |
followed by @{text "tac\<^sub>2"}. First, it applies @{text "tac\<^sub>1"} to the |
|
445 |
proof state, getting a sequence of possible next states; then, it |
|
446 |
applies @{text "tac\<^sub>2"} to each of these and concatenates the results |
|
447 |
to produce again one flat sequence of states. |
|
448 |
||
449 |
\item @{text "tac\<^sub>1 ORELSE tac\<^sub>2"} makes a choice between @{text |
|
450 |
"tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a state, it tries @{text |
|
451 |
"tac\<^sub>1"} and returns the result if non-empty; if @{text "tac\<^sub>1"} fails |
|
452 |
then it uses @{text "tac\<^sub>2"}. This is a deterministic choice: if |
|
453 |
@{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded from the |
|
454 |
result. |
|
455 |
||
456 |
\item @{text "tac\<^sub>1 APPEND tac\<^sub>2"} concatenates the possible results |
|
457 |
of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Unlike @{text "ORELSE"} there |
|
458 |
is \emph{no commitment} to either tactic, so @{text "APPEND"} helps |
|
459 |
to avoid incompleteness during search, at the cost of potential |
|
460 |
inefficiencies. |
|
39852 | 461 |
|
46258 | 462 |
\item @{text "EVERY [tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text "tac\<^sub>1 THEN |
463 |
\<dots> THEN tac\<^sub>n"}. Note that @{text "EVERY []"} is the same as @{ML |
|
464 |
all_tac}: it always succeeds. |
|
465 |
||
466 |
\item @{text "FIRST [tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text "tac\<^sub>1 |
|
467 |
ORELSE \<dots> ORELSE tac\<^sub>n"}. Note that @{text "FIRST []"} is the same as |
|
468 |
@{ML no_tac}: it always fails. |
|
469 |
||
470 |
\item @{text "THEN'"}, @{text "ORELSE'"}, and @{text "APPEND'"} are |
|
471 |
lifted versions of @{text "THEN"}, @{text "ORELSE"}, and @{text |
|
472 |
"APPEND"}, for tactics with explicit subgoal addressing. This means |
|
473 |
@{text "(tac\<^sub>1 THEN' tac\<^sub>2) i"} is the same as @{text "(tac\<^sub>1 i THEN |
|
474 |
tac\<^sub>2 i)"} etc. |
|
475 |
||
476 |
\item @{text "EVERY'"} and @{text "FIRST'"} are lifted versions of |
|
477 |
@{text "EVERY'"} and @{text "FIRST'"}, for tactics with explicit |
|
478 |
subgoal addressing. |
|
479 |
||
480 |
\item @{text "EVERY1"} and @{text "FIRST1"} are convenience versions |
|
481 |
of @{text "EVERY'"} and @{text "FIRST'"}, applied to subgoal 1. |
|
482 |
||
483 |
\end{description} |
|
484 |
*} |
|
30272 | 485 |
|
46259 | 486 |
|
487 |
subsection {* Repetition tacticals *} |
|
488 |
||
489 |
text {* These tacticals provide further control over repetition of |
|
490 |
tactics, beyond the stylized forms of ``@{verbatim "?"}'' and |
|
491 |
``@{verbatim "+"}'' in Isar method expressions. *} |
|
492 |
||
493 |
text %mlref {* |
|
494 |
\begin{mldecls} |
|
495 |
@{index_ML "TRY": "tactic -> tactic"} \\ |
|
496 |
@{index_ML "REPEAT_DETERM": "tactic -> tactic"} \\ |
|
497 |
@{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\ |
|
498 |
@{index_ML "REPEAT": "tactic -> tactic"} \\ |
|
499 |
@{index_ML "REPEAT1": "tactic -> tactic"} \\ |
|
500 |
@{index_ML "DETERM_UNTIL": "(thm -> bool) -> tactic -> tactic"} \\ |
|
501 |
\end{mldecls} |
|
502 |
||
503 |
\begin{description} |
|
504 |
||
505 |
\item @{ML TRY}~@{text "tac"} applies @{text "tac"} to the proof |
|
506 |
state and returns the resulting sequence, if non-empty; otherwise it |
|
507 |
returns the original state. Thus, it applies @{text "tac"} at most |
|
508 |
once. |
|
509 |
||
510 |
\item @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the |
|
511 |
proof state and, recursively, to the head of the resulting sequence. |
|
512 |
It returns the first state to make @{text "tac"} fail. It is |
|
513 |
deterministic, discarding alternative outcomes. |
|
514 |
||
515 |
\item @{ML REPEAT_DETERM_N}~@{text "n tac"} is like @{ML |
|
516 |
REPEAT_DETERM}~@{text "tac"} but the number of repetitions is bound |
|
517 |
by @{text "n"} (where @{ML "~1"} means @{text "\<infinity>"}). |
|
518 |
||
519 |
\item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the proof |
|
520 |
state and, recursively, to each element of the resulting sequence. |
|
521 |
The resulting sequence consists of those states that make @{text |
|
522 |
"tac"} fail. Thus, it applies @{text "tac"} as many times as |
|
523 |
possible (including zero times), and allows backtracking over each |
|
524 |
invocation of @{text "tac"}. @{ML REPEAT} is more general than @{ML |
|
525 |
REPEAT_DETERM}, but requires more space. |
|
526 |
||
527 |
\item @{ML REPEAT1}~@{text "tac"} is like @{ML REPEAT}~@{text "tac"} |
|
528 |
but it always applies @{text "tac"} at least once, failing if this |
|
529 |
is impossible. |
|
530 |
||
531 |
\item @{ML DETERM_UNTIL}~@{text "P tac"} applies @{text "tac"} to |
|
532 |
the proof state and, recursively, to the head of the resulting |
|
533 |
sequence, until the predicate @{text "P"} (applied on the proof |
|
534 |
state) yields @{ML true}. It fails if @{text "tac"} fails on any of |
|
535 |
the intermediate states. It is deterministic, discarding alternative |
|
536 |
outcomes. |
|
537 |
||
538 |
\end{description} |
|
539 |
*} |
|
540 |
||
541 |
||
542 |
subsection {* Identities for tacticals *} |
|
543 |
||
544 |
text %mlref {* |
|
545 |
\begin{mldecls} |
|
546 |
@{index_ML all_tac: tactic} \\ |
|
547 |
@{index_ML no_tac: tactic} \\ |
|
548 |
\end{mldecls} |
|
549 |
||
550 |
\begin{description} |
|
551 |
||
552 |
\item @{ML all_tac} maps any proof state to the one-element sequence |
|
553 |
containing that state. Thus, it succeeds for all states. It is the |
|
554 |
identity element of the tactical @{ML "op THEN"}. |
|
555 |
||
556 |
\item @{ML no_tac} maps any proof state to the empty sequence. Thus |
|
557 |
it succeeds for no state. It is the identity element of |
|
558 |
@{ML "op ORELSE"} and @{ML "op APPEND"}. Also, it is a zero element |
|
559 |
for @{ML "op THEN"}, which means that @{text "tac THEN"}~@{ML |
|
560 |
no_tac} is equivalent to @{ML no_tac}. |
|
561 |
||
562 |
\end{description} |
|
563 |
*} |
|
564 |
||
565 |
text %mlex {* The following examples illustrate how these primitive |
|
566 |
tactics can be used to imitate existing combinators like @{ML TRY} |
|
567 |
or @{ML REPEAT} (ignoring some further implementation tricks): |
|
568 |
*} |
|
569 |
||
570 |
ML {* |
|
571 |
fun TRY tac = tac ORELSE all_tac; |
|
572 |
fun REPEAT tac st = ((tac THEN REPEAT tac) ORELSE all_tac) st; |
|
573 |
*} |
|
574 |
||
575 |
text {* If @{text "tac"} can return multiple outcomes then so can @{ML |
|
576 |
REPEAT}~@{text "tac"}. @{ML REPEAT} uses @{ML "op ORELSE"} and not |
|
577 |
@{ML "op APPEND"}, it applies @{text "tac"} as many times as |
|
578 |
possible in each outcome. |
|
579 |
||
580 |
\begin{warn} |
|
581 |
Note @{ML REPEAT}'s explicit abstraction over the proof state. |
|
582 |
Recursive tacticals must be coded in this awkward fashion to avoid |
|
583 |
infinite recursion. With the following definition, @{ML |
|
584 |
REPEAT}~@{text "tac"} would loop due to the eager evaluation |
|
585 |
strategy of ML: |
|
586 |
\end{warn} |
|
587 |
*} |
|
588 |
||
589 |
ML {* |
|
590 |
fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac; (*BAD!*) |
|
591 |
*} |
|
592 |
||
18537 | 593 |
end |