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