src/HOLCF/ssum3.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/ssum3.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for ssum3.thy
     7 *)
     8 
     9 open Ssum3;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* continuity for Isinl and Isinr                                           *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 
    16 val contlub_Isinl = prove_goal Ssum3.thy "contlub(Isinl)"
    17  (fn prems =>
    18 	[
    19 	(rtac contlubI 1),
    20 	(strip_tac 1),
    21 	(rtac trans 1),
    22 	(rtac (thelub_ssum1a RS sym) 2),
    23 	(rtac allI 3),
    24 	(rtac exI 3),
    25 	(rtac refl 3),
    26 	(etac (monofun_Isinl RS ch2ch_monofun) 2),
    27 	(res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1),
    28 	(res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
    29 	(atac 1),
    30 	(res_inst_tac [("f","Isinl")] arg_cong  1),
    31 	(rtac (chain_UU_I_inverse RS sym) 1),
    32 	(rtac allI 1),
    33 	(res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1),
    34 	(etac (chain_UU_I RS spec ) 1),
    35 	(atac 1),
    36 	(rtac Iwhen1 1),
    37 	(res_inst_tac [("f","Isinl")] arg_cong  1),
    38 	(rtac lub_equal 1),
    39 	(atac 1),
    40 	(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
    41 	(etac (monofun_Isinl RS ch2ch_monofun) 1),
    42 	(rtac allI 1),
    43 	(res_inst_tac [("Q","Y(k)=UU")] classical2 1),
    44 	(asm_simp_tac Ssum_ss 1),
    45 	(asm_simp_tac Ssum_ss 1)
    46 	]);
    47 
    48 val contlub_Isinr = prove_goal Ssum3.thy "contlub(Isinr)"
    49  (fn prems =>
    50 	[
    51 	(rtac contlubI 1),
    52 	(strip_tac 1),
    53 	(rtac trans 1),
    54 	(rtac (thelub_ssum1b RS sym) 2),
    55 	(rtac allI 3),
    56 	(rtac exI 3),
    57 	(rtac refl 3),
    58 	(etac (monofun_Isinr RS ch2ch_monofun) 2),
    59 	(res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1),
    60 	(res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
    61 	(atac 1),
    62 	((rtac arg_cong 1) THEN (rtac (chain_UU_I_inverse RS sym) 1)),
    63 	(rtac allI 1),
    64 	(res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1),
    65 	(etac (chain_UU_I RS spec ) 1),
    66 	(atac 1),
    67 	(rtac (strict_IsinlIsinr RS subst) 1),
    68 	(rtac Iwhen1 1),
    69 	((rtac arg_cong 1) THEN (rtac lub_equal 1)),
    70 	(atac 1),
    71 	(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
    72 	(etac (monofun_Isinr RS ch2ch_monofun) 1),
    73 	(rtac allI 1),
    74 	(res_inst_tac [("Q","Y(k)=UU")] classical2 1),
    75 	(asm_simp_tac Ssum_ss 1),
    76 	(asm_simp_tac Ssum_ss 1)
    77 	]);
    78 
    79 val contX_Isinl = prove_goal Ssum3.thy "contX(Isinl)"
    80  (fn prems =>
    81 	[
    82 	(rtac monocontlub2contX 1),
    83 	(rtac monofun_Isinl 1),
    84 	(rtac contlub_Isinl 1)
    85 	]);
    86 
    87 val contX_Isinr = prove_goal Ssum3.thy "contX(Isinr)"
    88  (fn prems =>
    89 	[
    90 	(rtac monocontlub2contX 1),
    91 	(rtac monofun_Isinr 1),
    92 	(rtac contlub_Isinr 1)
    93 	]);
    94 
    95 
    96 (* ------------------------------------------------------------------------ *)
    97 (* continuity for Iwhen in the firts two arguments                          *)
    98 (* ------------------------------------------------------------------------ *)
    99 
   100 val contlub_Iwhen1 = prove_goal Ssum3.thy "contlub(Iwhen)"
   101  (fn prems =>
   102 	[
   103 	(rtac contlubI 1),
   104 	(strip_tac 1),
   105 	(rtac trans 1),
   106 	(rtac (thelub_fun RS sym) 2),
   107 	(etac (monofun_Iwhen1 RS ch2ch_monofun) 2),
   108 	(rtac (expand_fun_eq RS iffD2) 1),
   109 	(strip_tac 1),
   110 	(rtac trans 1),
   111 	(rtac (thelub_fun RS sym) 2),
   112 	(rtac ch2ch_fun 2),
   113 	(etac (monofun_Iwhen1 RS ch2ch_monofun) 2),
   114 	(rtac (expand_fun_eq RS iffD2) 1),
   115 	(strip_tac 1),
   116 	(res_inst_tac [("p","xa")] IssumE 1),
   117 	(asm_simp_tac Ssum_ss 1),
   118 	(rtac (lub_const RS thelubI RS sym) 1),
   119 	(asm_simp_tac Ssum_ss 1),
   120 	(etac contlub_cfun_fun 1),
   121 	(asm_simp_tac Ssum_ss 1),
   122 	(rtac (lub_const RS thelubI RS sym) 1)
   123 	]);
   124 
   125 val contlub_Iwhen2 = prove_goal Ssum3.thy "contlub(Iwhen(f))"
   126  (fn prems =>
   127 	[
   128 	(rtac contlubI 1),
   129 	(strip_tac 1),
   130 	(rtac trans 1),
   131 	(rtac (thelub_fun RS sym) 2),
   132 	(etac (monofun_Iwhen2 RS ch2ch_monofun) 2),
   133 	(rtac (expand_fun_eq RS iffD2) 1),
   134 	(strip_tac 1),
   135 	(res_inst_tac [("p","x")] IssumE 1),
   136 	(asm_simp_tac Ssum_ss 1),
   137 	(rtac (lub_const RS thelubI RS sym) 1),
   138 	(asm_simp_tac Ssum_ss 1),
   139 	(rtac (lub_const RS thelubI RS sym) 1),
   140 	(asm_simp_tac Ssum_ss 1),
   141 	(etac contlub_cfun_fun 1)
   142 	]);
   143 
   144 (* ------------------------------------------------------------------------ *)
   145 (* continuity for Iwhen in its third argument                               *)
   146 (* ------------------------------------------------------------------------ *)
   147 
   148 (* ------------------------------------------------------------------------ *)
   149 (* first 5 ugly lemmas                                                      *)
   150 (* ------------------------------------------------------------------------ *)
   151 
   152 val ssum_lemma9 = prove_goal Ssum3.thy 
   153 "[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x.Y(i)=Isinl(x)"
   154  (fn prems =>
   155 	[
   156 	(cut_facts_tac prems 1),
   157 	(strip_tac 1),
   158 	(res_inst_tac [("p","Y(i)")] IssumE 1),
   159 	(etac exI 1),
   160 	(etac exI 1),
   161 	(res_inst_tac [("P","y=UU")] notE 1),
   162 	(atac 1),
   163 	(rtac (less_ssum3d RS iffD1) 1),
   164 	(etac subst 1),
   165 	(etac subst 1),
   166 	(etac is_ub_thelub 1)
   167 	]);
   168 
   169 
   170 val ssum_lemma10 = prove_goal Ssum3.thy 
   171 "[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x.Y(i)=Isinr(x)"
   172  (fn prems =>
   173 	[
   174 	(cut_facts_tac prems 1),
   175 	(strip_tac 1),
   176 	(res_inst_tac [("p","Y(i)")] IssumE 1),
   177 	(rtac exI 1),
   178 	(etac trans 1),
   179 	(rtac strict_IsinlIsinr 1),
   180 	(etac exI 2),
   181 	(res_inst_tac [("P","xa=UU")] notE 1),
   182 	(atac 1),
   183 	(rtac (less_ssum3c RS iffD1) 1),
   184 	(etac subst 1),
   185 	(etac subst 1),
   186 	(etac is_ub_thelub 1)
   187 	]);
   188 
   189 val ssum_lemma11 = prove_goal Ssum3.thy 
   190 "[| is_chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
   191 \   Iwhen(f,g,lub(range(Y))) = lub(range(%i. Iwhen(f,g,Y(i))))"
   192  (fn prems =>
   193 	[
   194 	(cut_facts_tac prems 1),
   195 	(asm_simp_tac Ssum_ss 1),
   196 	(rtac (chain_UU_I_inverse RS sym) 1),
   197 	(rtac allI 1),
   198 	(res_inst_tac [("s","Isinl(UU)"),("t","Y(i)")] subst 1),
   199 	(rtac (inst_ssum_pcpo RS subst) 1),
   200 	(rtac (chain_UU_I RS spec RS sym) 1),
   201 	(atac 1),
   202 	(etac (inst_ssum_pcpo RS ssubst) 1),
   203 	(asm_simp_tac Ssum_ss 1)
   204 	]);
   205 
   206 val ssum_lemma12 = prove_goal Ssum3.thy 
   207 "[| is_chain(Y); lub(range(Y)) = Isinl(x); ~ x = UU |] ==>\
   208 \   Iwhen(f,g,lub(range(Y))) = lub(range(%i. Iwhen(f,g,Y(i))))"
   209  (fn prems =>
   210 	[
   211 	(cut_facts_tac prems 1),
   212 	(asm_simp_tac Ssum_ss 1),
   213 	(res_inst_tac [("t","x")] subst 1),
   214 	(rtac inject_Isinl 1),
   215 	(rtac trans 1),
   216 	(atac 2),
   217 	(rtac (thelub_ssum1a RS sym) 1),
   218 	(atac 1),
   219 	(etac ssum_lemma9 1),
   220 	(atac 1),
   221 	(rtac trans 1),
   222 	(rtac contlub_cfun_arg 1),
   223 	(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
   224 	(atac 1),
   225 	(rtac lub_equal2 1),
   226 	(rtac (chain_mono2 RS exE) 1),
   227 	(atac 2),
   228 	(rtac chain_UU_I_inverse2 1),
   229 	(rtac (inst_ssum_pcpo RS ssubst) 1),
   230 	(etac swap 1),
   231 	(rtac inject_Isinl 1),
   232 	(rtac trans 1),
   233 	(etac sym 1),
   234 	(etac notnotD 1),
   235 	(rtac exI 1),
   236 	(strip_tac 1),
   237 	(rtac (ssum_lemma9 RS spec RS exE) 1),
   238 	(atac 1),
   239 	(atac 1),
   240 	(res_inst_tac [("t","Y(i)")] ssubst 1),
   241 	(atac 1),
   242 	(rtac trans 1),
   243 	(rtac cfun_arg_cong 1),
   244 	(rtac Iwhen2 1),
   245 	(res_inst_tac [("P","Y(i)=UU")] swap 1),
   246 	(fast_tac HOL_cs 1),
   247 	(rtac (inst_ssum_pcpo RS ssubst) 1),
   248 	(res_inst_tac [("t","Y(i)")] ssubst 1),
   249 	(atac 1),
   250 	(fast_tac HOL_cs 1),
   251 	(rtac (Iwhen2 RS ssubst) 1),
   252 	(res_inst_tac [("P","Y(i)=UU")] swap 1),
   253 	(fast_tac HOL_cs 1),
   254 	(rtac (inst_ssum_pcpo RS ssubst) 1),
   255 	(res_inst_tac [("t","Y(i)")] ssubst 1),
   256 	(atac 1),
   257 	(fast_tac HOL_cs 1),
   258 	(simp_tac Cfun_ss 1),
   259 	(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
   260 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
   261 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
   262 	]);
   263 
   264 
   265 val ssum_lemma13 = prove_goal Ssum3.thy 
   266 "[| is_chain(Y); lub(range(Y)) = Isinr(x); ~ x = UU |] ==>\
   267 \   Iwhen(f,g,lub(range(Y))) = lub(range(%i. Iwhen(f,g,Y(i))))"
   268  (fn prems =>
   269 	[
   270 	(cut_facts_tac prems 1),
   271 	(asm_simp_tac Ssum_ss 1),
   272 	(res_inst_tac [("t","x")] subst 1),
   273 	(rtac inject_Isinr 1),
   274 	(rtac trans 1),
   275 	(atac 2),
   276 	(rtac (thelub_ssum1b RS sym) 1),
   277 	(atac 1),
   278 	(etac ssum_lemma10 1),
   279 	(atac 1),
   280 	(rtac trans 1),
   281 	(rtac contlub_cfun_arg 1),
   282 	(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
   283 	(atac 1),
   284 	(rtac lub_equal2 1),
   285 	(rtac (chain_mono2 RS exE) 1),
   286 	(atac 2),
   287 	(rtac chain_UU_I_inverse2 1),
   288 	(rtac (inst_ssum_pcpo RS ssubst) 1),
   289 	(etac swap 1),
   290 	(rtac inject_Isinr 1),
   291 	(rtac trans 1),
   292 	(etac sym 1),
   293 	(rtac (strict_IsinlIsinr RS subst) 1),
   294 	(etac notnotD 1),
   295 	(rtac exI 1),
   296 	(strip_tac 1),
   297 	(rtac (ssum_lemma10 RS spec RS exE) 1),
   298 	(atac 1),
   299 	(atac 1),
   300 	(res_inst_tac [("t","Y(i)")] ssubst 1),
   301 	(atac 1),
   302 	(rtac trans 1),
   303 	(rtac cfun_arg_cong 1),
   304 	(rtac Iwhen3 1),
   305 	(res_inst_tac [("P","Y(i)=UU")] swap 1),
   306 	(fast_tac HOL_cs 1),
   307 	(dtac notnotD 1),
   308 	(rtac (inst_ssum_pcpo RS ssubst) 1),
   309 	(rtac (strict_IsinlIsinr RS ssubst) 1),
   310 	(res_inst_tac [("t","Y(i)")] ssubst 1),
   311 	(atac 1),
   312 	(fast_tac HOL_cs 1),
   313 	(rtac (Iwhen3 RS ssubst) 1),
   314 	(res_inst_tac [("P","Y(i)=UU")] swap 1),
   315 	(fast_tac HOL_cs 1),
   316 	(dtac notnotD 1),
   317 	(rtac (inst_ssum_pcpo RS ssubst) 1),
   318 	(rtac (strict_IsinlIsinr RS ssubst) 1),
   319 	(res_inst_tac [("t","Y(i)")] ssubst 1),
   320 	(atac 1),
   321 	(fast_tac HOL_cs 1),
   322 	(simp_tac Cfun_ss 1),
   323 	(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
   324 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
   325 	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
   326 	]);
   327 
   328 
   329 val contlub_Iwhen3 = prove_goal Ssum3.thy "contlub(Iwhen(f)(g))"
   330  (fn prems =>
   331 	[
   332 	(rtac contlubI 1),
   333 	(strip_tac 1),
   334 	(res_inst_tac [("p","lub(range(Y))")] IssumE 1),
   335 	(etac ssum_lemma11 1),
   336 	(atac 1),
   337 	(etac ssum_lemma12 1),
   338 	(atac 1),
   339 	(atac 1),
   340 	(etac ssum_lemma13 1),
   341 	(atac 1),
   342 	(atac 1)
   343 	]);
   344 
   345 val contX_Iwhen1 = prove_goal Ssum3.thy "contX(Iwhen)"
   346  (fn prems =>
   347 	[
   348 	(rtac monocontlub2contX 1),
   349 	(rtac monofun_Iwhen1 1),
   350 	(rtac contlub_Iwhen1 1)
   351 	]);
   352 
   353 val contX_Iwhen2 = prove_goal Ssum3.thy "contX(Iwhen(f))"
   354  (fn prems =>
   355 	[
   356 	(rtac monocontlub2contX 1),
   357 	(rtac monofun_Iwhen2 1),
   358 	(rtac contlub_Iwhen2 1)
   359 	]);
   360 
   361 val contX_Iwhen3 = prove_goal Ssum3.thy "contX(Iwhen(f)(g))"
   362  (fn prems =>
   363 	[
   364 	(rtac monocontlub2contX 1),
   365 	(rtac monofun_Iwhen3 1),
   366 	(rtac contlub_Iwhen3 1)
   367 	]);
   368 
   369 (* ------------------------------------------------------------------------ *)
   370 (* continuous versions of lemmas for 'a ++ 'b                               *)
   371 (* ------------------------------------------------------------------------ *)
   372 
   373 val strict_sinl = prove_goalw Ssum3.thy [sinl_def] "sinl[UU]=UU"
   374  (fn prems =>
   375 	[
   376 	(simp_tac (Ssum_ss addsimps [contX_Isinl]) 1),
   377 	(rtac (inst_ssum_pcpo RS sym) 1)
   378 	]);
   379 
   380 val strict_sinr = prove_goalw Ssum3.thy [sinr_def] "sinr[UU]=UU"
   381  (fn prems =>
   382 	[
   383 	(simp_tac (Ssum_ss addsimps [contX_Isinr]) 1),
   384 	(rtac (inst_ssum_pcpo RS sym) 1)
   385 	]);
   386 
   387 val noteq_sinlsinr = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
   388 	"sinl[a]=sinr[b] ==> a=UU & b=UU"
   389  (fn prems =>
   390 	[
   391 	(cut_facts_tac prems 1),
   392 	(rtac noteq_IsinlIsinr 1),
   393 	(etac box_equals 1),
   394 	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1),
   395 	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1)
   396 	]);
   397 
   398 val inject_sinl = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
   399 	"sinl[a1]=sinl[a2]==> a1=a2"
   400  (fn prems =>
   401 	[
   402 	(cut_facts_tac prems 1),
   403 	(rtac inject_Isinl 1),
   404 	(etac box_equals 1),
   405 	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1),
   406 	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1)
   407 	]);
   408 
   409 val inject_sinr = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
   410 	"sinr[a1]=sinr[a2]==> a1=a2"
   411  (fn prems =>
   412 	[
   413 	(cut_facts_tac prems 1),
   414 	(rtac inject_Isinr 1),
   415 	(etac box_equals 1),
   416 	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1),
   417 	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1)
   418 	]);
   419 
   420 
   421 val defined_sinl = prove_goal Ssum3.thy  
   422 	"~x=UU ==> ~sinl[x]=UU"
   423  (fn prems =>
   424 	[
   425 	(cut_facts_tac prems 1),
   426 	(etac swap 1),
   427 	(rtac inject_sinl 1),
   428 	(rtac (strict_sinl RS ssubst) 1),
   429 	(etac notnotD 1)
   430 	]);
   431 
   432 val defined_sinr = prove_goal Ssum3.thy  
   433 	"~x=UU ==> ~sinr[x]=UU"
   434  (fn prems =>
   435 	[
   436 	(cut_facts_tac prems 1),
   437 	(etac swap 1),
   438 	(rtac inject_sinr 1),
   439 	(rtac (strict_sinr RS ssubst) 1),
   440 	(etac notnotD 1)
   441 	]);
   442 
   443 val Exh_Ssum1 = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
   444 	"z=UU | (? a. z=sinl[a] & ~a=UU) | (? b. z=sinr[b] & ~b=UU)"
   445  (fn prems =>
   446 	[
   447 	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1),
   448 	(rtac (inst_ssum_pcpo RS ssubst) 1),
   449 	(rtac Exh_Ssum 1)
   450 	]);
   451 
   452 
   453 val ssumE = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
   454 	"[|p=UU ==> Q ;\
   455 \	!!x.[|p=sinl[x]; ~x=UU |] ==> Q;\
   456 \	!!y.[|p=sinr[y]; ~y=UU |] ==> Q|] ==> Q"
   457  (fn prems =>
   458 	[
   459 	(rtac IssumE 1),
   460 	(resolve_tac prems 1),
   461 	(rtac (inst_ssum_pcpo RS ssubst) 1),
   462 	(atac 1),
   463 	(resolve_tac prems 1),
   464 	(atac 2),
   465 	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1),
   466 	(resolve_tac prems 1),
   467 	(atac 2),
   468 	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1)
   469 	]);
   470 
   471 
   472 val ssumE2 = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
   473       "[|!!x.[|p=sinl[x]|] ==> Q;\
   474 \	!!y.[|p=sinr[y]|] ==> Q|] ==> Q"
   475  (fn prems =>
   476 	[
   477 	(rtac IssumE2 1),
   478 	(resolve_tac prems 1),
   479 	(rtac (beta_cfun RS ssubst) 1),
   480 	(rtac contX_Isinl 1),
   481 	(atac 1),
   482 	(resolve_tac prems 1),
   483 	(rtac (beta_cfun RS ssubst) 1),
   484 	(rtac contX_Isinr 1),
   485 	(atac 1)
   486 	]);
   487 
   488 val when1 = prove_goalw Ssum3.thy [when_def,sinl_def,sinr_def] 
   489 	"when[f][g][UU] = UU"
   490  (fn prems =>
   491 	[
   492 	(rtac (inst_ssum_pcpo RS ssubst) 1),
   493 	(rtac (beta_cfun RS ssubst) 1),
   494 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   495 		contX_Iwhen3,contX2contX_CF1L]) 1)),
   496 	(rtac (beta_cfun RS ssubst) 1),
   497 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   498 		contX_Iwhen3,contX2contX_CF1L]) 1)),
   499 	(rtac (beta_cfun RS ssubst) 1),
   500 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   501 		contX_Iwhen3,contX2contX_CF1L]) 1)),
   502 	(simp_tac Ssum_ss  1)
   503 	]);
   504 
   505 val when2 = prove_goalw Ssum3.thy [when_def,sinl_def,sinr_def] 
   506 	"~x=UU==>when[f][g][sinl[x]] = f[x]"
   507  (fn prems =>
   508 	[
   509 	(cut_facts_tac prems 1),
   510 	(rtac (beta_cfun RS ssubst) 1),
   511 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   512 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   513 	(rtac (beta_cfun RS ssubst) 1),
   514 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   515 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   516 	(rtac (beta_cfun RS ssubst) 1),
   517 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   518 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   519 	(rtac (beta_cfun RS ssubst) 1),
   520 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   521 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   522 	(asm_simp_tac Ssum_ss  1)
   523 	]);
   524 
   525 
   526 
   527 val when3 = prove_goalw Ssum3.thy [when_def,sinl_def,sinr_def] 
   528 	"~x=UU==>when[f][g][sinr[x]] = g[x]"
   529  (fn prems =>
   530 	[
   531 	(cut_facts_tac prems 1),
   532 	(rtac (beta_cfun RS ssubst) 1),
   533 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   534 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   535 	(rtac (beta_cfun RS ssubst) 1),
   536 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   537 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   538 	(rtac (beta_cfun RS ssubst) 1),
   539 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   540 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   541 	(rtac (beta_cfun RS ssubst) 1),
   542 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   543 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   544 	(asm_simp_tac Ssum_ss  1)
   545 	]);
   546 
   547 
   548 val less_ssum4a = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
   549 	"(sinl[x] << sinl[y]) = (x << y)"
   550  (fn prems =>
   551 	[
   552 	(rtac (beta_cfun RS ssubst) 1),
   553 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   554 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   555 	(rtac (beta_cfun RS ssubst) 1),
   556 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   557 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   558 	(rtac less_ssum3a 1)
   559 	]);
   560 
   561 val less_ssum4b = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
   562 	"(sinr[x] << sinr[y]) = (x << y)"
   563  (fn prems =>
   564 	[
   565 	(rtac (beta_cfun RS ssubst) 1),
   566 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   567 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   568 	(rtac (beta_cfun RS ssubst) 1),
   569 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   570 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   571 	(rtac less_ssum3b 1)
   572 	]);
   573 
   574 val less_ssum4c = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
   575 	"(sinl[x] << sinr[y]) = (x = UU)"
   576  (fn prems =>
   577 	[
   578 	(rtac (beta_cfun RS ssubst) 1),
   579 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   580 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   581 	(rtac (beta_cfun RS ssubst) 1),
   582 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   583 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   584 	(rtac less_ssum3c 1)
   585 	]);
   586 
   587 val less_ssum4d = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
   588 	"(sinr[x] << sinl[y]) = (x = UU)"
   589  (fn prems =>
   590 	[
   591 	(rtac (beta_cfun RS ssubst) 1),
   592 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   593 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   594 	(rtac (beta_cfun RS ssubst) 1),
   595 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   596 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   597 	(rtac less_ssum3d 1)
   598 	]);
   599 
   600 val ssum_chainE = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
   601 	"is_chain(Y) ==> (!i.? x.Y(i)=sinl[x])|(!i.? y.Y(i)=sinr[y])"
   602  (fn prems =>
   603 	[
   604 	(cut_facts_tac prems 1),
   605 	(asm_simp_tac (Ssum_ss addsimps [contX_Isinr,contX_Isinl]) 1),
   606 	(etac ssum_lemma4 1)
   607 	]);
   608 
   609 
   610 val thelub_ssum2a = prove_goalw Ssum3.thy [sinl_def,sinr_def,when_def] 
   611 "[| is_chain(Y); !i.? x. Y(i) = sinl[x] |] ==>\ 
   612 \   lub(range(Y)) = sinl[lub(range(%i. when[LAM x. x][LAM y. UU][Y(i)]))]"
   613  (fn prems =>
   614 	[
   615 	(cut_facts_tac prems 1),
   616 	(rtac (beta_cfun RS ssubst) 1),
   617 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   618 	(rtac (beta_cfun RS ssubst) 1),
   619 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   620 	(rtac (beta_cfun RS ssubst) 1),
   621 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   622 	(rtac (beta_cfun RS ext RS ssubst) 1),
   623 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   624 	(rtac thelub_ssum1a 1),
   625 	(atac 1),
   626 	(rtac allI 1),
   627 	(etac allE 1),
   628 	(etac exE 1),
   629 	(rtac exI 1),
   630 	(etac box_equals 1),
   631 	(rtac refl 1),
   632 	(asm_simp_tac (Ssum_ss addsimps [contX_Isinl]) 1)
   633 	]);
   634 
   635 val thelub_ssum2b = prove_goalw Ssum3.thy [sinl_def,sinr_def,when_def] 
   636 "[| is_chain(Y); !i.? x. Y(i) = sinr[x] |] ==>\ 
   637 \   lub(range(Y)) = sinr[lub(range(%i. when[LAM y. UU][LAM x. x][Y(i)]))]"
   638  (fn prems =>
   639 	[
   640 	(cut_facts_tac prems 1),
   641 	(rtac (beta_cfun RS ssubst) 1),
   642 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   643 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   644 	(rtac (beta_cfun RS ssubst) 1),
   645 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   646 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   647 	(rtac (beta_cfun RS ssubst) 1),
   648 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   649 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   650 	(rtac (beta_cfun RS ext RS ssubst) 1),
   651 	(REPEAT (resolve_tac (contX_lemmas @ [contX_Iwhen1,contX_Iwhen2,
   652 		contX_Iwhen3,contX_Isinl,contX_Isinr,contX2contX_CF1L]) 1)),
   653 	(rtac thelub_ssum1b 1),
   654 	(atac 1),
   655 	(rtac allI 1),
   656 	(etac allE 1),
   657 	(etac exE 1),
   658 	(rtac exI 1),
   659 	(etac box_equals 1),
   660 	(rtac refl 1),
   661 	(asm_simp_tac (Ssum_ss addsimps 
   662 	[contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2,
   663 	contX_Iwhen3]) 1)
   664 	]);
   665 
   666 val thelub_ssum2a_rev = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
   667 	"[| is_chain(Y); lub(range(Y)) = sinl[x]|] ==> !i.? x.Y(i)=sinl[x]"
   668  (fn prems =>
   669 	[
   670 	(cut_facts_tac prems 1),
   671 	(asm_simp_tac (Ssum_ss addsimps 
   672 	[contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2,
   673 	contX_Iwhen3]) 1),
   674 	(etac ssum_lemma9 1),
   675 	(asm_simp_tac (Ssum_ss addsimps 
   676 	[contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2,
   677 	contX_Iwhen3]) 1)
   678 	]);
   679 
   680 val thelub_ssum2b_rev = prove_goalw Ssum3.thy [sinl_def,sinr_def] 
   681 	"[| is_chain(Y); lub(range(Y)) = sinr[x]|] ==> !i.? x.Y(i)=sinr[x]"
   682  (fn prems =>
   683 	[
   684 	(cut_facts_tac prems 1),
   685 	(asm_simp_tac (Ssum_ss addsimps 
   686 	[contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2,
   687 	contX_Iwhen3]) 1),
   688 	(etac ssum_lemma10 1),
   689 	(asm_simp_tac (Ssum_ss addsimps 
   690 	[contX_Isinr,contX_Isinl,contX_Iwhen1,contX_Iwhen2,
   691 	contX_Iwhen3]) 1)
   692 	]);
   693 
   694 val thelub_ssum3 = prove_goal Ssum3.thy  
   695 "is_chain(Y) ==>\ 
   696 \   lub(range(Y)) = sinl[lub(range(%i. when[LAM x. x][LAM y. UU][Y(i)]))]\
   697 \ | lub(range(Y)) = sinr[lub(range(%i. when[LAM y. UU][LAM x. x][Y(i)]))]"
   698  (fn prems =>
   699 	[
   700 	(cut_facts_tac prems 1),
   701 	(rtac (ssum_chainE RS disjE) 1),
   702 	(atac 1),
   703 	(rtac disjI1 1),
   704 	(etac thelub_ssum2a 1),
   705 	(atac 1),
   706 	(rtac disjI2 1),
   707 	(etac thelub_ssum2b 1),
   708 	(atac 1)
   709 	]);
   710 
   711 
   712 val when4 = prove_goal Ssum3.thy  
   713 	"when[sinl][sinr][z]=z"
   714  (fn prems =>
   715 	[
   716 	(res_inst_tac [("p","z")] ssumE 1),
   717 	(asm_simp_tac (Cfun_ss addsimps [when1,when2,when3]) 1),
   718 	(asm_simp_tac (Cfun_ss addsimps [when1,when2,when3]) 1),
   719 	(asm_simp_tac (Cfun_ss addsimps [when1,when2,when3]) 1)
   720 	]);
   721 
   722 
   723 (* ------------------------------------------------------------------------ *)
   724 (* install simplifier for Ssum                                              *)
   725 (* ------------------------------------------------------------------------ *)
   726 
   727 val Ssum_rews = [strict_sinl,strict_sinr,when1,when2,when3];
   728 val Ssum_ss = Cfun_ss addsimps Ssum_rews;