src/HOLCF/Cfun2.ML
author oheimb
Thu Sep 12 17:18:00 1996 +0200 (1996-09-12)
changeset 1989 8e0ff1bfcfea
parent 1779 1155c06fa956
child 2033 639de962ded4
permissions -rw-r--r--
added stric
tI
     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 bind_thm ("monofun_fapp2", cont_fapp2 RS cont2mono);
    52 (* monofun(fapp(?fo1)) *)
    53 
    54 
    55 bind_thm ("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 bind_thm ("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 bind_thm ("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 bind_thm ("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 qed_goal "strictI" Cfun2.thy "f`x = UU ==> f`UU = UU" (fn prems => [
   115 	cut_facts_tac prems 1,
   116 	rtac (eq_UU_iff RS iffD2) 1,
   117 	etac subst 1,
   118 	rtac (minimal RS monofun_cfun_arg) 1]);
   119 
   120 
   121 (* ------------------------------------------------------------------------ *)
   122 (* ch2ch - rules for the type 'a -> 'b                                      *)
   123 (* use MF2 lemmas from Cont.ML                                              *)
   124 (* ------------------------------------------------------------------------ *)
   125 
   126 qed_goal "ch2ch_fappR" Cfun2.thy 
   127  "is_chain(Y) ==> is_chain(%i. f`(Y i))"
   128 (fn prems =>
   129         [
   130         (cut_facts_tac prems 1),
   131         (etac (monofun_fapp2 RS ch2ch_MF2R) 1)
   132         ]);
   133 
   134 
   135 bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L);
   136 (* is_chain(?F) ==> is_chain (%i. ?F i`?x)                                  *)
   137 
   138 
   139 (* ------------------------------------------------------------------------ *)
   140 (*  the lub of a chain of continous functions is monotone                   *)
   141 (* use MF2 lemmas from Cont.ML                                              *)
   142 (* ------------------------------------------------------------------------ *)
   143 
   144 qed_goal "lub_cfun_mono" Cfun2.thy 
   145         "is_chain(F) ==> monofun(% x.lub(range(% j.(F j)`x)))"
   146 (fn prems =>
   147         [
   148         (cut_facts_tac prems 1),
   149         (rtac lub_MF2_mono 1),
   150         (rtac monofun_fapp1 1),
   151         (rtac (monofun_fapp2 RS allI) 1),
   152         (atac 1)
   153         ]);
   154 
   155 (* ------------------------------------------------------------------------ *)
   156 (* a lemma about the exchange of lubs for type 'a -> 'b                     *)
   157 (* use MF2 lemmas from Cont.ML                                              *)
   158 (* ------------------------------------------------------------------------ *)
   159 
   160 qed_goal "ex_lubcfun" Cfun2.thy
   161         "[| is_chain(F); is_chain(Y) |] ==>\
   162 \               lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
   163 \               lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
   164 (fn prems =>
   165         [
   166         (cut_facts_tac prems 1),
   167         (rtac ex_lubMF2 1),
   168         (rtac monofun_fapp1 1),
   169         (rtac (monofun_fapp2 RS allI) 1),
   170         (atac 1),
   171         (atac 1)
   172         ]);
   173 
   174 (* ------------------------------------------------------------------------ *)
   175 (* the lub of a chain of cont. functions is continuous                      *)
   176 (* ------------------------------------------------------------------------ *)
   177 
   178 qed_goal "cont_lubcfun" Cfun2.thy 
   179         "is_chain(F) ==> cont(% x.lub(range(% j.F(j)`x)))"
   180 (fn prems =>
   181         [
   182         (cut_facts_tac prems 1),
   183         (rtac monocontlub2cont 1),
   184         (etac lub_cfun_mono 1),
   185         (rtac contlubI 1),
   186         (strip_tac 1),
   187         (rtac (contlub_cfun_arg RS ext RS ssubst) 1),
   188         (atac 1),
   189         (etac ex_lubcfun 1),
   190         (atac 1)
   191         ]);
   192 
   193 (* ------------------------------------------------------------------------ *)
   194 (* type 'a -> 'b is chain complete                                          *)
   195 (* ------------------------------------------------------------------------ *)
   196 
   197 qed_goal "lub_cfun" Cfun2.thy 
   198   "is_chain(CCF) ==> range(CCF) <<| (LAM x.lub(range(% i.CCF(i)`x)))"
   199 (fn prems =>
   200         [
   201         (cut_facts_tac prems 1),
   202         (rtac is_lubI 1),
   203         (rtac conjI 1),
   204         (rtac ub_rangeI 1),  
   205         (rtac allI 1),
   206         (rtac (less_cfun RS ssubst) 1),
   207         (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   208         (etac cont_lubcfun 1),
   209         (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
   210         (etac (monofun_fapp1 RS ch2ch_monofun) 1),
   211         (strip_tac 1),
   212         (rtac (less_cfun RS ssubst) 1),
   213         (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   214         (etac cont_lubcfun 1),
   215         (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
   216         (etac (monofun_fapp1 RS ch2ch_monofun) 1),
   217         (etac (monofun_fapp1 RS ub2ub_monofun) 1)
   218         ]);
   219 
   220 bind_thm ("thelub_cfun", lub_cfun RS thelubI);
   221 (* 
   222 is_chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
   223 *)
   224 
   225 qed_goal "cpo_cfun" Cfun2.thy 
   226   "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
   227 (fn prems =>
   228         [
   229         (cut_facts_tac prems 1),
   230         (rtac exI 1),
   231         (etac lub_cfun 1)
   232         ]);
   233 
   234 
   235 (* ------------------------------------------------------------------------ *)
   236 (* Extensionality in 'a -> 'b                                               *)
   237 (* ------------------------------------------------------------------------ *)
   238 
   239 qed_goal "ext_cfun" Cfun1.thy "(!!x. f`x = g`x) ==> f = g"
   240  (fn prems =>
   241         [
   242         (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   243         (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   244         (res_inst_tac [("f","fabs")] arg_cong 1),
   245         (rtac ext 1),
   246         (resolve_tac prems 1)
   247         ]);
   248 
   249 (* ------------------------------------------------------------------------ *)
   250 (* Monotonicity of fabs                                                     *)
   251 (* ------------------------------------------------------------------------ *)
   252 
   253 qed_goal "semi_monofun_fabs" Cfun2.thy 
   254         "[|cont(f);cont(g);f<<g|]==>fabs(f)<<fabs(g)"
   255  (fn prems =>
   256         [
   257         (rtac (less_cfun RS iffD2) 1),
   258         (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   259         (resolve_tac prems 1),
   260         (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   261         (resolve_tac prems 1),
   262         (resolve_tac prems 1)
   263         ]);
   264 
   265 (* ------------------------------------------------------------------------ *)
   266 (* Extenionality wrt. << in 'a -> 'b                                        *)
   267 (* ------------------------------------------------------------------------ *)
   268 
   269 qed_goal "less_cfun2" Cfun2.thy "(!!x. f`x << g`x) ==> f << g"
   270  (fn prems =>
   271         [
   272         (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   273         (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   274         (rtac semi_monofun_fabs 1),
   275         (rtac cont_fapp2 1),
   276         (rtac cont_fapp2 1),
   277         (rtac (less_fun RS iffD2) 1),
   278         (rtac allI 1),
   279         (resolve_tac prems 1)
   280         ]);
   281 
   282