--- a/doc-src/Ref/classical.tex Sat Jun 04 22:09:42 2011 +0200
+++ b/doc-src/Ref/classical.tex Sun Jun 05 20:15:47 2011 +0200
@@ -5,110 +5,6 @@
\section{Classical rule sets}
\index{classical sets}
-Each automatic tactic takes a {\bf classical set} --- a collection of
-rules, classified as introduction or elimination and as {\bf safe} or {\bf
-unsafe}. In general, safe rules can be attempted blindly, while unsafe
-rules must be used with care. A safe rule must never reduce a provable
-goal to an unprovable set of subgoals.
-
-The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$. Any
-rule is unsafe whose premises contain new unknowns. The elimination
-rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,
-which discards the assumption $\forall x{.}P(x)$ and replaces it by the
-weaker assumption~$P(\Var{t})$. The rule $({\exists}I)$ is unsafe for
-similar reasons. The rule~$(\forall E@3)$ is unsafe in a different sense:
-since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.
-In classical first-order logic, all rules are safe except those mentioned
-above.
-
-The safe/unsafe distinction is vague, and may be regarded merely as a way
-of giving some rules priority over others. One could argue that
-$({\disj}E)$ is unsafe, because repeated application of it could generate
-exponentially many subgoals. Induction rules are unsafe because inductive
-proofs are difficult to set up automatically. Any inference is unsafe that
-instantiates an unknown in the proof state --- thus \ttindex{match_tac}
-must be used, rather than \ttindex{resolve_tac}. Even proof by assumption
-is unsafe if it instantiates unknowns shared with other subgoals --- thus
-\ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.
-
-\subsection{Adding rules to classical sets}
-Classical rule sets belong to the abstract type \mltydx{claset}, which
-supports the following operations (provided the classical reasoner is
-installed!):
-\begin{ttbox}
-empty_cs : claset
-print_cs : claset -> unit
-rep_cs : claset -> \{safeEs: thm list, safeIs: thm list,
- hazEs: thm list, hazIs: thm list,
- swrappers: (string * wrapper) list,
- uwrappers: (string * wrapper) list,
- safe0_netpair: netpair, safep_netpair: netpair,
- haz_netpair: netpair, dup_netpair: netpair\}
-addSIs : claset * thm list -> claset \hfill{\bf infix 4}
-addSEs : claset * thm list -> claset \hfill{\bf infix 4}
-addSDs : claset * thm list -> claset \hfill{\bf infix 4}
-addIs : claset * thm list -> claset \hfill{\bf infix 4}
-addEs : claset * thm list -> claset \hfill{\bf infix 4}
-addDs : claset * thm list -> claset \hfill{\bf infix 4}
-delrules : claset * thm list -> claset \hfill{\bf infix 4}
-\end{ttbox}
-The add operations ignore any rule already present in the claset with the same
-classification (such as safe introduction). They print a warning if the rule
-has already been added with some other classification, but add the rule
-anyway. Calling \texttt{delrules} deletes all occurrences of a rule from the
-claset, but see the warning below concerning destruction rules.
-\begin{ttdescription}
-\item[\ttindexbold{empty_cs}] is the empty classical set.
-
-\item[\ttindexbold{print_cs} $cs$] displays the printable contents of~$cs$,
- which is the rules. All other parts are non-printable.
-
-\item[\ttindexbold{rep_cs} $cs$] decomposes $cs$ as a record of its internal
- components, namely the safe introduction and elimination rules, the unsafe
- introduction and elimination rules, the lists of safe and unsafe wrappers
- (see \ref{sec:modifying-search}), and the internalized forms of the rules.
-
-\item[$cs$ addSIs $rules$] \indexbold{*addSIs}
-adds safe introduction~$rules$ to~$cs$.
-
-\item[$cs$ addSEs $rules$] \indexbold{*addSEs}
-adds safe elimination~$rules$ to~$cs$.
-
-\item[$cs$ addSDs $rules$] \indexbold{*addSDs}
-adds safe destruction~$rules$ to~$cs$.
-
-\item[$cs$ addIs $rules$] \indexbold{*addIs}
-adds unsafe introduction~$rules$ to~$cs$.
-
-\item[$cs$ addEs $rules$] \indexbold{*addEs}
-adds unsafe elimination~$rules$ to~$cs$.
-
-\item[$cs$ addDs $rules$] \indexbold{*addDs}
-adds unsafe destruction~$rules$ to~$cs$.
-
-\item[$cs$ delrules $rules$] \indexbold{*delrules}
-deletes~$rules$ from~$cs$. It prints a warning for those rules that are not
-in~$cs$.
-\end{ttdescription}
-
-\begin{warn}
- If you added $rule$ using \texttt{addSDs} or \texttt{addDs}, then you must delete
- it as follows:
-\begin{ttbox}
-\(cs\) delrules [make_elim \(rule\)]
-\end{ttbox}
-\par\noindent
-This is necessary because the operators \texttt{addSDs} and \texttt{addDs} convert
-the destruction rules to elimination rules by applying \ttindex{make_elim},
-and then insert them using \texttt{addSEs} and \texttt{addEs}, respectively.
-\end{warn}
-
-Introduction rules are those that can be applied using ordinary resolution.
-The classical set automatically generates their swapped forms, which will
-be applied using elim-resolution. Elimination rules are applied using
-elim-resolution. In a classical set, rules are sorted by the number of new
-subgoals they will yield; rules that generate the fewest subgoals will be
-tried first (see {\S}\ref{biresolve_tac}).
For elimination and destruction rules there are variants of the add operations
adding a rule in a way such that it is applied only if also its second premise