author | wenzelm |
Sat, 17 May 2008 13:54:30 +0200 | |
changeset 26928 | ca87aff1ad2d |
parent 26921 | 5d9f78c3d6de |
child 27180 | 51f3f3557ef4 |
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 |
||
26837
535290c908ae
Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents:
25906
diff
changeset
|
12 |
instantiation bool :: po |
25893 | 13 |
begin |
14 |
||
15 |
definition |
|
26837
535290c908ae
Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents:
25906
diff
changeset
|
16 |
less_bool_def: "(op \<sqsubseteq>) = (op \<longrightarrow>)" |
25893 | 17 |
|
25897 | 18 |
instance |
26921 | 19 |
by (intro_classes, unfold less_bool_def, safe) |
25893 | 20 |
|
25897 | 21 |
end |
25893 | 22 |
|
26837
535290c908ae
Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents:
25906
diff
changeset
|
23 |
lemma less_set_eq: "(op \<sqsubseteq>) = (op \<subseteq>)" |
535290c908ae
Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents:
25906
diff
changeset
|
24 |
by (simp add: less_fun_def less_bool_def le_fun_def le_bool_def expand_fun_eq) |
535290c908ae
Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents:
25906
diff
changeset
|
25 |
|
535290c908ae
Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents:
25906
diff
changeset
|
26 |
instance bool :: finite_po .. |
25893 | 27 |
|
28 |
lemma Union_is_lub: "A <<| Union A" |
|
26837
535290c908ae
Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents:
25906
diff
changeset
|
29 |
unfolding is_lub_def is_ub_def less_set_eq by fast |
25893 | 30 |
|
26837
535290c908ae
Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents:
25906
diff
changeset
|
31 |
instance bool :: cpo .. |
25893 | 32 |
|
33 |
lemma lub_eq_Union: "lub = Union" |
|
34 |
by (rule ext, rule thelubI [OF Union_is_lub]) |
|
35 |
||
26837
535290c908ae
Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents:
25906
diff
changeset
|
36 |
instance bool :: pcpo |
25893 | 37 |
proof |
26837
535290c908ae
Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents:
25906
diff
changeset
|
38 |
have "\<forall>y::bool. False \<sqsubseteq> y" unfolding less_bool_def by simp |
535290c908ae
Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents:
25906
diff
changeset
|
39 |
thus "\<exists>x::bool. \<forall>y. x \<sqsubseteq> y" .. |
25893 | 40 |
qed |
41 |
||
42 |
lemma UU_eq_empty: "\<bottom> = {}" |
|
26837
535290c908ae
Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents:
25906
diff
changeset
|
43 |
by (rule UU_I [symmetric], simp add: less_set_eq) |
25893 | 44 |
|
26837
535290c908ae
Replaced instance declarations for sets by instance declarations for bool.
berghofe
parents:
25906
diff
changeset
|
45 |
lemmas set_cpo_simps = less_set_eq lub_eq_Union UU_eq_empty |
25893 | 46 |
|
47 |
subsection {* Admissibility of set predicates *} |
|
48 |
||
49 |
lemma adm_nonempty: "adm (\<lambda>A. \<exists>x. x \<in> A)" |
|
50 |
by (rule admI, force simp add: lub_eq_Union) |
|
51 |
||
52 |
lemma adm_in: "adm (\<lambda>A. x \<in> A)" |
|
53 |
by (rule admI, simp add: lub_eq_Union) |
|
54 |
||
55 |
lemma adm_not_in: "adm (\<lambda>A. x \<notin> A)" |
|
56 |
by (rule admI, simp add: lub_eq_Union) |
|
57 |
||
58 |
lemma adm_Ball: "(\<And>x. adm (\<lambda>A. P A x)) \<Longrightarrow> adm (\<lambda>A. \<forall>x\<in>A. P A x)" |
|
59 |
unfolding Ball_def by (simp add: adm_not_in) |
|
60 |
||
61 |
lemma adm_Bex: "adm (\<lambda>A. Bex A P)" |
|
62 |
by (rule admI, simp add: lub_eq_Union) |
|
63 |
||
64 |
lemma adm_subset: "adm (\<lambda>A. A \<subseteq> B)" |
|
65 |
by (rule admI, auto simp add: lub_eq_Union) |
|
66 |
||
67 |
lemma adm_superset: "adm (\<lambda>A. B \<subseteq> A)" |
|
68 |
by (rule admI, auto simp add: lub_eq_Union) |
|
69 |
||
70 |
lemmas adm_set_lemmas = |
|
71 |
adm_nonempty adm_in adm_not_in adm_Bex adm_Ball adm_subset adm_superset |
|
72 |
||
73 |
subsection {* Compactness *} |
|
74 |
||
75 |
lemma compact_empty: "compact {}" |
|
76 |
by (fold UU_eq_empty, simp) |
|
77 |
||
78 |
lemma compact_insert: "compact A \<Longrightarrow> compact (insert x A)" |
|
79 |
unfolding compact_def set_cpo_simps |
|
80 |
by (simp add: adm_set_lemmas) |
|
81 |
||
82 |
lemma finite_imp_compact: "finite A \<Longrightarrow> compact A" |
|
83 |
by (induct A set: finite, rule compact_empty, erule compact_insert) |
|
84 |
||
85 |
end |