author  wenzelm 
Thu, 22 Oct 2009 15:50:12 +0200  
changeset 33071  362f59fe5092 
parent 32997  e760950ba6c5 
child 34915  7894c7dab132 
permissions  rwrr 
27411  1 
(* Title: HOLCF/Universal.thy 
2 
Author: Brian Huffman 

3 
*) 

4 

5 
theory Universal 

6 
imports CompactBasis NatIso 

7 
begin 

8 

9 
subsection {* Basis datatype *} 

10 

11 
types ubasis = nat 

12 

13 
definition 

14 
node :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis set \<Rightarrow> ubasis" 

15 
where 

30505  16 
"node i a S = Suc (prod2nat (i, prod2nat (a, set2nat S)))" 
27411  17 

30505  18 
lemma node_not_0 [simp]: "node i a S \<noteq> 0" 
27411  19 
unfolding node_def by simp 
20 

30505  21 
lemma node_gt_0 [simp]: "0 < node i a S" 
27411  22 
unfolding node_def by simp 
23 

24 
lemma node_inject [simp]: 

30505  25 
"\<lbrakk>finite S; finite T\<rbrakk> 
26 
\<Longrightarrow> node i a S = node j b T \<longleftrightarrow> i = j \<and> a = b \<and> S = T" 

27411  27 
unfolding node_def by simp 
28 

30505  29 
lemma node_gt0: "i < node i a S" 
27411  30 
unfolding node_def less_Suc_eq_le 
31 
by (rule le_prod2nat_1) 

32 

30505  33 
lemma node_gt1: "a < node i a S" 
27411  34 
unfolding node_def less_Suc_eq_le 
35 
by (rule order_trans [OF le_prod2nat_1 le_prod2nat_2]) 

36 

37 
lemma nat_less_power2: "n < 2^n" 

38 
by (induct n) simp_all 

39 

30505  40 
lemma node_gt2: "\<lbrakk>finite S; b \<in> S\<rbrakk> \<Longrightarrow> b < node i a S" 
27411  41 
unfolding node_def less_Suc_eq_le set2nat_def 
42 
apply (rule order_trans [OF _ le_prod2nat_2]) 

43 
apply (rule order_trans [OF _ le_prod2nat_2]) 

30505  44 
apply (rule order_trans [where y="setsum (op ^ 2) {b}"]) 
27411  45 
apply (simp add: nat_less_power2 [THEN order_less_imp_le]) 
46 
apply (erule setsum_mono2, simp, simp) 

47 
done 

48 

49 
lemma eq_prod2nat_pairI: 

50 
"\<lbrakk>fst (nat2prod x) = a; snd (nat2prod x) = b\<rbrakk> \<Longrightarrow> x = prod2nat (a, b)" 

51 
by (erule subst, erule subst, simp) 

52 

53 
lemma node_cases: 

54 
assumes 1: "x = 0 \<Longrightarrow> P" 

30505  55 
assumes 2: "\<And>i a S. \<lbrakk>finite S; x = node i a S\<rbrakk> \<Longrightarrow> P" 
27411  56 
shows "P" 
57 
apply (cases x) 

58 
apply (erule 1) 

59 
apply (rule 2) 

60 
apply (rule finite_nat2set) 

61 
apply (simp add: node_def) 

62 
apply (rule eq_prod2nat_pairI [OF refl]) 

63 
apply (rule eq_prod2nat_pairI [OF refl refl]) 

64 
done 

65 

66 
lemma node_induct: 

67 
assumes 1: "P 0" 

30505  68 
assumes 2: "\<And>i a S. \<lbrakk>P a; finite S; \<forall>b\<in>S. P b\<rbrakk> \<Longrightarrow> P (node i a S)" 
27411  69 
shows "P x" 
70 
apply (induct x rule: nat_less_induct) 

71 
apply (case_tac n rule: node_cases) 

72 
apply (simp add: 1) 

73 
apply (simp add: 2 node_gt1 node_gt2) 

74 
done 

75 

76 
subsection {* Basis ordering *} 

77 

78 
inductive 

79 
ubasis_le :: "nat \<Rightarrow> nat \<Rightarrow> bool" 

80 
where 

30505  81 
ubasis_le_refl: "ubasis_le a a" 
27411  82 
 ubasis_le_trans: 
30505  83 
"\<lbrakk>ubasis_le a b; ubasis_le b c\<rbrakk> \<Longrightarrow> ubasis_le a c" 
27411  84 
 ubasis_le_lower: 
30505  85 
"finite S \<Longrightarrow> ubasis_le a (node i a S)" 
27411  86 
 ubasis_le_upper: 
30505  87 
"\<lbrakk>finite S; b \<in> S; ubasis_le a b\<rbrakk> \<Longrightarrow> ubasis_le (node i a S) b" 
27411  88 

89 
lemma ubasis_le_minimal: "ubasis_le 0 x" 

90 
apply (induct x rule: node_induct) 

91 
apply (rule ubasis_le_refl) 

92 
apply (erule ubasis_le_trans) 

93 
apply (erule ubasis_le_lower) 

94 
done 

95 

96 
subsubsection {* Generic take function *} 

97 

98 
function 

