# HG changeset patch
# User wenzelm
# Date 979602057 -3600
# Node ID 9679326489cdb7e98794bdf55b934056e8d73609
# Parent  1044648b3f84d97cca4bbae01ad07323112f14a2
renamed Product_Type.split to split_conv;

diff -r 1044648b3f84 -r 9679326489cd TFL/rules.ML
--- a/TFL/rules.ML	Tue Jan 16 00:38:59 2001 +0100
+++ b/TFL/rules.ML	Tue Jan 16 00:40:57 2001 +0100
@@ -665,7 +665,7 @@
 
 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
  let val globals = func::G
-     val pbeta_reduce = simpl_conv empty_ss [split RS eq_reflection];
+     val pbeta_reduce = simpl_conv empty_ss [split_conv RS eq_reflection];
      val tc_list = ref[]: term list ref
      val dummy = term_ref := []
      val dummy = thm_ref  := []
diff -r 1044648b3f84 -r 9679326489cd src/HOL/BCV/JType.ML
--- a/src/HOL/BCV/JType.ML	Tue Jan 16 00:38:59 2001 +0100
+++ b/src/HOL/BCV/JType.ML	Tue Jan 16 00:40:57 2001 +0100
@@ -112,7 +112,7 @@
 
 AddIffs [OK_le_conv];
 
-Goalw [semilat_def,split RS eq_reflection,JType.esl_def,Err.sl_def]
+Goalw [semilat_def, split_conv RS eq_reflection,JType.esl_def,Err.sl_def]
  "[| single_valued S; acyclic S |] ==> err_semilat (JType.esl S)";
 by (asm_full_simp_tac (simpset() addsimps [acyclic_impl_order_subtype,closed_err_types]) 1);
 
diff -r 1044648b3f84 -r 9679326489cd src/HOL/BCV/Listn.ML
--- a/src/HOL/BCV/Listn.ML	Tue Jan 16 00:38:59 2001 +0100
+++ b/src/HOL/BCV/Listn.ML	Tue Jan 16 00:40:57 2001 +0100
@@ -269,7 +269,7 @@
 Goalw [Listn.sl_def]
  "!!L. semilat L ==> semilat (Listn.sl n L)";
 by (split_all_tac 1);
-by (simp_tac (HOL_basic_ss addsimps [semilat_Def,split]) 1);
+by (simp_tac (HOL_basic_ss addsimps [semilat_Def, split_conv]) 1);
 by (rtac conjI 1);
  by (Asm_simp_tac 1);
 by (rtac conjI 1);
@@ -400,7 +400,7 @@
 Goalw [Err.sl_def]
  "err_semilat (A,r,f) ==> \
 \ err_semilat (list n A, Listn.le r, sup f)";
-by (asm_full_simp_tac (HOL_basic_ss addsimps [split]) 1);
+by (asm_full_simp_tac (HOL_basic_ss addsimps [split_conv]) 1);
 by (simp_tac (HOL_basic_ss addsimps [semilat_Def,plussub_def]) 1);
 by (asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_lift2_sup]) 1);
 by (rtac conjI 1);
diff -r 1044648b3f84 -r 9679326489cd src/HOL/BCV/Opt.ML
--- a/src/HOL/BCV/Opt.ML	Tue Jan 16 00:38:59 2001 +0100
+++ b/src/HOL/BCV/Opt.ML	Tue Jan 16 00:40:57 2001 +0100
@@ -50,7 +50,7 @@
 AddIffs [le_None];
 
 
-Goalw [Opt.sl_def,semilat_def,closed_def,split RS eq_reflection]
+Goalw [Opt.sl_def,semilat_def,closed_def, split_conv RS eq_reflection]
  "!!L. semilat L ==> semilat (Opt.sl L)";
 by (split_all_tac 1);
 by (asm_full_simp_tac (simpset() addsplits [option.split]
diff -r 1044648b3f84 -r 9679326489cd src/HOL/BCV/Semilat.ML
--- a/src/HOL/BCV/Semilat.ML	Tue Jan 16 00:38:59 2001 +0100
+++ b/src/HOL/BCV/Semilat.ML	Tue Jan 16 00:40:57 2001 +0100
@@ -39,7 +39,7 @@
 qed "top_le_conv";
 Addsimps [top_le_conv];
 
-Goalw [semilat_def,split RS eq_reflection]
+Goalw [semilat_def, split_conv RS eq_reflection]
 "semilat(A,r,f) == order r & closed A f & \
 \                (!x:A. !y:A. x <=_r x +_f y)  & \
 \                (!x:A. !y:A. y <=_r x +_f y)  & \
diff -r 1044648b3f84 -r 9679326489cd src/HOL/Hoare/Hoare.ML
--- a/src/HOL/Hoare/Hoare.ML	Tue Jan 16 00:38:59 2001 +0100
+++ b/src/HOL/Hoare/Hoare.ML	Tue Jan 16 00:40:57 2001 +0100
@@ -147,7 +147,7 @@
 val before_set2pred_simp_tac =
   (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym,Compl_Collect]));
 
-val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split]));
+val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
 
 (*****************************************************************************)
 (** set2pred transforms sets inclusion into predicates implication,         **)
