\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}

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}

\subsection{Semi-automatic tactics}

\begin{ttbox} 

clarify_step_tac : claset -> int -> tactic

\end{ttbox}

\begin{ttdescription}

\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{Other classical tactics}

\begin{ttbox} 

slow_best_tac : claset -> int -> tactic

\end{ttbox}

\begin{ttdescription}

\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

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{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: