--- 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";
--- 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),
--- 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];
--- 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 |] ==>\
--- 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"
--- 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 =>