theory "Set-Cpo" imports "~~/src/HOL/HOLCF/HOLCF" begin default_sort type instantiation set :: (type) below begin definition below_set where "op ⊑ = op ⊆" 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 ⊆ UNION UNIV Y" 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 def 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