doc-src/Ref/classical.tex

moved/updated introduction to Classical Reasoner;

\chapter{The Classical Reasoner}\label{chap:classical}
\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}
\begin{ttbox}
addSE2      : claset * (string * thm) -> claset           \hfill{\bf infix 4}
addSD2      : claset * (string * thm) -> claset           \hfill{\bf infix 4}
addE2       : claset * (string * thm) -> claset           \hfill{\bf infix 4}
addD2       : claset * (string * thm) -> claset           \hfill{\bf infix 4}
\end{ttbox}
\begin{warn}
  A rule to be added in this special way must be given a name, which is used 
  to delete it again -- when desired -- using \texttt{delSWrappers} or 
  \texttt{delWrappers}, respectively. This is because these add operations
  are implemented as wrappers (see \ref{sec:modifying-search} below).
\end{warn}


\subsection{Modifying the search step}
\label{sec:modifying-search}
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 \texttt{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 \texttt{blast_tac}! --- allow
you to modify this basic proof strategy by applying two lists of arbitrary 
{\bf wrapper tacticals} to it. 
The first wrapper list, which is considered to contain safe wrappers only, 
affects \ttindex{safe_step_tac} and all the tactics that call it.  
The second one, which may contain unsafe wrappers, affects the unsafe parts
of \ttindex{step_tac}, \ttindex{slow_step_tac}, and the tactics that call them.
A wrapper transforms each step of the search, for example 
by attempting other tactics before or after the original step tactic. 
All members of a wrapper list are applied in turn to the respective step tactic.

Initially the two wrapper lists are empty, which means no modification of the
step tactics. Safe and unsafe wrappers are added to a claset 
with the functions given below, supplying them with wrapper names. 
These names may be used to selectively delete wrappers.

\begin{ttbox} 
type wrapper = (int -> tactic) -> (int -> tactic);

addSWrapper  : claset * (string *  wrapper       ) -> claset \hfill{\bf infix 4}
addSbefore   : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
addSafter    : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
delSWrapper  : claset *  string                    -> claset \hfill{\bf infix 4}

addWrapper   : claset * (string *  wrapper       ) -> claset \hfill{\bf infix 4}
addbefore    : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
addafter     : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
delWrapper   : claset *  string                    -> claset \hfill{\bf infix 4}

addSss       : claset * simpset -> claset                 \hfill{\bf infix 4}
addss        : claset * simpset -> claset                 \hfill{\bf infix 4}
\end{ttbox}
%

\begin{ttdescription}
\item[$cs$ addSWrapper $(name,wrapper)$] \indexbold{*addSWrapper}
adds a new wrapper, which should yield a safe tactic, 
to modify the existing safe step tactic.

\item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore}
adds the given tactic as a safe wrapper, such that it is tried 
{\em before} each safe step of the search.

\item[$cs$ addSafter $(name,tac)$] \indexbold{*addSafter}
adds the given tactic as a safe wrapper, such that it is tried 
when a safe step of the search would fail.

\item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper}
deletes the safe wrapper with the given name.

\item[$cs$ addWrapper $(name,wrapper)$] \indexbold{*addWrapper}
adds a new wrapper to modify the existing (unsafe) step tactic.

\item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore}
adds the given tactic as an unsafe wrapper, such that it its result is 
concatenated {\em before} the result of each unsafe step.

\item[$cs$ addafter $(name,tac)$] \indexbold{*addafter}
adds the given tactic as an unsafe wrapper, such that it its result is 
concatenated {\em after} the result of each unsafe step.

\item[$cs$ delWrapper $name$] \indexbold{*delWrapper}
deletes the unsafe wrapper with the given name.

\item[$cs$ addSss $ss$] \indexbold{*addss}
adds the simpset~$ss$ to the classical set.  The assumptions and goal will be
simplified, in a rather safe way, after each safe step of the search.

\item[$cs$ addss $ss$] \indexbold{*addss}
adds the simpset~$ss$ to the classical set.  The assumptions and goal will be
simplified, before the each unsafe step of the search.

\end{ttdescription}

\index{simplification!from classical reasoner} 
Strictly speaking, the operators \texttt{addss} and \texttt{addSss}
are not part of the classical reasoner.
, which are used as primitives 
for the automatic tactics described in {\S}\ref{sec:automatic-tactics}, are
implemented as wrapper tacticals.
they  
\begin{warn}
Being defined as wrappers, these operators are inappropriate for adding more 
than one simpset at a time: the simpset added last overwrites any earlier ones.
When a simpset combined with a claset is to be augmented, this should done 
{\em before} combining it with the claset.
\end{warn}


