src/HOLCF/Cfun2.ML
author regensbu
Thu Jun 29 16:28:40 1995 +0200 (1995-06-29)
changeset 1168 74be52691d62
parent 892 d0dc8d057929
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
The curried version of HOLCF is now just called HOLCF. The old
uncurried version is no longer supported
     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