# HG changeset patch
# User oheimb
# Date 902931678 -7200
# Node ID c133f16febc72df10ac7ffd17743dba3fa6434ac
# Parent  22029546d109ea678adceab7f861b7dfe23c982b
the splitter is now defined as a functor
moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML
moved split_thm_info to Provers/splitter.ML
definined atomize via general mk_atomize
removed superfluous rot_eq_tac from simplifier.ML
HOL/simpdata.ML: renamed mk_meta_eq to meta_eq,
              re-renamed mk_meta_eq_simp to mk_meta_eq
                 added Eps_eq to simpset

diff -r 22029546d109 -r c133f16febc7 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed Aug 12 16:20:49 1998 +0200
+++ b/src/FOL/simpdata.ML	Wed Aug 12 16:21:18 1998 +0200
@@ -60,21 +60,6 @@
 
 fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
 
-(*Make atomic rewrite rules*)
-fun atomize r =
-  case concl_of r of
-    Const("Trueprop",_) $ p =>
-      (case p of
-         Const("op -->",_)$_$_ => atomize(r RS mp)
-       | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
-                                  atomize(r RS conjunct2)
-       | Const("All",_)$_      => atomize(r RS spec)
-       | Const("True",_)       => []    (*True is DELETED*)
-       | Const("False",_)      => []    (*should False do something?*)
-       | _                     => [r])
-  | _ => [r];
-
-
 val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
 val iff_reflection_F = P_iff_F RS iff_reflection;
 
@@ -89,6 +74,28 @@
   | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
   | _                           => th RS iff_reflection_T;
 
+val mksimps_pairs =
+  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
+   ("All", [spec]), ("True", []), ("False", [])];
+
+(* FIXME: move to Provers/simplifier.ML
+val mk_atomize:      (string * thm list) list -> thm -> thm list
+*)
+(* FIXME: move to Provers/simplifier.ML*)
+fun mk_atomize pairs =
+  let fun atoms th =
+        (case concl_of th of
+           Const("Trueprop",_) $ p =>
+             (case head_of p of
+                Const(a,_) =>
+                  (case assoc(pairs,a) of
+                     Some(rls) => flat (map atoms ([th] RL rls))
+                   | None => [th])
+              | _ => [th])
+         | _ => [th])
+  in atoms end;
+
+fun mksimps pairs = (map mk_meta_eq o mk_atomize pairs o gen_all);
 
 (*** Classical laws ***)
 
@@ -230,22 +237,32 @@
 
 (*** Case splitting ***)
 
-qed_goal "meta_iffD" IFOL.thy "[| P==Q; Q |] ==> P"
-        (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
-
-local val mktac = mk_case_split_tac meta_iffD
-in
-fun split_tac splits = mktac (map mk_meta_eq splits)
-end;
+val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<->y"
+  (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]);
 
-local val mktac = mk_case_split_inside_tac meta_iffD
-in
-fun split_inside_tac splits = mktac (map mk_meta_eq splits)
-end;
+structure SplitterData =
+  struct
+  structure Simplifier = Simplifier
+  val mk_meta_eq     = mk_meta_eq
+  val meta_eq_to_iff = meta_eq_to_iff
+  val iffD           = iffD2
+  val disjE          = disjE
+  val conjE          = conjE
+  val exE            = exE
+  val contrapos      = contrapos
+  val contrapos2     = contrapos2
+  val notnotD        = notnotD
+  end;
 
-val split_asm_tac = mk_case_split_asm_tac split_tac 
-			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
+structure Splitter = SplitterFun(SplitterData);
 
+val split_tac        = Splitter.split_tac;
+val split_inside_tac = Splitter.split_inside_tac;
+val split_asm_tac    = Splitter.split_asm_tac;
+val addsplits        = Splitter.addsplits;
+val delsplits        = Splitter.delsplits;
+val Addsplits        = Splitter.Addsplits;
+val Delsplits        = Splitter.Delsplits;
 
 
 (*** Standard simpsets ***)
