src/Provers/simplifier.ML

--- a/src/Provers/simplifier.ML	Mon Nov 16 11:09:02 1998 +0100
+++ b/src/Provers/simplifier.ML	Mon Nov 16 11:10:00 1998 +0100
@@ -163,8 +163,8 @@
 
 fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
     addloop tac = make_ss (mss, subgoal_tac, 
-	(case assoc_string (loop_tacs,(fst tac)) of None => () | Some x => 
-	 warning ("overwriting looper "^fst tac); overwrite(loop_tacs,tac)),
+        (case assoc_string (loop_tacs,(fst tac)) of None => () | Some x => 
+         warning ("overwriting looper "^fst tac); overwrite(loop_tacs,tac)),
            finish_tac, unsafe_finish_tac);
 
 fun (ss as Simpset {mss,subgoal_tac,loop_tacs,finish_tac,unsafe_finish_tac})
@@ -245,7 +245,7 @@
       subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
 
 
-(* merge simpsets *)	(*NOTE: ignores tactics of 2nd simpset (except loopers)*)
+(* merge simpsets *)    (*NOTE: ignores tactics of 2nd simpset (except loopers)*)
 
 fun merge_ss
    (Simpset {mss = mss1, loop_tacs = loop_tacs1, subgoal_tac, finish_tac, unsafe_finish_tac},
@@ -265,7 +265,7 @@
   type T = simpset ref;
 
   val empty = ref empty_ss;
-  fun prep_ext (ref ss) = (ref ss): T;		  (*create new reference!*)
+  fun prep_ext (ref ss) = (ref ss): T;            (*create new reference!*)
   fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
   fun print _ (ref ss) = print_ss ss;
 end;
@@ -314,6 +314,22 @@
 val put_local_simpset = LocalSimpset.put;
 
 
+(* attributes *)
+
+fun change_global_ss f (thy, th) =
+  let val r = simpset_ref_of thy
+  in r := f (! r, [Attribute.thm_of th]); (thy, th) end;
+
+fun change_local_ss f (ctxt, th) =
+  let val ss = f (get_local_simpset ctxt, [Attribute.thm_of th])
+  in (put_local_simpset ss ctxt, th) end;
+
+val simp_add_global = change_global_ss (op addsimps);
+val simp_del_global = change_global_ss (op delsimps);
+val simp_add_local = change_local_ss (op addsimps);
+val simp_del_local = change_local_ss (op delsimps);
+
+
 
 (** simplification tactics **)
 
@@ -382,42 +398,30 @@
 
 
 
-(** attributes **)
+(** concrete syntax of attributes **)
 
-(* add / del rules *)
+(* add / del *)
 
 val simp_addN = "add";
 val simp_delN = "del";
-
-val addsimps' = Attribute.lift_modifier (op addsimps);
-val delsimps' = Attribute.lift_modifier (op delsimps);
-
-local
-  fun change_global_ss f (thy, tth) =
-    let val r = simpset_ref_of thy
-    in r := f (! r, [tth]); (thy, tth) end;
+val simp_ignoreN = "other";
 
-  fun change_local_ss f (ctxt, tth) =
-    let val ss = f (get_local_simpset ctxt, [tth])
-    in (put_local_simpset ss ctxt, tth) end;
+fun simp_att change =
+  (Args.$$$ simp_addN >> K (op addsimps) ||
+    Args.$$$ simp_delN >> K (op delsimps) ||
+    Scan.succeed (op addsimps))
+  >> change
+  |> Scan.lift
+  |> Attrib.syntax;
 
-  fun simp_att change = Attrib.syntax
-    (Args.$$$ simp_delN >> K delsimps' ||
-      Args.$$$ simp_addN >> K addsimps' || Scan.succeed addsimps') change;
-in
-  val simp_add_global = change_global_ss addsimps';
-  val simp_del_global = change_global_ss delsimps';
-  val simp_add_local = change_local_ss addsimps';
-  val simp_del_local = change_local_ss delsimps';
-  val simp_attr = (simp_att change_global_ss, simp_att change_local_ss);
-end;
+val simp_attr = (simp_att change_global_ss, simp_att change_local_ss);
 
 
 (* conversions *)
 
 fun conv_attr f =
-  (Attrib.no_args (Attribute.rule simpset_of f),
-    Attrib.no_args (Attribute.rule get_local_simpset f));
+  (Attrib.no_args (Attribute.rule (f o simpset_of)),
+    Attrib.no_args (Attribute.rule (f o get_local_simpset)));
 
 
 (* setup_attrs *)
@@ -435,37 +439,29 @@
 
 (* simplification *)
 
-fun smart_simp_tac [] ss i = simp_tac ss i
-  | smart_simp_tac facts ss i =
-      REPEAT_DETERM (etac Drule.thin_rl i) THEN
-      metacuts_tac (map Attribute.thm_of facts) i THEN
-      asm_full_simp_tac ss i;
-
-fun smart_simp ss = Method.METHOD (fn facts => FIRSTGOAL (smart_simp_tac facts ss));
-
+val simp_args =
+  Method.only_sectioned_args
+   [Args.$$$ simp_addN >> K simp_add_local,
+    Args.$$$ simp_delN >> K simp_del_local,
+    Args.$$$ simp_ignoreN >> K I];
 
-(* simp methods *)	(* FIXME !? *)
-
-fun simp_args meth =
-  Method.sectioned_args get_local_simpset addsimps'
-    [(simp_addN, addsimps'), (simp_delN, delsimps')] meth;
+fun simp_meth tac ctxt = Method.METHOD (fn facts =>
+  FIRSTGOAL (REPEAT_DETERM o etac Drule.thin_rl THEN'
+    metacuts_tac (Attribute.thms_of facts) THEN'
+    tac (get_local_simpset ctxt)));
 
-fun gen_simp tac =
-  let
-    fun tac' x = FIRSTGOAL (CHANGED o tac x);
-    fun meth ss = Method.METHOD (fn facts => tac' (addsimps' (ss, facts)));
-  in simp_args meth end;
+val simp_method = simp_args o simp_meth;
 
 
 (* setup_methods *)
 
 val setup_methods = Method.add_methods
- [("simp",          simp_args smart_simp, "simplification"),
-  ("simp_tac",      gen_simp simp_tac, "simp_tac"),
-  ("asm_simp",      gen_simp asm_simp_tac, "asm_simp_tac"),
-  ("full_simp",     gen_simp full_simp_tac, "full_simp_tac"),
-  ("asm_full_simp", gen_simp asm_full_simp_tac, "asm_full_simp_tac"),
-  ("asm_lr_simp",   gen_simp asm_lr_simp_tac, "asm_lr_simp_tac")];
+ [("simp",              simp_method asm_full_simp_tac, "simplification"),
+  ("simp_tac",          simp_method simp_tac, "simp_tac"),
+  ("asm_simp_tac",      simp_method asm_simp_tac, "asm_simp_tac"),
+  ("full_simp_tac",     simp_method full_simp_tac, "full_simp_tac"),
+  ("asm_full_simp_tac", simp_method asm_full_simp_tac, "asm_full_simp_tac"),
+  ("asm_lr_simp_tac",   simp_method asm_lr_simp_tac, "asm_lr_simp_tac")];