
diff -r d468d72a458f -r 83bd9eb1c70c doc-src/Ref/document/classical.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Ref/document/classical.tex	Mon Aug 27 17:24:01 2012 +0200
@@ -0,0 +1,224 @@
+
+\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{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{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}
+
+
+\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: 