@@ -264,35 +281,6 @@
 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
 
-(** FIXME: this is a PATCH until similar code in Provers/splitter is
-    generalized **)
-
-fun split_format_err() = error("Wrong format for split rule");
-
-fun split_thm_info thm =
-  (case concl_of thm of
-     Const("Trueprop",_) $ (Const("op <->", _)$(Var _$t)$c) =>
-        (case strip_comb t of
-           (Const(a,_),_) => (a,case c of (Const("Not",_)$_)=> true |_=> false)
-         | _              => split_format_err())
-   | _ => split_format_err());
-
-infix 4 addsplits delsplits;
-fun ss addsplits splits =
-  let fun addsplit (ss,split) =
-        let val (name,asm) = split_thm_info split 
-        in ss addloop ("split "^ name ^ (if asm then " asm" else ""),
-		       (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 ss delloop ("split "^ name ^ (if asm then " asm" else "")) end
-  in foldl delsplit (ss,splits) end;
-
-fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
-fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
 
 val IFOL_simps =
    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
@@ -312,7 +300,9 @@
                             addsimprocs [defALL_regroup,defEX_regroup]
 			    setSSolver   safe_solver
 			    setSolver  unsafe_solver
-			    setmksimps (map mk_meta_eq o atomize o gen_all);
+			    setmksimps (mksimps mksimps_pairs);
+
+
 
 (*intuitionistic simprules only*)
 val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps)
@@ -336,20 +326,6 @@
 
 (*** integration of simplifier with classical reasoner ***)
 
-(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
-   fails if there is no equaliy or if an equality is already at the front *)
-local
-  fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
-    | is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
-    | is_eq _ = false;
-  val find_eq = find_index is_eq;
-in
-val rot_eq_tac = 
-     SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
-		if n>0 then rotate_tac n i else no_tac end)
-end;
-
-
 structure Clasimp = ClasimpFun
  (structure Simplifier = Simplifier and Classical = Cla and Blast = Blast
   val op addcongs = op addcongs and op delcongs = op delcongs
diff -r 22029546d109 -r c133f16febc7 src/FOLP/simpdata.ML
--- a/src/FOLP/simpdata.ML	Wed Aug 12 16:20:49 1998 +0200
+++ b/src/FOLP/simpdata.ML	Wed Aug 12 16:21:18 1998 +0200
@@ -73,16 +73,25 @@
     | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F 
     | _ => make_iff_T th;
 
-fun atomize th = case concl_of th of (*The operator below is "Proof $ P $ p"*)
-      _ $ (Const("op -->",_) $ _ $ _) $ _ => atomize(th RS mp)
-    | _ $ (Const("op &",_) $ _ $ _) $ _ => atomize(th RS conjunct1) @
-                                       atomize(th RS conjunct2)
-    | _ $ (Const("All",_) $ _) $ _ => atomize(th RS spec)
-    | _ $ (Const("True",_)) $ _ => []
-    | _ $ (Const("False",_)) $ _ => []
-    | _ => [th];
+
+val mksimps_pairs =
+  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
+   ("All", [spec]), ("True", []), ("False", [])];
 
-fun mk_rew_rules th = map mk_eq (atomize th);
+fun mk_atomize pairs =
+  let fun atoms th =
+        (case concl_of th of
+           Const("Trueprop",_) $ p =>
+             (case head_of p of
+                Const(a,_) =>
+                  (case assoc(pairs,a) of
+                     Some(rls) => flat (map atoms ([th] RL rls))
+                   | None => [th])
+              | _ => [th])
+         | _ => [th])
+  in atoms end;
+
+fun mk_rew_rules th = map mk_eq (mk_atomize mksimps_pairs th);
 
 (*destruct function for analysing equations*)
 fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs)
diff -r 22029546d109 -r c133f16febc7 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Aug 12 16:20:49 1998 +0200
+++ b/src/HOL/simpdata.ML	Wed Aug 12 16:21:18 1998 +0200
@@ -3,7 +3,7 @@
     Author:     Tobias Nipkow
     Copyright   1991  University of Cambridge
 
