src/HOLCF/Cfun2.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5291 5706f0ef1d43
child 9245 428385c4bc50
permissions -rw-r--r--
tidying
clasohm@1461
     1
(*  Title:      HOLCF/cfun2.thy
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 cfun2.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Cfun2;
nipkow@243
    10
slotosch@2640
    11
(* for compatibility with old HOLCF-Version *)
slotosch@5291
    12
qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)"
slotosch@2640
    13
 (fn prems => 
slotosch@2640
    14
        [
slotosch@3323
    15
	(fold_goals_tac [less_cfun_def]),
slotosch@2640
    16
	(rtac refl 1)
slotosch@2640
    17
        ]);
slotosch@2640
    18
nipkow@243
    19
(* ------------------------------------------------------------------------ *)
nipkow@243
    20
(* access to less_cfun in class po                                          *)
nipkow@243
    21
(* ------------------------------------------------------------------------ *)
nipkow@243
    22
slotosch@5291
    23
qed_goal "less_cfun" thy "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))"
nipkow@243
    24
(fn prems =>
clasohm@1461
    25
        [
wenzelm@4098
    26
        (simp_tac (simpset() addsimps [inst_cfun_po]) 1)
clasohm@1461
    27
        ]);
nipkow@243
    28
nipkow@243
    29
(* ------------------------------------------------------------------------ *)
nipkow@243
    30
(* Type 'a ->'b  is pointed                                                 *)
nipkow@243
    31
(* ------------------------------------------------------------------------ *)
nipkow@243
    32
slotosch@5291
    33
qed_goal "minimal_cfun" thy "Abs_CFun(% x. UU) << f"
nipkow@243
    34
(fn prems =>
clasohm@1461
    35
        [
paulson@2033
    36
        (stac less_cfun 1),
paulson@2033
    37
        (stac Abs_Cfun_inverse2 1),
clasohm@1461
    38
        (rtac cont_const 1),
clasohm@1461
    39
        (rtac minimal_fun 1)
clasohm@1461
    40
        ]);
nipkow@243
    41
slotosch@2640
    42
bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
slotosch@2640
    43
wenzelm@3842
    44
qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y. x<<y"
slotosch@2640
    45
(fn prems =>
slotosch@2640
    46
        [
slotosch@5291
    47
        (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1),
slotosch@2640
    48
        (rtac (minimal_cfun RS allI) 1)
slotosch@2640
    49
        ]);
slotosch@2640
    50
nipkow@243
    51
(* ------------------------------------------------------------------------ *)
slotosch@5291
    52
(* Rep_CFun yields continuous functions in 'a => 'b                             *)
slotosch@5291
    53
(* this is continuity of Rep_CFun in its 'second' argument                      *)
slotosch@5291
    54
(* cont_Rep_CFun2 ==> monofun_Rep_CFun2 & contlub_Rep_CFun2                            *)
nipkow@243
    55
(* ------------------------------------------------------------------------ *)
nipkow@243
    56
slotosch@5291
    57
qed_goal "cont_Rep_CFun2" thy "cont(Rep_CFun(fo))"
nipkow@243
    58
(fn prems =>
clasohm@1461
    59
        [
clasohm@1461
    60
        (res_inst_tac [("P","cont")] CollectD 1),
slotosch@2640
    61
        (fold_goals_tac [CFun_def]),
clasohm@1461
    62
        (rtac Rep_Cfun 1)
clasohm@1461
    63
        ]);
nipkow@243
    64
slotosch@5291
    65
bind_thm ("monofun_Rep_CFun2", cont_Rep_CFun2 RS cont2mono);
slotosch@5291
    66
(* monofun(Rep_CFun(?fo1)) *)
nipkow@243
    67
nipkow@243
    68
slotosch@5291
    69
bind_thm ("contlub_Rep_CFun2", cont_Rep_CFun2 RS cont2contlub);
slotosch@5291
    70
(* contlub(Rep_CFun(?fo1)) *)
nipkow@243
    71
nipkow@243
    72
(* ------------------------------------------------------------------------ *)
slotosch@5291
    73
(* expanded thms cont_Rep_CFun2, contlub_Rep_CFun2                                 *)
regensbu@1168
    74
(* looks nice with mixfix syntac                                            *)
nipkow@243
    75
(* ------------------------------------------------------------------------ *)
nipkow@243
    76
slotosch@5291
    77
bind_thm ("cont_cfun_arg", (cont_Rep_CFun2 RS contE RS spec RS mp));
oheimb@4721
    78
(* chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
nipkow@243
    79
 
slotosch@5291
    80
bind_thm ("contlub_cfun_arg", (contlub_Rep_CFun2 RS contlubE RS spec RS mp));
oheimb@4721
    81
(* chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
nipkow@243
    82
nipkow@243
    83
nipkow@243
    84
(* ------------------------------------------------------------------------ *)
slotosch@5291
    85
(* Rep_CFun is monotone in its 'first' argument                                 *)
nipkow@243
    86
(* ------------------------------------------------------------------------ *)
nipkow@243
    87
slotosch@5291
    88
qed_goalw "monofun_Rep_CFun1" thy [monofun] "monofun(Rep_CFun)"
nipkow@243
    89
(fn prems =>
clasohm@1461
    90
        [
clasohm@1461
    91
        (strip_tac 1),
clasohm@1461
    92
        (etac (less_cfun RS subst) 1)
clasohm@1461
    93
        ]);
nipkow@243
    94
nipkow@243
    95
nipkow@243
    96
(* ------------------------------------------------------------------------ *)
slotosch@5291
    97
(* monotonicity of application Rep_CFun in mixfix syntax [_]_                   *)
nipkow@243
    98
(* ------------------------------------------------------------------------ *)
nipkow@243
    99
slotosch@2640
   100
qed_goal "monofun_cfun_fun" thy  "f1 << f2 ==> f1`x << f2`x"
nipkow@243
   101
(fn prems =>
clasohm@1461
   102
        [
clasohm@1461
   103
        (cut_facts_tac prems 1),
clasohm@1461
   104
        (res_inst_tac [("x","x")] spec 1),
clasohm@1461
   105
        (rtac (less_fun RS subst) 1),
slotosch@5291
   106
        (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1)
clasohm@1461
   107
        ]);
nipkow@243
   108
nipkow@243
   109
slotosch@5291
   110
bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp);
regensbu@1168
   111
(* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1                                      *)
nipkow@243
   112
nipkow@243
   113
(* ------------------------------------------------------------------------ *)
slotosch@5291
   114
(* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_             *)
nipkow@243
   115
(* ------------------------------------------------------------------------ *)
nipkow@243
   116
slotosch@2640
   117
qed_goal "monofun_cfun" thy
clasohm@1461
   118
        "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2"
nipkow@243
   119
(fn prems =>
clasohm@1461
   120
        [
clasohm@1461
   121
        (cut_facts_tac prems 1),
clasohm@1461
   122
        (rtac trans_less 1),
clasohm@1461
   123
        (etac monofun_cfun_arg 1),
clasohm@1461
   124
        (etac monofun_cfun_fun 1)
clasohm@1461
   125
        ]);
nipkow@243
   126
nipkow@243
   127
slotosch@2640
   128
qed_goal "strictI" thy "f`x = UU ==> f`UU = UU" (fn prems => [
paulson@2033
   129
        cut_facts_tac prems 1,
paulson@2033
   130
        rtac (eq_UU_iff RS iffD2) 1,
paulson@2033
   131
        etac subst 1,
paulson@2033
   132
        rtac (minimal RS monofun_cfun_arg) 1]);
oheimb@1989
   133
oheimb@1989
   134
nipkow@243
   135
(* ------------------------------------------------------------------------ *)
nipkow@243
   136
(* ch2ch - rules for the type 'a -> 'b                                      *)
nipkow@243
   137
(* use MF2 lemmas from Cont.ML                                              *)
nipkow@243
   138
(* ------------------------------------------------------------------------ *)
nipkow@243
   139
slotosch@5291
   140
qed_goal "ch2ch_Rep_CFunR" thy 
oheimb@4721
   141
 "chain(Y) ==> chain(%i. f`(Y i))"
nipkow@243
   142
(fn prems =>
clasohm@1461
   143
        [
clasohm@1461
   144
        (cut_facts_tac prems 1),
slotosch@5291
   145
        (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1)
clasohm@1461
   146
        ]);
nipkow@243
   147
nipkow@243
   148
slotosch@5291
   149
bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L);
oheimb@4721
   150
(* chain(?F) ==> chain (%i. ?F i`?x)                                  *)
nipkow@243
   151
nipkow@243
   152
nipkow@243
   153
(* ------------------------------------------------------------------------ *)
nipkow@243
   154
(*  the lub of a chain of continous functions is monotone                   *)
nipkow@243
   155
(* use MF2 lemmas from Cont.ML                                              *)
nipkow@243
   156
(* ------------------------------------------------------------------------ *)
nipkow@243
   157
slotosch@2640
   158
qed_goal "lub_cfun_mono" thy 
oheimb@4721
   159
        "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
nipkow@243
   160
(fn prems =>
clasohm@1461
   161
        [
clasohm@1461
   162
        (cut_facts_tac prems 1),
clasohm@1461
   163
        (rtac lub_MF2_mono 1),
slotosch@5291
   164
        (rtac monofun_Rep_CFun1 1),
slotosch@5291
   165
        (rtac (monofun_Rep_CFun2 RS allI) 1),
clasohm@1461
   166
        (atac 1)
clasohm@1461
   167
        ]);
nipkow@243
   168
nipkow@243
   169
(* ------------------------------------------------------------------------ *)
nipkow@243
   170
(* a lemma about the exchange of lubs for type 'a -> 'b                     *)
nipkow@243
   171
(* use MF2 lemmas from Cont.ML                                              *)
nipkow@243
   172
(* ------------------------------------------------------------------------ *)
nipkow@243
   173
slotosch@2640
   174
qed_goal "ex_lubcfun" thy
oheimb@4721
   175
        "[| chain(F); chain(Y) |] ==>\
clasohm@1461
   176
\               lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
clasohm@1461
   177
\               lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
nipkow@243
   178
(fn prems =>
clasohm@1461
   179
        [
clasohm@1461
   180
        (cut_facts_tac prems 1),
clasohm@1461
   181
        (rtac ex_lubMF2 1),
slotosch@5291
   182
        (rtac monofun_Rep_CFun1 1),
slotosch@5291
   183
        (rtac (monofun_Rep_CFun2 RS allI) 1),
clasohm@1461
   184
        (atac 1),
clasohm@1461
   185
        (atac 1)
clasohm@1461
   186
        ]);
nipkow@243
   187
nipkow@243
   188
(* ------------------------------------------------------------------------ *)
nipkow@243
   189
(* the lub of a chain of cont. functions is continuous                      *)
nipkow@243
   190
(* ------------------------------------------------------------------------ *)
nipkow@243
   191
slotosch@2640
   192
qed_goal "cont_lubcfun" thy 
oheimb@4721
   193
        "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
nipkow@243
   194
(fn prems =>
clasohm@1461
   195
        [
clasohm@1461
   196
        (cut_facts_tac prems 1),
clasohm@1461
   197
        (rtac monocontlub2cont 1),
clasohm@1461
   198
        (etac lub_cfun_mono 1),
clasohm@1461
   199
        (rtac contlubI 1),
clasohm@1461
   200
        (strip_tac 1),
paulson@2033
   201
        (stac (contlub_cfun_arg RS ext) 1),
clasohm@1461
   202
        (atac 1),
clasohm@1461
   203
        (etac ex_lubcfun 1),
clasohm@1461
   204
        (atac 1)
clasohm@1461
   205
        ]);
nipkow@243
   206
nipkow@243
   207
(* ------------------------------------------------------------------------ *)
nipkow@243
   208
(* type 'a -> 'b is chain complete                                          *)
nipkow@243
   209
(* ------------------------------------------------------------------------ *)
nipkow@243
   210
slotosch@2640
   211
qed_goal "lub_cfun" thy 
oheimb@4721
   212
  "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
nipkow@243
   213
(fn prems =>
clasohm@1461
   214
        [
clasohm@1461
   215
        (cut_facts_tac prems 1),
clasohm@1461
   216
        (rtac is_lubI 1),
clasohm@1461
   217
        (rtac conjI 1),
clasohm@1461
   218
        (rtac ub_rangeI 1),  
clasohm@1461
   219
        (rtac allI 1),
paulson@2033
   220
        (stac less_cfun 1),
paulson@2033
   221
        (stac Abs_Cfun_inverse2 1),
clasohm@1461
   222
        (etac cont_lubcfun 1),
clasohm@1461
   223
        (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
slotosch@5291
   224
        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
clasohm@1461
   225
        (strip_tac 1),
paulson@2033
   226
        (stac less_cfun 1),
paulson@2033
   227
        (stac Abs_Cfun_inverse2 1),
clasohm@1461
   228
        (etac cont_lubcfun 1),
clasohm@1461
   229
        (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
slotosch@5291
   230
        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
slotosch@5291
   231
        (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1)
clasohm@1461
   232
        ]);
nipkow@243
   233
oheimb@1779
   234
bind_thm ("thelub_cfun", lub_cfun RS thelubI);
nipkow@243
   235
(* 
oheimb@4721
   236
chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
nipkow@243
   237
*)
nipkow@243
   238
slotosch@2640
   239
qed_goal "cpo_cfun" thy 
oheimb@4721
   240
  "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
nipkow@243
   241
(fn prems =>
clasohm@1461
   242
        [
clasohm@1461
   243
        (cut_facts_tac prems 1),
clasohm@1461
   244
        (rtac exI 1),
clasohm@1461
   245
        (etac lub_cfun 1)
clasohm@1461
   246
        ]);
nipkow@243
   247
nipkow@243
   248
nipkow@243
   249
(* ------------------------------------------------------------------------ *)
nipkow@243
   250
(* Extensionality in 'a -> 'b                                               *)
nipkow@243
   251
(* ------------------------------------------------------------------------ *)
nipkow@243
   252
regensbu@1168
   253
qed_goal "ext_cfun" Cfun1.thy "(!!x. f`x = g`x) ==> f = g"
nipkow@243
   254
 (fn prems =>
clasohm@1461
   255
        [
clasohm@1461
   256
        (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
clasohm@1461
   257
        (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
slotosch@5291
   258
        (res_inst_tac [("f","Abs_CFun")] arg_cong 1),
clasohm@1461
   259
        (rtac ext 1),
clasohm@1461
   260
        (resolve_tac prems 1)
clasohm@1461
   261
        ]);
nipkow@243
   262
nipkow@243
   263
(* ------------------------------------------------------------------------ *)
slotosch@5291
   264
(* Monotonicity of Abs_CFun                                                     *)
nipkow@243
   265
(* ------------------------------------------------------------------------ *)
nipkow@243
   266
slotosch@5291
   267
qed_goal "semi_monofun_Abs_CFun" thy 
slotosch@5291
   268
        "[|cont(f);cont(g);f<<g|]==>Abs_CFun(f)<<Abs_CFun(g)"
nipkow@243
   269
 (fn prems =>
clasohm@1461
   270
        [
clasohm@1461
   271
        (rtac (less_cfun RS iffD2) 1),
paulson@2033
   272
        (stac Abs_Cfun_inverse2 1),
clasohm@1461
   273
        (resolve_tac prems 1),
paulson@2033
   274
        (stac Abs_Cfun_inverse2 1),
clasohm@1461
   275
        (resolve_tac prems 1),
clasohm@1461
   276
        (resolve_tac prems 1)
clasohm@1461
   277
        ]);
nipkow@243
   278
nipkow@243
   279
(* ------------------------------------------------------------------------ *)
nipkow@243
   280
(* Extenionality wrt. << in 'a -> 'b                                        *)
nipkow@243
   281
(* ------------------------------------------------------------------------ *)
nipkow@243
   282
slotosch@2640
   283
qed_goal "less_cfun2" thy "(!!x. f`x << g`x) ==> f << g"
nipkow@243
   284
 (fn prems =>
clasohm@1461
   285
        [
clasohm@1461
   286
        (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
clasohm@1461
   287
        (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
slotosch@5291
   288
        (rtac semi_monofun_Abs_CFun 1),
slotosch@5291
   289
        (rtac cont_Rep_CFun2 1),
slotosch@5291
   290
        (rtac cont_Rep_CFun2 1),
clasohm@1461
   291
        (rtac (less_fun RS iffD2) 1),
clasohm@1461
   292
        (rtac allI 1),
clasohm@1461
   293
        (resolve_tac prems 1)
clasohm@1461
   294
        ]);
nipkow@243
   295
nipkow@243
   296