# HG changeset patch
# User oheimb
# Date 895157409 -7200
# Node ID 89271bc4e7ed3a59b8d086fc7c2b16cc33ccbead
# Parent  bc3ec5af8593eff35449e27a7adcd5ee34e2ff20
extended addsplits and delsplits to handle also split rules for assumptions
extended const_of_split_thm, renamed it to split_thm_info

diff -r bc3ec5af8593 -r 89271bc4e7ed NEWS
--- a/NEWS	Thu May 14 16:44:04 1998 +0200
+++ b/NEWS	Thu May 14 16:50:09 1998 +0200
@@ -97,8 +97,8 @@
   remove it in a specific call of the simplifier using
   `... delsplits [split_if]'.
   You can also add/delete other case splitting rules to/from the default
-  simpset: every datatype generates a suitable rule `split_t_case' (where t
-  is the name of the datatype).
+  simpset: every datatype generates suitable rules `split_t_case' and
+  `split_t_case_asm' (where t is the name of the datatype).
 
 * new theory Vimage (inverse image of a function, syntax f-``B);
 
@@ -267,19 +267,16 @@
        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
      )
 
-  which can be added to a simpset via `addsplits'. The existing theorems
-  expand_list_case and expand_option_case have been renamed to
-  split_list_case and split_option_case.
-
-  Additionally, there is a theorem `split_t_case_asm' of the form
+  and a theorem `split_t_case_asm' of the form
 
   P(t_case f1 ... fn x) =
     ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
         ...
        (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
      )
-
-  it be used with the new `split_asm_tac'.
+  which can be added to a simpset via `addsplits'. The existing theorems
+  expand_list_case and expand_option_case have been renamed to
+  split_list_case and split_option_case.
 
 * HOL/Arithmetic:
   - `pred n' is automatically converted to `n-1'.
diff -r bc3ec5af8593 -r 89271bc4e7ed src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu May 14 16:44:04 1998 +0200
+++ b/src/FOL/simpdata.ML	Thu May 14 16:50:09 1998 +0200
@@ -264,13 +264,20 @@
 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
 
-infix 4 addsplits;
+infix 4 addsplits delsplits;
 fun ss addsplits splits =
-  let fun addsplit(ss,split) =
-        let val name = "split " ^ const_of_split_thm split
-        in ss addloop (name,split_tac [split]) end
+  let fun addsplit (ss,split) =
+        let val (name,asm) = split_thm_info split 
+        in ss addloop (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 (name ^ (if asm then " asm" else "")) end
+  in foldl delsplit (ss,splits) end;
+
 val IFOL_simps =
    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
     imp_simps @ iff_simps @ quant_simps;
diff -r bc3ec5af8593 -r 89271bc4e7ed src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu May 14 16:44:04 1998 +0200
+++ b/src/HOL/simpdata.ML	Thu May 14 16:50:09 1998 +0200
@@ -346,15 +346,16 @@
 infix 4 addsplits delsplits;
 
 fun ss addsplits splits =
-  let fun addsplit(ss,split) =
-        let val name = "split " ^ const_of_split_thm split
-        in ss addloop (name,split_tac [split]) end
+  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 = "split " ^ const_of_split_thm split
-        in ss delloop name end
+        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);
diff -r bc3ec5af8593 -r 89271bc4e7ed src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Thu May 14 16:44:04 1998 +0200
+++ b/src/Provers/splitter.ML	Thu May 14 16:50:09 1998 +0200
@@ -279,14 +279,13 @@
 
 in split_tac end;
 
-(* FIXME: this junk is only HOL specific and should therefore not go here! *)
-(* const_of_split_thm is used in HOL/simpdata.ML *)
-
-fun const_of_split_thm thm =
+(* 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)$_) =>
+     Const("Trueprop",_) $ (Const("op =", _)$(Var _$t)$c) =>
         (case strip_comb t of
-           (Const(a,_),_) => a
+           (Const(a,_),_) => (a,case c of (Const("Not",_)$_)=> true |_=> false)
          | _              => split_format_err())
    | _ => split_format_err());
 
@@ -303,7 +302,7 @@
 
 fun split_asm_tac []     = K no_tac
   | split_asm_tac splits = 
-  let val cname_list = map const_of_split_thm 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) 
@@ -335,7 +334,7 @@
 
 in
 
-val const_of_split_thm = const_of_split_thm;
+val split_thm_info = split_thm_info;
 
 fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD int_ord;