wenzelm@30184
|
1 |
|
lcp@104
|
2 |
\chapter{Tacticals}
|
lcp@104
|
3 |
\index{tacticals|(}
|
lcp@104
|
4 |
Tacticals are operations on tactics. Their implementation makes use of
|
lcp@104
|
5 |
functional programming techniques, especially for sequences. Most of the
|
lcp@104
|
6 |
time, you may forget about this and regard tacticals as high-level control
|
lcp@104
|
7 |
structures.
|
lcp@104
|
8 |
|
lcp@104
|
9 |
\section{The basic tacticals}
|
lcp@104
|
10 |
\subsection{Joining two tactics}
|
lcp@323
|
11 |
\index{tacticals!joining two tactics}
|
lcp@104
|
12 |
The tacticals {\tt THEN} and {\tt ORELSE}, which provide sequencing and
|
lcp@104
|
13 |
alternation, underlie most of the other control structures in Isabelle.
|
lcp@104
|
14 |
{\tt APPEND} and {\tt INTLEAVE} provide more sophisticated forms of
|
lcp@104
|
15 |
alternation.
|
lcp@104
|
16 |
\begin{ttbox}
|
lcp@104
|
17 |
THEN : tactic * tactic -> tactic \hfill{\bf infix 1}
|
lcp@104
|
18 |
ORELSE : tactic * tactic -> tactic \hfill{\bf infix}
|
lcp@104
|
19 |
APPEND : tactic * tactic -> tactic \hfill{\bf infix}
|
lcp@104
|
20 |
INTLEAVE : tactic * tactic -> tactic \hfill{\bf infix}
|
lcp@104
|
21 |
\end{ttbox}
|
lcp@323
|
22 |
\begin{ttdescription}
|
lcp@323
|
23 |
\item[$tac@1$ \ttindexbold{THEN} $tac@2$]
|
lcp@104
|
24 |
is the sequential composition of the two tactics. Applied to a proof
|
lcp@104
|
25 |
state, it returns all states reachable in two steps by applying $tac@1$
|
lcp@104
|
26 |
followed by~$tac@2$. First, it applies $tac@1$ to the proof state, getting a
|
lcp@104
|
27 |
sequence of next states; then, it applies $tac@2$ to each of these and
|
lcp@104
|
28 |
concatenates the results.
|
lcp@104
|
29 |
|
lcp@323
|
30 |
\item[$tac@1$ \ttindexbold{ORELSE} $tac@2$]
|
lcp@104
|
31 |
makes a choice between the two tactics. Applied to a state, it
|
lcp@104
|
32 |
tries~$tac@1$ and returns the result if non-empty; if $tac@1$ fails then it
|
lcp@104
|
33 |
uses~$tac@2$. This is a deterministic choice: if $tac@1$ succeeds then
|
lcp@104
|
34 |
$tac@2$ is excluded.
|
lcp@104
|
35 |
|
lcp@323
|
36 |
\item[$tac@1$ \ttindexbold{APPEND} $tac@2$]
|
lcp@104
|
37 |
concatenates the results of $tac@1$ and~$tac@2$. By not making a commitment
|
lcp@323
|
38 |
to either tactic, {\tt APPEND} helps avoid incompleteness during
|
lcp@323
|
39 |
search.\index{search}
|
lcp@104
|
40 |
|
lcp@323
|
41 |
\item[$tac@1$ \ttindexbold{INTLEAVE} $tac@2$]
|
lcp@104
|
42 |
interleaves the results of $tac@1$ and~$tac@2$. Thus, it includes all
|
lcp@104
|
43 |
possible next states, even if one of the tactics returns an infinite
|
lcp@104
|
44 |
sequence.
|
lcp@323
|
45 |
\end{ttdescription}
|
lcp@104
|
46 |
|
lcp@104
|
47 |
|
lcp@104
|
48 |
\subsection{Joining a list of tactics}
|
lcp@323
|
49 |
\index{tacticals!joining a list of tactics}
|
lcp@104
|
50 |
\begin{ttbox}
|
lcp@104
|
51 |
EVERY : tactic list -> tactic
|
lcp@104
|
52 |
FIRST : tactic list -> tactic
|
lcp@104
|
53 |
\end{ttbox}
|
lcp@104
|
54 |
{\tt EVERY} and {\tt FIRST} are block structured versions of {\tt THEN} and
|
lcp@104
|
55 |
{\tt ORELSE}\@.
|
lcp@323
|
56 |
\begin{ttdescription}
|
lcp@104
|
57 |
\item[\ttindexbold{EVERY} {$[tac@1,\ldots,tac@n]$}]
|
lcp@104
|
58 |
abbreviates \hbox{\tt$tac@1$ THEN \ldots{} THEN $tac@n$}. It is useful for
|
lcp@104
|
59 |
writing a series of tactics to be executed in sequence.
|
lcp@104
|
60 |
|
lcp@104
|
61 |
\item[\ttindexbold{FIRST} {$[tac@1,\ldots,tac@n]$}]
|
lcp@104
|
62 |
abbreviates \hbox{\tt$tac@1$ ORELSE \ldots{} ORELSE $tac@n$}. It is useful for
|
lcp@104
|
63 |
writing a series of tactics to be attempted one after another.
|
lcp@323
|
64 |
\end{ttdescription}
|
lcp@104
|
65 |
|
lcp@104
|
66 |
|
lcp@104
|
67 |
\subsection{Repetition tacticals}
|
lcp@323
|
68 |
\index{tacticals!repetition}
|
lcp@104
|
69 |
\begin{ttbox}
|
oheimb@8149
|
70 |
TRY : tactic -> tactic
|
oheimb@8149
|
71 |
REPEAT_DETERM : tactic -> tactic
|
oheimb@8149
|
72 |
REPEAT_DETERM_N : int -> tactic -> tactic
|
oheimb@8149
|
73 |
REPEAT : tactic -> tactic
|
oheimb@8149
|
74 |
REPEAT1 : tactic -> tactic
|
oheimb@8149
|
75 |
DETERM_UNTIL : (thm -> bool) -> tactic -> tactic
|
oheimb@8149
|
76 |
trace_REPEAT : bool ref \hfill{\bf initially false}
|
lcp@104
|
77 |
\end{ttbox}
|
lcp@323
|
78 |
\begin{ttdescription}
|
lcp@104
|
79 |
\item[\ttindexbold{TRY} {\it tac}]
|
lcp@104
|
80 |
applies {\it tac\/} to the proof state and returns the resulting sequence,
|
lcp@104
|
81 |
if non-empty; otherwise it returns the original state. Thus, it applies
|
lcp@104
|
82 |
{\it tac\/} at most once.
|
lcp@104
|
83 |
|
lcp@104
|
84 |
\item[\ttindexbold{REPEAT_DETERM} {\it tac}]
|
lcp@104
|
85 |
applies {\it tac\/} to the proof state and, recursively, to the head of the
|
lcp@104
|
86 |
resulting sequence. It returns the first state to make {\it tac\/} fail.
|
lcp@104
|
87 |
It is deterministic, discarding alternative outcomes.
|
lcp@104
|
88 |
|
oheimb@8149
|
89 |
\item[\ttindexbold{REPEAT_DETERM_N} {\it n} {\it tac}]
|
oheimb@8149
|
90 |
is like \hbox{\tt REPEAT_DETERM {\it tac}} but the number of repititions
|
oheimb@8149
|
91 |
is bound by {\it n} (unless negative).
|
oheimb@8149
|
92 |
|
lcp@104
|
93 |
\item[\ttindexbold{REPEAT} {\it tac}]
|
lcp@104
|
94 |
applies {\it tac\/} to the proof state and, recursively, to each element of
|
lcp@104
|
95 |
the resulting sequence. The resulting sequence consists of those states
|
lcp@104
|
96 |
that make {\it tac\/} fail. Thus, it applies {\it tac\/} as many times as
|
lcp@104
|
97 |
possible (including zero times), and allows backtracking over each
|
lcp@104
|
98 |
invocation of {\it tac}. It is more general than {\tt REPEAT_DETERM}, but
|
lcp@104
|
99 |
requires more space.
|
lcp@104
|
100 |
|
lcp@104
|
101 |
\item[\ttindexbold{REPEAT1} {\it tac}]
|
lcp@104
|
102 |
is like \hbox{\tt REPEAT {\it tac}} but it always applies {\it tac\/} at
|
lcp@104
|
103 |
least once, failing if this is impossible.
|
lcp@104
|
104 |
|
oheimb@8149
|
105 |
\item[\ttindexbold{DETERM_UNTIL} {\it p} {\it tac}]
|
oheimb@8149
|
106 |
applies {\it tac\/} to the proof state and, recursively, to the head of the
|
oheimb@8149
|
107 |
resulting sequence, until the predicate {\it p} (applied on the proof state)
|
oheimb@8149
|
108 |
yields {\it true}. It fails if {\it tac\/} fails on any of the intermediate
|
oheimb@8149
|
109 |
states. It is deterministic, discarding alternative outcomes.
|
oheimb@8149
|
110 |
|
wenzelm@4317
|
111 |
\item[set \ttindexbold{trace_REPEAT};]
|
lcp@286
|
112 |
enables an interactive tracing mode for the tacticals {\tt REPEAT_DETERM}
|
lcp@286
|
113 |
and {\tt REPEAT}. To view the tracing options, type {\tt h} at the prompt.
|
lcp@323
|
114 |
\end{ttdescription}
|
lcp@104
|
115 |
|
lcp@104
|
116 |
|
lcp@104
|
117 |
\subsection{Identities for tacticals}
|
lcp@323
|
118 |
\index{tacticals!identities for}
|
lcp@104
|
119 |
\begin{ttbox}
|
lcp@104
|
120 |
all_tac : tactic
|
lcp@104
|
121 |
no_tac : tactic
|
lcp@104
|
122 |
\end{ttbox}
|
lcp@323
|
123 |
\begin{ttdescription}
|
lcp@104
|
124 |
\item[\ttindexbold{all_tac}]
|
lcp@104
|
125 |
maps any proof state to the one-element sequence containing that state.
|
lcp@104
|
126 |
Thus, it succeeds for all states. It is the identity element of the
|
lcp@104
|
127 |
tactical \ttindex{THEN}\@.
|
lcp@104
|
128 |
|
lcp@104
|
129 |
\item[\ttindexbold{no_tac}]
|
lcp@104
|
130 |
maps any proof state to the empty sequence. Thus it succeeds for no state.
|
lcp@104
|
131 |
It is the identity element of \ttindex{ORELSE}, \ttindex{APPEND}, and
|
lcp@104
|
132 |
\ttindex{INTLEAVE}\@. Also, it is a zero element for \ttindex{THEN}, which means that
|
lcp@104
|
133 |
\hbox{\tt$tac$ THEN no_tac} is equivalent to {\tt no_tac}.
|
lcp@323
|
134 |
\end{ttdescription}
|
lcp@104
|
135 |
These primitive tactics are useful when writing tacticals. For example,
|
lcp@104
|
136 |
\ttindexbold{TRY} and \ttindexbold{REPEAT} (ignoring tracing) can be coded
|
lcp@104
|
137 |
as follows:
|
lcp@104
|
138 |
\begin{ttbox}
|
lcp@104
|
139 |
fun TRY tac = tac ORELSE all_tac;
|
lcp@104
|
140 |
|
wenzelm@3108
|
141 |
fun REPEAT tac =
|
wenzelm@3108
|
142 |
(fn state => ((tac THEN REPEAT tac) ORELSE all_tac) state);
|
lcp@104
|
143 |
\end{ttbox}
|
lcp@104
|
144 |
If $tac$ can return multiple outcomes then so can \hbox{\tt REPEAT $tac$}.
|
lcp@104
|
145 |
Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND} or {\tt
|
lcp@104
|
146 |
INTLEAVE}, it applies $tac$ as many times as possible in each
|
lcp@104
|
147 |
outcome.
|
lcp@104
|
148 |
|
lcp@104
|
149 |
\begin{warn}
|
lcp@104
|
150 |
Note {\tt REPEAT}'s explicit abstraction over the proof state. Recursive
|
lcp@104
|
151 |
tacticals must be coded in this awkward fashion to avoid infinite
|
lcp@104
|
152 |
recursion. With the following definition, \hbox{\tt REPEAT $tac$} would
|
lcp@332
|
153 |
loop due to \ML's eager evaluation strategy:
|
lcp@104
|
154 |
\begin{ttbox}
|
lcp@104
|
155 |
fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
|
lcp@104
|
156 |
\end{ttbox}
|
lcp@104
|
157 |
\par\noindent
|
lcp@104
|
158 |
The built-in {\tt REPEAT} avoids~{\tt THEN}, handling sequences explicitly
|
lcp@104
|
159 |
and using tail recursion. This sacrifices clarity, but saves much space by
|
lcp@104
|
160 |
discarding intermediate proof states.
|
lcp@104
|
161 |
\end{warn}
|
lcp@104
|
162 |
|
lcp@104
|
163 |
|
lcp@104
|
164 |
\section{Control and search tacticals}
|
lcp@323
|
165 |
\index{search!tacticals|(}
|
lcp@323
|
166 |
|
lcp@104
|
167 |
A predicate on theorems, namely a function of type \hbox{\tt thm->bool},
|
lcp@104
|
168 |
can test whether a proof state enjoys some desirable property --- such as
|
lcp@104
|
169 |
having no subgoals. Tactics that search for satisfactory states are easy
|
lcp@104
|
170 |
to express. The main search procedures, depth-first, breadth-first and
|
lcp@104
|
171 |
best-first, are provided as tacticals. They generate the search tree by
|
lcp@104
|
172 |
repeatedly applying a given tactic.
|
lcp@104
|
173 |
|
lcp@104
|
174 |
|
lcp@104
|
175 |
\subsection{Filtering a tactic's results}
|
lcp@323
|
176 |
\index{tacticals!for filtering}
|
lcp@323
|
177 |
\index{tactics!filtering results of}
|
lcp@104
|
178 |
\begin{ttbox}
|
lcp@104
|
179 |
FILTER : (thm -> bool) -> tactic -> tactic
|
lcp@104
|
180 |
CHANGED : tactic -> tactic
|
lcp@104
|
181 |
\end{ttbox}
|
lcp@323
|
182 |
\begin{ttdescription}
|
lcp@1118
|
183 |
\item[\ttindexbold{FILTER} {\it p} $tac$]
|
lcp@104
|
184 |
applies $tac$ to the proof state and returns a sequence consisting of those
|
lcp@104
|
185 |
result states that satisfy~$p$.
|
lcp@104
|
186 |
|
lcp@104
|
187 |
\item[\ttindexbold{CHANGED} {\it tac}]
|
lcp@104
|
188 |
applies {\it tac\/} to the proof state and returns precisely those states
|
lcp@104
|
189 |
that differ from the original state. Thus, \hbox{\tt CHANGED {\it tac}}
|
lcp@104
|
190 |
always has some effect on the state.
|
lcp@323
|
191 |
\end{ttdescription}
|
lcp@104
|
192 |
|
lcp@104
|
193 |
|
lcp@104
|
194 |
\subsection{Depth-first search}
|
lcp@323
|
195 |
\index{tacticals!searching}
|
lcp@104
|
196 |
\index{tracing!of searching tacticals}
|
lcp@104
|
197 |
\begin{ttbox}
|
lcp@104
|
198 |
DEPTH_FIRST : (thm->bool) -> tactic -> tactic
|
lcp@332
|
199 |
DEPTH_SOLVE : tactic -> tactic
|
lcp@332
|
200 |
DEPTH_SOLVE_1 : tactic -> tactic
|
lcp@104
|
201 |
trace_DEPTH_FIRST: bool ref \hfill{\bf initially false}
|
lcp@104
|
202 |
\end{ttbox}
|
lcp@323
|
203 |
\begin{ttdescription}
|
lcp@104
|
204 |
\item[\ttindexbold{DEPTH_FIRST} {\it satp} {\it tac}]
|
lcp@104
|
205 |
returns the proof state if {\it satp} returns true. Otherwise it applies
|
lcp@104
|
206 |
{\it tac}, then recursively searches from each element of the resulting
|
lcp@104
|
207 |
sequence. The code uses a stack for efficiency, in effect applying
|
lcp@104
|
208 |
\hbox{\tt {\it tac} THEN DEPTH_FIRST {\it satp} {\it tac}} to the state.
|
lcp@104
|
209 |
|
lcp@104
|
210 |
\item[\ttindexbold{DEPTH_SOLVE} {\it tac}]
|
lcp@104
|
211 |
uses {\tt DEPTH_FIRST} to search for states having no subgoals.
|
lcp@104
|
212 |
|
lcp@104
|
213 |
\item[\ttindexbold{DEPTH_SOLVE_1} {\it tac}]
|
lcp@104
|
214 |
uses {\tt DEPTH_FIRST} to search for states having fewer subgoals than the
|
lcp@104
|
215 |
given state. Thus, it insists upon solving at least one subgoal.
|
lcp@104
|
216 |
|
wenzelm@4317
|
217 |
\item[set \ttindexbold{trace_DEPTH_FIRST};]
|
lcp@104
|
218 |
enables interactive tracing for {\tt DEPTH_FIRST}. To view the
|
lcp@104
|
219 |
tracing options, type {\tt h} at the prompt.
|
lcp@323
|
220 |
\end{ttdescription}
|
lcp@104
|
221 |
|
lcp@104
|
222 |
|
lcp@104
|
223 |
\subsection{Other search strategies}
|
lcp@323
|
224 |
\index{tacticals!searching}
|
lcp@104
|
225 |
\index{tracing!of searching tacticals}
|
lcp@104
|
226 |
\begin{ttbox}
|
lcp@332
|
227 |
BREADTH_FIRST : (thm->bool) -> tactic -> tactic
|
lcp@104
|
228 |
BEST_FIRST : (thm->bool)*(thm->int) -> tactic -> tactic
|
lcp@104
|
229 |
THEN_BEST_FIRST : tactic * ((thm->bool) * (thm->int) * tactic)
|
lcp@104
|
230 |
-> tactic \hfill{\bf infix 1}
|
lcp@104
|
231 |
trace_BEST_FIRST: bool ref \hfill{\bf initially false}
|
lcp@104
|
232 |
\end{ttbox}
|
lcp@104
|
233 |
These search strategies will find a solution if one exists. However, they
|
lcp@104
|
234 |
do not enumerate all solutions; they terminate after the first satisfactory
|
lcp@104
|
235 |
result from {\it tac}.
|
lcp@323
|
236 |
\begin{ttdescription}
|
lcp@104
|
237 |
\item[\ttindexbold{BREADTH_FIRST} {\it satp} {\it tac}]
|
lcp@104
|
238 |
uses breadth-first search to find states for which {\it satp\/} is true.
|
lcp@104
|
239 |
For most applications, it is too slow.
|
lcp@104
|
240 |
|
lcp@104
|
241 |
\item[\ttindexbold{BEST_FIRST} $(satp,distf)$ {\it tac}]
|
lcp@104
|
242 |
does a heuristic search, using {\it distf\/} to estimate the distance from
|
lcp@104
|
243 |
a satisfactory state. It maintains a list of states ordered by distance.
|
lcp@104
|
244 |
It applies $tac$ to the head of this list; if the result contains any
|
lcp@104
|
245 |
satisfactory states, then it returns them. Otherwise, {\tt BEST_FIRST}
|
lcp@104
|
246 |
adds the new states to the list, and continues.
|
lcp@104
|
247 |
|
lcp@104
|
248 |
The distance function is typically \ttindex{size_of_thm}, which computes
|
lcp@104
|
249 |
the size of the state. The smaller the state, the fewer and simpler
|
lcp@104
|
250 |
subgoals it has.
|
lcp@104
|
251 |
|
lcp@104
|
252 |
\item[$tac@0$ \ttindexbold{THEN_BEST_FIRST} $(satp,distf,tac)$]
|
lcp@104
|
253 |
is like {\tt BEST_FIRST}, except that the priority queue initially
|
lcp@104
|
254 |
contains the result of applying $tac@0$ to the proof state. This tactical
|
lcp@104
|
255 |
permits separate tactics for starting the search and continuing the search.
|
lcp@104
|
256 |
|
wenzelm@4317
|
257 |
\item[set \ttindexbold{trace_BEST_FIRST};]
|
lcp@286
|
258 |
enables an interactive tracing mode for the tactical {\tt BEST_FIRST}. To
|
lcp@286
|
259 |
view the tracing options, type {\tt h} at the prompt.
|
lcp@323
|
260 |
\end{ttdescription}
|
lcp@104
|
261 |
|
lcp@104
|
262 |
|
lcp@104
|
263 |
\subsection{Auxiliary tacticals for searching}
|
lcp@104
|
264 |
\index{tacticals!conditional}
|
lcp@104
|
265 |
\index{tacticals!deterministic}
|
lcp@104
|
266 |
\begin{ttbox}
|
oheimb@8149
|
267 |
COND : (thm->bool) -> tactic -> tactic -> tactic
|
oheimb@8149
|
268 |
IF_UNSOLVED : tactic -> tactic
|
oheimb@8149
|
269 |
SOLVE : tactic -> tactic
|
oheimb@8149
|
270 |
DETERM : tactic -> tactic
|
oheimb@8149
|
271 |
DETERM_UNTIL_SOLVED : tactic -> tactic
|
lcp@104
|
272 |
\end{ttbox}
|
lcp@323
|
273 |
\begin{ttdescription}
|
lcp@1118
|
274 |
\item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$]
|
lcp@104
|
275 |
applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$
|
lcp@104
|
276 |
otherwise. It is a conditional tactical in that only one of $tac@1$ and
|
lcp@104
|
277 |
$tac@2$ is applied to a proof state. However, both $tac@1$ and $tac@2$ are
|
lcp@104
|
278 |
evaluated because \ML{} uses eager evaluation.
|
lcp@104
|
279 |
|
lcp@104
|
280 |
\item[\ttindexbold{IF_UNSOLVED} {\it tac}]
|
lcp@104
|
281 |
applies {\it tac\/} to the proof state if it has any subgoals, and simply
|
lcp@104
|
282 |
returns the proof state otherwise. Many common tactics, such as {\tt
|
lcp@104
|
283 |
resolve_tac}, fail if applied to a proof state that has no subgoals.
|
lcp@104
|
284 |
|
oheimb@5754
|
285 |
\item[\ttindexbold{SOLVE} {\it tac}]
|
oheimb@5754
|
286 |
applies {\it tac\/} to the proof state and then fails iff there are subgoals
|
oheimb@5754
|
287 |
left.
|
oheimb@5754
|
288 |
|
lcp@104
|
289 |
\item[\ttindexbold{DETERM} {\it tac}]
|
lcp@104
|
290 |
applies {\it tac\/} to the proof state and returns the head of the
|
lcp@104
|
291 |
resulting sequence. {\tt DETERM} limits the search space by making its
|
lcp@104
|
292 |
argument deterministic.
|
oheimb@8149
|
293 |
|
oheimb@8149
|
294 |
\item[\ttindexbold{DETERM_UNTIL_SOLVED} {\it tac}]
|
oheimb@8149
|
295 |
forces repeated deterministic application of {\it tac\/} to the proof state
|
oheimb@8149
|
296 |
until the goal is solved completely.
|
lcp@323
|
297 |
\end{ttdescription}
|
lcp@104
|
298 |
|
lcp@104
|
299 |
|
lcp@104
|
300 |
\subsection{Predicates and functions useful for searching}
|
lcp@104
|
301 |
\index{theorems!size of}
|
lcp@104
|
302 |
\index{theorems!equality of}
|
lcp@104
|
303 |
\begin{ttbox}
|
lcp@104
|
304 |
has_fewer_prems : int -> thm -> bool
|
lcp@104
|
305 |
eq_thm : thm * thm -> bool
|
wenzelm@13104
|
306 |
eq_thm_prop : thm * thm -> bool
|
lcp@104
|
307 |
size_of_thm : thm -> int
|
lcp@104
|
308 |
\end{ttbox}
|
lcp@323
|
309 |
\begin{ttdescription}
|
lcp@104
|
310 |
\item[\ttindexbold{has_fewer_prems} $n$ $thm$]
|
lcp@104
|
311 |
reports whether $thm$ has fewer than~$n$ premises. By currying,
|
lcp@104
|
312 |
\hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may
|
lcp@104
|
313 |
be given to the searching tacticals.
|
lcp@104
|
314 |
|
wenzelm@6569
|
315 |
\item[\ttindexbold{eq_thm} ($thm@1$, $thm@2$)] reports whether $thm@1$ and
|
wenzelm@13104
|
316 |
$thm@2$ are equal. Both theorems must have compatible signatures. Both
|
wenzelm@13104
|
317 |
theorems must have the same conclusions, the same hypotheses (in the same
|
wenzelm@13104
|
318 |
order), and the same set of sort hypotheses. Names of bound variables are
|
wenzelm@13104
|
319 |
ignored.
|
wenzelm@13104
|
320 |
|
wenzelm@13104
|
321 |
\item[\ttindexbold{eq_thm_prop} ($thm@1$, $thm@2$)] reports whether the
|
wenzelm@13104
|
322 |
propositions of $thm@1$ and $thm@2$ are equal. Names of bound variables are
|
wenzelm@13104
|
323 |
ignored.
|
lcp@104
|
324 |
|
lcp@104
|
325 |
\item[\ttindexbold{size_of_thm} $thm$]
|
lcp@104
|
326 |
computes the size of $thm$, namely the number of variables, constants and
|
lcp@104
|
327 |
abstractions in its conclusion. It may serve as a distance function for
|
lcp@104
|
328 |
\ttindex{BEST_FIRST}.
|
lcp@323
|
329 |
\end{ttdescription}
|
lcp@323
|
330 |
|
lcp@323
|
331 |
\index{search!tacticals|)}
|
lcp@104
|
332 |
|
lcp@104
|
333 |
|
lcp@104
|
334 |
\section{Tacticals for subgoal numbering}
|
lcp@104
|
335 |
When conducting a backward proof, we normally consider one goal at a time.
|
lcp@104
|
336 |
A tactic can affect the entire proof state, but many tactics --- such as
|
lcp@104
|
337 |
{\tt resolve_tac} and {\tt assume_tac} --- work on a single subgoal.
|
lcp@104
|
338 |
Subgoals are designated by a positive integer, so Isabelle provides
|
lcp@104
|
339 |
tacticals for combining values of type {\tt int->tactic}.
|
lcp@104
|
340 |
|
lcp@104
|
341 |
|
lcp@104
|
342 |
\subsection{Restricting a tactic to one subgoal}
|
lcp@104
|
343 |
\index{tactics!restricting to a subgoal}
|
lcp@104
|
344 |
\index{tacticals!for restriction to a subgoal}
|
lcp@104
|
345 |
\begin{ttbox}
|
lcp@104
|
346 |
SELECT_GOAL : tactic -> int -> tactic
|
lcp@104
|
347 |
METAHYPS : (thm list -> tactic) -> int -> tactic
|
lcp@104
|
348 |
\end{ttbox}
|
lcp@323
|
349 |
\begin{ttdescription}
|
lcp@104
|
350 |
\item[\ttindexbold{SELECT_GOAL} {\it tac} $i$]
|
lcp@104
|
351 |
restricts the effect of {\it tac\/} to subgoal~$i$ of the proof state. It
|
lcp@104
|
352 |
fails if there is no subgoal~$i$, or if {\it tac\/} changes the main goal
|
lcp@104
|
353 |
(do not use {\tt rewrite_tac}). It applies {\it tac\/} to a dummy proof
|
lcp@104
|
354 |
state and uses the result to refine the original proof state at
|
lcp@104
|
355 |
subgoal~$i$. If {\it tac\/} returns multiple results then so does
|
lcp@104
|
356 |
\hbox{\tt SELECT_GOAL {\it tac} $i$}.
|
lcp@104
|
357 |
|
lcp@323
|
358 |
{\tt SELECT_GOAL} works by creating a state of the form $\phi\Imp\phi$,
|
lcp@332
|
359 |
with the one subgoal~$\phi$. If subgoal~$i$ has the form $\psi\Imp\theta$
|
lcp@332
|
360 |
then $(\psi\Imp\theta)\Imp(\psi\Imp\theta)$ is in fact
|
lcp@332
|
361 |
$\List{\psi\Imp\theta;\; \psi}\Imp\theta$, a proof state with two subgoals.
|
lcp@332
|
362 |
Such a proof state might cause tactics to go astray. Therefore {\tt
|
lcp@332
|
363 |
SELECT_GOAL} inserts a quantifier to create the state
|
lcp@323
|
364 |
\[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta). \]
|
lcp@104
|
365 |
|
lcp@323
|
366 |
\item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{meta-assumptions}
|
lcp@104
|
367 |
takes subgoal~$i$, of the form
|
lcp@104
|
368 |
\[ \Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta, \]
|
lcp@104
|
369 |
and creates the list $\theta'@1$, \ldots, $\theta'@k$ of meta-level
|
lcp@104
|
370 |
assumptions. In these theorems, the subgoal's parameters ($x@1$,
|
lcp@104
|
371 |
\ldots,~$x@l$) become free variables. It supplies the assumptions to
|
lcp@104
|
372 |
$tacf$ and applies the resulting tactic to the proof state
|
lcp@104
|
373 |
$\theta\Imp\theta$.
|
lcp@104
|
374 |
|
lcp@104
|
375 |
If the resulting proof state is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$,
|
lcp@104
|
376 |
possibly containing $\theta'@1,\ldots,\theta'@k$ as assumptions, then it is
|
lcp@104
|
377 |
lifted back into the original context, yielding $n$ subgoals.
|
lcp@104
|
378 |
|
lcp@286
|
379 |
Meta-level assumptions may not contain unknowns. Unknowns in the
|
lcp@286
|
380 |
hypotheses $\theta@1,\ldots,\theta@k$ become free variables in $\theta'@1$,
|
lcp@286
|
381 |
\ldots, $\theta'@k$, and are restored afterwards; the {\tt METAHYPS} call
|
lcp@286
|
382 |
cannot instantiate them. Unknowns in $\theta$ may be instantiated. New
|
lcp@323
|
383 |
unknowns in $\phi@1$, \ldots, $\phi@n$ are lifted over the parameters.
|
lcp@104
|
384 |
|
lcp@104
|
385 |
Here is a typical application. Calling {\tt hyp_res_tac}~$i$ resolves
|
lcp@104
|
386 |
subgoal~$i$ with one of its own assumptions, which may itself have the form
|
lcp@104
|
387 |
of an inference rule (these are called {\bf higher-level assumptions}).
|
lcp@104
|
388 |
\begin{ttbox}
|
lcp@104
|
389 |
val hyp_res_tac = METAHYPS (fn prems => resolve_tac prems 1);
|
lcp@104
|
390 |
\end{ttbox}
|
lcp@332
|
391 |
The function \ttindex{gethyps} is useful for debugging applications of {\tt
|
lcp@332
|
392 |
METAHYPS}.
|
lcp@323
|
393 |
\end{ttdescription}
|
lcp@104
|
394 |
|
lcp@104
|
395 |
\begin{warn}
|
lcp@104
|
396 |
{\tt METAHYPS} fails if the context or new subgoals contain type unknowns.
|
lcp@104
|
397 |
In principle, the tactical could treat these like ordinary unknowns.
|
lcp@104
|
398 |
\end{warn}
|
lcp@104
|
399 |
|
lcp@104
|
400 |
|
lcp@104
|
401 |
\subsection{Scanning for a subgoal by number}
|
lcp@323
|
402 |
\index{tacticals!scanning for subgoals}
|
lcp@104
|
403 |
\begin{ttbox}
|
lcp@104
|
404 |
ALLGOALS : (int -> tactic) -> tactic
|
lcp@104
|
405 |
TRYALL : (int -> tactic) -> tactic
|
lcp@104
|
406 |
SOMEGOAL : (int -> tactic) -> tactic
|
lcp@104
|
407 |
FIRSTGOAL : (int -> tactic) -> tactic
|
lcp@104
|
408 |
REPEAT_SOME : (int -> tactic) -> tactic
|
lcp@104
|
409 |
REPEAT_FIRST : (int -> tactic) -> tactic
|
lcp@104
|
410 |
trace_goalno_tac : (int -> tactic) -> int -> tactic
|
lcp@104
|
411 |
\end{ttbox}
|
lcp@104
|
412 |
These apply a tactic function of type {\tt int -> tactic} to all the
|
lcp@104
|
413 |
subgoal numbers of a proof state, and join the resulting tactics using
|
lcp@104
|
414 |
\ttindex{THEN} or \ttindex{ORELSE}\@. Thus, they apply the tactic to all the
|
lcp@104
|
415 |
subgoals, or to one subgoal.
|
lcp@104
|
416 |
|
lcp@104
|
417 |
Suppose that the original proof state has $n$ subgoals.
|
lcp@104
|
418 |
|
lcp@323
|
419 |
\begin{ttdescription}
|
lcp@104
|
420 |
\item[\ttindexbold{ALLGOALS} {\it tacf}]
|
lcp@104
|
421 |
is equivalent to
|
lcp@104
|
422 |
\hbox{\tt$tacf(n)$ THEN \ldots{} THEN $tacf(1)$}.
|
lcp@104
|
423 |
|
lcp@323
|
424 |
It applies {\it tacf} to all the subgoals, counting downwards (to
|
lcp@104
|
425 |
avoid problems when subgoals are added or deleted).
|
lcp@104
|
426 |
|
lcp@104
|
427 |
\item[\ttindexbold{TRYALL} {\it tacf}]
|
lcp@104
|
428 |
is equivalent to
|
lcp@323
|
429 |
\hbox{\tt TRY$(tacf(n))$ THEN \ldots{} THEN TRY$(tacf(1))$}.
|
lcp@104
|
430 |
|
lcp@104
|
431 |
It attempts to apply {\it tacf} to all the subgoals. For instance,
|
lcp@286
|
432 |
the tactic \hbox{\tt TRYALL assume_tac} attempts to solve all the subgoals by
|
lcp@104
|
433 |
assumption.
|
lcp@104
|
434 |
|
lcp@104
|
435 |
\item[\ttindexbold{SOMEGOAL} {\it tacf}]
|
lcp@104
|
436 |
is equivalent to
|
lcp@104
|
437 |
\hbox{\tt$tacf(n)$ ORELSE \ldots{} ORELSE $tacf(1)$}.
|
lcp@104
|
438 |
|
lcp@323
|
439 |
It applies {\it tacf} to one subgoal, counting downwards. For instance,
|
lcp@286
|
440 |
the tactic \hbox{\tt SOMEGOAL assume_tac} solves one subgoal by assumption,
|
lcp@286
|
441 |
failing if this is impossible.
|
lcp@104
|
442 |
|
lcp@104
|
443 |
\item[\ttindexbold{FIRSTGOAL} {\it tacf}]
|
lcp@104
|
444 |
is equivalent to
|
lcp@104
|
445 |
\hbox{\tt$tacf(1)$ ORELSE \ldots{} ORELSE $tacf(n)$}.
|
lcp@104
|
446 |
|
lcp@323
|
447 |
It applies {\it tacf} to one subgoal, counting upwards.
|
lcp@104
|
448 |
|
lcp@104
|
449 |
\item[\ttindexbold{REPEAT_SOME} {\it tacf}]
|
lcp@323
|
450 |
applies {\it tacf} once or more to a subgoal, counting downwards.
|
lcp@104
|
451 |
|
lcp@104
|
452 |
\item[\ttindexbold{REPEAT_FIRST} {\it tacf}]
|
lcp@323
|
453 |
applies {\it tacf} once or more to a subgoal, counting upwards.
|
lcp@104
|
454 |
|
lcp@104
|
455 |
\item[\ttindexbold{trace_goalno_tac} {\it tac} {\it i}]
|
lcp@104
|
456 |
applies \hbox{\it tac i\/} to the proof state. If the resulting sequence
|
lcp@104
|
457 |
is non-empty, then it is returned, with the side-effect of printing {\tt
|
lcp@104
|
458 |
Subgoal~$i$ selected}. Otherwise, {\tt trace_goalno_tac} returns the empty
|
lcp@104
|
459 |
sequence and prints nothing.
|
lcp@104
|
460 |
|
lcp@323
|
461 |
It indicates that `the tactic worked for subgoal~$i$' and is mainly used
|
lcp@104
|
462 |
with {\tt SOMEGOAL} and {\tt FIRSTGOAL}.
|
lcp@323
|
463 |
\end{ttdescription}
|
lcp@104
|
464 |
|
lcp@104
|
465 |
|
lcp@104
|
466 |
\subsection{Joining tactic functions}
|
lcp@323
|
467 |
\index{tacticals!joining tactic functions}
|
lcp@104
|
468 |
\begin{ttbox}
|
lcp@104
|
469 |
THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix 1}
|
lcp@104
|
470 |
ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
|
lcp@104
|
471 |
APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
|
lcp@104
|
472 |
INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
|
lcp@104
|
473 |
EVERY' : ('a -> tactic) list -> 'a -> tactic
|
lcp@104
|
474 |
FIRST' : ('a -> tactic) list -> 'a -> tactic
|
lcp@104
|
475 |
\end{ttbox}
|
lcp@104
|
476 |
These help to express tactics that specify subgoal numbers. The tactic
|
lcp@104
|
477 |
\begin{ttbox}
|
lcp@104
|
478 |
SOMEGOAL (fn i => resolve_tac rls i ORELSE eresolve_tac erls i)
|
lcp@104
|
479 |
\end{ttbox}
|
lcp@104
|
480 |
can be simplified to
|
lcp@104
|
481 |
\begin{ttbox}
|
lcp@104
|
482 |
SOMEGOAL (resolve_tac rls ORELSE' eresolve_tac erls)
|
lcp@104
|
483 |
\end{ttbox}
|
lcp@104
|
484 |
Note that {\tt TRY'}, {\tt REPEAT'}, {\tt DEPTH_FIRST'}, etc.\ are not
|
lcp@104
|
485 |
provided, because function composition accomplishes the same purpose.
|
lcp@104
|
486 |
The tactic
|
lcp@104
|
487 |
\begin{ttbox}
|
lcp@104
|
488 |
ALLGOALS (fn i => REPEAT (etac exE i ORELSE atac i))
|
lcp@104
|
489 |
\end{ttbox}
|
lcp@104
|
490 |
can be simplified to
|
lcp@104
|
491 |
\begin{ttbox}
|
lcp@104
|
492 |
ALLGOALS (REPEAT o (etac exE ORELSE' atac))
|
lcp@104
|
493 |
\end{ttbox}
|
lcp@104
|
494 |
These tacticals are polymorphic; $x$ need not be an integer.
|
lcp@104
|
495 |
\begin{center} \tt
|
lcp@104
|
496 |
\begin{tabular}{r@{\rm\ \ yields\ \ }l}
|
lcp@323
|
497 |
$(tacf@1$~~THEN'~~$tacf@2)(x)$ \index{*THEN'} &
|
lcp@104
|
498 |
$tacf@1(x)$~~THEN~~$tacf@2(x)$ \\
|
lcp@104
|
499 |
|
lcp@323
|
500 |
$(tacf@1$ ORELSE' $tacf@2)(x)$ \index{*ORELSE'} &
|
lcp@104
|
501 |
$tacf@1(x)$ ORELSE $tacf@2(x)$ \\
|
lcp@104
|
502 |
|
lcp@323
|
503 |
$(tacf@1$ APPEND' $tacf@2)(x)$ \index{*APPEND'} &
|
lcp@104
|
504 |
$tacf@1(x)$ APPEND $tacf@2(x)$ \\
|
lcp@104
|
505 |
|
lcp@323
|
506 |
$(tacf@1$ INTLEAVE' $tacf@2)(x)$ \index{*INTLEAVE'} &
|
lcp@104
|
507 |
$tacf@1(x)$ INTLEAVE $tacf@2(x)$ \\
|
lcp@104
|
508 |
|
lcp@104
|
509 |
EVERY' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*EVERY'} &
|
lcp@104
|
510 |
EVERY $[tacf@1(x),\ldots,tacf@n(x)]$ \\
|
lcp@104
|
511 |
|
lcp@104
|
512 |
FIRST' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*FIRST'} &
|
lcp@104
|
513 |
FIRST $[tacf@1(x),\ldots,tacf@n(x)]$
|
lcp@104
|
514 |
\end{tabular}
|
lcp@104
|
515 |
\end{center}
|
lcp@104
|
516 |
|
lcp@104
|
517 |
|
lcp@104
|
518 |
\subsection{Applying a list of tactics to 1}
|
lcp@323
|
519 |
\index{tacticals!joining tactic functions}
|
lcp@104
|
520 |
\begin{ttbox}
|
lcp@104
|
521 |
EVERY1: (int -> tactic) list -> tactic
|
lcp@104
|
522 |
FIRST1: (int -> tactic) list -> tactic
|
lcp@104
|
523 |
\end{ttbox}
|
lcp@104
|
524 |
A common proof style is to treat the subgoals as a stack, always
|
lcp@104
|
525 |
restricting attention to the first subgoal. Such proofs contain long lists
|
lcp@104
|
526 |
of tactics, each applied to~1. These can be simplified using {\tt EVERY1}
|
lcp@104
|
527 |
and {\tt FIRST1}:
|
lcp@104
|
528 |
\begin{center} \tt
|
lcp@104
|
529 |
\begin{tabular}{r@{\rm\ \ abbreviates\ \ }l}
|
lcp@104
|
530 |
EVERY1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*EVERY1} &
|
lcp@104
|
531 |
EVERY $[tacf@1(1),\ldots,tacf@n(1)]$ \\
|
lcp@104
|
532 |
|
lcp@104
|
533 |
FIRST1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*FIRST1} &
|
lcp@104
|
534 |
FIRST $[tacf@1(1),\ldots,tacf@n(1)]$
|
lcp@104
|
535 |
\end{tabular}
|
lcp@104
|
536 |
\end{center}
|
lcp@104
|
537 |
|
lcp@104
|
538 |
\index{tacticals|)}
|
wenzelm@5371
|
539 |
|
wenzelm@5371
|
540 |
|
wenzelm@5371
|
541 |
%%% Local Variables:
|
wenzelm@5371
|
542 |
%%% mode: latex
|
wenzelm@5371
|
543 |
%%% TeX-master: "ref"
|
wenzelm@5371
|
544 |
%%% End:
|