src/HOLCF/Cfun2.ML
author clasohm
Tue Jan 30 13:42:57 1996 +0100 (1996-01-30)
changeset 1461 6bcb44e4d6e5
parent 1168 74be52691d62
child 1779 1155c06fa956
permissions -rw-r--r--
expanded tabs
     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 (* ------------------------------------------------------------------------ *)
    12 (* access to less_cfun in class po                                          *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
    16 (fn prems =>
    17         [
    18         (rtac (inst_cfun_po RS ssubst) 1),
    19         (fold_goals_tac [less_cfun_def]),
    20         (rtac refl 1)
    21         ]);
    22 
    23 (* ------------------------------------------------------------------------ *)
    24 (* Type 'a ->'b  is pointed                                                 *)
    25 (* ------------------------------------------------------------------------ *)
    26 
    27 qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f"
    28 (fn prems =>
    29         [
    30         (rtac (less_cfun RS ssubst) 1),
    31         (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
    32         (rtac cont_const 1),
    33         (fold_goals_tac [UU_fun_def]),
    34         (rtac minimal_fun 1)
    35         ]);
    36 
    37 (* ------------------------------------------------------------------------ *)
    38 (* fapp yields continuous functions in 'a => 'b                             *)
    39 (* this is continuity of fapp in its 'second' argument                      *)
    40 (* cont_fapp2 ==> monofun_fapp2 & contlub_fapp2                            *)
    41 (* ------------------------------------------------------------------------ *)
    42 
    43 qed_goal "cont_fapp2" Cfun2.thy "cont(fapp(fo))"
    44 (fn prems =>
    45         [
    46         (res_inst_tac [("P","cont")] CollectD 1),
    47         (fold_goals_tac [Cfun_def]),
    48         (rtac Rep_Cfun 1)
    49         ]);
    50 
    51 val monofun_fapp2 = cont_fapp2 RS cont2mono;
    52 (* monofun(fapp(?fo1)) *)
    53 
    54 
    55 val contlub_fapp2 = cont_fapp2 RS cont2contlub;
    56 (* contlub(fapp(?fo1)) *)
    57 
    58 (* ------------------------------------------------------------------------ *)
    59 (* expanded thms cont_fapp2, contlub_fapp2                                 *)
    60 (* looks nice with mixfix syntac                                            *)
    61 (* ------------------------------------------------------------------------ *)
    62 
    63 val cont_cfun_arg = (cont_fapp2 RS contE RS spec RS mp);
    64 (* is_chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
    65  
    66 val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp);
    67 (* is_chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
    68 
    69 
    70 (* ------------------------------------------------------------------------ *)
    71 (* fapp is monotone in its 'first' argument                                 *)
    72 (* ------------------------------------------------------------------------ *)
    73 
    74 qed_goalw "monofun_fapp1" Cfun2.thy [monofun] "monofun(fapp)"
    75 (fn prems =>
    76         [
    77         (strip_tac 1),
    78         (etac (less_cfun RS subst) 1)
    79         ]);
    80 
    81 
    82 (* ------------------------------------------------------------------------ *)
    83 (* monotonicity of application fapp in mixfix syntax [_]_                   *)
    84 (* ------------------------------------------------------------------------ *)
    85 
    86 qed_goal "monofun_cfun_fun" Cfun2.thy  "f1 << f2 ==> f1`x << f2`x"
    87 (fn prems =>
    88         [
    89         (cut_facts_tac prems 1),
    90         (res_inst_tac [("x","x")] spec 1),
    91         (rtac (less_fun RS subst) 1),
    92         (etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1)
    93         ]);
    94 
    95 
    96 val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp);
    97 (* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1                                      *)
    98 
    99 (* ------------------------------------------------------------------------ *)
   100 (* monotonicity of fapp in both arguments in mixfix syntax [_]_             *)
   101 (* ------------------------------------------------------------------------ *)
   102 
   103 qed_goal "monofun_cfun" Cfun2.thy
   104         "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2"
   105 (fn prems =>
   106         [
   107         (cut_facts_tac prems 1),
   108         (rtac trans_less 1),
   109         (etac monofun_cfun_arg 1),
   110         (etac monofun_cfun_fun 1)
   111         ]);
   112 
   113 
   114 (* ------------------------------------------------------------------------ *)
   115 (* ch2ch - rules for the type 'a -> 'b                                      *)
   116 (* use MF2 lemmas from Cont.ML                                              *)
   117 (* ------------------------------------------------------------------------ *)
   118 
   119 qed_goal "ch2ch_fappR" Cfun2.thy 
   120  "is_chain(Y) ==> is_chain(%i. f`(Y i))"
   121 (fn prems =>
   122         [
   123         (cut_facts_tac prems 1),
   124         (etac (monofun_fapp2 RS ch2ch_MF2R) 1)
   125         ]);
   126 
   127 
   128 val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L);
   129 (* is_chain(?F) ==> is_chain (%i. ?F i`?x)                                  *)
   130 
   131 
   132 (* ------------------------------------------------------------------------ *)
   133 (*  the lub of a chain of continous functions is monotone                   *)
   134 (* use MF2 lemmas from Cont.ML                                              *)
   135 (* ------------------------------------------------------------------------ *)
   136 
   137 qed_goal "lub_cfun_mono" Cfun2.thy 
   138         "is_chain(F) ==> monofun(% x.lub(range(% j.(F j)`x)))"
   139 (fn prems =>
   140         [
   141         (cut_facts_tac prems 1),
   142         (rtac lub_MF2_mono 1),
   143         (rtac monofun_fapp1 1),
   144         (rtac (monofun_fapp2 RS allI) 1),
   145         (atac 1)
   146         ]);
   147 
   148 (* ------------------------------------------------------------------------ *)
   149 (* a lemma about the exchange of lubs for type 'a -> 'b                     *)
   150 (* use MF2 lemmas from Cont.ML                                              *)
   151 (* ------------------------------------------------------------------------ *)
   152 
   153 qed_goal "ex_lubcfun" Cfun2.thy
   154         "[| is_chain(F); is_chain(Y) |] ==>\
   155 \               lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
   156 \               lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
   157 (fn prems =>
   158         [
   159         (cut_facts_tac prems 1),
   160         (rtac ex_lubMF2 1),
   161         (rtac monofun_fapp1 1),
   162         (rtac (monofun_fapp2 RS allI) 1),
   163         (atac 1),
   164         (atac 1)
   165         ]);
   166 
   167 (* ------------------------------------------------------------------------ *)
   168 (* the lub of a chain of cont. functions is continuous                      *)
   169 (* ------------------------------------------------------------------------ *)
   170 
   171 qed_goal "cont_lubcfun" Cfun2.thy 
   172         "is_chain(F) ==> cont(% x.lub(range(% j.F(j)`x)))"
   173 (fn prems =>
   174         [
   175         (cut_facts_tac prems 1),
   176         (rtac monocontlub2cont 1),
   177         (etac lub_cfun_mono 1),
   178         (rtac contlubI 1),
   179         (strip_tac 1),
   180         (rtac (contlub_cfun_arg RS ext RS ssubst) 1),
   181         (atac 1),
   182         (etac ex_lubcfun 1),
   183         (atac 1)
   184         ]);
   185 
   186 (* ------------------------------------------------------------------------ *)
   187 (* type 'a -> 'b is chain complete                                          *)
   188 (* ------------------------------------------------------------------------ *)
   189 
   190 qed_goal "lub_cfun" Cfun2.thy 
   191   "is_chain(CCF) ==> range(CCF) <<| (LAM x.lub(range(% i.CCF(i)`x)))"
   192 (fn prems =>
   193         [
   194         (cut_facts_tac prems 1),
   195         (rtac is_lubI 1),
   196         (rtac conjI 1),
   197         (rtac ub_rangeI 1),  
   198         (rtac allI 1),
   199         (rtac (less_cfun RS ssubst) 1),
   200         (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   201         (etac cont_lubcfun 1),
   202         (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
   203         (etac (monofun_fapp1 RS ch2ch_monofun) 1),
   204         (strip_tac 1),
   205         (rtac (less_cfun RS ssubst) 1),
   206         (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   207         (etac cont_lubcfun 1),
   208         (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
   209         (etac (monofun_fapp1 RS ch2ch_monofun) 1),
   210         (etac (monofun_fapp1 RS ub2ub_monofun) 1)
   211         ]);
   212 
   213 val thelub_cfun = (lub_cfun RS thelubI);
   214 (* 
   215 is_chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
   216 *)
   217 
   218 qed_goal "cpo_cfun" Cfun2.thy 
   219   "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
   220 (fn prems =>
   221         [
   222         (cut_facts_tac prems 1),
   223         (rtac exI 1),
   224         (etac lub_cfun 1)
   225         ]);
   226 
   227 
   228 (* ------------------------------------------------------------------------ *)
   229 (* Extensionality in 'a -> 'b                                               *)
   230 (* ------------------------------------------------------------------------ *)
   231 
   232 qed_goal "ext_cfun" Cfun1.thy "(!!x. f`x = g`x) ==> f = g"
   233  (fn prems =>
   234         [
   235         (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   236         (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   237         (res_inst_tac [("f","fabs")] arg_cong 1),
   238         (rtac ext 1),
   239         (resolve_tac prems 1)
   240         ]);
   241 
   242 (* ------------------------------------------------------------------------ *)
   243 (* Monotonicity of fabs                                                     *)
   244 (* ------------------------------------------------------------------------ *)
   245 
   246 qed_goal "semi_monofun_fabs" Cfun2.thy 
   247         "[|cont(f);cont(g);f<<g|]==>fabs(f)<<fabs(g)"
   248  (fn prems =>
   249         [
   250         (rtac (less_cfun RS iffD2) 1),
   251         (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   252         (resolve_tac prems 1),
   253         (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   254         (resolve_tac prems 1),
   255         (resolve_tac prems 1)
   256         ]);
   257 
   258 (* ------------------------------------------------------------------------ *)
   259 (* Extenionality wrt. << in 'a -> 'b                                        *)
   260 (* ------------------------------------------------------------------------ *)
   261 
   262 qed_goal "less_cfun2" Cfun2.thy "(!!x. f`x << g`x) ==> f << g"
   263  (fn prems =>
   264         [
   265         (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   266         (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   267         (rtac semi_monofun_fabs 1),
   268         (rtac cont_fapp2 1),
   269         (rtac cont_fapp2 1),
   270         (rtac (less_fun RS iffD2) 1),
   271         (rtac allI 1),
   272         (resolve_tac prems 1)
   273         ]);
   274 
   275