1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOLCF/Cfun2.ML Wed Jan 19 17:35:01 1994 +0100
1.3 @@ -0,0 +1,276 @@
1.4 +(* Title: HOLCF/cfun2.thy
1.5 + ID: $Id$
1.6 + Author: Franz Regensburger
1.7 + Copyright 1993 Technische Universitaet Muenchen
1.8 +
1.9 +Lemmas for cfun2.thy
1.10 +*)
1.11 +
1.12 +open Cfun2;
1.13 +
1.14 +(* ------------------------------------------------------------------------ *)
1.15 +(* access to less_cfun in class po *)
1.16 +(* ------------------------------------------------------------------------ *)
1.17 +
1.18 +val less_cfun = prove_goal Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
1.19 +(fn prems =>
1.20 + [
1.21 + (rtac (inst_cfun_po RS ssubst) 1),
1.22 + (fold_goals_tac [less_cfun_def]),
1.23 + (rtac refl 1)
1.24 + ]);
1.25 +
1.26 +(* ------------------------------------------------------------------------ *)
1.27 +(* Type 'a ->'b is pointed *)
1.28 +(* ------------------------------------------------------------------------ *)
1.29 +
1.30 +val minimal_cfun = prove_goalw Cfun2.thy [UU_cfun_def] "UU_cfun << f"
1.31 +(fn prems =>
1.32 + [
1.33 + (rtac (less_cfun RS ssubst) 1),
1.34 + (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
1.35 + (rtac contX_const 1),
1.36 + (fold_goals_tac [UU_fun_def]),
1.37 + (rtac minimal_fun 1)
1.38 + ]);
1.39 +
1.40 +(* ------------------------------------------------------------------------ *)
1.41 +(* fapp yields continuous functions in 'a => 'b *)
1.42 +(* this is continuity of fapp in its 'second' argument *)
1.43 +(* contX_fapp2 ==> monofun_fapp2 & contlub_fapp2 *)
1.44 +(* ------------------------------------------------------------------------ *)
1.45 +
1.46 +val contX_fapp2 = prove_goal Cfun2.thy "contX(fapp(fo))"
1.47 +(fn prems =>
1.48 + [
1.49 + (res_inst_tac [("P","contX")] CollectD 1),
1.50 + (fold_goals_tac [Cfun_def]),
1.51 + (rtac Rep_Cfun 1)
1.52 + ]);
1.53 +
1.54 +val monofun_fapp2 = contX_fapp2 RS contX2mono;
1.55 +(* monofun(fapp(?fo1)) *)
1.56 +
1.57 +
1.58 +val contlub_fapp2 = contX_fapp2 RS contX2contlub;
1.59 +(* contlub(fapp(?fo1)) *)
1.60 +
1.61 +(* ------------------------------------------------------------------------ *)
1.62 +(* expanded thms contX_fapp2, contlub_fapp2 *)
1.63 +(* looks nice with mixfix syntac _[_] *)
1.64 +(* ------------------------------------------------------------------------ *)
1.65 +
1.66 +val contX_cfun_arg = (contX_fapp2 RS contXE RS spec RS mp);
1.67 +(* is_chain(?x1) ==> range(%i. ?fo3[?x1(i)]) <<| ?fo3[lub(range(?x1))] *)
1.68 +
1.69 +val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp);
1.70 +(* is_chain(?x1) ==> ?fo4[lub(range(?x1))] = lub(range(%i. ?fo4[?x1(i)])) *)
1.71 +
1.72 +
1.73 +
1.74 +(* ------------------------------------------------------------------------ *)
1.75 +(* fapp is monotone in its 'first' argument *)
1.76 +(* ------------------------------------------------------------------------ *)
1.77 +
1.78 +val monofun_fapp1 = prove_goalw Cfun2.thy [monofun] "monofun(fapp)"
1.79 +(fn prems =>
1.80 + [
1.81 + (strip_tac 1),
1.82 + (etac (less_cfun RS subst) 1)
1.83 + ]);
1.84 +
1.85 +
1.86 +(* ------------------------------------------------------------------------ *)
1.87 +(* monotonicity of application fapp in mixfix syntax [_]_ *)
1.88 +(* ------------------------------------------------------------------------ *)
1.89 +
1.90 +val monofun_cfun_fun = prove_goal Cfun2.thy "f1 << f2 ==> f1[x] << f2[x]"
1.91 +(fn prems =>
1.92 + [
1.93 + (cut_facts_tac prems 1),
1.94 + (res_inst_tac [("x","x")] spec 1),
1.95 + (rtac (less_fun RS subst) 1),
1.96 + (etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1)
1.97 + ]);
1.98 +
1.99 +
1.100 +val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp);
1.101 +(* ?x2 << ?x1 ==> ?fo5[?x2] << ?fo5[?x1] *)
1.102 +
1.103 +(* ------------------------------------------------------------------------ *)
1.104 +(* monotonicity of fapp in both arguments in mixfix syntax [_]_ *)
1.105 +(* ------------------------------------------------------------------------ *)
1.106 +
1.107 +val monofun_cfun = prove_goal Cfun2.thy
1.108 + "[|f1<<f2;x1<<x2|] ==> f1[x1] << f2[x2]"
1.109 +(fn prems =>
1.110 + [
1.111 + (cut_facts_tac prems 1),
1.112 + (rtac trans_less 1),
1.113 + (etac monofun_cfun_arg 1),
1.114 + (etac monofun_cfun_fun 1)
1.115 + ]);
1.116 +
1.117 +
1.118 +(* ------------------------------------------------------------------------ *)
1.119 +(* ch2ch - rules for the type 'a -> 'b *)
1.120 +(* use MF2 lemmas from Cont.ML *)
1.121 +(* ------------------------------------------------------------------------ *)
1.122 +
1.123 +val ch2ch_fappR = prove_goal Cfun2.thy
1.124 + "is_chain(Y) ==> is_chain(%i. f[Y(i)])"
1.125 +(fn prems =>
1.126 + [
1.127 + (cut_facts_tac prems 1),
1.128 + (etac (monofun_fapp2 RS ch2ch_MF2R) 1)
1.129 + ]);
1.130 +
1.131 +
1.132 +val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L);
1.133 +(* is_chain(?F) ==> is_chain(%i. ?F(i)[?x]) *)
1.134 +
1.135 +
1.136 +(* ------------------------------------------------------------------------ *)
1.137 +(* the lub of a chain of continous functions is monotone *)
1.138 +(* use MF2 lemmas from Cont.ML *)
1.139 +(* ------------------------------------------------------------------------ *)
1.140 +
1.141 +val lub_cfun_mono = prove_goal Cfun2.thy
1.142 + "is_chain(F) ==> monofun(% x.lub(range(% j.F(j)[x])))"
1.143 +(fn prems =>
1.144 + [
1.145 + (cut_facts_tac prems 1),
1.146 + (rtac lub_MF2_mono 1),
1.147 + (rtac monofun_fapp1 1),
1.148 + (rtac (monofun_fapp2 RS allI) 1),
1.149 + (atac 1)
1.150 + ]);
1.151 +
1.152 +(* ------------------------------------------------------------------------ *)
1.153 +(* a lemma about the exchange of lubs for type 'a -> 'b *)
1.154 +(* use MF2 lemmas from Cont.ML *)
1.155 +(* ------------------------------------------------------------------------ *)
1.156 +
1.157 +val ex_lubcfun = prove_goal Cfun2.thy
1.158 + "[| is_chain(F); is_chain(Y) |] ==>\
1.159 +\ lub(range(%j. lub(range(%i. F(j)[Y(i)])))) =\
1.160 +\ lub(range(%i. lub(range(%j. F(j)[Y(i)]))))"
1.161 +(fn prems =>
1.162 + [
1.163 + (cut_facts_tac prems 1),
1.164 + (rtac ex_lubMF2 1),
1.165 + (rtac monofun_fapp1 1),
1.166 + (rtac (monofun_fapp2 RS allI) 1),
1.167 + (atac 1),
1.168 + (atac 1)
1.169 + ]);
1.170 +
1.171 +(* ------------------------------------------------------------------------ *)
1.172 +(* the lub of a chain of cont. functions is continuous *)
1.173 +(* ------------------------------------------------------------------------ *)
1.174 +
1.175 +val contX_lubcfun = prove_goal Cfun2.thy
1.176 + "is_chain(F) ==> contX(% x.lub(range(% j.F(j)[x])))"
1.177 +(fn prems =>
1.178 + [
1.179 + (cut_facts_tac prems 1),
1.180 + (rtac monocontlub2contX 1),
1.181 + (etac lub_cfun_mono 1),
1.182 + (rtac contlubI 1),
1.183 + (strip_tac 1),
1.184 + (rtac (contlub_cfun_arg RS ext RS ssubst) 1),
1.185 + (atac 1),
1.186 + (etac ex_lubcfun 1),
1.187 + (atac 1)
1.188 + ]);
1.189 +
1.190 +(* ------------------------------------------------------------------------ *)
1.191 +(* type 'a -> 'b is chain complete *)
1.192 +(* ------------------------------------------------------------------------ *)
1.193 +
1.194 +val lub_cfun = prove_goal Cfun2.thy
1.195 + "is_chain(CCF) ==> range(CCF) <<| fabs(% x.lub(range(% i.CCF(i)[x])))"
1.196 +(fn prems =>
1.197 + [
1.198 + (cut_facts_tac prems 1),
1.199 + (rtac is_lubI 1),
1.200 + (rtac conjI 1),
1.201 + (rtac ub_rangeI 1),
1.202 + (rtac allI 1),
1.203 + (rtac (less_cfun RS ssubst) 1),
1.204 + (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
1.205 + (etac contX_lubcfun 1),
1.206 + (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
1.207 + (etac (monofun_fapp1 RS ch2ch_monofun) 1),
1.208 + (strip_tac 1),
1.209 + (rtac (less_cfun RS ssubst) 1),
1.210 + (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
1.211 + (etac contX_lubcfun 1),
1.212 + (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
1.213 + (etac (monofun_fapp1 RS ch2ch_monofun) 1),
1.214 + (etac (monofun_fapp1 RS ub2ub_monofun) 1)
1.215 + ]);
1.216 +
1.217 +val thelub_cfun = (lub_cfun RS thelubI);
1.218 +(*
1.219 +is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
1.220 +*)
1.221 +
1.222 +val cpo_fun = prove_goal Cfun2.thy
1.223 + "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
1.224 +(fn prems =>
1.225 + [
1.226 + (cut_facts_tac prems 1),
1.227 + (rtac exI 1),
1.228 + (etac lub_cfun 1)
1.229 + ]);
1.230 +
1.231 +
1.232 +(* ------------------------------------------------------------------------ *)
1.233 +(* Extensionality in 'a -> 'b *)
1.234 +(* ------------------------------------------------------------------------ *)
1.235 +
1.236 +val ext_cfun = prove_goal Cfun1.thy "(!!x. f[x] = g[x]) ==> f = g"
1.237 + (fn prems =>
1.238 + [
1.239 + (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
1.240 + (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
1.241 + (res_inst_tac [("f","fabs")] arg_cong 1),
1.242 + (rtac ext 1),
1.243 + (resolve_tac prems 1)
1.244 + ]);
1.245 +
1.246 +(* ------------------------------------------------------------------------ *)
1.247 +(* Monotonicity of fabs *)
1.248 +(* ------------------------------------------------------------------------ *)
1.249 +
1.250 +val semi_monofun_fabs = prove_goal Cfun2.thy
1.251 + "[|contX(f);contX(g);f<<g|]==>fabs(f)<<fabs(g)"
1.252 + (fn prems =>
1.253 + [
1.254 + (rtac (less_cfun RS iffD2) 1),
1.255 + (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
1.256 + (resolve_tac prems 1),
1.257 + (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
1.258 + (resolve_tac prems 1),
1.259 + (resolve_tac prems 1)
1.260 + ]);
1.261 +
1.262 +(* ------------------------------------------------------------------------ *)
1.263 +(* Extenionality wrt. << in 'a -> 'b *)
1.264 +(* ------------------------------------------------------------------------ *)
1.265 +
1.266 +val less_cfun2 = prove_goal Cfun2.thy "(!!x. f[x] << g[x]) ==> f << g"
1.267 + (fn prems =>
1.268 + [
1.269 + (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
1.270 + (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
1.271 + (rtac semi_monofun_fabs 1),
1.272 + (rtac contX_fapp2 1),
1.273 + (rtac contX_fapp2 1),
1.274 + (rtac (less_fun RS iffD2) 1),
1.275 + (rtac allI 1),
1.276 + (resolve_tac prems 1)
1.277 + ]);
1.278 +
1.279 +