101 "Rp(D,E,e) == THE p. projpair(D,E,e,p)" |
101 "Rp(D,E,e) == THE p. projpair(D,E,e,p)" |
102 |
102 |
103 (* Twice, constructions on cpos are more difficult. *) |
103 (* Twice, constructions on cpos are more difficult. *) |
104 iprod :: "i=>i" |
104 iprod :: "i=>i" |
105 "iprod(DD) == |
105 "iprod(DD) == |
106 <(\<Pi>n \<in> nat. set(DD`n)), |
106 <(\<Pi> n \<in> nat. set(DD`n)), |
107 {x:(\<Pi>n \<in> nat. set(DD`n))*(\<Pi>n \<in> nat. set(DD`n)). |
107 {x:(\<Pi> n \<in> nat. set(DD`n))*(\<Pi> n \<in> nat. set(DD`n)). |
108 \<forall>n \<in> nat. rel(DD`n,fst(x)`n,snd(x)`n)}>" |
108 \<forall>n \<in> nat. rel(DD`n,fst(x)`n,snd(x)`n)}>" |
109 |
109 |
110 mkcpo :: "[i,i=>o]=>i" |
110 mkcpo :: "[i,i=>o]=>i" |
111 (* Cannot use rel(D), is meta fun, need two more args *) |
111 (* Cannot use rel(D), is meta fun, need two more args *) |
112 "mkcpo(D,P) == |
112 "mkcpo(D,P) == |
1022 (*----------------------------------------------------------------------*) |
1022 (*----------------------------------------------------------------------*) |
1023 (* Infinite cartesian product. *) |
1023 (* Infinite cartesian product. *) |
1024 (*----------------------------------------------------------------------*) |
1024 (*----------------------------------------------------------------------*) |
1025 |
1025 |
1026 lemma iprodI: |
1026 lemma iprodI: |
1027 "x:(\<Pi>n \<in> nat. set(DD`n)) ==> x \<in> set(iprod(DD))" |
1027 "x:(\<Pi> n \<in> nat. set(DD`n)) ==> x \<in> set(iprod(DD))" |
1028 by (simp add: set_def iprod_def) |
1028 by (simp add: set_def iprod_def) |
1029 |
1029 |
1030 lemma iprodE: |
1030 lemma iprodE: |
1031 "x \<in> set(iprod(DD)) ==> x:(\<Pi>n \<in> nat. set(DD`n))" |
1031 "x \<in> set(iprod(DD)) ==> x:(\<Pi> n \<in> nat. set(DD`n))" |
1032 by (simp add: set_def iprod_def) |
1032 by (simp add: set_def iprod_def) |
1033 |
1033 |
1034 (* Contains typing conditions in contrast to HOL-ST *) |
1034 (* Contains typing conditions in contrast to HOL-ST *) |
1035 |
1035 |
1036 lemma rel_iprodI: |
1036 lemma rel_iprodI: |
1037 "[|!!n. n \<in> nat ==> rel(DD`n,f`n,g`n); f:(\<Pi>n \<in> nat. set(DD`n)); |
1037 "[|!!n. n \<in> nat ==> rel(DD`n,f`n,g`n); f:(\<Pi> n \<in> nat. set(DD`n)); |
1038 g:(\<Pi>n \<in> nat. set(DD`n))|] ==> rel(iprod(DD),f,g)" |
1038 g:(\<Pi> n \<in> nat. set(DD`n))|] ==> rel(iprod(DD),f,g)" |
1039 by (simp add: iprod_def rel_I) |
1039 by (simp add: iprod_def rel_I) |
1040 |
1040 |
1041 lemma rel_iprodE: |
1041 lemma rel_iprodE: |
1042 "[|rel(iprod(DD),f,g); n \<in> nat|] ==> rel(DD`n,f`n,g`n)" |
1042 "[|rel(iprod(DD),f,g); n \<in> nat|] ==> rel(DD`n,f`n,g`n)" |
1043 by (simp add: iprod_def rel_def) |
1043 by (simp add: iprod_def rel_def) |
1203 (*----------------------------------------------------------------------*) |
1203 (*----------------------------------------------------------------------*) |
1204 (* Dinf, the inverse Limit. *) |
1204 (* Dinf, the inverse Limit. *) |
1205 (*----------------------------------------------------------------------*) |
1205 (*----------------------------------------------------------------------*) |
1206 |
1206 |
1207 lemma DinfI: |
1207 lemma DinfI: |
1208 "[|x:(\<Pi>n \<in> nat. set(DD`n)); |
1208 "[|x:(\<Pi> n \<in> nat. set(DD`n)); |
1209 !!n. n \<in> nat ==> Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n|] |
1209 !!n. n \<in> nat ==> Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n|] |
1210 ==> x \<in> set(Dinf(DD,ee))" |
1210 ==> x \<in> set(Dinf(DD,ee))" |
1211 apply (simp add: Dinf_def) |
1211 apply (simp add: Dinf_def) |
1212 apply (blast intro: mkcpoI iprodI) |
1212 apply (blast intro: mkcpoI iprodI) |
1213 done |
1213 done |
1214 |
1214 |
1215 lemma Dinf_prod: "x \<in> set(Dinf(DD,ee)) ==> x:(\<Pi>n \<in> nat. set(DD`n))" |
1215 lemma Dinf_prod: "x \<in> set(Dinf(DD,ee)) ==> x:(\<Pi> n \<in> nat. set(DD`n))" |
1216 apply (simp add: Dinf_def) |
1216 apply (simp add: Dinf_def) |
1217 apply (erule mkcpoD1 [THEN iprodE]) |
1217 apply (erule mkcpoD1 [THEN iprodE]) |
1218 done |
1218 done |
1219 |
1219 |
1220 lemma Dinf_eq: |
1220 lemma Dinf_eq: |
1224 apply (blast dest: mkcpoD2) |
1224 apply (blast dest: mkcpoD2) |
1225 done |
1225 done |
1226 |
1226 |
1227 lemma rel_DinfI: |
1227 lemma rel_DinfI: |
1228 "[|!!n. n \<in> nat ==> rel(DD`n,x`n,y`n); |
1228 "[|!!n. n \<in> nat ==> rel(DD`n,x`n,y`n); |
1229 x:(\<Pi>n \<in> nat. set(DD`n)); y:(\<Pi>n \<in> nat. set(DD`n))|] |
1229 x:(\<Pi> n \<in> nat. set(DD`n)); y:(\<Pi> n \<in> nat. set(DD`n))|] |
1230 ==> rel(Dinf(DD,ee),x,y)" |
1230 ==> rel(Dinf(DD,ee),x,y)" |
1231 apply (simp add: Dinf_def) |
1231 apply (simp add: Dinf_def) |
1232 apply (blast intro: rel_mkcpo [THEN iffD2] rel_iprodI iprodI) |
1232 apply (blast intro: rel_mkcpo [THEN iffD2] rel_iprodI iprodI) |
1233 done |
1233 done |
1234 |
1234 |