src/HOLCF/Cfun2.ML
author nipkow
Wed Jan 19 17:35:01 1994 +0100 (1994-01-19)
changeset 243 c22b85994e17
child 297 5ef75ff3baeb
permissions -rw-r--r--
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
in HOL.
     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 val less_cfun = prove_goal 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 val minimal_cfun = prove_goalw 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 contX_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 (* contX_fapp2 ==> monofun_fapp2 & contlub_fapp2                            *)
    41 (* ------------------------------------------------------------------------ *)
    42 
    43 val contX_fapp2 = prove_goal Cfun2.thy "contX(fapp(fo))"
    44 (fn prems =>
    45 	[
    46 	(res_inst_tac [("P","contX")] CollectD 1),
    47 	(fold_goals_tac [Cfun_def]),
    48 	(rtac Rep_Cfun 1)
    49 	]);
    50 
    51 val monofun_fapp2 = contX_fapp2 RS contX2mono;
    52 (* monofun(fapp(?fo1)) *)
    53 
    54 
    55 val contlub_fapp2 = contX_fapp2 RS contX2contlub;
    56 (* contlub(fapp(?fo1)) *)
    57 
    58 (* ------------------------------------------------------------------------ *)
    59 (* expanded thms contX_fapp2, contlub_fapp2                                 *)
    60 (* looks nice with mixfix syntac _[_]                                       *)
    61 (* ------------------------------------------------------------------------ *)
    62 
    63 val contX_cfun_arg = (contX_fapp2 RS contXE 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 (* ------------------------------------------------------------------------ *)
    72 (* fapp is monotone in its 'first' argument                                 *)
    73 (* ------------------------------------------------------------------------ *)
    74 
    75 val monofun_fapp1 = prove_goalw Cfun2.thy [monofun] "monofun(fapp)"
    76 (fn prems =>
    77 	[
    78 	(strip_tac 1),
    79 	(etac (less_cfun RS subst) 1)
    80 	]);
    81 
    82 
    83 (* ------------------------------------------------------------------------ *)
    84 (* monotonicity of application fapp in mixfix syntax [_]_                   *)
    85 (* ------------------------------------------------------------------------ *)
    86 
    87 val monofun_cfun_fun = prove_goal Cfun2.thy  "f1 << f2 ==> f1[x] << f2[x]"
    88 (fn prems =>
    89 	[
    90 	(cut_facts_tac prems 1),
    91 	(res_inst_tac [("x","x")] spec 1),
    92 	(rtac (less_fun RS subst) 1),
    93 	(etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1)
    94 	]);
    95 
    96 
    97 val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp);
    98 (* ?x2 << ?x1 ==> ?fo5[?x2] << ?fo5[?x1]                                    *)
    99 
   100 (* ------------------------------------------------------------------------ *)
   101 (* monotonicity of fapp in both arguments in mixfix syntax [_]_             *)
   102 (* ------------------------------------------------------------------------ *)
   103 
   104 val monofun_cfun = prove_goal Cfun2.thy
   105 	"[|f1<<f2;x1<<x2|] ==> f1[x1] << f2[x2]"
   106 (fn prems =>
   107 	[
   108 	(cut_facts_tac prems 1),
   109 	(rtac trans_less 1),
   110 	(etac monofun_cfun_arg 1),
   111 	(etac monofun_cfun_fun 1)
   112 	]);
   113 
   114 
   115 (* ------------------------------------------------------------------------ *)
   116 (* ch2ch - rules for the type 'a -> 'b                                      *)
   117 (* use MF2 lemmas from Cont.ML                                              *)
   118 (* ------------------------------------------------------------------------ *)
   119 
   120 val ch2ch_fappR = prove_goal Cfun2.thy 
   121  "is_chain(Y) ==> is_chain(%i. f[Y(i)])"
   122 (fn prems =>
   123 	[
   124 	(cut_facts_tac prems 1),
   125 	(etac (monofun_fapp2 RS ch2ch_MF2R) 1)
   126 	]);
   127 
   128 
   129 val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L);
   130 (* is_chain(?F) ==> is_chain(%i. ?F(i)[?x])                                 *)
   131 
   132 
   133 (* ------------------------------------------------------------------------ *)
   134 (*  the lub of a chain of continous functions is monotone                   *)
   135 (* use MF2 lemmas from Cont.ML                                              *)
   136 (* ------------------------------------------------------------------------ *)
   137 
   138 val lub_cfun_mono = prove_goal Cfun2.thy 
   139 	"is_chain(F) ==> monofun(% x.lub(range(% j.F(j)[x])))"
   140 (fn prems =>
   141 	[
   142 	(cut_facts_tac prems 1),
   143 	(rtac lub_MF2_mono 1),
   144 	(rtac monofun_fapp1 1),
   145 	(rtac (monofun_fapp2 RS allI) 1),
   146 	(atac 1)
   147 	]);
   148 
   149 (* ------------------------------------------------------------------------ *)
   150 (* a lemma about the exchange of lubs for type 'a -> 'b                     *)
   151 (* use MF2 lemmas from Cont.ML                                              *)
   152 (* ------------------------------------------------------------------------ *)
   153 
   154 val ex_lubcfun = prove_goal Cfun2.thy
   155 	"[| is_chain(F); is_chain(Y) |] ==>\
   156 \		lub(range(%j. lub(range(%i. F(j)[Y(i)])))) =\
   157 \		lub(range(%i. lub(range(%j. F(j)[Y(i)]))))"
   158 (fn prems =>
   159 	[
   160 	(cut_facts_tac prems 1),
   161 	(rtac ex_lubMF2 1),
   162 	(rtac monofun_fapp1 1),
   163 	(rtac (monofun_fapp2 RS allI) 1),
   164 	(atac 1),
   165 	(atac 1)
   166 	]);
   167 
   168 (* ------------------------------------------------------------------------ *)
   169 (* the lub of a chain of cont. functions is continuous                      *)
   170 (* ------------------------------------------------------------------------ *)
   171 
   172 val contX_lubcfun = prove_goal Cfun2.thy 
   173 	"is_chain(F) ==> contX(% x.lub(range(% j.F(j)[x])))"
   174 (fn prems =>
   175 	[
   176 	(cut_facts_tac prems 1),
   177 	(rtac monocontlub2contX 1),
   178 	(etac lub_cfun_mono 1),
   179 	(rtac contlubI 1),
   180 	(strip_tac 1),
   181 	(rtac (contlub_cfun_arg RS ext RS ssubst) 1),
   182 	(atac 1),
   183 	(etac ex_lubcfun 1),
   184 	(atac 1)
   185 	]);
   186 
   187 (* ------------------------------------------------------------------------ *)
   188 (* type 'a -> 'b is chain complete                                          *)
   189 (* ------------------------------------------------------------------------ *)
   190 
   191 val lub_cfun = prove_goal Cfun2.thy 
   192   "is_chain(CCF) ==> range(CCF) <<| fabs(% x.lub(range(% i.CCF(i)[x])))"
   193 (fn prems =>
   194 	[
   195 	(cut_facts_tac prems 1),
   196 	(rtac is_lubI 1),
   197 	(rtac conjI 1),
   198 	(rtac ub_rangeI 1),  
   199 	(rtac allI 1),
   200 	(rtac (less_cfun RS ssubst) 1),
   201 	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   202 	(etac contX_lubcfun 1),
   203 	(rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
   204 	(etac (monofun_fapp1 RS ch2ch_monofun) 1),
   205 	(strip_tac 1),
   206 	(rtac (less_cfun RS ssubst) 1),
   207 	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   208 	(etac contX_lubcfun 1),
   209 	(rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
   210 	(etac (monofun_fapp1 RS ch2ch_monofun) 1),
   211 	(etac (monofun_fapp1 RS ub2ub_monofun) 1)
   212 	]);
   213 
   214 val thelub_cfun = (lub_cfun RS thelubI);
   215 (* 
   216 is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
   217 *)
   218 
   219 val cpo_fun = prove_goal Cfun2.thy 
   220   "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
   221 (fn prems =>
   222 	[
   223 	(cut_facts_tac prems 1),
   224 	(rtac exI 1),
   225 	(etac lub_cfun 1)
   226 	]);
   227 
   228 
   229 (* ------------------------------------------------------------------------ *)
   230 (* Extensionality in 'a -> 'b                                               *)
   231 (* ------------------------------------------------------------------------ *)
   232 
   233 val ext_cfun = prove_goal Cfun1.thy "(!!x. f[x] = g[x]) ==> f = g"
   234  (fn prems =>
   235 	[
   236 	(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   237 	(res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   238 	(res_inst_tac [("f","fabs")] arg_cong 1),
   239 	(rtac ext 1),
   240 	(resolve_tac prems 1)
   241 	]);
   242 
   243 (* ------------------------------------------------------------------------ *)
   244 (* Monotonicity of fabs                                                     *)
   245 (* ------------------------------------------------------------------------ *)
   246 
   247 val semi_monofun_fabs = prove_goal Cfun2.thy 
   248 	"[|contX(f);contX(g);f<<g|]==>fabs(f)<<fabs(g)"
   249  (fn prems =>
   250 	[
   251 	(rtac (less_cfun RS iffD2) 1),
   252 	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   253 	(resolve_tac prems 1),
   254 	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   255 	(resolve_tac prems 1),
   256 	(resolve_tac prems 1)
   257 	]);
   258 
   259 (* ------------------------------------------------------------------------ *)
   260 (* Extenionality wrt. << in 'a -> 'b                                        *)
   261 (* ------------------------------------------------------------------------ *)
   262 
   263 val less_cfun2 = prove_goal Cfun2.thy "(!!x. f[x] << g[x]) ==> f << g"
   264  (fn prems =>
   265 	[
   266 	(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   267 	(res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   268 	(rtac semi_monofun_fabs 1),
   269 	(rtac contX_fapp2 1),
   270 	(rtac contX_fapp2 1),
   271 	(rtac (less_fun RS iffD2) 1),
   272 	(rtac allI 1),
   273 	(resolve_tac prems 1)
   274 	]);
   275 
   276