author | wenzelm |
Tue, 31 Mar 2015 22:31:05 +0200 | |
changeset 59886 | e0dc738eb08c |
parent 59780 | 23b67731f4f0 |
child 59902 | 6afbe5a99139 |
permissions | -rw-r--r-- |
29755 | 1 |
theory Tactic |
2 |
imports Base |
|
3 |
begin |
|
18537 | 4 |
|
58618 | 5 |
chapter \<open>Tactical reasoning\<close> |
18537 | 6 |
|
58618 | 7 |
text \<open>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 |
|
58618 | 13 |
"tactical"} is a combinator for composing tactics.\<close> |
18537 | 14 |
|
15 |
||
58618 | 16 |
section \<open>Goals \label{sec:tactical-goals}\<close> |
18537 | 17 |
|
58618 | 18 |
text \<open> |
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 |
\[ |
|
52456 | 56 |
\infer[@{text "(protect n)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}} |
57 |
\] |
|
58 |
\[ |
|
59 |
\infer[@{text "(conclude)"}]{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> C"}}{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> #C"}} |
|
18537 | 60 |
\] |
58618 | 61 |
\<close> |
18537 | 62 |
|
58618 | 63 |
text %mlref \<open> |
18537 | 64 |
\begin{mldecls} |
65 |
@{index_ML Goal.init: "cterm -> thm"} \\ |
|
32201
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30272
diff
changeset
|
66 |
@{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\ |
52456 | 67 |
@{index_ML Goal.protect: "int -> thm -> thm"} \\ |
18537 | 68 |
@{index_ML Goal.conclude: "thm -> thm"} \\ |
69 |
\end{mldecls} |
|
70 |
||
71 |
\begin{description} |
|
72 |
||
20474 | 73 |
\item @{ML "Goal.init"}~@{text C} initializes a tactical goal from |
74 |
the well-formed proposition @{text C}. |
|
18537 | 75 |
|
32201
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30272
diff
changeset
|
76 |
\item @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem |
20474 | 77 |
@{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
|
78 |
result by removing the goal protection. The context is only |
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30272
diff
changeset
|
79 |
required for printing error messages. |
18537 | 80 |
|
52456 | 81 |
\item @{ML "Goal.protect"}~@{text "n thm"} protects the statement |
82 |
of theorem @{text "thm"}. The parameter @{text n} indicates the |
|
83 |
number of premises to be retained. |
|
18537 | 84 |
|
20474 | 85 |
\item @{ML "Goal.conclude"}~@{text "thm"} removes the goal |
86 |
protection, even if there are pending subgoals. |
|
18537 | 87 |
|
88 |
\end{description} |
|
58618 | 89 |
\<close> |
18537 | 90 |
|
91 |
||
58618 | 92 |
section \<open>Tactics\label{sec:tactics}\<close> |
18537 | 93 |
|
58618 | 94 |
text \<open>A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that |
28781 | 95 |
maps a given goal state (represented as a theorem, cf.\ |
96 |
\secref{sec:tactical-goals}) to a lazy sequence of potential |
|
97 |
successor states. The underlying sequence implementation is lazy |
|
98 |
both in head and tail, and is purely functional in \emph{not} |
|
99 |
supporting memoing.\footnote{The lack of memoing and the strict |
|
57421 | 100 |
nature of ML requires some care when working with low-level |
28781 | 101 |
sequence operations, to avoid duplicate or premature evaluation of |
34930 | 102 |
results. It also means that modified runtime behavior, such as |
103 |
timeout, is very hard to achieve for general tactics.} |
|
18537 | 104 |
|
28781 | 105 |
An \emph{empty result sequence} means that the tactic has failed: in |
34930 | 106 |
a compound tactic expression other tactics might be tried instead, |
28781 | 107 |
or the whole refinement step might fail outright, producing a |
34930 | 108 |
toplevel error message in the end. When implementing tactics from |
109 |
scratch, one should take care to observe the basic protocol of |
|
110 |
mapping regular error conditions to an empty result; only serious |
|
111 |
faults should emerge as exceptions. |
|
28781 | 112 |
|
113 |
By enumerating \emph{multiple results}, a tactic can easily express |
|
114 |
the potential outcome of an internal search process. There are also |
|
115 |
combinators for building proof tools that involve search |
|
116 |
systematically, see also \secref{sec:tacticals}. |
|
117 |
||
34930 | 118 |
\medskip As explained before, a goal state essentially consists of a |
119 |
list of subgoals that imply the main goal (conclusion). Tactics may |
|
120 |
operate on all subgoals or on a particularly specified subgoal, but |
|
121 |
must not change the main conclusion (apart from instantiating |
|
122 |
schematic goal variables). |
|
18537 | 123 |
|
28781 | 124 |
Tactics with explicit \emph{subgoal addressing} are of the form |
125 |
@{text "int \<rightarrow> tactic"} and may be applied to a particular subgoal |
|
126 |
(counting from 1). If the subgoal number is out of range, the |
|
127 |
tactic should fail with an empty result sequence, but must not raise |
|
128 |
an exception! |
|
129 |
||
130 |
Operating on a particular subgoal means to replace it by an interval |
|
131 |
of zero or more subgoals in the same place; other subgoals must not |
|
132 |
be affected, apart from instantiating schematic variables ranging |
|
133 |
over the whole goal state. |
|
134 |
||
135 |
A common pattern of composing tactics with subgoal addressing is to |
|
136 |
try the first one, and then the second one only if the subgoal has |
|
137 |
not been solved yet. Special care is required here to avoid bumping |
|
28782 | 138 |
into unrelated subgoals that happen to come after the original |
139 |
subgoal. Assuming that there is only a single initial subgoal is a |
|
140 |
very common error when implementing tactics! |
|
141 |
||
142 |
Tactics with internal subgoal addressing should expose the subgoal |
|
143 |
index as @{text "int"} argument in full generality; a hardwired |
|
34930 | 144 |
subgoal 1 is not acceptable. |
28781 | 145 |
|
146 |
\medskip The main well-formedness conditions for proper tactics are |
|
147 |
summarized as follows. |
|
148 |
||
149 |
\begin{itemize} |
|
150 |
||
151 |
\item General tactic failure is indicated by an empty result, only |
|
152 |
serious faults may produce an exception. |
|
153 |
||
154 |
\item The main conclusion must not be changed, apart from |
|
155 |
instantiating schematic variables. |
|
156 |
||
157 |
\item A tactic operates either uniformly on all subgoals, or |
|
158 |
specifically on a selected subgoal (without bumping into unrelated |
|
159 |
subgoals). |
|
160 |
||
161 |
\item Range errors in subgoal addressing produce an empty result. |
|
162 |
||
163 |
\end{itemize} |
|
28782 | 164 |
|
165 |
Some of these conditions are checked by higher-level goal |
|
34930 | 166 |
infrastructure (\secref{sec:struct-goals}); others are not checked |
28782 | 167 |
explicitly, and violating them merely results in ill-behaved tactics |
168 |
experienced by the user (e.g.\ tactics that insist in being |
|
34930 | 169 |
applicable only to singleton goals, or prevent composition via |
46260 | 170 |
standard tacticals such as @{ML REPEAT}). |
58618 | 171 |
\<close> |
28782 | 172 |
|
58618 | 173 |
text %mlref \<open> |
28782 | 174 |
\begin{mldecls} |
175 |
@{index_ML_type tactic: "thm -> thm Seq.seq"} \\ |
|
28783 | 176 |
@{index_ML no_tac: tactic} \\ |
177 |
@{index_ML all_tac: tactic} \\ |
|
56491 | 178 |
@{index_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex] |
28783 | 179 |
@{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex] |
28782 | 180 |
@{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\ |
181 |
@{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\ |
|
52463 | 182 |
@{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\ |
183 |
@{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\ |
|
28782 | 184 |
\end{mldecls} |
185 |
||
186 |
\begin{description} |
|
187 |
||
39864 | 188 |
\item Type @{ML_type tactic} represents tactics. The |
189 |
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
|
190 |
also @{file "~~/src/Pure/General/seq.ML"} for the underlying |
39864 | 191 |
implementation of lazy sequences. |
28782 | 192 |
|
39864 | 193 |
\item Type @{ML_type "int -> tactic"} represents tactics with |
194 |
explicit subgoal addressing, with well-formedness conditions as |
|
195 |
described above. |
|
28782 | 196 |
|
28783 | 197 |
\item @{ML no_tac} is a tactic that always fails, returning the |
198 |
empty sequence. |
|
199 |
||
200 |
\item @{ML all_tac} is a tactic that always succeeds, returning a |
|
201 |
singleton sequence with unchanged goal state. |
|
202 |
||
56491 | 203 |
\item @{ML print_tac}~@{text "ctxt message"} is like @{ML all_tac}, but |
28783 | 204 |
prints a message together with the goal state on the tracing |
205 |
channel. |
|
206 |
||
28782 | 207 |
\item @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule |
208 |
into a tactic with unique result. Exception @{ML THM} is considered |
|
209 |
a regular tactic failure and produces an empty result; other |
|
210 |
exceptions are passed through. |
|
211 |
||
212 |
\item @{ML SUBGOAL}~@{text "(fn (subgoal, i) => tactic)"} is the |
|
28783 | 213 |
most basic form to produce a tactic with subgoal addressing. The |
28782 | 214 |
given abstraction over the subgoal term and subgoal number allows to |
215 |
peek at the relevant information of the full goal state. The |
|
216 |
subgoal range is checked as required above. |
|
217 |
||
218 |
\item @{ML CSUBGOAL} is similar to @{ML SUBGOAL}, but passes the |
|
28783 | 219 |
subgoal as @{ML_type cterm} instead of raw @{ML_type term}. This |
28782 | 220 |
avoids expensive re-certification in situations where the subgoal is |
221 |
used directly for primitive inferences. |
|
222 |
||
52463 | 223 |
\item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the |
224 |
specified subgoal @{text "i"}. This rearranges subgoals and the |
|
225 |
main goal protection (\secref{sec:tactical-goals}), while retaining |
|
226 |
the syntactic context of the overall goal state (concerning |
|
227 |
schematic variables etc.). |
|
228 |
||
229 |
\item @{ML PREFER_GOAL}~@{text "tac i"} rearranges subgoals to put |
|
230 |
@{text "i"} in front. This is similar to @{ML SELECT_GOAL}, but |
|
231 |
without changing the main goal protection. |
|
232 |
||
28782 | 233 |
\end{description} |
58618 | 234 |
\<close> |
18537 | 235 |
|
236 |
||
58618 | 237 |
subsection \<open>Resolution and assumption tactics \label{sec:resolve-assume-tac}\<close> |
28783 | 238 |
|
58618 | 239 |
text \<open>\emph{Resolution} is the most basic mechanism for refining a |
28783 | 240 |
subgoal using a theorem as object-level rule. |
241 |
\emph{Elim-resolution} is particularly suited for elimination rules: |
|
242 |
it resolves with a rule, proves its first premise by assumption, and |
|
243 |
finally deletes that assumption from any new subgoals. |
|
244 |
\emph{Destruct-resolution} is like elim-resolution, but the given |
|
245 |
destruction rules are first turned into canonical elimination |
|
246 |
format. \emph{Forward-resolution} is like destruct-resolution, but |
|
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
247 |
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
|
248 |
naming convention is maintained for several different kinds of |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
249 |
resolution rules and tactics. |
28783 | 250 |
|
251 |
Assumption tactics close a subgoal by unifying some of its premises |
|
252 |
against its conclusion. |
|
253 |
||
254 |
\medskip All the tactics in this section operate on a subgoal |
|
255 |
designated by a positive integer. Other subgoals might be affected |
|
256 |
indirectly, due to instantiation of schematic variables. |
|
257 |
||
258 |
There are various sources of non-determinism, the tactic result |
|
259 |
sequence enumerates all possibilities of the following choices (if |
|
260 |
applicable): |
|
261 |
||
262 |
\begin{enumerate} |
|
263 |
||
264 |
\item selecting one of the rules given as argument to the tactic; |
|
265 |
||
266 |
\item selecting a subgoal premise to eliminate, unifying it against |
|
267 |
the first premise of the rule; |
|
268 |
||
269 |
\item unifying the conclusion of the subgoal to the conclusion of |
|
270 |
the rule. |
|
271 |
||
272 |
\end{enumerate} |
|
273 |
||
274 |
Recall that higher-order unification may produce multiple results |
|
275 |
that are enumerated here. |
|
58618 | 276 |
\<close> |
28783 | 277 |
|
58618 | 278 |
text %mlref \<open> |
28783 | 279 |
\begin{mldecls} |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
280 |
@{index_ML resolve_tac: "Proof.context -> thm list -> int -> tactic"} \\ |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
281 |
@{index_ML eresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\ |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
282 |
@{index_ML dresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\ |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
283 |
@{index_ML forward_tac: "Proof.context -> thm list -> int -> tactic"} \\ |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
284 |
@{index_ML biresolve_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\[1ex] |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
285 |
@{index_ML assume_tac: "Proof.context -> int -> tactic"} \\ |
28783 | 286 |
@{index_ML eq_assume_tac: "int -> tactic"} \\[1ex] |
58957 | 287 |
@{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\ |
288 |
@{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\ |
|
289 |
@{index_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\ |
|
290 |
@{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\ |
|
28783 | 291 |
\end{mldecls} |
292 |
||
293 |
\begin{description} |
|
294 |
||
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
295 |
\item @{ML resolve_tac}~@{text "ctxt thms i"} refines the goal state |
28783 | 296 |
using the given theorems, which should normally be introduction |
297 |
rules. The tactic resolves a rule's conclusion with subgoal @{text |
|
298 |
i}, replacing it by the corresponding versions of the rule's |
|
299 |
premises. |
|
300 |
||
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
301 |
\item @{ML eresolve_tac}~@{text "ctxt thms i"} performs elim-resolution |
46278 | 302 |
with the given theorems, which are normally be elimination rules. |
303 |
||
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
304 |
Note that @{ML_text "eresolve_tac ctxt [asm_rl]"} is equivalent to @{ML_text |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
305 |
"assume_tac ctxt"}, which facilitates mixing of assumption steps with |
46278 | 306 |
genuine eliminations. |
28783 | 307 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
308 |
\item @{ML dresolve_tac}~@{text "ctxt thms i"} performs |
28783 | 309 |
destruct-resolution with the given theorems, which should normally |
310 |
be destruction rules. This replaces an assumption by the result of |
|
311 |
applying one of the rules. |
|
312 |
||
313 |
\item @{ML forward_tac} is like @{ML dresolve_tac} except that the |
|
314 |
selected assumption is not deleted. It applies a rule to an |
|
315 |
assumption, adding the result as a new assumption. |
|
316 |
||
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
317 |
\item @{ML biresolve_tac}~@{text "ctxt brls i"} refines the proof state |
50072 | 318 |
by resolution or elim-resolution on each rule, as indicated by its |
319 |
flag. It affects subgoal @{text "i"} of the proof state. |
|
320 |
||
321 |
For each pair @{text "(flag, rule)"}, it applies resolution if the |
|
322 |
flag is @{text "false"} and elim-resolution if the flag is @{text |
|
323 |
"true"}. A single tactic call handles a mixture of introduction and |
|
324 |
elimination rules, which is useful to organize the search process |
|
325 |
systematically in proof tools. |
|
326 |
||
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
327 |
\item @{ML assume_tac}~@{text "ctxt i"} attempts to solve subgoal @{text i} |
28783 | 328 |
by assumption (modulo higher-order unification). |
329 |
||
330 |
\item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks |
|
331 |
only for immediate @{text "\<alpha>"}-convertibility instead of using |
|
332 |
unification. It succeeds (with a unique next state) if one of the |
|
333 |
assumptions is equal to the subgoal's conclusion. Since it does not |
|
334 |
instantiate variables, it cannot make other subgoals unprovable. |
|
335 |
||
50072 | 336 |
\item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML |
337 |
bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac}, |
|
338 |
@{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do |
|
53096 | 339 |
not instantiate schematic variables in the goal state.% |
340 |
\footnote{Strictly speaking, matching means to treat the unknowns in the goal |
|
341 |
state as constants, but these tactics merely discard unifiers that would |
|
342 |
update the goal state. In rare situations (where the conclusion and |
|
343 |
goal state have flexible terms at the same position), the tactic |
|
344 |
will fail even though an acceptable unifier exists.} |
|
345 |
These tactics were written for a specific application within the classical reasoner. |
|
28783 | 346 |
|
347 |
Flexible subgoals are not updated at will, but are left alone. |
|
348 |
\end{description} |
|
58618 | 349 |
\<close> |
28783 | 350 |
|
351 |
||
58618 | 352 |
subsection \<open>Explicit instantiation within a subgoal context\<close> |
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
353 |
|
58618 | 354 |
text \<open>The main resolution tactics (\secref{sec:resolve-assume-tac}) |
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
355 |
use higher-order unification, which works well in many practical |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
356 |
situations despite its daunting theoretical properties. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
357 |
Nonetheless, there are important problem classes where unguided |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
358 |
higher-order unification is not so useful. This typically involves |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
359 |
rules like universal elimination, existential introduction, or |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
360 |
equational substitution. Here the unification problem involves |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
361 |
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
|
362 |
without further hints. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
363 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
364 |
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
|
365 |
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
|
366 |
"?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
|
367 |
sufficiently well-behaved in most practical situations. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
368 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
369 |
\medskip Isabelle provides separate versions of the standard @{text |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
370 |
"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
|
371 |
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
|
372 |
to the implicit context of the selected subgoal. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
373 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
374 |
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
|
375 |
"(?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
|
376 |
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
|
377 |
context, augmented by the local goal parameters of the selected |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
378 |
subgoal; cf.\ the @{text "focus"} operation described in |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
379 |
\secref{sec:variables}. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
380 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
381 |
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
|
382 |
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
|
383 |
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
|
384 |
global names. Explicit renaming of subgoal parameters prior to |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
385 |
explicit instantiation might help to achieve a bit more robustness. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
386 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
387 |
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
|
388 |
"(?'a, \<tau>)"}. Type instantiations are distinguished from term |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
389 |
instantiations by the syntactic form of the schematic variable. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
390 |
Types are instantiated before terms are. Since term instantiation |
34930 | 391 |
already performs simple type-inference, so explicit type |
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
392 |
instantiations are seldom necessary. |
58618 | 393 |
\<close> |
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
394 |
|
58618 | 395 |
text %mlref \<open> |
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
396 |
\begin{mldecls} |
59763 | 397 |
@{index_ML Rule_Insts.res_inst_tac: "Proof.context -> |
59780 | 398 |
((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> |
399 |
thm -> int -> tactic"} \\ |
|
59763 | 400 |
@{index_ML Rule_Insts.eres_inst_tac: "Proof.context -> |
59780 | 401 |
((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> |
402 |
thm -> int -> tactic"} \\ |
|
59763 | 403 |
@{index_ML Rule_Insts.dres_inst_tac: "Proof.context -> |
59780 | 404 |
((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> |
405 |
thm -> int -> tactic"} \\ |
|
59763 | 406 |
@{index_ML Rule_Insts.forw_inst_tac: "Proof.context -> |
59780 | 407 |
((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> |
408 |
thm -> int -> tactic"} \\ |
|
409 |
@{index_ML Rule_Insts.subgoal_tac: "Proof.context -> string -> |
|
410 |
(binding * string option * mixfix) list -> int -> tactic"} \\ |
|
411 |
@{index_ML Rule_Insts.thin_tac: "Proof.context -> string -> |
|
412 |
(binding * string option * mixfix) list -> int -> tactic"} \\ |
|
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
413 |
@{index_ML rename_tac: "string list -> int -> tactic"} \\ |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
414 |
\end{mldecls} |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
415 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
416 |
\begin{description} |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
417 |
|
59763 | 418 |
\item @{ML Rule_Insts.res_inst_tac}~@{text "ctxt insts thm i"} instantiates the |
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
419 |
rule @{text thm} with the instantiations @{text insts}, as described |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
420 |
above, and then performs resolution on subgoal @{text i}. |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
421 |
|
59763 | 422 |
\item @{ML Rule_Insts.eres_inst_tac} is like @{ML Rule_Insts.res_inst_tac}, |
423 |
but performs elim-resolution. |
|
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
424 |
|
59763 | 425 |
\item @{ML Rule_Insts.dres_inst_tac} is like @{ML Rule_Insts.res_inst_tac}, |
426 |
but performs destruct-resolution. |
|
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
427 |
|
59763 | 428 |
\item @{ML Rule_Insts.forw_inst_tac} is like @{ML Rule_Insts.dres_inst_tac} |
429 |
except that the selected assumption is not deleted. |
|
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
430 |
|
59763 | 431 |
\item @{ML Rule_Insts.subgoal_tac}~@{text "ctxt \<phi> i"} adds the proposition |
46271 | 432 |
@{text "\<phi>"} as local premise to subgoal @{text "i"}, and poses the |
433 |
same as a new subgoal @{text "i + 1"} (in the original context). |
|
434 |
||
59763 | 435 |
\item @{ML Rule_Insts.thin_tac}~@{text "ctxt \<phi> i"} deletes the specified |
46277 | 436 |
premise from subgoal @{text i}. Note that @{text \<phi>} may contain |
437 |
schematic variables, to abbreviate the intended proposition; the |
|
438 |
first matching subgoal premise will be deleted. Removing useless |
|
439 |
premises from a subgoal increases its readability and can make |
|
440 |
search tactics run faster. |
|
441 |
||
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
442 |
\item @{ML rename_tac}~@{text "names i"} renames the innermost |
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
443 |
parameters of subgoal @{text i} according to the provided @{text |
56579 | 444 |
names} (which need to be distinct identifiers). |
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
445 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
446 |
\end{description} |
34930 | 447 |
|
448 |
For historical reasons, the above instantiation tactics take |
|
449 |
unparsed string arguments, which makes them hard to use in general |
|
450 |
ML code. The slightly more advanced @{ML Subgoal.FOCUS} combinator |
|
451 |
of \secref{sec:struct-goals} allows to refer to internal goal |
|
452 |
structure with explicit context management. |
|
58618 | 453 |
\<close> |
28785
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
454 |
|
64163cddf3e6
added section "Explicit instantiation within a subgoal context";
wenzelm
parents:
28783
diff
changeset
|
455 |
|
58618 | 456 |
subsection \<open>Rearranging goal states\<close> |
46274 | 457 |
|
58618 | 458 |
text \<open>In rare situations there is a need to rearrange goal states: |
46274 | 459 |
either the overall collection of subgoals, or the local structure of |
460 |
a subgoal. Various administrative tactics allow to operate on the |
|
58618 | 461 |
concrete presentation these conceptual sets of formulae.\<close> |
46274 | 462 |
|
58618 | 463 |
text %mlref \<open> |
46274 | 464 |
\begin{mldecls} |
465 |
@{index_ML rotate_tac: "int -> int -> tactic"} \\ |
|
46276 | 466 |
@{index_ML distinct_subgoals_tac: tactic} \\ |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58618
diff
changeset
|
467 |
@{index_ML flexflex_tac: "Proof.context -> tactic"} \\ |
46274 | 468 |
\end{mldecls} |
469 |
||
470 |
\begin{description} |
|
471 |
||
472 |
\item @{ML rotate_tac}~@{text "n i"} rotates the premises of subgoal |
|
473 |
@{text i} by @{text n} positions: from right to left if @{text n} is |
|
474 |
positive, and from left to right if @{text n} is negative. |
|
475 |
||
46276 | 476 |
\item @{ML distinct_subgoals_tac} removes duplicate subgoals from a |
477 |
proof state. This is potentially inefficient. |
|
478 |
||
479 |
\item @{ML flexflex_tac} removes all flex-flex pairs from the proof |
|
480 |
state by applying the trivial unifier. This drastic step loses |
|
481 |
information. It is already part of the Isar infrastructure for |
|
482 |
facts resulting from goals, and rarely needs to be invoked manually. |
|
483 |
||
484 |
Flex-flex constraints arise from difficult cases of higher-order |
|
59763 | 485 |
unification. To prevent this, use @{ML Rule_Insts.res_inst_tac} to |
486 |
instantiate some variables in a rule. Normally flex-flex constraints |
|
487 |
can be ignored; they often disappear as unknowns get instantiated. |
|
46276 | 488 |
|
46274 | 489 |
\end{description} |
58618 | 490 |
\<close> |
46274 | 491 |
|
50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
492 |
|
58618 | 493 |
subsection \<open>Raw composition: resolution without lifting\<close> |
50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
494 |
|
58618 | 495 |
text \<open> |
50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
496 |
Raw composition of two rules means resolving them without prior |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
497 |
lifting or renaming of unknowns. This low-level operation, which |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
498 |
underlies the resolution tactics, may occasionally be useful for |
52467 | 499 |
special effects. Schematic variables are not renamed by default, so |
500 |
beware of clashes! |
|
58618 | 501 |
\<close> |
50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
502 |
|
58618 | 503 |
text %mlref \<open> |
50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
504 |
\begin{mldecls} |
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset
|
505 |
@{index_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\ |
52467 | 506 |
@{index_ML Drule.compose: "thm * int * thm -> thm"} \\ |
50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
507 |
@{index_ML_op COMP: "thm * thm -> thm"} \\ |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
508 |
\end{mldecls} |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
509 |
|
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
510 |
\begin{description} |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
511 |
|
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset
|
512 |
\item @{ML compose_tac}~@{text "ctxt (flag, rule, m) i"} refines subgoal |
50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
513 |
@{text "i"} using @{text "rule"}, without lifting. The @{text |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
514 |
"rule"} is taken to have the form @{text "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, where |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
515 |
@{text "\<psi>"} need not be atomic; thus @{text "m"} determines the |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
516 |
number of new subgoals. If @{text "flag"} is @{text "true"} then it |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
517 |
performs elim-resolution --- it solves the first premise of @{text |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
518 |
"rule"} by assumption and deletes that assumption. |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
519 |
|
52465 | 520 |
\item @{ML Drule.compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"}, |
50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
521 |
regarded as an atomic formula, to solve premise @{text "i"} of |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
522 |
@{text "thm\<^sub>2"}. Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text |
52467 | 523 |
"\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}. The unique @{text "s"} that |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52820
diff
changeset
|
524 |
unifies @{text "\<psi>"} and @{text "\<phi>\<^sub>i"} yields the theorem @{text "(\<phi>\<^sub>1 \<Longrightarrow> |
52467 | 525 |
\<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}. Multiple results are considered as |
526 |
error (exception @{ML THM}). |
|
50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
527 |
|
52467 | 528 |
\item @{text "thm\<^sub>1 COMP thm\<^sub>2"} is the same as @{text "Drule.compose |
529 |
(thm\<^sub>1, 1, thm\<^sub>2)"}. |
|
50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
530 |
|
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
531 |
\end{description} |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
532 |
|
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
533 |
\begin{warn} |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
534 |
These low-level operations are stepping outside the structure |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
535 |
imposed by regular rule resolution. Used without understanding of |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
536 |
the consequences, they may produce results that cause problems with |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
537 |
standard rules and tactics later on. |
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
538 |
\end{warn} |
58618 | 539 |
\<close> |
50074
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
540 |
|
0b02aaf7c7c5
some coverage of "resolution without lifting", which should be normally avoided;
wenzelm
parents:
50072
diff
changeset
|
541 |
|
58618 | 542 |
section \<open>Tacticals \label{sec:tacticals}\<close> |
18537 | 543 |
|
58618 | 544 |
text \<open>A \emph{tactical} is a functional combinator for building up |
46258 | 545 |
complex tactics from simpler ones. Common tacticals perform |
546 |
sequential composition, disjunctive choice, iteration, or goal |
|
547 |
addressing. Various search strategies may be expressed via |
|
548 |
tacticals. |
|
58618 | 549 |
\<close> |
46258 | 550 |
|
551 |
||
58618 | 552 |
subsection \<open>Combining tactics\<close> |
46258 | 553 |
|
58618 | 554 |
text \<open>Sequential composition and alternative choices are the most |
46258 | 555 |
basic ways to combine tactics, similarly to ``@{verbatim ","}'' and |
556 |
``@{verbatim "|"}'' in Isar method notation. This corresponds to |
|
46262 | 557 |
@{ML_op "THEN"} and @{ML_op "ORELSE"} in ML, but there are further |
558 |
possibilities for fine-tuning alternation of tactics such as @{ML_op |
|
46258 | 559 |
"APPEND"}. Further details become visible in ML due to explicit |
46262 | 560 |
subgoal addressing. |
58618 | 561 |
\<close> |
46258 | 562 |
|
58618 | 563 |
text %mlref \<open> |
46258 | 564 |
\begin{mldecls} |
46262 | 565 |
@{index_ML_op "THEN": "tactic * tactic -> tactic"} \\ |
566 |
@{index_ML_op "ORELSE": "tactic * tactic -> tactic"} \\ |
|
567 |
@{index_ML_op "APPEND": "tactic * tactic -> tactic"} \\ |
|
46258 | 568 |
@{index_ML "EVERY": "tactic list -> tactic"} \\ |
569 |
@{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex] |
|
570 |
||
46262 | 571 |
@{index_ML_op "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ |
572 |
@{index_ML_op "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ |
|
573 |
@{index_ML_op "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ |
|
46258 | 574 |
@{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\ |
575 |
@{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\ |
|
576 |
\end{mldecls} |
|
577 |
||
578 |
\begin{description} |
|
18537 | 579 |
|
46262 | 580 |
\item @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
581 |
composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a goal |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
582 |
state, it returns all states reachable in two steps by applying |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
583 |
@{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}. First, it applies @{text |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
584 |
"tac\<^sub>1"} to the goal state, getting a sequence of possible next |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
585 |
states; then, it applies @{text "tac\<^sub>2"} to each of these and |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
586 |
concatenates the results to produce again one flat sequence of |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
587 |
states. |
46258 | 588 |
|
46262 | 589 |
\item @{text "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "tac\<^sub>2"} makes a choice |
590 |
between @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a state, it |
|
591 |
tries @{text "tac\<^sub>1"} and returns the result if non-empty; if @{text |
|
592 |
"tac\<^sub>1"} fails then it uses @{text "tac\<^sub>2"}. This is a deterministic |
|
593 |
choice: if @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded |
|
594 |
from the result. |
|
46258 | 595 |
|
46262 | 596 |
\item @{text "tac\<^sub>1"}~@{ML_op APPEND}~@{text "tac\<^sub>2"} concatenates the |
597 |
possible results of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Unlike |
|
598 |
@{ML_op "ORELSE"} there is \emph{no commitment} to either tactic, so |
|
599 |
@{ML_op "APPEND"} helps to avoid incompleteness during search, at |
|
600 |
the cost of potential inefficiencies. |
|
39852 | 601 |
|
46262 | 602 |
\item @{ML EVERY}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text |
603 |
"tac\<^sub>1"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac\<^sub>n"}. |
|
604 |
Note that @{ML "EVERY []"} is the same as @{ML all_tac}: it always |
|
605 |
succeeds. |
|
46258 | 606 |
|
46262 | 607 |
\item @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text |
608 |
"tac\<^sub>1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op "ORELSE"}~@{text |
|
609 |
"tac\<^sub>n"}. Note that @{ML "FIRST []"} is the same as @{ML no_tac}: it |
|
610 |
always fails. |
|
46258 | 611 |
|
46264 | 612 |
\item @{ML_op "THEN'"} is the lifted version of @{ML_op "THEN"}, for |
46266 | 613 |
tactics with explicit subgoal addressing. So @{text |
46264 | 614 |
"(tac\<^sub>1"}~@{ML_op THEN'}~@{text "tac\<^sub>2) i"} is the same as @{text |
615 |
"(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"}. |
|
46258 | 616 |
|
46264 | 617 |
The other primed tacticals work analogously. |
46258 | 618 |
|
619 |
\end{description} |
|
58618 | 620 |
\<close> |
30272 | 621 |
|
46259 | 622 |
|
58618 | 623 |
subsection \<open>Repetition tacticals\<close> |
46259 | 624 |
|
58618 | 625 |
text \<open>These tacticals provide further control over repetition of |
46259 | 626 |
tactics, beyond the stylized forms of ``@{verbatim "?"}'' and |
58618 | 627 |
``@{verbatim "+"}'' in Isar method expressions.\<close> |
46259 | 628 |
|
58618 | 629 |
text %mlref \<open> |
46259 | 630 |
\begin{mldecls} |
631 |
@{index_ML "TRY": "tactic -> tactic"} \\ |
|
46266 | 632 |
@{index_ML "REPEAT": "tactic -> tactic"} \\ |
633 |
@{index_ML "REPEAT1": "tactic -> tactic"} \\ |
|
46259 | 634 |
@{index_ML "REPEAT_DETERM": "tactic -> tactic"} \\ |
635 |
@{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\ |
|
636 |
\end{mldecls} |
|
637 |
||
638 |
\begin{description} |
|
639 |
||
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
640 |
\item @{ML TRY}~@{text "tac"} applies @{text "tac"} to the goal |
46259 | 641 |
state and returns the resulting sequence, if non-empty; otherwise it |
642 |
returns the original state. Thus, it applies @{text "tac"} at most |
|
643 |
once. |
|
644 |
||
46266 | 645 |
Note that for tactics with subgoal addressing, the combinator can be |
646 |
applied via functional composition: @{ML "TRY"}~@{ML_op o}~@{text |
|
647 |
"tac"}. There is no need for @{verbatim TRY'}. |
|
46259 | 648 |
|
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
649 |
\item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the goal |
46259 | 650 |
state and, recursively, to each element of the resulting sequence. |
651 |
The resulting sequence consists of those states that make @{text |
|
652 |
"tac"} fail. Thus, it applies @{text "tac"} as many times as |
|
653 |
possible (including zero times), and allows backtracking over each |
|
654 |
invocation of @{text "tac"}. @{ML REPEAT} is more general than @{ML |
|
655 |
REPEAT_DETERM}, but requires more space. |
|
656 |
||
657 |
\item @{ML REPEAT1}~@{text "tac"} is like @{ML REPEAT}~@{text "tac"} |
|
658 |
but it always applies @{text "tac"} at least once, failing if this |
|
659 |
is impossible. |
|
660 |
||
46266 | 661 |
\item @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
662 |
goal state and, recursively, to the head of the resulting sequence. |
46266 | 663 |
It returns the first state to make @{text "tac"} fail. It is |
664 |
deterministic, discarding alternative outcomes. |
|
665 |
||
666 |
\item @{ML REPEAT_DETERM_N}~@{text "n tac"} is like @{ML |
|
667 |
REPEAT_DETERM}~@{text "tac"} but the number of repetitions is bound |
|
668 |
by @{text "n"} (where @{ML "~1"} means @{text "\<infinity>"}). |
|
46259 | 669 |
|
670 |
\end{description} |
|
58618 | 671 |
\<close> |
46259 | 672 |
|
58618 | 673 |
text %mlex \<open>The basic tactics and tacticals considered above follow |
46260 | 674 |
some algebraic laws: |
46259 | 675 |
|
46260 | 676 |
\begin{itemize} |
46259 | 677 |
|
46262 | 678 |
\item @{ML all_tac} is the identity element of the tactical @{ML_op |
679 |
"THEN"}. |
|
46259 | 680 |
|
46262 | 681 |
\item @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and |
682 |
@{ML_op "APPEND"}. Also, it is a zero element for @{ML_op "THEN"}, |
|
683 |
which means that @{text "tac"}~@{ML_op THEN}~@{ML no_tac} is |
|
684 |
equivalent to @{ML no_tac}. |
|
46259 | 685 |
|
46260 | 686 |
\item @{ML TRY} and @{ML REPEAT} can be expressed as (recursive) |
687 |
functions over more basic combinators (ignoring some internal |
|
688 |
implementation tricks): |
|
46259 | 689 |
|
46260 | 690 |
\end{itemize} |
58618 | 691 |
\<close> |
46259 | 692 |
|
58618 | 693 |
ML \<open> |
46259 | 694 |
fun TRY tac = tac ORELSE all_tac; |
695 |
fun REPEAT tac st = ((tac THEN REPEAT tac) ORELSE all_tac) st; |
|
58618 | 696 |
\<close> |
46259 | 697 |
|
58618 | 698 |
text \<open>If @{text "tac"} can return multiple outcomes then so can @{ML |
46262 | 699 |
REPEAT}~@{text "tac"}. @{ML REPEAT} uses @{ML_op "ORELSE"} and not |
700 |
@{ML_op "APPEND"}, it applies @{text "tac"} as many times as |
|
46259 | 701 |
possible in each outcome. |
702 |
||
703 |
\begin{warn} |
|
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
704 |
Note the explicit abstraction over the goal state in the ML |
46260 | 705 |
definition of @{ML REPEAT}. Recursive tacticals must be coded in |
706 |
this awkward fashion to avoid infinite recursion of eager functional |
|
707 |
evaluation in Standard ML. The following attempt would make @{ML |
|
708 |
REPEAT}~@{text "tac"} loop: |
|
46259 | 709 |
\end{warn} |
58618 | 710 |
\<close> |
46259 | 711 |
|
58618 | 712 |
ML \<open> |
46260 | 713 |
(*BAD -- does not terminate!*) |
714 |
fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac; |
|
58618 | 715 |
\<close> |
46259 | 716 |
|
46263 | 717 |
|
58618 | 718 |
subsection \<open>Applying tactics to subgoal ranges\<close> |
46263 | 719 |
|
58618 | 720 |
text \<open>Tactics with explicit subgoal addressing |
46263 | 721 |
@{ML_type "int -> tactic"} can be used together with tacticals that |
722 |
act like ``subgoal quantifiers'': guided by success of the body |
|
723 |
tactic a certain range of subgoals is covered. Thus the body tactic |
|
46267 | 724 |
is applied to \emph{all} subgoals, \emph{some} subgoal etc. |
46263 | 725 |
|
726 |
Suppose that the goal state has @{text "n \<ge> 0"} subgoals. Many of |
|
727 |
these tacticals address subgoal ranges counting downwards from |
|
728 |
@{text "n"} towards @{text "1"}. This has the fortunate effect that |
|
729 |
newly emerging subgoals are concatenated in the result, without |
|
730 |
interfering each other. Nonetheless, there might be situations |
|
58618 | 731 |
where a different order is desired.\<close> |
46263 | 732 |
|
58618 | 733 |
text %mlref \<open> |
46263 | 734 |
\begin{mldecls} |
735 |
@{index_ML ALLGOALS: "(int -> tactic) -> tactic"} \\ |
|
736 |
@{index_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\ |
|
737 |
@{index_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\ |
|
46267 | 738 |
@{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\ |
46263 | 739 |
@{index_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\ |
740 |
@{index_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\ |
|
46267 | 741 |
@{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\ |
46263 | 742 |
\end{mldecls} |
743 |
||
744 |
\begin{description} |
|
745 |
||
746 |
\item @{ML ALLGOALS}~@{text "tac"} is equivalent to @{text "tac |
|
747 |
n"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac 1"}. It |
|
748 |
applies the @{text tac} to all the subgoals, counting downwards. |
|
749 |
||
750 |
\item @{ML SOMEGOAL}~@{text "tac"} is equivalent to @{text "tac |
|
751 |
n"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac 1"}. It |
|
752 |
applies @{text "tac"} to one subgoal, counting downwards. |
|
753 |
||
754 |
\item @{ML FIRSTGOAL}~@{text "tac"} is equivalent to @{text "tac |
|
755 |
1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac n"}. It |
|
756 |
applies @{text "tac"} to one subgoal, counting upwards. |
|
757 |
||
46267 | 758 |
\item @{ML HEADGOAL}~@{text "tac"} is equivalent to @{text "tac 1"}. |
759 |
It applies @{text "tac"} unconditionally to the first subgoal. |
|
760 |
||
46263 | 761 |
\item @{ML REPEAT_SOME}~@{text "tac"} applies @{text "tac"} once or |
762 |
more to a subgoal, counting downwards. |
|
763 |
||
764 |
\item @{ML REPEAT_FIRST}~@{text "tac"} applies @{text "tac"} once or |
|
765 |
more to a subgoal, counting upwards. |
|
766 |
||
46267 | 767 |
\item @{ML RANGE}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>k] i"} is equivalent to |
768 |
@{text "tac\<^sub>k (i + k - 1)"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op |
|
769 |
THEN}~@{text "tac\<^sub>1 i"}. It applies the given list of tactics to the |
|
770 |
corresponding range of subgoals, counting downwards. |
|
771 |
||
46263 | 772 |
\end{description} |
58618 | 773 |
\<close> |
46263 | 774 |
|
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
775 |
|
58618 | 776 |
subsection \<open>Control and search tacticals\<close> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
777 |
|
58618 | 778 |
text \<open>A predicate on theorems @{ML_type "thm -> bool"} can test |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
779 |
whether a goal state enjoys some desirable property --- such as |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
780 |
having no subgoals. Tactics that search for satisfactory goal |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
781 |
states are easy to express. The main search procedures, |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
782 |
depth-first, breadth-first and best-first, are provided as |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
783 |
tacticals. They generate the search tree by repeatedly applying a |
58618 | 784 |
given tactic.\<close> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
785 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
786 |
|
46270 | 787 |
text %mlref "" |
788 |
||
58618 | 789 |
subsubsection \<open>Filtering a tactic's results\<close> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
790 |
|
58618 | 791 |
text \<open> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
792 |
\begin{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
793 |
@{index_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
794 |
@{index_ML CHANGED: "tactic -> tactic"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
795 |
\end{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
796 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
797 |
\begin{description} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
798 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
799 |
\item @{ML FILTER}~@{text "sat tac"} applies @{text "tac"} to the |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
800 |
goal state and returns a sequence consisting of those result goal |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
801 |
states that are satisfactory in the sense of @{text "sat"}. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
802 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
803 |
\item @{ML CHANGED}~@{text "tac"} applies @{text "tac"} to the goal |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
804 |
state and returns precisely those states that differ from the |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
805 |
original state (according to @{ML Thm.eq_thm}). Thus @{ML |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
806 |
CHANGED}~@{text "tac"} always has some effect on the state. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
807 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
808 |
\end{description} |
58618 | 809 |
\<close> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
810 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
811 |
|
58618 | 812 |
subsubsection \<open>Depth-first search\<close> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
813 |
|
58618 | 814 |
text \<open> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
815 |
\begin{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
816 |
@{index_ML DEPTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
817 |
@{index_ML DEPTH_SOLVE: "tactic -> tactic"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
818 |
@{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
819 |
\end{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
820 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
821 |
\begin{description} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
822 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
823 |
\item @{ML DEPTH_FIRST}~@{text "sat tac"} returns the goal state if |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
824 |
@{text "sat"} returns true. Otherwise it applies @{text "tac"}, |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
825 |
then recursively searches from each element of the resulting |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
826 |
sequence. The code uses a stack for efficiency, in effect applying |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
827 |
@{text "tac"}~@{ML_op THEN}~@{ML DEPTH_FIRST}~@{text "sat tac"} to |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
828 |
the state. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
829 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
830 |
\item @{ML DEPTH_SOLVE}@{text "tac"} uses @{ML DEPTH_FIRST} to |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
831 |
search for states having no subgoals. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
832 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
833 |
\item @{ML DEPTH_SOLVE_1}~@{text "tac"} uses @{ML DEPTH_FIRST} to |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
834 |
search for states having fewer subgoals than the given state. Thus, |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
835 |
it insists upon solving at least one subgoal. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
836 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
837 |
\end{description} |
58618 | 838 |
\<close> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
839 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
840 |
|
58618 | 841 |
subsubsection \<open>Other search strategies\<close> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
842 |
|
58618 | 843 |
text \<open> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
844 |
\begin{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
845 |
@{index_ML BREADTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
846 |
@{index_ML BEST_FIRST: "(thm -> bool) * (thm -> int) -> tactic -> tactic"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
847 |
@{index_ML THEN_BEST_FIRST: "tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
848 |
\end{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
849 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
850 |
These search strategies will find a solution if one exists. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
851 |
However, they do not enumerate all solutions; they terminate after |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
852 |
the first satisfactory result from @{text "tac"}. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
853 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
854 |
\begin{description} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
855 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
856 |
\item @{ML BREADTH_FIRST}~@{text "sat tac"} uses breadth-first |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
857 |
search to find states for which @{text "sat"} is true. For most |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
858 |
applications, it is too slow. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
859 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
860 |
\item @{ML BEST_FIRST}~@{text "(sat, dist) tac"} does a heuristic |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
861 |
search, using @{text "dist"} to estimate the distance from a |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
862 |
satisfactory state (in the sense of @{text "sat"}). It maintains a |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
863 |
list of states ordered by distance. It applies @{text "tac"} to the |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
864 |
head of this list; if the result contains any satisfactory states, |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
865 |
then it returns them. Otherwise, @{ML BEST_FIRST} adds the new |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
866 |
states to the list, and continues. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
867 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
868 |
The distance function is typically @{ML size_of_thm}, which computes |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
869 |
the size of the state. The smaller the state, the fewer and simpler |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
870 |
subgoals it has. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
871 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
872 |
\item @{ML THEN_BEST_FIRST}~@{text "tac\<^sub>0 (sat, dist) tac"} is like |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
873 |
@{ML BEST_FIRST}, except that the priority queue initially contains |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
874 |
the result of applying @{text "tac\<^sub>0"} to the goal state. This |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
875 |
tactical permits separate tactics for starting the search and |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
876 |
continuing the search. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
877 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
878 |
\end{description} |
58618 | 879 |
\<close> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
880 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
881 |
|
58618 | 882 |
subsubsection \<open>Auxiliary tacticals for searching\<close> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
883 |
|
58618 | 884 |
text \<open> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
885 |
\begin{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
886 |
@{index_ML COND: "(thm -> bool) -> tactic -> tactic -> tactic"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
887 |
@{index_ML IF_UNSOLVED: "tactic -> tactic"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
888 |
@{index_ML SOLVE: "tactic -> tactic"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
889 |
@{index_ML DETERM: "tactic -> tactic"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
890 |
\end{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
891 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
892 |
\begin{description} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
893 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
894 |
\item @{ML COND}~@{text "sat tac\<^sub>1 tac\<^sub>2"} applies @{text "tac\<^sub>1"} to |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
895 |
the goal state if it satisfies predicate @{text "sat"}, and applies |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
896 |
@{text "tac\<^sub>2"}. It is a conditional tactical in that only one of |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
897 |
@{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} is applied to a goal state. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
898 |
However, both @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} are evaluated |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
899 |
because ML uses eager evaluation. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
900 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
901 |
\item @{ML IF_UNSOLVED}~@{text "tac"} applies @{text "tac"} to the |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
902 |
goal state if it has any subgoals, and simply returns the goal state |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
903 |
otherwise. Many common tactics, such as @{ML resolve_tac}, fail if |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
904 |
applied to a goal state that has no subgoals. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
905 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
906 |
\item @{ML SOLVE}~@{text "tac"} applies @{text "tac"} to the goal |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
907 |
state and then fails iff there are subgoals left. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
908 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
909 |
\item @{ML DETERM}~@{text "tac"} applies @{text "tac"} to the goal |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
910 |
state and returns the head of the resulting sequence. @{ML DETERM} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
911 |
limits the search space by making its argument deterministic. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
912 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
913 |
\end{description} |
58618 | 914 |
\<close> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
915 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
916 |
|
58618 | 917 |
subsubsection \<open>Predicates and functions useful for searching\<close> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
918 |
|
58618 | 919 |
text \<open> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
920 |
\begin{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
921 |
@{index_ML has_fewer_prems: "int -> thm -> bool"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
922 |
@{index_ML Thm.eq_thm: "thm * thm -> bool"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
923 |
@{index_ML Thm.eq_thm_prop: "thm * thm -> bool"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
924 |
@{index_ML size_of_thm: "thm -> int"} \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
925 |
\end{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
926 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
927 |
\begin{description} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
928 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
929 |
\item @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
930 |
"thm"} has fewer than @{text "n"} premises. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
931 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
932 |
\item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text |
55547
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
wenzelm
parents:
53096
diff
changeset
|
933 |
"thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. Both theorems must have the |
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
wenzelm
parents:
53096
diff
changeset
|
934 |
same conclusions, the same set of hypotheses, and the same set of sort |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
935 |
hypotheses. Names of bound variables are ignored as usual. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
936 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
937 |
\item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
938 |
the propositions of @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
939 |
Names of bound variables are ignored. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
940 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
941 |
\item @{ML size_of_thm}~@{text "thm"} computes the size of @{text |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
942 |
"thm"}, namely the number of variables, constants and abstractions |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
943 |
in its conclusion. It may serve as a distance function for |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
944 |
@{ML BEST_FIRST}. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
945 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
946 |
\end{description} |
58618 | 947 |
\<close> |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
948 |
|
18537 | 949 |
end |