src/HOLCF/Cfun2.ML
changeset 1461 6bcb44e4d6e5
parent 1168 74be52691d62
child 1779 1155c06fa956
     1.1 --- a/src/HOLCF/Cfun2.ML	Mon Jan 29 14:16:13 1996 +0100
     1.2 +++ b/src/HOLCF/Cfun2.ML	Tue Jan 30 13:42:57 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	HOLCF/cfun2.thy
     1.5 +(*  Title:      HOLCF/cfun2.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Franz Regensburger
     1.8 +    Author:     Franz Regensburger
     1.9      Copyright   1993 Technische Universitaet Muenchen
    1.10  
    1.11  Lemmas for cfun2.thy 
    1.12 @@ -14,11 +14,11 @@
    1.13  
    1.14  qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
    1.15  (fn prems =>
    1.16 -	[
    1.17 -	(rtac (inst_cfun_po RS ssubst) 1),
    1.18 -	(fold_goals_tac [less_cfun_def]),
    1.19 -	(rtac refl 1)
    1.20 -	]);
    1.21 +        [
    1.22 +        (rtac (inst_cfun_po RS ssubst) 1),
    1.23 +        (fold_goals_tac [less_cfun_def]),
    1.24 +        (rtac refl 1)
    1.25 +        ]);
    1.26  
    1.27  (* ------------------------------------------------------------------------ *)
    1.28  (* Type 'a ->'b  is pointed                                                 *)
    1.29 @@ -26,13 +26,13 @@
    1.30  
    1.31  qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f"
    1.32  (fn prems =>
    1.33 -	[
    1.34 -	(rtac (less_cfun RS ssubst) 1),
    1.35 -	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
    1.36 -	(rtac cont_const 1),
    1.37 -	(fold_goals_tac [UU_fun_def]),
    1.38 -	(rtac minimal_fun 1)
    1.39 -	]);
    1.40 +        [
    1.41 +        (rtac (less_cfun RS ssubst) 1),
    1.42 +        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
    1.43 +        (rtac cont_const 1),
    1.44 +        (fold_goals_tac [UU_fun_def]),
    1.45 +        (rtac minimal_fun 1)
    1.46 +        ]);
    1.47  
    1.48  (* ------------------------------------------------------------------------ *)
    1.49  (* fapp yields continuous functions in 'a => 'b                             *)
    1.50 @@ -42,11 +42,11 @@
    1.51  
    1.52  qed_goal "cont_fapp2" Cfun2.thy "cont(fapp(fo))"
    1.53  (fn prems =>
    1.54 -	[
    1.55 -	(res_inst_tac [("P","cont")] CollectD 1),
    1.56 -	(fold_goals_tac [Cfun_def]),
    1.57 -	(rtac Rep_Cfun 1)
    1.58 -	]);
    1.59 +        [
    1.60 +        (res_inst_tac [("P","cont")] CollectD 1),
    1.61 +        (fold_goals_tac [Cfun_def]),
    1.62 +        (rtac Rep_Cfun 1)
    1.63 +        ]);
    1.64  
    1.65  val monofun_fapp2 = cont_fapp2 RS cont2mono;
    1.66  (* monofun(fapp(?fo1)) *)
    1.67 @@ -73,10 +73,10 @@
    1.68  
    1.69  qed_goalw "monofun_fapp1" Cfun2.thy [monofun] "monofun(fapp)"
    1.70  (fn prems =>
    1.71 -	[
    1.72 -	(strip_tac 1),
    1.73 -	(etac (less_cfun RS subst) 1)
    1.74 -	]);
    1.75 +        [
    1.76 +        (strip_tac 1),
    1.77 +        (etac (less_cfun RS subst) 1)
    1.78 +        ]);
    1.79  
    1.80  
    1.81  (* ------------------------------------------------------------------------ *)
    1.82 @@ -85,12 +85,12 @@
    1.83  
    1.84  qed_goal "monofun_cfun_fun" Cfun2.thy  "f1 << f2 ==> f1`x << f2`x"
    1.85  (fn prems =>
    1.86 -	[
    1.87 -	(cut_facts_tac prems 1),
    1.88 -	(res_inst_tac [("x","x")] spec 1),
    1.89 -	(rtac (less_fun RS subst) 1),
    1.90 -	(etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1)
    1.91 -	]);
    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 @@ -101,14 +101,14 @@
   1.102  (* ------------------------------------------------------------------------ *)
   1.103  
   1.104  qed_goal "monofun_cfun" Cfun2.thy
   1.105 -	"[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2"
   1.106 +        "[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2"
   1.107  (fn prems =>
   1.108 -	[
   1.109 -	(cut_facts_tac prems 1),
   1.110 -	(rtac trans_less 1),
   1.111 -	(etac monofun_cfun_arg 1),
   1.112 -	(etac monofun_cfun_fun 1)
   1.113 -	]);
   1.114 +        [
   1.115 +        (cut_facts_tac prems 1),
   1.116 +        (rtac trans_less 1),
   1.117 +        (etac monofun_cfun_arg 1),
   1.118 +        (etac monofun_cfun_fun 1)
   1.119 +        ]);
   1.120  
   1.121  
   1.122  (* ------------------------------------------------------------------------ *)
   1.123 @@ -119,10 +119,10 @@
   1.124  qed_goal "ch2ch_fappR" Cfun2.thy 
   1.125   "is_chain(Y) ==> is_chain(%i. f`(Y i))"
   1.126  (fn prems =>
   1.127 -	[
   1.128 -	(cut_facts_tac prems 1),
   1.129 -	(etac (monofun_fapp2 RS ch2ch_MF2R) 1)
   1.130 -	]);
   1.131 +        [
   1.132 +        (cut_facts_tac prems 1),
   1.133 +        (etac (monofun_fapp2 RS ch2ch_MF2R) 1)
   1.134 +        ]);
   1.135  
   1.136  
   1.137  val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L);
   1.138 @@ -135,15 +135,15 @@
   1.139  (* ------------------------------------------------------------------------ *)
   1.140  
   1.141  qed_goal "lub_cfun_mono" Cfun2.thy 
   1.142 -	"is_chain(F) ==> monofun(% x.lub(range(% j.(F j)`x)))"
   1.143 +        "is_chain(F) ==> monofun(% x.lub(range(% j.(F j)`x)))"
   1.144  (fn prems =>
   1.145 -	[
   1.146 -	(cut_facts_tac prems 1),
   1.147 -	(rtac lub_MF2_mono 1),
   1.148 -	(rtac monofun_fapp1 1),
   1.149 -	(rtac (monofun_fapp2 RS allI) 1),
   1.150 -	(atac 1)
   1.151 -	]);
   1.152 +        [
   1.153 +        (cut_facts_tac prems 1),
   1.154 +        (rtac lub_MF2_mono 1),
   1.155 +        (rtac monofun_fapp1 1),
   1.156 +        (rtac (monofun_fapp2 RS allI) 1),
   1.157 +        (atac 1)
   1.158 +        ]);
   1.159  
   1.160  (* ------------------------------------------------------------------------ *)
   1.161  (* a lemma about the exchange of lubs for type 'a -> 'b                     *)
   1.162 @@ -151,37 +151,37 @@
   1.163  (* ------------------------------------------------------------------------ *)
   1.164  
   1.165  qed_goal "ex_lubcfun" Cfun2.thy
   1.166 -	"[| is_chain(F); is_chain(Y) |] ==>\
   1.167 -\		lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
   1.168 -\		lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
   1.169 +        "[| is_chain(F); is_chain(Y) |] ==>\
   1.170 +\               lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
   1.171 +\               lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
   1.172  (fn prems =>
   1.173 -	[
   1.174 -	(cut_facts_tac prems 1),
   1.175 -	(rtac ex_lubMF2 1),
   1.176 -	(rtac monofun_fapp1 1),
   1.177 -	(rtac (monofun_fapp2 RS allI) 1),
   1.178 -	(atac 1),
   1.179 -	(atac 1)
   1.180 -	]);
   1.181 +        [
   1.182 +        (cut_facts_tac prems 1),
   1.183 +        (rtac ex_lubMF2 1),
   1.184 +        (rtac monofun_fapp1 1),
   1.185 +        (rtac (monofun_fapp2 RS allI) 1),
   1.186 +        (atac 1),
   1.187 +        (atac 1)
   1.188 +        ]);
   1.189  
   1.190  (* ------------------------------------------------------------------------ *)
   1.191  (* the lub of a chain of cont. functions is continuous                      *)
   1.192  (* ------------------------------------------------------------------------ *)
   1.193  
   1.194  qed_goal "cont_lubcfun" Cfun2.thy 
   1.195 -	"is_chain(F) ==> cont(% x.lub(range(% j.F(j)`x)))"
   1.196 +        "is_chain(F) ==> cont(% x.lub(range(% j.F(j)`x)))"
   1.197  (fn prems =>
   1.198 -	[
   1.199 -	(cut_facts_tac prems 1),
   1.200 -	(rtac monocontlub2cont 1),
   1.201 -	(etac lub_cfun_mono 1),
   1.202 -	(rtac contlubI 1),
   1.203 -	(strip_tac 1),
   1.204 -	(rtac (contlub_cfun_arg RS ext RS ssubst) 1),
   1.205 -	(atac 1),
   1.206 -	(etac ex_lubcfun 1),
   1.207 -	(atac 1)
   1.208 -	]);
   1.209 +        [
   1.210 +        (cut_facts_tac prems 1),
   1.211 +        (rtac monocontlub2cont 1),
   1.212 +        (etac lub_cfun_mono 1),
   1.213 +        (rtac contlubI 1),
   1.214 +        (strip_tac 1),
   1.215 +        (rtac (contlub_cfun_arg RS ext RS ssubst) 1),
   1.216 +        (atac 1),
   1.217 +        (etac ex_lubcfun 1),
   1.218 +        (atac 1)
   1.219 +        ]);
   1.220  
   1.221  (* ------------------------------------------------------------------------ *)
   1.222  (* type 'a -> 'b is chain complete                                          *)
   1.223 @@ -190,25 +190,25 @@
   1.224  qed_goal "lub_cfun" Cfun2.thy 
   1.225    "is_chain(CCF) ==> range(CCF) <<| (LAM x.lub(range(% i.CCF(i)`x)))"
   1.226  (fn prems =>
   1.227 -	[
   1.228 -	(cut_facts_tac prems 1),
   1.229 -	(rtac is_lubI 1),
   1.230 -	(rtac conjI 1),
   1.231 -	(rtac ub_rangeI 1),  
   1.232 -	(rtac allI 1),
   1.233 -	(rtac (less_cfun RS ssubst) 1),
   1.234 -	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   1.235 -	(etac cont_lubcfun 1),
   1.236 -	(rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
   1.237 -	(etac (monofun_fapp1 RS ch2ch_monofun) 1),
   1.238 -	(strip_tac 1),
   1.239 -	(rtac (less_cfun RS ssubst) 1),
   1.240 -	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   1.241 -	(etac cont_lubcfun 1),
   1.242 -	(rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
   1.243 -	(etac (monofun_fapp1 RS ch2ch_monofun) 1),
   1.244 -	(etac (monofun_fapp1 RS ub2ub_monofun) 1)
   1.245 -	]);
   1.246 +        [
   1.247 +        (cut_facts_tac prems 1),
   1.248 +        (rtac is_lubI 1),
   1.249 +        (rtac conjI 1),
   1.250 +        (rtac ub_rangeI 1),  
   1.251 +        (rtac allI 1),
   1.252 +        (rtac (less_cfun RS ssubst) 1),
   1.253 +        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   1.254 +        (etac cont_lubcfun 1),
   1.255 +        (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
   1.256 +        (etac (monofun_fapp1 RS ch2ch_monofun) 1),
   1.257 +        (strip_tac 1),
   1.258 +        (rtac (less_cfun RS ssubst) 1),
   1.259 +        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   1.260 +        (etac cont_lubcfun 1),
   1.261 +        (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
   1.262 +        (etac (monofun_fapp1 RS ch2ch_monofun) 1),
   1.263 +        (etac (monofun_fapp1 RS ub2ub_monofun) 1)
   1.264 +        ]);
   1.265  
   1.266  val thelub_cfun = (lub_cfun RS thelubI);
   1.267  (* 
   1.268 @@ -218,11 +218,11 @@
   1.269  qed_goal "cpo_cfun" Cfun2.thy 
   1.270    "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
   1.271  (fn prems =>
   1.272 -	[
   1.273 -	(cut_facts_tac prems 1),
   1.274 -	(rtac exI 1),
   1.275 -	(etac lub_cfun 1)
   1.276 -	]);
   1.277 +        [
   1.278 +        (cut_facts_tac prems 1),
   1.279 +        (rtac exI 1),
   1.280 +        (etac lub_cfun 1)
   1.281 +        ]);
   1.282  
   1.283  
   1.284  (* ------------------------------------------------------------------------ *)
   1.285 @@ -231,29 +231,29 @@
   1.286  
   1.287  qed_goal "ext_cfun" Cfun1.thy "(!!x. f`x = g`x) ==> f = g"
   1.288   (fn prems =>
   1.289 -	[
   1.290 -	(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   1.291 -	(res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   1.292 -	(res_inst_tac [("f","fabs")] arg_cong 1),
   1.293 -	(rtac ext 1),
   1.294 -	(resolve_tac prems 1)
   1.295 -	]);
   1.296 +        [
   1.297 +        (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   1.298 +        (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   1.299 +        (res_inst_tac [("f","fabs")] arg_cong 1),
   1.300 +        (rtac ext 1),
   1.301 +        (resolve_tac prems 1)
   1.302 +        ]);
   1.303  
   1.304  (* ------------------------------------------------------------------------ *)
   1.305  (* Monotonicity of fabs                                                     *)
   1.306  (* ------------------------------------------------------------------------ *)
   1.307  
   1.308  qed_goal "semi_monofun_fabs" Cfun2.thy 
   1.309 -	"[|cont(f);cont(g);f<<g|]==>fabs(f)<<fabs(g)"
   1.310 +        "[|cont(f);cont(g);f<<g|]==>fabs(f)<<fabs(g)"
   1.311   (fn prems =>
   1.312 -	[
   1.313 -	(rtac (less_cfun RS iffD2) 1),
   1.314 -	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   1.315 -	(resolve_tac prems 1),
   1.316 -	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   1.317 -	(resolve_tac prems 1),
   1.318 -	(resolve_tac prems 1)
   1.319 -	]);
   1.320 +        [
   1.321 +        (rtac (less_cfun RS iffD2) 1),
   1.322 +        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   1.323 +        (resolve_tac prems 1),
   1.324 +        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
   1.325 +        (resolve_tac prems 1),
   1.326 +        (resolve_tac prems 1)
   1.327 +        ]);
   1.328  
   1.329  (* ------------------------------------------------------------------------ *)
   1.330  (* Extenionality wrt. << in 'a -> 'b                                        *)
   1.331 @@ -261,15 +261,15 @@
   1.332  
   1.333  qed_goal "less_cfun2" Cfun2.thy "(!!x. f`x << g`x) ==> f << g"
   1.334   (fn prems =>
   1.335 -	[
   1.336 -	(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   1.337 -	(res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   1.338 -	(rtac semi_monofun_fabs 1),
   1.339 -	(rtac cont_fapp2 1),
   1.340 -	(rtac cont_fapp2 1),
   1.341 -	(rtac (less_fun RS iffD2) 1),
   1.342 -	(rtac allI 1),
   1.343 -	(resolve_tac prems 1)
   1.344 -	]);
   1.345 +        [
   1.346 +        (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   1.347 +        (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   1.348 +        (rtac semi_monofun_fabs 1),
   1.349 +        (rtac cont_fapp2 1),
   1.350 +        (rtac cont_fapp2 1),
   1.351 +        (rtac (less_fun RS iffD2) 1),
   1.352 +        (rtac allI 1),
   1.353 +        (resolve_tac prems 1)
   1.354 +        ]);
   1.355  
   1.356