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