Mercurial Mercurial > repos > isabelle / comparison
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 9169 85a47aa21f74
parent 8161 bde1391fd0a5
child 9245 428385c4bc50
equal deleted inserted replaced
9168:77658111e122 9169:85a47aa21f74 
     1 (*  Title:      HOLCF/ssum3.ML
 
     1 (*  Title:      HOLCF/Ssum3.ML
 
     2     ID:         $Id$
 
     2     ID:         $Id$
 
     3     Author:     Franz Regensburger
 
     3     Author:     Franz Regensburger
 
     4     Copyright   1993 Technische Universitaet Muenchen
 
     4     Copyright   1993 Technische Universitaet Muenchen
 
     5 
     5 
     6 Lemmas for ssum3.thy
 
     6 Class instance of  ++ for class pcpo
 
     7 *)
 
     7 *)
 
     8 
     8 
     9 open Ssum3;
 
       
    10 
       
    11 (* for compatibility with old HOLCF-Version *)
 
     9 (* for compatibility with old HOLCF-Version *)
 
    12 qed_goal "inst_ssum_pcpo" thy "UU = Isinl UU"
 
    10 Goal "UU = Isinl UU";
 
    13  (fn prems => 
    11 by (simp_tac (HOL_ss addsimps [UU_def,UU_ssum_def]) 1);
 
    14         [
 
    12 qed "inst_ssum_pcpo";
 
    15         (simp_tac (HOL_ss addsimps [UU_def,UU_ssum_def]) 1)
 
       
    16         ]);
 
       
    17 
    13 
    18 (* ------------------------------------------------------------------------ *)
 
    14 (* ------------------------------------------------------------------------ *)
 
    19 (* continuity for Isinl and Isinr                                           *)
 
    15 (* continuity for Isinl and Isinr                                           *)
 
    20 (* ------------------------------------------------------------------------ *)
 
    16 (* ------------------------------------------------------------------------ *)
 
    21 
    17 
    22 qed_goal "contlub_Isinl" Ssum3.thy "contlub(Isinl)"
 
    18 Goal "contlub(Isinl)";
 
    23  (fn prems =>
 
    19 by (rtac contlubI 1);
 
    24         [
 
    20 by (strip_tac 1);
 
    25         (rtac contlubI 1),
 
    21 by (rtac trans 1);
 
    26         (strip_tac 1),
 
    22 by (rtac (thelub_ssum1a RS sym) 2);
 
    27         (rtac trans 1),
 
    23 by (rtac allI 3);
 
    28         (rtac (thelub_ssum1a RS sym) 2),
 
    24 by (rtac exI 3);
 
    29         (rtac allI 3),
 
    25 by (rtac refl 3);
 
    30         (rtac exI 3),
 
    26 by (etac (monofun_Isinl RS ch2ch_monofun) 2);
 
    31         (rtac refl 3),
 
    27 by (case_tac "lub(range(Y))=UU" 1);
 
    32         (etac (monofun_Isinl RS ch2ch_monofun) 2),
 
    28 by (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1);
 
    33         (case_tac "lub(range(Y))=UU" 1),
 
    29 by (atac 1);
 
    34         (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
 
    30 by (res_inst_tac [("f","Isinl")] arg_cong  1);
 
    35         (atac 1),
 
    31 by (rtac (chain_UU_I_inverse RS sym) 1);
 
    36         (res_inst_tac [("f","Isinl")] arg_cong  1),
 
    32 by (rtac allI 1);
 
    37         (rtac (chain_UU_I_inverse RS sym) 1),
 
    33 by (res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1);
 
    38         (rtac allI 1),
 
    34 by (etac (chain_UU_I RS spec ) 1);
 
    39         (res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1),
 
    35 by (atac 1);
 
    40         (etac (chain_UU_I RS spec ) 1),
 
    36 by (rtac Iwhen1 1);
 
    41         (atac 1),
 
    37 by (res_inst_tac [("f","Isinl")] arg_cong  1);
 
    42         (rtac Iwhen1 1),
 
    38 by (rtac lub_equal 1);
 
    43         (res_inst_tac [("f","Isinl")] arg_cong  1),
 
    39 by (atac 1);
 
    44         (rtac lub_equal 1),
 
    40 by (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1);
 
    45         (atac 1),
 
    41 by (etac (monofun_Isinl RS ch2ch_monofun) 1);
 
    46         (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
 
    42 by (rtac allI 1);
 
    47         (etac (monofun_Isinl RS ch2ch_monofun) 1),
 
    43 by (case_tac "Y(k)=UU" 1);
 
    48         (rtac allI 1),
 
    44 by (asm_simp_tac Ssum0_ss 1);
 
    49         (case_tac "Y(k)=UU" 1),
 
    45 by (asm_simp_tac Ssum0_ss 1);
 
    50         (asm_simp_tac Ssum0_ss 1),
 
    46 qed "contlub_Isinl";
 
    51         (asm_simp_tac Ssum0_ss 1)
 
    47 
    52         ]);
 
    48 Goal "contlub(Isinr)";
 
    53 
    49 by (rtac contlubI 1);
 
    54 qed_goal "contlub_Isinr" Ssum3.thy "contlub(Isinr)"
 
    50 by (strip_tac 1);
 
    55  (fn prems =>
 
    51 by (rtac trans 1);
 
    56         [
 
    52 by (rtac (thelub_ssum1b RS sym) 2);
 
    57         (rtac contlubI 1),
 
    53 by (rtac allI 3);
 
    58         (strip_tac 1),
 
    54 by (rtac exI 3);
 
    59         (rtac trans 1),
 
    55 by (rtac refl 3);
 
    60         (rtac (thelub_ssum1b RS sym) 2),
 
    56 by (etac (monofun_Isinr RS ch2ch_monofun) 2);
 
    61         (rtac allI 3),
 
    57 by (case_tac "lub(range(Y))=UU" 1);
 
    62         (rtac exI 3),
 
    58 by (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1);
 
    63         (rtac refl 3),
 
    59 by (atac 1);
 
    64         (etac (monofun_Isinr RS ch2ch_monofun) 2),
 
    60 by ((rtac arg_cong 1) THEN (rtac (chain_UU_I_inverse RS sym) 1));
 
    65         (case_tac "lub(range(Y))=UU" 1),
 
    61 by (rtac allI 1);
 
    66         (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
 
    62 by (res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1);
 
    67         (atac 1),
 
    63 by (etac (chain_UU_I RS spec ) 1);
 
    68         ((rtac arg_cong 1) THEN (rtac (chain_UU_I_inverse RS sym) 1)),
 
    64 by (atac 1);
 
    69         (rtac allI 1),
 
    65 by (rtac (strict_IsinlIsinr RS subst) 1);
 
    70         (res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1),
 
    66 by (rtac Iwhen1 1);
 
    71         (etac (chain_UU_I RS spec ) 1),
 
    67 by ((rtac arg_cong 1) THEN (rtac lub_equal 1));
 
    72         (atac 1),
 
    68 by (atac 1);
 
    73         (rtac (strict_IsinlIsinr RS subst) 1),
 
    69 by (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1);
 
    74         (rtac Iwhen1 1),
 
    70 by (etac (monofun_Isinr RS ch2ch_monofun) 1);
 
    75         ((rtac arg_cong 1) THEN (rtac lub_equal 1)),
 
    71 by (rtac allI 1);
 
    76         (atac 1),
 
    72 by (case_tac "Y(k)=UU" 1);
 
    77         (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
 
    73 by (asm_simp_tac Ssum0_ss 1);
 
    78         (etac (monofun_Isinr RS ch2ch_monofun) 1),
 
    74 by (asm_simp_tac Ssum0_ss 1);
 
    79         (rtac allI 1),
 
    75 qed "contlub_Isinr";
 
    80         (case_tac "Y(k)=UU" 1),
 
    76 
    81         (asm_simp_tac Ssum0_ss 1),
 
    77 Goal "cont(Isinl)";
 
    82         (asm_simp_tac Ssum0_ss 1)
 
    78 by (rtac monocontlub2cont 1);
 
    83         ]);
 
    79 by (rtac monofun_Isinl 1);
 
    84 
    80 by (rtac contlub_Isinl 1);
 
    85 qed_goal "cont_Isinl" Ssum3.thy "cont(Isinl)"
 
    81 qed "cont_Isinl";
 
    86  (fn prems =>
 
    82 
    87         [
 
    83 Goal "cont(Isinr)";
 
    88         (rtac monocontlub2cont 1),
 
    84 by (rtac monocontlub2cont 1);
 
    89         (rtac monofun_Isinl 1),
 
    85 by (rtac monofun_Isinr 1);
 
    90         (rtac contlub_Isinl 1)
 
    86 by (rtac contlub_Isinr 1);
 
    91         ]);
 
    87 qed "cont_Isinr";
 
    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 
    88 
   101 
    89 
   102 (* ------------------------------------------------------------------------ *)
 
    90 (* ------------------------------------------------------------------------ *)
 
   103 (* continuity for Iwhen in the firts two arguments                          *)
 
    91 (* continuity for Iwhen in the firts two arguments                          *)
 
   104 (* ------------------------------------------------------------------------ *)
 
    92 (* ------------------------------------------------------------------------ *)
 
   105 
    93 
   106 qed_goal "contlub_Iwhen1" Ssum3.thy "contlub(Iwhen)"
 
    94 Goal "contlub(Iwhen)";
 
   107  (fn prems =>
 
    95 by (rtac contlubI 1);
 
   108         [
 
    96 by (strip_tac 1);
 
   109         (rtac contlubI 1),
 
    97 by (rtac trans 1);
 
   110         (strip_tac 1),
 
    98 by (rtac (thelub_fun RS sym) 2);
 
   111         (rtac trans 1),
 
    99 by (etac (monofun_Iwhen1 RS ch2ch_monofun) 2);
 
   112         (rtac (thelub_fun RS sym) 2),
 
   100 by (rtac (expand_fun_eq RS iffD2) 1);
 
   113         (etac (monofun_Iwhen1 RS ch2ch_monofun) 2),
 
   101 by (strip_tac 1);
 
   114         (rtac (expand_fun_eq RS iffD2) 1),
 
   102 by (rtac trans 1);
 
   115         (strip_tac 1),
 
   103 by (rtac (thelub_fun RS sym) 2);
 
   116         (rtac trans 1),
 
   104 by (rtac ch2ch_fun 2);
 
   117         (rtac (thelub_fun RS sym) 2),
 
   105 by (etac (monofun_Iwhen1 RS ch2ch_monofun) 2);
 
   118         (rtac ch2ch_fun 2),
 
   106 by (rtac (expand_fun_eq RS iffD2) 1);
 
   119         (etac (monofun_Iwhen1 RS ch2ch_monofun) 2),
 
   107 by (strip_tac 1);
 
   120         (rtac (expand_fun_eq RS iffD2) 1),
 
   108 by (res_inst_tac [("p","xa")] IssumE 1);
 
   121         (strip_tac 1),
 
   109 by (asm_simp_tac Ssum0_ss 1);
 
   122         (res_inst_tac [("p","xa")] IssumE 1),
 
   110 by (rtac (lub_const RS thelubI RS sym) 1);
 
   123         (asm_simp_tac Ssum0_ss 1),
 
   111 by (asm_simp_tac Ssum0_ss 1);
 
   124         (rtac (lub_const RS thelubI RS sym) 1),
 
   112 by (etac contlub_cfun_fun 1);
 
   125         (asm_simp_tac Ssum0_ss 1),
 
   113 by (asm_simp_tac Ssum0_ss 1);
 
   126         (etac contlub_cfun_fun 1),
 
   114 by (rtac (lub_const RS thelubI RS sym) 1);
 
   127         (asm_simp_tac Ssum0_ss 1),
 
   115 qed "contlub_Iwhen1";
 
   128         (rtac (lub_const RS thelubI RS sym) 1)
 
   116 
   129         ]);
 
   117 Goal "contlub(Iwhen(f))";
 
   130 
   118 by (rtac contlubI 1);
 
   131 qed_goal "contlub_Iwhen2" Ssum3.thy "contlub(Iwhen(f))"
 
   119 by (strip_tac 1);
 
   132  (fn prems =>
 
   120 by (rtac trans 1);
 
   133         [
 
   121 by (rtac (thelub_fun RS sym) 2);
 
   134         (rtac contlubI 1),
 
   122 by (etac (monofun_Iwhen2 RS ch2ch_monofun) 2);
 
   135         (strip_tac 1),
 
   123 by (rtac (expand_fun_eq RS iffD2) 1);
 
   136         (rtac trans 1),
 
   124 by (strip_tac 1);
 
   137         (rtac (thelub_fun RS sym) 2),
 
   125 by (res_inst_tac [("p","x")] IssumE 1);
 
   138         (etac (monofun_Iwhen2 RS ch2ch_monofun) 2),
 
   126 by (asm_simp_tac Ssum0_ss 1);
 
   139         (rtac (expand_fun_eq RS iffD2) 1),
 
   127 by (rtac (lub_const RS thelubI RS sym) 1);
 
   140         (strip_tac 1),
 
   128 by (asm_simp_tac Ssum0_ss 1);
 
   141         (res_inst_tac [("p","x")] IssumE 1),
 
   129 by (rtac (lub_const RS thelubI RS sym) 1);
 
   142         (asm_simp_tac Ssum0_ss 1),
 
   130 by (asm_simp_tac Ssum0_ss 1);
 
   143         (rtac (lub_const RS thelubI RS sym) 1),
 
   131 by (etac contlub_cfun_fun 1);
 
   144         (asm_simp_tac Ssum0_ss 1),
 
   132 qed "contlub_Iwhen2";
 
   145         (rtac (lub_const RS thelubI RS sym) 1),
 
       
   146         (asm_simp_tac Ssum0_ss 1),
 
       
   147         (etac contlub_cfun_fun 1)
 
       
   148         ]);
 
       
   149 
   133 
   150 (* ------------------------------------------------------------------------ *)
 
   134 (* ------------------------------------------------------------------------ *)
 
   151 (* continuity for Iwhen in its third argument                               *)
 
   135 (* continuity for Iwhen in its third argument                               *)
 
   152 (* ------------------------------------------------------------------------ *)
 
   136 (* ------------------------------------------------------------------------ *)
 
   153 
   137 
   154 (* ------------------------------------------------------------------------ *)
 
   138 (* ------------------------------------------------------------------------ *)
 
   155 (* first 5 ugly lemmas                                                      *)
 
   139 (* first 5 ugly lemmas                                                      *)
 
   156 (* ------------------------------------------------------------------------ *)
 
   140 (* ------------------------------------------------------------------------ *)
 
   157 
   141 
   158 qed_goal "ssum_lemma9" Ssum3.thy 
   142 Goal "[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)";
 
   159 "[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
 
   143 by (strip_tac 1);
 
   160  (fn prems =>
 
   144 by (res_inst_tac [("p","Y(i)")] IssumE 1);
 
   161         [
 
   145 by (etac exI 1);
 
   162         (cut_facts_tac prems 1),
 
   146 by (etac exI 1);
 
   163         (strip_tac 1),
 
   147 by (res_inst_tac [("P","y=UU")] notE 1);
 
   164         (res_inst_tac [("p","Y(i)")] IssumE 1),
 
   148 by (atac 1);
 
   165         (etac exI 1),
 
   149 by (rtac (less_ssum3d RS iffD1) 1);
 
   166         (etac exI 1),
 
   150 by (etac subst 1);
 
   167         (res_inst_tac [("P","y=UU")] notE 1),
 
   151 by (etac subst 1);
 
   168         (atac 1),
 
   152 by (etac is_ub_thelub 1);
 
   169         (rtac (less_ssum3d RS iffD1) 1),
 
   153 qed "ssum_lemma9";
 
   170         (etac subst 1),
 
   154 
   171         (etac subst 1),
 
   155 
   172         (etac is_ub_thelub 1)
 
   156 Goal "[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)";
 
   173         ]);
 
   157 by (strip_tac 1);
 
   174 
   158 by (res_inst_tac [("p","Y(i)")] IssumE 1);
 
   175 
   159 by (rtac exI 1);
 
   176 qed_goal "ssum_lemma10" Ssum3.thy 
   160 by (etac trans 1);
 
   177 "[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
 
   161 by (rtac strict_IsinlIsinr 1);
 
   178  (fn prems =>
 
   162 by (etac exI 2);
 
   179         [
 
   163 by (res_inst_tac [("P","xa=UU")] notE 1);
 
   180         (cut_facts_tac prems 1),
 
   164 by (atac 1);
 
   181         (strip_tac 1),
 
   165 by (rtac (less_ssum3c RS iffD1) 1);
 
   182         (res_inst_tac [("p","Y(i)")] IssumE 1),
 
   166 by (etac subst 1);
 
   183         (rtac exI 1),
 
   167 by (etac subst 1);
 
   184         (etac trans 1),
 
   168 by (etac is_ub_thelub 1);
 
   185         (rtac strict_IsinlIsinr 1),
 
   169 qed "ssum_lemma10";
 
   186         (etac exI 2),
 
   170 
   187         (res_inst_tac [("P","xa=UU")] notE 1),
 
   171 Goal "[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
 
   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 Goal  
       
   196 "[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\
 
       
   197 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))";
 
   172 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))";
 
   198 by (asm_simp_tac Ssum0_ss 1);
 
   173 by (asm_simp_tac Ssum0_ss 1);
 
   199 by (rtac (chain_UU_I_inverse RS sym) 1);
 
   174 by (rtac (chain_UU_I_inverse RS sym) 1);
 
   200 by (rtac allI 1);
 
   175 by (rtac allI 1);
 
   201 by (res_inst_tac [("s","Isinl(UU)"),("t","Y(i)")] subst 1);
 
   176 by (res_inst_tac [("s","Isinl(UU)"),("t","Y(i)")] subst 1);
 
   204 by (atac 1);
 
   179 by (atac 1);
 
   205 by (etac (inst_ssum_pcpo RS ssubst) 1);
 
   180 by (etac (inst_ssum_pcpo RS ssubst) 1);
 
   206 by (asm_simp_tac Ssum0_ss 1);
 
   181 by (asm_simp_tac Ssum0_ss 1);
 
   207 qed "ssum_lemma11";
 
   182 qed "ssum_lemma11";
 
   208 
   183 
   209 qed_goal "ssum_lemma12" Ssum3.thy 
   184 Goal "[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
 
   210 "[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\
 
   185 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))";
 
   211 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
 
   186 by (asm_simp_tac Ssum0_ss 1);
 
   212  (fn prems =>
 
   187 by (res_inst_tac [("t","x")] subst 1);
 
   213         [
 
   188 by (rtac inject_Isinl 1);
 
   214         (cut_facts_tac prems 1),
 
   189 by (rtac trans 1);
 
   215         (asm_simp_tac Ssum0_ss 1),
 
   190 by (atac 2);
 
   216         (res_inst_tac [("t","x")] subst 1),
 
   191 by (rtac (thelub_ssum1a RS sym) 1);
 
   217         (rtac inject_Isinl 1),
 
   192 by (atac 1);
 
   218         (rtac trans 1),
 
   193 by (etac ssum_lemma9 1);
 
   219         (atac 2),
 
   194 by (atac 1);
 
   220         (rtac (thelub_ssum1a RS sym) 1),
 
   195 by (rtac trans 1);
 
   221         (atac 1),
 
   196 by (rtac contlub_cfun_arg 1);
 
   222         (etac ssum_lemma9 1),
 
   197 by (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1);
 
   223         (atac 1),
 
   198 by (atac 1);
 
   224         (rtac trans 1),
 
   199 by (rtac lub_equal2 1);
 
   225         (rtac contlub_cfun_arg 1),
 
   200 by (rtac (chain_mono2 RS exE) 1);
 
   226         (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
 
   201 by (atac 2);
 
   227         (atac 1),
 
   202 by (rtac chain_UU_I_inverse2 1);
 
   228         (rtac lub_equal2 1),
 
   203 by (stac inst_ssum_pcpo 1);
 
   229         (rtac (chain_mono2 RS exE) 1),
 
   204 by (etac swap 1);
 
   230         (atac 2),
 
   205 by (rtac inject_Isinl 1);
 
   231         (rtac chain_UU_I_inverse2 1),
 
   206 by (rtac trans 1);
 
   232         (stac inst_ssum_pcpo 1),
 
   207 by (etac sym 1);
 
   233         (etac swap 1),
 
   208 by (etac notnotD 1);
 
   234         (rtac inject_Isinl 1),
 
   209 by (rtac exI 1);
 
   235         (rtac trans 1),
 
   210 by (strip_tac 1);
 
   236         (etac sym 1),
 
   211 by (rtac (ssum_lemma9 RS spec RS exE) 1);
 
   237         (etac notnotD 1),
 
   212 by (atac 1);
 
   238         (rtac exI 1),
 
   213 by (atac 1);
 
   239         (strip_tac 1),
 
   214 by (res_inst_tac [("t","Y(i)")] ssubst 1);
 
   240         (rtac (ssum_lemma9 RS spec RS exE) 1),
 
   215 by (atac 1);
 
   241         (atac 1),
 
   216 by (rtac trans 1);
 
   242         (atac 1),
 
   217 by (rtac cfun_arg_cong 1);
 
   243         (res_inst_tac [("t","Y(i)")] ssubst 1),
 
   218 by (rtac Iwhen2 1);
 
   244         (atac 1),
 
   219 by (res_inst_tac [("Pa","Y(i)=UU")] swap 1);
 
   245         (rtac trans 1),
 
   220 by (fast_tac HOL_cs 1);
 
   246         (rtac cfun_arg_cong 1),
 
   221 by (stac inst_ssum_pcpo 1);
 
   247         (rtac Iwhen2 1),
 
   222 by (res_inst_tac [("t","Y(i)")] ssubst 1);
 
   248         (res_inst_tac [("Pa","Y(i)=UU")] swap 1),
 
   223 by (atac 1);
 
   249         (fast_tac HOL_cs 1),
 
   224 by (fast_tac HOL_cs 1);
 
   250         (stac inst_ssum_pcpo 1),
 
   225 by (stac Iwhen2 1);
 
   251         (res_inst_tac [("t","Y(i)")] ssubst 1),
 
   226 by (res_inst_tac [("Pa","Y(i)=UU")] swap 1);
 
   252         (atac 1),
 
   227 by (fast_tac HOL_cs 1);
 
   253         (fast_tac HOL_cs 1),
 
   228 by (stac inst_ssum_pcpo 1);
 
   254         (stac Iwhen2 1),
 
   229 by (res_inst_tac [("t","Y(i)")] ssubst 1);
 
   255         (res_inst_tac [("Pa","Y(i)=UU")] swap 1),
 
   230 by (atac 1);
 
   256         (fast_tac HOL_cs 1),
 
   231 by (fast_tac HOL_cs 1);
 
   257         (stac inst_ssum_pcpo 1),
 
   232 by (simp_tac (simpset_of Cfun3.thy) 1);
 
   258         (res_inst_tac [("t","Y(i)")] ssubst 1),
 
   233 by (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1);
 
   259         (atac 1),
 
   234 by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);
 
   260         (fast_tac HOL_cs 1),
 
   235 by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);
 
   261         (simp_tac (simpset_of Cfun3.thy) 1),
 
   236 qed "ssum_lemma12";
 
   262         (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1),
 
   237 
   263         (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
 
   238 
   264         (etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
 
   239 Goal "[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\
 
   265         ]);
 
   240 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))";
 
   266 
   241 by (asm_simp_tac Ssum0_ss 1);
 
   267 
   242 by (res_inst_tac [("t","x")] subst 1);
 
   268 qed_goal "ssum_lemma13" Ssum3.thy 
   243 by (rtac inject_Isinr 1);
 
   269 "[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\
 
   244 by (rtac trans 1);
 
   270 \   Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
 
   245 by (atac 2);
 
   271  (fn prems =>
 
   246 by (rtac (thelub_ssum1b RS sym) 1);
 
   272         [
 
   247 by (atac 1);
 
   273         (cut_facts_tac prems 1),
 
   248 by (etac ssum_lemma10 1);
 
   274         (asm_simp_tac Ssum0_ss 1),
 
   249 by (atac 1);
 
   275         (res_inst_tac [("t","x")] subst 1),
 
   250 by (rtac trans 1);
 
   276         (rtac inject_Isinr 1),
 
   251 by (rtac contlub_cfun_arg 1);
 
   277         (rtac trans 1),
 
   252 by (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1);
 
   278         (atac 2),
 
   253 by (atac 1);
 
   279         (rtac (thelub_ssum1b RS sym) 1),
 
   254 by (rtac lub_equal2 1);
 
   280         (atac 1),
 
   255 by (rtac (chain_mono2 RS exE) 1);
 
   281         (etac ssum_lemma10 1),
 
   256 by (atac 2);
 
   282         (atac 1),
 
   257 by (rtac chain_UU_I_inverse2 1);
 
   283         (rtac trans 1),
 
   258 by (stac inst_ssum_pcpo 1);
 
   284         (rtac contlub_cfun_arg 1),
 
   259 by (etac swap 1);
 
   285         (rtac (monofun_Iwhen3 RS ch2ch_monofun) 1),
 
   260 by (rtac inject_Isinr 1);
 
   286         (atac 1),
 
   261 by (rtac trans 1);
 
   287         (rtac lub_equal2 1),
 
   262 by (etac sym 1);
 
   288         (rtac (chain_mono2 RS exE) 1),
 
   263 by (rtac (strict_IsinlIsinr RS subst) 1);
 
   289         (atac 2),
 
   264 by (etac notnotD 1);
 
   290         (rtac chain_UU_I_inverse2 1),
 
   265 by (rtac exI 1);
 
   291         (stac inst_ssum_pcpo 1),
 
   266 by (strip_tac 1);
 
   292         (etac swap 1),
 
   267 by (rtac (ssum_lemma10 RS spec RS exE) 1);
 
   293         (rtac inject_Isinr 1),
 
   268 by (atac 1);
 
   294         (rtac trans 1),
 
   269 by (atac 1);
 
   295         (etac sym 1),
 
   270 by (res_inst_tac [("t","Y(i)")] ssubst 1);
 
   296         (rtac (strict_IsinlIsinr RS subst) 1),
 
   271 by (atac 1);
 
   297         (etac notnotD 1),
 
   272 by (rtac trans 1);
 
   298         (rtac exI 1),
 
   273 by (rtac cfun_arg_cong 1);
 
   299         (strip_tac 1),
 
   274 by (rtac Iwhen3 1);
 
   300         (rtac (ssum_lemma10 RS spec RS exE) 1),
 
   275 by (res_inst_tac [("Pa","Y(i)=UU")] swap 1);
 
   301         (atac 1),
 
   276 by (fast_tac HOL_cs 1);
 
   302         (atac 1),
 
   277 by (dtac notnotD 1);
 
   303         (res_inst_tac [("t","Y(i)")] ssubst 1),
 
   278 by (stac inst_ssum_pcpo 1);
 
   304         (atac 1),
 
   279 by (stac strict_IsinlIsinr 1);
 
   305         (rtac trans 1),
 
   280 by (res_inst_tac [("t","Y(i)")] ssubst 1);
 
   306         (rtac cfun_arg_cong 1),
 
   281 by (atac 1);
 
   307         (rtac Iwhen3 1),
 
   282 by (fast_tac HOL_cs 1);
 
   308         (res_inst_tac [("Pa","Y(i)=UU")] swap 1),
 
   283 by (stac Iwhen3 1);
 
   309         (fast_tac HOL_cs 1),
 
   284 by (res_inst_tac [("Pa","Y(i)=UU")] swap 1);
 
   310         (dtac notnotD 1),
 
   285 by (fast_tac HOL_cs 1);
 
   311         (stac inst_ssum_pcpo 1),
 
   286 by (dtac notnotD 1);
 
   312         (stac strict_IsinlIsinr 1),
 
   287 by (stac inst_ssum_pcpo 1);
 
   313         (res_inst_tac [("t","Y(i)")] ssubst 1),
 
   288 by (stac strict_IsinlIsinr 1);
 
   314         (atac 1),
 
   289 by (res_inst_tac [("t","Y(i)")] ssubst 1);
 
   315         (fast_tac HOL_cs 1),
 
   290 by (atac 1);
 
   316         (stac Iwhen3 1),
 
   291 by (fast_tac HOL_cs 1);
 
   317         (res_inst_tac [("Pa","Y(i)=UU")] swap 1),
 
   292 by (simp_tac (simpset_of Cfun3.thy) 1);
 
   318         (fast_tac HOL_cs 1),
 
   293 by (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1);
 
   319         (dtac notnotD 1),
 
   294 by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);
 
   320         (stac inst_ssum_pcpo 1),
 
   295 by (etac (monofun_Iwhen3 RS ch2ch_monofun) 1);
 
   321         (stac strict_IsinlIsinr 1),
 
   296 qed "ssum_lemma13";
 
   322         (res_inst_tac [("t","Y(i)")] ssubst 1),
 
   297 
   323         (atac 1),
 
   298 
   324         (fast_tac HOL_cs 1),
 
   299 Goal "contlub(Iwhen(f)(g))";
 
   325         (simp_tac (simpset_of Cfun3.thy) 1),
 
   300 by (rtac contlubI 1);
 
   326         (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1),
 
   301 by (strip_tac 1);
 
   327         (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
 
   302 by (res_inst_tac [("p","lub(range(Y))")] IssumE 1);
 
   328         (etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
 
   303 by (etac ssum_lemma11 1);
 
   329         ]);
 
   304 by (atac 1);
 
   330 
   305 by (etac ssum_lemma12 1);
 
   331 
   306 by (atac 1);
 
   332 qed_goal "contlub_Iwhen3" Ssum3.thy "contlub(Iwhen(f)(g))"
 
   307 by (atac 1);
 
   333  (fn prems =>
 
   308 by (etac ssum_lemma13 1);
 
   334         [
 
   309 by (atac 1);
 
   335         (rtac contlubI 1),
 
   310 by (atac 1);
 
   336         (strip_tac 1),
 
   311 qed "contlub_Iwhen3";
 
   337         (res_inst_tac [("p","lub(range(Y))")] IssumE 1),
 
   312 
   338         (etac ssum_lemma11 1),
 
   313 Goal "cont(Iwhen)";
 
   339         (atac 1),
 
   314 by (rtac monocontlub2cont 1);
 
   340         (etac ssum_lemma12 1),
 
   315 by (rtac monofun_Iwhen1 1);
 
   341         (atac 1),
 
   316 by (rtac contlub_Iwhen1 1);
 
   342         (atac 1),
 
   317 qed "cont_Iwhen1";
 
   343         (etac ssum_lemma13 1),
 
   318 
   344         (atac 1),
 
   319 Goal "cont(Iwhen(f))";
 
   345         (atac 1)
 
   320 by (rtac monocontlub2cont 1);
 
   346         ]);
 
   321 by (rtac monofun_Iwhen2 1);
 
   347 
   322 by (rtac contlub_Iwhen2 1);
 
   348 qed_goal "cont_Iwhen1" Ssum3.thy "cont(Iwhen)"
 
   323 qed "cont_Iwhen2";
 
   349  (fn prems =>
 
   324 
   350         [
 
   325 Goal "cont(Iwhen(f)(g))";
 
   351         (rtac monocontlub2cont 1),
 
   326 by (rtac monocontlub2cont 1);
 
   352         (rtac monofun_Iwhen1 1),
 
   327 by (rtac monofun_Iwhen3 1);
 
   353         (rtac contlub_Iwhen1 1)
 
   328 by (rtac contlub_Iwhen3 1);
 
   354         ]);
 
   329 qed "cont_Iwhen3";
 
   355 
       
   356 qed_goal "cont_Iwhen2" Ssum3.thy "cont(Iwhen(f))"
 
       
   357  (fn prems =>
 
       
   358         [
 
       
   359         (rtac monocontlub2cont 1),
 
       
   360         (rtac monofun_Iwhen2 1),
 
       
   361         (rtac contlub_Iwhen2 1)
 
       
   362         ]);
 
       
   363 
       
   364 qed_goal "cont_Iwhen3" Ssum3.thy "cont(Iwhen(f)(g))"
 
       
   365  (fn prems =>
 
       
   366         [
 
       
   367         (rtac monocontlub2cont 1),
 
       
   368         (rtac monofun_Iwhen3 1),
 
       
   369         (rtac contlub_Iwhen3 1)
 
       
   370         ]);
 
       
   371 
   330 
   372 (* ------------------------------------------------------------------------ *)
 
   331 (* ------------------------------------------------------------------------ *)
 
   373 (* continuous versions of lemmas for 'a ++ 'b                               *)
 
   332 (* continuous versions of lemmas for 'a ++ 'b                               *)
 
   374 (* ------------------------------------------------------------------------ *)
 
   333 (* ------------------------------------------------------------------------ *)
 
   375 
   334 
   419         (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1),
 
   378         (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1),
 
   420         (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1)
 
   379         (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1)
 
   421         ]);
 
   380         ]);
 
   422 
   381 
   423 
   382 
   424 qed_goal "defined_sinl" Ssum3.thy  
   383 Goal "x~=UU ==> sinl`x ~= UU";
 
   425         "x~=UU ==> sinl`x ~= UU"
 
   384 by (etac swap 1);
 
   426  (fn prems =>
 
   385 by (rtac inject_sinl 1);
 
   427         [
 
   386 by (stac strict_sinl 1);
 
   428         (cut_facts_tac prems 1),
 
   387 by (etac notnotD 1);
 
   429         (etac swap 1),
 
   388 qed "defined_sinl";
 
   430         (rtac inject_sinl 1),
 
   389 
   431         (stac strict_sinl 1),
 
   390 Goal "x~=UU ==> sinr`x ~= UU";
 
   432         (etac notnotD 1)
 
   391 by (etac swap 1);
 
   433         ]);
 
   392 by (rtac inject_sinr 1);
 
   434 
   393 by (stac strict_sinr 1);
 
   435 qed_goal "defined_sinr" Ssum3.thy  
   394 by (etac notnotD 1);
 
   436         "x~=UU ==> sinr`x ~= UU"
 
   395 qed "defined_sinr";
 
   437  (fn prems =>
 
       
   438         [
 
       
   439         (cut_facts_tac prems 1),
 
       
   440         (etac swap 1),
 
       
   441         (rtac inject_sinr 1),
 
       
   442         (stac strict_sinr 1),
 
       
   443         (etac notnotD 1)
 
       
   444         ]);
 
       
   445 
   396 
   446 qed_goalw "Exh_Ssum1" Ssum3.thy [sinl_def,sinr_def] 
   397 qed_goalw "Exh_Ssum1" Ssum3.thy [sinl_def,sinr_def] 
   447         "z=UU | (? a. z=sinl`a & a~=UU) | (? b. z=sinr`b & b~=UU)"
 
   398         "z=UU | (? a. z=sinl`a & a~=UU) | (? b. z=sinr`b & b~=UU)"
 
   448  (fn prems =>
 
   399  (fn prems =>
 
   449         [
 
   400         [
 
   663         (asm_simp_tac (Ssum0_ss addsimps 
   614         (asm_simp_tac (Ssum0_ss addsimps 
   664         [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
 
   615         [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
 
   665         cont_Iwhen3]) 1)
 
   616         cont_Iwhen3]) 1)
 
   666         ]);
 
   617         ]);
 
   667 
   618 
   668 qed_goal "thelub_ssum3" Ssum3.thy  
   619 Goal "chain(Y) ==>\ 
   669 "chain(Y) ==>\ 
       
   670 \   lub(range(Y)) = sinl`(lub(range(%i. sscase`(LAM x. x)`(LAM y. UU)`(Y i))))\
 
   620 \   lub(range(Y)) = sinl`(lub(range(%i. sscase`(LAM x. x)`(LAM y. UU)`(Y i))))\
 
   671 \ | lub(range(Y)) = sinr`(lub(range(%i. sscase`(LAM y. UU)`(LAM x. x)`(Y i))))"
 
   621 \ | lub(range(Y)) = sinr`(lub(range(%i. sscase`(LAM y. UU)`(LAM x. x)`(Y i))))";
 
   672  (fn prems =>
 
   622 by (rtac (ssum_chainE RS disjE) 1);
 
   673         [
 
   623 by (atac 1);
 
   674         (cut_facts_tac prems 1),
 
   624 by (rtac disjI1 1);
 
   675         (rtac (ssum_chainE RS disjE) 1),
 
   625 by (etac thelub_ssum2a 1);
 
   676         (atac 1),
 
   626 by (atac 1);
 
   677         (rtac disjI1 1),
 
   627 by (rtac disjI2 1);
 
   678         (etac thelub_ssum2a 1),
 
   628 by (etac thelub_ssum2b 1);
 
   679         (atac 1),
 
   629 by (atac 1);
 
   680         (rtac disjI2 1),
 
   630 qed "thelub_ssum3";
 
   681         (etac thelub_ssum2b 1),
 
   631 
   682         (atac 1)
 
   632 
   683         ]);
 
   633 Goal "sscase`sinl`sinr`z=z";
 
   684 
   634 by (res_inst_tac [("p","z")] ssumE 1);
 
   685 
   635 by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1);
 
   686 qed_goal "sscase4" Ssum3.thy  
   636 by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1);
 
   687         "sscase`sinl`sinr`z=z"
 
   637 by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1);
 
   688  (fn prems =>
 
   638 qed "sscase4";
 
   689         [
 
       
   690         (res_inst_tac [("p","z")] ssumE 1),
 
       
   691         (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1),
 
       
   692         (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1),
 
       
   693         (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sscase1,sscase2,sscase3]) 1)
 
       
   694         ]);
 
       
   695 
   639 
   696 
   640 
   697 (* ------------------------------------------------------------------------ *)
 
   641 (* ------------------------------------------------------------------------ *)
 
   698 (* install simplifier for Ssum                                              *)
 
   642 (* install simplifier for Ssum                                              *)
 
   699 (* ------------------------------------------------------------------------ *)
 
   643 (* ------------------------------------------------------------------------ *)
isabelle