99 
ubasis_until :: "(ubasis \<Rightarrow> bool) \<Rightarrow> ubasis \<Rightarrow> ubasis" 

100 
where 

101 
"ubasis_until P 0 = 0" 

30505  102 
 "finite S \<Longrightarrow> ubasis_until P (node i a S) = 
103 
(if P (node i a S) then node i a S else ubasis_until P a)" 

27411  104 
apply clarify 
105 
apply (rule_tac x=b in node_cases) 

106 
apply simp 

107 
apply simp 

108 
apply fast 

109 
apply simp 

110 
apply simp 

111 
apply simp 

112 
done 

113 

114 
termination ubasis_until 

115 
apply (relation "measure snd") 

116 
apply (rule wf_measure) 

117 
apply (simp add: node_gt1) 

118 
done 

119 

120 
lemma ubasis_until: "P 0 \<Longrightarrow> P (ubasis_until P x)" 

121 
by (induct x rule: node_induct) simp_all 

122 

123 
lemma ubasis_until': "0 < ubasis_until P x \<Longrightarrow> P (ubasis_until P x)" 

124 
by (induct x rule: node_induct) auto 

125 

126 
lemma ubasis_until_same: "P x \<Longrightarrow> ubasis_until P x = x" 

127 
by (induct x rule: node_induct) simp_all 

128 

129 
lemma ubasis_until_idem: 

130 
"P 0 \<Longrightarrow> ubasis_until P (ubasis_until P x) = ubasis_until P x" 

131 
by (rule ubasis_until_same [OF ubasis_until]) 

132 

133 
lemma ubasis_until_0: 

134 
"\<forall>x. x \<noteq> 0 \<longrightarrow> \<not> P x \<Longrightarrow> ubasis_until P x = 0" 

135 
by (induct x rule: node_induct) simp_all 

136 

137 
lemma ubasis_until_less: "ubasis_le (ubasis_until P x) x" 

138 
apply (induct x rule: node_induct) 

139 
apply (simp add: ubasis_le_refl) 

140 
apply (simp add: ubasis_le_refl) 

141 
apply (rule impI) 

142 
apply (erule ubasis_le_trans) 

143 
apply (erule ubasis_le_lower) 

144 
done 

145 

146 
lemma ubasis_until_chain: 

147 
assumes PQ: "\<And>x. P x \<Longrightarrow> Q x" 

148 
shows "ubasis_le (ubasis_until P x) (ubasis_until Q x)" 

149 
apply (induct x rule: node_induct) 

150 
apply (simp add: ubasis_le_refl) 

151 
apply (simp add: ubasis_le_refl) 

152 
apply (simp add: PQ) 

153 
apply clarify 

154 
apply (rule ubasis_le_trans) 

155 
apply (rule ubasis_until_less) 

156 
apply (erule ubasis_le_lower) 

157 
done 

158 

159 
lemma ubasis_until_mono: 

30505  160 
assumes "\<And>i a S b. \<lbrakk>finite S; P (node i a S); b \<in> S; ubasis_le a b\<rbrakk> \<Longrightarrow> P b" 
161 
shows "ubasis_le a b \<Longrightarrow> ubasis_le (ubasis_until P a) (ubasis_until P b)" 

30561  162 
proof (induct set: ubasis_le) 
163 
case (ubasis_le_refl a) show ?case by (rule ubasis_le.ubasis_le_refl) 

164 
next 

165 
case (ubasis_le_trans a b c) thus ?case by  (rule ubasis_le.ubasis_le_trans) 

166 
next 

167 
case (ubasis_le_lower S a i) thus ?case 

168 
apply (clarsimp simp add: ubasis_le_refl) 

169 
apply (rule ubasis_le_trans [OF ubasis_until_less]) 

170 
apply (erule ubasis_le.ubasis_le_lower) 

171 
done 

172 
next 

173 
case (ubasis_le_upper S b a i) thus ?case 

174 
apply clarsimp 

175 
apply (subst ubasis_until_same) 

176 
apply (erule (3) prems) 

177 
apply (erule (2) ubasis_le.ubasis_le_upper) 

178 
done 

179 
qed 

27411  180 

181 
lemma finite_range_ubasis_until: 

182 
"finite {x. P x} \<Longrightarrow> finite (range (ubasis_until P))" 

183 
apply (rule finite_subset [where B="insert 0 {x. P x}"]) 

