25893
|
1 |
(* Title: HOLCF/SetPcpo.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Brian Huffman
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* Set as a pointed cpo *}
|
|
7 |
|
|
8 |
theory SetPcpo
|
|
9 |
imports Adm
|
|
10 |
begin
|
|
11 |
|
25897
|
12 |
instantiation set :: (type) po
|
25893
|
13 |
begin
|
|
14 |
|
|
15 |
definition
|
|
16 |
less_set_def: "(op \<sqsubseteq>) = (op \<subseteq>)"
|
|
17 |
|
25897
|
18 |
instance
|
|
19 |
by (intro_classes, auto simp add: less_set_def)
|
25893
|
20 |
|
25897
|
21 |
end
|
25893
|
22 |
|
|
23 |
instance set :: (finite) finite_po ..
|
|
24 |
|
|
25 |
lemma Union_is_lub: "A <<| Union A"
|
|
26 |
unfolding is_lub_def is_ub_def less_set_def by fast
|
|
27 |
|
|
28 |
instance set :: (type) dcpo
|
|
29 |
by (intro_classes, rule exI, rule Union_is_lub)
|
|
30 |
|
|
31 |
lemma lub_eq_Union: "lub = Union"
|
|
32 |
by (rule ext, rule thelubI [OF Union_is_lub])
|
|
33 |
|
|
34 |
instance set :: (type) pcpo
|
|
35 |
proof
|
|
36 |
have "\<forall>y::'a set. {} \<sqsubseteq> y" unfolding less_set_def by simp
|
|
37 |
thus "\<exists>x::'a set. \<forall>y. x \<sqsubseteq> y" ..
|
|
38 |
qed
|
|
39 |
|
|
40 |
lemma UU_eq_empty: "\<bottom> = {}"
|
|
41 |
by (rule UU_I [symmetric], simp add: less_set_def)
|
|
42 |
|
|
43 |
lemmas set_cpo_simps = less_set_def lub_eq_Union UU_eq_empty
|
|
44 |
|
|
45 |
subsection {* Admissibility of set predicates *}
|
|
46 |
|
|
47 |
lemma adm_nonempty: "adm (\<lambda>A. \<exists>x. x \<in> A)"
|
|
48 |
by (rule admI, force simp add: lub_eq_Union)
|
|
49 |
|
|
50 |
lemma adm_in: "adm (\<lambda>A. x \<in> A)"
|
|
51 |
by (rule admI, simp add: lub_eq_Union)
|
|
52 |
|
|
53 |
lemma adm_not_in: "adm (\<lambda>A. x \<notin> A)"
|
|
54 |
by (rule admI, simp add: lub_eq_Union)
|
|
55 |
|
|
56 |
lemma adm_Ball: "(\<And>x. adm (\<lambda>A. P A x)) \<Longrightarrow> adm (\<lambda>A. \<forall>x\<in>A. P A x)"
|
|
57 |
unfolding Ball_def by (simp add: adm_not_in)
|
|
58 |
|
|
59 |
lemma adm_Bex: "adm (\<lambda>A. Bex A P)"
|
|
60 |
by (rule admI, simp add: lub_eq_Union)
|
|
61 |
|
|
62 |
lemma adm_subset: "adm (\<lambda>A. A \<subseteq> B)"
|
|
63 |
by (rule admI, auto simp add: lub_eq_Union)
|
|
64 |
|
|
65 |
lemma adm_superset: "adm (\<lambda>A. B \<subseteq> A)"
|
|
66 |
by (rule admI, auto simp add: lub_eq_Union)
|
|
67 |
|
|
68 |
lemmas adm_set_lemmas =
|
|
69 |
adm_nonempty adm_in adm_not_in adm_Bex adm_Ball adm_subset adm_superset
|
|
70 |
|
|
71 |
subsection {* Compactness *}
|
|
72 |
|
|
73 |
lemma compact_empty: "compact {}"
|
|
74 |
by (fold UU_eq_empty, simp)
|
|
75 |
|
|
76 |
lemma compact_insert: "compact A \<Longrightarrow> compact (insert x A)"
|
|
77 |
unfolding compact_def set_cpo_simps
|
|
78 |
by (simp add: adm_set_lemmas)
|
|
79 |
|
|
80 |
lemma finite_imp_compact: "finite A \<Longrightarrow> compact A"
|
|
81 |
by (induct A set: finite, rule compact_empty, erule compact_insert)
|
|
82 |
|
|
83 |
end
|