# 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,