author  huffman 
Fri, 16 May 2008 21:41:07 +0200  
changeset 26921  5d9f78c3d6de 
parent 26837  535290c908ae 
child 27180  51f3f3557ef4 
permissions  rwrr 
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 