src/HOLCF/Cprod2.ML
changeset 1461 6bcb44e4d6e5
parent 1267 bca91b4e1710
child 1779 1155c06fa956
     1.1 --- a/src/HOLCF/Cprod2.ML	Mon Jan 29 14:16:13 1996 +0100
     1.2 +++ b/src/HOLCF/Cprod2.ML	Tue Jan 30 13:42:57 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	HOLCF/cprod2.ML
     1.5 +(*  Title:      HOLCF/cprod2.ML
     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 cprod2.thy 
    1.12 @@ -9,51 +9,51 @@
    1.13  open Cprod2;
    1.14  
    1.15  qed_goal "less_cprod3a" Cprod2.thy 
    1.16 -	"p1=(UU,UU) ==> p1 << p2"
    1.17 +        "p1=(UU,UU) ==> p1 << p2"
    1.18   (fn prems =>
    1.19 -	[
    1.20 -	(cut_facts_tac prems 1),
    1.21 -	(rtac (inst_cprod_po RS ssubst) 1),
    1.22 -	(rtac (less_cprod1b RS ssubst) 1),
    1.23 -	(hyp_subst_tac 1),
    1.24 -	(Asm_simp_tac  1)
    1.25 -	]);
    1.26 +        [
    1.27 +        (cut_facts_tac prems 1),
    1.28 +        (rtac (inst_cprod_po RS ssubst) 1),
    1.29 +        (rtac (less_cprod1b RS ssubst) 1),
    1.30 +        (hyp_subst_tac 1),
    1.31 +        (Asm_simp_tac  1)
    1.32 +        ]);
    1.33  
    1.34  qed_goal "less_cprod3b" Cprod2.thy
    1.35   "(p1 << p2) = (fst(p1)<<fst(p2) & snd(p1)<<snd(p2))"
    1.36   (fn prems =>
    1.37 -	[
    1.38 -	(rtac (inst_cprod_po RS ssubst) 1),
    1.39 -	(rtac less_cprod1b 1)
    1.40 -	]);
    1.41 +        [
    1.42 +        (rtac (inst_cprod_po RS ssubst) 1),
    1.43 +        (rtac less_cprod1b 1)
    1.44 +        ]);
    1.45  
    1.46  qed_goal "less_cprod4a" Cprod2.thy 
    1.47 -	"(x1,x2) << (UU,UU) ==> x1=UU & x2=UU"
    1.48 +        "(x1,x2) << (UU,UU) ==> x1=UU & x2=UU"
    1.49   (fn prems =>
    1.50 -	[
    1.51 -	(cut_facts_tac prems 1),
    1.52 -	(rtac less_cprod2a 1),
    1.53 -	(etac (inst_cprod_po RS subst) 1)
    1.54 -	]);
    1.55 +        [
    1.56 +        (cut_facts_tac prems 1),
    1.57 +        (rtac less_cprod2a 1),
    1.58 +        (etac (inst_cprod_po RS subst) 1)
    1.59 +        ]);
    1.60  
    1.61  qed_goal "less_cprod4b" Cprod2.thy 
    1.62 -	"p << (UU,UU) ==> p = (UU,UU)"
    1.63 +        "p << (UU,UU) ==> p = (UU,UU)"
    1.64  (fn prems =>
    1.65 -	[
    1.66 -	(cut_facts_tac prems 1),
    1.67 -	(rtac less_cprod2b 1),
    1.68 -	(etac (inst_cprod_po RS subst) 1)
    1.69 -	]);
    1.70 +        [
    1.71 +        (cut_facts_tac prems 1),
    1.72 +        (rtac less_cprod2b 1),
    1.73 +        (etac (inst_cprod_po RS subst) 1)
    1.74 +        ]);
    1.75  
    1.76  qed_goal "less_cprod4c" Cprod2.thy
    1.77   " (xa,ya) << (x,y) ==> xa<<x & ya << y"
    1.78  (fn prems =>
    1.79 -	[
    1.80 -	(cut_facts_tac prems 1),
    1.81 -	(rtac less_cprod2c 1),
    1.82 -	(etac (inst_cprod_po RS subst) 1),
    1.83 -	(REPEAT (atac 1))
    1.84 -	]);
    1.85 +        [
    1.86 +        (cut_facts_tac prems 1),
    1.87 +        (rtac less_cprod2c 1),
    1.88 +        (etac (inst_cprod_po RS subst) 1),
    1.89 +        (REPEAT (atac 1))
    1.90 +        ]);
    1.91  
    1.92  (* ------------------------------------------------------------------------ *)
    1.93  (* type cprod is pointed                                                    *)
    1.94 @@ -61,10 +61,10 @@
    1.95  
    1.96  qed_goal "minimal_cprod" Cprod2.thy  "(UU,UU)<<p"
    1.97  (fn prems =>
    1.98 -	[
    1.99 -	(rtac less_cprod3a 1),
   1.100 -	(rtac refl 1)
   1.101 -	]);
   1.102 +        [
   1.103 +        (rtac less_cprod3a 1),
   1.104 +        (rtac refl 1)
   1.105 +        ]);
   1.106  
   1.107  (* ------------------------------------------------------------------------ *)
   1.108  (* Pair <_,_>  is monotone in both arguments                                *)
   1.109 @@ -72,34 +72,34 @@
   1.110  
   1.111  qed_goalw "monofun_pair1" Cprod2.thy [monofun] "monofun(Pair)"
   1.112   (fn prems =>
   1.113 -	[
   1.114 -	(strip_tac 1),
   1.115 -	(rtac (less_fun RS iffD2) 1),
   1.116 -	(strip_tac 1),
   1.117 -	(rtac (less_cprod3b RS iffD2) 1),
   1.118 -	(Simp_tac 1)
   1.119 -	]);
   1.120 +        [
   1.121 +        (strip_tac 1),
   1.122 +        (rtac (less_fun RS iffD2) 1),
   1.123 +        (strip_tac 1),
   1.124 +        (rtac (less_cprod3b RS iffD2) 1),
   1.125 +        (Simp_tac 1)
   1.126 +        ]);
   1.127  
   1.128  qed_goalw "monofun_pair2" Cprod2.thy [monofun] "monofun(Pair(x))"
   1.129   (fn prems =>
   1.130 -	[
   1.131 -	(strip_tac 1),
   1.132 -	(rtac (less_cprod3b RS iffD2) 1),
   1.133 -	(Simp_tac 1)
   1.134 -	]);
   1.135 +        [
   1.136 +        (strip_tac 1),
   1.137 +        (rtac (less_cprod3b RS iffD2) 1),
   1.138 +        (Simp_tac 1)
   1.139 +        ]);
   1.140  
   1.141  qed_goal "monofun_pair" Cprod2.thy 
   1.142   "[|x1<<x2; y1<<y2|] ==> (x1,y1) << (x2,y2)"
   1.143   (fn prems =>
   1.144 -	[
   1.145 -	(cut_facts_tac prems 1),
   1.146 -	(rtac trans_less 1),
   1.147 -	(rtac (monofun_pair1 RS monofunE RS spec RS spec RS mp RS 
   1.148 -	(less_fun RS iffD1 RS spec)) 1),
   1.149 -	(rtac (monofun_pair2 RS monofunE RS spec RS spec RS mp) 2),
   1.150 -	(atac 1),
   1.151 -	(atac 1)
   1.152 -	]);
   1.153 +        [
   1.154 +        (cut_facts_tac prems 1),
   1.155 +        (rtac trans_less 1),
   1.156 +        (rtac (monofun_pair1 RS monofunE RS spec RS spec RS mp RS 
   1.157 +        (less_fun RS iffD1 RS spec)) 1),
   1.158 +        (rtac (monofun_pair2 RS monofunE RS spec RS spec RS mp) 2),
   1.159 +        (atac 1),
   1.160 +        (atac 1)
   1.161 +        ]);
   1.162  
   1.163  (* ------------------------------------------------------------------------ *)
   1.164  (* fst and snd are monotone                                                 *)
   1.165 @@ -107,27 +107,27 @@
   1.166  
   1.167  qed_goalw "monofun_fst" Cprod2.thy [monofun] "monofun(fst)"
   1.168   (fn prems =>
   1.169 -	[
   1.170 -	(strip_tac 1),
   1.171 -	(res_inst_tac [("p","x")] PairE 1),
   1.172 -	(hyp_subst_tac 1),
   1.173 -	(res_inst_tac [("p","y")] PairE 1),
   1.174 -	(hyp_subst_tac 1),
   1.175 -	(Asm_simp_tac  1),
   1.176 -	(etac (less_cprod4c RS conjunct1) 1)
   1.177 -	]);
   1.178 +        [
   1.179 +        (strip_tac 1),
   1.180 +        (res_inst_tac [("p","x")] PairE 1),
   1.181 +        (hyp_subst_tac 1),
   1.182 +        (res_inst_tac [("p","y")] PairE 1),
   1.183 +        (hyp_subst_tac 1),
   1.184 +        (Asm_simp_tac  1),
   1.185 +        (etac (less_cprod4c RS conjunct1) 1)
   1.186 +        ]);
   1.187  
   1.188  qed_goalw "monofun_snd" Cprod2.thy [monofun] "monofun(snd)"
   1.189   (fn prems =>
   1.190 -	[
   1.191 -	(strip_tac 1),
   1.192 -	(res_inst_tac [("p","x")] PairE 1),
   1.193 -	(hyp_subst_tac 1),
   1.194 -	(res_inst_tac [("p","y")] PairE 1),
   1.195 -	(hyp_subst_tac 1),
   1.196 -	(Asm_simp_tac  1),
   1.197 -	(etac (less_cprod4c RS conjunct2) 1)
   1.198 -	]);
   1.199 +        [
   1.200 +        (strip_tac 1),
   1.201 +        (res_inst_tac [("p","x")] PairE 1),
   1.202 +        (hyp_subst_tac 1),
   1.203 +        (res_inst_tac [("p","y")] PairE 1),
   1.204 +        (hyp_subst_tac 1),
   1.205 +        (Asm_simp_tac  1),
   1.206 +        (etac (less_cprod4c RS conjunct2) 1)
   1.207 +        ]);
   1.208  
   1.209  (* ------------------------------------------------------------------------ *)
   1.210  (* the type 'a * 'b is a cpo                                                *)
   1.211 @@ -137,28 +137,28 @@
   1.212  " is_chain(S) ==> range(S) <<| \
   1.213  \   (lub(range(%i.fst(S i))),lub(range(%i.snd(S i)))) "
   1.214   (fn prems =>
   1.215 -	[
   1.216 -	(cut_facts_tac prems 1),
   1.217 -	(rtac is_lubI 1),
   1.218 -	(rtac conjI 1),
   1.219 -	(rtac ub_rangeI 1),
   1.220 -	(rtac allI 1),
   1.221 -	(res_inst_tac [("t","S(i)")] (surjective_pairing RS ssubst) 1),
   1.222 -	(rtac monofun_pair 1),
   1.223 -	(rtac is_ub_thelub 1),
   1.224 -	(etac (monofun_fst RS ch2ch_monofun) 1),
   1.225 -	(rtac is_ub_thelub 1),
   1.226 -	(etac (monofun_snd RS ch2ch_monofun) 1),
   1.227 -	(strip_tac 1),
   1.228 -	(res_inst_tac [("t","u")] (surjective_pairing RS ssubst) 1),
   1.229 -	(rtac monofun_pair 1),
   1.230 -	(rtac is_lub_thelub 1),
   1.231 -	(etac (monofun_fst RS ch2ch_monofun) 1),
   1.232 -	(etac (monofun_fst RS ub2ub_monofun) 1),
   1.233 -	(rtac is_lub_thelub 1),
   1.234 -	(etac (monofun_snd RS ch2ch_monofun) 1),
   1.235 -	(etac (monofun_snd RS ub2ub_monofun) 1)
   1.236 -	]);
   1.237 +        [
   1.238 +        (cut_facts_tac prems 1),
   1.239 +        (rtac is_lubI 1),
   1.240 +        (rtac conjI 1),
   1.241 +        (rtac ub_rangeI 1),
   1.242 +        (rtac allI 1),
   1.243 +        (res_inst_tac [("t","S(i)")] (surjective_pairing RS ssubst) 1),
   1.244 +        (rtac monofun_pair 1),
   1.245 +        (rtac is_ub_thelub 1),
   1.246 +        (etac (monofun_fst RS ch2ch_monofun) 1),
   1.247 +        (rtac is_ub_thelub 1),
   1.248 +        (etac (monofun_snd RS ch2ch_monofun) 1),
   1.249 +        (strip_tac 1),
   1.250 +        (res_inst_tac [("t","u")] (surjective_pairing RS ssubst) 1),
   1.251 +        (rtac monofun_pair 1),
   1.252 +        (rtac is_lub_thelub 1),
   1.253 +        (etac (monofun_fst RS ch2ch_monofun) 1),
   1.254 +        (etac (monofun_fst RS ub2ub_monofun) 1),
   1.255 +        (rtac is_lub_thelub 1),
   1.256 +        (etac (monofun_snd RS ch2ch_monofun) 1),
   1.257 +        (etac (monofun_snd RS ub2ub_monofun) 1)
   1.258 +        ]);
   1.259  
   1.260  val thelub_cprod = (lub_cprod RS thelubI);
   1.261  (*
   1.262 @@ -169,12 +169,12 @@
   1.263  *)
   1.264  
   1.265  qed_goal "cpo_cprod" Cprod2.thy 
   1.266 -	"is_chain(S::nat=>'a*'b)==>? x.range(S)<<| x"
   1.267 +        "is_chain(S::nat=>'a*'b)==>? x.range(S)<<| x"
   1.268  (fn prems =>
   1.269 -	[
   1.270 -	(cut_facts_tac prems 1),
   1.271 -	(rtac exI 1),
   1.272 -	(etac lub_cprod 1)
   1.273 -	]);
   1.274 +        [
   1.275 +        (cut_facts_tac prems 1),
   1.276 +        (rtac exI 1),
   1.277 +        (etac lub_cprod 1)
   1.278 +        ]);
   1.279  
   1.280