doc-src/Ref/classical.tex

 \index{classical reasoner|(}
 \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
 
 \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
 can be unified with an assumption of the current proof state:
 \indexbold{*addSE2}\indexbold{*addSD2}\indexbold{*addE2}\indexbold{*addD2}