@@ -171,7 +171,7 @@
                   dtac CollectD i,
                   (TRY(split_all_tac i)) THEN_MAYBE
                   ((rename_tac var_string i) THEN
-                   (full_simp_tac (HOL_basic_ss addsimps [split]) i)) ])) thm
+                   (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
       end;
 
 (*****************************************************************************)
@@ -186,7 +186,7 @@
 
 fun BasicSimpTac tac =
   simp_tac
-    (HOL_basic_ss addsimps [mem_Collect_eq,split] addsimprocs [record_simproc])
+    (HOL_basic_ss addsimps [mem_Collect_eq,split_conv] addsimprocs [record_simproc])
   THEN_MAYBE' MaxSimpTac tac;
 
 (** HoareRuleTac **)
diff -r 1044648b3f84 -r 9679326489cd src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Tue Jan 16 00:38:59 2001 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy	Tue Jan 16 00:40:57 2001 +0100
@@ -340,7 +340,7 @@
   "!!L. semilat L ==> semilat (Listn.sl n L)"
 apply (unfold Listn.sl_def)
 apply (simp (no_asm_simp) only: split_tupled_all)
-apply (simp (no_asm) only: semilat_Def Product_Type.split)
+apply (simp (no_asm) only: semilat_Def split_conv)
 apply (rule conjI)
  apply simp
 apply (rule conjI)
@@ -471,7 +471,7 @@
   "err_semilat (A,r,f) ==> 
   err_semilat (list n A, Listn.le r, sup f)"
 apply (unfold Err.sl_def)
-apply (simp only: Product_Type.split)
+apply (simp only: split_conv)
 apply (simp (no_asm) only: semilat_Def plussub_def)
 apply (simp (no_asm_simp) only: semilatDclosedI closed_lift2_sup)
 apply (rule conjI)
diff -r 1044648b3f84 -r 9679326489cd src/HOL/MicroJava/BV/Semilat.thy
--- a/src/HOL/MicroJava/BV/Semilat.thy	Tue Jan 16 00:38:59 2001 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Tue Jan 16 00:40:57 2001 +0100
@@ -102,7 +102,7 @@
                  (!x:A. !y:A. x <=_r x +_f y) & 
                  (!x:A. !y:A. y <=_r x +_f y) & 
                  (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
-apply (unfold semilat_def Product_Type.split [THEN eq_reflection])
+apply (unfold semilat_def split_conv [THEN eq_reflection])
 apply (rule refl [THEN eq_reflection])
 done
 
diff -r 1044648b3f84 -r 9679326489cd src/HOL/Product_Type.ML
--- a/src/HOL/Product_Type.ML	Tue Jan 16 00:38:59 2001 +0100
+++ b/src/HOL/Product_Type.ML	Tue Jan 16 00:40:57 2001 +0100
@@ -167,8 +167,9 @@
 
 Goalw [split_def] "split c (a,b) = c a b";
 by (Simp_tac 1);
-qed "split";
-Addsimps [split];
+qed "split_conv";
+Addsimps [split_conv];
+(*bind_thm ("split", split_conv);                  (*for compatibility*)*)
 
 (*Subsumes the old split_Pair when f is the identity function*)
 Goal "split (%x y. f(x,y)) = f";
@@ -200,7 +201,7 @@
 Goal "(%(x,y). f(x,y)) = f";
 by (rtac ext 1);
 by (split_all_tac 1);
-by (rtac split 1);
+by (rtac split_conv 1);
 qed "split_eta";
 
 val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g";
@@ -260,13 +261,13 @@
 Addsimprocs [split_beta_proc,split_eta_proc];
 
 Goal "(%(x,y). P x y) z = P (fst z) (snd z)";
-by (stac surjective_pairing 1 THEN rtac split 1);
+by (stac surjective_pairing 1 THEN rtac split_conv 1);
 qed "split_beta";
 
 (*For use with split_tac and the simplifier*)
 Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
 by (stac surjective_pairing 1);
-by (stac split 1);
+by (stac split_conv 1);
 by (Blast_tac 1);
 qed "split_split";
 
@@ -318,7 +319,7 @@
 qed "splitE2";
 
 Goal "split R (a,b) ==> R a b";
-by (etac (split RS iffD1) 1);
+by (etac (split_conv RS iffD1) 1);
 qed "splitD";
 
 Goal "z: c a b ==> z: split c (a,b)";
@@ -377,7 +378,7 @@
 (*** prod_fun -- action of the product functor upon functions ***)
 
 Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
-by (rtac split 1);
+by (rtac split_conv 1);
 qed "prod_fun";
 Addsimps [prod_fun];
 
@@ -569,7 +570,7 @@
 
 
 (*Attempts to remove occurrences of split, and pair-valued parameters*)
-val remove_split = rewrite_rule [split RS eq_reflection] o split_all;
+val remove_split = rewrite_rule [split_conv RS eq_reflection] o split_all;
 
 local
 
diff -r 1044648b3f84 -r 9679326489cd src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Tue Jan 16 00:38:59 2001 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML	Tue Jan 16 00:40:57 2001 +0100
@@ -360,7 +360,7 @@
 \     (UN s:A. UN f. {insert_map i s f}) <*> UNIV";
 by (auto_tac (claset() addSIs [bexI, image_eqI],
               simpset() addsimps [lift_map_def]));
-by (rtac (split RS sym) 1);
+by (rtac (split_conv RS sym) 1);
 qed "lift_map_image_Times";
 
 Goal "(lift i F : preserves v) = (F : preserves (v o lift_map i))";