author | huffman |
Mon, 14 Jan 2008 20:28:59 +0100 | |
changeset 25906 | 2179c6661218 |
parent 25897 | e9d45709bece |
child 26837 | 535290c908ae |
permissions | -rw-r--r-- |
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 |
||
25906
2179c6661218
class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
huffman
parents:
25897
diff
changeset
|
28 |
instance set :: (type) cpo |
25893 | 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 |