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