src/HOLCF/Cfun2.ML
author nipkow
Tue Jan 09 15:32:27 2001 +0100 (2001-01-09)
changeset 10834 a7897aebbffc
parent 9248 e1dee89de037
child 11341 100edbd42dba
permissions -rw-r--r--
*** empty log message ***
     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 (* ------------------------------------------------------------------------ *)
    97 (* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_             *)
    98 (* ------------------------------------------------------------------------ *)
    99 
   100 Goal "[|f1<<f2;x1<<x2|] ==> f1$x1 << f2$x2";
   101 by (rtac trans_less 1);
   102 by (etac monofun_cfun_arg 1);
   103 by (etac monofun_cfun_fun 1);
   104 qed "monofun_cfun";
   105 
   106 
   107 Goal "f$x = UU ==> f$UU = UU";
   108 by (rtac (eq_UU_iff RS iffD2) 1);
   109 by (etac subst 1);
   110 by (rtac (minimal RS monofun_cfun_arg) 1);
   111 qed "strictI";
   112 
   113 
   114 (* ------------------------------------------------------------------------ *)
   115 (* ch2ch - rules for the type 'a -> 'b                                      *)
   116 (* use MF2 lemmas from Cont.ML                                              *)
   117 (* ------------------------------------------------------------------------ *)
   118 
   119 Goal "chain(Y) ==> chain(%i. f$(Y i))";
   120 by (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1);
   121 qed "ch2ch_Rep_CFunR";
   122 
   123 
   124 bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L);
   125 (* chain(?F) ==> chain (%i. ?F i$?x)                                  *)
   126 
   127 
   128 (* ------------------------------------------------------------------------ *)
   129 (*  the lub of a chain of continous functions is monotone                   *)
   130 (* use MF2 lemmas from Cont.ML                                              *)
   131 (* ------------------------------------------------------------------------ *)
   132 
   133 Goal "chain(F) ==> monofun(% x. lub(range(% j.(F j)$x)))";
   134 by (rtac lub_MF2_mono 1);
   135 by (rtac monofun_Rep_CFun1 1);
   136 by (rtac (monofun_Rep_CFun2 RS allI) 1);
   137 by (atac 1);
   138 qed "lub_cfun_mono";
   139 
   140 (* ------------------------------------------------------------------------ *)
   141 (* a lemma about the exchange of lubs for type 'a -> 'b                     *)
   142 (* use MF2 lemmas from Cont.ML                                              *)
   143 (* ------------------------------------------------------------------------ *)
   144 
   145 Goal "[| chain(F); chain(Y) |] ==>\
   146 \               lub(range(%j. lub(range(%i. F(j)$(Y i))))) =\
   147 \               lub(range(%i. lub(range(%j. F(j)$(Y i)))))";
   148 by (rtac ex_lubMF2 1);
   149 by (rtac monofun_Rep_CFun1 1);
   150 by (rtac (monofun_Rep_CFun2 RS allI) 1);
   151 by (atac 1);
   152 by (atac 1);
   153 qed "ex_lubcfun";
   154 
   155 (* ------------------------------------------------------------------------ *)
   156 (* the lub of a chain of cont. functions is continuous                      *)
   157 (* ------------------------------------------------------------------------ *)
   158 
   159 Goal "chain(F) ==> cont(% x. lub(range(% j. F(j)$x)))";
   160 by (rtac monocontlub2cont 1);
   161 by (etac lub_cfun_mono 1);
   162 by (rtac contlubI 1);
   163 by (strip_tac 1);
   164 by (stac (contlub_cfun_arg RS ext) 1);
   165 by (atac 1);
   166 by (etac ex_lubcfun 1);
   167 by (atac 1);
   168 qed "cont_lubcfun";
   169 
   170 (* ------------------------------------------------------------------------ *)
   171 (* type 'a -> 'b is chain complete                                          *)
   172 (* ------------------------------------------------------------------------ *)
   173 
   174 Goal "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)$x)))";
   175 by (rtac is_lubI 1);
   176 by (rtac ub_rangeI 1);
   177 by (stac less_cfun 1);
   178 by (stac Abs_Cfun_inverse2 1);
   179 by (etac cont_lubcfun 1);
   180 by (rtac (lub_fun RS is_lubD1 RS ub_rangeD) 1);
   181 by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
   182 by (stac less_cfun 1);
   183 by (stac Abs_Cfun_inverse2 1);
   184 by (etac cont_lubcfun 1);
   185 by (rtac (lub_fun RS is_lub_lub) 1);
   186 by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
   187 by (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1);
   188 qed "lub_cfun";
   189 
   190 bind_thm ("thelub_cfun", lub_cfun RS thelubI);
   191 (* 
   192 chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i$x)))
   193 *)
   194 
   195 Goal "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x";
   196 by (rtac exI 1);
   197 by (etac lub_cfun 1);
   198 qed "cpo_cfun";
   199 
   200 
   201 (* ------------------------------------------------------------------------ *)
   202 (* Extensionality in 'a -> 'b                                               *)
   203 (* ------------------------------------------------------------------------ *)
   204 
   205 val prems = Goal "(!!x. f$x = g$x) ==> f = g";
   206 by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
   207 by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
   208 by (res_inst_tac [("f","Abs_CFun")] arg_cong 1);
   209 by (rtac ext 1);
   210 by (resolve_tac prems 1);
   211 qed "ext_cfun";
   212 
   213 (* ------------------------------------------------------------------------ *)
   214 (* Monotonicity of Abs_CFun                                                     *)
   215 (* ------------------------------------------------------------------------ *)
   216 
   217 Goal "[| cont(f); cont(g); f<<g|] ==> Abs_CFun(f)<<Abs_CFun(g)";
   218 by (rtac (less_cfun RS iffD2) 1);
   219 by (stac Abs_Cfun_inverse2 1);
   220 by (assume_tac 1);
   221 by (stac Abs_Cfun_inverse2 1);
   222 by (assume_tac 1);
   223 by (assume_tac 1);
   224 qed "semi_monofun_Abs_CFun";
   225 
   226 (* ------------------------------------------------------------------------ *)
   227 (* Extenionality wrt. << in 'a -> 'b                                        *)
   228 (* ------------------------------------------------------------------------ *)
   229 
   230 val prems = Goal "(!!x. f$x << g$x) ==> f << g";
   231 by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
   232 by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
   233 by (rtac semi_monofun_Abs_CFun 1);
   234 by (rtac cont_Rep_CFun2 1);
   235 by (rtac cont_Rep_CFun2 1);
   236 by (rtac (less_fun RS iffD2) 1);
   237 by (rtac allI 1);
   238 by (resolve_tac prems 1);
   239 qed "less_cfun2";
   240 
   241