Theory SetPcpo

Up to index of Isabelle/HOLCF

theory SetPcpo
imports Adm
begin

(*  Title:      HOLCF/SetPcpo.thy
    ID:         $Id: SetPcpo.thy,v 1.5 2008/05/16 19:41:07 huffman Exp $
    Author:     Brian Huffman
*)

header {* Set as a pointed cpo *}

theory SetPcpo
imports Adm
begin

instantiation bool :: po
begin

definition
  less_bool_def: "(op \<sqsubseteq>) = (op -->)"

instance
by (intro_classes, unfold less_bool_def, safe)

end

lemma less_set_eq: "(op \<sqsubseteq>) = (op ⊆)"
  by (simp add: less_fun_def less_bool_def le_fun_def le_bool_def expand_fun_eq)

instance bool :: finite_po ..

lemma Union_is_lub: "A <<| Union A"
unfolding is_lub_def is_ub_def less_set_eq by fast

instance bool :: cpo ..

lemma lub_eq_Union: "lub = Union"
by (rule ext, rule thelubI [OF Union_is_lub])

instance bool :: pcpo
proof
  have "∀y::bool. False \<sqsubseteq> y" unfolding less_bool_def by simp
  thus "∃x::bool. ∀y. x \<sqsubseteq> y" ..
qed

lemma UU_eq_empty: "⊥ = {}"
by (rule UU_I [symmetric], simp add: less_set_eq)

lemmas set_cpo_simps = less_set_eq lub_eq_Union UU_eq_empty

subsection {* Admissibility of set predicates *}

lemma adm_nonempty: "adm (λA. ∃x. x ∈ A)"
by (rule admI, force simp add: lub_eq_Union)

lemma adm_in: "adm (λA. x ∈ A)"
by (rule admI, simp add: lub_eq_Union)

lemma adm_not_in: "adm (λA. x ∉ A)"
by (rule admI, simp add: lub_eq_Union)

lemma adm_Ball: "(!!x. adm (λA. P A x)) ==> adm (λA. ∀x∈A. P A x)"
unfolding Ball_def by (simp add: adm_not_in)

lemma adm_Bex: "adm (λA. Bex A P)"
by (rule admI, simp add: lub_eq_Union)

lemma adm_subset: "adm (λA. A ⊆ B)"
by (rule admI, auto simp add: lub_eq_Union)

lemma adm_superset: "adm (λA. B ⊆ A)"
by (rule admI, auto simp add: lub_eq_Union)

lemmas adm_set_lemmas =
  adm_nonempty adm_in adm_not_in adm_Bex adm_Ball adm_subset adm_superset

subsection {* Compactness *}

lemma compact_empty: "compact {}"
by (fold UU_eq_empty, simp)

lemma compact_insert: "compact A ==> compact (insert x A)"
unfolding compact_def set_cpo_simps
by (simp add: adm_set_lemmas)

lemma finite_imp_compact: "finite A ==> compact A"
by (induct A set: finite, rule compact_empty, erule compact_insert)

end

lemma less_set_eq:

  op << = op 

lemma Union_is_lub:

  A <<| Union A

lemma lub_eq_Union:

  lub = Union

lemma UU_eq_empty:

  UU = {}

lemma set_cpo_simps:

  op << = op 
  lub = Union
  UU = {}

Admissibility of set predicates

lemma adm_nonempty:

  admA. ∃x. xA)

lemma adm_in:

  adm (op ∈ x)

lemma adm_not_in:

  adm (op  x)

lemma adm_Ball:

  (!!x. admA. P A x)) ==> admA. ∀xA. P A x)

lemma adm_Bex:

  admA. Bex A P)

lemma adm_subset:

  admA. A  B)

lemma adm_superset:

  adm (op  B)

lemma adm_set_lemmas:

  admA. ∃x. xA)
  adm (op ∈ x)
  adm (op  x)
  admA. Bex A P)
  (!!x. admA. P A x)) ==> admA. ∀xA. P A x)
  admA. A  B)
  adm (op  B)

Compactness

lemma compact_empty:

  compact {}

lemma compact_insert:

  compact A ==> compact (insert x A)

lemma finite_imp_compact:

  finite A ==> compact A