--- 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 := []
--- 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);
--- 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);
--- 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]
--- 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) & \
--- 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 **)
--- 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)
--- 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
--- 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
--- 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))";