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