93 |
93 |
94 |
94 |
95 subsection {* Type definition *} |
95 subsection {* Type definition *} |
96 |
96 |
97 cpodef (open) 'a upper_pd = |
97 cpodef (open) 'a upper_pd = |
98 "{S::'a::profinite pd_basis set. upper_le.ideal S}" |
98 "{S::'a pd_basis cset. upper_le.ideal (Rep_cset S)}" |
99 apply (simp add: upper_le.adm_ideal) |
99 by (rule upper_le.cpodef_ideal_lemma) |
100 apply (fast intro: upper_le.ideal_principal) |
100 |
101 done |
101 lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_cset (Rep_upper_pd xs))" |
102 |
|
103 lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd x)" |
|
104 by (rule Rep_upper_pd [unfolded mem_Collect_eq]) |
102 by (rule Rep_upper_pd [unfolded mem_Collect_eq]) |
105 |
103 |
106 definition |
104 definition |
107 upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where |
105 upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where |
108 "upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}" |
106 "upper_principal t = Abs_upper_pd (Abs_cset {u. u \<le>\<sharp> t})" |
109 |
107 |
110 lemma Rep_upper_principal: |
108 lemma Rep_upper_principal: |
111 "Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> t}" |
109 "Rep_cset (Rep_upper_pd (upper_principal t)) = {u. u \<le>\<sharp> t}" |
112 unfolding upper_principal_def |
110 unfolding upper_principal_def |
113 apply (rule Abs_upper_pd_inverse [unfolded mem_Collect_eq]) |
111 by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal) |
114 apply (rule upper_le.ideal_principal) |
|
115 done |
|
116 |
112 |
117 interpretation upper_pd: |
113 interpretation upper_pd: |
118 ideal_completion [upper_le approx_pd upper_principal Rep_upper_pd] |
114 ideal_completion |
|
115 [upper_le approx_pd upper_principal "\<lambda>x. Rep_cset (Rep_upper_pd x)"] |
119 apply unfold_locales |
116 apply unfold_locales |
120 apply (rule approx_pd_upper_le) |
117 apply (rule approx_pd_upper_le) |
121 apply (rule approx_pd_idem) |
118 apply (rule approx_pd_idem) |
122 apply (erule approx_pd_upper_mono) |
119 apply (erule approx_pd_upper_mono) |
123 apply (rule approx_pd_upper_chain) |
120 apply (rule approx_pd_upper_chain) |
124 apply (rule finite_range_approx_pd) |
121 apply (rule finite_range_approx_pd) |
125 apply (rule approx_pd_covers) |
122 apply (rule approx_pd_covers) |
126 apply (rule ideal_Rep_upper_pd) |
123 apply (rule ideal_Rep_upper_pd) |
127 apply (rule cont_Rep_upper_pd) |
124 apply (simp add: cont2contlubE [OF cont_Rep_upper_pd] Rep_cset_lub) |
128 apply (rule Rep_upper_principal) |
125 apply (rule Rep_upper_principal) |
129 apply (simp only: less_upper_pd_def less_set_eq) |
126 apply (simp only: less_upper_pd_def sq_le_cset_def) |
130 done |
127 done |
131 |
128 |
132 text {* Upper powerdomain is pointed *} |
129 text {* Upper powerdomain is pointed *} |
133 |
130 |
134 lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys" |
131 lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys" |
164 "approx n\<cdot>(upper_principal t) = upper_principal (approx_pd n t)" |
161 "approx n\<cdot>(upper_principal t) = upper_principal (approx_pd n t)" |
165 unfolding approx_upper_pd_def |
162 unfolding approx_upper_pd_def |
166 by (rule upper_pd.completion_approx_principal) |
163 by (rule upper_pd.completion_approx_principal) |
167 |
164 |
168 lemma approx_eq_upper_principal: |
165 lemma approx_eq_upper_principal: |
169 "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)" |
166 "\<exists>t\<in>Rep_cset (Rep_upper_pd xs). |
|
167 approx n\<cdot>xs = upper_principal (approx_pd n t)" |
170 unfolding approx_upper_pd_def |
168 unfolding approx_upper_pd_def |
171 by (rule upper_pd.completion_approx_eq_principal) |
169 by (rule upper_pd.completion_approx_eq_principal) |
172 |
170 |
173 |
171 |
174 subsection {* Monadic unit and plus *} |
172 subsection {* Monadic unit and plus *} |