1 (* Title: ZF/ex/Limit |
1 (* Title: ZF/ex/Limit.thy |
2 ID: $Id$ |
|
3 Author: Sten Agerholm |
2 Author: Sten Agerholm |
4 |
3 Author: Lawrence C Paulson |
5 A formalization of the inverse limit construction of domain theory. |
4 |
6 |
5 A formalization of the inverse limit construction of domain theory. |
7 The following paper comments on the formalization: |
6 |
8 |
7 The following paper comments on the formalization: |
9 "A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm |
8 |
10 In Proceedings of the First Isabelle Users Workshop, Technical |
9 "A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm |
11 Report No. 379, University of Cambridge Computer Laboratory, 1995. |
10 In Proceedings of the First Isabelle Users Workshop, Technical |
12 |
11 Report No. 379, University of Cambridge Computer Laboratory, 1995. |
13 This is a condensed version of: |
12 |
14 |
13 This is a condensed version of: |
15 "A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm |
14 |
16 Technical Report No. 369, University of Cambridge Computer |
15 "A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm |
17 Laboratory, 1995. |
16 Technical Report No. 369, University of Cambridge Computer |
18 |
17 Laboratory, 1995. |
19 (Proofs converted to Isar and tidied up considerably by lcp) |
|
20 *) |
18 *) |
21 |
19 |
22 theory Limit imports Main begin |
20 theory Limit imports Main begin |
23 |
21 |
24 definition |
22 definition |
521 and rel: "\<forall>n\<in>nat. rel(D, M ` n ` n, y)" |
519 and rel: "\<forall>n\<in>nat. rel(D, M ` n ` n, y)" |
522 have "rel(D, lub(D, M ` n), y)" |
520 have "rel(D, lub(D, M ` n), y)" |
523 proof (rule matrix_chain_left [THEN cpo_lub, THEN islub_least], simp_all add: n D DM) |
521 proof (rule matrix_chain_left [THEN cpo_lub, THEN islub_least], simp_all add: n D DM) |
524 show "isub(D, M ` n, y)" |
522 show "isub(D, M ` n, y)" |
525 proof (unfold isub_def, intro conjI ballI y) |
523 proof (unfold isub_def, intro conjI ballI y) |
526 fix k assume k: "k \<in> nat" |
524 fix k assume k: "k \<in> nat" |
527 show "rel(D, M ` n ` k, y)" |
525 show "rel(D, M ` n ` k, y)" |
528 proof (cases "n le k") |
526 proof (cases "n le k") |
529 case True |
527 case True |
530 hence yy: "rel(D, M`n`k, M`k`k)" |
528 hence yy: "rel(D, M`n`k, M`k`k)" |
531 by (blast intro: lemma2 n k y DM D chain_rel_gen matrix_chain_right) |
529 by (blast intro: lemma2 n k y DM D chain_rel_gen matrix_chain_right) |
532 show "?thesis" |
530 show "?thesis" |
533 by (rule cpo_trans [OF D yy], |
531 by (rule cpo_trans [OF D yy], |
534 simp_all add: k rel n y DM matrix_in) |
532 simp_all add: k rel n y DM matrix_in) |
535 next |
533 next |
536 case False |
534 case False |
537 hence le: "k le n" |
535 hence le: "k le n" |
538 by (blast intro: not_le_iff_lt [THEN iffD1, THEN leI] nat_into_Ord n k) |
536 by (blast intro: not_le_iff_lt [THEN iffD1, THEN leI] nat_into_Ord n k) |
539 show "?thesis" |
537 show "?thesis" |
540 by (rule cpo_trans [OF D chain_rel_gen [OF le]], |
538 by (rule cpo_trans [OF D chain_rel_gen [OF le]], |
541 simp_all add: n y k rel DM D matrix_chain_left) |
539 simp_all add: n y k rel DM D matrix_chain_left) |
542 qed |
540 qed |
543 qed |
541 qed |
544 qed |
542 qed |
545 moreover |
543 moreover |
546 have "M ` n \<in> nat \<rightarrow> set(D)" by (blast intro: DM n matrix_fun [THEN apply_type]) |
544 have "M ` n \<in> nat \<rightarrow> set(D)" by (blast intro: DM n matrix_fun [THEN apply_type]) |
547 ultimately show "rel(D, lub(D, Lambda(nat, op `(M ` n))), y)" by simp |
545 ultimately show "rel(D, lub(D, Lambda(nat, op `(M ` n))), y)" by simp |
548 qed |
546 qed |
950 could be exploited?*} |
948 could be exploited?*} |
951 lemma projpair_unique_aux2: |
949 lemma projpair_unique_aux2: |
952 "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p'); |
950 "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p'); |
953 rel(cf(E,D),p',p)|] ==> rel(cf(D,E),e,e')" |
951 rel(cf(E,D),p',p)|] ==> rel(cf(D,E),e,e')" |
954 apply (rule_tac b=e |
952 apply (rule_tac b=e |
955 in projpair_e_cont [THEN cont_fun, THEN comp_id, THEN subst], |
953 in projpair_e_cont [THEN cont_fun, THEN comp_id, THEN subst], |
956 assumption) |
954 assumption) |
957 apply (rule_tac e1=e' in projpair_eq [THEN subst], assumption) |
955 apply (rule_tac e1=e' in projpair_eq [THEN subst], assumption) |
958 apply (rule cpo_trans) |
956 apply (rule cpo_trans) |
959 apply (assumption | rule cpo_cf)+ |
957 apply (assumption | rule cpo_cf)+ |
960 apply (rule_tac [4] f = "(e O p) O e'" in cont_cf) |
958 apply (rule_tac [4] f = "(e O p) O e'" in cont_cf) |
1111 apply (rule rel_iprodI, simp) |
1109 apply (rule rel_iprodI, simp) |
1112 (*looks like something should be inserted into the assumptions!*) |
1110 (*looks like something should be inserted into the assumptions!*) |
1113 apply (rule_tac P = "%t. rel (DD`na,t,lub (DD`na,\<lambda>x \<in> nat. X`x`na))" |
1111 apply (rule_tac P = "%t. rel (DD`na,t,lub (DD`na,\<lambda>x \<in> nat. X`x`na))" |
1114 and b1 = "%n. X`n`na" in beta [THEN subst]) |
1112 and b1 = "%n. X`n`na" in beta [THEN subst]) |
1115 apply (simp del: beta_if |
1113 apply (simp del: beta_if |
1116 add: chain_iprod [THEN cpo_lub, THEN islub_ub] iprodE |
1114 add: chain_iprod [THEN cpo_lub, THEN islub_ub] iprodE |
1117 chain_in)+ |
1115 chain_in)+ |
1118 apply (blast intro: iprodI lam_type chain_iprod [THEN cpo_lub, THEN islub_in]) |
1116 apply (blast intro: iprodI lam_type chain_iprod [THEN cpo_lub, THEN islub_in]) |
1119 apply (rule rel_iprodI) |
1117 apply (rule rel_iprodI) |
1120 apply (simp | rule islub_least chain_iprod [THEN cpo_lub])+ |
1118 apply (simp | rule islub_least chain_iprod [THEN cpo_lub])+ |
1121 apply (simp add: isub_def, safe) |
1119 apply (simp add: isub_def, safe) |
1412 apply (subst e_less_le) |
1410 apply (subst e_less_le) |
1413 apply (assumption | rule add_le_mono nat_le_refl add_type nat_succI)+ |
1411 apply (assumption | rule add_le_mono nat_le_refl add_type nat_succI)+ |
1414 apply (subst comp_assoc) |
1412 apply (subst comp_assoc) |
1415 apply (assumption | rule comp_mono_eq refl)+ |
1413 apply (assumption | rule comp_mono_eq refl)+ |
1416 apply (simp del: add_succ_right add: add_succ_right [symmetric] |
1414 apply (simp del: add_succ_right add: add_succ_right [symmetric] |
1417 add: e_less_eq add_type nat_succI) |
1415 add: e_less_eq add_type nat_succI) |
1418 apply (subst id_comp) (* simp cannot unify/inst right, use brr below (?) . *) |
1416 apply (subst id_comp) (* simp cannot unify/inst right, use brr below (?) . *) |
1419 apply (assumption | |
1417 apply (assumption | |
1420 rule emb_e_less_add [THEN emb_cont, THEN cont_fun] refl nat_succI)+ |
1418 rule emb_e_less_add [THEN emb_cont, THEN cont_fun] refl nat_succI)+ |
1421 done |
1419 done |
1422 |
1420 |
1485 apply (assumption | rule add_le_mono nat_le_refl add_type nat_succI)+ |
1483 apply (assumption | rule add_le_mono nat_le_refl add_type nat_succI)+ |
1486 apply (subst comp_assoc) |
1484 apply (subst comp_assoc) |
1487 apply (assumption | rule comp_mono_eq refl)+ |
1485 apply (assumption | rule comp_mono_eq refl)+ |
1488 (* New direct subgoal *) |
1486 (* New direct subgoal *) |
1489 apply (simp del: add_succ_right add: add_succ_right [symmetric] |
1487 apply (simp del: add_succ_right add: add_succ_right [symmetric] |
1490 add: e_gr_eq) |
1488 add: e_gr_eq) |
1491 apply (subst comp_id) (* simp cannot unify/inst right, use brr below (?) . *) |
1489 apply (subst comp_id) (* simp cannot unify/inst right, use brr below (?) . *) |
1492 apply (assumption | rule e_gr_fun add_type refl add_le_self nat_succI)+ |
1490 apply (assumption | rule e_gr_fun add_type refl add_le_self nat_succI)+ |
1493 done |
1491 done |
1494 |
1492 |
1495 lemma e_gr_split_add: |
1493 lemma e_gr_split_add: |
1539 apply (assumption | rule emb_chain_emb add_type emb_chain_cpo nat_succI)+ |
1537 apply (assumption | rule emb_chain_emb add_type emb_chain_cpo nat_succI)+ |
1540 apply (subst id_comp) |
1538 apply (subst id_comp) |
1541 apply (blast intro: e_less_cont [THEN cont_fun] add_le_self) |
1539 apply (blast intro: e_less_cont [THEN cont_fun] add_le_self) |
1542 apply (rule refl) |
1540 apply (rule refl) |
1543 apply (simp del: add_succ_right add: add_succ_right [symmetric] |
1541 apply (simp del: add_succ_right add: add_succ_right [symmetric] |
1544 add: e_gr_eq) |
1542 add: e_gr_eq) |
1545 apply (blast intro: id_comp [symmetric] e_less_cont [THEN cont_fun] |
1543 apply (blast intro: id_comp [symmetric] e_less_cont [THEN cont_fun] |
1546 add_le_self) |
1544 add_le_self) |
1547 done |
1545 done |
1548 |
1546 |
1549 (* Again considerably shorter, and easy to obtain from the previous thm. *) |
1547 (* Again considerably shorter, and easy to obtain from the previous thm. *) |
2110 "[| commute(DD,ee,E,r); commute(DD,ee,G,f); |
2108 "[| commute(DD,ee,E,r); commute(DD,ee,G,f); |
2111 emb_chain(DD,ee); cpo(E); cpo(G) |] |
2109 emb_chain(DD,ee); cpo(E); cpo(G) |] |
2112 ==> chain(cf(G,E),\<lambda>n \<in> nat. r(n) O Rp(DD`n,G,f(n)))" |
2110 ==> chain(cf(G,E),\<lambda>n \<in> nat. r(n) O Rp(DD`n,G,f(n)))" |
2113 apply (rule chainI) |
2111 apply (rule chainI) |
2114 apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont |
2112 apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont |
2115 emb_cont emb_chain_cpo, simp) |
2113 emb_cont emb_chain_cpo, simp) |
2116 apply (rule_tac r1 = r and m1 = n in commute_eq [THEN subst]) |
2114 apply (rule_tac r1 = r and m1 = n in commute_eq [THEN subst]) |
2117 apply (rule_tac [5] r1 = f and m1 = n in commute_eq [THEN subst]) |
2115 apply (rule_tac [5] r1 = f and m1 = n in commute_eq [THEN subst]) |
2118 apply (assumption | rule le_succ nat_succI)+ |
2116 apply (assumption | rule le_succ nat_succI)+ |
2119 apply (subst Rp_comp) |
2117 apply (subst Rp_comp) |
2120 apply (assumption | rule emb_eps commute_emb emb_chain_cpo le_succ nat_succI)+ |
2118 apply (assumption | rule emb_eps commute_emb emb_chain_cpo le_succ nat_succI)+ |
2121 apply (rule comp_assoc [THEN subst]) (* comp_assoc is simpler in Isa *) |
2119 apply (rule comp_assoc [THEN subst]) (* comp_assoc is simpler in Isa *) |
2122 apply (rule_tac r1 = "r (succ (n))" in comp_assoc [THEN ssubst]) |
2120 apply (rule_tac r1 = "r (succ (n))" in comp_assoc [THEN ssubst]) |
2123 apply (rule comp_mono) |
2121 apply (rule comp_mono) |
2124 apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont |
2122 apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont |
2125 emb_cont emb_chain_cpo le_succ)+ |
2123 emb_cont emb_chain_cpo le_succ)+ |
2126 apply (rule_tac b="r(succ(n))" in comp_id [THEN subst]) (* 1 subst too much *) |
2124 apply (rule_tac b="r(succ(n))" in comp_id [THEN subst]) (* 1 subst too much *) |
2127 apply (rule_tac [2] comp_mono) |
2125 apply (rule_tac [2] comp_mono) |
2128 apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb |
2126 apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb |
2129 Rp_cont emb_cont cont_fun emb_chain_cpo le_succ)+ |
2127 Rp_cont emb_cont cont_fun emb_chain_cpo le_succ)+ |
2130 apply (subst comp_id) (* Undoes "1 subst too much", typing next anyway *) |
2128 apply (subst comp_id) (* Undoes "1 subst too much", typing next anyway *) |
2131 apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf |
2129 apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf |
2132 emb_chain_cpo embRp_rel emb_eps le_succ)+ |
2130 emb_chain_cpo embRp_rel emb_eps le_succ)+ |
2133 done |
2131 done |
2134 |
2132 |
2156 lemma theta_projpair: |
2154 lemma theta_projpair: |
2157 "[| lub(cf(E,E), \<lambda>n \<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E)); |
2155 "[| lub(cf(E,E), \<lambda>n \<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E)); |
2158 commute(DD,ee,E,r); commute(DD,ee,G,f); |
2156 commute(DD,ee,E,r); commute(DD,ee,G,f); |
2159 emb_chain(DD,ee); cpo(E); cpo(G) |] |
2157 emb_chain(DD,ee); cpo(E); cpo(G) |] |
2160 ==> projpair |
2158 ==> projpair |
2161 (E,G, |
2159 (E,G, |
2162 lub(cf(E,G), \<lambda>n \<in> nat. f(n) O Rp(DD`n,E,r(n))), |
2160 lub(cf(E,G), \<lambda>n \<in> nat. f(n) O Rp(DD`n,E,r(n))), |
2163 lub(cf(G,E), \<lambda>n \<in> nat. r(n) O Rp(DD`n,G,f(n))))" |
2161 lub(cf(G,E), \<lambda>n \<in> nat. r(n) O Rp(DD`n,G,f(n))))" |
2164 apply (simp add: projpair_def rho_proj_def, safe) |
2162 apply (simp add: projpair_def rho_proj_def, safe) |
2165 apply (rule_tac [3] comp_lubs [THEN ssubst]) |
2163 apply (rule_tac [3] comp_lubs [THEN ssubst]) |
2166 (* The following one line is 15 lines in HOL, and includes existentials. *) |
2164 (* The following one line is 15 lines in HOL, and includes existentials. *) |
2167 apply (assumption | |
2165 apply (assumption | |
2168 rule cf_cont islub_in cpo_lub cpo_cf theta_chain theta_proj_chain)+ |
2166 rule cf_cont islub_in cpo_lub cpo_cf theta_chain theta_proj_chain)+ |
2183 apply (blast intro: embRp_rel commute_emb emb_chain_cpo) |
2181 apply (blast intro: embRp_rel commute_emb emb_chain_cpo) |
2184 done |
2182 done |
2185 |
2183 |
2186 lemma emb_theta: |
2184 lemma emb_theta: |
2187 "[| lub(cf(E,E), \<lambda>n \<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E)); |
2185 "[| lub(cf(E,E), \<lambda>n \<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E)); |
2188 commute(DD,ee,E,r); commute(DD,ee,G,f); |
2186 commute(DD,ee,E,r); commute(DD,ee,G,f); |
2189 emb_chain(DD,ee); cpo(E); cpo(G) |] |
2187 emb_chain(DD,ee); cpo(E); cpo(G) |] |
2190 ==> emb(E,G,lub(cf(E,G), \<lambda>n \<in> nat. f(n) O Rp(DD`n,E,r(n))))" |
2188 ==> emb(E,G,lub(cf(E,G), \<lambda>n \<in> nat. f(n) O Rp(DD`n,E,r(n))))" |
2191 apply (simp add: emb_def) |
2189 apply (simp add: emb_def) |
2192 apply (blast intro: theta_projpair) |
2190 apply (blast intro: theta_projpair) |
2193 done |
2191 done |
2194 |
2192 |
2269 emb_chain_cpo) |
2267 emb_chain_cpo) |
2270 done |
2268 done |
2271 |
2269 |
2272 lemma lub_universal_unique: |
2270 lemma lub_universal_unique: |
2273 "[| mediating(E,G,r,f,t); |
2271 "[| mediating(E,G,r,f,t); |
2274 lub(cf(E,E), \<lambda>n \<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E)); |
2272 lub(cf(E,E), \<lambda>n \<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E)); |
2275 commute(DD,ee,E,r); commute(DD,ee,G,f); |
2273 commute(DD,ee,E,r); commute(DD,ee,G,f); |
2276 emb_chain(DD,ee); cpo(E); cpo(G) |] |
2274 emb_chain(DD,ee); cpo(E); cpo(G) |] |
2277 ==> t = lub(cf(E,G), \<lambda>n \<in> nat. f(n) O Rp(DD`n,E,r(n)))" |
2275 ==> t = lub(cf(E,G), \<lambda>n \<in> nat. f(n) O Rp(DD`n,E,r(n)))" |
2278 apply (rule_tac b = t in comp_id [THEN subst]) |
2276 apply (rule_tac b = t in comp_id [THEN subst]) |
2279 apply (erule_tac [2] subst) |
2277 apply (erule_tac [2] subst) |
2280 apply (rule_tac [2] b = t in lub_const [THEN subst]) |
2278 apply (rule_tac [2] b = t in lub_const [THEN subst]) |
2281 apply (rule_tac [4] comp_lubs [THEN ssubst]) |
2279 apply (rule_tac [4] comp_lubs [THEN ssubst]) |