# HG changeset patch
# User oheimb
# Date 949068495 -3600
# Node ID bde1391fd0a5b4507fcfdfaa1cd70e201b07fc18
# Parent  837a6b515005ec85de08ea9d1078a2dd50534318
added range_composition (also to simpset)

diff -r 837a6b515005 -r bde1391fd0a5 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Jan 28 14:49:00 2000 +0100
+++ b/src/HOL/equalities.ML	Fri Jan 28 15:08:15 2000 +0100
@@ -164,6 +164,11 @@
 by Auto_tac;
 qed "full_SetCompr_eq";
 
+Goal "range (%x. f (g x)) = f``range g";
+by (stac image_image 1);
+by (Simp_tac 1);
+qed "range_composition";
+Addsimps[range_composition];
 
 section "Int";
 
diff -r 837a6b515005 -r bde1391fd0a5 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Fri Jan 28 14:49:00 2000 +0100
+++ b/src/HOLCF/Fix.ML	Fri Jan 28 15:08:15 2000 +0100
@@ -130,7 +130,7 @@
         (induct_tac "i" 1),
         (Asm_simp_tac 1),
         (rtac (lub_const RS thelubI RS sym) 1),
-        (Asm_simp_tac 1),
+        (asm_simp_tac (simpset() delsimps [range_composition]) 1),
         (rtac ext 1),
         (stac thelub_fun 1),
         (rtac chainI 1),
diff -r 837a6b515005 -r bde1391fd0a5 src/HOLCF/Ssum0.ML
--- a/src/HOLCF/Ssum0.ML	Fri Jan 28 14:49:00 2000 +0100
+++ b/src/HOLCF/Ssum0.ML	Fri Jan 28 15:08:15 2000 +0100
@@ -388,6 +388,6 @@
 (* instantiate the simplifier                                               *)
 (* ------------------------------------------------------------------------ *)
 
-val Ssum0_ss = (simpset_of Cfun3.thy) addsimps 
+val Ssum0_ss = (simpset_of Cfun3.thy) delsimps [range_composition] addsimps 
                 [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
 
diff -r 837a6b515005 -r bde1391fd0a5 src/HOLCF/Ssum3.ML
--- a/src/HOLCF/Ssum3.ML	Fri Jan 28 14:49:00 2000 +0100
+++ b/src/HOLCF/Ssum3.ML	Fri Jan 28 15:08:15 2000 +0100
@@ -192,22 +192,19 @@
         (etac is_ub_thelub 1)
         ]);
 
-qed_goal "ssum_lemma11" Ssum3.thy 
+Goal  
 "[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
-\   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (asm_simp_tac Ssum0_ss 1),
-        (rtac (chain_UU_I_inverse RS sym) 1),
-        (rtac allI 1),
-        (res_inst_tac [("s","Isinl(UU)"),("t","Y(i)")] subst 1),
-        (rtac (inst_ssum_pcpo RS subst) 1),
-        (rtac (chain_UU_I RS spec RS sym) 1),
-        (atac 1),
-        (etac (inst_ssum_pcpo RS ssubst) 1),
-        (asm_simp_tac Ssum0_ss 1)
-        ]);
+\   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))";
+by (asm_simp_tac Ssum0_ss 1);
+by (rtac (chain_UU_I_inverse RS sym) 1);
+by (rtac allI 1);
+by (res_inst_tac [("s","Isinl(UU)"),("t","Y(i)")] subst 1);
+by (rtac (inst_ssum_pcpo RS subst) 1);
+by (rtac (chain_UU_I RS spec RS sym) 1);
+by (atac 1);
+by (etac (inst_ssum_pcpo RS ssubst) 1);
+by (asm_simp_tac Ssum0_ss 1);
+qed "ssum_lemma11";
 
 qed_goal "ssum_lemma12" Ssum3.thy 
 "[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
diff -r 837a6b515005 -r bde1391fd0a5 src/HOLCF/Up1.ML
--- a/src/HOLCF/Up1.ML	Fri Jan 28 14:49:00 2000 +0100
+++ b/src/HOLCF/Up1.ML	Fri Jan 28 15:08:15 2000 +0100
@@ -90,7 +90,8 @@
         (rtac refl 1)
         ]);
 
