author lcp Fri, 15 Apr 1994 16:29:48 +0200 changeset 319 f143f7686cd6 parent 318 a0e27395abe3 child 320 76ae17549558
penultimate Springer draft
 doc-src/Ref/classical.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/classical.tex	Fri Apr 15 16:08:31 1994 +0200
+++ b/doc-src/Ref/classical.tex	Fri Apr 15 16:29:48 1994 +0200
@@ -1,5 +1,5 @@
%% $Id$
-\chapter{The Classical Reasoner}
+\chapter{The Classical Reasoner}\label{chap:classical}
\index{classical reasoner|(}
\newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}

@@ -109,8 +109,9 @@
\eqno({\neg}L) $$What about reasoning on the right? Introduction rules can only affect the formula in the conclusion, namely~Q@1. The other right-side formulae are -represented as negated assumptions, \neg Q@2, \ldots,~\neg Q@n. In -order to operate on one of these, it must first be exchanged with~Q@1. +represented as negated assumptions, \neg Q@2, \ldots,~\neg Q@n. +\index{assumptions!negated} +In order to operate on one of these, it must first be exchanged with~Q@1. Elim-resolution with the {\bf swap} rule has this effect:$$ \List{\neg P; \; \neg R\Imp P} \Imp R   \eqno(swap)
To ensure that swaps occur only when necessary, each introduction rule is
@@ -176,8 +177,8 @@

\section{Classical rule sets}
-\index{classical sets|bold}
-Each automatic tactic takes a {\bf classical rule set} --- a collection of
+\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
@@ -203,7 +204,7 @@
is unsafe if it instantiates unknowns shared with other subgoals --- thus
\ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.

-Classical rule sets belong to the abstract type \ttindexbold{claset}, which
+Classical rule sets belong to the abstract type \mltydx{claset}, which
supports the following operations (provided the classical reasoner is
installed!):
\begin{ttbox}
@@ -252,14 +253,13 @@
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 \ttindex{hyp_subst_tac}, if they have been set up to do so (see
+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$.

\section{The classical tactics}
-\index{classical prover!tactics|bold}
-\index{tactics!for classical proof|bold}
+\index{classical reasoner!tactics}
If installed, the classical module provides several tactics (and other
operations) for simulating the classical sequent calculus.

@@ -275,8 +275,8 @@
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$.  This may include proof by assumption or Modus Ponens, taking
-care not to instantiate unknowns, or \ttindex{hyp_subst_tac}.
+subgoal~$i$.  This may include proof by assumption or Modus Ponens (taking
+care not to instantiate unknowns), or {\tt hyp_subst_tac}.

\item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all
subgoals.  It is deterministic, with at most one outcome.  If the automatic
@@ -319,8 +319,8 @@

\subsection{Other useful tactics}
-\index{tactics!for Modus Ponens|bold}
+\index{tactics!for Modus Ponens}
\begin{ttbox}
contr_tac    :             int -> tactic
mp_tac       :             int -> tactic
@@ -329,10 +329,11 @@
\end{ttbox}
These can be used in the body of a specialized search.
\begin{ttdescription}
-\item[\ttindexbold{contr_tac} {\it i}] solves subgoal~$i$ by detecting a
-contradiction among two assumptions of the form $P$ and~$\neg P$, or fail.
-It may instantiate unknowns.  The tactic can produce multiple outcomes,
+  solves subgoal~$i$ by detecting a contradiction among two assumptions of
+  the form $P$ and~$\neg P$, or fail.  It may instantiate unknowns.  The
+  tactic can produce multiple outcomes, enumerating all possible

\item[\ttindexbold{mp_tac} {\it i}]
is like {\tt contr_tac}, but also attempts to perform Modus Ponens in
@@ -346,7 +347,7 @@

\item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
the proof state using {\it thms}, which should be a list of introduction
-rules.  First, it attempts to solve the goal using \ttindex{assume_tac} or
+rules.  First, it attempts to solve the goal using {\tt assume_tac} or
{\tt contr_tac}.  It then attempts to apply each rule in turn, attempting
resolution and also elim-resolution with the swapped form.
\end{ttdescription}
@@ -369,12 +370,12 @@

\section{Setting up the classical reasoner}
-\index{classical reasoner!setting up|bold}
+\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,
you should set up the reasoner yourself.  It consists of the \ML{} functor
\ttindex{ClassicalFun}, which takes the argument
-signature\indexbold{*CLASSICAL_DATA}
+signature {\tt CLASSICAL_DATA}:
\begin{ttbox}
signature CLASSICAL_DATA =
sig
@@ -387,13 +388,13 @@
\end{ttbox}
Thus, the functor requires the following items:
\begin{ttdescription}
-\item[\ttindexbold{mp}] should be the Modus Ponens rule
+\item[\tdxbold{mp}] should be the Modus Ponens rule
$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.

-\item[\ttindexbold{not_elim}] should be the contradiction rule
+\item[\tdxbold{not_elim}] should be the contradiction rule
$\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.

-\item[\ttindexbold{swap}] should be the swap rule
+\item[\tdxbold{swap}] should be the swap rule
$\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.

\item[\ttindexbold{sizef}] is the heuristic function used for best-first
@@ -403,7 +404,7 @@
those concerned with type checking).  A heuristic function might simply
count the subgoals.

-\item[\ttindexbold{hyp_subst_tac}] is a list of tactics for substitution in
+\item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
the hypotheses, typically created by \ttindex{HypsubstFun} (see
Chapter~\ref{substitution}).  This list can, of course, be empty.  The
tactics are assumed to be safe!
@@ -411,6 +412,6 @@
The functor is not at all sensitive to the formalization of the
object-logic.  It does not even examine the rules, but merely applies them
according to its fixed strategy.  The functor resides in {\tt
-Provers/classical.ML} on the Isabelle distribution directory.
+Provers/classical.ML} in the Isabelle distribution directory.

-\index{classical prover|)}
+\index{classical reasoner|)}