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