-val Up0_ss = (simpset_of Cfun3.thy) addsimps [Ifup1,Ifup2];
+val Up0_ss = (simpset_of Cfun3.thy) delsimps [range_composition] 
+	     addsimps [Ifup1,Ifup2];
 
 qed_goalw "less_up1a"  thy [less_up_def]
         "Abs_Up(Inl ())<< z"
diff -r 837a6b515005 -r bde1391fd0a5 src/HOLCF/Up3.ML
--- a/src/HOLCF/Up3.ML	Fri Jan 28 14:49:00 2000 +0100
+++ b/src/HOLCF/Up3.ML	Fri Jan 28 15:08:15 2000 +0100
@@ -84,52 +84,50 @@
         ]);
 
 
-qed_goal "contlub_Ifup2" thy "contlub(Ifup(f))"
- (fn prems =>
-        [
-        (rtac contlubI 1),
-        (strip_tac 1),
-        (rtac disjE 1),
-        (stac thelub_up1a 2),
-        (atac 2),
-        (atac 2),
-        (asm_simp_tac Up0_ss 2),
-        (stac thelub_up1b 3),
-        (atac 3),
-        (atac 3),
-        (fast_tac HOL_cs 1),
-        (asm_simp_tac Up0_ss 2),
-        (rtac (chain_UU_I_inverse RS sym) 2),
-        (rtac allI 2),
-        (res_inst_tac [("p","Y(i)")] upE 2),
-        (asm_simp_tac Up0_ss 2),
-        (rtac notE 2),
-        (dtac spec 2),
-        (etac spec 2),
-        (atac 2),
-        (stac contlub_cfun_arg 1),
-        (etac (monofun_Ifup2 RS ch2ch_monofun) 1),
-        (rtac lub_equal2 1),
-        (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 2),
-        (etac (monofun_Ifup2 RS ch2ch_monofun) 2),
-        (etac (monofun_Ifup2 RS ch2ch_monofun) 2),
-        (rtac (chain_mono2 RS exE) 1),
-        (atac 2),
-        (etac exE 1),
-        (etac exE 1),
-        (rtac exI 1),
-        (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1),
-        (atac 1),
-        (rtac defined_Iup2 1),
-        (rtac exI 1),
-        (strip_tac 1),
-        (res_inst_tac [("p","Y(i)")] upE 1),
-        (asm_simp_tac Up0_ss 2),
-        (res_inst_tac [("P","Y(i) = UU")] notE 1),
-        (fast_tac HOL_cs 1),
-        (stac inst_up_pcpo 1),
-        (atac 1)
-        ]);
+Goal "contlub(Ifup(f))";
+by (rtac contlubI 1);
+by (strip_tac 1);
+by (rtac disjE 1);
+by   (stac thelub_up1a 2);
+by     (atac 2);
+by    (atac 2);
+by   (asm_simp_tac Up0_ss 2);
+by   (stac thelub_up1b 3);
+by     (atac 3);
+by    (atac 3);
+by   (fast_tac HOL_cs 1);
+by  (asm_simp_tac Up0_ss 2);
+by  (rtac (chain_UU_I_inverse RS sym) 2);
+by  (rtac allI 2);
+by  (res_inst_tac [("p","Y(i)")] upE 2);
+by   (asm_simp_tac Up0_ss 2);
+by  (rtac notE 2);
+by   (dtac spec 2);
+by   (etac spec 2);
+by  (atac 2);
+by (stac contlub_cfun_arg 1);
+by  (etac (monofun_Ifup2 RS ch2ch_monofun) 1);
+by (rtac lub_equal2 1);
+by   (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 2);
+by   (etac (monofun_Ifup2 RS ch2ch_monofun) 2);
+by  (etac (monofun_Ifup2 RS ch2ch_monofun) 2);
+by (rtac (chain_mono2 RS exE) 1);
+by   (atac 2);
+by  (etac exE 1);
+by  (etac exE 1);
+by  (rtac exI 1);
+by  (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1);
+by   (atac 1);
+by  (rtac defined_Iup2 1);
+by (rtac exI 1);
+by (strip_tac 1);
+by (res_inst_tac [("p","Y(i)")] upE 1);
+by  (asm_simp_tac Up0_ss 2);
+by (res_inst_tac [("P","Y(i) = UU")] notE 1);
+by  (fast_tac HOL_cs 1);
+by (stac inst_up_pcpo 1);
+by (atac 1);
+qed "contlub_Ifup2";
 
 qed_goal "cont_Ifup1" thy "cont(Ifup)"
  (fn prems =>