# HG changeset patch # User oheimb # Date 856022539 -3600 # Node ID 5e5c78ba955e80cf14ce307c6e8d708bc4f60be6 # Parent 7a962f6829ca6203d5a22812c029f9c44a7d41b8 description of safe vs. unsafe wrapper and the functions involved diff -r 7a962f6829ca -r 5e5c78ba955e doc-src/Ref/classical.tex --- a/doc-src/Ref/classical.tex Sat Feb 15 16:23:58 1997 +0100 +++ b/doc-src/Ref/classical.tex Sat Feb 15 17:02:19 1997 +0100 @@ -273,44 +273,64 @@ $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$. The classical reasoner allows you to modify this basic proof strategy by -applying an arbitrary {\bf wrapper tactical} to it. This affects each step of -the search. Usually it is the identity tactical, but it could apply another -tactic before or after the step tactic. It affects \ttindex{step_tac}, -\ttindex{slow_step_tac} and the tactics that call them. +applying two arbitrary {\bf wrapper tactical}s to it. This affects each step of +the search. Usually they are the identity tacticals, but they could apply +another tactic before or after the step tactic. The first one, which is +considered to be safe, affects \ttindex{safe_step_tac} and all the tactics that +call it. The the second one, which may be unsafe, affects +\ttindex{safe_step_tac}, \ttindex{slow_step_tac} and the tactics that call them. \begin{ttbox} addss : claset * simpset -> claset \hfill{\bf infix 4} -addbefore : claset * tactic -> claset \hfill{\bf infix 4} -addafter : claset * tactic -> claset \hfill{\bf infix 4} -setwrapper : claset * (tactic->tactic) -> claset \hfill{\bf infix 4} -compwrapper : claset * (tactic->tactic) -> claset \hfill{\bf infix 4} +addSbefore : claset * (int -> tactic) -> claset \hfill{\bf infix 4} +addSaltern : claset * (int -> tactic) -> claset \hfill{\bf infix 4} +setSWrapper : claset * ((int -> tactic) -> (int -> tactic)) -> claset \hfill{\bf infix 4} +compSWrapper : claset * ((int -> tactic) -> (int -> tactic)) -> claset \hfill{\bf infix 4} +addbefore : claset * (int -> tactic) -> claset \hfill{\bf infix 4} +addaltern : claset * (int -> tactic) -> claset \hfill{\bf infix 4} +setWrapper : claset * ((int -> tactic) -> (int -> tactic)) -> claset \hfill{\bf infix 4} +compWrapper : claset * ((int -> tactic) -> (int -> tactic)) -> claset \hfill{\bf infix 4} \end{ttbox} % \index{simplification!from classical reasoner} -The wrapper tactical underlies the operator \ttindex{addss}, which precedes +The wrapper tacticals underly the operator \ttindex{addss}, which combines each search step by simplification. Strictly speaking, {\tt addss} is not -part of the classical reasoner. It should be defined (using {\tt addbefore}) -when the simplifier is installed. +part of the classical reasoner. It should be defined (using {\tt addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss)}) when the simplifier is installed. \begin{ttdescription} \item[$cs$ addss $ss$] \indexbold{*addss} -adds the simpset~$ss$ to the classical set. The assumptions and goal will be -simplified before each step of the search. +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. + +\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. + +\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 wrapper tactical to apply the given tactic {\em before} -each step of the search. +changes the (unsafe) wrapper tactical to apply the given tactic, which should +be safe, {\em before} each step of the search. -\item[$cs$ addafter $tac$] \indexbold{*addafter} -changes the wrapper tactical to apply the given tactic {\em after} -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 wrapper tactical. +\item[$cs$ setWrapper $tactical$] \indexbold{*setWrapper} +specifies a new (unsafe) wrapper tactical. -\item[$cs$ compwrapper $tactical$] \indexbold{*compwrapper} -composes the $tactical$ with the existing wrapper tactical, to combine their -effects. +\item[$cs$ compWrapper $tactical$] \indexbold{*compWrapper} +composes the $tactical$ with the existing (unsafe) wrapper tactical, +to combine their effects. \end{ttdescription} @@ -383,8 +403,9 @@ 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$. This may include proof by assumption or Modus Ponens (taking -care not to instantiate unknowns), or {\tt hyp_subst_tac}. +subgoal~$i$. The safe wrapper tactical is applied to a tactic that may include +proof by assumption or Modus Ponens (taking care not to instantiate unknowns), +or {\tt hyp_subst_tac}. \item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all subgoals. It is deterministic, with at most one outcome. If the automatic @@ -395,8 +416,8 @@ but allows unknowns to be instantiated. \item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof - procedure. The wrapper tactical is applied to a tactic that tries {\tt - safe_tac}, {\tt inst_step_tac}, or applies an unsafe rule from~$cs$. + procedure. The (unsafe) wrapper tactical is applied to a tactic that tries + {\tt safe_tac}, {\tt inst_step_tac}, or applies an unsafe rule from~$cs$. \item[\ttindexbold{slow_step_tac}] resembles {\tt step_tac}, but allows backtracking between using safe