src/HOLCF/Cfun2.ML
changeset 5291 5706f0ef1d43
parent 4721 c8a8482a8124
child 9245 428385c4bc50
     1.1 --- a/src/HOLCF/Cfun2.ML	Mon Aug 10 17:06:02 1998 +0200
     1.2 +++ b/src/HOLCF/Cfun2.ML	Wed Aug 12 12:17:20 1998 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  open Cfun2;
     1.5  
     1.6  (* for compatibility with old HOLCF-Version *)
     1.7 -qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. fapp f1 << fapp f2)"
     1.8 +qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)"
     1.9   (fn prems => 
    1.10          [
    1.11  	(fold_goals_tac [less_cfun_def]),
    1.12 @@ -20,7 +20,7 @@
    1.13  (* access to less_cfun in class po                                          *)
    1.14  (* ------------------------------------------------------------------------ *)
    1.15  
    1.16 -qed_goal "less_cfun" thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
    1.17 +qed_goal "less_cfun" thy "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))"
    1.18  (fn prems =>
    1.19          [
    1.20          (simp_tac (simpset() addsimps [inst_cfun_po]) 1)
    1.21 @@ -30,7 +30,7 @@
    1.22  (* Type 'a ->'b  is pointed                                                 *)
    1.23  (* ------------------------------------------------------------------------ *)
    1.24  
    1.25 -qed_goal "minimal_cfun" thy "fabs(% x. UU) << f"
    1.26 +qed_goal "minimal_cfun" thy "Abs_CFun(% x. UU) << f"
    1.27  (fn prems =>
    1.28          [
    1.29          (stac less_cfun 1),
    1.30 @@ -44,17 +44,17 @@
    1.31  qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y. x<<y"
    1.32  (fn prems =>
    1.33          [
    1.34 -        (res_inst_tac [("x","fabs(% x. UU)")] exI 1),
    1.35 +        (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1),
    1.36          (rtac (minimal_cfun RS allI) 1)
    1.37          ]);
    1.38  
    1.39  (* ------------------------------------------------------------------------ *)
    1.40 -(* fapp yields continuous functions in 'a => 'b                             *)
    1.41 -(* this is continuity of fapp in its 'second' argument                      *)
    1.42 -(* cont_fapp2 ==> monofun_fapp2 & contlub_fapp2                            *)
    1.43 +(* Rep_CFun yields continuous functions in 'a => 'b                             *)
    1.44 +(* this is continuity of Rep_CFun in its 'second' argument                      *)
    1.45 +(* cont_Rep_CFun2 ==> monofun_Rep_CFun2 & contlub_Rep_CFun2                            *)
    1.46  (* ------------------------------------------------------------------------ *)
    1.47  
    1.48 -qed_goal "cont_fapp2" thy "cont(fapp(fo))"
    1.49 +qed_goal "cont_Rep_CFun2" thy "cont(Rep_CFun(fo))"
    1.50  (fn prems =>
    1.51          [
    1.52          (res_inst_tac [("P","cont")] CollectD 1),
    1.53 @@ -62,30 +62,30 @@
    1.54          (rtac Rep_Cfun 1)
    1.55          ]);
    1.56  
    1.57 -bind_thm ("monofun_fapp2", cont_fapp2 RS cont2mono);
    1.58 -(* monofun(fapp(?fo1)) *)
    1.59 +bind_thm ("monofun_Rep_CFun2", cont_Rep_CFun2 RS cont2mono);
    1.60 +(* monofun(Rep_CFun(?fo1)) *)
    1.61  
    1.62  
    1.63 -bind_thm ("contlub_fapp2", cont_fapp2 RS cont2contlub);
    1.64 -(* contlub(fapp(?fo1)) *)
    1.65 +bind_thm ("contlub_Rep_CFun2", cont_Rep_CFun2 RS cont2contlub);
    1.66 +(* contlub(Rep_CFun(?fo1)) *)
    1.67  
    1.68  (* ------------------------------------------------------------------------ *)
    1.69 -(* expanded thms cont_fapp2, contlub_fapp2                                 *)
    1.70 +(* expanded thms cont_Rep_CFun2, contlub_Rep_CFun2                                 *)
    1.71  (* looks nice with mixfix syntac                                            *)
    1.72  (* ------------------------------------------------------------------------ *)
    1.73  
    1.74 -bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp));
    1.75 +bind_thm ("cont_cfun_arg", (cont_Rep_CFun2 RS contE RS spec RS mp));
    1.76  (* chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
    1.77   
    1.78 -bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp));
    1.79 +bind_thm ("contlub_cfun_arg", (contlub_Rep_CFun2 RS contlubE RS spec RS mp));
    1.80  (* chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
    1.81  
    1.82  
    1.83  (* ------------------------------------------------------------------------ *)
    1.84 -(* fapp is monotone in its 'first' argument                                 *)
    1.85 +(* Rep_CFun is monotone in its 'first' argument                                 *)
    1.86  (* ------------------------------------------------------------------------ *)
    1.87  
    1.88 -qed_goalw "monofun_fapp1" thy [monofun] "monofun(fapp)"
    1.89 +qed_goalw "monofun_Rep_CFun1" thy [monofun] "monofun(Rep_CFun)"
    1.90  (fn prems =>
    1.91          [
    1.92          (strip_tac 1),
    1.93 @@ -94,7 +94,7 @@
    1.94  
    1.95  
    1.96  (* ------------------------------------------------------------------------ *)
    1.97 -(* monotonicity of application fapp in mixfix syntax [_]_                   *)
    1.98 +(* monotonicity of application Rep_CFun in mixfix syntax [_]_                   *)
    1.99  (* ------------------------------------------------------------------------ *)
   1.100  
   1.101  qed_goal "monofun_cfun_fun" thy  "f1 << f2 ==> f1`x << f2`x"
   1.102 @@ -103,15 +103,15 @@
   1.103          (cut_facts_tac prems 1),
   1.104          (res_inst_tac [("x","x")] spec 1),
   1.105          (rtac (less_fun RS subst) 1),
   1.106 -        (etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1)
   1.107 +        (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1)
   1.108          ]);
   1.109  
   1.110  
   1.111 -bind_thm ("monofun_cfun_arg", monofun_fapp2 RS monofunE RS spec RS spec RS mp);
   1.112 +bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp);
   1.113  (* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1                                      *)
   1.114  
   1.115  (* ------------------------------------------------------------------------ *)
   1.116 -(* monotonicity of fapp in both arguments in mixfix syntax [_]_             *)
   1.117 +(* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_             *)
   1.118  (* ------------------------------------------------------------------------ *)
   1.119  
   1.120  qed_goal "monofun_cfun" thy
   1.121 @@ -137,16 +137,16 @@
   1.122  (* use MF2 lemmas from Cont.ML                                              *)
   1.123  (* ------------------------------------------------------------------------ *)
   1.124  
   1.125 -qed_goal "ch2ch_fappR" thy 
   1.126 +qed_goal "ch2ch_Rep_CFunR" thy 
   1.127   "chain(Y) ==> chain(%i. f`(Y i))"
   1.128  (fn prems =>
   1.129          [
   1.130          (cut_facts_tac prems 1),
   1.131 -        (etac (monofun_fapp2 RS ch2ch_MF2R) 1)
   1.132 +        (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1)
   1.133          ]);
   1.134  
   1.135  
   1.136 -bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L);
   1.137 +bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L);
   1.138  (* chain(?F) ==> chain (%i. ?F i`?x)                                  *)
   1.139  
   1.140  
   1.141 @@ -161,8 +161,8 @@
   1.142          [
   1.143          (cut_facts_tac prems 1),
   1.144          (rtac lub_MF2_mono 1),
   1.145 -        (rtac monofun_fapp1 1),
   1.146 -        (rtac (monofun_fapp2 RS allI) 1),
   1.147 +        (rtac monofun_Rep_CFun1 1),
   1.148 +        (rtac (monofun_Rep_CFun2 RS allI) 1),
   1.149          (atac 1)
   1.150          ]);
   1.151  
   1.152 @@ -179,8 +179,8 @@
   1.153          [
   1.154          (cut_facts_tac prems 1),
   1.155          (rtac ex_lubMF2 1),
   1.156 -        (rtac monofun_fapp1 1),
   1.157 -        (rtac (monofun_fapp2 RS allI) 1),
   1.158 +        (rtac monofun_Rep_CFun1 1),
   1.159 +        (rtac (monofun_Rep_CFun2 RS allI) 1),
   1.160          (atac 1),
   1.161          (atac 1)
   1.162          ]);
   1.163 @@ -221,14 +221,14 @@
   1.164          (stac Abs_Cfun_inverse2 1),
   1.165          (etac cont_lubcfun 1),
   1.166          (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
   1.167 -        (etac (monofun_fapp1 RS ch2ch_monofun) 1),
   1.168 +        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
   1.169          (strip_tac 1),
   1.170          (stac less_cfun 1),
   1.171          (stac Abs_Cfun_inverse2 1),
   1.172          (etac cont_lubcfun 1),
   1.173          (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
   1.174 -        (etac (monofun_fapp1 RS ch2ch_monofun) 1),
   1.175 -        (etac (monofun_fapp1 RS ub2ub_monofun) 1)
   1.176 +        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
   1.177 +        (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1)
   1.178          ]);
   1.179  
   1.180  bind_thm ("thelub_cfun", lub_cfun RS thelubI);
   1.181 @@ -255,17 +255,17 @@
   1.182          [
   1.183          (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   1.184          (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   1.185 -        (res_inst_tac [("f","fabs")] arg_cong 1),
   1.186 +        (res_inst_tac [("f","Abs_CFun")] arg_cong 1),
   1.187          (rtac ext 1),
   1.188          (resolve_tac prems 1)
   1.189          ]);
   1.190  
   1.191  (* ------------------------------------------------------------------------ *)
   1.192 -(* Monotonicity of fabs                                                     *)
   1.193 +(* Monotonicity of Abs_CFun                                                     *)
   1.194  (* ------------------------------------------------------------------------ *)
   1.195  
   1.196 -qed_goal "semi_monofun_fabs" thy 
   1.197 -        "[|cont(f);cont(g);f<<g|]==>fabs(f)<<fabs(g)"
   1.198 +qed_goal "semi_monofun_Abs_CFun" thy 
   1.199 +        "[|cont(f);cont(g);f<<g|]==>Abs_CFun(f)<<Abs_CFun(g)"
   1.200   (fn prems =>
   1.201          [
   1.202          (rtac (less_cfun RS iffD2) 1),
   1.203 @@ -285,9 +285,9 @@
   1.204          [
   1.205          (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   1.206          (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   1.207 -        (rtac semi_monofun_fabs 1),
   1.208 -        (rtac cont_fapp2 1),
   1.209 -        (rtac cont_fapp2 1),
   1.210 +        (rtac semi_monofun_Abs_CFun 1),
   1.211 +        (rtac cont_Rep_CFun2 1),
   1.212 +        (rtac cont_Rep_CFun2 1),
   1.213          (rtac (less_fun RS iffD2) 1),
   1.214          (rtac allI 1),
   1.215          (resolve_tac prems 1)