--- a/doc-src/Ref/tactic.tex Sun Mar 01 12:37:59 2009 +0100
+++ b/doc-src/Ref/tactic.tex Sun Mar 01 13:48:17 2009 +0100
@@ -1,235 +1,8 @@
-%% $Id$
+
\chapter{Tactics} \label{tactics}
-\index{tactics|(} Tactics have type \mltydx{tactic}. This is just an
-abbreviation for functions from theorems to theorem sequences, where
-the theorems represent states of a backward proof. Tactics seldom
-need to be coded from scratch, as functions; instead they are
-expressed using basic tactics and tacticals.
-
-This chapter only presents the primitive tactics. Substantial proofs
-require the power of automatic tools like simplification
-(Chapter~\ref{chap:simplification}) and classical tableau reasoning
-(Chapter~\ref{chap:classical}).
-
-\section{Resolution and assumption tactics}
-{\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using
-a rule. {\bf Elim-resolution} is particularly suited for elimination
-rules, while {\bf destruct-resolution} is particularly suited for
-destruction rules. The {\tt r}, {\tt e}, {\tt d} naming convention is
-maintained for several different kinds of resolution tactics, as well as
-the shortcuts in the subgoal module.
-
-All the tactics in this section act on a subgoal designated by a positive
-integer~$i$. They fail (by returning the empty sequence) if~$i$ is out of
-range.
-
-\subsection{Resolution tactics}
-\index{resolution!tactics}
-\index{tactics!resolution|bold}
-\begin{ttbox}
-resolve_tac : thm list -> int -> tactic
-eresolve_tac : thm list -> int -> tactic
-dresolve_tac : thm list -> int -> tactic
-forward_tac : thm list -> int -> tactic
-\end{ttbox}
-These perform resolution on a list of theorems, $thms$, representing a list
-of object-rules. When generating next states, they take each of the rules
-in the order given. Each rule may yield several next states, or none:
-higher-order resolution may yield multiple resolvents.
-\begin{ttdescription}
-\item[\ttindexbold{resolve_tac} {\it thms} {\it i}]
- refines the proof state using the rules, which should normally be
- introduction rules. It resolves a rule's conclusion with
- subgoal~$i$ of the proof state.
-
-\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}]
- \index{elim-resolution}
- performs elim-resolution with the rules, which should normally be
- elimination rules. It resolves with a rule, proves its first premise by
- assumption, and finally \emph{deletes} that assumption from any new
- subgoals. (To rotate a rule's premises,
- see \texttt{rotate_prems} in~{\S}\ref{MiscellaneousForwardRules}.)
-
-\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}]
- \index{forward proof}\index{destruct-resolution}
- performs destruct-resolution with the rules, which normally should
- be destruction rules. This replaces an assumption by the result of
- applying one of the rules.
-
-\item[\ttindexbold{forward_tac}]\index{forward proof}
- is like {\tt dresolve_tac} except that the selected assumption is not
- deleted. It applies a rule to an assumption, adding the result as a new
- assumption.
-\end{ttdescription}
-
-\subsection{Assumption tactics}
-\index{tactics!assumption|bold}\index{assumptions!tactics for}
-\begin{ttbox}
-assume_tac : int -> tactic
-eq_assume_tac : int -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{assume_tac} {\it i}]
-attempts to solve subgoal~$i$ by assumption.
-
-\item[\ttindexbold{eq_assume_tac}]
-is like {\tt assume_tac} but does not use unification. It succeeds (with a
-\emph{unique} next state) if one of the assumptions is identical to the
-subgoal's conclusion. Since it does not instantiate variables, it cannot
-make other subgoals unprovable. It is intended to be called from proof
-strategies, not interactively.
-\end{ttdescription}
-
-\subsection{Matching tactics} \label{match_tac}
-\index{tactics!matching}
-\begin{ttbox}
-match_tac : thm list -> int -> tactic
-ematch_tac : thm list -> int -> tactic
-dmatch_tac : thm list -> int -> tactic
-\end{ttbox}
-These are just like the resolution tactics except that they never
-instantiate unknowns in the proof state. Flexible subgoals are not updated
-willy-nilly, but are left alone. Matching --- strictly speaking --- means
-treating the unknowns in the proof state as constants; these tactics merely
-discard unifiers that would update the proof state.
-\begin{ttdescription}
-\item[\ttindexbold{match_tac} {\it thms} {\it i}]
-refines the proof state using the rules, matching a rule's
-conclusion with subgoal~$i$ of the proof state.
-
-\item[\ttindexbold{ematch_tac}]
-is like {\tt match_tac}, but performs elim-resolution.
-
-\item[\ttindexbold{dmatch_tac}]
-is like {\tt match_tac}, but performs destruct-resolution.
-\end{ttdescription}
-
-
-\subsection{Explicit instantiation} \label{res_inst_tac}
-\index{tactics!instantiation}\index{instantiation}
-\begin{ttbox}
-res_inst_tac : (string*string)list -> thm -> int -> tactic
-eres_inst_tac : (string*string)list -> thm -> int -> tactic
-dres_inst_tac : (string*string)list -> thm -> int -> tactic
-forw_inst_tac : (string*string)list -> thm -> int -> tactic
-instantiate_tac : (string*string)list -> tactic
-\end{ttbox}
-The first four of these tactics are designed for applying rules by resolution
-such as substitution and induction, which cause difficulties for higher-order
-unification. The tactics accept explicit instantiations for unknowns
-in the rule ---typically, in the rule's conclusion. The last one,
-{\tt instantiate_tac}, may be used to instantiate unknowns in the proof state,
-independently of rule application.
-
-Each instantiation is a pair {\tt($v$,$e$)},
-where $v$ is an unknown \emph{without} its leading question mark!
-\begin{itemize}
-\item If $v$ is the type unknown {\tt'a}, then
-the rule must contain a type unknown \verb$?'a$ of some
-sort~$s$, and $e$ should be a type of sort $s$.
-
-\item If $v$ is the unknown {\tt P}, then
-the rule must contain an unknown \verb$?P$ of some type~$\tau$,
-and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
-$\sigma$ are unifiable. If the unification of $\tau$ and $\sigma$
-instantiates any type unknowns in $\tau$, these instantiations
-are recorded for application to the rule.
-\end{itemize}
-Types are instantiated before terms are. Because type instantiations are
-inferred from term instantiations, explicit type instantiations are seldom
-necessary --- if \verb$?t$ has type \verb$?'a$, then the instantiation list
-\texttt{[("'a","bool"), ("t","True")]} may be simplified to
-\texttt{[("t","True")]}. Type unknowns in the proof state may cause
-failure because the tactics cannot instantiate them.
-
-The first four instantiation tactics act on a given subgoal. Terms in the
-instantiations are type-checked in the context of that subgoal --- in
-particular, they may refer to that subgoal's parameters. Any unknowns in
-the terms receive subscripts and are lifted over the parameters; thus, you
-may not refer to unknowns in the subgoal.
-
-\begin{ttdescription}
-\item[\ttindexbold{res_inst_tac} {\it insts} {\it thm} {\it i}]
-instantiates the rule {\it thm} with the instantiations {\it insts}, as
-described above, and then performs resolution on subgoal~$i$. Resolution
-typically causes further instantiations; you need not give explicit
-instantiations for every unknown in the rule.
-
-\item[\ttindexbold{eres_inst_tac}]
-is like {\tt res_inst_tac}, but performs elim-resolution.
-
-\item[\ttindexbold{dres_inst_tac}]
-is like {\tt res_inst_tac}, but performs destruct-resolution.
-
-\item[\ttindexbold{forw_inst_tac}]
-is like {\tt dres_inst_tac} except that the selected assumption is not
-deleted. It applies the instantiated rule to an assumption, adding the
-result as a new assumption.
-
-\item[\ttindexbold{instantiate_tac} {\it insts}]
-instantiates unknowns in the proof state. This affects the main goal as
-well as all subgoals.
-\end{ttdescription}
-
+\index{tactics|(}
\section{Other basic tactics}
-\subsection{Tactic shortcuts}
-\index{shortcuts!for tactics}
-\index{tactics!resolution}\index{tactics!assumption}
-\index{tactics!meta-rewriting}
-\begin{ttbox}
-rtac : thm -> int -> tactic
-etac : thm -> int -> tactic
-dtac : thm -> int -> tactic
-ftac : thm -> int -> tactic
-atac : int -> tactic
-eatac : thm -> int -> int -> tactic
-datac : thm -> int -> int -> tactic
-fatac : thm -> int -> int -> tactic
-ares_tac : thm list -> int -> tactic
-rewtac : thm -> tactic
-\end{ttbox}
-These abbreviate common uses of tactics.
-\begin{ttdescription}
-\item[\ttindexbold{rtac} {\it thm} {\it i}]
-abbreviates \hbox{\tt resolve_tac [{\it thm}] {\it i}}, doing resolution.
-
-\item[\ttindexbold{etac} {\it thm} {\it i}]
-abbreviates \hbox{\tt eresolve_tac [{\it thm}] {\it i}}, doing elim-resolution.
-
-\item[\ttindexbold{dtac} {\it thm} {\it i}]
-abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
-destruct-resolution.
-
-\item[\ttindexbold{ftac} {\it thm} {\it i}]
-abbreviates \hbox{\tt forward_tac [{\it thm}] {\it i}}, doing
-destruct-resolution without deleting the assumption.
-
-\item[\ttindexbold{atac} {\it i}]
-abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
-
-\item[\ttindexbold{eatac} {\it thm} {\it j} {\it i}]
-performs \hbox{\tt etac {\it thm}} and then {\it j} times \texttt{atac},
-solving additionally {\it j}~premises of the rule {\it thm} by assumption.
-
-\item[\ttindexbold{datac} {\it thm} {\it j} {\it i}]
-performs \hbox{\tt dtac {\it thm}} and then {\it j} times \texttt{atac},
-solving additionally {\it j}~premises of the rule {\it thm} by assumption.
-
-\item[\ttindexbold{fatac} {\it thm} {\it j} {\it i}]
-performs \hbox{\tt ftac {\it thm}} and then {\it j} times \texttt{atac},
-solving additionally {\it j}~premises of the rule {\it thm} by assumption.
-
-\item[\ttindexbold{ares_tac} {\it thms} {\it i}]
-tries proof by assumption and resolution; it abbreviates
-\begin{ttbox}
-assume_tac {\it i} ORELSE resolve_tac {\it thms} {\it i}
-\end{ttbox}
-
-\item[\ttindexbold{rewtac} {\it def}]
-abbreviates \hbox{\tt rewrite_goals_tac [{\it def}]}, unfolding a definition.
-\end{ttdescription}
-
\subsection{Inserting premises and facts}\label{cut_facts_tac}
\index{tactics!for inserting facts}\index{assumptions!inserting}
@@ -351,52 +124,6 @@
\section{Obscure tactics}
-\subsection{Renaming parameters in a goal} \index{parameters!renaming}
-\begin{ttbox}
-rename_tac : string -> int -> tactic
-rename_last_tac : string -> string list -> int -> tactic
-Logic.set_rename_prefix : string -> unit
-Logic.auto_rename : bool ref \hfill{\bf initially false}
-\end{ttbox}
-When creating a parameter, Isabelle chooses its name by matching variable
-names via the object-rule. Given the rule $(\forall I)$ formalized as
-$\left(\Forall x. P(x)\right) \Imp \forall x.P(x)$, Isabelle will note that
-the $\Forall$-bound variable in the premise has the same name as the
-$\forall$-bound variable in the conclusion.
-
-Sometimes there is insufficient information and Isabelle chooses an
-arbitrary name. The renaming tactics let you override Isabelle's choice.
-Because renaming parameters has no logical effect on the proof state, the
-{\tt by} command prints the message {\tt Warning:\ same as previous
-level}.
-
-Alternatively, you can suppress the naming mechanism described above and
-have Isabelle generate uniform names for parameters. These names have the
-form $p${\tt a}, $p${\tt b}, $p${\tt c},~\ldots, where $p$ is any desired
-prefix. They are ugly but predictable.
-
-\begin{ttdescription}
-\item[\ttindexbold{rename_tac} {\it str} {\it i}]
-interprets the string {\it str} as a series of blank-separated variable
-names, and uses them to rename the parameters of subgoal~$i$. The names
-must be distinct. If there are fewer names than parameters, then the
-tactic renames the innermost parameters and may modify the remaining ones
-to ensure that all the parameters are distinct.
-
-\item[\ttindexbold{rename_last_tac} {\it prefix} {\it suffixes} {\it i}]
-generates a list of names by attaching each of the {\it suffixes\/} to the
-{\it prefix}. It is intended for coding structural induction tactics,
-where several of the new parameters should have related names.
-
-\item[\ttindexbold{Logic.set_rename_prefix} {\it prefix};]
-sets the prefix for uniform renaming to~{\it prefix}. The default prefix
-is {\tt"k"}.
-
-\item[set \ttindexbold{Logic.auto_rename};]
-makes Isabelle generate uniform names for parameters.
-\end{ttdescription}
-
-
\subsection{Manipulating assumptions}
\index{assumptions!rotating}
\begin{ttbox}
@@ -594,142 +321,6 @@
is no longer than {\it limit}.
\end{ttdescription}
-
-\section{Programming tools for proof strategies}
-Do not consider using the primitives discussed in this section unless you
-really need to code tactics from scratch.
-
-\subsection{Operations on tactics}
-\index{tactics!primitives for coding} A tactic maps theorems to sequences of
-theorems. The type constructor for sequences (lazy lists) is called
-\mltydx{Seq.seq}. To simplify the types of tactics and tacticals,
-Isabelle defines a type abbreviation:
-\begin{ttbox}
-type tactic = thm -> thm Seq.seq
-\end{ttbox}
-The following operations provide means for coding tactics in a clean style.
-\begin{ttbox}
-PRIMITIVE : (thm -> thm) -> tactic
-SUBGOAL : ((term*int) -> tactic) -> int -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{PRIMITIVE} $f$] packages the meta-rule~$f$ as a tactic that
- applies $f$ to the proof state and returns the result as a one-element
- sequence. If $f$ raises an exception, then the tactic's result is the empty
- sequence.
-
-\item[\ttindexbold{SUBGOAL} $f$ $i$]
-extracts subgoal~$i$ from the proof state as a term~$t$, and computes a
-tactic by calling~$f(t,i)$. It applies the resulting tactic to the same
-state. The tactic body is expressed using tactics and tacticals, but may
-peek at a particular subgoal:
-\begin{ttbox}
-SUBGOAL (fn (t,i) => {\it tactic-valued expression})
-\end{ttbox}
-\end{ttdescription}
-
-
-\subsection{Tracing}
-\index{tactics!tracing}
-\index{tracing!of tactics}
-\begin{ttbox}
-pause_tac: tactic
-print_tac: string -> tactic
-\end{ttbox}
-These tactics print tracing information when they are applied to a proof
-state. Their output may be difficult to interpret. Note that certain of
-the searching tacticals, such as {\tt REPEAT}, have built-in tracing
-options.
-\begin{ttdescription}
-\item[\ttindexbold{pause_tac}]
-prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line
-from the terminal. If this line is blank then it returns the proof state
-unchanged; otherwise it fails (which may terminate a repetition).
-
-\item[\ttindexbold{print_tac}~$msg$]
-returns the proof state unchanged, with the side effect of printing it at
-the terminal.
-\end{ttdescription}
-
-
-\section{*Sequences}
-\index{sequences (lazy lists)|bold}
-The module {\tt Seq} declares a type of lazy lists. It uses
-Isabelle's type \mltydx{option} to represent the possible presence
-(\ttindexbold{Some}) or absence (\ttindexbold{None}) of
-a value:
-\begin{ttbox}
-datatype 'a option = None | Some of 'a;
-\end{ttbox}
-The {\tt Seq} structure is supposed to be accessed via fully qualified
-names and should not be \texttt{open}.
-
-\subsection{Basic operations on sequences}
-\begin{ttbox}
-Seq.empty : 'a seq
-Seq.make : (unit -> ('a * 'a seq) option) -> 'a seq
-Seq.single : 'a -> 'a seq
-Seq.pull : 'a seq -> ('a * 'a seq) option
-\end{ttbox}
-\begin{ttdescription}
-\item[Seq.empty] is the empty sequence.
-
-\item[\tt Seq.make (fn () => Some ($x$, $xq$))] constructs the
- sequence with head~$x$ and tail~$xq$, neither of which is evaluated.
-
-\item[Seq.single $x$]
-constructs the sequence containing the single element~$x$.
-
-\item[Seq.pull $xq$] returns {\tt None} if the sequence is empty and
- {\tt Some ($x$, $xq'$)} if the sequence has head~$x$ and tail~$xq'$.
- Warning: calling \hbox{Seq.pull $xq$} again will {\it recompute\/}
- the value of~$x$; it is not stored!
-\end{ttdescription}
-
-
-\subsection{Converting between sequences and lists}
-\begin{ttbox}
-Seq.chop : int * 'a seq -> 'a list * 'a seq
-Seq.list_of : 'a seq -> 'a list
-Seq.of_list : 'a list -> 'a seq
-\end{ttbox}
-\begin{ttdescription}
-\item[Seq.chop ($n$, $xq$)] returns the first~$n$ elements of~$xq$ as a
- list, paired with the remaining elements of~$xq$. If $xq$ has fewer
- than~$n$ elements, then so will the list.
-
-\item[Seq.list_of $xq$] returns the elements of~$xq$, which must be
- finite, as a list.
-
-\item[Seq.of_list $xs$] creates a sequence containing the elements
- of~$xs$.
-\end{ttdescription}
-
-
-\subsection{Combining sequences}
-\begin{ttbox}
-Seq.append : 'a seq * 'a seq -> 'a seq
-Seq.interleave : 'a seq * 'a seq -> 'a seq
-Seq.flat : 'a seq seq -> 'a seq
-Seq.map : ('a -> 'b) -> 'a seq -> 'b seq
-Seq.filter : ('a -> bool) -> 'a seq -> 'a seq
-\end{ttbox}
-\begin{ttdescription}
-\item[Seq.append ($xq$, $yq$)] concatenates $xq$ to $yq$.
-
-\item[Seq.interleave ($xq$, $yq$)] joins $xq$ with $yq$ by
- interleaving their elements. The result contains all the elements
- of the sequences, even if both are infinite.
-
-\item[Seq.flat $xqq$] concatenates a sequence of sequences.
-
-\item[Seq.map $f$ $xq$] applies $f$ to every element
- of~$xq=x@1,x@2,\ldots$, yielding the sequence $f(x@1),f(x@2),\ldots$.
-
-\item[Seq.filter $p$ $xq$] returns the sequence consisting of all
- elements~$x$ of~$xq$ such that $p(x)$ is {\tt true}.
-\end{ttdescription}
-
\index{tactics|)}