# HG changeset patch
# User paulson
# Date 875186750 -7200
# Node ID 2885b760a4b41c3542a31da9e6e7452d138b468a
# Parent  6e074b41c73536b56e2b14eb6badbe17d0a99181
Clarify_tac and some textual improvements

diff -r 6e074b41c735 -r 2885b760a4b4 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Thu Sep 25 13:23:41 1997 +0200
+++ b/doc-src/Ref/classical.tex	Thu Sep 25 13:25:50 1997 +0200
@@ -29,20 +29,24 @@
 be traced, and their components can be called directly; in this manner,
 any proof can be viewed interactively.
 
-The simplest way to apply the classical reasoner (to subgoal~$i$) is as
-follows:
+The simplest way to apply the classical reasoner (to subgoal~$i$) is to type
 \begin{ttbox}
 by (Blast_tac \(i\));
 \end{ttbox}
-If the subgoal is a simple formula of the predicate calculus or set theory,
-then it should be proved quickly.  To attempt to prove \emph{all} subgoals
-using a combination of rewriting and classical reasoning, try
+This command quickly proves most simple formulas of the predicate calculus or
+set theory.  To attempt to prove \emph{all} subgoals using a combination of
+rewriting and classical reasoning, try
 \begin{ttbox}
 by (Auto_tac());
 \end{ttbox}
-To use the classical reasoner effectively, you need to know how it works.  It
-provides many tactics to choose from, including {\tt Fast_tac} and {\tt
-  Best_tac}.
+To do all obvious logical steps, even if they do not prove the
+subgoal, type
+\begin{ttbox}
+by (Clarify_tac \(i\));
+\end{ttbox}
+You need to know how the classical reasoner works in order to use it
+effectively.  There are many tactics to choose from, including {\tt
+  Fast_tac} and {\tt Best_tac}.
 
 We shall first discuss the underlying principles, then present the
 classical reasoner.  Finally, we shall see how to instantiate it for
@@ -297,12 +301,13 @@
 
 
 \subsection{Modifying the search step}
-For a given classical set, the proof strategy is simple.  Perform as many
-safe inferences as possible; or else, apply certain safe rules, allowing
-instantiation of unknowns; or else, apply an unsafe rule.  The tactics may
-also apply {\tt hyp_subst_tac}, if they have been set up to do so (see
-below).  They may perform a form of Modus Ponens: if there are assumptions
-$P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$.
+For a given classical set, the proof strategy is simple.  Perform as many safe
+inferences as possible; or else, apply certain safe rules, allowing
+instantiation of unknowns; or else, apply an unsafe rule.  The tactics also
+eliminate assumptions of the form $x=t$ by substitution if they have been set
+up to do so (see {\tt hyp_subst_tacs} in~\S\ref{sec:classical-setup} below).
+They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$
+and~$P$, then replace $P\imp Q$ by~$Q$.
 
 The classical reasoning tactics --- except {\tt blast_tac}! --- allow
 you to modify this basic proof strategy by applying two arbitrary {\bf
@@ -375,9 +380,31 @@
 
 
 \section{The classical tactics}
-\index{classical reasoner!tactics}
-If installed, the classical module provides several tactics (and other
-operations) for simulating the classical sequent calculus.
+\index{classical reasoner!tactics} If installed, the classical module provides
+powerful theorem-proving tactics.  Most of them have capitalized analogues
+that use the default claset; see \S\ref{sec:current-claset}.
+
+\subsection{Semi-automatic tactics}
+\begin{ttbox} 
+clarify_tac      : claset -> int -> tactic
+clarify_step_tac : claset -> int -> tactic
+\end{ttbox}
+Use these when the automatic tactics fail.  They perform all the obvious
+logical inferences that do not split the subgoal.  The result is a
+simpler subgoal that can be tackled by other means, such as by
+instantiating quantifiers yourself.
+\begin{ttdescription}
+\item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on
+subgoal~$i$, using \texttt{clarify_step_tac}.
+
+\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
+  subgoal~$i$.  No splitting step is applied; for example, the subgoal $A\conj
+  B$ is left as a conjunction.  Proof by assumption, Modus Ponens, etc., may be
+  performed provided they do not instantiate unknowns.  Assumptions of the
+  form $x=t$ may be eliminated.  The user-supplied safe wrapper tactical is
+  applied.
+\end{ttdescription}
+
 
 \subsection{The tableau prover}
 The tactic {\tt blast_tac} searches for a proof using a fast tableau prover,
@@ -475,7 +502,7 @@
 \end{ttdescription}
 
 
-\subsection{Depth-limited tactics}
+\subsection{Depth-limited automatic tactics}
 \begin{ttbox} 
 depth_tac  : claset -> int -> int -> tactic
 deepen_tac : claset -> int -> int -> tactic
@@ -509,14 +536,12 @@
 yourself, you can execute these procedures one step at a time.
 \begin{ttdescription}
 \item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
-subgoal~$i$.  The safe wrapper tactical is applied to a tactic that may include 
-proof by assumption or Modus Ponens (taking care not to instantiate unknowns), 
-or {\tt hyp_subst_tac}.
+  subgoal~$i$.  The safe wrapper tactical is applied to a tactic that may
+  include proof by assumption or Modus Ponens (taking care not to instantiate
+  unknowns), or substitution.
 
 \item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all 
-subgoals.  It is deterministic, with at most one outcome.  If the automatic
-tactics fail, try using {\tt safe_tac} to open up your formula; then you
-can replicate certain quantifiers explicitly by applying appropriate rules.
+subgoals.  It is deterministic, with at most one outcome.  
 
 \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like {\tt safe_step_tac},
 but allows unknowns to be instantiated.
@@ -539,16 +564,19 @@
 warnings.  Just like simpsets, clasets can be associated with theories.  The
 tactics
 \begin{ttbox}
-Blast_tac    : int -> tactic
-Auto_tac     : unit -> tactic
-Fast_tac     : int -> tactic
-Best_tac     : int -> tactic
-Deepen_tac   : int -> int -> tactic
-Step_tac     : int -> tactic
+Blast_tac        : int -> tactic
+Auto_tac         : unit -> tactic
+Fast_tac         : int -> tactic
+Best_tac         : int -> tactic
+Deepen_tac       : int -> int -> tactic
+Clarify_tac      : int -> tactic
+Clarify_step_tac : int -> tactic
+Step_tac         : int -> tactic
 \end{ttbox}
 \indexbold{*Blast_tac}\indexbold{*Auto_tac}
 \indexbold{*Best_tac}\indexbold{*Fast_tac}%
-\indexbold{*Deepen_tac}\indexbold{*Step_tac}
+\indexbold{*Deepen_tac}\indexbold{*Clarify_tac}
+\indexbold{*Clarify_step_tac}\indexbold{*Step_tac}
 make use of the current claset.  E.g. {\tt Blast_tac} is defined as follows:
 \begin{ttbox}
 fun Blast_tac i = fast_tac (!claset) i;
@@ -618,7 +646,7 @@
 \end{ttdescription}
 
 
-\section{Setting up the classical reasoner}
+\section{Setting up the classical reasoner}\label{sec:classical-setup}
 \index{classical reasoner!setting up}
 Isabelle's classical object-logics, including {\tt FOL} and {\tt HOL}, have
 the classical reasoner already set up.  When defining a new classical logic,