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
     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 val prems = goal thy "(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 val prems = goal thy "( 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 val prems = goal thy "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 val prems = goal thy "? 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 val prems = goal thy "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 val prems = goalw thy [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 val prems = goal thy  "f1 << f2 ==> f1`x << f2`x";
    87 by (cut_facts_tac prems 1);
    88 by (res_inst_tac [("x","x")] spec 1);
    89 by (rtac (less_fun RS subst) 1);
    90 by (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1);
    91 qed "monofun_cfun_fun";
    92 
    93 
    94 bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp);
    95 (* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1                                      *)
    96 
    97 (* ------------------------------------------------------------------------ *)
    98 (* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_             *)
    99 (* ------------------------------------------------------------------------ *)
   100 
   101 val prems = goal thy
   102         "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2";
   103 by (cut_facts_tac prems 1);
   104 by (rtac trans_less 1);
   105 by (etac monofun_cfun_arg 1);
   106 by (etac monofun_cfun_fun 1);
   107 qed "monofun_cfun";
   108 
   109 
   110 Goal "f`x = UU ==> f`UU = UU";
   111 by (rtac (eq_UU_iff RS iffD2) 1);
   112 by (etac subst 1);
   113 by (rtac (minimal RS monofun_cfun_arg) 1);
   114 qed "strictI";
   115 
   116 
   117 (* ------------------------------------------------------------------------ *)
   118 (* ch2ch - rules for the type 'a -> 'b                                      *)
   119 (* use MF2 lemmas from Cont.ML                                              *)
   120 (* ------------------------------------------------------------------------ *)
   121 
   122 val prems = goal thy 
   123  "chain(Y) ==> chain(%i. f`(Y i))";
   124 by (cut_facts_tac prems 1);
   125 by (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1);
   126 qed "ch2ch_Rep_CFunR";
   127 
   128 
   129 bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L);
   130 (* chain(?F) ==> chain (%i. ?F i`?x)                                  *)
   131 
   132 
   133 (* ------------------------------------------------------------------------ *)
   134 (*  the lub of a chain of continous functions is monotone                   *)
   135 (* use MF2 lemmas from Cont.ML                                              *)
   136 (* ------------------------------------------------------------------------ *)
   137 
   138 val prems = goal thy 
   139         "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))";
   140 by (cut_facts_tac prems 1);
   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 val prems = goal thy
   153         "[| chain(F); chain(Y) |] ==>\
   154 \               lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
   155 \               lub(range(%i. lub(range(%j. F(j)`(Y i)))))";
   156 by (cut_facts_tac prems 1);
   157 by (rtac ex_lubMF2 1);
   158 by (rtac monofun_Rep_CFun1 1);
   159 by (rtac (monofun_Rep_CFun2 RS allI) 1);
   160 by (atac 1);
   161 by (atac 1);
   162 qed "ex_lubcfun";
   163 
   164 (* ------------------------------------------------------------------------ *)
   165 (* the lub of a chain of cont. functions is continuous                      *)
   166 (* ------------------------------------------------------------------------ *)
   167 
   168 val prems = goal thy 
   169         "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))";
   170 by (cut_facts_tac prems 1);
   171 by (rtac monocontlub2cont 1);
   172 by (etac lub_cfun_mono 1);
   173 by (rtac contlubI 1);
   174 by (strip_tac 1);
   175 by (stac (contlub_cfun_arg RS ext) 1);
   176 by (atac 1);
   177 by (etac ex_lubcfun 1);
   178 by (atac 1);
   179 qed "cont_lubcfun";
   180 
   181 (* ------------------------------------------------------------------------ *)
   182 (* type 'a -> 'b is chain complete                                          *)
   183 (* ------------------------------------------------------------------------ *)
   184 
   185 val prems = goal thy 
   186   "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))";
   187 by (cut_facts_tac prems 1);
   188 by (rtac is_lubI 1);
   189 by (rtac conjI 1);
   190 by (rtac ub_rangeI 1);
   191 by (rtac allI 1);
   192 by (stac less_cfun 1);
   193 by (stac Abs_Cfun_inverse2 1);
   194 by (etac cont_lubcfun 1);
   195 by (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1);
   196 by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
   197 by (strip_tac 1);
   198 by (stac less_cfun 1);
   199 by (stac Abs_Cfun_inverse2 1);
   200 by (etac cont_lubcfun 1);
   201 by (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1);
   202 by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
   203 by (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1);
   204 qed "lub_cfun";
   205 
   206 bind_thm ("thelub_cfun", lub_cfun RS thelubI);
   207 (* 
   208 chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
   209 *)
   210 
   211 val prems = goal thy 
   212   "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x";
   213 by (cut_facts_tac prems 1);
   214 by (rtac exI 1);
   215 by (etac lub_cfun 1);
   216 qed "cpo_cfun";
   217 
   218 
   219 (* ------------------------------------------------------------------------ *)
   220 (* Extensionality in 'a -> 'b                                               *)
   221 (* ------------------------------------------------------------------------ *)
   222 
   223 val prems = goal Cfun1.thy "(!!x. f`x = g`x) ==> f = g";
   224 by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
   225 by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
   226 by (res_inst_tac [("f","Abs_CFun")] arg_cong 1);
   227 by (rtac ext 1);
   228 by (resolve_tac prems 1);
   229 qed "ext_cfun";
   230 
   231 (* ------------------------------------------------------------------------ *)
   232 (* Monotonicity of Abs_CFun                                                     *)
   233 (* ------------------------------------------------------------------------ *)
   234 
   235 val prems = goal thy 
   236         "[|cont(f);cont(g);f<<g|]==>Abs_CFun(f)<<Abs_CFun(g)";
   237 by (rtac (less_cfun RS iffD2) 1);
   238 by (stac Abs_Cfun_inverse2 1);
   239 by (resolve_tac prems 1);
   240 by (stac Abs_Cfun_inverse2 1);
   241 by (resolve_tac prems 1);
   242 by (resolve_tac prems 1);
   243 qed "semi_monofun_Abs_CFun";
   244 
   245 (* ------------------------------------------------------------------------ *)
   246 (* Extenionality wrt. << in 'a -> 'b                                        *)
   247 (* ------------------------------------------------------------------------ *)
   248 
   249 val prems = goal thy "(!!x. f`x << g`x) ==> f << g";
   250 by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
   251 by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
   252 by (rtac semi_monofun_Abs_CFun 1);
   253 by (rtac cont_Rep_CFun2 1);
   254 by (rtac cont_Rep_CFun2 1);
   255 by (rtac (less_fun RS iffD2) 1);
   256 by (rtac allI 1);
   257 by (resolve_tac prems 1);
   258 qed "less_cfun2";
   259 
   260