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