1.1 --- a/doc-src/Ref/tactic.tex Sun Mar 01 12:37:59 2009 +0100
1.2 +++ b/doc-src/Ref/tactic.tex Sun Mar 01 13:48:17 2009 +0100
1.3 @@ -1,235 +1,8 @@
1.4 -%% $Id$
1.5 +
1.6 \chapter{Tactics} \label{tactics}
1.7 -\index{tactics|(} Tactics have type \mltydx{tactic}. This is just an
1.8 -abbreviation for functions from theorems to theorem sequences, where
1.9 -the theorems represent states of a backward proof. Tactics seldom
1.10 -need to be coded from scratch, as functions; instead they are
1.11 -expressed using basic tactics and tacticals.
1.12 -
1.13 -This chapter only presents the primitive tactics. Substantial proofs
1.14 -require the power of automatic tools like simplification
1.15 -(Chapter~\ref{chap:simplification}) and classical tableau reasoning
1.16 -(Chapter~\ref{chap:classical}).
1.17 -
1.18 -\section{Resolution and assumption tactics}
1.19 -{\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
1.20 -a rule. {\bf Elim-resolution} is particularly suited for elimination
1.21 -rules, while {\bf destruct-resolution} is particularly suited for
1.22 -destruction rules. The {\tt r}, {\tt e}, {\tt d} naming convention is
1.23 -maintained for several different kinds of resolution tactics, as well as
1.24 -the shortcuts in the subgoal module.
1.25 -
1.26 -All the tactics in this section act on a subgoal designated by a positive
1.27 -integer~$i$. They fail (by returning the empty sequence) if~$i$ is out of
1.28 -range.
1.29 -
1.30 -\subsection{Resolution tactics}
1.31 -\index{resolution!tactics}
1.32 -\index{tactics!resolution|bold}
1.33 -\begin{ttbox}
1.34 -resolve_tac : thm list -> int -> tactic
1.35 -eresolve_tac : thm list -> int -> tactic
1.36 -dresolve_tac : thm list -> int -> tactic
1.37 -forward_tac : thm list -> int -> tactic
1.38 -\end{ttbox}
1.39 -These perform resolution on a list of theorems, $thms$, representing a list
1.40 -of object-rules. When generating next states, they take each of the rules
1.41 -in the order given. Each rule may yield several next states, or none:
1.42 -higher-order resolution may yield multiple resolvents.
1.43 -\begin{ttdescription}
1.44 -\item[\ttindexbold{resolve_tac} {\it thms} {\it i}]
1.45 - refines the proof state using the rules, which should normally be
1.46 - introduction rules. It resolves a rule's conclusion with
1.47 - subgoal~$i$ of the proof state.
1.48 -
1.49 -\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}]
1.50 - \index{elim-resolution}
1.51 - performs elim-resolution with the rules, which should normally be
1.52 - elimination rules. It resolves with a rule, proves its first premise by
1.53 - assumption, and finally \emph{deletes} that assumption from any new
1.54 - subgoals. (To rotate a rule's premises,
1.55 - see \texttt{rotate_prems} in~{\S}\ref{MiscellaneousForwardRules}.)
1.56 -
1.57 -\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}]
1.58 - \index{forward proof}\index{destruct-resolution}
1.59 - performs destruct-resolution with the rules, which normally should
1.60 - be destruction rules. This replaces an assumption by the result of
1.61 - applying one of the rules.
1.62 -
1.63 -\item[\ttindexbold{forward_tac}]\index{forward proof}
1.64 - is like {\tt dresolve_tac} except that the selected assumption is not
1.65 - deleted. It applies a rule to an assumption, adding the result as a new
1.66 - assumption.
1.67 -\end{ttdescription}
1.68 -
1.69 -\subsection{Assumption tactics}
1.70 -\index{tactics!assumption|bold}\index{assumptions!tactics for}
1.71 -\begin{ttbox}
1.72 -assume_tac : int -> tactic
1.73 -eq_assume_tac : int -> tactic
1.74 -\end{ttbox}
1.75 -\begin{ttdescription}
1.76 -\item[\ttindexbold{assume_tac} {\it i}]
1.77 -attempts to solve subgoal~$i$ by assumption.
1.78 -
1.79 -\item[\ttindexbold{eq_assume_tac}]
1.80 -is like {\tt assume_tac} but does not use unification. It succeeds (with a
1.81 -\emph{unique} next state) if one of the assumptions is identical to the
1.82 -subgoal's conclusion. Since it does not instantiate variables, it cannot
1.83 -make other subgoals unprovable. It is intended to be called from proof
1.84 -strategies, not interactively.
1.85 -\end{ttdescription}
1.86 -
1.87 -\subsection{Matching tactics} \label{match_tac}
1.88 -\index{tactics!matching}
1.89 -\begin{ttbox}
1.90 -match_tac : thm list -> int -> tactic
1.91 -ematch_tac : thm list -> int -> tactic
1.92 -dmatch_tac : thm list -> int -> tactic
1.93 -\end{ttbox}
1.94 -These are just like the resolution tactics except that they never
1.95 -instantiate unknowns in the proof state. Flexible subgoals are not updated
1.96 -willy-nilly, but are left alone. Matching --- strictly speaking --- means
1.97 -treating the unknowns in the proof state as constants; these tactics merely
1.98 -discard unifiers that would update the proof state.
1.99 -\begin{ttdescription}
1.100 -\item[\ttindexbold{match_tac} {\it thms} {\it i}]
1.101 -refines the proof state using the rules, matching a rule's
1.102 -conclusion with subgoal~$i$ of the proof state.
1.103 -
1.104 -\item[\ttindexbold{ematch_tac}]
1.105 -is like {\tt match_tac}, but performs elim-resolution.
1.106 -
1.107 -\item[\ttindexbold{dmatch_tac}]
1.108 -is like {\tt match_tac}, but performs destruct-resolution.
1.109 -\end{ttdescription}
1.110 -
1.111 -
1.112 -\subsection{Explicit instantiation} \label{res_inst_tac}
1.113 -\index{tactics!instantiation}\index{instantiation}
1.114 -\begin{ttbox}
1.115 -res_inst_tac : (string*string)list -> thm -> int -> tactic
1.116 -eres_inst_tac : (string*string)list -> thm -> int -> tactic
1.117 -dres_inst_tac : (string*string)list -> thm -> int -> tactic
1.118 -forw_inst_tac : (string*string)list -> thm -> int -> tactic
1.119 -instantiate_tac : (string*string)list -> tactic
1.120 -\end{ttbox}
1.121 -The first four of these tactics are designed for applying rules by resolution
1.122 -such as substitution and induction, which cause difficulties for higher-order
1.123 -unification. The tactics accept explicit instantiations for unknowns
1.124 -in the rule ---typically, in the rule's conclusion. The last one,
1.125 -{\tt instantiate_tac}, may be used to instantiate unknowns in the proof state,
1.126 -independently of rule application.
1.127 -
1.128 -Each instantiation is a pair {\tt($v$,$e$)},
1.129 -where $v$ is an unknown \emph{without} its leading question mark!
1.130 -\begin{itemize}
1.131 -\item If $v$ is the type unknown {\tt'a}, then
1.132 -the rule must contain a type unknown \verb$?'a$ of some
1.133 -sort~$s$, and $e$ should be a type of sort $s$.
1.134 -
1.135 -\item If $v$ is the unknown {\tt P}, then
1.136 -the rule must contain an unknown \verb$?P$ of some type~$\tau$,
1.137 -and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
1.138 -$\sigma$ are unifiable. If the unification of $\tau$ and $\sigma$
1.139 -instantiates any type unknowns in $\tau$, these instantiations
1.140 -are recorded for application to the rule.
1.141 -\end{itemize}
1.142 -Types are instantiated before terms are. Because type instantiations are
1.143 -inferred from term instantiations, explicit type instantiations are seldom
1.144 -necessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list
1.145 -\texttt{[("'a","bool"), ("t","True")]} may be simplified to
1.146 -\texttt{[("t","True")]}. Type unknowns in the proof state may cause
1.147 -failure because the tactics cannot instantiate them.
1.148 -
1.149 -The first four instantiation tactics act on a given subgoal. Terms in the
1.150 -instantiations are type-checked in the context of that subgoal --- in
1.151 -particular, they may refer to that subgoal's parameters. Any unknowns in
1.152 -the terms receive subscripts and are lifted over the parameters; thus, you
1.153 -may not refer to unknowns in the subgoal.
1.154 -
1.155 -\begin{ttdescription}
1.156 -\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
1.157 -instantiates the rule {\it thm} with the instantiations {\it insts}, as
1.158 -described above, and then performs resolution on subgoal~$i$. Resolution
1.159 -typically causes further instantiations; you need not give explicit
1.160 -instantiations for every unknown in the rule.
1.161 -
1.162 -\item[\ttindexbold{eres_inst_tac}]
1.163 -is like {\tt res_inst_tac}, but performs elim-resolution.
1.164 -
1.165 -\item[\ttindexbold{dres_inst_tac}]
1.166 -is like {\tt res_inst_tac}, but performs destruct-resolution.
1.167 -
1.168 -\item[\ttindexbold{forw_inst_tac}]
1.169 -is like {\tt dres_inst_tac} except that the selected assumption is not
1.170 -deleted. It applies the instantiated rule to an assumption, adding the
1.171 -result as a new assumption.
1.172 -
1.173 -\item[\ttindexbold{instantiate_tac} {\it insts}]
1.174 -instantiates unknowns in the proof state. This affects the main goal as
1.175 -well as all subgoals.
1.176 -\end{ttdescription}
1.177 -
1.178 +\index{tactics|(}
1.179
1.180 \section{Other basic tactics}
1.181 -\subsection{Tactic shortcuts}
1.182 -\index{shortcuts!for tactics}
1.183 -\index{tactics!resolution}\index{tactics!assumption}
1.184 -\index{tactics!meta-rewriting}
1.185 -\begin{ttbox}
1.186 -rtac : thm -> int -> tactic
1.187 -etac : thm -> int -> tactic
1.188 -dtac : thm -> int -> tactic
1.189 -ftac : thm -> int -> tactic
1.190 -atac : int -> tactic
1.191 -eatac : thm -> int -> int -> tactic
1.192 -datac : thm -> int -> int -> tactic
1.193 -fatac : thm -> int -> int -> tactic
1.194 -ares_tac : thm list -> int -> tactic
1.195 -rewtac : thm -> tactic
1.196 -\end{ttbox}
1.197 -These abbreviate common uses of tactics.
1.198 -\begin{ttdescription}
1.199 -\item[\ttindexbold{rtac} {\it thm} {\it i}]
1.200 -abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.
1.201 -
1.202 -\item[\ttindexbold{etac} {\it thm} {\it i}]
1.203 -abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.
1.204 -
1.205 -\item[\ttindexbold{dtac} {\it thm} {\it i}]
1.206 -abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
1.207 -destruct-resolution.
1.208 -
1.209 -\item[\ttindexbold{ftac} {\it thm} {\it i}]
1.210 -abbreviates \hbox{\tt forward_tac [{\it thm}] {\it i}}, doing
1.211 -destruct-resolution without deleting the assumption.
1.212 -
1.213 -\item[\ttindexbold{atac} {\it i}]
1.214 -abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
1.215 -
1.216 -\item[\ttindexbold{eatac} {\it thm} {\it j} {\it i}]
1.217 -performs \hbox{\tt etac {\it thm}} and then {\it j} times \texttt{atac},
1.218 -solving additionally {\it j}~premises of the rule {\it thm} by assumption.
1.219 -
1.220 -\item[\ttindexbold{datac} {\it thm} {\it j} {\it i}]
1.221 -performs \hbox{\tt dtac {\it thm}} and then {\it j} times \texttt{atac},
1.222 -solving additionally {\it j}~premises of the rule {\it thm} by assumption.
1.223 -
1.224 -\item[\ttindexbold{fatac} {\it thm} {\it j} {\it i}]
1.225 -performs \hbox{\tt ftac {\it thm}} and then {\it j} times \texttt{atac},
1.226 -solving additionally {\it j}~premises of the rule {\it thm} by assumption.
1.227 -
1.228 -\item[\ttindexbold{ares_tac} {\it thms} {\it i}]
1.229 -tries proof by assumption and resolution; it abbreviates
1.230 -\begin{ttbox}
1.231 -assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}
1.232 -\end{ttbox}
1.233 -
1.234 -\item[\ttindexbold{rewtac} {\it def}]
1.235 -abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.
1.236 -\end{ttdescription}
1.237 -
1.238
1.239 \subsection{Inserting premises and facts}\label{cut_facts_tac}
1.240 \index{tactics!for inserting facts}\index{assumptions!inserting}
1.241 @@ -351,52 +124,6 @@
1.242
1.243 \section{Obscure tactics}
1.244
1.245 -\subsection{Renaming parameters in a goal} \index{parameters!renaming}
1.246 -\begin{ttbox}
1.247 -rename_tac : string -> int -> tactic
1.248 -rename_last_tac : string -> string list -> int -> tactic
1.249 -Logic.set_rename_prefix : string -> unit
1.250 -Logic.auto_rename : bool ref \hfill{\bf initially false}
1.251 -\end{ttbox}
1.252 -When creating a parameter, Isabelle chooses its name by matching variable
1.253 -names via the object-rule. Given the rule $(\forall I)$ formalized as
1.254 -$\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note that
1.255 -the $\Forall$-bound variable in the premise has the same name as the
1.256 -$\forall$-bound variable in the conclusion.
1.257 -
1.258 -Sometimes there is insufficient information and Isabelle chooses an
1.259 -arbitrary name. The renaming tactics let you override Isabelle's choice.
1.260 -Because renaming parameters has no logical effect on the proof state, the
1.261 -{\tt by} command prints the message {\tt Warning:\ same as previous
1.262 -level}.
1.263 -
1.264 -Alternatively, you can suppress the naming mechanism described above and
1.265 -have Isabelle generate uniform names for parameters. These names have the
1.266 -form $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desired
1.267 -prefix. They are ugly but predictable.
1.268 -
1.269 -\begin{ttdescription}
1.270 -\item[\ttindexbold{rename_tac} {\it str} {\it i}]
1.271 -interprets the string {\it str} as a series of blank-separated variable
1.272 -names, and uses them to rename the parameters of subgoal~$i$. The names
1.273 -must be distinct. If there are fewer names than parameters, then the
1.274 -tactic renames the innermost parameters and may modify the remaining ones
1.275 -to ensure that all the parameters are distinct.
1.276 -
1.277 -\item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}]
1.278 -generates a list of names by attaching each of the {\it suffixes\/} to the
1.279 -{\it prefix}. It is intended for coding structural induction tactics,
1.280 -where several of the new parameters should have related names.
1.281 -
1.282 -\item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};]
1.283 -sets the prefix for uniform renaming to~{\it prefix}. The default prefix
1.284 -is {\tt"k"}.
1.285 -
1.286 -\item[set \ttindexbold{Logic.auto_rename};]
1.287 -makes Isabelle generate uniform names for parameters.
1.288 -\end{ttdescription}
1.289 -
1.290 -
1.291 \subsection{Manipulating assumptions}
1.292 \index{assumptions!rotating}
1.293 \begin{ttbox}
1.294 @@ -594,142 +321,6 @@
1.295 is no longer than {\it limit}.
1.296 \end{ttdescription}
1.297
1.298 -
1.299 -\section{Programming tools for proof strategies}
1.300 -Do not consider using the primitives discussed in this section unless you
1.301 -really need to code tactics from scratch.
1.302 -
1.303 -\subsection{Operations on tactics}
1.304 -\index{tactics!primitives for coding} A tactic maps theorems to sequences of
1.305 -theorems. The type constructor for sequences (lazy lists) is called
1.306 -\mltydx{Seq.seq}. To simplify the types of tactics and tacticals,
1.307 -Isabelle defines a type abbreviation:
1.308 -\begin{ttbox}
1.309 -type tactic = thm -> thm Seq.seq
1.310 -\end{ttbox}
1.311 -The following operations provide means for coding tactics in a clean style.
1.312 -\begin{ttbox}
1.313 -PRIMITIVE : (thm -> thm) -> tactic
1.314 -SUBGOAL : ((term*int) -> tactic) -> int -> tactic
1.315 -\end{ttbox}
1.316 -\begin{ttdescription}
1.317 -\item[\ttindexbold{PRIMITIVE} $f$] packages the meta-rule~$f$ as a tactic that
1.318 - applies $f$ to the proof state and returns the result as a one-element
1.319 - sequence. If $f$ raises an exception, then the tactic's result is the empty
1.320 - sequence.
1.321 -
1.322 -\item[\ttindexbold{SUBGOAL} $f$ $i$]
1.323 -extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
1.324 -tactic by calling~$f(t,i)$. It applies the resulting tactic to the same
1.325 -state. The tactic body is expressed using tactics and tacticals, but may
1.326 -peek at a particular subgoal:
1.327 -\begin{ttbox}
1.328 -SUBGOAL (fn (t,i) => {\it tactic-valued expression})
1.329 -\end{ttbox}
1.330 -\end{ttdescription}
1.331 -
1.332 -
1.333 -\subsection{Tracing}
1.334 -\index{tactics!tracing}
1.335 -\index{tracing!of tactics}
1.336 -\begin{ttbox}
1.337 -pause_tac: tactic
1.338 -print_tac: string -> tactic
1.339 -\end{ttbox}
1.340 -These tactics print tracing information when they are applied to a proof
1.341 -state. Their output may be difficult to interpret. Note that certain of
1.342 -the searching tacticals, such as {\tt REPEAT}, have built-in tracing
1.343 -options.
1.344 -\begin{ttdescription}
1.345 -\item[\ttindexbold{pause_tac}]
1.346 -prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line
1.347 -from the terminal. If this line is blank then it returns the proof state
1.348 -unchanged; otherwise it fails (which may terminate a repetition).
1.349 -
1.350 -\item[\ttindexbold{print_tac}~$msg$]
1.351 -returns the proof state unchanged, with the side effect of printing it at
1.352 -the terminal.
1.353 -\end{ttdescription}
1.354 -
1.355 -
1.356 -\section{*Sequences}
1.357 -\index{sequences (lazy lists)|bold}
1.358 -The module {\tt Seq} declares a type of lazy lists. It uses
1.359 -Isabelle's type \mltydx{option} to represent the possible presence
1.360 -(\ttindexbold{Some}) or absence (\ttindexbold{None}) of
1.361 -a value:
1.362 -\begin{ttbox}
1.363 -datatype 'a option = None | Some of 'a;
1.364 -\end{ttbox}
1.365 -The {\tt Seq} structure is supposed to be accessed via fully qualified
1.366 -names and should not be \texttt{open}.
1.367 -
1.368 -\subsection{Basic operations on sequences}
1.369 -\begin{ttbox}
1.370 -Seq.empty : 'a seq
1.371 -Seq.make : (unit -> ('a * 'a seq) option) -> 'a seq
1.372 -Seq.single : 'a -> 'a seq
1.373 -Seq.pull : 'a seq -> ('a * 'a seq) option
1.374 -\end{ttbox}
1.375 -\begin{ttdescription}
1.376 -\item[Seq.empty] is the empty sequence.
1.377 -
1.378 -\item[\tt Seq.make (fn () => Some ($x$, $xq$))] constructs the
1.379 - sequence with head~$x$ and tail~$xq$, neither of which is evaluated.
1.380 -
1.381 -\item[Seq.single $x$]
1.382 -constructs the sequence containing the single element~$x$.
1.383 -
1.384 -\item[Seq.pull $xq$] returns {\tt None} if the sequence is empty and
1.385 - {\tt Some ($x$, $xq'$)} if the sequence has head~$x$ and tail~$xq'$.
1.386 - Warning: calling \hbox{Seq.pull $xq$} again will {\it recompute\/}
1.387 - the value of~$x$; it is not stored!
1.388 -\end{ttdescription}
1.389 -
1.390 -
1.391 -\subsection{Converting between sequences and lists}
1.392 -\begin{ttbox}
1.393 -Seq.chop : int * 'a seq -> 'a list * 'a seq
1.394 -Seq.list_of : 'a seq -> 'a list
1.395 -Seq.of_list : 'a list -> 'a seq
1.396 -\end{ttbox}
1.397 -\begin{ttdescription}
1.398 -\item[Seq.chop ($n$, $xq$)] returns the first~$n$ elements of~$xq$ as a
1.399 - list, paired with the remaining elements of~$xq$. If $xq$ has fewer
1.400 - than~$n$ elements, then so will the list.
1.401 -
1.402 -\item[Seq.list_of $xq$] returns the elements of~$xq$, which must be
1.403 - finite, as a list.
1.404 -
1.405 -\item[Seq.of_list $xs$] creates a sequence containing the elements
1.406 - of~$xs$.
1.407 -\end{ttdescription}
1.408 -
1.409 -
1.410 -\subsection{Combining sequences}
1.411 -\begin{ttbox}
1.412 -Seq.append : 'a seq * 'a seq -> 'a seq
1.413 -Seq.interleave : 'a seq * 'a seq -> 'a seq
1.414 -Seq.flat : 'a seq seq -> 'a seq
1.415 -Seq.map : ('a -> 'b) -> 'a seq -> 'b seq
1.416 -Seq.filter : ('a -> bool) -> 'a seq -> 'a seq
1.417 -\end{ttbox}
1.418 -\begin{ttdescription}
1.419 -\item[Seq.append ($xq$, $yq$)] concatenates $xq$ to $yq$.
1.420 -
1.421 -\item[Seq.interleave ($xq$, $yq$)] joins $xq$ with $yq$ by
1.422 - interleaving their elements. The result contains all the elements
1.423 - of the sequences, even if both are infinite.
1.424 -
1.425 -\item[Seq.flat $xqq$] concatenates a sequence of sequences.
1.426 -
1.427 -\item[Seq.map $f$ $xq$] applies $f$ to every element
1.428 - of~$xq=x@1,x@2,\ldots$, yielding the sequence $f(x@1),f(x@2),\ldots$.
1.429 -
1.430 -\item[Seq.filter $p$ $xq$] returns the sequence consisting of all
1.431 - elements~$x$ of~$xq$ such that $p(x)$ is {\tt true}.
1.432 -\end{ttdescription}
1.433 -
1.434 \index{tactics|)}
1.435
1.436