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. xS. 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 " xS. f x  i" unfolding i_def by auto
  with chain_mono[OF chain Y]
  have " xS. 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