src/HOLCF/Cfun2.ML
changeset 9245 428385c4bc50
parent 5291 5706f0ef1d43
child 9248 e1dee89de037
     1.1 --- a/src/HOLCF/Cfun2.ML	Tue Jul 04 14:58:40 2000 +0200
     1.2 +++ b/src/HOLCF/Cfun2.ML	Tue Jul 04 15:58:11 2000 +0200
     1.3 @@ -1,52 +1,42 @@
     1.4 -(*  Title:      HOLCF/cfun2.thy
     1.5 +(*  Title:      HOLCF/Cfun2
     1.6      ID:         $Id$
     1.7      Author:     Franz Regensburger
     1.8      Copyright   1993 Technische Universitaet Muenchen
     1.9  
    1.10 -Lemmas for cfun2.thy 
    1.11 +Class Instance ->::(cpo,cpo)po
    1.12  *)
    1.13  
    1.14 -open Cfun2;
    1.15 -
    1.16  (* for compatibility with old HOLCF-Version *)
    1.17 -qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)"
    1.18 - (fn prems => 
    1.19 -        [
    1.20 -	(fold_goals_tac [less_cfun_def]),
    1.21 -	(rtac refl 1)
    1.22 -        ]);
    1.23 +val prems = goal thy "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)";
    1.24 +by (fold_goals_tac [less_cfun_def]);
    1.25 +by (rtac refl 1);
    1.26 +qed "inst_cfun_po";
    1.27  
    1.28  (* ------------------------------------------------------------------------ *)
    1.29  (* access to less_cfun in class po                                          *)
    1.30  (* ------------------------------------------------------------------------ *)
    1.31  
    1.32 -qed_goal "less_cfun" thy "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))"
    1.33 -(fn prems =>
    1.34 -        [
    1.35 -        (simp_tac (simpset() addsimps [inst_cfun_po]) 1)
    1.36 -        ]);
    1.37 +val prems = goal thy "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))";
    1.38 +by (simp_tac (simpset() addsimps [inst_cfun_po]) 1);
    1.39 +qed "less_cfun";
    1.40  
    1.41  (* ------------------------------------------------------------------------ *)
    1.42  (* Type 'a ->'b  is pointed                                                 *)
    1.43  (* ------------------------------------------------------------------------ *)
    1.44  
    1.45 -qed_goal "minimal_cfun" thy "Abs_CFun(% x. UU) << f"
    1.46 -(fn prems =>
    1.47 -        [
    1.48 -        (stac less_cfun 1),
    1.49 -        (stac Abs_Cfun_inverse2 1),
    1.50 -        (rtac cont_const 1),
    1.51 -        (rtac minimal_fun 1)
    1.52 -        ]);
    1.53 +val prems = goal thy "Abs_CFun(% x. UU) << f";
    1.54 +by (stac less_cfun 1);
    1.55 +by (stac Abs_Cfun_inverse2 1);
    1.56 +by (rtac cont_const 1);
    1.57 +by (rtac minimal_fun 1);
    1.58 +qed "minimal_cfun";
    1.59  
    1.60  bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
    1.61  
    1.62 -qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y. x<<y"
    1.63 -(fn prems =>
    1.64 -        [
    1.65 -        (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1),
    1.66 -        (rtac (minimal_cfun RS allI) 1)
    1.67 -        ]);
    1.68 +val prems = goal thy "? x::'a->'b::pcpo.!y. x<<y";
    1.69 +by (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1);
    1.70 +by (rtac (minimal_cfun RS allI) 1);
    1.71 +qed "least_cfun";
    1.72  
    1.73  (* ------------------------------------------------------------------------ *)
    1.74  (* Rep_CFun yields continuous functions in 'a => 'b                             *)
    1.75 @@ -54,13 +44,11 @@
    1.76  (* cont_Rep_CFun2 ==> monofun_Rep_CFun2 & contlub_Rep_CFun2                            *)
    1.77  (* ------------------------------------------------------------------------ *)
    1.78  
    1.79 -qed_goal "cont_Rep_CFun2" thy "cont(Rep_CFun(fo))"
    1.80 -(fn prems =>
    1.81 -        [
    1.82 -        (res_inst_tac [("P","cont")] CollectD 1),
    1.83 -        (fold_goals_tac [CFun_def]),
    1.84 -        (rtac Rep_Cfun 1)
    1.85 -        ]);
    1.86 +val prems = goal thy "cont(Rep_CFun(fo))";
    1.87 +by (res_inst_tac [("P","cont")] CollectD 1);
    1.88 +by (fold_goals_tac [CFun_def]);
    1.89 +by (rtac Rep_Cfun 1);
    1.90 +qed "cont_Rep_CFun2";
    1.91  
    1.92  bind_thm ("monofun_Rep_CFun2", cont_Rep_CFun2 RS cont2mono);
    1.93  (* monofun(Rep_CFun(?fo1)) *)
    1.94 @@ -85,26 +73,22 @@
    1.95  (* Rep_CFun is monotone in its 'first' argument                                 *)
    1.96  (* ------------------------------------------------------------------------ *)
    1.97  
    1.98 -qed_goalw "monofun_Rep_CFun1" thy [monofun] "monofun(Rep_CFun)"
    1.99 -(fn prems =>
   1.100 -        [
   1.101 -        (strip_tac 1),
   1.102 -        (etac (less_cfun RS subst) 1)
   1.103 -        ]);
   1.104 +val prems = goalw thy [monofun] "monofun(Rep_CFun)";
   1.105 +by (strip_tac 1);
   1.106 +by (etac (less_cfun RS subst) 1);
   1.107 +qed "monofun_Rep_CFun1";
   1.108  
   1.109  
   1.110  (* ------------------------------------------------------------------------ *)
   1.111  (* monotonicity of application Rep_CFun in mixfix syntax [_]_                   *)
   1.112  (* ------------------------------------------------------------------------ *)
   1.113  
   1.114 -qed_goal "monofun_cfun_fun" thy  "f1 << f2 ==> f1`x << f2`x"
   1.115 -(fn prems =>
   1.116 -        [
   1.117 -        (cut_facts_tac prems 1),
   1.118 -        (res_inst_tac [("x","x")] spec 1),
   1.119 -        (rtac (less_fun RS subst) 1),
   1.120 -        (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1)
   1.121 -        ]);
   1.122 +val prems = goal thy  "f1 << f2 ==> f1`x << f2`x";
   1.123 +by (cut_facts_tac prems 1);
   1.124 +by (res_inst_tac [("x","x")] spec 1);
   1.125 +by (rtac (less_fun RS subst) 1);
   1.126 +by (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1);
   1.127 +qed "monofun_cfun_fun";
   1.128  
   1.129  
   1.130  bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp);
   1.131 @@ -114,22 +98,20 @@
   1.132  (* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_             *)
   1.133  (* ------------------------------------------------------------------------ *)
   1.134  
   1.135 -qed_goal "monofun_cfun" thy
   1.136 -        "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2"
   1.137 -(fn prems =>
   1.138 -        [
   1.139 -        (cut_facts_tac prems 1),
   1.140 -        (rtac trans_less 1),
   1.141 -        (etac monofun_cfun_arg 1),
   1.142 -        (etac monofun_cfun_fun 1)
   1.143 -        ]);
   1.144 +val prems = goal thy
   1.145 +        "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2";
   1.146 +by (cut_facts_tac prems 1);
   1.147 +by (rtac trans_less 1);
   1.148 +by (etac monofun_cfun_arg 1);
   1.149 +by (etac monofun_cfun_fun 1);
   1.150 +qed "monofun_cfun";
   1.151  
   1.152  
   1.153 -qed_goal "strictI" thy "f`x = UU ==> f`UU = UU" (fn prems => [
   1.154 -        cut_facts_tac prems 1,
   1.155 -        rtac (eq_UU_iff RS iffD2) 1,
   1.156 -        etac subst 1,
   1.157 -        rtac (minimal RS monofun_cfun_arg) 1]);
   1.158 +Goal "f`x = UU ==> f`UU = UU";
   1.159 +by (rtac (eq_UU_iff RS iffD2) 1);
   1.160 +by (etac subst 1);
   1.161 +by (rtac (minimal RS monofun_cfun_arg) 1);
   1.162 +qed "strictI";
   1.163  
   1.164  
   1.165  (* ------------------------------------------------------------------------ *)
   1.166 @@ -137,13 +119,11 @@
   1.167  (* use MF2 lemmas from Cont.ML                                              *)
   1.168  (* ------------------------------------------------------------------------ *)
   1.169  
   1.170 -qed_goal "ch2ch_Rep_CFunR" thy 
   1.171 - "chain(Y) ==> chain(%i. f`(Y i))"
   1.172 -(fn prems =>
   1.173 -        [
   1.174 -        (cut_facts_tac prems 1),
   1.175 -        (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1)
   1.176 -        ]);
   1.177 +val prems = goal thy 
   1.178 + "chain(Y) ==> chain(%i. f`(Y i))";
   1.179 +by (cut_facts_tac prems 1);
   1.180 +by (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1);
   1.181 +qed "ch2ch_Rep_CFunR";
   1.182  
   1.183  
   1.184  bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L);
   1.185 @@ -155,142 +135,126 @@
   1.186  (* use MF2 lemmas from Cont.ML                                              *)
   1.187  (* ------------------------------------------------------------------------ *)
   1.188  
   1.189 -qed_goal "lub_cfun_mono" thy 
   1.190 -        "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
   1.191 -(fn prems =>
   1.192 -        [
   1.193 -        (cut_facts_tac prems 1),
   1.194 -        (rtac lub_MF2_mono 1),
   1.195 -        (rtac monofun_Rep_CFun1 1),
   1.196 -        (rtac (monofun_Rep_CFun2 RS allI) 1),
   1.197 -        (atac 1)
   1.198 -        ]);
   1.199 +val prems = goal thy 
   1.200 +        "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))";
   1.201 +by (cut_facts_tac prems 1);
   1.202 +by (rtac lub_MF2_mono 1);
   1.203 +by (rtac monofun_Rep_CFun1 1);
   1.204 +by (rtac (monofun_Rep_CFun2 RS allI) 1);
   1.205 +by (atac 1);
   1.206 +qed "lub_cfun_mono";
   1.207  
   1.208  (* ------------------------------------------------------------------------ *)
   1.209  (* a lemma about the exchange of lubs for type 'a -> 'b                     *)
   1.210  (* use MF2 lemmas from Cont.ML                                              *)
   1.211  (* ------------------------------------------------------------------------ *)
   1.212  
   1.213 -qed_goal "ex_lubcfun" thy
   1.214 +val prems = goal thy
   1.215          "[| chain(F); chain(Y) |] ==>\
   1.216  \               lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
   1.217 -\               lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
   1.218 -(fn prems =>
   1.219 -        [
   1.220 -        (cut_facts_tac prems 1),
   1.221 -        (rtac ex_lubMF2 1),
   1.222 -        (rtac monofun_Rep_CFun1 1),
   1.223 -        (rtac (monofun_Rep_CFun2 RS allI) 1),
   1.224 -        (atac 1),
   1.225 -        (atac 1)
   1.226 -        ]);
   1.227 +\               lub(range(%i. lub(range(%j. F(j)`(Y i)))))";
   1.228 +by (cut_facts_tac prems 1);
   1.229 +by (rtac ex_lubMF2 1);
   1.230 +by (rtac monofun_Rep_CFun1 1);
   1.231 +by (rtac (monofun_Rep_CFun2 RS allI) 1);
   1.232 +by (atac 1);
   1.233 +by (atac 1);
   1.234 +qed "ex_lubcfun";
   1.235  
   1.236  (* ------------------------------------------------------------------------ *)
   1.237  (* the lub of a chain of cont. functions is continuous                      *)
   1.238  (* ------------------------------------------------------------------------ *)
   1.239  
   1.240 -qed_goal "cont_lubcfun" thy 
   1.241 -        "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
   1.242 -(fn prems =>
   1.243 -        [
   1.244 -        (cut_facts_tac prems 1),
   1.245 -        (rtac monocontlub2cont 1),
   1.246 -        (etac lub_cfun_mono 1),
   1.247 -        (rtac contlubI 1),
   1.248 -        (strip_tac 1),
   1.249 -        (stac (contlub_cfun_arg RS ext) 1),
   1.250 -        (atac 1),
   1.251 -        (etac ex_lubcfun 1),
   1.252 -        (atac 1)
   1.253 -        ]);
   1.254 +val prems = goal thy 
   1.255 +        "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))";
   1.256 +by (cut_facts_tac prems 1);
   1.257 +by (rtac monocontlub2cont 1);
   1.258 +by (etac lub_cfun_mono 1);
   1.259 +by (rtac contlubI 1);
   1.260 +by (strip_tac 1);
   1.261 +by (stac (contlub_cfun_arg RS ext) 1);
   1.262 +by (atac 1);
   1.263 +by (etac ex_lubcfun 1);
   1.264 +by (atac 1);
   1.265 +qed "cont_lubcfun";
   1.266  
   1.267  (* ------------------------------------------------------------------------ *)
   1.268  (* type 'a -> 'b is chain complete                                          *)
   1.269  (* ------------------------------------------------------------------------ *)
   1.270  
   1.271 -qed_goal "lub_cfun" thy 
   1.272 -  "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
   1.273 -(fn prems =>
   1.274 -        [
   1.275 -        (cut_facts_tac prems 1),
   1.276 -        (rtac is_lubI 1),
   1.277 -        (rtac conjI 1),
   1.278 -        (rtac ub_rangeI 1),  
   1.279 -        (rtac allI 1),
   1.280 -        (stac less_cfun 1),
   1.281 -        (stac Abs_Cfun_inverse2 1),
   1.282 -        (etac cont_lubcfun 1),
   1.283 -        (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
   1.284 -        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
   1.285 -        (strip_tac 1),
   1.286 -        (stac less_cfun 1),
   1.287 -        (stac Abs_Cfun_inverse2 1),
   1.288 -        (etac cont_lubcfun 1),
   1.289 -        (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
   1.290 -        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
   1.291 -        (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1)
   1.292 -        ]);
   1.293 +val prems = goal thy 
   1.294 +  "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))";
   1.295 +by (cut_facts_tac prems 1);
   1.296 +by (rtac is_lubI 1);
   1.297 +by (rtac conjI 1);
   1.298 +by (rtac ub_rangeI 1);
   1.299 +by (rtac allI 1);
   1.300 +by (stac less_cfun 1);
   1.301 +by (stac Abs_Cfun_inverse2 1);
   1.302 +by (etac cont_lubcfun 1);
   1.303 +by (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1);
   1.304 +by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
   1.305 +by (strip_tac 1);
   1.306 +by (stac less_cfun 1);
   1.307 +by (stac Abs_Cfun_inverse2 1);
   1.308 +by (etac cont_lubcfun 1);
   1.309 +by (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1);
   1.310 +by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
   1.311 +by (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1);
   1.312 +qed "lub_cfun";
   1.313  
   1.314  bind_thm ("thelub_cfun", lub_cfun RS thelubI);
   1.315  (* 
   1.316  chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
   1.317  *)
   1.318  
   1.319 -qed_goal "cpo_cfun" thy 
   1.320 -  "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
   1.321 -(fn prems =>
   1.322 -        [
   1.323 -        (cut_facts_tac prems 1),
   1.324 -        (rtac exI 1),
   1.325 -        (etac lub_cfun 1)
   1.326 -        ]);
   1.327 +val prems = goal thy 
   1.328 +  "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x";
   1.329 +by (cut_facts_tac prems 1);
   1.330 +by (rtac exI 1);
   1.331 +by (etac lub_cfun 1);
   1.332 +qed "cpo_cfun";
   1.333  
   1.334  
   1.335  (* ------------------------------------------------------------------------ *)
   1.336  (* Extensionality in 'a -> 'b                                               *)
   1.337  (* ------------------------------------------------------------------------ *)
   1.338  
   1.339 -qed_goal "ext_cfun" Cfun1.thy "(!!x. f`x = g`x) ==> f = g"
   1.340 - (fn prems =>
   1.341 -        [
   1.342 -        (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   1.343 -        (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   1.344 -        (res_inst_tac [("f","Abs_CFun")] arg_cong 1),
   1.345 -        (rtac ext 1),
   1.346 -        (resolve_tac prems 1)
   1.347 -        ]);
   1.348 +val prems = goal Cfun1.thy "(!!x. f`x = g`x) ==> f = g";
   1.349 +by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
   1.350 +by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
   1.351 +by (res_inst_tac [("f","Abs_CFun")] arg_cong 1);
   1.352 +by (rtac ext 1);
   1.353 +by (resolve_tac prems 1);
   1.354 +qed "ext_cfun";
   1.355  
   1.356  (* ------------------------------------------------------------------------ *)
   1.357  (* Monotonicity of Abs_CFun                                                     *)
   1.358  (* ------------------------------------------------------------------------ *)
   1.359  
   1.360 -qed_goal "semi_monofun_Abs_CFun" thy 
   1.361 -        "[|cont(f);cont(g);f<<g|]==>Abs_CFun(f)<<Abs_CFun(g)"
   1.362 - (fn prems =>
   1.363 -        [
   1.364 -        (rtac (less_cfun RS iffD2) 1),
   1.365 -        (stac Abs_Cfun_inverse2 1),
   1.366 -        (resolve_tac prems 1),
   1.367 -        (stac Abs_Cfun_inverse2 1),
   1.368 -        (resolve_tac prems 1),
   1.369 -        (resolve_tac prems 1)
   1.370 -        ]);
   1.371 +val prems = goal thy 
   1.372 +        "[|cont(f);cont(g);f<<g|]==>Abs_CFun(f)<<Abs_CFun(g)";
   1.373 +by (rtac (less_cfun RS iffD2) 1);
   1.374 +by (stac Abs_Cfun_inverse2 1);
   1.375 +by (resolve_tac prems 1);
   1.376 +by (stac Abs_Cfun_inverse2 1);
   1.377 +by (resolve_tac prems 1);
   1.378 +by (resolve_tac prems 1);
   1.379 +qed "semi_monofun_Abs_CFun";
   1.380  
   1.381  (* ------------------------------------------------------------------------ *)
   1.382  (* Extenionality wrt. << in 'a -> 'b                                        *)
   1.383  (* ------------------------------------------------------------------------ *)
   1.384  
   1.385 -qed_goal "less_cfun2" thy "(!!x. f`x << g`x) ==> f << g"
   1.386 - (fn prems =>
   1.387 -        [
   1.388 -        (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   1.389 -        (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   1.390 -        (rtac semi_monofun_Abs_CFun 1),
   1.391 -        (rtac cont_Rep_CFun2 1),
   1.392 -        (rtac cont_Rep_CFun2 1),
   1.393 -        (rtac (less_fun RS iffD2) 1),
   1.394 -        (rtac allI 1),
   1.395 -        (resolve_tac prems 1)
   1.396 -        ]);
   1.397 +val prems = goal thy "(!!x. f`x << g`x) ==> f << g";
   1.398 +by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
   1.399 +by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
   1.400 +by (rtac semi_monofun_Abs_CFun 1);
   1.401 +by (rtac cont_Rep_CFun2 1);
   1.402 +by (rtac cont_Rep_CFun2 1);
   1.403 +by (rtac (less_fun RS iffD2) 1);
   1.404 +by (rtac allI 1);
   1.405 +by (resolve_tac prems 1);
   1.406 +qed "less_cfun2";
   1.407  
   1.408