Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Ssum3.ML
changeset 243 c22b85994e17
child 676 f304c8379e4d 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Ssum3.ML	Wed Jan 19 17:35:01 1994 +0100
@@ -0,0 +1,728 @@
+(*  Title: 	HOLCF/ssum3.ML
+    ID:         $Id$
+    Author: 	Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+Lemmas for ssum3.thy
+*)
+
+open Ssum3;
+
+(* ------------------------------------------------------------------------ *)
+(* continuity for Isinl and Isinr                                           *)
+(* ------------------------------------------------------------------------ *)
+
+
+val contlub_Isinl = prove_goal Ssum3.thy "contlub(Isinl)"
+ (fn prems =>
+	[
+	(rtac contlubI 1),
+	(strip_tac 1),
+	(rtac trans 1),
+	(rtac (thelub_ssum1a RS sym) 2),
+	(rtac allI 3),
+	(rtac exI 3),
+	(rtac refl 3),
+	(etac (monofun_Isinl RS ch2ch_monofun) 2),
+	(res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1),
+	(res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
+	(atac 1),
+	(res_inst_tac [("f","Isinl")] arg_cong  1),
+	(rtac (chain_UU_I_inverse RS sym) 1),
+	(rtac allI 1),
+	(res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1),
+	(etac (chain_UU_I RS spec ) 1),
+	(atac 1),
+	(rtac Iwhen1 1),
+	(res_inst_tac [("f","Isinl")] arg_cong  1),
+	(rtac lub_equal 1),
+	(atac 1),
+	(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
+	(etac (monofun_Isinl RS ch2ch_monofun) 1),
+	(rtac allI 1),
+	(res_inst_tac [("Q","Y(k)=UU")] classical2 1),
+	(asm_simp_tac Ssum_ss 1),
+	(asm_simp_tac Ssum_ss 1)
+	]);
+
+val contlub_Isinr = prove_goal Ssum3.thy "contlub(Isinr)"
+ (fn prems =>
+	[
+	(rtac contlubI 1),
+	(strip_tac 1),
+	(rtac trans 1),
+	(rtac (thelub_ssum1b RS sym) 2),
+	(rtac allI 3),
+	(rtac exI 3),
+	(rtac refl 3),
+	(etac (monofun_Isinr RS ch2ch_monofun) 2),
+	(res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1),
+	(res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
+	(atac 1),
+	((rtac arg_cong 1) THEN (rtac (chain_UU_I_inverse RS sym) 1)),
+	(rtac allI 1),
+	(res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1),
+	(etac (chain_UU_I RS spec ) 1),
+	(atac 1),
+	(rtac (strict_IsinlIsinr RS subst) 1),
+	(rtac Iwhen1 1),
+	((rtac arg_cong 1) THEN (rtac lub_equal 1)),
+	(atac 1),
+	(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
+	(etac (monofun_Isinr RS ch2ch_monofun) 1),
+	(rtac allI 1),
+	(res_inst_tac [("Q","Y(k)=UU")] classical2 1),
+	(asm_simp_tac Ssum_ss 1),
+	(asm_simp_tac Ssum_ss 1)
+	]);
+
+val contX_Isinl = prove_goal Ssum3.thy "contX(Isinl)"
+ (fn prems =>
+	[
+	(rtac monocontlub2contX 1),
+	(rtac monofun_Isinl 1),
+	(rtac contlub_Isinl 1)
+	]);
+
+val contX_Isinr = prove_goal Ssum3.thy "contX(Isinr)"
+ (fn prems =>
+	[
+	(rtac monocontlub2contX 1),
+	(rtac monofun_Isinr 1),
+	(rtac contlub_Isinr 1)
+	]);
+
+
+(* ------------------------------------------------------------------------ *)
+(* continuity for Iwhen in the firts two arguments                          *)
+(* ------------------------------------------------------------------------ *)
+
+val contlub_Iwhen1 = prove_goal Ssum3.thy "contlub(Iwhen)"
+ (fn prems =>
+	[
+	(rtac contlubI 1),
+	(strip_tac 1),
+	(rtac trans 1),
+	(rtac (thelub_fun RS sym) 2),
+	(etac (monofun_Iwhen1 RS ch2ch_monofun) 2),
+	(rtac (expand_fun_eq RS iffD2) 1),
+	(strip_tac 1),
+	(rtac trans 1),
+	(rtac (thelub_fun RS sym) 2),
+	(rtac ch2ch_fun 2),
+	(etac (monofun_Iwhen1 RS ch2ch_monofun) 2),
+	(rtac (expand_fun_eq RS iffD2) 1),
+	(strip_tac 1),
+	(res_inst_tac [("p","xa")] IssumE 1),
+	(asm_simp_tac Ssum_ss 1),
+	(rtac (lub_const RS thelubI RS sym) 1),
+	(asm_simp_tac Ssum_ss 1),
+	(etac contlub_cfun_fun 1),
+	(asm_simp_tac Ssum_ss 1),
+	(rtac (lub_const RS thelubI RS sym) 1)
+	]);
+
+val contlub_Iwhen2 = prove_goal Ssum3.thy "contlub(Iwhen(f))"
+ (fn prems =>
+	[
+	(rtac contlubI 1),
+	(strip_tac 1),
+	(rtac trans 1),
+	(rtac (thelub_fun RS sym) 2),
+	(etac (monofun_Iwhen2 RS ch2ch_monofun) 2),
+	(rtac (expand_fun_eq RS iffD2) 1),
+	(strip_tac 1),
+	(res_inst_tac [("p","x")] IssumE 1),
+	(asm_simp_tac Ssum_ss 1),
+	(rtac (lub_const RS thelubI RS sym) 1),
+	(asm_simp_tac Ssum_ss 1),
+	(rtac (lub_const RS thelubI RS sym) 1),
+	(asm_simp_tac Ssum_ss 1),
+	(etac contlub_cfun_fun 1)
+	]);
+
+(* ------------------------------------------------------------------------ *)
+(* continuity for Iwhen in its third argument                               *)
+(* ------------------------------------------------------------------------ *)
+
+(* ------------------------------------------------------------------------ *)
+(* first 5 ugly lemmas                                                      *)
+(* ------------------------------------------------------------------------ *)
+
+val ssum_lemma9 = prove_goal Ssum3.thy 
+"[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x.Y(i)=Isinl(x)"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(strip_tac 1),
+	(res_inst_tac [("p","Y(i)")] IssumE 1),
+	(etac exI 1),
+	(etac exI 1),
+	(res_inst_tac [("P","y=UU")] notE 1),
+	(atac 1),
+	(rtac (less_ssum3d RS iffD1) 1),
+	(etac subst 1),
+	(etac subst 1),
+	(etac is_ub_thelub 1)
+	]);
+
+
+val ssum_lemma10 = prove_goal Ssum3.thy 
+"[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x.Y(i)=Isinr(x)"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(strip_tac 1),
+	(res_inst_tac [("p","Y(i)")] IssumE 1),
+	(rtac exI 1),
+	(etac trans 1),
+	(rtac strict_IsinlIsinr 1),
+	(etac exI 2),
+	(res_inst_tac [("P","xa=UU")] notE 1),
+	(atac 1),
+	(rtac (less_ssum3c RS iffD1) 1),
+	(etac subst 1),
+	(etac subst 1),
+	(etac is_ub_thelub 1)
+	]);
+
+val ssum_lemma11 = prove_goal Ssum3.thy 
+"[| is_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 Ssum_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 Ssum_ss 1)
+	]);
+
+val ssum_lemma12 = prove_goal Ssum3.thy 
+"[| is_chain(Y); lub(range(Y)) = Isinl(x); ~ x = 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 Ssum_ss 1),
+	(res_inst_tac [("t","x")] subst 1),
+	(rtac inject_Isinl 1),
+	(rtac trans 1),
+	(atac 2),
+	(rtac (thelub_ssum1a RS sym) 1),
+	(atac 1),
+	(etac ssum_lemma9 1),
+	(atac 1),
+	(rtac trans 1),
+	(rtac contlub_cfun_arg 1),
+	(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
+	(atac 1),
+	(rtac lub_equal2 1),
+	(rtac (chain_mono2 RS exE) 1),
+	(atac 2),
+	(rtac chain_UU_I_inverse2 1),
+	(rtac (inst_ssum_pcpo RS ssubst) 1),
+	(etac swap 1),
+	(rtac inject_Isinl 1),
+	(rtac trans 1),
+	(etac sym 1),
+	(etac notnotD 1),
+	(rtac exI 1),
+	(strip_tac 1),
+	(rtac (ssum_lemma9 RS spec RS exE) 1),
+	(atac 1),
+	(atac 1),
+	(res_inst_tac [("t","Y(i)")] ssubst 1),
+	(atac 1),
+	(rtac trans 1),
+	(rtac cfun_arg_cong 1),
+	(rtac Iwhen2 1),
+	(res_inst_tac [("P","Y(i)=UU")] swap 1),
+	(fast_tac HOL_cs 1),
+	(rtac (inst_ssum_pcpo RS ssubst) 1),
+	(res_inst_tac [("t","Y(i)")] ssubst 1),
+	(atac 1),
+	(fast_tac HOL_cs 1),
+	(rtac (Iwhen2 RS ssubst) 1),
+	(res_inst_tac [("P","Y(i)=UU")] swap 1),
+	(fast_tac HOL_cs 1),
+	(rtac (inst_ssum_pcpo RS ssubst) 1),
+	(res_inst_tac [("t","Y(i)")] ssubst 1),
+	(atac 1),
+	(fast_tac HOL_cs 1),
+	(simp_tac Cfun_ss 1),
+	(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
+	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
+	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
+	]);
+
+
+val ssum_lemma13 = prove_goal Ssum3.thy 
+"[| is_chain(Y); lub(range(Y)) = Isinr(x); ~ x = 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 Ssum_ss 1),
+	(res_inst_tac [("t","x")] subst 1),
+	(rtac inject_Isinr 1),
+	(rtac trans 1),
+	(atac 2),
+	(rtac (thelub_ssum1b RS sym) 1),
+	(atac 1),
+	(etac ssum_lemma10 1),
+	(atac 1),
+	(rtac trans 1),
+	(rtac contlub_cfun_arg 1),
+	(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
+	(atac 1),
+	(rtac lub_equal2 1),
+	(rtac (chain_mono2 RS exE) 1),
+	(atac 2),
+	(rtac chain_UU_I_inverse2 1),
+	(rtac (inst_ssum_pcpo RS ssubst) 1),
+	(etac swap 1),
+	(rtac inject_Isinr 1),
+	(rtac trans 1),
+	(etac sym 1),
+	(rtac (strict_IsinlIsinr RS subst) 1),
+	(etac notnotD 1),
+	(rtac exI 1),
+	(strip_tac 1),
+	(rtac (ssum_lemma10 RS spec RS exE) 1),
+	(atac 1),
+	(atac 1),
+	(res_inst_tac [("t","Y(i)")] ssubst 1),
+	(atac 1),
+	(rtac trans 1),
+	(rtac cfun_arg_cong 1),
+	(rtac Iwhen3 1),
+	(res_inst_tac [("P","Y(i)=UU")] swap 1),
+	(fast_tac HOL_cs 1),
+	(dtac notnotD 1),
+	(rtac (inst_ssum_pcpo RS ssubst) 1),
+	(rtac (strict_IsinlIsinr RS ssubst) 1),
+	(res_inst_tac [("t","Y(i)")] ssubst 1),
+	(atac 1),
+	(fast_tac HOL_cs 1),
+	(rtac (Iwhen3 RS ssubst) 1),
+	(res_inst_tac [("P","Y(i)=UU")] swap 1),
+	(fast_tac HOL_cs 1),
+	(dtac notnotD 1),
+	(rtac (inst_ssum_pcpo RS ssubst) 1),
+	(rtac (strict_IsinlIsinr RS ssubst) 1),
+	(res_inst_tac [("t","Y(i)")] ssubst 1),
+	(atac 1),
+	(fast_tac HOL_cs 1),
+	(simp_tac Cfun_ss 1),
+	(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
+	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
+	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
+	]);
+
+
+val contlub_Iwhen3 = prove_goal Ssum3.thy "contlub(Iwhen(f)(g))"
+ (fn prems =>
+	[
+	(rtac contlubI 1),
+	(strip_tac 1),
+	(res_inst_tac [("p","lub(range(Y))")] IssumE 1),
+	(etac ssum_lemma11 1),
+	(atac 1),
+	(etac ssum_lemma12 1),
+	(atac 1),
+	(atac 1),
+	(etac ssum_lemma13 1),
+	(atac 1),
+	(atac 1)
+	]);
+
+val contX_Iwhen1 = prove_goal Ssum3.thy "contX(Iwhen)"
+ (fn prems =>
+	[
+	(rtac monocontlub2contX 1),
+	(rtac monofun_Iwhen1 1),
+	(rtac contlub_Iwhen1 1)
+	]);
+
+val contX_Iwhen2 = prove_goal Ssum3.thy "contX(Iwhen(f))"
+ (fn prems =>
+	[
+	(rtac monocontlub2contX 1),
+	(rtac monofun_Iwhen2 1),
+	(rtac contlub_Iwhen2 1)
+	]);
+
+val contX_Iwhen3 = prove_goal Ssum3.thy "contX(Iwhen(f)(g))"
+ (fn prems =>
+	[
+	(rtac monocontlub2contX 1),
+	(rtac monofun_Iwhen3 1),
+	(rtac contlub_Iwhen3 1)
+	]);
+
+(* ------------------------------------------------------------------------ *)
+(* continuous versions of lemmas for 'a ++ 'b                               *)
+(* ------------------------------------------------------------------------ *)
+
+val strict_sinl = prove_goalw Ssum3.thy [sinl_def] "sinl[UU]=UU"
+ (fn prems =>
+	[
+	(simp_tac (Ssum_ss addsimps [contX_Isinl]) 1),
+	(rtac (inst_ssum_pcpo RS sym) 1)
+	]);
+
+val strict_sinr = prove_goalw Ssum3.thy [sinr_def] "sinr[UU]=UU"
+ (fn prems =>
+	[
+	(simp_tac (Ssum_ss addsimps [contX_Isinr]) 1),
+	(rtac (inst_ssum_pcpo RS sym) 1)
+	]);
+
+val noteq_sinlsinr = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
+	"sinl[a]=sinr[b] ==> a=UU & b=UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac noteq_IsinlIsinr 1),
+	(etac box_equals 1),
+	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1),
+	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1)
+	]);
+
+val inject_sinl = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
+	"sinl[a1]=sinl[a2]==> a1=a2"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac inject_Isinl 1),
+	(etac box_equals 1),
+	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1),
+	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1)
+	]);
+
+val inject_sinr = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
+	"sinr[a1]=sinr[a2]==> a1=a2"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac inject_Isinr 1),
+	(etac box_equals 1),
+	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1),
+	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1)
+	]);
+
+
+val defined_sinl = prove_goal Ssum3.thy  
+	"~x=UU ==> ~sinl[x]=UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac swap 1),
+	(rtac inject_sinl 1),
+	(rtac (strict_sinl RS ssubst) 1),
+	(etac notnotD 1)
+	]);
+
+val defined_sinr = prove_goal Ssum3.thy  
+	"~x=UU ==> ~sinr[x]=UU"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac swap 1),
+	(rtac inject_sinr 1),
+	(rtac (strict_sinr RS ssubst) 1),
+	(etac notnotD 1)
+	]);
+
+val Exh_Ssum1 = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
+	"z=UU | (? a. z=sinl[a] & ~a=UU) | (? b. z=sinr[b] & ~b=UU)"
+ (fn prems =>
+	[
+	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1),
+	(rtac (inst_ssum_pcpo RS ssubst) 1),
+	(rtac Exh_Ssum 1)
+	]);
+
+
+val ssumE = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
+	"[|p=UU ==> Q ;\
+\	!!x.[|p=sinl[x]; ~x=UU |] ==> Q;\
+\	!!y.[|p=sinr[y]; ~y=UU |] ==> Q|] ==> Q"
+ (fn prems =>
+	[
+	(rtac IssumE 1),
+	(resolve_tac prems 1),
+	(rtac (inst_ssum_pcpo RS ssubst) 1),
+	(atac 1),
+	(resolve_tac prems 1),
+	(atac 2),
+	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1),
+	(resolve_tac prems 1),
+	(atac 2),
+	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1)
+	]);
+
+
+val ssumE2 = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
+      "[|!!x.[|p=sinl[x]|] ==> Q;\
+\	!!y.[|p=sinr[y]|] ==> Q|] ==> Q"
+ (fn prems =>
+	[
+	(rtac IssumE2 1),
+	(resolve_tac prems 1),
+	(rtac (beta_cfun RS ssubst) 1),
+	(rtac contX_Isinl 1),
+	(atac 1),
+	(resolve_tac prems 1),
+	(rtac (beta_cfun RS ssubst) 1),
+	(rtac contX_Isinr 1),
+	(atac 1)
+	]);
+
+val when1 = prove_goalw Ssum3.thy [when_def,sinl_def,sinr_def] 
+	"when[f][g][UU] = UU"
+ (fn prems =>
+	[
+	(rtac (inst_ssum_pcpo RS ssubst) 1),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX2contX_CF1L]) 1)),
+	(simp_tac Ssum_ss  1)
+	]);
+
+val when2 = prove_goalw Ssum3.thy [when_def,sinl_def,sinr_def] 
+	"~x=UU==>when[f][g][sinl[x]] = f[x]"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(asm_simp_tac Ssum_ss  1)
+	]);
+
+
+
+val when3 = prove_goalw Ssum3.thy [when_def,sinl_def,sinr_def] 
+	"~x=UU==>when[f][g][sinr[x]] = g[x]"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(asm_simp_tac Ssum_ss  1)
+	]);
+
+
+val less_ssum4a = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
+	"(sinl[x] << sinl[y]) = (x << y)"
+ (fn prems =>
+	[
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac less_ssum3a 1)
+	]);
+
+val less_ssum4b = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
+	"(sinr[x] << sinr[y]) = (x << y)"
+ (fn prems =>
+	[
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac less_ssum3b 1)
+	]);
+
+val less_ssum4c = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
+	"(sinl[x] << sinr[y]) = (x = UU)"
+ (fn prems =>
+	[
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac less_ssum3c 1)
+	]);
+
+val less_ssum4d = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
+	"(sinr[x] << sinl[y]) = (x = UU)"
+ (fn prems =>
+	[
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac less_ssum3d 1)
+	]);
+
+val ssum_chainE = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
+	"is_chain(Y) ==> (!i.? x.Y(i)=sinl[x])|(!i.? y.Y(i)=sinr[y])"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1),
+	(etac ssum_lemma4 1)
+	]);
+
+
+val thelub_ssum2a = prove_goalw Ssum3.thy [sinl_def,sinr_def,when_def] 
+"[| is_chain(Y); !i.? x. Y(i) = sinl[x] |] ==>\ 
+\   lub(range(Y)) = sinl[lub(range(%i. when[LAM x. x][LAM y. UU][Y(i)]))]"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ext RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac thelub_ssum1a 1),
+	(atac 1),
+	(rtac allI 1),
+	(etac allE 1),
+	(etac exE 1),
+	(rtac exI 1),
+	(etac box_equals 1),
+	(rtac refl 1),
+	(asm_simp_tac (Ssum_ss addsimps [contX_Isinl]) 1)
+	]);
+
+val thelub_ssum2b = prove_goalw Ssum3.thy [sinl_def,sinr_def,when_def] 
+"[| is_chain(Y); !i.? x. Y(i) = sinr[x] |] ==>\ 
+\   lub(range(Y)) = sinr[lub(range(%i. when[LAM y. UU][LAM x. x][Y(i)]))]"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac (beta_cfun RS ext RS ssubst) 1),
+	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
+		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
+	(rtac thelub_ssum1b 1),
+	(atac 1),
+	(rtac allI 1),
+	(etac allE 1),
+	(etac exE 1),
+	(rtac exI 1),
+	(etac box_equals 1),
+	(rtac refl 1),
+	(asm_simp_tac (Ssum_ss addsimps 
+	[contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2,
+	contX_Iwhen3]) 1)
+	]);
+
+val thelub_ssum2a_rev = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
+	"[| is_chain(Y); lub(range(Y)) = sinl[x]|] ==> !i.? x.Y(i)=sinl[x]"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(asm_simp_tac (Ssum_ss addsimps 
+	[contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2,
+	contX_Iwhen3]) 1),
+	(etac ssum_lemma9 1),
+	(asm_simp_tac (Ssum_ss addsimps 
+	[contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2,
+	contX_Iwhen3]) 1)
+	]);
+
+val thelub_ssum2b_rev = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
+	"[| is_chain(Y); lub(range(Y)) = sinr[x]|] ==> !i.? x.Y(i)=sinr[x]"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(asm_simp_tac (Ssum_ss addsimps 
+	[contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2,
+	contX_Iwhen3]) 1),
+	(etac ssum_lemma10 1),
+	(asm_simp_tac (Ssum_ss addsimps 
+	[contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2,
+	contX_Iwhen3]) 1)
+	]);
+
+val thelub_ssum3 = prove_goal Ssum3.thy  
+"is_chain(Y) ==>\ 
+\   lub(range(Y)) = sinl[lub(range(%i. when[LAM x. x][LAM y. UU][Y(i)]))]\
+\ | lub(range(Y)) = sinr[lub(range(%i. when[LAM y. UU][LAM x. x][Y(i)]))]"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac (ssum_chainE RS disjE) 1),
+	(atac 1),
+	(rtac disjI1 1),
+	(etac thelub_ssum2a 1),
+	(atac 1),
+	(rtac disjI2 1),
+	(etac thelub_ssum2b 1),
+	(atac 1)
+	]);
+
+
+val when4 = prove_goal Ssum3.thy  
+	"when[sinl][sinr][z]=z"
+ (fn prems =>
+	[
+	(res_inst_tac [("p","z")] ssumE 1),
+	(asm_simp_tac (Cfun_ss addsimps [when1,when2,when3]) 1),
+	(asm_simp_tac (Cfun_ss addsimps [when1,when2,when3]) 1),
+	(asm_simp_tac (Cfun_ss addsimps [when1,when2,when3]) 1)
+	]);
+
+
+(* ------------------------------------------------------------------------ *)
+(* install simplifier for Ssum                                              *)
+(* ------------------------------------------------------------------------ *)
+
+val Ssum_rews = [strict_sinl,strict_sinr,when1,when2,when3];
+val Ssum_ss = Cfun_ss addsimps Ssum_rews;
isabelle