lcp@104
|
1 |
%% $Id$
|
lcp@104
|
2 |
\chapter{Tactics} \label{tactics}
|
wenzelm@3108
|
3 |
\index{tactics|(} Tactics have type \mltydx{tactic}. This is just an
|
wenzelm@3108
|
4 |
abbreviation for functions from theorems to theorem sequences, where
|
wenzelm@3108
|
5 |
the theorems represent states of a backward proof. Tactics seldom
|
wenzelm@3108
|
6 |
need to be coded from scratch, as functions; instead they are
|
wenzelm@3108
|
7 |
expressed using basic tactics and tacticals.
|
lcp@104
|
8 |
|
paulson@2039
|
9 |
This chapter only presents the primitive tactics. Substantial proofs require
|
nipkow@3950
|
10 |
the power of simplification (Chapter~\ref{chap:simplification}) and classical
|
nipkow@3950
|
11 |
reasoning (Chapter~\ref{chap:classical}).
|
paulson@2039
|
12 |
|
lcp@104
|
13 |
\section{Resolution and assumption tactics}
|
lcp@104
|
14 |
{\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
|
lcp@104
|
15 |
a rule. {\bf Elim-resolution} is particularly suited for elimination
|
lcp@104
|
16 |
rules, while {\bf destruct-resolution} is particularly suited for
|
lcp@104
|
17 |
destruction rules. The {\tt r}, {\tt e}, {\tt d} naming convention is
|
lcp@104
|
18 |
maintained for several different kinds of resolution tactics, as well as
|
lcp@104
|
19 |
the shortcuts in the subgoal module.
|
lcp@104
|
20 |
|
lcp@104
|
21 |
All the tactics in this section act on a subgoal designated by a positive
|
lcp@104
|
22 |
integer~$i$. They fail (by returning the empty sequence) if~$i$ is out of
|
lcp@104
|
23 |
range.
|
lcp@104
|
24 |
|
lcp@104
|
25 |
\subsection{Resolution tactics}
|
lcp@323
|
26 |
\index{resolution!tactics}
|
lcp@104
|
27 |
\index{tactics!resolution|bold}
|
lcp@104
|
28 |
\begin{ttbox}
|
lcp@104
|
29 |
resolve_tac : thm list -> int -> tactic
|
lcp@104
|
30 |
eresolve_tac : thm list -> int -> tactic
|
lcp@104
|
31 |
dresolve_tac : thm list -> int -> tactic
|
lcp@104
|
32 |
forward_tac : thm list -> int -> tactic
|
lcp@104
|
33 |
\end{ttbox}
|
lcp@104
|
34 |
These perform resolution on a list of theorems, $thms$, representing a list
|
lcp@104
|
35 |
of object-rules. When generating next states, they take each of the rules
|
lcp@104
|
36 |
in the order given. Each rule may yield several next states, or none:
|
lcp@104
|
37 |
higher-order resolution may yield multiple resolvents.
|
lcp@323
|
38 |
\begin{ttdescription}
|
lcp@104
|
39 |
\item[\ttindexbold{resolve_tac} {\it thms} {\it i}]
|
lcp@323
|
40 |
refines the proof state using the rules, which should normally be
|
lcp@323
|
41 |
introduction rules. It resolves a rule's conclusion with
|
lcp@323
|
42 |
subgoal~$i$ of the proof state.
|
lcp@104
|
43 |
|
lcp@104
|
44 |
\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}]
|
lcp@323
|
45 |
\index{elim-resolution}
|
lcp@323
|
46 |
performs elim-resolution with the rules, which should normally be
|
lcp@323
|
47 |
elimination rules. It resolves with a rule, solves its first premise by
|
lcp@323
|
48 |
assumption, and finally {\em deletes\/} that assumption from any new
|
lcp@323
|
49 |
subgoals.
|
lcp@104
|
50 |
|
lcp@104
|
51 |
\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}]
|
lcp@323
|
52 |
\index{forward proof}\index{destruct-resolution}
|
lcp@323
|
53 |
performs destruct-resolution with the rules, which normally should
|
lcp@323
|
54 |
be destruction rules. This replaces an assumption by the result of
|
lcp@323
|
55 |
applying one of the rules.
|
lcp@104
|
56 |
|
lcp@323
|
57 |
\item[\ttindexbold{forward_tac}]\index{forward proof}
|
lcp@323
|
58 |
is like {\tt dresolve_tac} except that the selected assumption is not
|
lcp@323
|
59 |
deleted. It applies a rule to an assumption, adding the result as a new
|
lcp@323
|
60 |
assumption.
|
lcp@323
|
61 |
\end{ttdescription}
|
lcp@104
|
62 |
|
lcp@104
|
63 |
\subsection{Assumption tactics}
|
lcp@323
|
64 |
\index{tactics!assumption|bold}\index{assumptions!tactics for}
|
lcp@104
|
65 |
\begin{ttbox}
|
lcp@104
|
66 |
assume_tac : int -> tactic
|
lcp@104
|
67 |
eq_assume_tac : int -> tactic
|
lcp@104
|
68 |
\end{ttbox}
|
lcp@323
|
69 |
\begin{ttdescription}
|
lcp@104
|
70 |
\item[\ttindexbold{assume_tac} {\it i}]
|
lcp@104
|
71 |
attempts to solve subgoal~$i$ by assumption.
|
lcp@104
|
72 |
|
lcp@104
|
73 |
\item[\ttindexbold{eq_assume_tac}]
|
lcp@104
|
74 |
is like {\tt assume_tac} but does not use unification. It succeeds (with a
|
lcp@323
|
75 |
{\em unique\/} next state) if one of the assumptions is identical to the
|
lcp@104
|
76 |
subgoal's conclusion. Since it does not instantiate variables, it cannot
|
lcp@104
|
77 |
make other subgoals unprovable. It is intended to be called from proof
|
lcp@104
|
78 |
strategies, not interactively.
|
lcp@323
|
79 |
\end{ttdescription}
|
lcp@104
|
80 |
|
lcp@104
|
81 |
\subsection{Matching tactics} \label{match_tac}
|
lcp@323
|
82 |
\index{tactics!matching}
|
lcp@104
|
83 |
\begin{ttbox}
|
lcp@104
|
84 |
match_tac : thm list -> int -> tactic
|
lcp@104
|
85 |
ematch_tac : thm list -> int -> tactic
|
lcp@104
|
86 |
dmatch_tac : thm list -> int -> tactic
|
lcp@104
|
87 |
\end{ttbox}
|
lcp@104
|
88 |
These are just like the resolution tactics except that they never
|
lcp@104
|
89 |
instantiate unknowns in the proof state. Flexible subgoals are not updated
|
lcp@104
|
90 |
willy-nilly, but are left alone. Matching --- strictly speaking --- means
|
lcp@104
|
91 |
treating the unknowns in the proof state as constants; these tactics merely
|
lcp@104
|
92 |
discard unifiers that would update the proof state.
|
lcp@323
|
93 |
\begin{ttdescription}
|
lcp@104
|
94 |
\item[\ttindexbold{match_tac} {\it thms} {\it i}]
|
lcp@323
|
95 |
refines the proof state using the rules, matching a rule's
|
lcp@104
|
96 |
conclusion with subgoal~$i$ of the proof state.
|
lcp@104
|
97 |
|
lcp@104
|
98 |
\item[\ttindexbold{ematch_tac}]
|
lcp@104
|
99 |
is like {\tt match_tac}, but performs elim-resolution.
|
lcp@104
|
100 |
|
lcp@104
|
101 |
\item[\ttindexbold{dmatch_tac}]
|
lcp@104
|
102 |
is like {\tt match_tac}, but performs destruct-resolution.
|
lcp@323
|
103 |
\end{ttdescription}
|
lcp@104
|
104 |
|
lcp@104
|
105 |
|
lcp@104
|
106 |
\subsection{Resolution with instantiation} \label{res_inst_tac}
|
lcp@323
|
107 |
\index{tactics!instantiation}\index{instantiation}
|
lcp@104
|
108 |
\begin{ttbox}
|
lcp@104
|
109 |
res_inst_tac : (string*string)list -> thm -> int -> tactic
|
lcp@104
|
110 |
eres_inst_tac : (string*string)list -> thm -> int -> tactic
|
lcp@104
|
111 |
dres_inst_tac : (string*string)list -> thm -> int -> tactic
|
lcp@104
|
112 |
forw_inst_tac : (string*string)list -> thm -> int -> tactic
|
lcp@104
|
113 |
\end{ttbox}
|
lcp@104
|
114 |
These tactics are designed for applying rules such as substitution and
|
lcp@104
|
115 |
induction, which cause difficulties for higher-order unification. The
|
lcp@332
|
116 |
tactics accept explicit instantiations for unknowns in the rule ---
|
lcp@332
|
117 |
typically, in the rule's conclusion. Each instantiation is a pair
|
lcp@332
|
118 |
{\tt($v$,$e$)}, where $v$ is an unknown {\em without\/} its leading
|
lcp@332
|
119 |
question mark!
|
lcp@104
|
120 |
\begin{itemize}
|
lcp@332
|
121 |
\item If $v$ is the type unknown {\tt'a}, then
|
lcp@332
|
122 |
the rule must contain a type unknown \verb$?'a$ of some
|
lcp@104
|
123 |
sort~$s$, and $e$ should be a type of sort $s$.
|
lcp@104
|
124 |
|
lcp@332
|
125 |
\item If $v$ is the unknown {\tt P}, then
|
lcp@332
|
126 |
the rule must contain an unknown \verb$?P$ of some type~$\tau$,
|
lcp@104
|
127 |
and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
|
lcp@104
|
128 |
$\sigma$ are unifiable. If the unification of $\tau$ and $\sigma$
|
lcp@332
|
129 |
instantiates any type unknowns in $\tau$, these instantiations
|
lcp@104
|
130 |
are recorded for application to the rule.
|
lcp@104
|
131 |
\end{itemize}
|
lcp@104
|
132 |
Types are instantiated before terms. Because type instantiations are
|
lcp@104
|
133 |
inferred from term instantiations, explicit type instantiations are seldom
|
lcp@104
|
134 |
necessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list
|
lcp@104
|
135 |
\verb$[("'a","bool"),("t","True")]$ may be simplified to
|
lcp@104
|
136 |
\verb$[("t","True")]$. Type unknowns in the proof state may cause
|
lcp@104
|
137 |
failure because the tactics cannot instantiate them.
|
lcp@104
|
138 |
|
lcp@104
|
139 |
The instantiation tactics act on a given subgoal. Terms in the
|
lcp@104
|
140 |
instantiations are type-checked in the context of that subgoal --- in
|
lcp@104
|
141 |
particular, they may refer to that subgoal's parameters. Any unknowns in
|
lcp@104
|
142 |
the terms receive subscripts and are lifted over the parameters; thus, you
|
lcp@104
|
143 |
may not refer to unknowns in the subgoal.
|
lcp@104
|
144 |
|
lcp@323
|
145 |
\begin{ttdescription}
|
lcp@104
|
146 |
\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
|
lcp@104
|
147 |
instantiates the rule {\it thm} with the instantiations {\it insts}, as
|
lcp@104
|
148 |
described above, and then performs resolution on subgoal~$i$. Resolution
|
lcp@104
|
149 |
typically causes further instantiations; you need not give explicit
|
lcp@332
|
150 |
instantiations for every unknown in the rule.
|
lcp@104
|
151 |
|
lcp@104
|
152 |
\item[\ttindexbold{eres_inst_tac}]
|
lcp@104
|
153 |
is like {\tt res_inst_tac}, but performs elim-resolution.
|
lcp@104
|
154 |
|
lcp@104
|
155 |
\item[\ttindexbold{dres_inst_tac}]
|
lcp@104
|
156 |
is like {\tt res_inst_tac}, but performs destruct-resolution.
|
lcp@104
|
157 |
|
lcp@104
|
158 |
\item[\ttindexbold{forw_inst_tac}]
|
lcp@104
|
159 |
is like {\tt dres_inst_tac} except that the selected assumption is not
|
lcp@104
|
160 |
deleted. It applies the instantiated rule to an assumption, adding the
|
lcp@104
|
161 |
result as a new assumption.
|
lcp@323
|
162 |
\end{ttdescription}
|
lcp@104
|
163 |
|
lcp@104
|
164 |
|
lcp@104
|
165 |
\section{Other basic tactics}
|
paulson@2039
|
166 |
\subsection{Tactic shortcuts}
|
paulson@2039
|
167 |
\index{shortcuts!for tactics}
|
paulson@2039
|
168 |
\index{tactics!resolution}\index{tactics!assumption}
|
paulson@2039
|
169 |
\index{tactics!meta-rewriting}
|
paulson@2039
|
170 |
\begin{ttbox}
|
paulson@2039
|
171 |
rtac : thm -> int -> tactic
|
paulson@2039
|
172 |
etac : thm -> int -> tactic
|
paulson@2039
|
173 |
dtac : thm -> int -> tactic
|
paulson@2039
|
174 |
atac : int -> tactic
|
paulson@2039
|
175 |
ares_tac : thm list -> int -> tactic
|
paulson@2039
|
176 |
rewtac : thm -> tactic
|
paulson@2039
|
177 |
\end{ttbox}
|
paulson@2039
|
178 |
These abbreviate common uses of tactics.
|
paulson@2039
|
179 |
\begin{ttdescription}
|
paulson@2039
|
180 |
\item[\ttindexbold{rtac} {\it thm} {\it i}]
|
paulson@2039
|
181 |
abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.
|
paulson@2039
|
182 |
|
paulson@2039
|
183 |
\item[\ttindexbold{etac} {\it thm} {\it i}]
|
paulson@2039
|
184 |
abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.
|
paulson@2039
|
185 |
|
paulson@2039
|
186 |
\item[\ttindexbold{dtac} {\it thm} {\it i}]
|
paulson@2039
|
187 |
abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
|
paulson@2039
|
188 |
destruct-resolution.
|
paulson@2039
|
189 |
|
paulson@2039
|
190 |
\item[\ttindexbold{atac} {\it i}]
|
paulson@2039
|
191 |
abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
|
paulson@2039
|
192 |
|
paulson@2039
|
193 |
\item[\ttindexbold{ares_tac} {\it thms} {\it i}]
|
paulson@2039
|
194 |
tries proof by assumption and resolution; it abbreviates
|
paulson@2039
|
195 |
\begin{ttbox}
|
paulson@2039
|
196 |
assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}
|
paulson@2039
|
197 |
\end{ttbox}
|
paulson@2039
|
198 |
|
paulson@2039
|
199 |
\item[\ttindexbold{rewtac} {\it def}]
|
paulson@2039
|
200 |
abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.
|
paulson@2039
|
201 |
\end{ttdescription}
|
paulson@2039
|
202 |
|
paulson@2039
|
203 |
|
paulson@2039
|
204 |
\subsection{Inserting premises and facts}\label{cut_facts_tac}
|
paulson@2039
|
205 |
\index{tactics!for inserting facts}\index{assumptions!inserting}
|
paulson@2039
|
206 |
\begin{ttbox}
|
paulson@2039
|
207 |
cut_facts_tac : thm list -> int -> tactic
|
paulson@2039
|
208 |
cut_inst_tac : (string*string)list -> thm -> int -> tactic
|
paulson@2039
|
209 |
subgoal_tac : string -> int -> tactic
|
paulson@2039
|
210 |
subgoal_tacs : string list -> int -> tactic
|
paulson@2039
|
211 |
\end{ttbox}
|
paulson@2039
|
212 |
These tactics add assumptions to a subgoal.
|
paulson@2039
|
213 |
\begin{ttdescription}
|
paulson@2039
|
214 |
\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}]
|
paulson@2039
|
215 |
adds the {\it thms} as new assumptions to subgoal~$i$. Once they have
|
paulson@2039
|
216 |
been inserted as assumptions, they become subject to tactics such as {\tt
|
paulson@2039
|
217 |
eresolve_tac} and {\tt rewrite_goals_tac}. Only rules with no premises
|
paulson@2039
|
218 |
are inserted: Isabelle cannot use assumptions that contain $\Imp$
|
paulson@2039
|
219 |
or~$\Forall$. Sometimes the theorems are premises of a rule being
|
paulson@2039
|
220 |
derived, returned by~{\tt goal}; instead of calling this tactic, you
|
paulson@2039
|
221 |
could state the goal with an outermost meta-quantifier.
|
paulson@2039
|
222 |
|
paulson@2039
|
223 |
\item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
|
paulson@2039
|
224 |
instantiates the {\it thm} with the instantiations {\it insts}, as
|
paulson@2039
|
225 |
described in \S\ref{res_inst_tac}. It adds the resulting theorem as a
|
paulson@2039
|
226 |
new assumption to subgoal~$i$.
|
paulson@2039
|
227 |
|
paulson@2039
|
228 |
\item[\ttindexbold{subgoal_tac} {\it formula} {\it i}]
|
paulson@2039
|
229 |
adds the {\it formula} as a assumption to subgoal~$i$, and inserts the same
|
paulson@2039
|
230 |
{\it formula} as a new subgoal, $i+1$.
|
paulson@2039
|
231 |
|
paulson@2039
|
232 |
\item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}]
|
paulson@2039
|
233 |
uses {\tt subgoal_tac} to add the members of the list of {\it
|
paulson@2039
|
234 |
formulae} as assumptions to subgoal~$i$.
|
paulson@2039
|
235 |
\end{ttdescription}
|
paulson@2039
|
236 |
|
paulson@2039
|
237 |
|
paulson@2039
|
238 |
\subsection{``Putting off'' a subgoal}
|
paulson@2039
|
239 |
\begin{ttbox}
|
paulson@2039
|
240 |
defer_tac : int -> tactic
|
paulson@2039
|
241 |
\end{ttbox}
|
paulson@2039
|
242 |
\begin{ttdescription}
|
paulson@2039
|
243 |
\item[\ttindexbold{defer_tac} {\it i}]
|
paulson@2039
|
244 |
moves subgoal~$i$ to the last position in the proof state. It can be
|
paulson@2039
|
245 |
useful when correcting a proof script: if the tactic given for subgoal~$i$
|
paulson@2039
|
246 |
fails, calling {\tt defer_tac} instead will let you continue with the rest
|
paulson@2039
|
247 |
of the script.
|
paulson@2039
|
248 |
|
paulson@2039
|
249 |
The tactic fails if subgoal~$i$ does not exist or if the proof state
|
paulson@2039
|
250 |
contains type unknowns.
|
paulson@2039
|
251 |
\end{ttdescription}
|
paulson@2039
|
252 |
|
paulson@2039
|
253 |
|
lcp@104
|
254 |
\subsection{Definitions and meta-level rewriting}
|
lcp@323
|
255 |
\index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
|
lcp@323
|
256 |
\index{definitions}
|
lcp@323
|
257 |
|
lcp@332
|
258 |
Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
|
lcp@104
|
259 |
constant or a constant applied to a list of variables, for example $\it
|
lcp@104
|
260 |
sqr(n)\equiv n\times n$. (Conditional definitions, $\phi\Imp t\equiv u$,
|
lcp@332
|
261 |
are not supported.) {\bf Unfolding} the definition ${t\equiv u}$ means using
|
lcp@104
|
262 |
it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem. {\bf
|
lcp@104
|
263 |
Folding} $t\equiv u$ means replacing~$u$ by~$t$. Rewriting continues until
|
lcp@104
|
264 |
no rewrites are applicable to any subterm.
|
lcp@104
|
265 |
|
lcp@104
|
266 |
There are rules for unfolding and folding definitions; Isabelle does not do
|
lcp@104
|
267 |
this automatically. The corresponding tactics rewrite the proof state,
|
lcp@332
|
268 |
yielding a single next state. See also the {\tt goalw} command, which is the
|
lcp@104
|
269 |
easiest way of handling definitions.
|
lcp@104
|
270 |
\begin{ttbox}
|
lcp@104
|
271 |
rewrite_goals_tac : thm list -> tactic
|
lcp@104
|
272 |
rewrite_tac : thm list -> tactic
|
lcp@104
|
273 |
fold_goals_tac : thm list -> tactic
|
lcp@104
|
274 |
fold_tac : thm list -> tactic
|
lcp@104
|
275 |
\end{ttbox}
|
lcp@323
|
276 |
\begin{ttdescription}
|
lcp@104
|
277 |
\item[\ttindexbold{rewrite_goals_tac} {\it defs}]
|
lcp@104
|
278 |
unfolds the {\it defs} throughout the subgoals of the proof state, while
|
lcp@104
|
279 |
leaving the main goal unchanged. Use \ttindex{SELECT_GOAL} to restrict it to a
|
lcp@104
|
280 |
particular subgoal.
|
lcp@104
|
281 |
|
lcp@104
|
282 |
\item[\ttindexbold{rewrite_tac} {\it defs}]
|
lcp@104
|
283 |
unfolds the {\it defs} throughout the proof state, including the main goal
|
lcp@104
|
284 |
--- not normally desirable!
|
lcp@104
|
285 |
|
lcp@104
|
286 |
\item[\ttindexbold{fold_goals_tac} {\it defs}]
|
lcp@104
|
287 |
folds the {\it defs} throughout the subgoals of the proof state, while
|
lcp@104
|
288 |
leaving the main goal unchanged.
|
lcp@104
|
289 |
|
lcp@104
|
290 |
\item[\ttindexbold{fold_tac} {\it defs}]
|
lcp@104
|
291 |
folds the {\it defs} throughout the proof state.
|
lcp@323
|
292 |
\end{ttdescription}
|
lcp@104
|
293 |
|
lcp@104
|
294 |
|
lcp@104
|
295 |
\subsection{Theorems useful with tactics}
|
lcp@323
|
296 |
\index{theorems!of pure theory}
|
lcp@104
|
297 |
\begin{ttbox}
|
lcp@104
|
298 |
asm_rl: thm
|
lcp@104
|
299 |
cut_rl: thm
|
lcp@104
|
300 |
\end{ttbox}
|
lcp@323
|
301 |
\begin{ttdescription}
|
lcp@323
|
302 |
\item[\tdx{asm_rl}]
|
lcp@104
|
303 |
is $\psi\Imp\psi$. Under elim-resolution it does proof by assumption, and
|
lcp@104
|
304 |
\hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to
|
lcp@104
|
305 |
\begin{ttbox}
|
lcp@104
|
306 |
assume_tac {\it i} ORELSE eresolve_tac {\it thms} {\it i}
|
lcp@104
|
307 |
\end{ttbox}
|
lcp@104
|
308 |
|
lcp@323
|
309 |
\item[\tdx{cut_rl}]
|
lcp@104
|
310 |
is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting
|
lcp@323
|
311 |
assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}
|
lcp@323
|
312 |
and {\tt subgoal_tac}.
|
lcp@323
|
313 |
\end{ttdescription}
|
lcp@104
|
314 |
|
lcp@104
|
315 |
|
lcp@104
|
316 |
\section{Obscure tactics}
|
nipkow@1212
|
317 |
|
lcp@323
|
318 |
\subsection{Renaming parameters in a goal} \index{parameters!renaming}
|
lcp@104
|
319 |
\begin{ttbox}
|
lcp@104
|
320 |
rename_tac : string -> int -> tactic
|
lcp@104
|
321 |
rename_last_tac : string -> string list -> int -> tactic
|
lcp@104
|
322 |
Logic.set_rename_prefix : string -> unit
|
lcp@104
|
323 |
Logic.auto_rename : bool ref \hfill{\bf initially false}
|
lcp@104
|
324 |
\end{ttbox}
|
lcp@104
|
325 |
When creating a parameter, Isabelle chooses its name by matching variable
|
lcp@104
|
326 |
names via the object-rule. Given the rule $(\forall I)$ formalized as
|
lcp@104
|
327 |
$\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note that
|
lcp@104
|
328 |
the $\Forall$-bound variable in the premise has the same name as the
|
lcp@104
|
329 |
$\forall$-bound variable in the conclusion.
|
lcp@104
|
330 |
|
lcp@104
|
331 |
Sometimes there is insufficient information and Isabelle chooses an
|
lcp@104
|
332 |
arbitrary name. The renaming tactics let you override Isabelle's choice.
|
lcp@104
|
333 |
Because renaming parameters has no logical effect on the proof state, the
|
lcp@323
|
334 |
{\tt by} command prints the message {\tt Warning:\ same as previous
|
lcp@104
|
335 |
level}.
|
lcp@104
|
336 |
|
lcp@104
|
337 |
Alternatively, you can suppress the naming mechanism described above and
|
lcp@104
|
338 |
have Isabelle generate uniform names for parameters. These names have the
|
lcp@104
|
339 |
form $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desired
|
lcp@104
|
340 |
prefix. They are ugly but predictable.
|
lcp@104
|
341 |
|
lcp@323
|
342 |
\begin{ttdescription}
|
lcp@104
|
343 |
\item[\ttindexbold{rename_tac} {\it str} {\it i}]
|
lcp@104
|
344 |
interprets the string {\it str} as a series of blank-separated variable
|
lcp@104
|
345 |
names, and uses them to rename the parameters of subgoal~$i$. The names
|
lcp@104
|
346 |
must be distinct. If there are fewer names than parameters, then the
|
lcp@104
|
347 |
tactic renames the innermost parameters and may modify the remaining ones
|
lcp@104
|
348 |
to ensure that all the parameters are distinct.
|
lcp@104
|
349 |
|
lcp@104
|
350 |
\item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}]
|
lcp@104
|
351 |
generates a list of names by attaching each of the {\it suffixes\/} to the
|
lcp@104
|
352 |
{\it prefix}. It is intended for coding structural induction tactics,
|
lcp@104
|
353 |
where several of the new parameters should have related names.
|
lcp@104
|
354 |
|
lcp@104
|
355 |
\item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};]
|
lcp@104
|
356 |
sets the prefix for uniform renaming to~{\it prefix}. The default prefix
|
lcp@104
|
357 |
is {\tt"k"}.
|
lcp@104
|
358 |
|
lcp@323
|
359 |
\item[\ttindexbold{Logic.auto_rename} := true;]
|
lcp@104
|
360 |
makes Isabelle generate uniform names for parameters.
|
lcp@323
|
361 |
\end{ttdescription}
|
lcp@104
|
362 |
|
lcp@104
|
363 |
|
paulson@2612
|
364 |
\subsection{Manipulating assumptions}
|
paulson@2612
|
365 |
\index{assumptions!rotating}
|
paulson@2612
|
366 |
\begin{ttbox}
|
paulson@2612
|
367 |
thin_tac : string -> int -> tactic
|
paulson@2612
|
368 |
rotate_tac : int -> int -> tactic
|
paulson@2612
|
369 |
\end{ttbox}
|
paulson@2612
|
370 |
\begin{ttdescription}
|
paulson@2612
|
371 |
\item[\ttindexbold{thin_tac} {\it formula} $i$]
|
paulson@2612
|
372 |
\index{assumptions!deleting}
|
paulson@2612
|
373 |
deletes the specified assumption from subgoal $i$. Often the assumption
|
paulson@2612
|
374 |
can be abbreviated, replacing subformul{\ae} by unknowns; the first matching
|
paulson@2612
|
375 |
assumption will be deleted. Removing useless assumptions from a subgoal
|
paulson@2612
|
376 |
increases its readability and can make search tactics run faster.
|
paulson@2612
|
377 |
|
paulson@2612
|
378 |
\item[\ttindexbold{rotate_tac} $n$ $i$]
|
paulson@2612
|
379 |
\index{assumptions!rotating}
|
paulson@2612
|
380 |
rotates the assumptions of subgoal $i$ by $n$ positions: from right to left
|
paulson@2612
|
381 |
if $n$ is positive, and from left to right if $n$ is negative. This is
|
paulson@2612
|
382 |
sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which
|
paulson@2612
|
383 |
processes assumptions from left to right.
|
paulson@2612
|
384 |
\end{ttdescription}
|
paulson@2612
|
385 |
|
paulson@2612
|
386 |
|
paulson@2612
|
387 |
\subsection{Tidying the proof state}
|
paulson@3400
|
388 |
\index{duplicate subgoals!removing}
|
paulson@2612
|
389 |
\index{parameters!removing unused}
|
paulson@2612
|
390 |
\index{flex-flex constraints}
|
paulson@2612
|
391 |
\begin{ttbox}
|
paulson@3400
|
392 |
distinct_subgoals_tac : tactic
|
paulson@3400
|
393 |
prune_params_tac : tactic
|
paulson@3400
|
394 |
flexflex_tac : tactic
|
paulson@2612
|
395 |
\end{ttbox}
|
paulson@2612
|
396 |
\begin{ttdescription}
|
paulson@3400
|
397 |
\item[\ttindexbold{distinct_subgoals_tac}]
|
paulson@3400
|
398 |
removes duplicate subgoals from a proof state. (These arise especially
|
paulson@3400
|
399 |
in \ZF{}, where the subgoals are essentially type constraints.)
|
paulson@3400
|
400 |
|
paulson@2612
|
401 |
\item[\ttindexbold{prune_params_tac}]
|
paulson@2612
|
402 |
removes unused parameters from all subgoals of the proof state. It works
|
paulson@2612
|
403 |
by rewriting with the theorem $(\Forall x. V)\equiv V$. This tactic can
|
paulson@2612
|
404 |
make the proof state more readable. It is used with
|
paulson@2612
|
405 |
\ttindex{rule_by_tactic} to simplify the resulting theorem.
|
paulson@2612
|
406 |
|
paulson@2612
|
407 |
\item[\ttindexbold{flexflex_tac}]
|
paulson@2612
|
408 |
removes all flex-flex pairs from the proof state by applying the trivial
|
paulson@2612
|
409 |
unifier. This drastic step loses information, and should only be done as
|
paulson@2612
|
410 |
the last step of a proof.
|
paulson@2612
|
411 |
|
paulson@2612
|
412 |
Flex-flex constraints arise from difficult cases of higher-order
|
paulson@2612
|
413 |
unification. To prevent this, use \ttindex{res_inst_tac} to instantiate
|
paulson@2612
|
414 |
some variables in a rule~(\S\ref{res_inst_tac}). Normally flex-flex
|
paulson@2612
|
415 |
constraints can be ignored; they often disappear as unknowns get
|
paulson@2612
|
416 |
instantiated.
|
paulson@2612
|
417 |
\end{ttdescription}
|
paulson@2612
|
418 |
|
paulson@2612
|
419 |
|
lcp@104
|
420 |
\subsection{Composition: resolution without lifting}
|
lcp@323
|
421 |
\index{tactics!for composition}
|
lcp@104
|
422 |
\begin{ttbox}
|
lcp@104
|
423 |
compose_tac: (bool * thm * int) -> int -> tactic
|
lcp@104
|
424 |
\end{ttbox}
|
lcp@332
|
425 |
{\bf Composing} two rules means resolving them without prior lifting or
|
lcp@104
|
426 |
renaming of unknowns. This low-level operation, which underlies the
|
lcp@104
|
427 |
resolution tactics, may occasionally be useful for special effects.
|
lcp@104
|
428 |
A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
|
lcp@104
|
429 |
rule, then passes the result to {\tt compose_tac}.
|
lcp@323
|
430 |
\begin{ttdescription}
|
lcp@104
|
431 |
\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$]
|
lcp@104
|
432 |
refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to
|
lcp@104
|
433 |
have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
|
lcp@323
|
434 |
not be atomic; thus $m$ determines the number of new subgoals. If
|
lcp@104
|
435 |
$flag$ is {\tt true} then it performs elim-resolution --- it solves the
|
lcp@104
|
436 |
first premise of~$rule$ by assumption and deletes that assumption.
|
lcp@323
|
437 |
\end{ttdescription}
|
lcp@104
|
438 |
|
lcp@104
|
439 |
|
wenzelm@4276
|
440 |
\section{*Managing lots of rules}
|
lcp@104
|
441 |
These operations are not intended for interactive use. They are concerned
|
lcp@104
|
442 |
with the processing of large numbers of rules in automatic proof
|
lcp@104
|
443 |
strategies. Higher-order resolution involving a long list of rules is
|
lcp@104
|
444 |
slow. Filtering techniques can shorten the list of rules given to
|
paulson@2039
|
445 |
resolution, and can also detect whether a subgoal is too flexible,
|
lcp@104
|
446 |
with too many rules applicable.
|
lcp@104
|
447 |
|
lcp@104
|
448 |
\subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
|
lcp@104
|
449 |
\index{tactics!resolution}
|
lcp@104
|
450 |
\begin{ttbox}
|
lcp@104
|
451 |
biresolve_tac : (bool*thm)list -> int -> tactic
|
lcp@104
|
452 |
bimatch_tac : (bool*thm)list -> int -> tactic
|
lcp@104
|
453 |
subgoals_of_brl : bool*thm -> int
|
lcp@104
|
454 |
lessb : (bool*thm) * (bool*thm) -> bool
|
lcp@104
|
455 |
\end{ttbox}
|
lcp@104
|
456 |
{\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs. For each
|
lcp@104
|
457 |
pair, it applies resolution if the flag is~{\tt false} and
|
lcp@104
|
458 |
elim-resolution if the flag is~{\tt true}. A single tactic call handles a
|
lcp@104
|
459 |
mixture of introduction and elimination rules.
|
lcp@104
|
460 |
|
lcp@323
|
461 |
\begin{ttdescription}
|
lcp@104
|
462 |
\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}]
|
lcp@104
|
463 |
refines the proof state by resolution or elim-resolution on each rule, as
|
lcp@104
|
464 |
indicated by its flag. It affects subgoal~$i$ of the proof state.
|
lcp@104
|
465 |
|
lcp@104
|
466 |
\item[\ttindexbold{bimatch_tac}]
|
lcp@104
|
467 |
is like {\tt biresolve_tac}, but performs matching: unknowns in the
|
lcp@104
|
468 |
proof state are never updated (see~\S\ref{match_tac}).
|
lcp@104
|
469 |
|
lcp@104
|
470 |
\item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})]
|
lcp@104
|
471 |
returns the number of new subgoals that bi-resolution would yield for the
|
lcp@104
|
472 |
pair (if applied to a suitable subgoal). This is $n$ if the flag is
|
lcp@104
|
473 |
{\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
|
lcp@104
|
474 |
of premises of the rule. Elim-resolution yields one fewer subgoal than
|
lcp@104
|
475 |
ordinary resolution because it solves the major premise by assumption.
|
lcp@104
|
476 |
|
lcp@104
|
477 |
\item[\ttindexbold{lessb} ({\it brl1},{\it brl2})]
|
lcp@104
|
478 |
returns the result of
|
lcp@104
|
479 |
\begin{ttbox}
|
lcp@332
|
480 |
subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
|
lcp@104
|
481 |
\end{ttbox}
|
lcp@323
|
482 |
\end{ttdescription}
|
lcp@104
|
483 |
Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
|
lcp@104
|
484 |
(flag,rule)$ pairs by the number of new subgoals they will yield. Thus,
|
lcp@104
|
485 |
those that yield the fewest subgoals should be tried first.
|
lcp@104
|
486 |
|
lcp@104
|
487 |
|
lcp@323
|
488 |
\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}
|
lcp@104
|
489 |
\index{discrimination nets|bold}
|
lcp@104
|
490 |
\index{tactics!resolution}
|
lcp@104
|
491 |
\begin{ttbox}
|
lcp@104
|
492 |
net_resolve_tac : thm list -> int -> tactic
|
lcp@104
|
493 |
net_match_tac : thm list -> int -> tactic
|
lcp@104
|
494 |
net_biresolve_tac: (bool*thm) list -> int -> tactic
|
lcp@104
|
495 |
net_bimatch_tac : (bool*thm) list -> int -> tactic
|
lcp@104
|
496 |
filt_resolve_tac : thm list -> int -> int -> tactic
|
lcp@104
|
497 |
could_unify : term*term->bool
|
lcp@104
|
498 |
filter_thms : (term*term->bool) -> int*term*thm list -> thm list
|
lcp@104
|
499 |
\end{ttbox}
|
lcp@323
|
500 |
The module {\tt Net} implements a discrimination net data structure for
|
lcp@104
|
501 |
fast selection of rules \cite[Chapter 14]{charniak80}. A term is
|
lcp@104
|
502 |
classified by the symbol list obtained by flattening it in preorder.
|
lcp@104
|
503 |
The flattening takes account of function applications, constants, and free
|
lcp@104
|
504 |
and bound variables; it identifies all unknowns and also regards
|
lcp@323
|
505 |
\index{lambda abs@$\lambda$-abstractions}
|
lcp@104
|
506 |
$\lambda$-abstractions as unknowns, since they could $\eta$-contract to
|
lcp@104
|
507 |
anything.
|
lcp@104
|
508 |
|
lcp@104
|
509 |
A discrimination net serves as a polymorphic dictionary indexed by terms.
|
lcp@104
|
510 |
The module provides various functions for inserting and removing items from
|
lcp@104
|
511 |
nets. It provides functions for returning all items whose term could match
|
lcp@104
|
512 |
or unify with a target term. The matching and unification tests are
|
lcp@104
|
513 |
overly lax (due to the identifications mentioned above) but they serve as
|
lcp@104
|
514 |
useful filters.
|
lcp@104
|
515 |
|
lcp@104
|
516 |
A net can store introduction rules indexed by their conclusion, and
|
lcp@104
|
517 |
elimination rules indexed by their major premise. Isabelle provides
|
lcp@323
|
518 |
several functions for `compiling' long lists of rules into fast
|
lcp@104
|
519 |
resolution tactics. When supplied with a list of theorems, these functions
|
lcp@104
|
520 |
build a discrimination net; the net is used when the tactic is applied to a
|
lcp@332
|
521 |
goal. To avoid repeatedly constructing the nets, use currying: bind the
|
lcp@104
|
522 |
resulting tactics to \ML{} identifiers.
|
lcp@104
|
523 |
|
lcp@323
|
524 |
\begin{ttdescription}
|
lcp@104
|
525 |
\item[\ttindexbold{net_resolve_tac} {\it thms}]
|
lcp@104
|
526 |
builds a discrimination net to obtain the effect of a similar call to {\tt
|
lcp@104
|
527 |
resolve_tac}.
|
lcp@104
|
528 |
|
lcp@104
|
529 |
\item[\ttindexbold{net_match_tac} {\it thms}]
|
lcp@104
|
530 |
builds a discrimination net to obtain the effect of a similar call to {\tt
|
lcp@104
|
531 |
match_tac}.
|
lcp@104
|
532 |
|
lcp@104
|
533 |
\item[\ttindexbold{net_biresolve_tac} {\it brls}]
|
lcp@104
|
534 |
builds a discrimination net to obtain the effect of a similar call to {\tt
|
lcp@104
|
535 |
biresolve_tac}.
|
lcp@104
|
536 |
|
lcp@104
|
537 |
\item[\ttindexbold{net_bimatch_tac} {\it brls}]
|
lcp@104
|
538 |
builds a discrimination net to obtain the effect of a similar call to {\tt
|
lcp@104
|
539 |
bimatch_tac}.
|
lcp@104
|
540 |
|
lcp@104
|
541 |
\item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}]
|
lcp@104
|
542 |
uses discrimination nets to extract the {\it thms} that are applicable to
|
lcp@104
|
543 |
subgoal~$i$. If more than {\it maxr\/} theorems are applicable then the
|
lcp@104
|
544 |
tactic fails. Otherwise it calls {\tt resolve_tac}.
|
lcp@104
|
545 |
|
lcp@104
|
546 |
This tactic helps avoid runaway instantiation of unknowns, for example in
|
lcp@104
|
547 |
type inference.
|
lcp@104
|
548 |
|
lcp@104
|
549 |
\item[\ttindexbold{could_unify} ({\it t},{\it u})]
|
lcp@323
|
550 |
returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and
|
lcp@104
|
551 |
otherwise returns~{\tt true}. It assumes all variables are distinct,
|
lcp@104
|
552 |
reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
|
lcp@104
|
553 |
|
lcp@104
|
554 |
\item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$]
|
lcp@104
|
555 |
returns the list of potentially resolvable rules (in {\it thms\/}) for the
|
lcp@104
|
556 |
subgoal {\it prem}, using the predicate {\it could\/} to compare the
|
lcp@104
|
557 |
conclusion of the subgoal with the conclusion of each rule. The resulting list
|
lcp@104
|
558 |
is no longer than {\it limit}.
|
lcp@323
|
559 |
\end{ttdescription}
|
lcp@104
|
560 |
|
lcp@104
|
561 |
|
wenzelm@4276
|
562 |
\section{*Programming tools for proof strategies}
|
lcp@104
|
563 |
Do not consider using the primitives discussed in this section unless you
|
lcp@323
|
564 |
really need to code tactics from scratch.
|
lcp@104
|
565 |
|
lcp@104
|
566 |
\subsection{Operations on type {\tt tactic}}
|
paulson@3561
|
567 |
\index{tactics!primitives for coding} A tactic maps theorems to sequences of
|
paulson@3561
|
568 |
theorems. The type constructor for sequences (lazy lists) is called
|
wenzelm@4276
|
569 |
\mltydx{Seq.seq}. To simplify the types of tactics and tacticals,
|
paulson@3561
|
570 |
Isabelle defines a type abbreviation:
|
lcp@104
|
571 |
\begin{ttbox}
|
wenzelm@4276
|
572 |
type tactic = thm -> thm Seq.seq
|
lcp@104
|
573 |
\end{ttbox}
|
wenzelm@3108
|
574 |
The following operations provide means for coding tactics in a clean style.
|
lcp@104
|
575 |
\begin{ttbox}
|
lcp@104
|
576 |
PRIMITIVE : (thm -> thm) -> tactic
|
lcp@104
|
577 |
SUBGOAL : ((term*int) -> tactic) -> int -> tactic
|
lcp@104
|
578 |
\end{ttbox}
|
lcp@323
|
579 |
\begin{ttdescription}
|
paulson@3561
|
580 |
\item[\ttindexbold{PRIMITIVE} $f$] packages the meta-rule~$f$ as a tactic that
|
paulson@3561
|
581 |
applies $f$ to the proof state and returns the result as a one-element
|
paulson@3561
|
582 |
sequence. If $f$ raises an exception, then the tactic's result is the empty
|
paulson@3561
|
583 |
sequence.
|
lcp@104
|
584 |
|
lcp@104
|
585 |
\item[\ttindexbold{SUBGOAL} $f$ $i$]
|
lcp@104
|
586 |
extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
|
lcp@104
|
587 |
tactic by calling~$f(t,i)$. It applies the resulting tactic to the same
|
lcp@323
|
588 |
state. The tactic body is expressed using tactics and tacticals, but may
|
lcp@323
|
589 |
peek at a particular subgoal:
|
lcp@104
|
590 |
\begin{ttbox}
|
lcp@323
|
591 |
SUBGOAL (fn (t,i) => {\it tactic-valued expression})
|
lcp@104
|
592 |
\end{ttbox}
|
lcp@323
|
593 |
\end{ttdescription}
|
lcp@104
|
594 |
|
lcp@104
|
595 |
|
lcp@104
|
596 |
\subsection{Tracing}
|
lcp@323
|
597 |
\index{tactics!tracing}
|
lcp@104
|
598 |
\index{tracing!of tactics}
|
lcp@104
|
599 |
\begin{ttbox}
|
lcp@104
|
600 |
pause_tac: tactic
|
lcp@104
|
601 |
print_tac: tactic
|
lcp@104
|
602 |
\end{ttbox}
|
lcp@332
|
603 |
These tactics print tracing information when they are applied to a proof
|
lcp@332
|
604 |
state. Their output may be difficult to interpret. Note that certain of
|
lcp@332
|
605 |
the searching tacticals, such as {\tt REPEAT}, have built-in tracing
|
lcp@332
|
606 |
options.
|
lcp@323
|
607 |
\begin{ttdescription}
|
lcp@104
|
608 |
\item[\ttindexbold{pause_tac}]
|
lcp@332
|
609 |
prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line
|
lcp@332
|
610 |
from the terminal. If this line is blank then it returns the proof state
|
lcp@332
|
611 |
unchanged; otherwise it fails (which may terminate a repetition).
|
lcp@104
|
612 |
|
lcp@104
|
613 |
\item[\ttindexbold{print_tac}]
|
lcp@104
|
614 |
returns the proof state unchanged, with the side effect of printing it at
|
lcp@104
|
615 |
the terminal.
|
lcp@323
|
616 |
\end{ttdescription}
|
lcp@104
|
617 |
|
lcp@104
|
618 |
|
wenzelm@4276
|
619 |
\section{*Sequences}
|
lcp@104
|
620 |
\index{sequences (lazy lists)|bold}
|
wenzelm@4276
|
621 |
The module {\tt Seq} declares a type of lazy lists. It uses
|
lcp@323
|
622 |
Isabelle's type \mltydx{option} to represent the possible presence
|
lcp@104
|
623 |
(\ttindexbold{Some}) or absence (\ttindexbold{None}) of
|
lcp@104
|
624 |
a value:
|
lcp@104
|
625 |
\begin{ttbox}
|
lcp@104
|
626 |
datatype 'a option = None | Some of 'a;
|
lcp@104
|
627 |
\end{ttbox}
|
wenzelm@4276
|
628 |
The {\tt Seq} structure is supposed to be accessed via fully qualified
|
wenzelm@4276
|
629 |
names and should not be \texttt{open}ed.
|
lcp@104
|
630 |
|
lcp@323
|
631 |
\subsection{Basic operations on sequences}
|
lcp@104
|
632 |
\begin{ttbox}
|
wenzelm@4276
|
633 |
Seq.empty : 'a seq
|
wenzelm@4276
|
634 |
Seq.make : (unit -> ('a * 'a seq) option) -> 'a seq
|
wenzelm@4276
|
635 |
Seq.single : 'a -> 'a seq
|
wenzelm@4276
|
636 |
Seq.pull : 'a seq -> ('a * 'a seq) option
|
lcp@104
|
637 |
\end{ttbox}
|
lcp@323
|
638 |
\begin{ttdescription}
|
wenzelm@4276
|
639 |
\item[Seq.empty] is the empty sequence.
|
lcp@104
|
640 |
|
wenzelm@4276
|
641 |
\item[\tt Seq.make (fn () => Some ($x$, $xq$))] constructs the
|
wenzelm@4276
|
642 |
sequence with head~$x$ and tail~$xq$, neither of which is evaluated.
|
lcp@104
|
643 |
|
wenzelm@4276
|
644 |
\item[Seq.single $x$]
|
lcp@104
|
645 |
constructs the sequence containing the single element~$x$.
|
lcp@104
|
646 |
|
wenzelm@4276
|
647 |
\item[Seq.pull $xq$] returns {\tt None} if the sequence is empty and
|
wenzelm@4276
|
648 |
{\tt Some ($x$, $xq'$)} if the sequence has head~$x$ and tail~$xq'$.
|
wenzelm@4276
|
649 |
Warning: calling \hbox{Seq.pull $xq$} again will {\it recompute\/}
|
wenzelm@4276
|
650 |
the value of~$x$; it is not stored!
|
lcp@323
|
651 |
\end{ttdescription}
|
lcp@104
|
652 |
|
lcp@104
|
653 |
|
lcp@323
|
654 |
\subsection{Converting between sequences and lists}
|
lcp@104
|
655 |
\begin{ttbox}
|
wenzelm@4276
|
656 |
Seq.chop : int * 'a seq -> 'a list * 'a seq
|
wenzelm@4276
|
657 |
Seq.list_of : 'a seq -> 'a list
|
wenzelm@4276
|
658 |
Seq.of_list : 'a list -> 'a seq
|
lcp@104
|
659 |
\end{ttbox}
|
lcp@323
|
660 |
\begin{ttdescription}
|
wenzelm@4276
|
661 |
\item[Seq.chop ($n$, $xq$)] returns the first~$n$ elements of~$xq$ as a
|
wenzelm@4276
|
662 |
list, paired with the remaining elements of~$xq$. If $xq$ has fewer
|
wenzelm@4276
|
663 |
than~$n$ elements, then so will the list.
|
wenzelm@4276
|
664 |
|
wenzelm@4276
|
665 |
\item[Seq.list_of $xq$] returns the elements of~$xq$, which must be
|
wenzelm@4276
|
666 |
finite, as a list.
|
wenzelm@4276
|
667 |
|
wenzelm@4276
|
668 |
\item[Seq.of_list $xs$] creates a sequence containing the elements
|
wenzelm@4276
|
669 |
of~$xs$.
|
lcp@323
|
670 |
\end{ttdescription}
|
lcp@104
|
671 |
|
lcp@104
|
672 |
|
lcp@323
|
673 |
\subsection{Combining sequences}
|
lcp@104
|
674 |
\begin{ttbox}
|
wenzelm@4276
|
675 |
Seq.append : 'a seq * 'a seq -> 'a seq
|
wenzelm@4276
|
676 |
Seq.interleave : 'a seq * 'a seq -> 'a seq
|
wenzelm@4276
|
677 |
Seq.flat : 'a seq seq -> 'a seq
|
wenzelm@4276
|
678 |
Seq.map : ('a -> 'b) -> 'a seq -> 'b seq
|
wenzelm@4276
|
679 |
Seq.filter : ('a -> bool) -> 'a seq -> 'a seq
|
lcp@104
|
680 |
\end{ttbox}
|
lcp@323
|
681 |
\begin{ttdescription}
|
wenzelm@4276
|
682 |
\item[Seq.append ($xq$, $yq$)] concatenates $xq$ to $yq$.
|
wenzelm@4276
|
683 |
|
wenzelm@4276
|
684 |
\item[Seq.interleave ($xq$, $yq$)] joins $xq$ with $yq$ by
|
wenzelm@4276
|
685 |
interleaving their elements. The result contains all the elements
|
wenzelm@4276
|
686 |
of the sequences, even if both are infinite.
|
wenzelm@4276
|
687 |
|
wenzelm@4276
|
688 |
\item[Seq.flat $xqq$] concatenates a sequence of sequences.
|
wenzelm@4276
|
689 |
|
wenzelm@4276
|
690 |
\item[Seq.map $f$ $xq$] applies $f$ to every element
|
wenzelm@4276
|
691 |
of~$xq=x@1,x@2,\ldots$, yielding the sequence $f(x@1),f(x@2),\ldots$.
|
wenzelm@4276
|
692 |
|
wenzelm@4276
|
693 |
\item[Seq.filter $p$ $xq$] returns the sequence consisting of all
|
wenzelm@4276
|
694 |
elements~$x$ of~$xq$ such that $p(x)$ is {\tt true}.
|
lcp@323
|
695 |
\end{ttdescription}
|
lcp@104
|
696 |
|
lcp@104
|
697 |
\index{tactics|)}
|