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