# HG changeset patch
# User wenzelm
# Date 953141932 -3600
# Node ID d99902232df8e1ce42bee017172411690e8868d4
# Parent  58dbeea60bb86ee0d285821677fa0156ae500bbe
added attributes, method modifiers, theory setup;

diff -r 58dbeea60bb8 -r d99902232df8 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Mar 15 18:36:53 2000 +0100
+++ b/src/Provers/splitter.ML	Wed Mar 15 18:38:52 2000 +0100
@@ -32,12 +32,19 @@
   val delsplits       : simpset * thm list -> simpset
   val Addsplits       : thm list -> unit
   val Delsplits       : thm list -> unit
+  val split_add_global: theory attribute
+  val split_del_global: theory attribute
+  val split_add_local: Proof.context attribute
+  val split_del_local: Proof.context attribute
+  val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
+  val setup: (theory -> theory) list
 end;
 
 functor SplitterFun(Data: SPLITTER_DATA): SPLITTER =
 struct 
 
-type simpset = Data.Simplifier.simpset;
+structure Simplifier = Data.Simplifier;
+type simpset = Simplifier.simpset;
 
 val Const ("==>", _) $ (Const ("Trueprop", _) $
          (Const (const_not, _) $ _    )) $ _ = #prop (rep_thm(Data.notnotD));
@@ -361,24 +368,68 @@
   in SUBGOAL tac
   end;
 
+
+
+(** declare split rules **)
+
+(* addsplits / delsplits *)
+
 fun split_name name asm = "split " ^ name ^ (if asm then " asm" else "");
 
 fun ss addsplits splits =
   let fun addsplit (ss,split) =
         let val (name,asm) = split_thm_info split
-        in Data.Simplifier.addloop(ss,(split_name name asm,
+        in Simplifier.addloop(ss,(split_name name asm,
 		       (if asm then split_asm_tac else split_tac) [split])) end
   in foldl addsplit (ss,splits) end;
 
 fun ss delsplits splits =
   let fun delsplit(ss,split) =
         let val (name,asm) = split_thm_info split
-        in Data.Simplifier.delloop(ss,split_name name asm)
+        in Simplifier.delloop(ss,split_name name asm)
   end in foldl delsplit (ss,splits) end;
 
-fun Addsplits splits = (Data.Simplifier.simpset_ref() := 
-			Data.Simplifier.simpset() addsplits splits);
-fun Delsplits splits = (Data.Simplifier.simpset_ref() := 
-			Data.Simplifier.simpset() delsplits splits);
+fun Addsplits splits = (Simplifier.simpset_ref() := 
+			Simplifier.simpset() addsplits splits);
+fun Delsplits splits = (Simplifier.simpset_ref() := 
+			Simplifier.simpset() delsplits splits);
+
+
+(* attributes *)
+
+val splitN = "split";
+val addN = "add";
+val delN = "del";
+
+fun split_att change =
+  (Args.$$$ addN >> K (op addsplits) ||
+    Args.$$$ delN >> K (op delsplits) ||
+    Scan.succeed (op addsplits))
+  >> change
+  |> Scan.lift
+  |> Attrib.syntax;
+
+val setup_attrs = Attrib.add_attributes
+ [(splitN, (split_att Simplifier.change_global_ss, split_att Simplifier.change_local_ss),
+    "declare splitter rule")];
+
+val split_add_global = Simplifier.change_global_ss (op addsplits);
+val split_del_global = Simplifier.change_global_ss (op delsplits);
+val split_add_local = Simplifier.change_local_ss (op addsplits);
+val split_del_local = Simplifier.change_local_ss (op delsplits);
+
+
+(* method modifiers *)
+
+val split_modifiers =
+ [Args.$$$ splitN -- Args.$$$ ":" >> K (I, split_add_local),
+  Args.$$$ splitN -- Args.$$$ addN -- Args.$$$ ":" >> K (I, split_add_local),
+  Args.$$$ splitN -- Args.$$$ delN -- Args.$$$ ":" >> K (I, split_del_local)];
+
+
+
+(** theory setup **)
+
+val setup = [setup_attrs];
 
 end;