\section{The classical tactics}
\index{classical reasoner!tactics} If installed, the classical module provides
powerful theorem-proving tactics.


\subsection{The tableau prover}
The tactic \texttt{blast_tac} searches for a proof using a fast tableau prover,
coded directly in \ML.  It then reconstructs the proof using Isabelle
tactics.  It is faster and more powerful than the other classical
reasoning tactics, but has major limitations too.
\begin{itemize}
\item It does not use the wrapper tacticals described above, such as
  \ttindex{addss}.
\item It does not perform higher-order unification, as needed by the rule {\tt
    rangeI} in HOL and \texttt{RepFunI} in ZF.  There are often alternatives
  to such rules, for example {\tt range_eqI} and \texttt{RepFun_eqI}.
\item Function variables may only be applied to parameters of the subgoal.
(This restriction arises because the prover does not use higher-order
unification.)  If other function variables are present then the prover will
fail with the message {\small\tt Function Var's argument not a bound variable}.
\item Its proof strategy is more general than \texttt{fast_tac}'s but can be
  slower.  If \texttt{blast_tac} fails or seems to be running forever, try {\tt
  fast_tac} and the other tactics described below.
\end{itemize}
%
\begin{ttbox} 
blast_tac        : claset -> int -> tactic
Blast.depth_tac  : claset -> int -> int -> tactic
Blast.trace      : bool ref \hfill{\bf initially false}
\end{ttbox}
The two tactics differ on how they bound the number of unsafe steps used in a
proof.  While \texttt{blast_tac} starts with a bound of zero and increases it
successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound.
\begin{ttdescription}
\item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove
  subgoal~$i$, increasing the search bound using iterative
  deepening~\cite{korf85}. 
  
\item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries
  to prove subgoal~$i$ using a search bound of $lim$.  Sometimes a slow
  proof using \texttt{blast_tac} can be made much faster by supplying the
  successful search bound to this tactic instead.
  
\item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover}
  causes the tableau prover to print a trace of its search.  At each step it
  displays the formula currently being examined and reports whether the branch
  has been closed, extended or split.
\end{ttdescription}


\subsection{Automatic tactics}\label{sec:automatic-tactics}
\begin{ttbox} 
type clasimpset = claset * simpset;
auto_tac        : clasimpset ->        tactic
force_tac       : clasimpset -> int -> tactic
auto            : unit -> unit
force           : int  -> unit
\end{ttbox}
The automatic tactics attempt to prove goals using a combination of
simplification and classical reasoning. 
\begin{ttdescription}
\item[\ttindexbold{auto_tac $(cs,ss)$}] is intended for situations where 
there are a lot of mostly trivial subgoals; it proves all the easy ones, 
leaving the ones it cannot prove.
(Unfortunately, attempting to prove the hard ones may take a long time.)  
\item[\ttindexbold{force_tac} $(cs,ss)$ $i$] is intended to prove subgoal~$i$ 
completely. It tries to apply all fancy tactics it knows about, 
performing a rather exhaustive search.
\end{ttdescription}


\subsection{Semi-automatic tactics}
\begin{ttbox} 
clarify_tac      : claset -> int -> tactic
clarify_step_tac : claset -> int -> tactic
clarsimp_tac     : clasimpset -> 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$ by repeatedly calling \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.
\item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but
also does simplification with the given simpset. Note that if the simpset 
includes a splitter for the premises, the subgoal may still be split.
\end{ttdescription}


\subsection{Other classical tactics}
\begin{ttbox} 
fast_tac      : claset -> int -> tactic
best_tac      : claset -> int -> tactic
slow_tac      : claset -> int -> tactic
slow_best_tac : claset -> int -> tactic
\end{ttbox}
These tactics attempt to prove a subgoal using sequent-style reasoning.
Unlike \texttt{blast_tac}, they construct proofs directly in Isabelle.  Their
effect is restricted (by \texttt{SELECT_GOAL}) to one subgoal; they either prove
this subgoal or fail.  The \texttt{slow_} versions conduct a broader
search.%
\footnote{They may, when backtracking from a failed proof attempt, undo even
  the step of proving a subgoal by assumption.}

The best-first tactics are guided by a heuristic function: typically, the
total size of the proof state.  This function is supplied in the functor call
that sets up the classical reasoner.
\begin{ttdescription}
\item[\ttindexbold{fast_tac} $cs$ $i$] applies \texttt{step_tac} using
depth-first search to prove subgoal~$i$.

\item[\ttindexbold{best_tac} $cs$ $i$] applies \texttt{step_tac} using
best-first search to prove subgoal~$i$.

