--- a/doc-src/Ref/document/tactic.tex Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,173 +0,0 @@
-
-\chapter{Tactics} \label{tactics}
-\index{tactics|(}
-
-\section{Other basic tactics}
-
-\subsection{Inserting premises and facts}\label{cut_facts_tac}
-\index{tactics!for inserting facts}\index{assumptions!inserting}
-\begin{ttbox}
-cut_facts_tac : thm list -> int -> tactic
-\end{ttbox}
-These tactics add assumptions to a subgoal.
-\begin{ttdescription}
-\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}]
- adds the {\it thms} as new assumptions to subgoal~$i$. Once they have
- been inserted as assumptions, they become subject to tactics such as {\tt
- eresolve_tac} and {\tt rewrite_goals_tac}. Only rules with no premises
- are inserted: Isabelle cannot use assumptions that contain $\Imp$
- or~$\Forall$. Sometimes the theorems are premises of a rule being
- derived, returned by~{\tt goal}; instead of calling this tactic, you
- could state the goal with an outermost meta-quantifier.
-
-\end{ttdescription}
-
-
-\subsection{Composition: resolution without lifting}
-\index{tactics!for composition}
-\begin{ttbox}
-compose_tac: (bool * thm * int) -> int -> tactic
-\end{ttbox}
-{\bf Composing} two rules means resolving them without prior lifting or
-renaming of unknowns. This low-level operation, which underlies the
-resolution tactics, may occasionally be useful for special effects.
-A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
-rule, then passes the result to {\tt compose_tac}.
-\begin{ttdescription}
-\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$]
-refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to
-have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
-not be atomic; thus $m$ determines the number of new subgoals. If
-$flag$ is {\tt true} then it performs elim-resolution --- it solves the
-first premise of~$rule$ by assumption and deletes that assumption.
-\end{ttdescription}
-
-
-\section{*Managing lots of rules}
-These operations are not intended for interactive use. They are concerned
-with the processing of large numbers of rules in automatic proof
-strategies. Higher-order resolution involving a long list of rules is
-slow. Filtering techniques can shorten the list of rules given to
-resolution, and can also detect whether a subgoal is too flexible,
-with too many rules applicable.
-
-\subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
-\index{tactics!resolution}
-\begin{ttbox}
-biresolve_tac : (bool*thm)list -> int -> tactic
-bimatch_tac : (bool*thm)list -> int -> tactic
-subgoals_of_brl : bool*thm -> int
-lessb : (bool*thm) * (bool*thm) -> bool
-\end{ttbox}
-{\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs. For each
-pair, it applies resolution if the flag is~{\tt false} and
-elim-resolution if the flag is~{\tt true}. A single tactic call handles a
-mixture of introduction and elimination rules.
-
-\begin{ttdescription}
-\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}]
-refines the proof state by resolution or elim-resolution on each rule, as
-indicated by its flag. It affects subgoal~$i$ of the proof state.
-
-\item[\ttindexbold{bimatch_tac}]
-is like {\tt biresolve_tac}, but performs matching: unknowns in the
-proof state are never updated (see~{\S}\ref{match_tac}).
-
-\item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})]
-returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the
-pair (if applied to a suitable subgoal). This is $n$ if the flag is
-{\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
-of premises of the rule. Elim-resolution yields one fewer subgoal than
-ordinary resolution because it solves the major premise by assumption.
-
-\item[\ttindexbold{lessb} ({\it brl1},{\it brl2})]
-returns the result of
-\begin{ttbox}
-subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
-\end{ttbox}
-\end{ttdescription}
-Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
-(flag,rule)$ pairs by the number of new subgoals they will yield. Thus,
-those that yield the fewest subgoals should be tried first.
-
-
-\subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}
-\index{discrimination nets|bold}
-\index{tactics!resolution}
-\begin{ttbox}
-net_resolve_tac : thm list -> int -> tactic
-net_match_tac : thm list -> int -> tactic
-net_biresolve_tac: (bool*thm) list -> int -> tactic
-net_bimatch_tac : (bool*thm) list -> int -> tactic
-filt_resolve_tac : thm list -> int -> int -> tactic
-could_unify : term*term->bool
-filter_thms : (term*term->bool) -> int*term*thm list -> thm{\ts}list
-\end{ttbox}
-The module {\tt Net} implements a discrimination net data structure for
-fast selection of rules \cite[Chapter 14]{charniak80}. A term is
-classified by the symbol list obtained by flattening it in preorder.
-The flattening takes account of function applications, constants, and free
-and bound variables; it identifies all unknowns and also regards
-\index{lambda abs@$\lambda$-abstractions}
-$\lambda$-abstractions as unknowns, since they could $\eta$-contract to
-anything.
-
-A discrimination net serves as a polymorphic dictionary indexed by terms.
-The module provides various functions for inserting and removing items from
-nets. It provides functions for returning all items whose term could match
-or unify with a target term. The matching and unification tests are
-overly lax (due to the identifications mentioned above) but they serve as
-useful filters.
-
-A net can store introduction rules indexed by their conclusion, and
-elimination rules indexed by their major premise. Isabelle provides
-several functions for `compiling' long lists of rules into fast
-resolution tactics. When supplied with a list of theorems, these functions
-build a discrimination net; the net is used when the tactic is applied to a
-goal. To avoid repeatedly constructing the nets, use currying: bind the
-resulting tactics to \ML{} identifiers.
-
-\begin{ttdescription}
-\item[\ttindexbold{net_resolve_tac} {\it thms}]
-builds a discrimination net to obtain the effect of a similar call to {\tt
-resolve_tac}.
-
-\item[\ttindexbold{net_match_tac} {\it thms}]
-builds a discrimination net to obtain the effect of a similar call to {\tt
-match_tac}.
-
-\item[\ttindexbold{net_biresolve_tac} {\it brls}]
-builds a discrimination net to obtain the effect of a similar call to {\tt
-biresolve_tac}.
-
-\item[\ttindexbold{net_bimatch_tac} {\it brls}]
-builds a discrimination net to obtain the effect of a similar call to {\tt
-bimatch_tac}.
-
-\item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}]
-uses discrimination nets to extract the {\it thms} that are applicable to
-subgoal~$i$. If more than {\it maxr\/} theorems are applicable then the
-tactic fails. Otherwise it calls {\tt resolve_tac}.
-
-This tactic helps avoid runaway instantiation of unknowns, for example in
-type inference.
-
-\item[\ttindexbold{could_unify} ({\it t},{\it u})]
-returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and
-otherwise returns~{\tt true}. It assumes all variables are distinct,
-reporting that {\tt ?a=?a} may unify with {\tt 0=1}.
-
-\item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$]
-returns the list of potentially resolvable rules (in {\it thms\/}) for the
-subgoal {\it prem}, using the predicate {\it could\/} to compare the
-conclusion of the subgoal with the conclusion of each rule. The resulting list
-is no longer than {\it limit}.
-\end{ttdescription}
-
-\index{tactics|)}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "ref"
-%%% End: