# HG changeset patch # User oheimb # Date 888417932 -3600 # Node ID 89ad3eb863a15b72f4ed2506e3ae211088824829 # Parent f04da668581cd5758581e9968641a806fb89e035 changed wrapper mechanism of classical reasoner diff -r f04da668581c -r 89ad3eb863a1 NEWS --- a/NEWS Tue Feb 24 11:35:33 1998 +0100 +++ b/NEWS Wed Feb 25 15:45:32 1998 +0100 @@ -1,7 +1,23 @@ + + Isabelle NEWS -- history of user-visible changes ================================================ +New in Isabelle98? (???) +----------------------- + +* changed wrapper mechanism for the classical reasoner now allows for selected + deletion of wrappers, by introduction of names for wrapper functionals. + This implies that addbefore, addSbefore, addaltern, and addSaltern now take + a pair (name, tactic) as argument, and that adding two tactics with the same + name overwrites the first one (emitting a warning). + setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by + addWrapper, addSWrapper: claset * wrapper -> claset + delWrapper, delSWrapper: claset * string -> claset + getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; + + New in Isabelle98 (January 1998) -------------------------------- diff -r f04da668581c -r 89ad3eb863a1 doc-src/Ref/classical.tex --- a/doc-src/Ref/classical.tex Tue Feb 24 11:35:33 1998 +0100 +++ b/doc-src/Ref/classical.tex Wed Feb 25 15:45:32 1998 +0100 @@ -311,29 +311,33 @@ 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 arbitrary {\bf - wrapper tacticals} 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{step_tac}, \ttindex{slow_step_tac} and the tactics that call -them. +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 \ttindex{step_tac}, +\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. + +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); +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} +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} + addss : claset * simpset -> 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 tacticals @@ -343,7 +347,7 @@ installed: \begin{ttbox} infix 4 addss; -fun cs addss ss = cs addbefore asm_full_simp_tac ss; +fun cs addss ss = cs addbefore asm_full_simp_tac ss; \end{ttbox} \begin{ttdescription} diff -r f04da668581c -r 89ad3eb863a1 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Tue Feb 24 11:35:33 1998 +0100 +++ b/src/FOL/simpdata.ML Wed Feb 25 15:45:32 1998 +0100 @@ -334,8 +334,9 @@ (*Add a simpset to a classical set!*) infix 4 addSss addss; -fun cs addSss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss)); -fun cs addss ss = cs addbefore asm_full_simp_tac ss; +fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac", + CHANGED o (safe_asm_more_full_simp_tac ss)); +fun cs addss ss = cs addbefore ("asm_full_simp_tac", asm_full_simp_tac ss); fun Addss ss = (claset_ref() := claset() addss ss);