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