-Instantiation of the generic simplifier.
+Instantiation of the generic simplifier for HOL.
 *)
 
 section "Simplifier";
@@ -56,6 +56,7 @@
 fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms);
 end;
 
+
 qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
   (fn [prem] => [rewtac prem, rtac refl 1]);
 
@@ -69,32 +70,19 @@
   val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp;
   val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection;
 
-  fun atomize pairs =
-    let fun atoms th =
-          (case concl_of th of
-             Const("Trueprop",_) $ p =>
-               (case head_of p of
-                  Const(a,_) =>
-                    (case assoc(pairs,a) of
-                       Some(rls) => flat (map atoms ([th] RL rls))
-                     | None => [th])
-                | _ => [th])
-           | _ => [th])
-    in atoms end;
-
-  fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
-
 in
 
-  fun mk_meta_eq r = r RS eq_reflection;
+  fun meta_eq r = r RS eq_reflection;
+
+  fun mk_meta_eq th = case concl_of th of
+          Const("==",_)$_$_       => th
+      |   _$(Const("op =",_)$_$_) => meta_eq th
+      |   _$(Const("Not",_)$_)    => th RS not_P_imp_P_eq_False
+      |   _                       => th RS P_imp_P_eq_True;
+  (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
+
   fun mk_meta_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
 
-  fun mk_meta_eq_simp r = case concl_of r of
-          Const("==",_)$_$_ => r
-      |   _$(Const("op =",_)$lhs$rhs) => mk_meta_eq r
-      |   _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
-      |   _ => r RS P_imp_P_eq_True;
-  (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
 
 val simp_thms = map prover
  [ "(x=x) = True",
@@ -122,7 +110,7 @@
 infix 4 addcongs delcongs;
 
 fun mk_meta_cong rl =
-  standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
+  standard(meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
   handle THM _ =>
   error("Premises and conclusion of congruence rules must be =-equalities");
 
@@ -133,8 +121,6 @@
 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
 
-fun mksimps pairs = map mk_meta_eq_simp o atomize pairs o gen_all;
-
 val imp_cong = impI RSN
     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
         (fn _=> [Blast_tac 1]) RS mp RS mp);
@@ -249,9 +235,6 @@
 
 prove "eq_sym_conv" "(x=y) = (y=x)";
 
-qed_goalw "o_apply" HOL.thy [o_def] "(f o g) x = f (g x)"
- (K [rtac refl 1]);
-
 
 (** if-then-else rules **)
 
@@ -261,12 +244,9 @@
 qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y"
  (K [Blast_tac 1]);
 
-qed_goal "if_P" HOL.thy "P ==> (if P then x else y) = x"
- (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
-(*
-qed_goal "if_not_P" HOL.thy "~P ==> (if P then x else y) = y"
- (fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]);
-*)
+qed_goalw "if_P" HOL.thy [if_def] "!!P. P ==> (if P then x else y) = x"
+ (K [Blast_tac 1]);
+
 qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
  (K [Blast_tac 1]);
 
@@ -284,6 +264,12 @@
     (K [stac split_if 1,
 	Blast_tac 1]);
 
+qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
+  (K [stac split_if 1, Blast_tac 1]);
+
+qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
+  (K [stac split_if 1, Blast_tac 1]);
+
 (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
 qed_goal "if_bool_eq_conj" HOL.thy
     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
@@ -339,42 +325,29 @@
 
 (*** Case splitting ***)
 
-local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2)
-in
-fun split_tac splits = mktac (map mk_meta_eq splits)
-end;
-
-local val mktac = mk_case_split_inside_tac (meta_eq_to_obj_eq RS iffD2)
-in
-fun split_inside_tac splits = mktac (map mk_meta_eq splits)
-end;
-
-val split_asm_tac = mk_case_split_asm_tac split_tac 
-			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
-
-infix 4 addsplits delsplits;
+structure SplitterData =
+  struct
+  structure Simplifier = Simplifier
+  val mk_meta_eq     = mk_meta_eq
+  val meta_eq_to_iff = meta_eq_to_obj_eq
+  val iffD           = iffD2
+  val disjE          = disjE
+  val conjE          = conjE
+  val exE            = exE
+  val contrapos      = contrapos
+  val contrapos2     = contrapos2
+  val notnotD        = notnotD
+  end;
 
-fun ss addsplits splits =
-  let fun addsplit (ss,split) =
-        let val (name,asm) = split_thm_info split 
-        in ss addloop ("split "^ name ^ (if asm then " asm" else ""),
-		       (if asm then split_asm_tac else split_tac) [split]) end
-  in foldl addsplit (ss,splits) end;
+structure Splitter = SplitterFun(SplitterData);
 
-fun ss delsplits splits =
-  let fun delsplit(ss,split) =
-        let val (name,asm) = split_thm_info split 
-        in ss delloop ("split "^ name ^ (if asm then " asm" else "")) end
-  in foldl delsplit (ss,splits) end;
-
-fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
-fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
-
-qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
-  (K [split_tac [split_if] 1, Blast_tac 1]);
-
-qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
-  (K [split_tac [split_if] 1, Blast_tac 1]);
+val split_tac        = Splitter.split_tac;
+val split_inside_tac = Splitter.split_inside_tac;
+val split_asm_tac    = Splitter.split_asm_tac;
+val addsplits        = Splitter.addsplits;
+val delsplits        = Splitter.delsplits;
+val Addsplits        = Splitter.Addsplits;
+val Delsplits        = Splitter.Delsplits;
 
 (** 'if' congruence rules: neither included by default! *)
 
@@ -402,11 +375,32 @@
   rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
   grounds that it allows simplification of R in the two cases.*)
 
+fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
+
 val mksimps_pairs =
   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    ("All", [spec]), ("True", []), ("False", []),
    ("If", [if_bool_eq_conj RS iffD1])];
 
+(* FIXME: move to Provers/simplifier.ML
+val mk_atomize:      (string * thm list) list -> thm -> thm list
+*)
+(* FIXME: move to Provers/simplifier.ML*)
+fun mk_atomize pairs =
+  let fun atoms th =
+        (case concl_of th of
+           Const("Trueprop",_) $ p =>
+             (case head_of p of
+                Const(a,_) =>
+                  (case assoc(pairs,a) of
+                     Some(rls) => flat (map atoms ([th] RL rls))
+                   | None => [th])
+              | _ => [th])
+         | _ => [th])
+  in atoms end;
+
+fun mksimps pairs = (map mk_meta_eq o mk_atomize pairs o gen_all);
+
 fun unsafe_solver prems = FIRST'[resolve_tac (reflexive_thm::TrueI::refl::prems),
 				 atac, etac FalseE];
 (*No premature instantiation of variables during simplification*)
