88 qed |
88 qed |
89 |
89 |
90 text {* Ideal completion *} |
90 text {* Ideal completion *} |
91 |
91 |
92 definition |
92 definition |
93 compacts :: "'a \<Rightarrow> 'a compact_basis set" where |
93 approximants :: "'a \<Rightarrow> 'a compact_basis set" where |
94 "compacts = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})" |
94 "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})" |
95 |
95 |
96 interpretation compact_basis: |
96 interpretation compact_basis: |
97 ideal_completion [sq_le compact_take Rep_compact_basis compacts] |
97 ideal_completion [sq_le compact_take Rep_compact_basis approximants] |
98 proof |
98 proof |
99 fix w :: 'a |
99 fix w :: 'a |
100 show "preorder.ideal sq_le (compacts w)" |
100 show "preorder.ideal sq_le (approximants w)" |
101 proof (rule sq_le.idealI) |
101 proof (rule sq_le.idealI) |
102 show "\<exists>x. x \<in> compacts w" |
102 show "\<exists>x. x \<in> approximants w" |
103 unfolding compacts_def |
103 unfolding approximants_def |
104 apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI) |
104 apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI) |
105 apply (simp add: Abs_compact_basis_inverse approx_less) |
105 apply (simp add: Abs_compact_basis_inverse approx_less) |
106 done |
106 done |
107 next |
107 next |
108 fix x y :: "'a compact_basis" |
108 fix x y :: "'a compact_basis" |
109 assume "x \<in> compacts w" "y \<in> compacts w" |
109 assume "x \<in> approximants w" "y \<in> approximants w" |
110 thus "\<exists>z \<in> compacts w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
110 thus "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
111 unfolding compacts_def |
111 unfolding approximants_def |
112 apply simp |
112 apply simp |
113 apply (cut_tac a=x in compact_Rep_compact_basis) |
113 apply (cut_tac a=x in compact_Rep_compact_basis) |
114 apply (cut_tac a=y in compact_Rep_compact_basis) |
114 apply (cut_tac a=y in compact_Rep_compact_basis) |
115 apply (drule profinite_compact_eq_approx) |
115 apply (drule profinite_compact_eq_approx) |
116 apply (drule profinite_compact_eq_approx) |
116 apply (drule profinite_compact_eq_approx) |
121 apply (erule subst, erule subst) |
121 apply (erule subst, erule subst) |
122 apply (simp add: monofun_cfun chain_mono [OF chain_approx]) |
122 apply (simp add: monofun_cfun chain_mono [OF chain_approx]) |
123 done |
123 done |
124 next |
124 next |
125 fix x y :: "'a compact_basis" |
125 fix x y :: "'a compact_basis" |
126 assume "x \<sqsubseteq> y" "y \<in> compacts w" thus "x \<in> compacts w" |
126 assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w" |
127 unfolding compacts_def |
127 unfolding approximants_def |
128 apply simp |
128 apply simp |
129 apply (simp add: compact_le_def) |
129 apply (simp add: compact_le_def) |
130 apply (erule (1) trans_less) |
130 apply (erule (1) trans_less) |
131 done |
131 done |
132 qed |
132 qed |
133 next |
133 next |
134 fix Y :: "nat \<Rightarrow> 'a" |
134 fix Y :: "nat \<Rightarrow> 'a" |
135 assume Y: "chain Y" |
135 assume Y: "chain Y" |
136 show "compacts (\<Squnion>i. Y i) = (\<Union>i. compacts (Y i))" |
136 show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))" |
137 unfolding compacts_def |
137 unfolding approximants_def |
138 apply safe |
138 apply safe |
139 apply (simp add: compactD2 [OF compact_Rep_compact_basis Y]) |
139 apply (simp add: compactD2 [OF compact_Rep_compact_basis Y]) |
140 apply (erule trans_less, rule is_ub_thelub [OF Y]) |
140 apply (erule trans_less, rule is_ub_thelub [OF Y]) |
141 done |
141 done |
142 next |
142 next |
143 fix a :: "'a compact_basis" |
143 fix a :: "'a compact_basis" |
144 show "compacts (Rep_compact_basis a) = {b. b \<sqsubseteq> a}" |
144 show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}" |
145 unfolding compacts_def compact_le_def .. |
145 unfolding approximants_def compact_le_def .. |
146 next |
146 next |
147 fix x y :: "'a" |
147 fix x y :: "'a" |
148 assume "compacts x \<subseteq> compacts y" thus "x \<sqsubseteq> y" |
148 assume "approximants x \<subseteq> approximants y" thus "x \<sqsubseteq> y" |
149 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp) |
149 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp) |
150 apply (rule admD, simp, simp) |
150 apply (rule admD, simp, simp) |
151 apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD) |
151 apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD) |
152 apply (simp add: compacts_def Abs_compact_basis_inverse approx_less) |
152 apply (simp add: approximants_def Abs_compact_basis_inverse approx_less) |
153 apply (simp add: compacts_def Abs_compact_basis_inverse) |
153 apply (simp add: approximants_def Abs_compact_basis_inverse) |
154 done |
154 done |
155 qed |
155 qed |
156 |
156 |
157 text {* minimal compact element *} |
157 text {* minimal compact element *} |
158 |
158 |
161 "compact_bot = Abs_compact_basis \<bottom>" |
161 "compact_bot = Abs_compact_basis \<bottom>" |
162 |
162 |
163 lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>" |
163 lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>" |
164 unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse) |
164 unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse) |
165 |
165 |
166 lemma compact_minimal [simp]: "compact_bot \<sqsubseteq> a" |
166 lemma compact_bot_minimal [simp]: "compact_bot \<sqsubseteq> a" |
167 unfolding compact_le_def Rep_compact_bot by simp |
167 unfolding compact_le_def Rep_compact_bot by simp |
168 |
168 |
169 |
169 |
170 subsection {* A compact basis for powerdomains *} |
170 subsection {* A compact basis for powerdomains *} |
171 |
171 |