src/Doc/Ref/document/tactic.tex

 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{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: