src/HOLCF/cont.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/cont.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 cont.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Cont;
nipkow@243
    10
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
(* access to definition                                                     *)
nipkow@243
    13
(* ------------------------------------------------------------------------ *)
nipkow@243
    14
nipkow@243
    15
val contlubI = prove_goalw Cont.thy [contlub]
nipkow@243
    16
	"! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
nipkow@243
    17
\	 contlub(f)"
nipkow@243
    18
(fn prems =>
nipkow@243
    19
	[
nipkow@243
    20
	(cut_facts_tac prems 1),
nipkow@243
    21
	(atac 1)
nipkow@243
    22
	]);
nipkow@243
    23
nipkow@243
    24
val contlubE = prove_goalw Cont.thy [contlub]
nipkow@243
    25
	" contlub(f)==>\
nipkow@243
    26
\         ! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
nipkow@243
    27
(fn prems =>
nipkow@243
    28
	[
nipkow@243
    29
	(cut_facts_tac prems 1),
nipkow@243
    30
	(atac 1)
nipkow@243
    31
	]);
nipkow@243
    32
nipkow@243
    33
nipkow@243
    34
val contXI = prove_goalw Cont.thy [contX]
nipkow@243
    35
 "! Y. is_chain(Y) --> range(% i.f(Y(i))) <<| f(lub(range(Y))) ==> contX(f)"
nipkow@243
    36
(fn prems =>
nipkow@243
    37
	[
nipkow@243
    38
	(cut_facts_tac prems 1),
nipkow@243
    39
	(atac 1)
nipkow@243
    40
	]);
nipkow@243
    41
nipkow@243
    42
val contXE = prove_goalw Cont.thy [contX]
nipkow@243
    43
 "contX(f) ==> ! Y. is_chain(Y) --> range(% i.f(Y(i))) <<| f(lub(range(Y)))"
nipkow@243
    44
(fn prems =>
nipkow@243
    45
	[
nipkow@243
    46
	(cut_facts_tac prems 1),
nipkow@243
    47
	(atac 1)
nipkow@243
    48
	]);
nipkow@243
    49
nipkow@243
    50
nipkow@243
    51
val monofunI = prove_goalw Cont.thy [monofun]
nipkow@243
    52
	"! x y. x << y --> f(x) << f(y) ==> monofun(f)"
nipkow@243
    53
(fn prems =>
nipkow@243
    54
	[
nipkow@243
    55
	(cut_facts_tac prems 1),
nipkow@243
    56
	(atac 1)
nipkow@243
    57
	]);
nipkow@243
    58
nipkow@243
    59
val monofunE = prove_goalw Cont.thy [monofun]
nipkow@243
    60
	"monofun(f) ==> ! x y. x << y --> f(x) << f(y)"
nipkow@243
    61
(fn prems =>
nipkow@243
    62
	[
nipkow@243
    63
	(cut_facts_tac prems 1),
nipkow@243
    64
	(atac 1)
nipkow@243
    65
	]);
nipkow@243
    66
nipkow@243
    67
(* ------------------------------------------------------------------------ *)
nipkow@243
    68
(* the main purpose of cont.thy is to show:                                 *)
nipkow@243
    69
(*              monofun(f) & contlub(f)  <==> contX(f)                      *)
nipkow@243
    70
(* ------------------------------------------------------------------------ *)
nipkow@243
    71
nipkow@243
    72
(* ------------------------------------------------------------------------ *)
nipkow@243
    73
(* monotone functions map chains to chains                                  *)
nipkow@243
    74
(* ------------------------------------------------------------------------ *)
nipkow@243
    75
nipkow@243
    76
val ch2ch_monofun= prove_goal Cont.thy 
nipkow@243
    77
	"[| monofun(f); is_chain(Y) |] ==> is_chain(%i. f(Y(i)))"
nipkow@243
    78
(fn prems =>
nipkow@243
    79
	[
nipkow@243
    80
	(cut_facts_tac prems 1),
nipkow@243
    81
	(rtac is_chainI 1),
nipkow@243
    82
	(rtac allI 1),
nipkow@243
    83
	(etac (monofunE RS spec RS spec RS mp) 1),
nipkow@243
    84
	(etac (is_chainE RS spec) 1)
nipkow@243
    85
	]);
nipkow@243
    86
nipkow@243
    87
(* ------------------------------------------------------------------------ *)
nipkow@243
    88
(* monotone functions map upper bound to upper bounds                       *)
nipkow@243
    89
(* ------------------------------------------------------------------------ *)
nipkow@243
    90
nipkow@243
    91
val ub2ub_monofun = prove_goal Cont.thy 
nipkow@243
    92
 "[| monofun(f); range(Y) <| u|]  ==> range(%i.f(Y(i))) <| f(u)"
nipkow@243
    93
(fn prems =>
nipkow@243
    94
	[
nipkow@243
    95
	(cut_facts_tac prems 1),
nipkow@243
    96
	(rtac ub_rangeI 1),
nipkow@243
    97
	(rtac allI 1),
nipkow@243
    98
	(etac (monofunE RS spec RS spec RS mp) 1),
nipkow@243
    99
	(etac (ub_rangeE RS spec) 1)
nipkow@243
   100
	]);
nipkow@243
   101
nipkow@243
   102
(* ------------------------------------------------------------------------ *)
nipkow@243
   103
(* left to right: monofun(f) & contlub(f)  ==> contX(f)                     *)
nipkow@243
   104
(* ------------------------------------------------------------------------ *)
nipkow@243
   105
nipkow@243
   106
val monocontlub2contX = prove_goalw Cont.thy [contX]
nipkow@243
   107
	"[|monofun(f);contlub(f)|] ==> contX(f)"
nipkow@243
   108
(fn prems =>
nipkow@243
   109
	[
nipkow@243
   110
	(cut_facts_tac prems 1),
nipkow@243
   111
	(strip_tac 1),
nipkow@243
   112
	(rtac thelubE 1),
nipkow@243
   113
	(etac ch2ch_monofun 1),
nipkow@243
   114
	(atac 1),
nipkow@243
   115
	(etac (contlubE RS spec RS mp RS sym) 1),
nipkow@243
   116
	(atac 1)
nipkow@243
   117
	]);
nipkow@243
   118
nipkow@243
   119
(* ------------------------------------------------------------------------ *)
nipkow@243
   120
(* first a lemma about binary chains                                        *)
nipkow@243
   121
(* ------------------------------------------------------------------------ *)
nipkow@243
   122
nipkow@243
   123
val binchain_contX =  prove_goal Cont.thy
nipkow@243
   124
"[| contX(f); x << y |]  ==> range(%i. f(if(i = 0,x,y))) <<| f(y)"
nipkow@243
   125
(fn prems => 
nipkow@243
   126
	[
nipkow@243
   127
	(cut_facts_tac prems 1),
nipkow@243
   128
	(rtac subst 1), 
nipkow@243
   129
	(etac (contXE RS spec RS mp) 2),
nipkow@243
   130
	(etac bin_chain 2),
nipkow@243
   131
	(res_inst_tac [("y","y")] arg_cong 1),
nipkow@243
   132
	(etac (lub_bin_chain RS thelubI) 1)
nipkow@243
   133
	]);
nipkow@243
   134
nipkow@243
   135
(* ------------------------------------------------------------------------ *)
nipkow@243
   136
(* right to left: contX(f) ==> monofun(f) & contlub(f)                      *)
nipkow@243
   137
(* part1:         contX(f) ==> monofun(f                                    *)
nipkow@243
   138
(* ------------------------------------------------------------------------ *)
nipkow@243
   139
nipkow@243
   140
val contX2mono =  prove_goalw Cont.thy [monofun]
nipkow@243
   141
	"contX(f) ==> monofun(f)"
nipkow@243
   142
(fn prems =>
nipkow@243
   143
	[
nipkow@243
   144
	(cut_facts_tac prems 1),
nipkow@243
   145
	(strip_tac 1),
nipkow@243
   146
	(res_inst_tac [("s","if(0 = 0,x,y)")] subst 1),
nipkow@243
   147
	(rtac (binchain_contX RS is_ub_lub) 2),
nipkow@243
   148
	(atac 2),
nipkow@243
   149
	(atac 2),
nipkow@243
   150
	(simp_tac nat_ss 1)
nipkow@243
   151
	]);
nipkow@243
   152
nipkow@243
   153
(* ------------------------------------------------------------------------ *)
nipkow@243
   154
(* right to left: contX(f) ==> monofun(f) & contlub(f)                      *)
nipkow@243
   155
(* part2:         contX(f) ==>              contlub(f)                      *)
nipkow@243
   156
(* ------------------------------------------------------------------------ *)
nipkow@243
   157
nipkow@243
   158
val contX2contlub = prove_goalw Cont.thy [contlub]
nipkow@243
   159
	"contX(f) ==> contlub(f)"
nipkow@243
   160
(fn prems =>
nipkow@243
   161
	[
nipkow@243
   162
	(cut_facts_tac prems 1),
nipkow@243
   163
	(strip_tac 1),
nipkow@243
   164
	(rtac (thelubI RS sym) 1),
nipkow@243
   165
	(etac (contXE RS spec RS mp) 1),
nipkow@243
   166
	(atac 1)
nipkow@243
   167
	]);
nipkow@243
   168
nipkow@243
   169
(* ------------------------------------------------------------------------ *)
nipkow@243
   170
(* The following results are about a curried function that is monotone      *)
nipkow@243
   171
(* in both arguments                                                        *)
nipkow@243
   172
(* ------------------------------------------------------------------------ *)
nipkow@243
   173
nipkow@243
   174
val ch2ch_MF2L = prove_goal Cont.thy 
nipkow@243
   175
"[|monofun(MF2::('a::po=>'b::po=>'c::po));\
nipkow@243
   176
\	is_chain(F)|] ==> is_chain(%i. MF2(F(i),x))"
nipkow@243
   177
(fn prems =>
nipkow@243
   178
	[
nipkow@243
   179
	(cut_facts_tac prems 1),
nipkow@243
   180
	(etac (ch2ch_monofun RS ch2ch_fun) 1),
nipkow@243
   181
	(atac 1)
nipkow@243
   182
	]);
nipkow@243
   183
nipkow@243
   184
nipkow@243
   185
val ch2ch_MF2R = prove_goal Cont.thy "[|monofun(MF2(f)::('b::po=>'c::po));\
nipkow@243
   186
\	is_chain(Y)|] ==> is_chain(%i. MF2(f,Y(i)))"
nipkow@243
   187
(fn prems =>
nipkow@243
   188
	[
nipkow@243
   189
	(cut_facts_tac prems 1),
nipkow@243
   190
	(etac ch2ch_monofun 1),
nipkow@243
   191
	(atac 1)
nipkow@243
   192
	]);
nipkow@243
   193
nipkow@243
   194
val ch2ch_MF2LR = prove_goal Cont.thy 
nipkow@243
   195
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
nipkow@243
   196
\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
nipkow@243
   197
\	is_chain(F); is_chain(Y)|] ==> \
nipkow@243
   198
\  is_chain(%i. MF2(F(i))(Y(i)))"
nipkow@243
   199
(fn prems =>
nipkow@243
   200
	[
nipkow@243
   201
	(cut_facts_tac prems 1),
nipkow@243
   202
	(rtac is_chainI 1),
nipkow@243
   203
	(strip_tac 1 ),
nipkow@243
   204
	(rtac trans_less 1),
nipkow@243
   205
	(etac (ch2ch_MF2L RS is_chainE RS spec) 1),
nipkow@243
   206
	(atac 1),
nipkow@243
   207
	((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
nipkow@243
   208
	(etac (is_chainE RS spec) 1)
nipkow@243
   209
	]);
nipkow@243
   210
nipkow@243
   211
val ch2ch_lubMF2R = prove_goal Cont.thy 
nipkow@243
   212
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
nipkow@243
   213
\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
nipkow@243
   214
\	is_chain(F);is_chain(Y)|] ==> \
nipkow@243
   215
\	is_chain(%j. lub(range(%i. MF2(F(j),Y(i)))))"
nipkow@243
   216
(fn prems =>
nipkow@243
   217
	[
nipkow@243
   218
	(cut_facts_tac prems 1),
nipkow@243
   219
	(rtac (lub_mono RS allI RS is_chainI) 1),
nipkow@243
   220
	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
nipkow@243
   221
	(atac 1),
nipkow@243
   222
	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
nipkow@243
   223
	(atac 1),
nipkow@243
   224
	(strip_tac 1),
nipkow@243
   225
	(rtac (is_chainE RS spec) 1),
nipkow@243
   226
	(etac ch2ch_MF2L 1),
nipkow@243
   227
	(atac 1)
nipkow@243
   228
	]);
nipkow@243
   229
nipkow@243
   230
nipkow@243
   231
val ch2ch_lubMF2L = prove_goal Cont.thy 
nipkow@243
   232
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
nipkow@243
   233
\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
nipkow@243
   234
\	is_chain(F);is_chain(Y)|] ==> \
nipkow@243
   235
\	is_chain(%i. lub(range(%j. MF2(F(j),Y(i)))))"
nipkow@243
   236
(fn prems =>
nipkow@243
   237
	[
nipkow@243
   238
	(cut_facts_tac prems 1),
nipkow@243
   239
	(rtac (lub_mono RS allI RS is_chainI) 1),
nipkow@243
   240
	(etac ch2ch_MF2L 1),
nipkow@243
   241
	(atac 1),
nipkow@243
   242
	(etac ch2ch_MF2L 1),
nipkow@243
   243
	(atac 1),
nipkow@243
   244
	(strip_tac 1),
nipkow@243
   245
	(rtac (is_chainE RS spec) 1),
nipkow@243
   246
	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
nipkow@243
   247
	(atac 1)
nipkow@243
   248
	]);
nipkow@243
   249
nipkow@243
   250
nipkow@243
   251
val lub_MF2_mono = prove_goal Cont.thy 
nipkow@243
   252
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
nipkow@243
   253
\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
nipkow@243
   254
\	is_chain(F)|] ==> \
nipkow@243
   255
\	monofun(% x.lub(range(% j.MF2(F(j),x))))"
nipkow@243
   256
(fn prems =>
nipkow@243
   257
	[
nipkow@243
   258
	(cut_facts_tac prems 1),
nipkow@243
   259
	(rtac monofunI 1),
nipkow@243
   260
	(strip_tac 1),
nipkow@243
   261
	(rtac lub_mono 1),
nipkow@243
   262
	(etac ch2ch_MF2L 1),
nipkow@243
   263
	(atac 1),
nipkow@243
   264
	(etac ch2ch_MF2L 1),
nipkow@243
   265
	(atac 1),
nipkow@243
   266
	(strip_tac 1),
nipkow@243
   267
	((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
nipkow@243
   268
	(atac 1)
nipkow@243
   269
	]);
nipkow@243
   270
nipkow@243
   271
nipkow@243
   272
val ex_lubMF2 = prove_goal Cont.thy 
nipkow@243
   273
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
nipkow@243
   274
\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
nipkow@243
   275
\	is_chain(F); is_chain(Y)|] ==> \
nipkow@243
   276
\		lub(range(%j. lub(range(%i. MF2(F(j),Y(i)))))) =\
nipkow@243
   277
\		lub(range(%i. lub(range(%j. MF2(F(j),Y(i))))))"
nipkow@243
   278
(fn prems =>
nipkow@243
   279
	[
nipkow@243
   280
	(cut_facts_tac prems 1),
nipkow@243
   281
	(rtac antisym_less 1),
nipkow@243
   282
	(rtac is_lub_thelub 1),
nipkow@243
   283
	(etac ch2ch_lubMF2R 1),
nipkow@243
   284
	(atac 1),(atac 1),(atac 1),
nipkow@243
   285
	(rtac ub_rangeI 1),
nipkow@243
   286
	(strip_tac 1),
nipkow@243
   287
	(rtac lub_mono 1),
nipkow@243
   288
	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
nipkow@243
   289
	(atac 1),
nipkow@243
   290
	(etac ch2ch_lubMF2L 1),
nipkow@243
   291
	(atac 1),(atac 1),(atac 1),
nipkow@243
   292
	(strip_tac 1),
nipkow@243
   293
	(rtac is_ub_thelub 1),
nipkow@243
   294
	(etac ch2ch_MF2L 1),(atac 1),
nipkow@243
   295
	(rtac is_lub_thelub 1),
nipkow@243
   296
	(etac ch2ch_lubMF2L 1),
nipkow@243
   297
	(atac 1),(atac 1),(atac 1),
nipkow@243
   298
	(rtac ub_rangeI 1),
nipkow@243
   299
	(strip_tac 1),
nipkow@243
   300
	(rtac lub_mono 1),
nipkow@243
   301
	(etac ch2ch_MF2L 1),(atac 1),
nipkow@243
   302
	(etac ch2ch_lubMF2R 1),
nipkow@243
   303
	(atac 1),(atac 1),(atac 1),
nipkow@243
   304
	(strip_tac 1),
nipkow@243
   305
	(rtac is_ub_thelub 1),
nipkow@243
   306
	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
nipkow@243
   307
	(atac 1)
nipkow@243
   308
	]);
nipkow@243
   309
nipkow@243
   310
(* ------------------------------------------------------------------------ *)
nipkow@243
   311
(* The following results are about a curried function that is continuous    *)
nipkow@243
   312
(* in both arguments                                                        *)
nipkow@243
   313
(* ------------------------------------------------------------------------ *)
nipkow@243
   314
nipkow@243
   315
val diag_lubCF2_1 = prove_goal Cont.thy 
nipkow@243
   316
"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
nipkow@243
   317
\ lub(range(%i. lub(range(%j. CF2(FY(j))(TY(i)))))) =\
nipkow@243
   318
\ lub(range(%i. CF2(FY(i))(TY(i))))"
nipkow@243
   319
(fn prems =>
nipkow@243
   320
	[
nipkow@243
   321
	(cut_facts_tac prems 1),
nipkow@243
   322
	(rtac antisym_less 1),
nipkow@243
   323
	(rtac is_lub_thelub 1),
nipkow@243
   324
	(rtac ch2ch_lubMF2L 1),
nipkow@243
   325
	(rtac contX2mono 1),
nipkow@243
   326
	(atac 1),
nipkow@243
   327
	(rtac allI 1),
nipkow@243
   328
	(rtac contX2mono 1),
nipkow@243
   329
	(etac spec 1),
nipkow@243
   330
	(atac 1),
nipkow@243
   331
	(atac 1),
nipkow@243
   332
	(rtac ub_rangeI 1),
nipkow@243
   333
	(strip_tac 1 ),
nipkow@243
   334
	(rtac is_lub_thelub 1),
nipkow@243
   335
	((rtac ch2ch_MF2L 1) THEN (rtac contX2mono 1) THEN (atac 1)),
nipkow@243
   336
	(atac 1),
nipkow@243
   337
	(rtac ub_rangeI 1),
nipkow@243
   338
	(strip_tac 1 ),
nipkow@243
   339
	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
nipkow@243
   340
	(rtac trans_less 1),
nipkow@243
   341
	(rtac is_ub_thelub 2),
nipkow@243
   342
	(rtac (chain_mono RS mp) 1),
nipkow@243
   343
	((rtac ch2ch_MF2R 1) THEN (rtac contX2mono 1) THEN (etac spec 1)),
nipkow@243
   344
	(atac 1),
nipkow@243
   345
	(atac 1),
nipkow@243
   346
	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
nipkow@243
   347
	(rtac allI 1),
nipkow@243
   348
	((rtac contX2mono 1) THEN (etac spec 1)),
nipkow@243
   349
	(atac 1),
nipkow@243
   350
	(atac 1),
nipkow@243
   351
	(hyp_subst_tac 1),
nipkow@243
   352
	(rtac is_ub_thelub 1),
nipkow@243
   353
	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
nipkow@243
   354
	(rtac allI 1),
nipkow@243
   355
	((rtac contX2mono 1) THEN (etac spec 1)),
nipkow@243
   356
	(atac 1),
nipkow@243
   357
	(atac 1),
nipkow@243
   358
	(rtac trans_less 1),
nipkow@243
   359
	(rtac is_ub_thelub 2),
nipkow@243
   360
	(res_inst_tac [("x1","ia")] (chain_mono RS mp) 1),
nipkow@243
   361
	((rtac ch2ch_MF2L 1) THEN (etac contX2mono 1)),
nipkow@243
   362
	(atac 1),
nipkow@243
   363
	(atac 1),
nipkow@243
   364
	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
nipkow@243
   365
	(rtac allI 1),
nipkow@243
   366
	((rtac contX2mono 1) THEN (etac spec 1)),
nipkow@243
   367
	(atac 1),
nipkow@243
   368
	(atac 1),
nipkow@243
   369
	(rtac lub_mono 1),
nipkow@243
   370
	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
nipkow@243
   371
	(rtac allI 1),
nipkow@243
   372
	((rtac contX2mono 1) THEN (etac spec 1)),
nipkow@243
   373
	(atac 1),
nipkow@243
   374
	(atac 1),
nipkow@243
   375
	(rtac ch2ch_lubMF2L 1),
nipkow@243
   376
	(rtac contX2mono 1),
nipkow@243
   377
	(atac 1),
nipkow@243
   378
	(rtac allI 1),
nipkow@243
   379
	((rtac contX2mono 1) THEN (etac spec 1)),
nipkow@243
   380
	(atac 1),
nipkow@243
   381
	(atac 1),
nipkow@243
   382
	(strip_tac 1 ),
nipkow@243
   383
	(rtac is_ub_thelub 1),
nipkow@243
   384
	((rtac ch2ch_MF2L 1) THEN (etac contX2mono 1)),
nipkow@243
   385
	(atac 1)
nipkow@243
   386
	]);
nipkow@243
   387
nipkow@243
   388
nipkow@243
   389
val diag_lubCF2_2 = prove_goal Cont.thy 
nipkow@243
   390
"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
nipkow@243
   391
\ lub(range(%j. lub(range(%i. CF2(FY(j))(TY(i)))))) =\
nipkow@243
   392
\ lub(range(%i. CF2(FY(i))(TY(i))))"
nipkow@243
   393
(fn prems =>
nipkow@243
   394
	[
nipkow@243
   395
	(cut_facts_tac prems 1),
nipkow@243
   396
	(rtac trans 1),
nipkow@243
   397
	(rtac ex_lubMF2 1),
nipkow@243
   398
	(rtac ((hd prems) RS contX2mono) 1), 
nipkow@243
   399
	(rtac allI 1),
nipkow@243
   400
	(rtac (((hd (tl prems)) RS spec RS contX2mono)) 1),
nipkow@243
   401
	(atac 1),
nipkow@243
   402
	(atac 1),
nipkow@243
   403
	(rtac diag_lubCF2_1 1),
nipkow@243
   404
	(atac 1),
nipkow@243
   405
	(atac 1),
nipkow@243
   406
	(atac 1),
nipkow@243
   407
	(atac 1)
nipkow@243
   408
	]);
nipkow@243
   409
nipkow@243
   410
nipkow@243
   411
val contlub_CF2 = prove_goal Cont.thy 
nipkow@243
   412
"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
nipkow@243
   413
\ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i.CF2(FY(i))(TY(i))))"
nipkow@243
   414
(fn prems =>
nipkow@243
   415
	[
nipkow@243
   416
	(cut_facts_tac prems 1),
nipkow@243
   417
	(rtac ((hd prems) RS contX2contlub RS contlubE RS 
nipkow@243
   418
		spec RS mp RS ssubst) 1),
nipkow@243
   419
	(atac 1),
nipkow@243
   420
	(rtac (thelub_fun RS ssubst) 1),
nipkow@243
   421
	(rtac ((hd prems) RS contX2mono RS ch2ch_monofun) 1), 
nipkow@243
   422
	(atac 1),
nipkow@243
   423
	(rtac trans 1),
nipkow@243
   424
	(rtac (((hd (tl prems)) RS spec RS contX2contlub) RS 
nipkow@243
   425
	contlubE RS spec RS mp RS ext RS arg_cong RS arg_cong) 1),
nipkow@243
   426
	(atac 1),
nipkow@243
   427
	(rtac diag_lubCF2_2 1),
nipkow@243
   428
	(atac 1),
nipkow@243
   429
	(atac 1),
nipkow@243
   430
	(atac 1),
nipkow@243
   431
	(atac 1)
nipkow@243
   432
	]);
nipkow@243
   433
nipkow@243
   434
(* ------------------------------------------------------------------------ *)
nipkow@243
   435
(* The following results are about application for functions in 'a=>'b      *)
nipkow@243
   436
(* ------------------------------------------------------------------------ *)
nipkow@243
   437
nipkow@243
   438
val monofun_fun_fun = prove_goal Cont.thy 
nipkow@243
   439
	"f1 << f2 ==> f1(x) << f2(x)"
nipkow@243
   440
(fn prems =>
nipkow@243
   441
	[
nipkow@243
   442
	(cut_facts_tac prems 1),
nipkow@243
   443
	(etac (less_fun RS iffD1 RS spec) 1)
nipkow@243
   444
	]);
nipkow@243
   445
nipkow@243
   446
val monofun_fun_arg = prove_goal Cont.thy 
nipkow@243
   447
	"[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)"
nipkow@243
   448
(fn prems =>
nipkow@243
   449
	[
nipkow@243
   450
	(cut_facts_tac prems 1),
nipkow@243
   451
	(etac (monofunE RS spec RS spec RS mp) 1),
nipkow@243
   452
	(atac 1)
nipkow@243
   453
	]);
nipkow@243
   454
nipkow@243
   455
val monofun_fun = prove_goal Cont.thy 
nipkow@243
   456
"[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)"
nipkow@243
   457
(fn prems =>
nipkow@243
   458
	[
nipkow@243
   459
	(cut_facts_tac prems 1),
nipkow@243
   460
	(rtac trans_less 1),
nipkow@243
   461
	(etac monofun_fun_arg 1),
nipkow@243
   462
	(atac 1),
nipkow@243
   463
	(etac monofun_fun_fun 1)
nipkow@243
   464
	]);
nipkow@243
   465
nipkow@243
   466
nipkow@243
   467
(* ------------------------------------------------------------------------ *)
nipkow@243
   468
(* The following results are about the propagation of monotonicity and      *)
nipkow@243
   469
(* continuity                                                               *)
nipkow@243
   470
(* ------------------------------------------------------------------------ *)
nipkow@243
   471
nipkow@243
   472
val mono2mono_MF1L = prove_goal Cont.thy 
nipkow@243
   473
	"[|monofun(c1)|] ==> monofun(%x. c1(x,y))"
nipkow@243
   474
(fn prems =>
nipkow@243
   475
	[
nipkow@243
   476
	(cut_facts_tac prems 1),
nipkow@243
   477
	(rtac monofunI 1),
nipkow@243
   478
	(strip_tac 1),
nipkow@243
   479
	(etac (monofun_fun_arg RS monofun_fun_fun) 1),
nipkow@243
   480
	(atac 1)
nipkow@243
   481
	]);
nipkow@243
   482
nipkow@243
   483
val contX2contX_CF1L = prove_goal Cont.thy 
nipkow@243
   484
	"[|contX(c1)|] ==> contX(%x. c1(x,y))"
nipkow@243
   485
(fn prems =>
nipkow@243
   486
	[
nipkow@243
   487
	(cut_facts_tac prems 1),
nipkow@243
   488
	(rtac monocontlub2contX 1),
nipkow@243
   489
	(etac (contX2mono RS mono2mono_MF1L) 1),
nipkow@243
   490
	(rtac contlubI 1),
nipkow@243
   491
	(strip_tac 1),
nipkow@243
   492
	(rtac ((hd prems) RS contX2contlub RS 
nipkow@243
   493
		contlubE RS spec RS mp RS ssubst) 1),
nipkow@243
   494
	(atac 1),
nipkow@243
   495
	(rtac (thelub_fun RS ssubst) 1),
nipkow@243
   496
	(rtac ch2ch_monofun 1),
nipkow@243
   497
	(etac contX2mono 1),
nipkow@243
   498
	(atac 1),
nipkow@243
   499
	(rtac refl 1)
nipkow@243
   500
	]);
nipkow@243
   501
nipkow@243
   502
(*********  Note "(%x.%y.c1(x,y)) = c1" ***********)
nipkow@243
   503
nipkow@243
   504
val mono2mono_MF1L_rev = prove_goal Cont.thy
nipkow@243
   505
	"!y.monofun(%x.c1(x,y)) ==> monofun(c1)"
nipkow@243
   506
(fn prems =>
nipkow@243
   507
	[
nipkow@243
   508
	(cut_facts_tac prems 1),
nipkow@243
   509
	(rtac monofunI 1),
nipkow@243
   510
	(strip_tac 1),
nipkow@243
   511
	(rtac (less_fun RS iffD2) 1),
nipkow@243
   512
	(strip_tac 1),
nipkow@243
   513
	(rtac ((hd prems) RS spec RS monofunE RS spec RS spec RS mp) 1),
nipkow@243
   514
	(atac 1)
nipkow@243
   515
	]);
nipkow@243
   516
nipkow@243
   517
val contX2contX_CF1L_rev = prove_goal Cont.thy
nipkow@243
   518
	"!y.contX(%x.c1(x,y)) ==> contX(c1)"
nipkow@243
   519
(fn prems =>
nipkow@243
   520
	[
nipkow@243
   521
	(cut_facts_tac prems 1),
nipkow@243
   522
	(rtac monocontlub2contX 1),
nipkow@243
   523
	(rtac (contX2mono RS allI RS mono2mono_MF1L_rev ) 1),
nipkow@243
   524
	(etac spec 1),
nipkow@243
   525
	(rtac contlubI 1),
nipkow@243
   526
	(strip_tac 1),
nipkow@243
   527
	(rtac ext 1),
nipkow@243
   528
	(rtac (thelub_fun RS ssubst) 1),
nipkow@243
   529
	(rtac (contX2mono RS allI RS mono2mono_MF1L_rev RS ch2ch_monofun) 1),
nipkow@243
   530
	(etac spec 1),
nipkow@243
   531
	(atac 1),
nipkow@243
   532
	(rtac 
nipkow@243
   533
	((hd prems) RS spec RS contX2contlub RS contlubE RS spec RS mp) 1),
nipkow@243
   534
	(atac 1)
nipkow@243
   535
	]);
nipkow@243
   536
nipkow@243
   537
nipkow@243
   538
(* ------------------------------------------------------------------------ *)
nipkow@243
   539
(* What D.A.Schmidt calls continuity of abstraction                         *)
nipkow@243
   540
(* never used here                                                          *)
nipkow@243
   541
(* ------------------------------------------------------------------------ *)
nipkow@243
   542
nipkow@243
   543
val contlub_abstraction = prove_goal Cont.thy
nipkow@243
   544
"[|is_chain(Y::nat=>'a);!y.contX(%x.(c::'a=>'b=>'c)(x,y))|] ==>\
nipkow@243
   545
\ (%y.lub(range(%i.c(Y(i),y)))) = (lub(range(%i.%y.c(Y(i),y))))"
nipkow@243
   546
 (fn prems =>
nipkow@243
   547
	[
nipkow@243
   548
	(cut_facts_tac prems 1),
nipkow@243
   549
	(rtac trans 1),
nipkow@243
   550
	(rtac (contX2contlub RS contlubE RS spec RS mp) 2),
nipkow@243
   551
	(atac 3),
nipkow@243
   552
	(etac contX2contX_CF1L_rev 2),
nipkow@243
   553
	(rtac ext 1), 
nipkow@243
   554
	(rtac (contX2contlub RS contlubE RS spec RS mp RS sym) 1),
nipkow@243
   555
	(etac spec 1),
nipkow@243
   556
	(atac 1)
nipkow@243
   557
	]);
nipkow@243
   558
nipkow@243
   559
nipkow@243
   560
val mono2mono_app = prove_goal Cont.thy 
nipkow@243
   561
"[|monofun(ft);!x.monofun(ft(x));monofun(tt)|] ==>\
nipkow@243
   562
\	 monofun(%x.(ft(x))(tt(x)))"
nipkow@243
   563
 (fn prems =>
nipkow@243
   564
	[
nipkow@243
   565
	(cut_facts_tac prems 1),
nipkow@243
   566
	(rtac monofunI 1),
nipkow@243
   567
	(strip_tac 1),
nipkow@243
   568
	(res_inst_tac [("f1.0","ft(x)"),("f2.0","ft(y)")] monofun_fun 1),
nipkow@243
   569
	(etac spec 1),
nipkow@243
   570
	(etac spec 1),
nipkow@243
   571
	(etac (monofunE RS spec RS spec RS mp) 1),
nipkow@243
   572
	(atac 1),
nipkow@243
   573
	(etac (monofunE RS spec RS spec RS mp) 1),
nipkow@243
   574
	(atac 1)
nipkow@243
   575
	]);
nipkow@243
   576
nipkow@243
   577
val contX2contlub_app = prove_goal Cont.thy 
nipkow@243
   578
"[|contX(ft);!x.contX(ft(x));contX(tt)|] ==>\
nipkow@243
   579
\	 contlub(%x.(ft(x))(tt(x)))"
nipkow@243
   580
 (fn prems =>
nipkow@243
   581
	[
nipkow@243
   582
	(cut_facts_tac prems 1),
nipkow@243
   583
	(rtac contlubI 1),
nipkow@243
   584
	(strip_tac 1),
nipkow@243
   585
	(res_inst_tac [("f3","tt")] (contlubE RS spec RS mp RS ssubst) 1),
nipkow@243
   586
	(rtac contX2contlub 1),
nipkow@243
   587
	(resolve_tac prems 1),
nipkow@243
   588
	(atac 1),
nipkow@243
   589
	(rtac contlub_CF2 1),
nipkow@243
   590
	(resolve_tac prems 1),
nipkow@243
   591
	(resolve_tac prems 1),
nipkow@243
   592
	(atac 1),
nipkow@243
   593
	(rtac (contX2mono RS ch2ch_monofun) 1),
nipkow@243
   594
	(resolve_tac prems 1),
nipkow@243
   595
	(atac 1)
nipkow@243
   596
	]);
nipkow@243
   597
nipkow@243
   598
nipkow@243
   599
val contX2contX_app = prove_goal Cont.thy 
nipkow@243
   600
"[|contX(ft);!x.contX(ft(x));contX(tt)|] ==>\
nipkow@243
   601
\	 contX(%x.(ft(x))(tt(x)))"
nipkow@243
   602
 (fn prems =>
nipkow@243
   603
	[
nipkow@243
   604
	(rtac monocontlub2contX 1),
nipkow@243
   605
	(rtac mono2mono_app 1),
nipkow@243
   606
	(rtac contX2mono 1),
nipkow@243
   607
	(resolve_tac prems 1),
nipkow@243
   608
	(strip_tac 1),
nipkow@243
   609
	(rtac contX2mono 1),
nipkow@243
   610
	(cut_facts_tac prems 1),
nipkow@243
   611
	(etac spec 1),
nipkow@243
   612
	(rtac contX2mono 1),
nipkow@243
   613
	(resolve_tac prems 1),
nipkow@243
   614
	(rtac contX2contlub_app 1),
nipkow@243
   615
	(resolve_tac prems 1),
nipkow@243
   616
	(resolve_tac prems 1),
nipkow@243
   617
	(resolve_tac prems 1)
nipkow@243
   618
	]);
nipkow@243
   619
nipkow@243
   620
nipkow@243
   621
val contX2contX_app2 = (allI RSN (2,contX2contX_app));
nipkow@243
   622
(*  [| contX(?ft); !!x. contX(?ft(x)); contX(?tt) |] ==>                 *)
nipkow@243
   623
(*                                      contX(%x. ?ft(x,?tt(x)))         *)
nipkow@243
   624
nipkow@243
   625
nipkow@243
   626
(* ------------------------------------------------------------------------ *)
nipkow@243
   627
(* The identity function is continuous                                      *)
nipkow@243
   628
(* ------------------------------------------------------------------------ *)
nipkow@243
   629
nipkow@243
   630
val contX_id = prove_goal Cont.thy "contX(% x.x)"
nipkow@243
   631
 (fn prems =>
nipkow@243
   632
	[
nipkow@243
   633
	(rtac contXI 1),
nipkow@243
   634
	(strip_tac 1),
nipkow@243
   635
	(etac thelubE 1),
nipkow@243
   636
	(rtac refl 1)
nipkow@243
   637
	]);
nipkow@243
   638
nipkow@243
   639
nipkow@243
   640
nipkow@243
   641
(* ------------------------------------------------------------------------ *)
nipkow@243
   642
(* constant functions are continuous                                        *)
nipkow@243
   643
(* ------------------------------------------------------------------------ *)
nipkow@243
   644
nipkow@243
   645
val contX_const = prove_goalw Cont.thy [contX] "contX(%x.c)"
nipkow@243
   646
 (fn prems =>
nipkow@243
   647
	[
nipkow@243
   648
	(strip_tac 1),
nipkow@243
   649
	(rtac is_lubI 1),
nipkow@243
   650
	(rtac conjI 1),
nipkow@243
   651
	(rtac ub_rangeI 1),
nipkow@243
   652
	(strip_tac 1),
nipkow@243
   653
	(rtac refl_less 1),
nipkow@243
   654
	(strip_tac 1),
nipkow@243
   655
	(dtac ub_rangeE 1),
nipkow@243
   656
	(etac spec 1)
nipkow@243
   657
	]);
nipkow@243
   658
nipkow@243
   659
nipkow@243
   660
val contX2contX_app3 = prove_goal Cont.thy 
nipkow@243
   661
 "[|contX(f);contX(t) |] ==> contX(%x. f(t(x)))"
nipkow@243
   662
 (fn prems =>
nipkow@243
   663
	[
nipkow@243
   664
	(cut_facts_tac prems 1),
nipkow@243
   665
	(rtac contX2contX_app2 1),
nipkow@243
   666
	(rtac contX_const 1),
nipkow@243
   667
	(atac 1),
nipkow@243
   668
	(atac 1)
nipkow@243
   669
	]);
nipkow@243
   670