1 (* Title: HOLCF/CompactBasis.thy
5 header {* Compact bases of domains *}
11 subsection {* Compact bases of bifinite domains *}
15 typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}"
16 by (fast intro: compact_approx)
18 lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
19 by (rule Rep_compact_basis [unfolded mem_Collect_eq])
21 instantiation compact_basis :: (profinite) sq_ord
26 "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)"
32 instance compact_basis :: (profinite) po
34 [OF type_definition_compact_basis compact_le_def])
36 text {* Take function for compact basis *}
39 compact_take :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" where
40 "compact_take = (\<lambda>n a. Abs_compact_basis (approx n\<cdot>(Rep_compact_basis a)))"
42 lemma Rep_compact_take:
43 "Rep_compact_basis (compact_take n a) = approx n\<cdot>(Rep_compact_basis a)"
44 unfolding compact_take_def
45 by (simp add: Abs_compact_basis_inverse)
47 lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
49 interpretation compact_basis!:
50 basis_take sq_le compact_take
52 fix n :: nat and a :: "'a compact_basis"
53 show "compact_take n a \<sqsubseteq> a"
54 unfolding compact_le_def
55 by (simp add: Rep_compact_take approx_less)
57 fix n :: nat and a :: "'a compact_basis"
58 show "compact_take n (compact_take n a) = compact_take n a"
59 by (simp add: Rep_compact_basis_inject [symmetric] Rep_compact_take)
61 fix n :: nat and a b :: "'a compact_basis"
62 assume "a \<sqsubseteq> b" thus "compact_take n a \<sqsubseteq> compact_take n b"
63 unfolding compact_le_def Rep_compact_take
64 by (rule monofun_cfun_arg)
66 fix n :: nat and a :: "'a compact_basis"
67 show "\<And>n a. compact_take n a \<sqsubseteq> compact_take (Suc n) a"
68 unfolding compact_le_def Rep_compact_take
69 by (rule chainE, simp)
72 show "finite (range (compact_take n))"
73 apply (rule finite_imageD [where f="Rep_compact_basis"])
74 apply (rule finite_subset [where B="range (\<lambda>x. approx n\<cdot>x)"])
75 apply (clarsimp simp add: Rep_compact_take)
76 apply (rule finite_range_approx)
77 apply (rule inj_onI, simp add: Rep_compact_basis_inject)
80 fix a :: "'a compact_basis"
81 show "\<exists>n. compact_take n a = a"
82 apply (simp add: Rep_compact_basis_inject [symmetric])
83 apply (simp add: Rep_compact_take)
84 apply (rule profinite_compact_eq_approx)
85 apply (rule compact_Rep_compact_basis)
89 text {* Ideal completion *}
92 approximants :: "'a \<Rightarrow> 'a compact_basis set" where
93 "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
95 interpretation compact_basis!:
96 ideal_completion sq_le compact_take Rep_compact_basis approximants
99 show "preorder.ideal sq_le (approximants w)"
100 proof (rule sq_le.idealI)
101 show "\<exists>x. x \<in> approximants w"
102 unfolding approximants_def
103 apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
104 apply (simp add: Abs_compact_basis_inverse approx_less)
107 fix x y :: "'a compact_basis"
108 assume "x \<in> approximants w" "y \<in> approximants w"
109 thus "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
110 unfolding approximants_def
112 apply (cut_tac a=x in compact_Rep_compact_basis)
113 apply (cut_tac a=y in compact_Rep_compact_basis)
114 apply (drule profinite_compact_eq_approx)
115 apply (drule profinite_compact_eq_approx)
116 apply (clarify, rename_tac i j)
117 apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
118 apply (simp add: compact_le_def)
119 apply (simp add: Abs_compact_basis_inverse approx_less)
120 apply (erule subst, erule subst)
121 apply (simp add: monofun_cfun chain_mono [OF chain_approx])
124 fix x y :: "'a compact_basis"
125 assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w"
126 unfolding approximants_def
128 apply (simp add: compact_le_def)
129 apply (erule (1) trans_less)
133 fix Y :: "nat \<Rightarrow> 'a"
135 show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))"
136 unfolding approximants_def
138 apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
139 apply (erule trans_less, rule is_ub_thelub [OF Y])
142 fix a :: "'a compact_basis"
143 show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
144 unfolding approximants_def compact_le_def ..
147 assume "approximants x \<subseteq> approximants y" thus "x \<sqsubseteq> y"
148 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
149 apply (rule admD, simp, simp)
150 apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
151 apply (simp add: approximants_def Abs_compact_basis_inverse approx_less)
152 apply (simp add: approximants_def Abs_compact_basis_inverse)
156 text {* minimal compact element *}
159 compact_bot :: "'a::bifinite compact_basis" where
160 "compact_bot = Abs_compact_basis \<bottom>"
162 lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>"
163 unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
165 lemma compact_bot_minimal [simp]: "compact_bot \<sqsubseteq> a"
166 unfolding compact_le_def Rep_compact_bot by simp
169 subsection {* A compact basis for powerdomains *}
171 typedef 'a pd_basis =
172 "{S::'a::profinite compact_basis set. finite S \<and> S \<noteq> {}}"
173 by (rule_tac x="{arbitrary}" in exI, simp)
175 lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
176 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
178 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
179 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
181 text {* unit and plus *}
184 PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
185 "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
188 PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
189 "PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)"
192 "Rep_pd_basis (PDUnit x) = {x}"
193 unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
196 "Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v"
197 unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def)
199 lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)"
200 unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp
202 lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)"
203 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc)
205 lemma PDPlus_commute: "PDPlus t u = PDPlus u t"
206 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute)
208 lemma PDPlus_absorb: "PDPlus t t = t"
209 unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
211 lemma pd_basis_induct1:
212 assumes PDUnit: "\<And>a. P (PDUnit a)"
213 assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
215 apply (induct x, unfold pd_basis_def, clarify)
216 apply (erule (1) finite_ne_induct)
217 apply (cut_tac a=x in PDUnit)
218 apply (simp add: PDUnit_def)
219 apply (drule_tac a=x in PDPlus)
220 apply (simp add: PDUnit_def PDPlus_def Abs_pd_basis_inverse [unfolded pd_basis_def])
223 lemma pd_basis_induct:
224 assumes PDUnit: "\<And>a. P (PDUnit a)"
225 assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
227 apply (induct x rule: pd_basis_induct1)
228 apply (rule PDUnit, erule PDPlus [OF PDUnit])
235 "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
236 where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
238 lemma fold_pd_PDUnit:
239 assumes "ab_semigroup_idem_mult f"
240 shows "fold_pd g f (PDUnit x) = g x"
241 unfolding fold_pd_def Rep_PDUnit by simp
243 lemma fold_pd_PDPlus:
244 assumes "ab_semigroup_idem_mult f"
245 shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
247 interpret ab_semigroup_idem_mult f by fact
248 show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
251 text {* Take function for powerdomain basis *}
254 pd_take :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
255 "pd_take n = (\<lambda>t. Abs_pd_basis (compact_take n ` Rep_pd_basis t))"
258 "Rep_pd_basis (pd_take n t) = compact_take n ` Rep_pd_basis t"
259 unfolding pd_take_def
260 apply (rule Abs_pd_basis_inverse)
261 apply (simp add: pd_basis_def)
264 lemma pd_take_simps [simp]:
265 "pd_take n (PDUnit a) = PDUnit (compact_take n a)"
266 "pd_take n (PDPlus t u) = PDPlus (pd_take n t) (pd_take n u)"
267 apply (simp_all add: Rep_pd_basis_inject [symmetric])
268 apply (simp_all add: Rep_pd_take Rep_PDUnit Rep_PDPlus image_Un)
271 lemma pd_take_idem: "pd_take n (pd_take n t) = pd_take n t"
272 apply (induct t rule: pd_basis_induct)
273 apply (simp add: compact_basis.take_take)
277 lemma finite_range_pd_take: "finite (range (pd_take n))"
278 apply (rule finite_imageD [where f="Rep_pd_basis"])
279 apply (rule finite_subset [where B="Pow (range (compact_take n))"])
280 apply (clarsimp simp add: Rep_pd_take)
281 apply (simp add: compact_basis.finite_range_take)
282 apply (rule inj_onI, simp add: Rep_pd_basis_inject)
285 lemma pd_take_covers: "\<exists>n. pd_take n t = t"
286 apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. pd_take m t = t", fast)
287 apply (induct t rule: pd_basis_induct)
288 apply (cut_tac a=a in compact_basis.take_covers)
289 apply (clarify, rule_tac x=n in exI)
290 apply (clarify, simp)
291 apply (rule antisym_less)
292 apply (rule compact_basis.take_less)
293 apply (drule_tac a=a in compact_basis.take_chain_le)
295 apply (clarify, rename_tac i j)
296 apply (rule_tac x="max i j" in exI, simp)