(* 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;