184 
apply (clarsimp simp add: ubasis_until') 

185 
apply simp 

186 
done 

187 

188 
subsubsection {* Take function for @{typ ubasis} *} 

189 

190 
definition 

191 
ubasis_take :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis" 

192 
where 

193 
"ubasis_take n = ubasis_until (\<lambda>x. x \<le> n)" 

194 

195 
lemma ubasis_take_le: "ubasis_take n x \<le> n" 

196 
unfolding ubasis_take_def by (rule ubasis_until, rule le0) 

197 

198 
lemma ubasis_take_same: "x \<le> n \<Longrightarrow> ubasis_take n x = x" 

199 
unfolding ubasis_take_def by (rule ubasis_until_same) 

200 

201 
lemma ubasis_take_idem: "ubasis_take n (ubasis_take n x) = ubasis_take n x" 

202 
by (rule ubasis_take_same [OF ubasis_take_le]) 

203 

204 
lemma ubasis_take_0 [simp]: "ubasis_take 0 x = 0" 

205 
unfolding ubasis_take_def by (simp add: ubasis_until_0) 

206 

207 
lemma ubasis_take_less: "ubasis_le (ubasis_take n x) x" 

208 
unfolding ubasis_take_def by (rule ubasis_until_less) 

209 

210 
lemma ubasis_take_chain: "ubasis_le (ubasis_take n x) (ubasis_take (Suc n) x)" 

211 
unfolding ubasis_take_def by (rule ubasis_until_chain) simp 

212 

213 
lemma ubasis_take_mono: 

214 
assumes "ubasis_le x y" 

215 
shows "ubasis_le (ubasis_take n x) (ubasis_take n y)" 

216 
unfolding ubasis_take_def 

217 
apply (rule ubasis_until_mono [OF _ prems]) 

218 
apply (frule (2) order_less_le_trans [OF node_gt2]) 

219 
apply (erule order_less_imp_le) 

220 
done 

221 

222 
lemma finite_range_ubasis_take: "finite (range (ubasis_take n))" 

223 
apply (rule finite_subset [where B="{..n}"]) 

224 
apply (simp add: subset_eq ubasis_take_le) 

225 
apply simp 

226 
done 

227 

228 
lemma ubasis_take_covers: "\<exists>n. ubasis_take n x = x" 

229 
apply (rule exI [where x=x]) 

230 
apply (simp add: ubasis_take_same) 

231 
done 

232 

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

233 
interpretation udom: preorder ubasis_le 
27411  234 
apply default 
235 
apply (rule ubasis_le_refl) 

236 
apply (erule (1) ubasis_le_trans) 

237 
done 

238 

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

239 
interpretation udom: basis_take ubasis_le ubasis_take 
27411  240 
apply default 
241 
apply (rule ubasis_take_less) 

242 
apply (rule ubasis_take_idem) 

243 
apply (erule ubasis_take_mono) 

244 
apply (rule ubasis_take_chain) 

245 
apply (rule finite_range_ubasis_take) 

246 
apply (rule ubasis_take_covers) 

247 
done 

248 

249 
subsection {* Defining the universal domain by ideal completion *} 

250 

251 
typedef (open) udom = "{S. udom.ideal S}" 

252 
by (fast intro: udom.ideal_principal) 

253 

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

254 
instantiation udom :: below 
27411  255 
begin 
256 

257 
definition 

258 
"x \<sqsubseteq> y \<longleftrightarrow> Rep_udom x \<subseteq> Rep_udom y" 

259 

260 
instance .. 

261 
end 

262 

263 
instance udom :: po 

264 
by (rule udom.typedef_ideal_po 

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

265 
[OF type_definition_udom below_udom_def]) 
27411  266 

267 
instance udom :: cpo 

268 
by (rule udom.typedef_ideal_cpo 

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

269 
[OF type_definition_udom below_udom_def]) 
27411  270 

271 
lemma Rep_udom_lub: 

272 
"chain Y \<Longrightarrow> Rep_udom (\<Squnion>i. Y i) = (\<Union>i. Rep_udom (Y i))" 

273 
by (rule udom.typedef_ideal_rep_contlub 

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

274 
[OF type_definition_udom below_udom_def]) 
27411  275 

276 
lemma ideal_Rep_udom: "udom.ideal (Rep_udom xs)" 

277 
by (rule Rep_udom [unfolded mem_Collect_eq]) 

278 

279 
definition 

280 
udom_principal :: "nat \<Rightarrow> udom" where 

281 
"udom_principal t = Abs_udom {u. ubasis_le u t}" 

282 

283 
lemma Rep_udom_principal: 

284 
"Rep_udom (udom_principal t) = {u. ubasis_le u t}" 

285 
unfolding udom_principal_def 

286 
by (simp add: Abs_udom_inverse udom.ideal_principal) 

287 

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

288 
interpretation udom: 
29237  289 
ideal_completion ubasis_le ubasis_take udom_principal Rep_udom 
27411  290 
apply unfold_locales 
291 
apply (rule ideal_Rep_udom) 

292 
apply (erule Rep_udom_lub) 

293 
apply (rule Rep_udom_principal) 

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

294 
apply (simp only: below_udom_def) 
27411  295 
done 
296 

297 
text {* Universal domain is pointed *} 

298 

299 
lemma udom_minimal: "udom_principal 0 \<sqsubseteq> x" 

300 
apply (induct x rule: udom.principal_induct) 

301 
apply (simp, simp add: ubasis_le_minimal) 

302 
done 

303 

304 
instance udom :: pcpo 

305 
by intro_classes (fast intro: udom_minimal) 

306 

307 
lemma inst_udom_pcpo: "\<bottom> = udom_principal 0" 

308 
by (rule udom_minimal [THEN UU_I, symmetric]) 

309 

310 
text {* Universal domain is bifinite *} 

311 

312 
instantiation udom :: bifinite 

313 
begin 

314 

315 
definition 

316 
approx_udom_def: "approx = udom.completion_approx" 

317 

318 
instance 

319 
apply (intro_classes, unfold approx_udom_def) 

320 
apply (rule udom.chain_completion_approx) 

321 
apply (rule udom.lub_completion_approx) 

322 
apply (rule udom.completion_approx_idem) 

323 
apply (rule udom.finite_fixes_completion_approx) 

324 
done 

325 

326 
end 

327 

328 
lemma approx_udom_principal [simp]: 

329 
"approx n\<cdot>(udom_principal x) = udom_principal (ubasis_take n x)" 

330 
unfolding approx_udom_def 

331 
by (rule udom.completion_approx_principal) 

332 

333 
lemma approx_eq_udom_principal: 

334 
"\<exists>a\<in>Rep_udom x. approx n\<cdot>x = udom_principal (ubasis_take n a)" 

335 
unfolding approx_udom_def 

336 
by (rule udom.completion_approx_eq_principal) 

337 

338 

339 
subsection {* Universality of @{typ udom} *} 

340 

341 
defaultsort bifinite 

342 

343 
subsubsection {* Choosing a maximal element from a finite set *} 

344 

345 
lemma finite_has_maximal: 

346 
fixes A :: "'a::po set" 

347 
shows "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq> y \<longrightarrow> x = y" 

348 
proof (induct rule: finite_ne_induct) 

349 
case (singleton x) 

350 
show ?case by simp 

351 
next 

352 
case (insert a A) 

353 
from `\<exists>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq> y \<longrightarrow> x = y` 

354 
obtain x where x: "x \<in> A" 

355 
and x_eq: "\<And>y. \<lbrakk>y \<in> A; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> x = y" by fast 

356 
show ?case 

357 
proof (intro bexI ballI impI) 

358 
fix y 

359 
assume "y \<in> insert a A" and "(if x \<sqsubseteq> a then a else x) \<sqsubseteq> y" 

360 
thus "(if x \<sqsubseteq> a then a else x) = y" 

361 
apply auto 

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

362 
apply (frule (1) below_trans) 
27411  363 
apply (frule (1) x_eq) 
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

364 
apply (rule below_antisym, assumption) 
27411  365 
apply simp 
366 
apply (erule (1) x_eq) 

367 
done 

368 
next 

369 
show "(if x \<sqsubseteq> a then a else x) \<in> insert a A" 

370 
by (simp add: x) 

371 
qed 

372 
qed 

373 

374 
definition 

375 
choose :: "'a compact_basis set \<Rightarrow> 'a compact_basis" 

376 
where 

377 
"choose A = (SOME x. x \<in> {x\<in>A. \<forall>y\<in>A. x \<sqsubseteq> y \<longrightarrow> x = y})" 

378 

379 
lemma choose_lemma: 

380 
"\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> choose A \<in> {x\<in>A. \<forall>y\<in>A. x \<sqsubseteq> y \<longrightarrow> x = y}" 

381 
unfolding choose_def 

382 
apply (rule someI_ex) 

383 
apply (frule (1) finite_has_maximal, fast) 

384 
done 

385 

386 
lemma maximal_choose: 

387 
"\<lbrakk>finite A; y \<in> A; choose A \<sqsubseteq> y\<rbrakk> \<Longrightarrow> choose A = y" 

388 
apply (cases "A = {}", simp) 

389 
apply (frule (1) choose_lemma, simp) 

390 
done 

391 

392 
lemma choose_in: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> choose A \<in> A" 

393 
by (frule (1) choose_lemma, simp) 

394 

395 
function 

396 
choose_pos :: "'a compact_basis set \<Rightarrow> 'a compact_basis \<Rightarrow> nat" 

397 
where 

398 
"choose_pos A x = 

399 
(if finite A \<and> x \<in> A \<and> x \<noteq> choose A 

400 
then Suc (choose_pos (A  {choose A}) x) else 0)" 

401 
by auto 

402 

403 
termination choose_pos 

404 
apply (relation "measure (card \<circ> fst)", simp) 

405 
apply clarsimp 

406 
apply (rule card_Diff1_less) 

407 
apply assumption 

408 
apply (erule choose_in) 

409 
apply clarsimp 

410 
done 

411 

412 
declare choose_pos.simps [simp del] 

413 

414 
lemma choose_pos_choose: "finite A \<Longrightarrow> choose_pos A (choose A) = 0" 

415 
by (simp add: choose_pos.simps) 

416 

417 
lemma inj_on_choose_pos [OF refl]: 

418 
"\<lbrakk>card A = n; finite A\<rbrakk> \<Longrightarrow> inj_on (choose_pos A) A" 

419 
apply (induct n arbitrary: A) 

420 
apply simp 

421 
apply (case_tac "A = {}", simp) 

422 
apply (frule (1) choose_in) 

423 
apply (rule inj_onI) 

424 
apply (drule_tac x="A  {choose A}" in meta_spec, simp) 

425 
apply (simp add: choose_pos.simps) 

426 
apply (simp split: split_if_asm) 

427 
apply (erule (1) inj_onD, simp, simp) 

428 
done 

429 

430 
lemma choose_pos_bounded [OF refl]: 

431 
"\<lbrakk>card A = n; finite A; x \<in> A\<rbrakk> \<Longrightarrow> choose_pos A x < n" 

432 
apply (induct n arbitrary: A) 

433 
apply simp 

434 
apply (case_tac "A = {}", simp) 

435 
apply (frule (1) choose_in) 

436 
apply (subst choose_pos.simps) 

437 
apply simp 

438 
done 

439 

440 
lemma choose_pos_lessD: 

441 
"\<lbrakk>choose_pos A x < choose_pos A y; finite A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<not> x \<sqsubseteq> y" 

442 
apply (induct A x arbitrary: y rule: choose_pos.induct) 

443 
apply simp 

444 
apply (case_tac "x = choose A") 

445 
apply simp 

446 
apply (rule notI) 

447 
apply (frule (2) maximal_choose) 

448 
apply simp 

449 
apply (case_tac "y = choose A") 

450 
apply (simp add: choose_pos_choose) 

451 
apply (drule_tac x=y in meta_spec) 

452 
apply simp 

453 
apply (erule meta_mp) 

454 
apply (simp add: choose_pos.simps) 

455 
done 

456 

457 
subsubsection {* Rank of basis elements *} 

458 

459 
primrec 

460 
cb_take :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" 

461 
where 

462 
"cb_take 0 = (\<lambda>x. compact_bot)" 

463 
 "cb_take (Suc n) = compact_take n" 

464 

465 
lemma cb_take_covers: "\<exists>n. cb_take n x = x" 

466 
apply (rule exE [OF compact_basis.take_covers [where a=x]]) 

467 
apply (rename_tac n, rule_tac x="Suc n" in exI, simp) 

468 
done 

469 

470 
lemma cb_take_less: "cb_take n x \<sqsubseteq> x" 

471 
by (cases n, simp, simp add: compact_basis.take_less) 

472 

473 
lemma cb_take_idem: "cb_take n (cb_take n x) = cb_take n x" 

474 
by (cases n, simp, simp add: compact_basis.take_take) 

475 

476 
lemma cb_take_mono: "x \<sqsubseteq> y \<Longrightarrow> cb_take n x \<sqsubseteq> cb_take n y" 

477 
by (cases n, simp, simp add: compact_basis.take_mono) 

478 

479 
lemma cb_take_chain_le: "m \<le> n \<Longrightarrow> cb_take m x \<sqsubseteq> cb_take n x" 

480 
apply (cases m, simp) 

481 
apply (cases n, simp) 

482 
apply (simp add: compact_basis.take_chain_le) 

483 
done 

484 

485 
lemma range_const: "range (\<lambda>x. c) = {c}" 

486 
by auto 

487 

488 
lemma finite_range_cb_take: "finite (range (cb_take n))" 

489 
apply (cases n) 

490 
apply (simp add: range_const) 

491 
apply (simp add: compact_basis.finite_range_take) 

492 
done 

493 

494 
definition 

495 
rank :: "'a compact_basis \<Rightarrow> nat" 

496 
where 

497 
"rank x = (LEAST n. cb_take n x = x)" 

498 

499 
lemma compact_approx_rank: "cb_take (rank x) x = x" 

500 
unfolding rank_def 

501 
apply (rule LeastI_ex) 

502 
apply (rule cb_take_covers) 

503 
done 

504 

505 
lemma rank_leD: "rank x \<le> n \<Longrightarrow> cb_take n x = x" 

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

506 
apply (rule below_antisym [OF cb_take_less]) 
27411  507 
apply (subst compact_approx_rank [symmetric]) 
508 
apply (erule cb_take_chain_le) 

509 
done 

510 

511 
lemma rank_leI: "cb_take n x = x \<Longrightarrow> rank x \<le> n" 

512 
unfolding rank_def by (rule Least_le) 

513 

514 
lemma rank_le_iff: "rank x \<le> n \<longleftrightarrow> cb_take n x = x" 

515 
by (rule iffI [OF rank_leD rank_leI]) 

516 

30505  517 
lemma rank_compact_bot [simp]: "rank compact_bot = 0" 
518 
using rank_leI [of 0 compact_bot] by simp 

519 

520 
lemma rank_eq_0_iff [simp]: "rank x = 0 \<longleftrightarrow> x = compact_bot" 

521 
using rank_le_iff [of x 0] by auto 

522 

27411  523 
definition 
524 
rank_le :: "'a compact_basis \<Rightarrow> 'a compact_basis set" 

525 
where 

526 
"rank_le x = {y. rank y \<le> rank x}" 

527 

528 
definition 

529 
rank_lt :: "'a compact_basis \<Rightarrow> 'a compact_basis set" 

530 
where 

531 
"rank_lt x = {y. rank y < rank x}" 

532 

533 
definition 

534 
rank_eq :: "'a compact_basis \<Rightarrow> 'a compact_basis set" 

535 
where 

536 
"rank_eq x = {y. rank y = rank x}" 

537 

538 
lemma rank_eq_cong: "rank x = rank y \<Longrightarrow> rank_eq x = rank_eq y" 

539 
unfolding rank_eq_def by simp 

540 

541 
lemma rank_lt_cong: "rank x = rank y \<Longrightarrow> rank_lt x = rank_lt y" 

542 
unfolding rank_lt_def by simp 

543 

544 
lemma rank_eq_subset: "rank_eq x \<subseteq> rank_le x" 

545 
unfolding rank_eq_def rank_le_def by auto 

546 

547 
lemma rank_lt_subset: "rank_lt x \<subseteq> rank_le x" 

548 
unfolding rank_lt_def rank_le_def by auto 

549 

550 
lemma finite_rank_le: "finite (rank_le x)" 

551 
unfolding rank_le_def 

552 
apply (rule finite_subset [where B="range (cb_take (rank x))"]) 

553 
apply clarify 

554 
apply (rule range_eqI) 

555 
apply (erule rank_leD [symmetric]) 

556 
apply (rule finite_range_cb_take) 

557 
done 

558 

559 
lemma finite_rank_eq: "finite (rank_eq x)" 

560 
by (rule finite_subset [OF rank_eq_subset finite_rank_le]) 

561 

562 
lemma finite_rank_lt: "finite (rank_lt x)" 

563 
by (rule finite_subset [OF rank_lt_subset finite_rank_le]) 

564 

565 
lemma rank_lt_Int_rank_eq: "rank_lt x \<inter> rank_eq x = {}" 

566 
unfolding rank_lt_def rank_eq_def rank_le_def by auto 

567 

568 
lemma rank_lt_Un_rank_eq: "rank_lt x \<union> rank_eq x = rank_le x" 

569 
unfolding rank_lt_def rank_eq_def rank_le_def by auto 

570 

30505  571 
subsubsection {* Sequencing basis elements *} 
27411  572 

573 
definition 

30505  574 
place :: "'a compact_basis \<Rightarrow> nat" 
27411  575 
where 
30505  576 
"place x = card (rank_lt x) + choose_pos (rank_eq x) x" 
27411  577 

30505  578 
lemma place_bounded: "place x < card (rank_le x)" 
579 
unfolding place_def 

27411  580 
apply (rule ord_less_eq_trans) 
581 
apply (rule add_strict_left_mono) 

582 
apply (rule choose_pos_bounded) 

583 
apply (rule finite_rank_eq) 

584 
apply (simp add: rank_eq_def) 

585 
apply (subst card_Un_disjoint [symmetric]) 

586 
apply (rule finite_rank_lt) 

587 
apply (rule finite_rank_eq) 

588 
apply (rule rank_lt_Int_rank_eq) 

589 
apply (simp add: rank_lt_Un_rank_eq) 

590 
done 

591 

30505  592 
lemma place_ge: "card (rank_lt x) \<le> place x" 
593 
unfolding place_def by simp 

27411  594 

30505  595 
lemma place_rank_mono: 
27411  596 
fixes x y :: "'a compact_basis" 
30505  597 
shows "rank x < rank y \<Longrightarrow> place x < place y" 
598 
apply (rule less_le_trans [OF place_bounded]) 

599 
apply (rule order_trans [OF _ place_ge]) 

27411  600 
apply (rule card_mono) 
601 
apply (rule finite_rank_lt) 

602 
apply (simp add: rank_le_def rank_lt_def subset_eq) 

603 
done 

604 

30505  605 
lemma place_eqD: "place x = place y \<Longrightarrow> x = y" 
27411  606 
apply (rule linorder_cases [where x="rank x" and y="rank y"]) 
30505  607 
apply (drule place_rank_mono, simp) 
608 
apply (simp add: place_def) 

27411  609 
apply (rule inj_on_choose_pos [where A="rank_eq x", THEN inj_onD]) 
610 
apply (rule finite_rank_eq) 

611 
apply (simp cong: rank_lt_cong rank_eq_cong) 

612 
apply (simp add: rank_eq_def) 

613 
apply (simp add: rank_eq_def) 

30505  614 
apply (drule place_rank_mono, simp) 
27411  615 
done 
616 

30505  617 
lemma inj_place: "inj place" 
618 
by (rule inj_onI, erule place_eqD) 

27411  619 

620 
subsubsection {* Embedding and projection on basis elements *} 

621 

30505  622 
definition 
623 
sub :: "'a compact_basis \<Rightarrow> 'a compact_basis" 

624 
where 

625 
"sub x = (case rank x of 0 \<Rightarrow> compact_bot  Suc k \<Rightarrow> cb_take k x)" 

626 

627 
lemma rank_sub_less: "x \<noteq> compact_bot \<Longrightarrow> rank (sub x) < rank x" 

628 
unfolding sub_def 

629 
apply (cases "rank x", simp) 

630 
apply (simp add: less_Suc_eq_le) 

631 
apply (rule rank_leI) 

632 
apply (rule cb_take_idem) 

633 
done 

634 

635 
lemma place_sub_less: "x \<noteq> compact_bot \<Longrightarrow> place (sub x) < place x" 

636 
apply (rule place_rank_mono) 

637 
apply (erule rank_sub_less) 

638 
done 

639 

640 
lemma sub_below: "sub x \<sqsubseteq> x" 

641 
unfolding sub_def by (cases "rank x", simp_all add: cb_take_less) 

642 

643 
lemma rank_less_imp_below_sub: "\<lbrakk>x \<sqsubseteq> y; rank x < rank y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> sub y" 

644 
unfolding sub_def 

645 
apply (cases "rank y", simp) 

646 
apply (simp add: less_Suc_eq_le) 

647 
apply (subgoal_tac "cb_take nat x \<sqsubseteq> cb_take nat y") 

648 
apply (simp add: rank_leD) 

649 
apply (erule cb_take_mono) 

650 
done 

651 

27411  652 
function 
653 
basis_emb :: "'a compact_basis \<Rightarrow> ubasis" 

654 
where 

655 
"basis_emb x = (if x = compact_bot then 0 else 

30505  656 
node (place x) (basis_emb (sub x)) 
657 
(basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y}))" 

