author  huffman 
Mon, 22 Mar 2010 13:27:35 0700  
changeset 35901  12f09bf2c77f 
parent 31076  99fe356cbbc2 
child 36452  d37c6eed8117 
permissions  rwrr 
25904  1 
(* Title: HOLCF/CompactBasis.thy 
2 
Author: Brian Huffman 

3 
*) 

4 

5 
header {* Compact bases of domains *} 

6 

7 
theory CompactBasis 

27404  8 
imports Completion 
25904  9 
begin 
10 

11 
subsection {* Compact bases of bifinite domains *} 

12 

26407
562a1d615336
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents:
26041
diff
changeset

13 
defaultsort profinite 
25904  14 

26407
562a1d615336
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents:
26041
diff
changeset

15 
typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}" 
25904  16 
by (fast intro: compact_approx) 
17 

27289  18 
lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)" 
26927  19 
by (rule Rep_compact_basis [unfolded mem_Collect_eq]) 
25904  20 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

21 
instantiation compact_basis :: (profinite) below 
26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

22 
begin 
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

23 

57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

24 
definition 
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

25 
compact_le_def: 
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

26 
"(op \<sqsubseteq>) \<equiv> (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)" 
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

27 

57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

28 
instance .. 
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

29 

57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

30 
end 
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

31 

57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

32 
instance compact_basis :: (profinite) po 
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

33 
by (rule typedef_po 
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

34 
[OF type_definition_compact_basis compact_le_def]) 
25904  35 

27289  36 
text {* Take function for compact basis *} 
25904  37 

38 
definition 

27406  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)))" 

25904  41 

27406  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 

25904  45 
by (simp add: Abs_compact_basis_inverse) 
46 

27406  47 
lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric] 
25904  48 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29511
diff
changeset

49 
interpretation compact_basis: 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

50 
basis_take below compact_take 
27289  51 
proof 
52 
fix n :: nat and a :: "'a compact_basis" 

27406  53 
show "compact_take n a \<sqsubseteq> a" 
27289  54 
unfolding compact_le_def 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

55 
by (simp add: Rep_compact_take approx_below) 
27289  56 
next 
57 
fix n :: nat and a :: "'a compact_basis" 

27406  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) 

27289  60 
next 
61 
fix n :: nat and a b :: "'a compact_basis" 

27406  62 
assume "a \<sqsubseteq> b" thus "compact_take n a \<sqsubseteq> compact_take n b" 
63 
unfolding compact_le_def Rep_compact_take 

27289  64 
by (rule monofun_cfun_arg) 
65 
next 

66 
fix n :: nat and a :: "'a compact_basis" 

27406  67 
show "\<And>n a. compact_take n a \<sqsubseteq> compact_take (Suc n) a" 
68 
unfolding compact_le_def Rep_compact_take 

27289  69 
by (rule chainE, simp) 
70 
next 

71 
fix n :: nat 

27406  72 
show "finite (range (compact_take n))" 
27289  73 
apply (rule finite_imageD [where f="Rep_compact_basis"]) 
74 
apply (rule finite_subset [where B="range (\<lambda>x. approx n\<cdot>x)"]) 

27406  75 
apply (clarsimp simp add: Rep_compact_take) 
27289  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" 

27406  81 
show "\<exists>n. compact_take n a = a" 
27289  82 
apply (simp add: Rep_compact_basis_inject [symmetric]) 
27406  83 
apply (simp add: Rep_compact_take) 
27309  84 
apply (rule profinite_compact_eq_approx) 
27289  85 
apply (rule compact_Rep_compact_basis) 
86 
done 

87 
qed 

25904  88 

27289  89 
text {* Ideal completion *} 
25904  90 

27289  91 
definition 
28890
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

92 
approximants :: "'a \<Rightarrow> 'a compact_basis set" where 
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

93 
"approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})" 
25904  94 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29511
diff
changeset

95 
interpretation compact_basis: 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

96 
ideal_completion below compact_take Rep_compact_basis approximants 
27289  97 
proof 
98 
fix w :: 'a 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

99 
show "preorder.ideal below (approximants w)" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