\item[\ttindexbold{slow_tac} $cs$ $i$] applies \texttt{slow_step_tac} using
depth-first search to prove subgoal~$i$.

\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with
best-first search to prove subgoal~$i$.
\end{ttdescription}


\subsection{Depth-limited automatic tactics}
\begin{ttbox} 
depth_tac  : claset -> int -> int -> tactic
deepen_tac : claset -> int -> int -> tactic
\end{ttbox}
These work by exhaustive search up to a specified depth.  Unsafe rules are
modified to preserve the formula they act on, so that it be used repeatedly.
They can prove more goals than \texttt{fast_tac} can but are much
slower, for example if the assumptions have many universal quantifiers.

The depth limits the number of unsafe steps.  If you can estimate the minimum
number of unsafe steps needed, supply this value as~$m$ to save time.
\begin{ttdescription}
\item[\ttindexbold{depth_tac} $cs$ $m$ $i$] 
tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.

\item[\ttindexbold{deepen_tac} $cs$ $m$ $i$] 
tries to prove subgoal~$i$ by iterative deepening.  It calls \texttt{depth_tac}
repeatedly with increasing depths, starting with~$m$.
\end{ttdescription}


\subsection{Single-step tactics}
\begin{ttbox} 
safe_step_tac : claset -> int -> tactic
safe_tac      : claset        -> tactic
inst_step_tac : claset -> int -> tactic
step_tac      : claset -> int -> tactic
slow_step_tac : claset -> int -> tactic
\end{ttbox}
The automatic proof procedures call these tactics.  By calling them
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 tacticals are 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.  

\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
but allows unknowns to be instantiated.

\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
  procedure.  The unsafe wrapper tacticals are applied to a tactic that tries
  \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule
  from~$cs$.

\item[\ttindexbold{slow_step_tac}] 
  resembles \texttt{step_tac}, but allows backtracking between using safe
  rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules.
  The resulting search space is larger.
\end{ttdescription}


\subsection{Other useful tactics}
\index{tactics!for contradiction}
\index{tactics!for Modus Ponens}
\begin{ttbox} 
contr_tac    :             int -> tactic
mp_tac       :             int -> tactic
eq_mp_tac    :             int -> tactic
swap_res_tac : thm list -> int -> tactic
\end{ttbox}
These can be used in the body of a specialized search.
\begin{ttdescription}
\item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}
  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
  contradictions.

\item[\ttindexbold{mp_tac} {\it i}] 
is like \texttt{contr_tac}, but also attempts to perform Modus Ponens in
subgoal~$i$.  If there are assumptions $P\imp Q$ and~$P$, then it replaces
$P\imp Q$ by~$Q$.  It may instantiate unknowns.  It fails if it can do
nothing.

\item[\ttindexbold{eq_mp_tac} {\it i}] 
is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
is safe.

\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 prove the goal using \texttt{assume_tac} or
\texttt{contr_tac}.  It then attempts to apply each rule in turn, attempting
resolution and also elim-resolution with the swapped form.
\end{ttdescription}

\subsection{Creating swapped rules}
\begin{ttbox} 
swapify   : thm list -> thm list
joinrules : thm list * thm list -> (bool * thm) list
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the
swapped versions of~{\it thms}, regarded as introduction rules.

\item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]
joins introduction rules, their swapped versions, and elimination rules for
use with \ttindex{biresolve_tac}.  Each rule is paired with~\texttt{false}
(indicating ordinary resolution) or~\texttt{true} (indicating
elim-resolution).
\end{ttdescription}


\section{Setting up the classical reasoner}\label{sec:classical-setup}
\index{classical reasoner!setting up}
Isabelle's classical object-logics, including \texttt{FOL} and \texttt{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 \texttt{CLASSICAL_DATA}:
\begin{ttbox} 
signature CLASSICAL_DATA =
  sig
  val mp             : thm
  val not_elim       : thm
  val swap           : thm
  val sizef          : thm -> int
  val hyp_subst_tacs : (int -> tactic) list
  end;
\end{ttbox}
Thus, the functor requires the following items:
\begin{ttdescription}
\item[\tdxbold{mp}] should be the Modus Ponens rule
$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.

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

\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
search.  It should estimate the size of the remaining subgoals.  A good
heuristic function is \ttindex{size_of_thm}, which measures the size of the
proof state.  Another size function might ignore certain subgoals (say,
those concerned with type-checking).  A heuristic function might simply
count the subgoals.

\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!
\end{ttdescription}
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} in the Isabelle sources.

\index{classical reasoner|)}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "ref"
%%% End: