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: