--- a/src/Doc/IsarImplementation/Tactic.thy Wed Nov 07 12:14:38 2012 +0100
+++ b/src/Doc/IsarImplementation/Tactic.thy Wed Nov 07 16:02:43 2012 +0100
@@ -265,12 +265,14 @@
@{index_ML resolve_tac: "thm list -> int -> tactic"} \\
@{index_ML eresolve_tac: "thm list -> int -> tactic"} \\
@{index_ML dresolve_tac: "thm list -> int -> tactic"} \\
- @{index_ML forward_tac: "thm list -> int -> tactic"} \\[1ex]
+ @{index_ML forward_tac: "thm list -> int -> tactic"} \\
+ @{index_ML biresolve_tac: "(bool * thm) list -> int -> tactic"} \\[1ex]
@{index_ML assume_tac: "int -> tactic"} \\
@{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
@{index_ML match_tac: "thm list -> int -> tactic"} \\
@{index_ML ematch_tac: "thm list -> int -> tactic"} \\
@{index_ML dmatch_tac: "thm list -> int -> tactic"} \\
+ @{index_ML bimatch_tac: "(bool * thm) list -> int -> tactic"} \\
\end{mldecls}
\begin{description}
@@ -297,6 +299,16 @@
selected assumption is not deleted. It applies a rule to an
assumption, adding the result as a new assumption.
+ \item @{ML biresolve_tac}~@{text "brls i"} refines the proof state
+ by resolution or elim-resolution on each rule, as indicated by its
+ flag. It affects subgoal @{text "i"} of the proof state.
+
+ For each pair @{text "(flag, rule)"}, it applies resolution if the
+ flag is @{text "false"} and elim-resolution if the flag is @{text
+ "true"}. A single tactic call handles a mixture of introduction and
+ elimination rules, which is useful to organize the search process
+ systematically in proof tools.
+
\item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i}
by assumption (modulo higher-order unification).
@@ -306,10 +318,10 @@
assumptions is equal to the subgoal's conclusion. Since it does not
instantiate variables, it cannot make other subgoals unprovable.
- \item @{ML match_tac}, @{ML ematch_tac}, and @{ML dmatch_tac} are
- similar to @{ML resolve_tac}, @{ML eresolve_tac}, and @{ML
- dresolve_tac}, respectively, but do not instantiate schematic
- variables in the goal state.
+ \item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML
+ bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac},
+ @{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do
+ not instantiate schematic variables in the goal state.
Flexible subgoals are not updated at will, but are left alone.
Strictly speaking, matching means to treat the unknowns in the goal
--- a/src/Doc/Ref/document/tactic.tex Wed Nov 07 12:14:38 2012 +0100
+++ b/src/Doc/Ref/document/tactic.tex Wed Nov 07 16:02:43 2012 +0100
@@ -4,25 +4,6 @@
\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}
@@ -51,45 +32,6 @@
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}