Theory Set-Cpo

theory "Set-Cpo"
imports HOLCF
begin

default_sort type

instantiation set :: (type) below
begin
  definition below_set where "(⊑) = (⊆)"
instance..  
end

instance set :: (type) po
  by standard (auto simp add: below_set_def)

lemma is_lub_set:
  "S <<| ⋃S"
  by(auto simp add: is_lub_def below_set_def is_ub_def)

lemma lub_set: "lub S = ⋃S"
  by (metis is_lub_set lub_eqI)
  
instance set  :: (type) cpo
  by standard (rule exI, rule is_lub_set)

lemma minimal_set: "{} ⊑ S"
  unfolding below_set_def by simp

instance set  :: (type) pcpo
  by standard (rule+, rule minimal_set)

lemma set_contI:
  assumes  "⋀ Y. chain Y ⟹ f (⨆ i. Y i) = ⋃ (f ` range Y)"
  shows "cont f"
proof(rule contI)
  fix Y :: "nat ⇒ 'a"
  assume "chain Y"
  hence "f (⨆ i. Y i) = ⋃ (f ` range Y)" by (rule assms)
  also have "… = ⋃ (range (λi. f (Y i)))" by simp
  finally
  show "range (λi. f (Y i)) <<| f (⨆ i. Y i)" using is_lub_set by metis
qed

lemma set_set_contI:
  assumes  "⋀ S. f (⋃S) = ⋃ (f ` S)"
  shows "cont f"
  by (metis set_contI assms is_lub_set  lub_eqI)

lemma adm_subseteq[simp]:
  assumes "cont f"
  shows "adm (λa. f a ⊆ S)"
by (rule admI)(auto simp add: cont2contlubE[OF assms] lub_set)

lemma adm_Ball[simp]: "adm (λS. ∀x∈S. P x)"
  by (auto intro!: admI  simp add: lub_set)

lemma finite_subset_chain:
  fixes Y :: "nat ⇒ 'a set"
  assumes "chain Y"
  assumes "S ⊆ ⋃(Y ` UNIV)"
  assumes "finite S"
  shows "∃i. S ⊆ Y i"
proof-
  from assms(2)
  have "∀x ∈ S. ∃ i. x ∈ Y i" by auto
  then obtain f where f: "∀ x∈ S. x ∈ Y (f x)" by metis

  define i where "i = Max (f ` S)"
  from ‹finite S›
  have "finite (f ` S)" by simp
  hence "∀ x∈S. f x ≤ i" unfolding i_def by auto
  with chain_mono[OF ‹chain Y›]
  have "∀ x∈S. Y (f x) ⊆ Y i" by (auto simp add: below_set_def)
  with f
  have "S ⊆ Y i" by auto
  thus ?thesis..
qed

lemma diff_cont[THEN cont_compose, simp, cont2cont]:
  fixes S' :: "'a set"
  shows  "cont (λS. S - S')"
by (rule set_set_contI) simp


end