src/HOLCF/Cfun2.ML
changeset 1168 74be52691d62
parent 892 d0dc8d057929
child 1461 6bcb44e4d6e5
     1.1 --- a/src/HOLCF/Cfun2.ML	Thu Jun 29 16:16:24 1995 +0200
     1.2 +++ b/src/HOLCF/Cfun2.ML	Thu Jun 29 16:28:40 1995 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  	[
     1.5  	(rtac (less_cfun RS ssubst) 1),
     1.6  	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
     1.7 -	(rtac contX_const 1),
     1.8 +	(rtac cont_const 1),
     1.9  	(fold_goals_tac [UU_fun_def]),
    1.10  	(rtac minimal_fun 1)
    1.11  	]);
    1.12 @@ -37,35 +37,34 @@
    1.13  (* ------------------------------------------------------------------------ *)
    1.14  (* fapp yields continuous functions in 'a => 'b                             *)
    1.15  (* this is continuity of fapp in its 'second' argument                      *)
    1.16 -(* contX_fapp2 ==> monofun_fapp2 & contlub_fapp2                            *)
    1.17 +(* cont_fapp2 ==> monofun_fapp2 & contlub_fapp2                            *)
    1.18  (* ------------------------------------------------------------------------ *)
    1.19  
    1.20 -qed_goal "contX_fapp2" Cfun2.thy "contX(fapp(fo))"
    1.21 +qed_goal "cont_fapp2" Cfun2.thy "cont(fapp(fo))"
    1.22  (fn prems =>
    1.23  	[
    1.24 -	(res_inst_tac [("P","contX")] CollectD 1),
    1.25 +	(res_inst_tac [("P","cont")] CollectD 1),
    1.26  	(fold_goals_tac [Cfun_def]),
    1.27  	(rtac Rep_Cfun 1)
    1.28  	]);
    1.29  
    1.30 -val monofun_fapp2 = contX_fapp2 RS contX2mono;
    1.31 +val monofun_fapp2 = cont_fapp2 RS cont2mono;
    1.32  (* monofun(fapp(?fo1)) *)
    1.33  
    1.34  
    1.35 -val contlub_fapp2 = contX_fapp2 RS contX2contlub;
    1.36 +val contlub_fapp2 = cont_fapp2 RS cont2contlub;
    1.37  (* contlub(fapp(?fo1)) *)
    1.38  
    1.39  (* ------------------------------------------------------------------------ *)
    1.40 -(* expanded thms contX_fapp2, contlub_fapp2                                 *)
    1.41 -(* looks nice with mixfix syntac _[_]                                       *)
    1.42 +(* expanded thms cont_fapp2, contlub_fapp2                                 *)
    1.43 +(* looks nice with mixfix syntac                                            *)
    1.44  (* ------------------------------------------------------------------------ *)
    1.45  
    1.46 -val contX_cfun_arg = (contX_fapp2 RS contXE RS spec RS mp);
    1.47 -(* is_chain(?x1) ==> range(%i. ?fo3[?x1(i)]) <<| ?fo3[lub(range(?x1))]      *)
    1.48 +val cont_cfun_arg = (cont_fapp2 RS contE RS spec RS mp);
    1.49 +(* is_chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
    1.50   
    1.51  val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp);
    1.52 -(* is_chain(?x1) ==> ?fo4[lub(range(?x1))] = lub(range(%i. ?fo4[?x1(i)]))   *)
    1.53 -
    1.54 +(* is_chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
    1.55  
    1.56  
    1.57  (* ------------------------------------------------------------------------ *)
    1.58 @@ -84,7 +83,7 @@
    1.59  (* monotonicity of application fapp in mixfix syntax [_]_                   *)
    1.60  (* ------------------------------------------------------------------------ *)
    1.61  
    1.62 -qed_goal "monofun_cfun_fun" Cfun2.thy  "f1 << f2 ==> f1[x] << f2[x]"
    1.63 +qed_goal "monofun_cfun_fun" Cfun2.thy  "f1 << f2 ==> f1`x << f2`x"
    1.64  (fn prems =>
    1.65  	[
    1.66  	(cut_facts_tac prems 1),
    1.67 @@ -95,14 +94,14 @@
    1.68  
    1.69  
    1.70  val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp);
    1.71 -(* ?x2 << ?x1 ==> ?fo5[?x2] << ?fo5[?x1]                                    *)
    1.72 +(* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1                                      *)
    1.73  
    1.74  (* ------------------------------------------------------------------------ *)
    1.75  (* monotonicity of fapp in both arguments in mixfix syntax [_]_             *)
    1.76  (* ------------------------------------------------------------------------ *)
    1.77  
    1.78  qed_goal "monofun_cfun" Cfun2.thy
    1.79 -	"[|f1<<f2;x1<<x2|] ==> f1[x1] << f2[x2]"
    1.80 +	"[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2"
    1.81  (fn prems =>
    1.82  	[
    1.83  	(cut_facts_tac prems 1),
    1.84 @@ -118,7 +117,7 @@
    1.85  (* ------------------------------------------------------------------------ *)
    1.86  
    1.87  qed_goal "ch2ch_fappR" Cfun2.thy 
    1.88 - "is_chain(Y) ==> is_chain(%i. f[Y(i)])"
    1.89 + "is_chain(Y) ==> is_chain(%i. f`(Y i))"
    1.90  (fn prems =>
    1.91  	[
    1.92  	(cut_facts_tac prems 1),
    1.93 @@ -127,7 +126,7 @@
    1.94  
    1.95  
    1.96  val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L);
    1.97 -(* is_chain(?F) ==> is_chain(%i. ?F(i)[?x])                                 *)
    1.98 +(* is_chain(?F) ==> is_chain (%i. ?F i`?x)                                  *)
    1.99  
   1.100  
   1.101  (* ------------------------------------------------------------------------ *)
   1.102 @@ -136,7 +135,7 @@
   1.103  (* ------------------------------------------------------------------------ *)
   1.104  
   1.105  qed_goal "lub_cfun_mono" Cfun2.thy 
   1.106 -	"is_chain(F) ==> monofun(% x.lub(range(% j.F(j)[x])))"
   1.107 +	"is_chain(F) ==> monofun(% x.lub(range(% j.(F j)`x)))"
   1.108  (fn prems =>
   1.109  	[
   1.110  	(cut_facts_tac prems 1),
   1.111 @@ -153,8 +152,8 @@
   1.112  
   1.113  qed_goal "ex_lubcfun" Cfun2.thy
   1.114  	"[| is_chain(F); is_chain(Y) |] ==>\
   1.115 -\		lub(range(%j. lub(range(%i. F(j)[Y(i)])))) =\
   1.116 -\		lub(range(%i. lub(range(%j. F(j)[Y(i)]))))"
   1.117 +\		lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
   1.118 +\		lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
   1.119  (fn prems =>
   1.120  	[
   1.121  	(cut_facts_tac prems 1),
   1.122 @@ -169,12 +168,12 @@
   1.123  (* the lub of a chain of cont. functions is continuous                      *)
   1.124  (* ------------------------------------------------------------------------ *)
   1.125  
   1.126 -qed_goal "contX_lubcfun" Cfun2.thy 
   1.127 -	"is_chain(F) ==> contX(% x.lub(range(% j.F(j)[x])))"
   1.128 +qed_goal "cont_lubcfun" Cfun2.thy 
   1.129 +	"is_chain(F) ==> cont(% x.lub(range(% j.F(j)`x)))"
   1.130  (fn prems =>
   1.131  	[
   1.132  	(cut_facts_tac prems 1),
   1.133 -	(rtac monocontlub2contX 1),
   1.134 +	(rtac monocontlub2cont 1),
   1.135  	(etac lub_cfun_mono 1),
   1.136  	(rtac contlubI 1),
   1.137  	(strip_tac 1),
   1.138 @@ -189,7 +188,7 @@
   1.139  (* ------------------------------------------------------------------------ *)
   1.140  
   1.141  qed_goal "lub_cfun" Cfun2.thy 
   1.142 -  "is_chain(CCF) ==> range(CCF) <<| fabs(% x.lub(range(% i.CCF(i)[x])))"
   1.143 +  "is_chain(CCF) ==> range(CCF) <<| (LAM x.lub(range(% i.CCF(i)`x)))"
   1.144  (fn prems =>
   1.145  	[
   1.146  	(cut_facts_tac prems 1),
   1.147 @@ -199,13 +198,13 @@
   1.148  	(rtac allI 1),
   1.149  	(rtac (less_cfun RS ssubst) 1),
   1.150  	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   1.151 -	(etac contX_lubcfun 1),
   1.152 +	(etac cont_lubcfun 1),
   1.153  	(rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
   1.154  	(etac (monofun_fapp1 RS ch2ch_monofun) 1),
   1.155  	(strip_tac 1),
   1.156  	(rtac (less_cfun RS ssubst) 1),
   1.157  	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   1.158 -	(etac contX_lubcfun 1),
   1.159 +	(etac cont_lubcfun 1),
   1.160  	(rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
   1.161  	(etac (monofun_fapp1 RS ch2ch_monofun) 1),
   1.162  	(etac (monofun_fapp1 RS ub2ub_monofun) 1)
   1.163 @@ -213,7 +212,7 @@
   1.164  
   1.165  val thelub_cfun = (lub_cfun RS thelubI);
   1.166  (* 
   1.167 -is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
   1.168 +is_chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
   1.169  *)
   1.170  
   1.171  qed_goal "cpo_cfun" Cfun2.thy 
   1.172 @@ -230,7 +229,7 @@
   1.173  (* Extensionality in 'a -> 'b                                               *)
   1.174  (* ------------------------------------------------------------------------ *)
   1.175  
   1.176 -qed_goal "ext_cfun" Cfun1.thy "(!!x. f[x] = g[x]) ==> f = g"
   1.177 +qed_goal "ext_cfun" Cfun1.thy "(!!x. f`x = g`x) ==> f = g"
   1.178   (fn prems =>
   1.179  	[
   1.180  	(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   1.181 @@ -245,7 +244,7 @@
   1.182  (* ------------------------------------------------------------------------ *)
   1.183  
   1.184  qed_goal "semi_monofun_fabs" Cfun2.thy 
   1.185 -	"[|contX(f);contX(g);f<<g|]==>fabs(f)<<fabs(g)"
   1.186 +	"[|cont(f);cont(g);f<<g|]==>fabs(f)<<fabs(g)"
   1.187   (fn prems =>
   1.188  	[
   1.189  	(rtac (less_cfun RS iffD2) 1),
   1.190 @@ -260,14 +259,14 @@
   1.191  (* Extenionality wrt. << in 'a -> 'b                                        *)
   1.192  (* ------------------------------------------------------------------------ *)
   1.193  
   1.194 -qed_goal "less_cfun2" Cfun2.thy "(!!x. f[x] << g[x]) ==> f << g"
   1.195 +qed_goal "less_cfun2" Cfun2.thy "(!!x. f`x << g`x) ==> f << g"
   1.196   (fn prems =>
   1.197  	[
   1.198  	(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   1.199  	(res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   1.200  	(rtac semi_monofun_fabs 1),
   1.201 -	(rtac contX_fapp2 1),
   1.202 -	(rtac contX_fapp2 1),
   1.203 +	(rtac cont_fapp2 1),
   1.204 +	(rtac cont_fapp2 1),
   1.205  	(rtac (less_fun RS iffD2) 1),
   1.206  	(rtac allI 1),
   1.207  	(resolve_tac prems 1)