100 
proof (rule below.idealI) 
28890
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

101 
show "\<exists>x. x \<in> approximants w" 
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

102 
unfolding approximants_def 
27289  103 
apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI) 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

104 
apply (simp add: Abs_compact_basis_inverse approx_below) 
27289  105 
done 
106 
next 

107 
fix x y :: "'a compact_basis" 

28890
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

108 
assume "x \<in> approximants w" "y \<in> approximants w" 
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

109 
thus "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" 
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

110 
unfolding approximants_def 
27289  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) 

27309  114 
apply (drule profinite_compact_eq_approx) 
115 
apply (drule profinite_compact_eq_approx) 

27289  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) 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

119 
apply (simp add: Abs_compact_basis_inverse approx_below) 
27289  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" 

28890
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

125 
assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w" 
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

126 
unfolding approximants_def 
27289  127 
apply simp 
128 
apply (simp add: compact_le_def) 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

129 
apply (erule (1) below_trans) 
27289  130 
done 
131 
qed 

132 
next 

27297
2c42b1505f25
removed SetPcpo.thy and cpo instance for type bool;
huffman
parents:
27289
diff
changeset

133 
fix Y :: "nat \<Rightarrow> 'a" 
2c42b1505f25
removed SetPcpo.thy and cpo instance for type bool;
huffman
parents:
27289
diff
changeset

134 
assume Y: "chain Y" 
28890
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

135 
show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))" 
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

136 
unfolding approximants_def 
27297
2c42b1505f25
removed SetPcpo.thy and cpo instance for type bool;
huffman
parents:
27289
diff
changeset

137 
apply safe 
2c42b1505f25
removed SetPcpo.thy and cpo instance for type bool;
huffman
parents:
27289
diff
changeset

138 
apply (simp add: compactD2 [OF compact_Rep_compact_basis Y]) 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

139 
apply (erule below_trans, rule is_ub_thelub [OF Y]) 
27289  140 
done 
26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

141 
next 
27289  142 
fix a :: "'a compact_basis" 
28890
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

143 
show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}" 
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

144 
unfolding approximants_def compact_le_def .. 
26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

145 
next 
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

146 
fix x y :: "'a" 
28890
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

147 
assume "approximants x \<subseteq> approximants y" thus "x \<sqsubseteq> y" 
27289  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) 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

151 
apply (simp add: approximants_def Abs_compact_basis_inverse approx_below) 
28890
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

152 
apply (simp add: approximants_def Abs_compact_basis_inverse) 
27289  153 
done 
26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset

154 
qed 
25904  155 

27289  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 

28890
1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal;
huffman
parents:
28611
diff
changeset

165 
lemma compact_bot_minimal [simp]: "compact_bot \<sqsubseteq> a" 
27289  166 
unfolding compact_le_def Rep_compact_bot by simp 
167 

25904  168 

169 
subsection {* A compact basis for powerdomains *} 

170 

171 
typedef 'a pd_basis = 

26407
562a1d615336
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents:
26041
diff
changeset

172 
"{S::'a::profinite compact_basis set. finite S \<and> S \<noteq> {}}" 
25904  173 
by (rule_tac x="{arbitrary}" in exI, simp) 
174 

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 

177 

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 

180 

181 
text {* unit and plus *} 

182 

183 
definition 

184 
PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where 

185 
"PDUnit = (\<lambda>x. Abs_pd_basis {x})" 

186 

187 
definition 

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)" 

190 

191 
lemma Rep_PDUnit: 

192 
"Rep_pd_basis (PDUnit x) = {x}" 

193 
unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def) 

194 

195 
lemma Rep_PDPlus: 

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) 

198 

199 
lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)" 

200 
unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp 

201 

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) 

204 

205 
lemma PDPlus_commute: "PDPlus t u = PDPlus u t" 

206 
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute) 

207 

208 
lemma PDPlus_absorb: "PDPlus t t = t" 

209 
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb) 

210 

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)" 

214 
shows "P x" 

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) 

35901
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
31076
diff
changeset

220 
apply (simp add: PDUnit_def PDPlus_def 
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
31076
diff
changeset

221 
Abs_pd_basis_inverse [unfolded pd_basis_def]) 
25904  222 
done 
223 

224 
lemma pd_basis_induct: 

225 
assumes PDUnit: "\<And>a. P (PDUnit a)" 

226 
assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)" 

227 
shows "P x" 

228 
apply (induct x rule: pd_basis_induct1) 

229 
apply (rule PDUnit, erule PDPlus [OF PDUnit]) 

230 
done 

231 

232 
text {* foldpd *} 

233 

234 
definition 

235 
fold_pd :: 

236 
"('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b" 

237 
where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)" 

238 

26927  239 
lemma fold_pd_PDUnit: 
28611  240 
assumes "ab_semigroup_idem_mult f" 
26927  241 
shows "fold_pd g f (PDUnit x) = g x" 
25904  242 
unfolding fold_pd_def Rep_PDUnit by simp 
243 

26927  244 
lemma fold_pd_PDPlus: 
28611  245 
assumes "ab_semigroup_idem_mult f" 
26927  246 
shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)" 
28611  247 
proof  
29511
7071b017cb35
migrated class package to new locale implementation
haftmann
parents:
29252
diff
changeset

248 
interpret ab_semigroup_idem_mult f by fact 
35901
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
31076
diff
changeset

249 
show ?thesis unfolding fold_pd_def Rep_PDPlus 
12f09bf2c77f
fix LaTeX overfull hbox warnings in HOLCF document
huffman
parents:
31076
diff
changeset

250 
by (simp add: image_Un fold1_Un2) 
28611  251 
qed 
25904  252 

27405  253 
text {* Take function for powerdomain basis *} 
25904  254 

255 
definition 

27405  256 
pd_take :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where 
27406  257 
"pd_take n = (\<lambda>t. Abs_pd_basis (compact_take n ` Rep_pd_basis t))" 
25904  258 

27405  259 
lemma Rep_pd_take: 
27406  260 
"Rep_pd_basis (pd_take n t) = compact_take n ` Rep_pd_basis t" 
27405  261 
unfolding pd_take_def 
25904  262 
apply (rule Abs_pd_basis_inverse) 
263 
apply (simp add: pd_basis_def) 

264 
done 

265 

27405  266 
lemma pd_take_simps [simp]: 
27406  267 
"pd_take n (PDUnit a) = PDUnit (compact_take n a)" 
27405  268 
"pd_take n (PDPlus t u) = PDPlus (pd_take n t) (pd_take n u)" 
25904  269 
apply (simp_all add: Rep_pd_basis_inject [symmetric]) 
27405  270 
apply (simp_all add: Rep_pd_take Rep_PDUnit Rep_PDPlus image_Un) 
25904  271 
done 
272 

27405  273 
lemma pd_take_idem: "pd_take n (pd_take n t) = pd_take n t" 
25904  274 
apply (induct t rule: pd_basis_induct) 
27289  275 
apply (simp add: compact_basis.take_take) 
25904  276 
apply simp 
277 
done 

278 

27405  279 
lemma finite_range_pd_take: "finite (range (pd_take n))" 
27289  280 
apply (rule finite_imageD [where f="Rep_pd_basis"]) 
27406  281 
apply (rule finite_subset [where B="Pow (range (compact_take n))"]) 
27405  282 
apply (clarsimp simp add: Rep_pd_take) 
27289  283 
apply (simp add: compact_basis.finite_range_take) 
25904  284 
apply (rule inj_onI, simp add: Rep_pd_basis_inject) 
285 
done 

286 

27405  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) 

25904  289 
apply (induct t rule: pd_basis_induct) 
27289  290 
apply (cut_tac a=a in compact_basis.take_covers) 
25904  291 
apply (clarify, rule_tac x=n in exI) 
292 
apply (clarify, simp) 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

293 
apply (rule below_antisym) 
27289  294 
apply (rule compact_basis.take_less) 
295 
apply (drule_tac a=a in compact_basis.take_chain_le) 

25904  296 
apply simp 
297 
apply (clarify, rename_tac i j) 

298 
apply (rule_tac x="max i j" in exI, simp) 

299 
done 

300 

301 
end 