@@ -424,9 +418,9 @@
      ([triv_forall_equality, (* prunes params *)
        True_implies_equals, (* prune asms `True' *)
        if_True, if_False, if_cancel, if_eq_cancel,
-       o_apply, imp_disjL, conj_assoc, disj_assoc,
+       imp_disjL, conj_assoc, disj_assoc,
        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
-       disj_not1, not_all, not_ex, cases_simp]
+       disj_not1, not_all, not_ex, cases_simp, Eps_eq]
      @ ex_simps @ all_simps @ simp_thms)
      addsimprocs [defALL_regroup,defEX_regroup]
      addcongs [imp_cong]
@@ -436,9 +430,6 @@
   "f(if c then x else y) = (if c then f x else f y)" 
   (K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]);
 
-qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h"
-  (K [rtac ext 1, rtac refl 1]);
-
 
 (*For expand_case_tac*)
 val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
@@ -462,19 +453,6 @@
 
 (*** integration of simplifier with classical reasoner ***)
 
-(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
-   fails if there is no equaliy or if an equality is already at the front *)
-local
-  fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
-    | is_eq _ = false;
-  val find_eq = find_index is_eq;
-in
-val rot_eq_tac = 
-     SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
-		if n>0 then rotate_tac n i else no_tac end)
-end;
-
-
 structure Clasimp = ClasimpFun
  (structure Simplifier = Simplifier and Classical = Classical and Blast = Blast
   val op addcongs = op addcongs and op delcongs = op delcongs
diff -r 22029546d109 -r c133f16febc7 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Aug 12 16:20:49 1998 +0200
+++ b/src/Provers/splitter.ML	Wed Aug 12 16:21:18 1998 +0200
@@ -4,23 +4,57 @@
     Copyright   1995  TU Munich
 
 Generic case-splitter, suitable for most logics.
-
-Use:
-
-val split_tac = mk_case_split_tac iffD;
-
-by(split_tac splits i);
-
-where splits = [P(elim(...)) == rhs, ...]
-      iffD  = [| P <-> Q; Q |] ==> P (* is called iffD2 in HOL *)
-
 *)
 
-local
+infix 4 addsplits delsplits;
+
+signature SPLITTER_DATA =
+sig
+  structure Simplifier: SIMPLIFIER
+  val mk_meta_eq    : thm -> thm
+  val meta_eq_to_iff: thm (* "x == y ==> x = y"                    *)
+  val iffD          : thm (* "[| P = Q; Q |] ==> P"                *)
+  val disjE         : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *)
+  val conjE         : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *)
+  val exE           : thm (* "[|  x. P x; !!x. P x ==> Q |] ==> Q" *)
+  val contrapos     : thm (* "[| ~ Q; P ==> Q |] ==> ~ P"          *)
+  val contrapos2    : thm (* "[| Q; ~ P ==> ~ Q |] ==> P"          *)
+  val notnotD       : thm (* "~ ~ P ==> P"                         *)
+end
+
+signature SPLITTER =
+sig
+  type simpset
+  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 Addsplits       : thm list -> unit
+  val Delsplits       : thm list -> unit
+end;
+
+functor SplitterFun(Data: SPLITTER_DATA): SPLITTER =
+struct 
+
+type simpset = Data.Simplifier.simpset;
+
+val Const ("==>", _) $ (Const ("Trueprop", _) $
+         (Const (const_not, _) $ _    )) $ _ = #prop (rep_thm(Data.notnotD));
+
+val Const ("==>", _) $ (Const ("Trueprop", _) $
+         (Const (const_or , _) $ _ $ _)) $ _ = #prop (rep_thm(Data.disjE));
 
 fun split_format_err() = error("Wrong format for split rule");
 
-fun mk_case_split_tac_2 iffD order =
+fun split_thm_info thm = case concl_of (Data.mk_meta_eq thm) of
+     Const("==", _)$(Var _$t)$c =>
+        (case strip_comb t of
+           (Const(a,_),_) => (a,case c of (Const(s,_)$_)=>s=const_not|_=> false)
+         | _              => split_format_err())
+   | _ => split_format_err();
+
+fun mk_case_split_tac order =
 let
 
 
@@ -30,9 +64,10 @@
    [| !! x. Q(x)==R(x) ; P(R) == C |] ==> P(Q)==C
 
 *************************************************************)
- 
+
+val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
 val lift =
-  let val ct = read_cterm (#sign(rep_thm iffD))
+  let val ct = read_cterm (#sign(rep_thm Data.iffD))
            ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
             \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
   in prove_goalw_cterm [] ct
@@ -253,7 +288,8 @@
 
 fun split_tac [] i = no_tac
   | split_tac splits i =
-  let fun const(thm) =
+  let val splits = map Data.mk_meta_eq splits;
+      fun const(thm) =
             (case concl_of thm of _$(t as _$lhs)$_ =>
                (case strip_comb lhs of (Const(a,_),args) =>
                   (a,(thm,fastype_of t,length args))
@@ -274,72 +310,70 @@
                                     lift_split_tac])
             end
   in COND (has_fewer_prems i) no_tac 
-          (rtac iffD i THEN lift_split_tac)
+          (rtac meta_iffD i THEN lift_split_tac)
   end;
 
 in split_tac end;
 
-(* FIXME: this junk is only FOL/HOL specific and should therefore not go here!*)
-(* split_thm_info is used in FOL/simpdata.ML and HOL/simpdata.ML *)
-fun split_thm_info thm =
-  (case concl_of thm of
-     Const("Trueprop",_) $ (Const("op =", _)$(Var _$t)$c) =>
-        (case strip_comb t of
-           (Const(a,_),_) => (a,case c of (Const("Not",_)$_)=> true |_=> false)
-         | _              => split_format_err())
-   | _ => split_format_err());
+
+val split_tac        = mk_case_split_tac              int_ord;
 
-fun mk_case_split_asm_tac split_tac 
-			  (disjE,conjE,exE,contrapos,contrapos2,notnotD) = 
-let
+val split_inside_tac = mk_case_split_tac (rev_order o int_ord);
+
 
 (*****************************************************************************
    The split-tactic for premises
    
    splits : list of split-theorems to be tried
-   i      : number of subgoal the tactic should be applied to
-*****************************************************************************)
-
+****************************************************************************)
 fun split_asm_tac []     = K no_tac
   | split_asm_tac splits = 
+
   let val cname_list = map (fst o split_thm_info) splits;
       fun is_case (a,_) = a mem cname_list;
       fun tac (t,i) = 
 	  let val n = find_index (exists_Const is_case) 
 				 (Logic.strip_assums_hyp t);
 	      fun first_prem_is_disj (Const ("==>", _) $ (Const ("Trueprop", _)
-				 $ (Const ("op |", _) $ _ $ _ )) $ _ ) = true
+				 $ (Const (s, _) $ _ $ _ )) $ _ ) = (s=const_or)
 	      |   first_prem_is_disj (Const("all",_)$Abs(_,_,t)) = 
 					first_prem_is_disj t
 	      |   first_prem_is_disj _ = false;
 	      fun flat_prems_tac i = SUBGOAL (fn (t,i) => 
-				   (if first_prem_is_disj t
-				    then EVERY[etac disjE i, rotate_tac ~1 i,
-					       rotate_tac ~1  (i+1),
-					       flat_prems_tac (i+1)]
-				    else all_tac) 
-				   THEN REPEAT (eresolve_tac [conjE,exE] i)
-				   THEN REPEAT (dresolve_tac [notnotD]   i)) i;
+			   (if first_prem_is_disj t
+			    then EVERY[etac Data.disjE i,rotate_tac ~1 i,
+				       rotate_tac ~1  (i+1),
+				       flat_prems_tac (i+1)]
+			    else all_tac) 
+			   THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i)
+			   THEN REPEAT (dresolve_tac [Data.notnotD]   i)) i;
 	  in if n<0 then no_tac else DETERM (EVERY'
-		[rotate_tac n, etac contrapos2,
+		[rotate_tac n, etac Data.contrapos2,
 		 split_tac splits, 
-		 rotate_tac ~1, etac contrapos, rotate_tac ~1, 
+		 rotate_tac ~1, etac Data.contrapos, rotate_tac ~1, 
 		 flat_prems_tac] i)
 	  end;
   in SUBGOAL tac
   end;
 
-in split_asm_tac end;
+fun split_name name asm = "split " ^ name ^ (if asm then " asm" else "");
 
-
-in
+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,
+		       (if asm then split_asm_tac else split_tac) [split])) end
+  in foldl addsplit (ss,splits) end;
 
-val split_thm_info = split_thm_info;
-
-fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD int_ord;
+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)
+  end in foldl delsplit (ss,splits) end;
 
-fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (rev_order o int_ord);
-
-val mk_case_split_asm_tac = mk_case_split_asm_tac;
+fun Addsplits splits = (Data.Simplifier.simpset_ref() := 
+			Data.Simplifier.simpset() addsplits splits);
+fun Delsplits splits = (Data.Simplifier.simpset_ref() := 
+			Data.Simplifier.simpset() delsplits splits);
 
 end;