src/HOLCF/Sprod2.ML
changeset 243 c22b85994e17
child 892 d0dc8d057929
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/Sprod2.ML	Wed Jan 19 17:35:01 1994 +0100
     1.3 @@ -0,0 +1,274 @@
     1.4 +(*  Title: 	HOLCF/sprod2.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Franz Regensburger
     1.7 +    Copyright   1993 Technische Universitaet Muenchen
     1.8 +
     1.9 +Lemmas for sprod2.thy
    1.10 +*)
    1.11 +
    1.12 +
    1.13 +open Sprod2;
    1.14 +
    1.15 +(* ------------------------------------------------------------------------ *)
    1.16 +(* access to less_sprod in class po                                         *)
    1.17 +(* ------------------------------------------------------------------------ *)
    1.18 +
    1.19 +val less_sprod3a = prove_goal Sprod2.thy 
    1.20 +	"p1=Ispair(UU,UU) ==> p1 << p2"
    1.21 +(fn prems =>
    1.22 +	[
    1.23 +	(cut_facts_tac prems 1),
    1.24 +	(rtac (inst_sprod_po RS ssubst) 1),
    1.25 +	(etac less_sprod1a 1)
    1.26 +	]);
    1.27 +
    1.28 +
    1.29 +val less_sprod3b = prove_goal Sprod2.thy
    1.30 + "~p1=Ispair(UU,UU) ==>\
    1.31 +\	(p1<<p2) = (Isfst(p1)<<Isfst(p2) & Issnd(p1)<<Issnd(p2))" 
    1.32 +(fn prems =>
    1.33 +	[
    1.34 +	(cut_facts_tac prems 1),
    1.35 +	(rtac (inst_sprod_po RS ssubst) 1),
    1.36 +	(etac less_sprod1b 1)
    1.37 +	]);
    1.38 +
    1.39 +val less_sprod4b = prove_goal Sprod2.thy 
    1.40 +	"p << Ispair(UU,UU) ==> p = Ispair(UU,UU)"
    1.41 +(fn prems =>
    1.42 +	[
    1.43 +	(cut_facts_tac prems 1),
    1.44 +	(rtac less_sprod2b 1),
    1.45 +	(etac (inst_sprod_po RS subst) 1)
    1.46 +	]);
    1.47 +
    1.48 +val less_sprod4a = (less_sprod4b RS defined_Ispair_rev);
    1.49 +(* Ispair(?a,?b) << Ispair(UU,UU) ==> ?a = UU | ?b = UU *)
    1.50 +
    1.51 +val less_sprod4c = prove_goal Sprod2.thy
    1.52 + "[|Ispair(xa,ya)<<Ispair(x,y);~xa=UU;~ya=UU;~x=UU;~y=UU|] ==>\
    1.53 +\		xa<<x & ya << y"
    1.54 +(fn prems =>
    1.55 +	[
    1.56 +	(cut_facts_tac prems 1),
    1.57 +	(rtac less_sprod2c 1),
    1.58 +	(etac (inst_sprod_po RS subst) 1),
    1.59 +	(REPEAT (atac 1))
    1.60 +	]);
    1.61 +
    1.62 +(* ------------------------------------------------------------------------ *)
    1.63 +(* type sprod is pointed                                                    *)
    1.64 +(* ------------------------------------------------------------------------ *)
    1.65 +
    1.66 +val minimal_sprod = prove_goal Sprod2.thy  "Ispair(UU,UU)<<p"
    1.67 +(fn prems =>
    1.68 +	[
    1.69 +	(rtac less_sprod3a 1),
    1.70 +	(rtac refl 1)
    1.71 +	]);
    1.72 +
    1.73 +(* ------------------------------------------------------------------------ *)
    1.74 +(* Ispair is monotone in both arguments                                     *)
    1.75 +(* ------------------------------------------------------------------------ *)
    1.76 +
    1.77 +val monofun_Ispair1 = prove_goalw Sprod2.thy [monofun] "monofun(Ispair)"
    1.78 +(fn prems =>
    1.79 +	[
    1.80 +	(strip_tac 1),
    1.81 +	(rtac (less_fun RS iffD2) 1),
    1.82 +	(strip_tac 1),
    1.83 +	(res_inst_tac [("Q",
    1.84 +	" Ispair(y,xa) =Ispair(UU,UU)")] (excluded_middle RS disjE) 1),
    1.85 +	(res_inst_tac [("Q",
    1.86 +	" Ispair(x,xa) =Ispair(UU,UU)")] (excluded_middle RS disjE) 1),
    1.87 +	(rtac (less_sprod3b RS iffD2) 1),
    1.88 +	(atac 1),
    1.89 +	(rtac conjI 1),
    1.90 +	(rtac (Isfst RS ssubst) 1),
    1.91 +	(etac (strict_Ispair_rev RS conjunct1) 1),
    1.92 +	(etac (strict_Ispair_rev RS conjunct2) 1),
    1.93 +	(rtac (Isfst RS ssubst) 1),
    1.94 +	(etac (strict_Ispair_rev RS conjunct1) 1),
    1.95 +	(etac (strict_Ispair_rev RS conjunct2) 1),
    1.96 +	(atac 1),
    1.97 +	(rtac (Issnd RS ssubst) 1),
    1.98 +	(etac (strict_Ispair_rev RS conjunct1) 1),
    1.99 +	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.100 +	(rtac (Issnd RS ssubst) 1),
   1.101 +	(etac (strict_Ispair_rev RS conjunct1) 1),
   1.102 +	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.103 +	(rtac refl_less 1),
   1.104 +	(etac less_sprod3a 1),
   1.105 +	(res_inst_tac [("Q",
   1.106 +	" Ispair(x,xa) =Ispair(UU,UU)")] (excluded_middle RS disjE) 1),
   1.107 +	(etac less_sprod3a 2),
   1.108 +	(res_inst_tac [("P","Ispair(y,xa) = Ispair(UU,UU)")] notE 1),
   1.109 +	(atac 2),
   1.110 +	(rtac defined_Ispair 1),
   1.111 +	(etac notUU_I 1),
   1.112 +	(etac (strict_Ispair_rev RS  conjunct1) 1),
   1.113 +	(etac (strict_Ispair_rev RS  conjunct2) 1)
   1.114 +	]);
   1.115 +
   1.116 +
   1.117 +val monofun_Ispair2 = prove_goalw Sprod2.thy [monofun] "monofun(Ispair(x))"
   1.118 +(fn prems =>
   1.119 +	[
   1.120 +	(strip_tac 1),
   1.121 +	(res_inst_tac [("Q",
   1.122 +	" Ispair(x,y) =Ispair(UU,UU)")] (excluded_middle RS disjE) 1),
   1.123 +	(res_inst_tac [("Q",
   1.124 +	" Ispair(x,xa) =Ispair(UU,UU)")] (excluded_middle RS disjE) 1),
   1.125 +	(rtac (less_sprod3b RS iffD2) 1),
   1.126 +	(atac 1),
   1.127 +	(rtac conjI 1),
   1.128 +	(rtac (Isfst RS ssubst) 1),
   1.129 +	(etac (strict_Ispair_rev RS conjunct1) 1),
   1.130 +	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.131 +	(rtac (Isfst RS ssubst) 1),
   1.132 +	(etac (strict_Ispair_rev RS conjunct1) 1),
   1.133 +	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.134 +	(rtac refl_less 1),
   1.135 +	(rtac (Issnd RS ssubst) 1),
   1.136 +	(etac (strict_Ispair_rev RS conjunct1) 1),
   1.137 +	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.138 +	(rtac (Issnd RS ssubst) 1),
   1.139 +	(etac (strict_Ispair_rev RS conjunct1) 1),
   1.140 +	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.141 +	(atac 1),
   1.142 +	(etac less_sprod3a 1),
   1.143 +	(res_inst_tac [("Q",
   1.144 +	" Ispair(x,xa) =Ispair(UU,UU)")] (excluded_middle RS disjE) 1),
   1.145 +	(etac less_sprod3a 2),
   1.146 +	(res_inst_tac [("P","Ispair(x,y) = Ispair(UU,UU)")] notE 1),
   1.147 +	(atac 2),
   1.148 +	(rtac defined_Ispair 1),
   1.149 +	(etac (strict_Ispair_rev RS  conjunct1) 1),
   1.150 +	(etac notUU_I 1),
   1.151 +	(etac (strict_Ispair_rev RS  conjunct2) 1)
   1.152 +	]);
   1.153 +
   1.154 +val  monofun_Ispair = prove_goal Sprod2.thy 
   1.155 + "[|x1<<x2; y1<<y2|] ==> Ispair(x1,y1)<<Ispair(x2,y2)"
   1.156 +(fn prems =>
   1.157 +	[
   1.158 +	(cut_facts_tac prems 1),
   1.159 +	(rtac trans_less 1),
   1.160 +	(rtac (monofun_Ispair1 RS monofunE RS spec RS spec RS mp RS 
   1.161 +	(less_fun RS iffD1 RS spec)) 1),
   1.162 +	(rtac (monofun_Ispair2 RS monofunE RS spec RS spec RS mp) 2),
   1.163 +	(atac 1),
   1.164 +	(atac 1)
   1.165 +	]);
   1.166 +
   1.167 +
   1.168 +(* ------------------------------------------------------------------------ *)
   1.169 +(* Isfst and Issnd are monotone                                             *)
   1.170 +(* ------------------------------------------------------------------------ *)
   1.171 +
   1.172 +val  monofun_Isfst = prove_goalw Sprod2.thy [monofun] "monofun(Isfst)"
   1.173 +(fn prems =>
   1.174 +	[
   1.175 +	(strip_tac 1),
   1.176 +	(res_inst_tac [("p","x")] IsprodE 1),
   1.177 +	(hyp_subst_tac 1),
   1.178 +	(rtac trans_less 1),
   1.179 +	(rtac minimal 2),
   1.180 +	(rtac (strict_Isfst1 RS ssubst) 1),
   1.181 +	(rtac refl_less 1),
   1.182 +	(hyp_subst_tac 1),
   1.183 +	(res_inst_tac [("p","y")] IsprodE 1),
   1.184 +	(hyp_subst_tac 1),
   1.185 +	(res_inst_tac [("t","Isfst(Ispair(xa,ya))")] subst 1),
   1.186 +	(rtac refl_less 2),
   1.187 +	(etac (less_sprod4b RS sym RS arg_cong) 1),
   1.188 +	(hyp_subst_tac 1),
   1.189 +	(rtac (Isfst RS ssubst) 1),
   1.190 +	(atac 1),
   1.191 +	(atac 1),
   1.192 +	(rtac (Isfst RS ssubst) 1),
   1.193 +	(atac 1),
   1.194 +	(atac 1),
   1.195 +	(etac (less_sprod4c RS  conjunct1) 1),
   1.196 +	(REPEAT (atac 1))
   1.197 +	]);
   1.198 +
   1.199 +val monofun_Issnd = prove_goalw Sprod2.thy [monofun] "monofun(Issnd)"
   1.200 +(fn prems =>
   1.201 +	[
   1.202 +	(strip_tac 1),
   1.203 +	(res_inst_tac [("p","x")] IsprodE 1),
   1.204 +	(hyp_subst_tac 1),
   1.205 +	(rtac trans_less 1),
   1.206 +	(rtac minimal 2),
   1.207 +	(rtac (strict_Issnd1 RS ssubst) 1),
   1.208 +	(rtac refl_less 1),
   1.209 +	(hyp_subst_tac 1),
   1.210 +	(res_inst_tac [("p","y")] IsprodE 1),
   1.211 +	(hyp_subst_tac 1),
   1.212 +	(res_inst_tac [("t","Issnd(Ispair(xa,ya))")] subst 1),
   1.213 +	(rtac refl_less 2),
   1.214 +	(etac (less_sprod4b RS sym RS arg_cong) 1),
   1.215 +	(hyp_subst_tac 1),
   1.216 +	(rtac (Issnd RS ssubst) 1),
   1.217 +	(atac 1),
   1.218 +	(atac 1),
   1.219 +	(rtac (Issnd RS ssubst) 1),
   1.220 +	(atac 1),
   1.221 +	(atac 1),
   1.222 +	(etac (less_sprod4c RS  conjunct2) 1),
   1.223 +	(REPEAT (atac 1))
   1.224 +	]);
   1.225 +
   1.226 +
   1.227 +(* ------------------------------------------------------------------------ *)
   1.228 +(* the type 'a ** 'b is a cpo                                               *)
   1.229 +(* ------------------------------------------------------------------------ *)
   1.230 +
   1.231 +val lub_sprod = prove_goal Sprod2.thy 
   1.232 +"[|is_chain(S)|] ==> range(S) <<| \
   1.233 +\ Ispair(lub(range(%i.Isfst(S(i)))),lub(range(%i.Issnd(S(i)))))"
   1.234 +(fn prems =>
   1.235 +	[
   1.236 +	(cut_facts_tac prems 1),
   1.237 +	(rtac is_lubI 1),
   1.238 +	(rtac conjI 1),
   1.239 +	(rtac ub_rangeI 1),
   1.240 +	(rtac allI 1),
   1.241 +	(res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1),
   1.242 +	(rtac monofun_Ispair 1),
   1.243 +	(rtac is_ub_thelub 1),
   1.244 +	(etac (monofun_Isfst RS ch2ch_monofun) 1),
   1.245 +	(rtac is_ub_thelub 1),
   1.246 +	(etac (monofun_Issnd RS ch2ch_monofun) 1),
   1.247 +	(strip_tac 1),
   1.248 +	(res_inst_tac [("t","u")] (surjective_pairing_Sprod RS ssubst) 1),
   1.249 +	(rtac monofun_Ispair 1),
   1.250 +	(rtac is_lub_thelub 1),
   1.251 +	(etac (monofun_Isfst RS ch2ch_monofun) 1),
   1.252 +	(etac (monofun_Isfst RS ub2ub_monofun) 1),
   1.253 +	(rtac is_lub_thelub 1),
   1.254 +	(etac (monofun_Issnd RS ch2ch_monofun) 1),
   1.255 +	(etac (monofun_Issnd RS ub2ub_monofun) 1)
   1.256 +	]);
   1.257 +
   1.258 +val thelub_sprod = (lub_sprod RS thelubI);
   1.259 +(* is_chain(?S1) ==> lub(range(?S1)) =                                     *)
   1.260 +(* Ispair(lub(range(%i. Isfst(?S1(i)))),lub(range(%i. Issnd(?S1(i)))))     *)
   1.261 +
   1.262 +val cpo_sprod = prove_goal Sprod2.thy 
   1.263 +	"is_chain(S::nat=>'a**'b)==>? x.range(S)<<| x"
   1.264 +(fn prems =>
   1.265 +	[
   1.266 +	(cut_facts_tac prems 1),
   1.267 +	(rtac exI 1),
   1.268 +	(etac lub_sprod 1)
   1.269 +	]);
   1.270 +
   1.271 +
   1.272 +
   1.273 +
   1.274 +
   1.275 +
   1.276 +
   1.277 +