27411  658 
by auto 
659 

660 
termination basis_emb 

30505  661 
apply (relation "measure place", simp) 
662 
apply (simp add: place_sub_less) 

27411  663 
apply simp 
664 
done 

665 

666 
declare basis_emb.simps [simp del] 

667 

668 
lemma basis_emb_compact_bot [simp]: "basis_emb compact_bot = 0" 

669 
by (simp add: basis_emb.simps) 

670 

30505  671 
lemma fin1: "finite {y. place y < place x \<and> x \<sqsubseteq> y}" 
27411  672 
apply (subst Collect_conj_eq) 
673 
apply (rule finite_Int) 

674 
apply (rule disjI1) 

30505  675 
apply (subgoal_tac "finite (place ` {n. n < place x})", simp) 
676 
apply (rule finite_vimageI [OF _ inj_place]) 

27411  677 
apply (simp add: lessThan_def [symmetric]) 
678 
done 

679 

30505  680 
lemma fin2: "finite (basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y})" 
27411  681 
by (rule finite_imageI [OF fin1]) 
682 

30505  683 
lemma rank_place_mono: 
684 
"\<lbrakk>place x < place y; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> rank x < rank y" 

685 
apply (rule linorder_cases, assumption) 

686 
apply (simp add: place_def cong: rank_lt_cong rank_eq_cong) 

687 
apply (drule choose_pos_lessD) 

688 
apply (rule finite_rank_eq) 

689 
apply (simp add: rank_eq_def) 

690 
apply (simp add: rank_eq_def) 

691 
apply simp 

692 
apply (drule place_rank_mono, simp) 

693 
done 

694 

695 
lemma basis_emb_mono: 

696 
"x \<sqsubseteq> y \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)" 

697 
proof (induct n \<equiv> "max (place x) (place y)" arbitrary: x y rule: less_induct) 

27411  698 
case (less n) 
30505  699 
hence IH: 
700 
"\<And>(a::'a compact_basis) b. 

701 
\<lbrakk>max (place a) (place b) < max (place x) (place y); a \<sqsubseteq> b\<rbrakk> 

702 
\<Longrightarrow> ubasis_le (basis_emb a) (basis_emb b)" 

703 
by simp 

704 
show ?case proof (rule linorder_cases) 

705 
assume "place x < place y" 

706 
then have "rank x < rank y" 

707 
using `x \<sqsubseteq> y` by (rule rank_place_mono) 

708 
with `place x < place y` show ?case 

709 
apply (case_tac "y = compact_bot", simp) 

710 
apply (simp add: basis_emb.simps [of y]) 

711 
apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]]) 

712 
apply (rule IH) 

713 
apply (simp add: less_max_iff_disj) 

714 
apply (erule place_sub_less) 

715 
apply (erule rank_less_imp_below_sub [OF `x \<sqsubseteq> y`]) 

27411  716 
done 
30505  717 
next 
718 
assume "place x = place y" 

719 
hence "x = y" by (rule place_eqD) 

720 
thus ?case by (simp add: ubasis_le_refl) 

721 
next 

722 
assume "place x > place y" 

723 
with `x \<sqsubseteq> y` show ?case 

724 
apply (case_tac "x = compact_bot", simp add: ubasis_le_minimal) 

725 
apply (simp add: basis_emb.simps [of x]) 

726 
apply (rule ubasis_le_upper [OF fin2], simp) 

727 
apply (rule IH) 

728 
apply (simp add: less_max_iff_disj) 

729 
apply (erule place_sub_less) 

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

730 
apply (erule rev_below_trans) 
30505  731 
apply (rule sub_below) 
732 
done 

27411  733 
qed 
734 
qed 

735 

736 
lemma inj_basis_emb: "inj basis_emb" 

737 
apply (rule inj_onI) 

738 
apply (case_tac "x = compact_bot") 

739 
apply (case_tac [!] "y = compact_bot") 

740 
apply simp 

741 
apply (simp add: basis_emb.simps) 

742 
apply (simp add: basis_emb.simps) 

743 
apply (simp add: basis_emb.simps) 

30505  744 
apply (simp add: fin2 inj_eq [OF inj_place]) 
27411  745 
done 
746 

747 
definition 

30505  748 
basis_prj :: "ubasis \<Rightarrow> 'a compact_basis" 
27411  749 
where 
750 
"basis_prj x = inv basis_emb 

30505  751 
(ubasis_until (\<lambda>x. x \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> ubasis)) x)" 
27411  752 

753 
lemma basis_prj_basis_emb: "\<And>x. basis_prj (basis_emb x) = x" 

754 
unfolding basis_prj_def 

755 
apply (subst ubasis_until_same) 

756 
apply (rule rangeI) 

757 
apply (rule inv_f_f) 

758 
apply (rule inj_basis_emb) 

759 
done 

760 

761 
lemma basis_prj_node: 

30505  762 
"\<lbrakk>finite S; node i a S \<notin> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)\<rbrakk> 
763 
\<Longrightarrow> basis_prj (node i a S) = (basis_prj a :: 'a compact_basis)" 

27411  764 
unfolding basis_prj_def by simp 
765 

766 
lemma basis_prj_0: "basis_prj 0 = compact_bot" 

767 
apply (subst basis_emb_compact_bot [symmetric]) 

768 
apply (rule basis_prj_basis_emb) 

769 
done 

770 

30505  771 
lemma node_eq_basis_emb_iff: 
772 
"finite S \<Longrightarrow> node i a S = basis_emb x \<longleftrightarrow> 

773 
x \<noteq> compact_bot \<and> i = place x \<and> a = basis_emb (sub x) \<and> 

774 
S = basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y}" 

