1 (* Title: HOLCF/CompactBasis.thy |
1 (* Title: HOLCF/CompactBasis.thy |
2 Author: Brian Huffman |
2 Author: Brian Huffman |
3 *) |
3 *) |
4 |
4 |
5 header {* Compact bases of domains *} |
5 header {* A compact basis for powerdomains *} |
6 |
6 |
7 theory CompactBasis |
7 theory CompactBasis |
8 imports Completion Bifinite |
8 imports Algebraic |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Compact bases of bifinite domains *} |
11 default_sort sfp |
12 |
|
13 default_sort profinite |
|
14 |
|
15 typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}" |
|
16 by (fast intro: compact_approx) |
|
17 |
|
18 lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)" |
|
19 by (rule Rep_compact_basis [unfolded mem_Collect_eq]) |
|
20 |
|
21 instantiation compact_basis :: (profinite) below |
|
22 begin |
|
23 |
|
24 definition |
|
25 compact_le_def: |
|
26 "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)" |
|
27 |
|
28 instance .. |
|
29 |
|
30 end |
|
31 |
|
32 instance compact_basis :: (profinite) po |
|
33 by (rule typedef_po |
|
34 [OF type_definition_compact_basis compact_le_def]) |
|
35 |
|
36 text {* Take function for compact basis *} |
|
37 |
|
38 definition |
|
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)))" |
|
41 |
|
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) |
|
46 |
|
47 lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric] |
|
48 |
|
49 interpretation compact_basis: |
|
50 basis_take below compact_take |
|
51 proof |
|
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_below) |
|
56 next |
|
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) |
|
60 next |
|
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) |
|
65 next |
|
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) |
|
70 next |
|
71 fix n :: nat |
|
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) |
|
78 done |
|
79 next |
|
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) |
|
86 done |
|
87 qed |
|
88 |
|
89 text {* Ideal completion *} |
|
90 |
|
91 definition |
|
92 approximants :: "'a \<Rightarrow> 'a compact_basis set" where |
|
93 "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})" |
|
94 |
|
95 interpretation compact_basis: |
|
96 ideal_completion below compact_take Rep_compact_basis approximants |
|
97 proof |
|
98 fix w :: 'a |
|
99 show "preorder.ideal below (approximants w)" |
|
100 proof (rule below.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_below) |
|
105 done |
|
106 next |
|
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 |
|
111 apply simp |
|
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_below) |
|
120 apply (erule subst, erule subst) |
|
121 apply (simp add: monofun_cfun chain_mono [OF chain_approx]) |
|
122 done |
|
123 next |
|
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 |
|
127 apply simp |
|
128 apply (simp add: compact_le_def) |
|
129 apply (erule (1) below_trans) |
|
130 done |
|
131 qed |
|
132 next |
|
133 fix Y :: "nat \<Rightarrow> 'a" |
|
134 assume Y: "chain Y" |
|
135 show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))" |
|
136 unfolding approximants_def |
|
137 apply safe |
|
138 apply (simp add: compactD2 [OF compact_Rep_compact_basis Y]) |
|
139 apply (erule below_trans, rule is_ub_thelub [OF Y]) |
|
140 done |
|
141 next |
|
142 fix a :: "'a compact_basis" |
|
143 show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}" |
|
144 unfolding approximants_def compact_le_def .. |
|
145 next |
|
146 fix x y :: "'a" |
|
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_below) |
|
152 apply (simp add: approximants_def Abs_compact_basis_inverse) |
|
153 done |
|
154 qed |
|
155 |
|
156 text {* minimal compact element *} |
|
157 |
|
158 definition |
|
159 compact_bot :: "'a::bifinite compact_basis" where |
|
160 "compact_bot = Abs_compact_basis \<bottom>" |
|
161 |
|
162 lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>" |
|
163 unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse) |
|
164 |
|
165 lemma compact_bot_minimal [simp]: "compact_bot \<sqsubseteq> a" |
|
166 unfolding compact_le_def Rep_compact_bot by simp |
|
167 |
|
168 |
12 |
169 subsection {* A compact basis for powerdomains *} |
13 subsection {* A compact basis for powerdomains *} |
170 |
14 |
171 typedef 'a pd_basis = |
15 typedef 'a pd_basis = |
172 "{S::'a::profinite compact_basis set. finite S \<and> S \<noteq> {}}" |
16 "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}" |
173 by (rule_tac x="{arbitrary}" in exI, simp) |
17 by (rule_tac x="{arbitrary}" in exI, simp) |
174 |
18 |
175 lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)" |
19 lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)" |
176 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
20 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
177 |
21 |
178 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}" |
22 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}" |
179 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
23 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
180 |
24 |
181 text {* unit and plus *} |
25 text {* The powerdomain basis type is countable. *} |
|
26 |
|
27 lemma pd_basis_countable: "\<exists>f::'a::sfp pd_basis \<Rightarrow> nat. inj f" |
|
28 proof - |
|
29 obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g" |
|
30 using compact_basis.countable .. |
|
31 hence image_g_eq: "\<And>A B. g ` A = g ` B \<longleftrightarrow> A = B" |
|
32 by (rule inj_image_eq_iff) |
|
33 have "inj (\<lambda>t. set_encode (g ` Rep_pd_basis t))" |
|
34 by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject) |
|
35 thus ?thesis by - (rule exI) |
|
36 (* FIXME: why doesn't ".." or "by (rule exI)" work? *) |
|
37 qed |
|
38 |
|
39 subsection {* Unit and plus constructors *} |
182 |
40 |
183 definition |
41 definition |
184 PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where |
42 PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where |
185 "PDUnit = (\<lambda>x. Abs_pd_basis {x})" |
43 "PDUnit = (\<lambda>x. Abs_pd_basis {x})" |
186 |
44 |
248 interpret ab_semigroup_idem_mult f by fact |
106 interpret ab_semigroup_idem_mult f by fact |
249 show ?thesis unfolding fold_pd_def Rep_PDPlus |
107 show ?thesis unfolding fold_pd_def Rep_PDPlus |
250 by (simp add: image_Un fold1_Un2) |
108 by (simp add: image_Un fold1_Un2) |
251 qed |
109 qed |
252 |
110 |
253 text {* Take function for powerdomain basis *} |
111 subsection {* Lemmas for proving if-and-only-if inequalities *} |
254 |
112 |
255 definition |
113 lemma chain_max_below_iff: |
256 pd_take :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where |
114 assumes Y: "chain Y" shows "Y (max i j) \<sqsubseteq> x \<longleftrightarrow> Y i \<sqsubseteq> x \<and> Y j \<sqsubseteq> x" |
257 "pd_take n = (\<lambda>t. Abs_pd_basis (compact_take n ` Rep_pd_basis t))" |
115 apply auto |
258 |
116 apply (erule below_trans [OF chain_mono [OF Y le_maxI1]]) |
259 lemma Rep_pd_take: |
117 apply (erule below_trans [OF chain_mono [OF Y le_maxI2]]) |
260 "Rep_pd_basis (pd_take n t) = compact_take n ` Rep_pd_basis t" |
118 apply (simp add: max_def) |
261 unfolding pd_take_def |
|
262 apply (rule Abs_pd_basis_inverse) |
|
263 apply (simp add: pd_basis_def) |
|
264 done |
119 done |
265 |
120 |
266 lemma pd_take_simps [simp]: |
121 lemma all_ex_below_disj_iff: |
267 "pd_take n (PDUnit a) = PDUnit (compact_take n a)" |
122 assumes "chain X" and "chain Y" |
268 "pd_take n (PDPlus t u) = PDPlus (pd_take n t) (pd_take n u)" |
123 shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<or> Y i \<sqsubseteq> Z j) \<longleftrightarrow> |
269 apply (simp_all add: Rep_pd_basis_inject [symmetric]) |
124 (\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<or> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)" |
270 apply (simp_all add: Rep_pd_take Rep_PDUnit Rep_PDPlus image_Un) |
125 by (metis chain_max_below_iff assms) |
271 done |
|
272 |
126 |
273 lemma pd_take_idem: "pd_take n (pd_take n t) = pd_take n t" |
127 lemma all_ex_below_conj_iff: |
274 apply (induct t rule: pd_basis_induct) |
128 assumes "chain X" and "chain Y" and "chain Z" |
275 apply (simp add: compact_basis.take_take) |
129 shows "(\<forall>i. \<exists>j. X i \<sqsubseteq> Z j \<and> Y i \<sqsubseteq> Z j) \<longleftrightarrow> |
276 apply simp |
130 (\<forall>i. \<exists>j. X i \<sqsubseteq> Z j) \<and> (\<forall>i. \<exists>j. Y i \<sqsubseteq> Z j)" |
277 done |
131 oops |
278 |
|
279 lemma finite_range_pd_take: "finite (range (pd_take n))" |
|
280 apply (rule finite_imageD [where f="Rep_pd_basis"]) |
|
281 apply (rule finite_subset [where B="Pow (range (compact_take n))"]) |
|
282 apply (clarsimp simp add: Rep_pd_take) |
|
283 apply (simp add: compact_basis.finite_range_take) |
|
284 apply (rule inj_onI, simp add: Rep_pd_basis_inject) |
|
285 done |
|
286 |
|
287 lemma pd_take_covers: "\<exists>n. pd_take n t = t" |
|
288 apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. pd_take m t = t", fast) |
|
289 apply (induct t rule: pd_basis_induct) |
|
290 apply (cut_tac a=a in compact_basis.take_covers) |
|
291 apply (clarify, rule_tac x=n in exI) |
|
292 apply (clarify, simp) |
|
293 apply (rule below_antisym) |
|
294 apply (rule compact_basis.take_less) |
|
295 apply (drule_tac a=a in compact_basis.take_chain_le) |
|
296 apply simp |
|
297 apply (clarify, rename_tac i j) |
|
298 apply (rule_tac x="max i j" in exI, simp) |
|
299 done |
|
300 |
132 |
301 end |
133 end |