--- a/doc-src/Ref/classical.tex Mon Aug 27 17:11:55 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,224 +0,0 @@
-
-\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: