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