src/HOLCF/ssum2.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 243 c22b85994e17
permissions -rw-r--r--
tidying
nipkow@243
     1
(*  Title: 	HOLCF/ssum2.ML
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
Lemmas for ssum2.thy
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Ssum2;
nipkow@243
    10
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
(* access to less_ssum in class po                                          *)
nipkow@243
    13
(* ------------------------------------------------------------------------ *)
nipkow@243
    14
nipkow@243
    15
val less_ssum3a = prove_goal Ssum2.thy 
nipkow@243
    16
	"(Isinl(x) << Isinl(y)) = (x << y)"
nipkow@243
    17
 (fn prems =>
nipkow@243
    18
	[
nipkow@243
    19
	(rtac (inst_ssum_po RS ssubst) 1),
nipkow@243
    20
	(rtac less_ssum2a 1)
nipkow@243
    21
	]);
nipkow@243
    22
nipkow@243
    23
val less_ssum3b = prove_goal Ssum2.thy 
nipkow@243
    24
	"(Isinr(x) << Isinr(y)) = (x << y)"
nipkow@243
    25
 (fn prems =>
nipkow@243
    26
	[
nipkow@243
    27
	(rtac (inst_ssum_po RS ssubst) 1),
nipkow@243
    28
	(rtac less_ssum2b 1)
nipkow@243
    29
	]);
nipkow@243
    30
nipkow@243
    31
val less_ssum3c = prove_goal Ssum2.thy 
nipkow@243
    32
	"(Isinl(x) << Isinr(y)) = (x = UU)"
nipkow@243
    33
 (fn prems =>
nipkow@243
    34
	[
nipkow@243
    35
	(rtac (inst_ssum_po RS ssubst) 1),
nipkow@243
    36
	(rtac less_ssum2c 1)
nipkow@243
    37
	]);
nipkow@243
    38
nipkow@243
    39
val less_ssum3d = prove_goal Ssum2.thy 
nipkow@243
    40
	"(Isinr(x) << Isinl(y)) = (x = UU)"
nipkow@243
    41
 (fn prems =>
nipkow@243
    42
	[
nipkow@243
    43
	(rtac (inst_ssum_po RS ssubst) 1),
nipkow@243
    44
	(rtac less_ssum2d 1)
nipkow@243
    45
	]);
nipkow@243
    46
nipkow@243
    47
nipkow@243
    48
(* ------------------------------------------------------------------------ *)
nipkow@243
    49
(* type ssum ++ is pointed                                                  *)
nipkow@243
    50
(* ------------------------------------------------------------------------ *)
nipkow@243
    51
nipkow@243
    52
val minimal_ssum = prove_goal Ssum2.thy "Isinl(UU) << s"
nipkow@243
    53
 (fn prems =>
nipkow@243
    54
	[
nipkow@243
    55
	(res_inst_tac [("p","s")] IssumE2 1),
nipkow@243
    56
	(hyp_subst_tac 1),
nipkow@243
    57
	(rtac (less_ssum3a RS iffD2) 1),
nipkow@243
    58
	(rtac minimal 1),
nipkow@243
    59
	(hyp_subst_tac 1),
nipkow@243
    60
	(rtac (strict_IsinlIsinr RS ssubst) 1),
nipkow@243
    61
	(rtac (less_ssum3b RS iffD2) 1),
nipkow@243
    62
	(rtac minimal 1)
nipkow@243
    63
	]);
nipkow@243
    64
nipkow@243
    65
nipkow@243
    66
(* ------------------------------------------------------------------------ *)
nipkow@243
    67
(* Isinl, Isinr are monotone                                                *)
nipkow@243
    68
(* ------------------------------------------------------------------------ *)
nipkow@243
    69
nipkow@243
    70
val monofun_Isinl = prove_goalw Ssum2.thy [monofun] "monofun(Isinl)"
nipkow@243
    71
 (fn prems =>
nipkow@243
    72
	[
nipkow@243
    73
	(strip_tac 1),
nipkow@243
    74
	(etac (less_ssum3a RS iffD2) 1)
nipkow@243
    75
	]);
nipkow@243
    76
nipkow@243
    77
val monofun_Isinr = prove_goalw Ssum2.thy [monofun] "monofun(Isinr)"
nipkow@243
    78
 (fn prems =>
nipkow@243
    79
	[
nipkow@243
    80
	(strip_tac 1),
nipkow@243
    81
	(etac (less_ssum3b RS iffD2) 1)
nipkow@243
    82
	]);
nipkow@243
    83
nipkow@243
    84
nipkow@243
    85
(* ------------------------------------------------------------------------ *)
nipkow@243
    86
(* Iwhen is monotone in all arguments                                       *)
nipkow@243
    87
(* ------------------------------------------------------------------------ *)
nipkow@243
    88
nipkow@243
    89
nipkow@243
    90
val monofun_Iwhen1 = prove_goalw Ssum2.thy [monofun] "monofun(Iwhen)"
nipkow@243
    91
 (fn prems =>
nipkow@243
    92
	[
nipkow@243
    93
	(strip_tac 1),
nipkow@243
    94
	(rtac (less_fun RS iffD2) 1),
nipkow@243
    95
	(strip_tac 1),
nipkow@243
    96
	(rtac (less_fun RS iffD2) 1),
nipkow@243
    97
	(strip_tac 1),
nipkow@243
    98
	(res_inst_tac [("p","xb")] IssumE 1),
nipkow@243
    99
	(hyp_subst_tac 1),
nipkow@243
   100
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   101
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   102
	(etac monofun_cfun_fun 1),
nipkow@243
   103
	(asm_simp_tac Ssum_ss 1)
nipkow@243
   104
	]);
nipkow@243
   105
nipkow@243
   106
val monofun_Iwhen2 = prove_goalw Ssum2.thy [monofun] "monofun(Iwhen(f))"
nipkow@243
   107
 (fn prems =>
nipkow@243
   108
	[
nipkow@243
   109
	(strip_tac 1),
nipkow@243
   110
	(rtac (less_fun RS iffD2) 1),
nipkow@243
   111
	(strip_tac 1),
nipkow@243
   112
	(res_inst_tac [("p","xa")] IssumE 1),
nipkow@243
   113
	(hyp_subst_tac 1),
nipkow@243
   114
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   115
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   116
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   117
	(etac monofun_cfun_fun 1)
nipkow@243
   118
	]);
nipkow@243
   119
nipkow@243
   120
val monofun_Iwhen3 = prove_goalw Ssum2.thy [monofun] "monofun(Iwhen(f)(g))"
nipkow@243
   121
 (fn prems =>
nipkow@243
   122
	[
nipkow@243
   123
	(strip_tac 1),
nipkow@243
   124
	(res_inst_tac [("p","x")] IssumE 1),
nipkow@243
   125
	(hyp_subst_tac 1),
nipkow@243
   126
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   127
	(hyp_subst_tac 1),
nipkow@243
   128
	(res_inst_tac [("p","y")] IssumE 1),
nipkow@243
   129
	(hyp_subst_tac 1),
nipkow@243
   130
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   131
	(res_inst_tac  [("P","xa=UU")] notE 1),
nipkow@243
   132
	(atac 1),
nipkow@243
   133
	(rtac UU_I 1),
nipkow@243
   134
	(rtac (less_ssum3a  RS iffD1) 1),
nipkow@243
   135
	(atac 1),
nipkow@243
   136
	(hyp_subst_tac 1),
nipkow@243
   137
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   138
	(rtac monofun_cfun_arg 1),
nipkow@243
   139
	(etac (less_ssum3a  RS iffD1) 1),
nipkow@243
   140
	(hyp_subst_tac 1),
nipkow@243
   141
	(res_inst_tac [("s","UU"),("t","xa")] subst 1),
nipkow@243
   142
	(etac (less_ssum3c  RS iffD1 RS sym) 1),
nipkow@243
   143
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   144
	(hyp_subst_tac 1),
nipkow@243
   145
	(res_inst_tac [("p","y")] IssumE 1),
nipkow@243
   146
	(hyp_subst_tac 1),
nipkow@243
   147
	(res_inst_tac [("s","UU"),("t","ya")] subst 1),
nipkow@243
   148
	(etac (less_ssum3d  RS iffD1 RS sym) 1),
nipkow@243
   149
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   150
	(hyp_subst_tac 1),
nipkow@243
   151
	(res_inst_tac [("s","UU"),("t","ya")] subst 1),
nipkow@243
   152
	(etac (less_ssum3d  RS iffD1 RS sym) 1),
nipkow@243
   153
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   154
	(hyp_subst_tac 1),
nipkow@243
   155
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   156
	(rtac monofun_cfun_arg 1),
nipkow@243
   157
	(etac (less_ssum3b  RS iffD1) 1)
nipkow@243
   158
	]);
nipkow@243
   159
nipkow@243
   160
nipkow@243
   161
nipkow@243
   162
nipkow@243
   163
(* ------------------------------------------------------------------------ *)
nipkow@243
   164
(* some kind of exhaustion rules for chains in 'a ++ 'b                     *)
nipkow@243
   165
(* ------------------------------------------------------------------------ *)
nipkow@243
   166
nipkow@243
   167
nipkow@243
   168
val ssum_lemma1 = prove_goal Ssum2.thy 
nipkow@243
   169
"[|~(!i.? x.Y(i::nat)=Isinl(x))|] ==> (? i.! x.~Y(i)=Isinl(x))"
nipkow@243
   170
 (fn prems =>
nipkow@243
   171
	[
nipkow@243
   172
	(cut_facts_tac prems 1),
nipkow@243
   173
	(fast_tac HOL_cs 1)
nipkow@243
   174
	]);
nipkow@243
   175
nipkow@243
   176
val ssum_lemma2 = prove_goal Ssum2.thy 
nipkow@243
   177
"[|(? i.!x.~(Y::nat => 'a++'b)(i::nat)=Isinl(x::'a))|] ==>\
nipkow@243
   178
\   (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & ~y=UU)"
nipkow@243
   179
 (fn prems =>
nipkow@243
   180
	[
nipkow@243
   181
	(cut_facts_tac prems 1),
nipkow@243
   182
	(etac exE 1),
nipkow@243
   183
	(res_inst_tac [("p","Y(i)")] IssumE 1),
nipkow@243
   184
	(dtac spec 1),
nipkow@243
   185
	(contr_tac 1),
nipkow@243
   186
	(dtac spec 1),
nipkow@243
   187
	(contr_tac 1),
nipkow@243
   188
	(fast_tac HOL_cs 1)
nipkow@243
   189
	]);
nipkow@243
   190
nipkow@243
   191
nipkow@243
   192
val ssum_lemma3 = prove_goal Ssum2.thy 
nipkow@243
   193
"[|is_chain(Y);(? i x. Y(i)=Isinr(x) & ~x=UU)|] ==> (!i.? y.Y(i)=Isinr(y))"
nipkow@243
   194
 (fn prems =>
nipkow@243
   195
	[
nipkow@243
   196
	(cut_facts_tac prems 1),
nipkow@243
   197
	(etac exE 1),
nipkow@243
   198
	(etac exE 1),
nipkow@243
   199
	(rtac allI 1),
nipkow@243
   200
	(res_inst_tac [("p","Y(ia)")] IssumE 1),
nipkow@243
   201
	(rtac exI 1),
nipkow@243
   202
	(rtac trans 1),
nipkow@243
   203
	(rtac strict_IsinlIsinr 2),
nipkow@243
   204
	(atac 1),
nipkow@243
   205
	(etac exI 2),
nipkow@243
   206
	(etac conjE 1),
nipkow@243
   207
	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
nipkow@243
   208
	(hyp_subst_tac 2),
nipkow@243
   209
	(etac exI 2),
nipkow@243
   210
	(res_inst_tac [("P","x=UU")] notE 1),
nipkow@243
   211
	(atac 1),
nipkow@243
   212
	(rtac (less_ssum3d RS iffD1) 1),
nipkow@243
   213
	(res_inst_tac [("s","Y(i)"),("t","Isinr(x)")] subst 1),
nipkow@243
   214
	(atac 1),
nipkow@243
   215
	(res_inst_tac [("s","Y(ia)"),("t","Isinl(xa)")] subst 1),
nipkow@243
   216
	(atac 1),
nipkow@243
   217
	(etac (chain_mono RS mp) 1),
nipkow@243
   218
	(atac 1),
nipkow@243
   219
	(res_inst_tac [("P","xa=UU")] notE 1),
nipkow@243
   220
	(atac 1),
nipkow@243
   221
	(rtac (less_ssum3c RS iffD1) 1),
nipkow@243
   222
	(res_inst_tac [("s","Y(i)"),("t","Isinr(x)")] subst 1),
nipkow@243
   223
	(atac 1),
nipkow@243
   224
	(res_inst_tac [("s","Y(ia)"),("t","Isinl(xa)")] subst 1),
nipkow@243
   225
	(atac 1),
nipkow@243
   226
	(etac (chain_mono RS mp) 1),
nipkow@243
   227
	(atac 1)
nipkow@243
   228
	]);
nipkow@243
   229
nipkow@243
   230
val ssum_lemma4 = prove_goal Ssum2.thy 
nipkow@243
   231
"is_chain(Y) ==> (!i.? x.Y(i)=Isinl(x))|(!i.? y.Y(i)=Isinr(y))"
nipkow@243
   232
 (fn prems =>
nipkow@243
   233
	[
nipkow@243
   234
	(cut_facts_tac prems 1),
nipkow@243
   235
	(rtac classical2 1),
nipkow@243
   236
	(etac disjI1 1),
nipkow@243
   237
	(rtac disjI2 1),
nipkow@243
   238
	(etac ssum_lemma3 1),
nipkow@243
   239
	(rtac ssum_lemma2 1),
nipkow@243
   240
	(etac ssum_lemma1 1)
nipkow@243
   241
	]);
nipkow@243
   242
nipkow@243
   243
nipkow@243
   244
(* ------------------------------------------------------------------------ *)
nipkow@243
   245
(* restricted surjectivity of Isinl                                         *)
nipkow@243
   246
(* ------------------------------------------------------------------------ *)
nipkow@243
   247
nipkow@243
   248
val ssum_lemma5 = prove_goal Ssum2.thy 
nipkow@243
   249
"z=Isinl(x)==> Isinl((Iwhen (LAM x.x) (LAM y.UU))(z)) = z"
nipkow@243
   250
 (fn prems =>
nipkow@243
   251
	[
nipkow@243
   252
	(cut_facts_tac prems 1),
nipkow@243
   253
	(hyp_subst_tac 1),
nipkow@243
   254
	(res_inst_tac [("Q","x=UU")] classical2 1),
nipkow@243
   255
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   256
	(asm_simp_tac Ssum_ss 1)
nipkow@243
   257
	]);
nipkow@243
   258
nipkow@243
   259
(* ------------------------------------------------------------------------ *)
nipkow@243
   260
(* restricted surjectivity of Isinr                                         *)
nipkow@243
   261
(* ------------------------------------------------------------------------ *)
nipkow@243
   262
nipkow@243
   263
val ssum_lemma6 = prove_goal Ssum2.thy 
nipkow@243
   264
"z=Isinr(x)==> Isinr((Iwhen (LAM y.UU) (LAM x.x))(z)) = z"
nipkow@243
   265
 (fn prems =>
nipkow@243
   266
	[
nipkow@243
   267
	(cut_facts_tac prems 1),
nipkow@243
   268
	(hyp_subst_tac 1),
nipkow@243
   269
	(res_inst_tac [("Q","x=UU")] classical2 1),
nipkow@243
   270
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   271
	(asm_simp_tac Ssum_ss 1)
nipkow@243
   272
	]);
nipkow@243
   273
nipkow@243
   274
(* ------------------------------------------------------------------------ *)
nipkow@243
   275
(* technical lemmas                                                         *)
nipkow@243
   276
(* ------------------------------------------------------------------------ *)
nipkow@243
   277
nipkow@243
   278
val ssum_lemma7 = prove_goal Ssum2.thy 
nipkow@243
   279
"[|Isinl(x) << z; ~x=UU|] ==> ? y.z=Isinl(y) & ~y=UU"
nipkow@243
   280
 (fn prems =>
nipkow@243
   281
	[
nipkow@243
   282
	(cut_facts_tac prems 1),
nipkow@243
   283
	(res_inst_tac [("p","z")] IssumE 1),
nipkow@243
   284
	(hyp_subst_tac 1),
nipkow@243
   285
	(etac notE 1),
nipkow@243
   286
	(rtac antisym_less 1),
nipkow@243
   287
	(etac (less_ssum3a RS iffD1) 1),
nipkow@243
   288
	(rtac minimal 1),
nipkow@243
   289
	(fast_tac HOL_cs 1),
nipkow@243
   290
	(hyp_subst_tac 1),
nipkow@243
   291
	(rtac notE 1),
nipkow@243
   292
	(etac (less_ssum3c RS iffD1) 2),
nipkow@243
   293
	(atac 1)
nipkow@243
   294
	]);
nipkow@243
   295
nipkow@243
   296
val ssum_lemma8 = prove_goal Ssum2.thy 
nipkow@243
   297
"[|Isinr(x) << z; ~x=UU|] ==> ? y.z=Isinr(y) & ~y=UU"
nipkow@243
   298
 (fn prems =>
nipkow@243
   299
	[
nipkow@243
   300
	(cut_facts_tac prems 1),
nipkow@243
   301
	(res_inst_tac [("p","z")] IssumE 1),
nipkow@243
   302
	(hyp_subst_tac 1),
nipkow@243
   303
	(etac notE 1),
nipkow@243
   304
	(etac (less_ssum3d RS iffD1) 1),
nipkow@243
   305
	(hyp_subst_tac 1),
nipkow@243
   306
	(rtac notE 1),
nipkow@243
   307
	(etac (less_ssum3d RS iffD1) 2),
nipkow@243
   308
	(atac 1),
nipkow@243
   309
	(fast_tac HOL_cs 1)
nipkow@243
   310
	]);
nipkow@243
   311
nipkow@243
   312
(* ------------------------------------------------------------------------ *)
nipkow@243
   313
(* the type 'a ++ 'b is a cpo in three steps                                *)
nipkow@243
   314
(* ------------------------------------------------------------------------ *)
nipkow@243
   315
nipkow@243
   316
val lub_ssum1a = prove_goal Ssum2.thy 
nipkow@243
   317
"[|is_chain(Y);(!i.? x.Y(i)=Isinl(x))|] ==>\
nipkow@243
   318
\ range(Y) <<|\
nipkow@243
   319
\ Isinl(lub(range(%i.(Iwhen (LAM x.x) (LAM y.UU))(Y(i)))))"
nipkow@243
   320
 (fn prems =>
nipkow@243
   321
	[
nipkow@243
   322
	(cut_facts_tac prems 1),
nipkow@243
   323
	(rtac is_lubI 1),
nipkow@243
   324
	(rtac conjI 1),
nipkow@243
   325
	(rtac ub_rangeI 1),
nipkow@243
   326
	(rtac allI 1),
nipkow@243
   327
	(etac allE 1),
nipkow@243
   328
	(etac exE 1),
nipkow@243
   329
	(res_inst_tac [("t","Y(i)")] (ssum_lemma5 RS subst) 1),
nipkow@243
   330
	(atac 1),
nipkow@243
   331
	(rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1),
nipkow@243
   332
	(rtac is_ub_thelub 1),
nipkow@243
   333
	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
nipkow@243
   334
	(strip_tac 1),
nipkow@243
   335
	(res_inst_tac [("p","u")] IssumE2 1),
nipkow@243
   336
	(res_inst_tac [("t","u")] (ssum_lemma5 RS subst) 1),
nipkow@243
   337
	(atac 1),
nipkow@243
   338
	(rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1),
nipkow@243
   339
	(rtac is_lub_thelub 1),
nipkow@243
   340
	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
nipkow@243
   341
	(etac (monofun_Iwhen3 RS ub2ub_monofun) 1),
nipkow@243
   342
	(hyp_subst_tac 1),
nipkow@243
   343
	(rtac (less_ssum3c RS iffD2) 1),
nipkow@243
   344
	(rtac chain_UU_I_inverse 1),
nipkow@243
   345
	(rtac allI 1),
nipkow@243
   346
	(res_inst_tac [("p","Y(i)")] IssumE 1),
nipkow@243
   347
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   348
	(asm_simp_tac Ssum_ss 2),
nipkow@243
   349
	(etac notE 1),
nipkow@243
   350
	(rtac (less_ssum3c RS iffD1) 1),
nipkow@243
   351
	(res_inst_tac [("t","Isinl(x)")] subst 1),
nipkow@243
   352
	(atac 1),
nipkow@243
   353
	(etac (ub_rangeE RS spec) 1)
nipkow@243
   354
	]);
nipkow@243
   355
nipkow@243
   356
nipkow@243
   357
val lub_ssum1b = prove_goal Ssum2.thy 
nipkow@243
   358
"[|is_chain(Y);(!i.? x.Y(i)=Isinr(x))|] ==>\
nipkow@243
   359
\ range(Y) <<|\
nipkow@243
   360
\ Isinr(lub(range(%i.(Iwhen (LAM y.UU) (LAM x.x))(Y(i)))))"
nipkow@243
   361
 (fn prems =>
nipkow@243
   362
	[
nipkow@243
   363
	(cut_facts_tac prems 1),
nipkow@243
   364
	(rtac is_lubI 1),
nipkow@243
   365
	(rtac conjI 1),
nipkow@243
   366
	(rtac ub_rangeI 1),
nipkow@243
   367
	(rtac allI 1),
nipkow@243
   368
	(etac allE 1),
nipkow@243
   369
	(etac exE 1),
nipkow@243
   370
	(res_inst_tac [("t","Y(i)")] (ssum_lemma6 RS subst) 1),
nipkow@243
   371
	(atac 1),
nipkow@243
   372
	(rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1),
nipkow@243
   373
	(rtac is_ub_thelub 1),
nipkow@243
   374
	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
nipkow@243
   375
	(strip_tac 1),
nipkow@243
   376
	(res_inst_tac [("p","u")] IssumE2 1),
nipkow@243
   377
	(hyp_subst_tac 1),
nipkow@243
   378
	(rtac (less_ssum3d RS iffD2) 1),
nipkow@243
   379
	(rtac chain_UU_I_inverse 1),
nipkow@243
   380
	(rtac allI 1),
nipkow@243
   381
	(res_inst_tac [("p","Y(i)")] IssumE 1),
nipkow@243
   382
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   383
	(asm_simp_tac Ssum_ss 1),
nipkow@243
   384
	(etac notE 1),
nipkow@243
   385
	(rtac (less_ssum3d RS iffD1) 1),
nipkow@243
   386
	(res_inst_tac [("t","Isinr(y)")] subst 1),
nipkow@243
   387
	(atac 1),
nipkow@243
   388
	(etac (ub_rangeE RS spec) 1),
nipkow@243
   389
	(res_inst_tac [("t","u")] (ssum_lemma6 RS subst) 1),
nipkow@243
   390
	(atac 1),
nipkow@243
   391
	(rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1),
nipkow@243
   392
	(rtac is_lub_thelub 1),
nipkow@243
   393
	(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
nipkow@243
   394
	(etac (monofun_Iwhen3 RS ub2ub_monofun) 1)
nipkow@243
   395
	]);
nipkow@243
   396
nipkow@243
   397
nipkow@243
   398
val thelub_ssum1a = lub_ssum1a RS thelubI;
nipkow@243
   399
(* [| is_chain(?Y1); ! i. ? x. ?Y1(i) = Isinl(x) |] ==>                     *)
nipkow@243
   400
(* lub(range(?Y1)) = Isinl(lub(range(%i. Iwhen(LAM x. x,LAM y. UU,?Y1(i)))))*)
nipkow@243
   401
nipkow@243
   402
val thelub_ssum1b = lub_ssum1b RS thelubI;
nipkow@243
   403
(* [| is_chain(?Y1); ! i. ? x. ?Y1(i) = Isinr(x) |] ==>                     *)
nipkow@243
   404
(* lub(range(?Y1)) = Isinr(lub(range(%i. Iwhen(LAM y. UU,LAM x. x,?Y1(i)))))*)
nipkow@243
   405
nipkow@243
   406
val cpo_ssum = prove_goal Ssum2.thy 
nipkow@243
   407
	"is_chain(Y::nat=>'a ++'b) ==> ? x.range(Y) <<|x"
nipkow@243
   408
 (fn prems =>
nipkow@243
   409
	[
nipkow@243
   410
	(cut_facts_tac prems 1),
nipkow@243
   411
	(rtac (ssum_lemma4 RS disjE) 1),
nipkow@243
   412
	(atac 1),
nipkow@243
   413
	(rtac exI 1),
nipkow@243
   414
	(etac lub_ssum1a 1),
nipkow@243
   415
	(atac 1),
nipkow@243
   416
	(rtac exI 1),
nipkow@243
   417
	(etac lub_ssum1b 1),
nipkow@243
   418
	(atac 1)
nipkow@243
   419
	]);