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