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