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