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