# HG changeset patch
# User wenzelm
# Date 953141813 -3600
# Node ID 58dbeea60bb86ee0d285821677fa0156ae500bbe
# Parent  f7b06595d0c8666df4b75da850999410fd17ee91
export change_global_ss, change_local_ss;
separate method_setup, includes further modifiers;
clear_ss / 'only': remove loopers as well;
simp_modifiers: 'add' optional;

diff -r f7b06595d0c8 -r 58dbeea60bb8 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Wed Mar 15 18:33:41 2000 +0100
+++ b/src/Provers/simplifier.ML	Wed Mar 15 18:36:53 2000 +0100
@@ -87,6 +87,8 @@
   val print_local_simpset: Proof.context -> unit
   val get_local_simpset: Proof.context -> simpset
   val put_local_simpset: simpset -> Proof.context -> Proof.context
+  val change_global_ss: (simpset * thm list -> simpset) -> theory attribute
+  val change_local_ss: (simpset * thm list -> simpset) -> Proof.context attribute
   val simp_add_global: theory attribute
   val simp_del_global: theory attribute
   val simp_add_local: Proof.context attribute
@@ -94,6 +96,8 @@
   val change_simpset_of: (simpset * 'a -> simpset) -> 'a -> theory -> theory
   val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   val setup: (theory -> theory) list
+  val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
+    -> (theory -> theory) list
   val easy_setup: thm -> thm list -> (theory -> theory) list
 end;
 
@@ -113,6 +117,8 @@
 
 fun rep_simproc (Simproc args) = args;
 
+
+
 (** solvers **)
 
 datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
@@ -127,6 +133,8 @@
   | app_sols (Solver(_,solver,_)::sols) thms i =
        solver thms i ORELSE app_sols sols thms i;
 
+
+
 (** simplification sets **)
 
 (* type simpset *)
@@ -260,12 +268,13 @@
     (Thm.del_simprocs (mss, map rep_simproc simprocs),
       subgoal_tac, loop_tacs, unsafe_solvers, solvers);
 
-fun clear_ss (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers}) =
-  make_ss (Thm.clear_mss mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers);
+fun clear_ss (Simpset {mss, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers}) =
+  make_ss (Thm.clear_mss mss, subgoal_tac, [], unsafe_solvers, solvers);
 
 
 (* merge simpsets *)
-(*NOTE: ignores subgoal_tac of 2nd simpset *)
+
+(*ignores subgoal_tac of 2nd simpset!*)
 
 fun merge_ss
    (Simpset {mss = mss1, loop_tacs = loop_tacs1, subgoal_tac,
@@ -278,6 +287,7 @@
     merge_solvers solvers1 solvers2);
 
 
+
 (** global and local simpset data **)
 
 (* theory data kind 'Provers/simpset' *)
@@ -462,7 +472,7 @@
 (* setup_attrs *)
 
 val setup_attrs = Attrib.add_attributes
- [(simpN,               simp_attr, "simplification rule"),
+ [(simpN,               simp_attr, "declare simplification rule"),
   ("simplify",          conv_attr simplify, "simplify rule"),
   ("asm_simplify",      conv_attr asm_simplify, "simplify rule, using assumptions"),
   ("full_simplify",     conv_attr full_simplify, "fully simplify rule"),
@@ -477,7 +487,8 @@
 val colon = Args.$$$ ":";
 
 val simp_modifiers =
- [Args.$$$ simpN -- Args.$$$ addN -- colon >> K (I, simp_add_local),
+ [Args.$$$ simpN -- colon >> K (I, simp_add_local),
+  Args.$$$ simpN -- Args.$$$ addN -- colon >> K (I, simp_add_local),
   Args.$$$ simpN -- Args.$$$ delN -- colon >> K (I, simp_del_local),
   Args.$$$ simpN -- Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local),
   Args.$$$ otherN -- colon >> K (I, I)];
@@ -488,34 +499,36 @@
   Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local),
   Args.$$$ otherN -- colon >> K (I, I)];
 
-fun simp_method tac =
+fun simp_method more_mods tac =
   (fn prems => fn ctxt => Method.METHOD (fn facts =>
     ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_simpset ctxt)))
-  |> Method.bang_sectioned_args simp_modifiers';
+  |> Method.bang_sectioned_args (more_mods @ simp_modifiers');
 
-fun simp_method' tac =
+fun simp_method' more_mods tac =
   (fn prems => fn ctxt => Method.METHOD (fn facts =>
     HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
-  |> Method.bang_sectioned_args simp_modifiers';
+  |> Method.bang_sectioned_args (more_mods @ simp_modifiers');
   
 
 (* setup_methods *)
 
-val setup_methods = Method.add_methods
- [(simpN,               simp_method' (CHANGED oo asm_full_simp_tac), "full simplification"),
-  ("simp_all",          simp_method  (CHANGED o ALLGOALS o asm_full_simp_tac),
+fun setup_methods more_mods = Method.add_methods
+ [(simpN,               simp_method' more_mods
+    (CHANGED oo asm_full_simp_tac), "full simplification"),
+  ("simp_all",          simp_method  more_mods (CHANGED o ALLGOALS o asm_full_simp_tac),
     "full simplification (all goals)"),
-  ("simp_tac",          simp_method' simp_tac, "simp_tac (improper!)"),
-  ("asm_simp_tac",      simp_method' asm_simp_tac, "asm_simp_tac (improper!)"),
-  ("full_simp_tac",     simp_method' full_simp_tac, "full_simp_tac (improper!)"),
-  ("asm_full_simp_tac", simp_method' asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
-  ("asm_lr_simp_tac",   simp_method' asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];
+  ("simp_tac",          simp_method' more_mods simp_tac, "simp_tac (improper!)"),
+  ("asm_simp_tac",      simp_method' more_mods asm_simp_tac, "asm_simp_tac (improper!)"),
+  ("full_simp_tac",     simp_method' more_mods full_simp_tac, "full_simp_tac (improper!)"),
+  ("asm_full_simp_tac", simp_method' more_mods asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
+  ("asm_lr_simp_tac",   simp_method' more_mods asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];
 
 
 
 (** theory setup **)
 
-val setup = [GlobalSimpset.init, LocalSimpset.init, setup_attrs, setup_methods];
+val setup = [GlobalSimpset.init, LocalSimpset.init, setup_attrs];
+fun method_setup mods = [setup_methods mods];
 
 fun easy_setup reflect trivs =
   let
@@ -540,7 +553,7 @@
         setSSolver safe_solver
         setSolver unsafe_solver
         setmksimps mksimps; thy);
-  in setup @ [init_ss] end;
+  in setup @ method_setup [] @ [init_ss] end;
 
 
 end;