renamed Product_Type.split to split_conv;
authorwenzelm
Tue Jan 16 00:40:57 2001 +0100 (2001-01-16)
changeset 109189679326489cd
parent 10917 1044648b3f84
child 10919 144ede948e58
renamed Product_Type.split to split_conv;
TFL/rules.ML
src/HOL/BCV/JType.ML
src/HOL/BCV/Listn.ML
src/HOL/BCV/Opt.ML
src/HOL/BCV/Semilat.ML
src/HOL/Hoare/Hoare.ML
src/HOL/MicroJava/BV/Listn.thy
src/HOL/MicroJava/BV/Semilat.thy
src/HOL/Product_Type.ML
src/HOL/UNITY/Lift_prog.ML
     1.1 --- a/TFL/rules.ML	Tue Jan 16 00:38:59 2001 +0100
     1.2 +++ b/TFL/rules.ML	Tue Jan 16 00:40:57 2001 +0100
     1.3 @@ -665,7 +665,7 @@
     1.4  
     1.5  fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
     1.6   let val globals = func::G
     1.7 -     val pbeta_reduce = simpl_conv empty_ss [split RS eq_reflection];
     1.8 +     val pbeta_reduce = simpl_conv empty_ss [split_conv RS eq_reflection];
     1.9       val tc_list = ref[]: term list ref
    1.10       val dummy = term_ref := []
    1.11       val dummy = thm_ref  := []
     2.1 --- a/src/HOL/BCV/JType.ML	Tue Jan 16 00:38:59 2001 +0100
     2.2 +++ b/src/HOL/BCV/JType.ML	Tue Jan 16 00:40:57 2001 +0100
     2.3 @@ -112,7 +112,7 @@
     2.4  
     2.5  AddIffs [OK_le_conv];
     2.6  
     2.7 -Goalw [semilat_def,split RS eq_reflection,JType.esl_def,Err.sl_def]
     2.8 +Goalw [semilat_def, split_conv RS eq_reflection,JType.esl_def,Err.sl_def]
     2.9   "[| single_valued S; acyclic S |] ==> err_semilat (JType.esl S)";
    2.10  by (asm_full_simp_tac (simpset() addsimps [acyclic_impl_order_subtype,closed_err_types]) 1);
    2.11  
     3.1 --- a/src/HOL/BCV/Listn.ML	Tue Jan 16 00:38:59 2001 +0100
     3.2 +++ b/src/HOL/BCV/Listn.ML	Tue Jan 16 00:40:57 2001 +0100
     3.3 @@ -269,7 +269,7 @@
     3.4  Goalw [Listn.sl_def]
     3.5   "!!L. semilat L ==> semilat (Listn.sl n L)";
     3.6  by (split_all_tac 1);
     3.7 -by (simp_tac (HOL_basic_ss addsimps [semilat_Def,split]) 1);
     3.8 +by (simp_tac (HOL_basic_ss addsimps [semilat_Def, split_conv]) 1);
     3.9  by (rtac conjI 1);
    3.10   by (Asm_simp_tac 1);
    3.11  by (rtac conjI 1);
    3.12 @@ -400,7 +400,7 @@
    3.13  Goalw [Err.sl_def]
    3.14   "err_semilat (A,r,f) ==> \
    3.15  \ err_semilat (list n A, Listn.le r, sup f)";
    3.16 -by (asm_full_simp_tac (HOL_basic_ss addsimps [split]) 1);
    3.17 +by (asm_full_simp_tac (HOL_basic_ss addsimps [split_conv]) 1);
    3.18  by (simp_tac (HOL_basic_ss addsimps [semilat_Def,plussub_def]) 1);
    3.19  by (asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_lift2_sup]) 1);
    3.20  by (rtac conjI 1);
     4.1 --- a/src/HOL/BCV/Opt.ML	Tue Jan 16 00:38:59 2001 +0100
     4.2 +++ b/src/HOL/BCV/Opt.ML	Tue Jan 16 00:40:57 2001 +0100
     4.3 @@ -50,7 +50,7 @@
     4.4  AddIffs [le_None];
     4.5  
     4.6  
     4.7 -Goalw [Opt.sl_def,semilat_def,closed_def,split RS eq_reflection]
     4.8 +Goalw [Opt.sl_def,semilat_def,closed_def, split_conv RS eq_reflection]
     4.9   "!!L. semilat L ==> semilat (Opt.sl L)";
    4.10  by (split_all_tac 1);
    4.11  by (asm_full_simp_tac (simpset() addsplits [option.split]
     5.1 --- a/src/HOL/BCV/Semilat.ML	Tue Jan 16 00:38:59 2001 +0100
     5.2 +++ b/src/HOL/BCV/Semilat.ML	Tue Jan 16 00:40:57 2001 +0100
     5.3 @@ -39,7 +39,7 @@
     5.4  qed "top_le_conv";
     5.5  Addsimps [top_le_conv];
     5.6  
     5.7 -Goalw [semilat_def,split RS eq_reflection]
     5.8 +Goalw [semilat_def, split_conv RS eq_reflection]
     5.9  "semilat(A,r,f) == order r & closed A f & \
    5.10  \                (!x:A. !y:A. x <=_r x +_f y)  & \
    5.11  \                (!x:A. !y:A. y <=_r x +_f y)  & \
     6.1 --- a/src/HOL/Hoare/Hoare.ML	Tue Jan 16 00:38:59 2001 +0100
     6.2 +++ b/src/HOL/Hoare/Hoare.ML	Tue Jan 16 00:40:57 2001 +0100
     6.3 @@ -147,7 +147,7 @@
     6.4  val before_set2pred_simp_tac =
     6.5    (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym,Compl_Collect]));
     6.6  
     6.7 -val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split]));
     6.8 +val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
     6.9  
    6.10  (*****************************************************************************)
    6.11  (** set2pred transforms sets inclusion into predicates implication,         **)
    6.12 @@ -171,7 +171,7 @@
    6.13                    dtac CollectD i,
    6.14                    (TRY(split_all_tac i)) THEN_MAYBE
    6.15                    ((rename_tac var_string i) THEN
    6.16 -                   (full_simp_tac (HOL_basic_ss addsimps [split]) i)) ])) thm
    6.17 +                   (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
    6.18        end;
    6.19  
    6.20  (*****************************************************************************)
    6.21 @@ -186,7 +186,7 @@
    6.22  
    6.23  fun BasicSimpTac tac =
    6.24    simp_tac
    6.25 -    (HOL_basic_ss addsimps [mem_Collect_eq,split] addsimprocs [record_simproc])
    6.26 +    (HOL_basic_ss addsimps [mem_Collect_eq,split_conv] addsimprocs [record_simproc])
    6.27    THEN_MAYBE' MaxSimpTac tac;
    6.28  
    6.29  (** HoareRuleTac **)
     7.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Tue Jan 16 00:38:59 2001 +0100
     7.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Tue Jan 16 00:40:57 2001 +0100
     7.3 @@ -340,7 +340,7 @@
     7.4    "!!L. semilat L ==> semilat (Listn.sl n L)"
     7.5  apply (unfold Listn.sl_def)
     7.6  apply (simp (no_asm_simp) only: split_tupled_all)
     7.7 -apply (simp (no_asm) only: semilat_Def Product_Type.split)
     7.8 +apply (simp (no_asm) only: semilat_Def split_conv)
     7.9  apply (rule conjI)
    7.10   apply simp
    7.11  apply (rule conjI)
    7.12 @@ -471,7 +471,7 @@
    7.13    "err_semilat (A,r,f) ==> 
    7.14    err_semilat (list n A, Listn.le r, sup f)"
    7.15  apply (unfold Err.sl_def)
    7.16 -apply (simp only: Product_Type.split)
    7.17 +apply (simp only: split_conv)
    7.18  apply (simp (no_asm) only: semilat_Def plussub_def)
    7.19  apply (simp (no_asm_simp) only: semilatDclosedI closed_lift2_sup)
    7.20  apply (rule conjI)
     8.1 --- a/src/HOL/MicroJava/BV/Semilat.thy	Tue Jan 16 00:38:59 2001 +0100
     8.2 +++ b/src/HOL/MicroJava/BV/Semilat.thy	Tue Jan 16 00:40:57 2001 +0100
     8.3 @@ -102,7 +102,7 @@
     8.4                   (!x:A. !y:A. x <=_r x +_f y) & 
     8.5                   (!x:A. !y:A. y <=_r x +_f y) & 
     8.6                   (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
     8.7 -apply (unfold semilat_def Product_Type.split [THEN eq_reflection])
     8.8 +apply (unfold semilat_def split_conv [THEN eq_reflection])
     8.9  apply (rule refl [THEN eq_reflection])
    8.10  done
    8.11  
     9.1 --- a/src/HOL/Product_Type.ML	Tue Jan 16 00:38:59 2001 +0100
     9.2 +++ b/src/HOL/Product_Type.ML	Tue Jan 16 00:40:57 2001 +0100
     9.3 @@ -167,8 +167,9 @@
     9.4  
     9.5  Goalw [split_def] "split c (a,b) = c a b";
     9.6  by (Simp_tac 1);
     9.7 -qed "split";
     9.8 -Addsimps [split];
     9.9 +qed "split_conv";
    9.10 +Addsimps [split_conv];
    9.11 +(*bind_thm ("split", split_conv);                  (*for compatibility*)*)
    9.12  
    9.13  (*Subsumes the old split_Pair when f is the identity function*)
    9.14  Goal "split (%x y. f(x,y)) = f";
    9.15 @@ -200,7 +201,7 @@
    9.16  Goal "(%(x,y). f(x,y)) = f";
    9.17  by (rtac ext 1);
    9.18  by (split_all_tac 1);
    9.19 -by (rtac split 1);
    9.20 +by (rtac split_conv 1);
    9.21  qed "split_eta";
    9.22  
    9.23  val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g";
    9.24 @@ -260,13 +261,13 @@
    9.25  Addsimprocs [split_beta_proc,split_eta_proc];
    9.26  
    9.27  Goal "(%(x,y). P x y) z = P (fst z) (snd z)";
    9.28 -by (stac surjective_pairing 1 THEN rtac split 1);
    9.29 +by (stac surjective_pairing 1 THEN rtac split_conv 1);
    9.30  qed "split_beta";
    9.31  
    9.32  (*For use with split_tac and the simplifier*)
    9.33  Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
    9.34  by (stac surjective_pairing 1);
    9.35 -by (stac split 1);
    9.36 +by (stac split_conv 1);
    9.37  by (Blast_tac 1);
    9.38  qed "split_split";
    9.39  
    9.40 @@ -318,7 +319,7 @@
    9.41  qed "splitE2";
    9.42  
    9.43  Goal "split R (a,b) ==> R a b";
    9.44 -by (etac (split RS iffD1) 1);
    9.45 +by (etac (split_conv RS iffD1) 1);
    9.46  qed "splitD";
    9.47  
    9.48  Goal "z: c a b ==> z: split c (a,b)";
    9.49 @@ -377,7 +378,7 @@
    9.50  (*** prod_fun -- action of the product functor upon functions ***)
    9.51  
    9.52  Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
    9.53 -by (rtac split 1);
    9.54 +by (rtac split_conv 1);
    9.55  qed "prod_fun";
    9.56  Addsimps [prod_fun];
    9.57  
    9.58 @@ -569,7 +570,7 @@
    9.59  
    9.60  
    9.61  (*Attempts to remove occurrences of split, and pair-valued parameters*)
    9.62 -val remove_split = rewrite_rule [split RS eq_reflection] o split_all;
    9.63 +val remove_split = rewrite_rule [split_conv RS eq_reflection] o split_all;
    9.64  
    9.65  local
    9.66  
    10.1 --- a/src/HOL/UNITY/Lift_prog.ML	Tue Jan 16 00:38:59 2001 +0100
    10.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Tue Jan 16 00:40:57 2001 +0100
    10.3 @@ -360,7 +360,7 @@
    10.4  \     (UN s:A. UN f. {insert_map i s f}) <*> UNIV";
    10.5  by (auto_tac (claset() addSIs [bexI, image_eqI],
    10.6                simpset() addsimps [lift_map_def]));
    10.7 -by (rtac (split RS sym) 1);
    10.8 +by (rtac (split_conv RS sym) 1);
    10.9  qed "lift_map_image_Times";
   10.10  
   10.11  Goal "(lift i F : preserves v) = (F : preserves (v o lift_map i))";