775 
apply (cases "x = compact_bot", simp) 

776 
apply (simp add: basis_emb.simps [of x]) 

777 
apply (simp add: fin2) 

27411  778 
done 
779 

30505  780 
lemma basis_prj_mono: "ubasis_le a b \<Longrightarrow> basis_prj a \<sqsubseteq> basis_prj b" 
781 
proof (induct a b rule: ubasis_le.induct) 

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

782 
case (ubasis_le_refl a) show ?case by (rule below_refl) 
30505  783 
next 
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

784 
case (ubasis_le_trans a b c) thus ?case by  (rule below_trans) 
30505  785 
next 
786 
case (ubasis_le_lower S a i) thus ?case 

30561  787 
apply (cases "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)") 
30505  788 
apply (erule rangeE, rename_tac x) 
789 
apply (simp add: basis_prj_basis_emb) 

790 
apply (simp add: node_eq_basis_emb_iff) 

791 
apply (simp add: basis_prj_basis_emb) 

792 
apply (rule sub_below) 

793 
apply (simp add: basis_prj_node) 

794 
done 

795 
next 

796 
case (ubasis_le_upper S b a i) thus ?case 

30561  797 
apply (cases "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)") 
30505  798 
apply (erule rangeE, rename_tac x) 
799 
apply (simp add: basis_prj_basis_emb) 

800 
apply (clarsimp simp add: node_eq_basis_emb_iff) 

801 
apply (simp add: basis_prj_basis_emb) 

802 
apply (simp add: basis_prj_node) 

803 
done 

804 
qed 

805 

27411  806 
lemma basis_emb_prj_less: "ubasis_le (basis_emb (basis_prj x)) x" 
807 
unfolding basis_prj_def 

33071
362f59fe5092
renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538);
wenzelm
parents:
32997
diff
changeset

808 
apply (subst f_inv_into_f [where f=basis_emb]) 
27411  809 
apply (rule ubasis_until) 
810 
apply (rule range_eqI [where x=compact_bot]) 

811 
apply simp 

812 
apply (rule ubasis_until_less) 

813 
done 

814 

815 
hide (open) const 

816 
node 

817 
choose 

818 
choose_pos 

30505  819 
place 
820 
sub 

27411  821 

822 
subsubsection {* EPpair from any bifinite domain into @{typ udom} *} 

823 

824 
definition 

825 
udom_emb :: "'a::bifinite \<rightarrow> udom" 

826 
where 

827 
"udom_emb = compact_basis.basis_fun (\<lambda>x. udom_principal (basis_emb x))" 

828 

829 
definition 

830 
udom_prj :: "udom \<rightarrow> 'a::bifinite" 

831 
where 

832 
"udom_prj = udom.basis_fun (\<lambda>x. Rep_compact_basis (basis_prj x))" 

833 

834 
lemma udom_emb_principal: 

835 
"udom_emb\<cdot>(Rep_compact_basis x) = udom_principal (basis_emb x)" 

836 
unfolding udom_emb_def 

837 
apply (rule compact_basis.basis_fun_principal) 

838 
apply (rule udom.principal_mono) 

839 
apply (erule basis_emb_mono) 

840 
done 

841 

842 
lemma udom_prj_principal: 

843 
"udom_prj\<cdot>(udom_principal x) = Rep_compact_basis (basis_prj x)" 

844 
unfolding udom_prj_def 

845 
apply (rule udom.basis_fun_principal) 

846 
apply (rule compact_basis.principal_mono) 

847 
apply (erule basis_prj_mono) 

848 
done 

849 

850 
lemma ep_pair_udom: "ep_pair udom_emb udom_prj" 

851 
apply default 

852 
apply (rule compact_basis.principal_induct, simp) 

853 
apply (simp add: udom_emb_principal udom_prj_principal) 

854 
apply (simp add: basis_prj_basis_emb) 

855 
apply (rule udom.principal_induct, simp) 

856 
apply (simp add: udom_emb_principal udom_prj_principal) 

857 
apply (rule basis_emb_prj_less) 

858 
done 

859 

860 
end 