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