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 


12 
instantiation set :: (type) sq_ord


13 
begin


14 


15 
definition


16 
less_set_def: "(op \<sqsubseteq>) = (op \<subseteq>)"


17 


18 
instance ..


19 
end


20 


21 
instance set :: (type) po


22 
by (intro_classes, auto simp add: less_set_def)


23 


24 
instance set :: (finite) finite_po ..


25 


26 
lemma Union_is_lub: "A << Union A"


27 
unfolding is_lub_def is_ub_def less_set_def by fast


28 


29 
instance set :: (type) dcpo


30 
by (intro_classes, rule exI, rule Union_is_lub)


31 


32 
lemma lub_eq_Union: "lub = Union"


33 
by (rule ext, rule thelubI [OF Union_is_lub])


34 


35 
instance set :: (type) pcpo


36 
proof


37 
have "\<forall>y::'a set. {} \<sqsubseteq> y" unfolding less_set_def by simp


38 
thus "\<exists>x::'a set. \<forall>y. x \<sqsubseteq> y" ..


39 
qed


40 


41 
lemma UU_eq_empty: "\<bottom> = {}"


42 
by (rule UU_I [symmetric], simp add: less_set_def)


43 


44 
lemmas set_cpo_simps = less_set_def lub_eq_Union UU_eq_empty


45 


46 
subsection {* Admissibility of set predicates *}


47 


48 
lemma adm_nonempty: "adm (\<lambda>A. \<exists>x. x \<in> A)"


49 
by (rule admI, force simp add: lub_eq_Union)


50 


51 
lemma adm_in: "adm (\<lambda>A. x \<in> A)"


52 
by (rule admI, simp add: lub_eq_Union)


53 


54 
lemma adm_not_in: "adm (\<lambda>A. x \<notin> A)"


55 
by (rule admI, simp add: lub_eq_Union)


56 


57 
lemma adm_Ball: "(\<And>x. adm (\<lambda>A. P A x)) \<Longrightarrow> adm (\<lambda>A. \<forall>x\<in>A. P A x)"


58 
unfolding Ball_def by (simp add: adm_not_in)


59 


60 
lemma adm_Bex: "adm (\<lambda>A. Bex A P)"


61 
by (rule admI, simp add: lub_eq_Union)


62 


63 
lemma adm_subset: "adm (\<lambda>A. A \<subseteq> B)"


64 
by (rule admI, auto simp add: lub_eq_Union)


65 


66 
lemma adm_superset: "adm (\<lambda>A. B \<subseteq> A)"


67 
by (rule admI, auto simp add: lub_eq_Union)


68 


69 
lemmas adm_set_lemmas =


70 
adm_nonempty adm_in adm_not_in adm_Bex adm_Ball adm_subset adm_superset


71 


72 
subsection {* Compactness *}


73 


74 
lemma compact_empty: "compact {}"


75 
by (fold UU_eq_empty, simp)


76 


77 
lemma compact_insert: "compact A \<Longrightarrow> compact (insert x A)"


78 
unfolding compact_def set_cpo_simps


79 
by (simp add: adm_set_lemmas)


80 


81 
lemma finite_imp_compact: "finite A \<Longrightarrow> compact A"


82 
by (induct A set: finite, rule compact_empty, erule compact_insert)


83 


84 
end
