src/Provers/splitter.ML

 
 Generic case-splitter, suitable for most logics.
 Deals with equalities of the form ?P(f args) = ...
 where "f args" must be a first-order term without duplicate variables.
 *)
-
-infix 4 addsplits delsplits;
 
 signature SPLITTER_DATA =
 sig
   val thy           : theory
   val mk_eq         : thm -> thm

     (* first argument is a "cmap", returns a list of "split packs" *)
   (* the "real" interface, providing a number of tactics *)
   val split_tac       : thm list -> int -> tactic
   val split_inside_tac: thm list -> int -> tactic
   val split_asm_tac   : thm list -> int -> tactic
-  val addsplits       : simpset * thm list -> simpset
-  val delsplits       : simpset * thm list -> simpset
+  val add_split: thm -> simpset -> simpset
+  val del_split: thm -> simpset -> simpset
   val split_add: attribute
   val split_del: attribute
   val split_modifiers : Method.modifier parser list
   val setup: theory -> theory
 end;

       end;
 
 
 (** declare split rules **)
 
-(* addsplits / delsplits *)
+(* add_split / del_split *)
 
 fun string_of_typ (Type (s, Ts)) =
       (if null Ts then "" else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s
   | string_of_typ _ = "_";
 
 fun split_name (name, T) asm = "split " ^
   (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T;
 
-fun ss addsplits splits =
+fun add_split split ss =
   let
-    fun addsplit split ss =
-      let
-        val (name, asm) = split_thm_info split
-        val tac = (if asm then split_asm_tac else split_tac) [split]
-      in Simplifier.addloop (ss, (split_name name asm, tac)) end
-  in fold addsplit splits ss end;
-
-fun ss delsplits splits =
-  let
-    fun delsplit split ss =
-      let val (name, asm) = split_thm_info split
-      in Simplifier.delloop (ss, split_name name asm) end
-  in fold delsplit splits ss end;
+    val (name, asm) = split_thm_info split
+    val tac = (if asm then split_asm_tac else split_tac) [split]
+  in Simplifier.addloop (ss, (split_name name asm, tac)) end;
+
+fun del_split split ss =
+  let val (name, asm) = split_thm_info split
+  in Simplifier.delloop (ss, split_name name asm) end;
 
 
 (* attributes *)
 
 val splitN = "split";
 
-val split_add = Simplifier.attrib (op addsplits);
-val split_del = Simplifier.attrib (op delsplits);
+val split_add = Simplifier.attrib add_split;
+val split_del = Simplifier.attrib del_split;
 
 
 (* methods *)
 
 val split_modifiers =