# HG changeset patch # User oheimb # Date 894045063 -7200 # Node ID d80faf83c82f4e65072a9e71dc4f5b1423c596e2 # Parent 312115d20c45d34fa42004aa3d8ff220b8d54a77 corrected and updated description of wrapper mechanism (including addss) added documentation of force_tac diff -r 312115d20c45 -r d80faf83c82f doc-src/Ref/classical.tex --- a/doc-src/Ref/classical.tex Fri May 01 11:43:38 1998 +0200 +++ b/doc-src/Ref/classical.tex Fri May 01 19:51:03 1998 +0200 @@ -329,7 +329,7 @@ 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 \ttindex{step_tac}, -\ttindex{slow_step_tac} and the tactics that call them. +\ttindex{slow_step_tac}, and the tactics that call them. A wrapper transforms each step of the search, for example by invoking other tactics before or alternatively to the original step tactic. All members of a wrapper list are applied in turn to the respective step tactic. @@ -341,63 +341,79 @@ \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} addSaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} -addSWrapper : claset * (string * wrapper ) -> 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} addaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} -addWrapper : claset * (string * wrapper ) -> 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} % -\index{simplification!from classical reasoner} The wrapper tacticals -underly the operator addss, which combines each search step by -simplification. Strictly speaking, \texttt{addss} is not part of the -classical reasoner. It should be defined when the simplifier is -installed: -\begin{ttbox} -infix 4 addss; -fun cs addss ss = cs addbefore asm_full_simp_tac ss; -\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 safe wrapper, such that it is +applied {\em before} each safe step of the search. + +\item[$cs$ addSaltern $(name,tac)$] \indexbold{*addSaltern} +adds the given tactic as safe wrapper, such that it is +applied 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 unsafe wrapper, such that it is +applied {\em before} each step of the search. + +\item[$cs$ addaltern $(name,tac)$] \indexbold{*addaltern} +adds the given tactic as unsafe wrapper, such that it is +applied when a step of the search would fail. + +\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, in a safe way, after the safe steps of the search. - -\item[$cs$ addSbefore $tac$] \indexbold{*addSbefore} -changes the safe wrapper tactical to apply the given tactic {\em before} -each safe step of the search. +simplified, before the each unsafe step of the search. -\item[$cs$ addSaltern $tac$] \indexbold{*addSaltern} -changes the safe wrapper tactical to apply the given tactic when a safe step -of the search would fail. - -\item[$cs$ setSWrapper $tactical$] \indexbold{*setSWrapper} -specifies a new safe wrapper tactical. +\end{ttdescription} -\item[$cs$ compSWrapper $tactical$] \indexbold{*compSWrapper} -composes the $tactical$ with the existing safe wrapper tactical, -to combine their effects. - -\item[$cs$ addbefore $tac$] \indexbold{*addbefore} -changes the (unsafe) wrapper tactical to apply the given tactic, which should -be safe, {\em before} each step of the search. - -\item[$cs$ addaltern $tac$] \indexbold{*addaltern} -changes the (unsafe) wrapper tactical to apply the given tactic -{\em alternatively} after each step of the search. - -\item[$cs$ setWrapper $tactical$] \indexbold{*setWrapper} -specifies a new (unsafe) wrapper tactical. - -\item[$cs$ compWrapper $tactical$] \indexbold{*compWrapper} -composes the $tactical$ with the existing (unsafe) wrapper tactical, -to combine their effects. -\end{ttdescription} +\index{simplification!from classical reasoner} The wrapper tacticals +underly the operators addss and addSss, which are used as primitives +for the automatic tactics described in \S\label{sec:automatic-tactics}. +Strictly speaking, both operators are not part of the classical reasoner. +They should be defined when the simplifier is installed: +\begin{ttbox} +infix 4 addSss addss; +fun cs addSss ss = cs addSaltern ("safe_asm_full_simp_tac", + CHANGED o (safe_asm_full_simp_tac ss)); +fun cs addss ss = cs addbefore ("asm_full_simp_tac", asm_full_simp_tac ss); +\end{ttbox} +\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} @@ -473,22 +489,36 @@ \end{ttdescription} -\subsection{An automatic tactic} +\subsection{Automatic tactics}\label{sec:automatic-tactics} \begin{ttbox} -auto_tac : claset * simpset -> tactic -auto : unit -> unit +type clasimpset = claset * simpset; +auto_tac : clasimpset -> tactic +force_tac : clasimpset -> int -> tactic +auto : unit -> unit +force : int -> unit \end{ttbox} -The auto-tactic attempts to prove all subgoals using a combination of -simplification and classical reasoning. It is intended for situations where -there are a lot of mostly trivial subgoals; it proves all the easy ones, -leaving the ones it cannot prove. (Unfortunately, attempting to prove the -hard ones may take a long time.) It must be supplied both a simpset and a -claset; therefore it is most easily called as \texttt{Auto_tac}, which uses -the default claset and simpset (see \S\ref{sec:current-claset} below). For -interactive use, the shorthand \texttt{auto();} abbreviates +The automatic tactics attempt to prove goals using a combination of +simplification and classical reasoning. +\begin{itemize} +\item[\ttindexbold{auto_tac $(cs,ss)$}] is intended for situations where +there are a lot of mostly trivial subgoals; it proves all the easy ones, +leaving the ones it cannot prove. +(Unfortunately, attempting to prove the hard ones may take a long time.) +\item[\ttindexbold{force_tac} $(cs,ss)$ $i$] is intended to prove subgoal~$i$ +completely. It tries to apply all fancy tactics it knows about, +performing a rather exhaustive search. +\end{itemize} +They must be supplied both a simpset and a claset; therefore +they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which +use the default claset and simpset (see \S\ref{sec:current-claset} below). +For interactive use, the shorthand \texttt{auto();} abbreviates \begin{ttbox} by Auto_tac; \end{ttbox} +while \texttt{force 1;} abbreviates +\begin{ttbox} +by (Force_tac 1); +\end{ttbox} \subsection{Other classical tactics} \begin{ttbox} @@ -557,7 +587,7 @@ 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 tactical is applied to a tactic that may + 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. @@ -568,7 +598,7 @@ but allows unknowns to be instantiated. \item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof - procedure. The (unsafe) wrapper tactical is applied to a tactic that tries + 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}] @@ -597,6 +627,7 @@ \begin{ttbox} Blast_tac : int -> tactic Auto_tac : tactic +Force_tac : int -> tactic Fast_tac : int -> tactic Best_tac : int -> tactic Deepen_tac : int -> int -> tactic @@ -606,7 +637,7 @@ Safe_step_tac : int -> tactic Step_tac : int -> tactic \end{ttbox} -\indexbold{*Blast_tac}\indexbold{*Auto_tac} +\indexbold{*Blast_tac}\indexbold{*Auto_tac}\indexbold{*Force_tac} \indexbold{*Best_tac}\indexbold{*Fast_tac}% \indexbold{*Deepen_tac} \indexbold{*Clarify_tac}\indexbold{*Clarify_step_tac}