equal
deleted
inserted
replaced
1 (* Title: HOL/HOLCF/UpperPD.thy |
1 (* Title: HOL/HOLCF/UpperPD.thy |
2 Author: Brian Huffman |
2 Author: Brian Huffman |
3 *) |
3 *) |
4 |
4 |
5 section {* Upper powerdomain *} |
5 section \<open>Upper powerdomain\<close> |
6 |
6 |
7 theory UpperPD |
7 theory UpperPD |
8 imports Compact_Basis |
8 imports Compact_Basis |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Basis preorder *} |
11 subsection \<open>Basis preorder\<close> |
12 |
12 |
13 definition |
13 definition |
14 upper_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<sharp>" 50) where |
14 upper_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<sharp>" 50) where |
15 "upper_le = (\<lambda>u v. \<forall>y\<in>Rep_pd_basis v. \<exists>x\<in>Rep_pd_basis u. x \<sqsubseteq> y)" |
15 "upper_le = (\<lambda>u v. \<forall>y\<in>Rep_pd_basis v. \<exists>x\<in>Rep_pd_basis u. x \<sqsubseteq> y)" |
16 |
16 |
68 apply (simp add: 2) |
68 apply (simp add: 2) |
69 apply (simp add: upper_le_PDPlus_iff 3) |
69 apply (simp add: upper_le_PDPlus_iff 3) |
70 done |
70 done |
71 |
71 |
72 |
72 |
73 subsection {* Type definition *} |
73 subsection \<open>Type definition\<close> |
74 |
74 |
75 typedef 'a upper_pd ("('(_')\<sharp>)") = |
75 typedef 'a upper_pd ("('(_')\<sharp>)") = |
76 "{S::'a pd_basis set. upper_le.ideal S}" |
76 "{S::'a pd_basis set. upper_le.ideal S}" |
77 by (rule upper_le.ex_ideal) |
77 by (rule upper_le.ex_ideal) |
78 |
78 |
101 ideal_completion upper_le upper_principal Rep_upper_pd |
101 ideal_completion upper_le upper_principal Rep_upper_pd |
102 using type_definition_upper_pd below_upper_pd_def |
102 using type_definition_upper_pd below_upper_pd_def |
103 using upper_principal_def pd_basis_countable |
103 using upper_principal_def pd_basis_countable |
104 by (rule upper_le.typedef_ideal_completion) |
104 by (rule upper_le.typedef_ideal_completion) |
105 |
105 |
106 text {* Upper powerdomain is pointed *} |
106 text \<open>Upper powerdomain is pointed\<close> |
107 |
107 |
108 lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys" |
108 lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys" |
109 by (induct ys rule: upper_pd.principal_induct, simp, simp) |
109 by (induct ys rule: upper_pd.principal_induct, simp, simp) |
110 |
110 |
111 instance upper_pd :: (bifinite) pcpo |
111 instance upper_pd :: (bifinite) pcpo |
113 |
113 |
114 lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)" |
114 lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)" |
115 by (rule upper_pd_minimal [THEN bottomI, symmetric]) |
115 by (rule upper_pd_minimal [THEN bottomI, symmetric]) |
116 |
116 |
117 |
117 |
118 subsection {* Monadic unit and plus *} |
118 subsection \<open>Monadic unit and plus\<close> |
119 |
119 |
120 definition |
120 definition |
121 upper_unit :: "'a \<rightarrow> 'a upper_pd" where |
121 upper_unit :: "'a \<rightarrow> 'a upper_pd" where |
122 "upper_unit = compact_basis.extension (\<lambda>a. upper_principal (PDUnit a))" |
122 "upper_unit = compact_basis.extension (\<lambda>a. upper_principal (PDUnit a))" |
123 |
123 |
172 lemmas upper_plus_commute = upper_add.commute |
172 lemmas upper_plus_commute = upper_add.commute |
173 lemmas upper_plus_absorb = upper_add.idem |
173 lemmas upper_plus_absorb = upper_add.idem |
174 lemmas upper_plus_left_commute = upper_add.left_commute |
174 lemmas upper_plus_left_commute = upper_add.left_commute |
175 lemmas upper_plus_left_absorb = upper_add.left_idem |
175 lemmas upper_plus_left_absorb = upper_add.left_idem |
176 |
176 |
177 text {* Useful for @{text "simp add: upper_plus_ac"} *} |
177 text \<open>Useful for \<open>simp add: upper_plus_ac\<close>\<close> |
178 lemmas upper_plus_ac = |
178 lemmas upper_plus_ac = |
179 upper_plus_assoc upper_plus_commute upper_plus_left_commute |
179 upper_plus_assoc upper_plus_commute upper_plus_left_commute |
180 |
180 |
181 text {* Useful for @{text "simp only: upper_plus_aci"} *} |
181 text \<open>Useful for \<open>simp only: upper_plus_aci\<close>\<close> |
182 lemmas upper_plus_aci = |
182 lemmas upper_plus_aci = |
183 upper_plus_ac upper_plus_absorb upper_plus_left_absorb |
183 upper_plus_ac upper_plus_absorb upper_plus_left_absorb |
184 |
184 |
185 lemma upper_plus_below1: "xs \<union>\<sharp> ys \<sqsubseteq> xs" |
185 lemma upper_plus_below1: "xs \<union>\<sharp> ys \<sqsubseteq> xs" |
186 apply (induct xs rule: upper_pd.principal_induct, simp) |
186 apply (induct xs rule: upper_pd.principal_induct, simp) |
259 lemma compact_upper_plus [simp]: |
259 lemma compact_upper_plus [simp]: |
260 "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<sharp> ys)" |
260 "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<sharp> ys)" |
261 by (auto dest!: upper_pd.compact_imp_principal) |
261 by (auto dest!: upper_pd.compact_imp_principal) |
262 |
262 |
263 |
263 |
264 subsection {* Induction rules *} |
264 subsection \<open>Induction rules\<close> |
265 |
265 |
266 lemma upper_pd_induct1: |
266 lemma upper_pd_induct1: |
267 assumes P: "adm P" |
267 assumes P: "adm P" |
268 assumes unit: "\<And>x. P {x}\<sharp>" |
268 assumes unit: "\<And>x. P {x}\<sharp>" |
269 assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> \<union>\<sharp> ys)" |
269 assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> \<union>\<sharp> ys)" |
288 apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit) |
288 apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit) |
289 apply (simp only: upper_plus_principal [symmetric] plus) |
289 apply (simp only: upper_plus_principal [symmetric] plus) |
290 done |
290 done |
291 |
291 |
292 |
292 |
293 subsection {* Monadic bind *} |
293 subsection \<open>Monadic bind\<close> |
294 |
294 |
295 definition |
295 definition |
296 upper_bind_basis :: |
296 upper_bind_basis :: |
297 "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where |
297 "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where |
298 "upper_bind_basis = fold_pd |
298 "upper_bind_basis = fold_pd |
360 lemma upper_bind_bind: |
360 lemma upper_bind_bind: |
361 "upper_bind\<cdot>(upper_bind\<cdot>xs\<cdot>f)\<cdot>g = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_bind\<cdot>(f\<cdot>x)\<cdot>g)" |
361 "upper_bind\<cdot>(upper_bind\<cdot>xs\<cdot>f)\<cdot>g = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_bind\<cdot>(f\<cdot>x)\<cdot>g)" |
362 by (induct xs, simp_all) |
362 by (induct xs, simp_all) |
363 |
363 |
364 |
364 |
365 subsection {* Map *} |
365 subsection \<open>Map\<close> |
366 |
366 |
367 definition |
367 definition |
368 upper_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where |
368 upper_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where |
369 "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<sharp>))" |
369 "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<sharp>))" |
370 |
370 |
451 done |
451 done |
452 thus "finite {xs. upper_map\<cdot>d\<cdot>xs = xs}" |
452 thus "finite {xs. upper_map\<cdot>d\<cdot>xs = xs}" |
453 by (rule finite_range_imp_finite_fixes) |
453 by (rule finite_range_imp_finite_fixes) |
454 qed |
454 qed |
455 |
455 |
456 subsection {* Upper powerdomain is bifinite *} |
456 subsection \<open>Upper powerdomain is bifinite\<close> |
457 |
457 |
458 lemma approx_chain_upper_map: |
458 lemma approx_chain_upper_map: |
459 assumes "approx_chain a" |
459 assumes "approx_chain a" |
460 shows "approx_chain (\<lambda>i. upper_map\<cdot>(a i))" |
460 shows "approx_chain (\<lambda>i. upper_map\<cdot>(a i))" |
461 using assms unfolding approx_chain_def |
461 using assms unfolding approx_chain_def |
466 show "\<exists>(a::nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd). approx_chain a" |
466 show "\<exists>(a::nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd). approx_chain a" |
467 using bifinite [where 'a='a] |
467 using bifinite [where 'a='a] |
468 by (fast intro!: approx_chain_upper_map) |
468 by (fast intro!: approx_chain_upper_map) |
469 qed |
469 qed |
470 |
470 |
471 subsection {* Join *} |
471 subsection \<open>Join\<close> |
472 |
472 |
473 definition |
473 definition |
474 upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where |
474 upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where |
475 "upper_join = (\<Lambda> xss. upper_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))" |
475 "upper_join = (\<Lambda> xss. upper_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))" |
476 |
476 |