Quelle  Set_Idioms.thy

(*  Title:      HOL/Library/Set_Idioms.thy
  Author: Lawrence Paulson (but borrowed from HOL Light)
*)

section ‹Set Idioms›

theory Set_Idioms
imports Countable_Set

begin


subsection‹Idioms for being a suitable union/intersection of something›

definition union_of :: "('a set set ==> bool) ==> ('a set ==> bool) ==> 'a set ==> bool"
  (infixr ‹union'_of› 60)
  where "P union_of Q ≡ λS. ∃U. P U ∧ U ⊆ Collect Q ∧ ∪U = S"

definition intersection_of :: "('a set set ==> bool) ==> ('a set ==> bool) ==> 'a set ==> bool"
  (infixr ‹intersection'_of› 60)
  where "P intersection_of Q ≡ λS. ∃U. P U ∧ U ⊆ Collect Q ∧ ∩U = S"

definition arbitrary:: "'a set set ==> bool" where "arbitrary U ≡ True"

lemma union_of_inc: "[P {S}; Q S] ==> (P union_of Q) S"
  by (auto simp: union_of_def)

lemma intersection_of_inc:
   "[P {S}; Q S] ==> (P intersection_of Q) S"
  by (auto simp: intersection_of_def)

lemma union_of_mono:
   "[(P union_of Q) S; ∧x. Q x ==> Q' x] ==> (P union_of Q') S"
  by (auto simp: union_of_def)

lemma intersection_of_mono:
   "[(P intersection_of Q) S; ∧x. Q x ==> Q' x] ==> (P intersection_of Q') S"
  by (auto simp: intersection_of_def)

lemma all_union_of:
     "(∀S. (P union_of Q) S ⟶ R S) ⟷ (∀T. P T ∧ T ⊆ Collect Q ⟶ R(∪T))"
  by (auto simp: union_of_def)

lemma all_intersection_of:
     "(∀S. (P intersection_of Q) S ⟶ R S) ⟷ (∀T. P T ∧ T ⊆ Collect Q ⟶ R(∩T))"
  by (auto simp: intersection_of_def)
             
lemma intersection_ofE:
     "[(P intersection_of Q) S; ∧T. [P T; T ⊆ Collect Q] ==> R(∩T)] ==> R S"
  by (auto simp: intersection_of_def)

lemma union_of_empty:
     "P {} ==> (P union_of Q) {}"
  by (auto simp: union_of_def)

lemma intersection_of_empty:
     "P {} ==> (P intersection_of Q) UNIV"
  by (auto simp: intersection_of_def)

text‹ The arbitrary and finite cases›

lemma arbitrary_union_of_alt:
   "(arbitrary union_of Q) S ⟷ (∀x ∈ S. ∃U. Q U ∧ x ∈ U ∧ U ⊆ S)"
 (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (force simp: union_of_def arbitrary_def)
next
  assume ?rhs
  then have "{U. Q U ∧ U ⊆ S} ⊆ Collect Q" "∪{U. Q U ∧ U ⊆ S} = S"
    by auto
  then show ?lhs
    unfolding union_of_def arbitrary_def by blast
qed

lemma arbitrary_union_of_empty [simp]: "(arbitrary union_of P) {}"
  by (force simp: union_of_def arbitrary_def)

lemma arbitrary_intersection_of_empty [simp]:
  "(arbitrary intersection_of P) UNIV"
  by (force simp: intersection_of_def arbitrary_def)

lemma arbitrary_union_of_inc:
  "P S ==> (arbitrary union_of P) S"
  by (force simp: union_of_inc arbitrary_def)

lemma arbitrary_intersection_of_inc:
  "P S ==> (arbitrary intersection_of P) S"
  by (force simp: intersection_of_inc arbitrary_def)

lemma arbitrary_union_of_complement:
   "(arbitrary union_of P) S ⟷ (arbitrary intersection_of (λS. P(- S))) (- S)"  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then obtain U where "U ⊆ Collect P" "S = ∪U"
    by (auto simp: union_of_def arbitrary_def)
  then show ?rhs
    unfolding intersection_of_def arbitrary_def
    by (rule_tac x="uminus ` U" in exI) auto
next
  assume ?rhs
  then obtain U where "U ⊆ {S. P (- S)}" "∩U = - S"
    by (auto simp: union_of_def intersection_of_def arbitrary_def)
  then show ?lhs
    unfolding union_of_def arbitrary_def
    by (rule_tac x="uminus ` U" in exI) auto
qed

lemma arbitrary_intersection_of_complement:
   "(arbitrary intersection_of P) S ⟷ (arbitrary union_of (λS. P(- S))) (- S)"
  by (simp add: arbitrary_union_of_complement)

lemma arbitrary_union_of_idempot [simp]:
  "arbitrary union_of arbitrary union_of P = arbitrary union_of P"
proof -
  have 1: "∃U'⊆Collect P. ∪U' = ∪U" if "U ⊆ {S. ∃V⊆Collect P. ∪V = S}" for U
  proof -
    let ?W = "{V. ∃V. V⊆Collect P ∧ V ∈ V ∧ (∃S ∈ U. ∪V = S)}"
    have *: "∧x U. [x ∈ U; U ∈ U] ==> x ∈ ∪?W"
      using that
      apply simp
      apply (drule subsetD, assumption, auto)
      done
    show ?thesis
    apply (rule_tac x="{V. ∃V. V⊆Collect P ∧ V ∈ V ∧ (∃S ∈ U. ∪V = S)}" in exI)
      using that by (blast intro: *)
  qed
  have 2: "∃U'⊆{S. ∃U⊆Collect P. ∪U = S}. ∪U' = ∪U" if "U ⊆ Collect P" for U
    by (metis (mono_tags, lifting) union_of_def arbitrary_union_of_inc that)
  show ?thesis
    unfolding union_of_def arbitrary_def by (force simp: 1 2)
qed

lemma arbitrary_intersection_of_idempot:
   "arbitrary intersection_of arbitrary intersection_of P = arbitrary intersection_of P" (is "?lhs = ?rhs")
proof -
  have "- ?lhs = - ?rhs"
    unfolding arbitrary_intersection_of_complement by simp
  then show ?thesis
    by simp
qed

lemma arbitrary_union_of_Union:
   "(∧S. S ∈ U ==> (arbitrary union_of P) S) ==> (arbitrary union_of P) (∪U)"
  by (metis union_of_def arbitrary_def arbitrary_union_of_idempot mem_Collect_eq subsetI)

lemma arbitrary_union_of_Un:
   "[(arbitrary union_of P) S; (arbitrary union_of P) T]
           ==> (arbitrary union_of P) (S ∪ T)"
  using arbitrary_union_of_Union [of "{S,T}"] by auto

lemma arbitrary_intersection_of_Inter:
   "(∧S. S ∈ U ==> (arbitrary intersection_of P) S) ==> (arbitrary intersection_of P) (∩U)"
  by (metis intersection_of_def arbitrary_def arbitrary_intersection_of_idempot mem_Collect_eq subsetI)

lemma arbitrary_intersection_of_Int:
   "[(arbitrary intersection_of P) S; (arbitrary intersection_of P) T]
           ==> (arbitrary intersection_of P) (S ∩ T)"
  using arbitrary_intersection_of_Inter [of "{S,T}"] by auto

lemma arbitrary_union_of_Int_eq:
  "(∀S T. (arbitrary union_of P) S ∧ (arbitrary union_of P) T
               ⟶ (arbitrary union_of P) (S ∩ T))
   ⟷ (∀S T. P S ∧ P T ⟶ (arbitrary union_of P) (S ∩ T))"  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (simp add: arbitrary_union_of_inc)
next
  assume R: ?rhs
  show ?lhs
  proof clarify
    fix S :: "'a set" and T :: "'a set"
    assume "(arbitrary union_of P) S" and "(arbitrary union_of P) T"
    then obtain U V where *: "U ⊆ Collect P" "∪U = S" "V ⊆ Collect P" "∪V = T"
      by (auto simp: union_of_def)
    then have "(arbitrary union_of P) (∪C∈U. ∪D∈V. C ∩ D)"
     using R by (blast intro: arbitrary_union_of_Union)
   then show "(arbitrary union_of P) (S ∩ T)"
     by (simp add: Int_UN_distrib2 *)
 qed
qed

lemma arbitrary_intersection_of_Un_eq:
   "(∀S T. (arbitrary intersection_of P) S ∧ (arbitrary intersection_of P) T
               ⟶ (arbitrary intersection_of P) (S ∪ T)) ⟷
        (∀S T. P S ∧ P T ⟶ (arbitrary intersection_of P) (S ∪ T))"
  apply (simp add: arbitrary_intersection_of_complement)
  using arbitrary_union_of_Int_eq [of "λS. P (- S)"]
  by (metis (no_types, lifting) arbitrary_def double_compl union_of_inc)

lemma finite_union_of_empty [simp]: "(finite union_of P) {}"
  by (simp add: union_of_empty)

lemma finite_intersection_of_empty [simp]: "(finite intersection_of P) UNIV"
  by (simp add: intersection_of_empty)

lemma finite_union_of_inc:
   "P S ==> (finite union_of P) S"
  by (simp add: union_of_inc)

lemma finite_intersection_of_inc:
   "P S ==> (finite intersection_of P) S"
  by (simp add: intersection_of_inc)

lemma finite_union_of_complement:
  "(finite union_of P) S ⟷ (finite intersection_of (λS. P(- S))) (- S)"
  unfolding union_of_def intersection_of_def
  apply safe
   apply (rule_tac x="uminus ` U" in exI, fastforce)+
  done

lemma finite_intersection_of_complement:
   "(finite intersection_of P) S ⟷ (finite union_of (λS. P(- S))) (- S)"
  by (simp add: finite_union_of_complement)

lemma finite_union_of_idempot [simp]:
  "finite union_of finite union_of P = finite union_of P"
proof -
  have "(finite union_of P) S" if S: "(finite union_of finite union_of P) S" for S
  proof -
    obtain U where "finite U" "S = ∪U" and U: "∀U∈U. ∃U. finite U ∧ (U ⊆ Collect P) ∧ ∪U = U"
      using S unfolding union_of_def by (auto simp: subset_eq)
    then obtain f where "∀U∈U. finite (f U) ∧ (f U ⊆ Collect P) ∧ ∪(f U) = U"
      by metis
    then show ?thesis
      unfolding union_of_def ‹S = ∪U›
      by (rule_tac x = "snd ` Sigma U f" in exI) (fastforce simp: ‹finite U›)
  qed
  moreover
  have "(finite union_of finite union_of P) S" if "(finite union_of P) S" for S
    by (simp add: finite_union_of_inc that)
  ultimately show ?thesis
    by force
qed

lemma finite_intersection_of_idempot [simp]:
   "finite intersection_of finite intersection_of P = finite intersection_of P"
  by (force simp: finite_intersection_of_complement)

lemma finite_union_of_Union:
   "[finite U; ∧S. S ∈ U ==> (finite union_of P) S] ==> (finite union_of P) (∪U)"
  using finite_union_of_idempot [of P]
  by (metis mem_Collect_eq subsetI union_of_def)

lemma finite_union_of_Un:
   "[(finite union_of P) S; (finite union_of P) T] ==> (finite union_of P) (S ∪ T)"
  by (auto simp: union_of_def)

lemma finite_intersection_of_Inter:
   "[finite U; ∧S. S ∈ U ==> (finite intersection_of P) S] ==> (finite intersection_of P) (∩U)"
  using finite_intersection_of_idempot [of P]
  by (metis intersection_of_def mem_Collect_eq subsetI)

lemma finite_intersection_of_Int:
   "[(finite intersection_of P) S; (finite intersection_of P) T]
           ==> (finite intersection_of P) (S ∩ T)"
  by (auto simp: intersection_of_def)

lemma finite_union_of_Int_eq:
   "(∀S T. (finite union_of P) S ∧ (finite union_of P) T ⟶ (finite union_of P) (S ∩ T))
    ⟷ (∀S T. P S ∧ P T ⟶ (finite union_of P) (S ∩ T))"
(is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (simp add: finite_union_of_inc)
next
  assume R: ?rhs
  show ?lhs
  proof clarify
    fix S :: "'a set" and T :: "'a set"
    assume "(finite union_of P) S" and "(finite union_of P) T"
    then obtain U V where *: "U ⊆ Collect P" "∪U = S" "finite U" "V ⊆ Collect P" "∪V = T" "finite V"
      by (auto simp: union_of_def)
    then have "(finite union_of P) (∪C∈U. ∪D∈V. C ∩ D)"
      using R
      by (blast intro: finite_union_of_Union)
   then show "(finite union_of P) (S ∩ T)"
     by (simp add: Int_UN_distrib2 *)
 qed
qed

lemma finite_intersection_of_Un_eq:
   "(∀S T. (finite intersection_of P) S ∧
               (finite intersection_of P) T
               ⟶ (finite intersection_of P) (S ∪ T)) ⟷
        (∀S T. P S ∧ P T ⟶ (finite intersection_of P) (S ∪ T))"
  apply (simp add: finite_intersection_of_complement)
  using finite_union_of_Int_eq [of "λS. P (- S)"]
  by (metis (no_types, lifting) double_compl)


abbreviation finite' :: "'a set ==> bool"
  where "finite' A ≡ finite A ∧ A ≠ {}"

lemma finite'_intersection_of_Int:
   "[(finite' intersection_of P) S; (finite' intersection_of P) T]
           ==> (finite' intersection_of P) (S ∩ T)"
  by (auto simp: intersection_of_def)

lemma finite'_intersection_of_inc:
   "P S ==> (finite' intersection_of P) S"
  by (simp add: intersection_of_inc)


subsection ‹The ``Relative to'' operator›

text‹A somewhat cheap but handy way of getting localized forms of various topological concepts
 (open, closed, borel, fsigma, gdelta etc.)›

definition relative_to :: "['a set ==> bool, 'a set, 'a set] ==> bool" (infixl ‹relative'_to› 55)
  where "P relative_to S ≡ λT. ∃U. P U ∧ S ∩ U = T"

lemma relative_to_UNIV [simp]: "(P relative_to UNIV) S ⟷ P S"
  by (simp add: relative_to_def)

lemma relative_to_imp_subset:
   "(P relative_to S) T ==> T ⊆ S"
  by (auto simp: relative_to_def)

lemma all_relative_to: "(∀S. (P relative_to U) S ⟶ Q S) ⟷ (∀S. P S ⟶ Q(U ∩ S))"
  by (auto simp: relative_to_def)

lemma relative_toE: "[(P relative_to U) S; ∧S. P S ==> Q(U ∩ S)] ==> Q S"
  by (auto simp: relative_to_def)

lemma relative_to_inc:
   "P S ==> (P relative_to U) (U ∩ S)"
  by (auto simp: relative_to_def)

lemma relative_to_relative_to [simp]:
   "P relative_to S relative_to T = P relative_to (S ∩ T)"
  unfolding relative_to_def
  by auto

lemma relative_to_compl:
   "S ⊆ U ==> ((P relative_to U) (U - S) ⟷ ((λc. P(- c)) relative_to U) S)"
  unfolding relative_to_def
  by (metis Diff_Diff_Int Diff_eq double_compl inf.absorb_iff2)

lemma relative_to_subset_trans:
   "[(P relative_to U) S; S ⊆ T; T ⊆ U] ==> (P relative_to T) S"
  unfolding relative_to_def by auto

lemma relative_to_mono:
   "[(P relative_to U) S; ∧S. P S ==> Q S] ==> (Q relative_to U) S"
  unfolding relative_to_def by auto

lemma relative_to_subset_inc: "[S ⊆ U; P S] ==> (P relative_to U) S"
  unfolding relative_to_def by auto

lemma relative_to_Int:
   "[(P relative_to S) C; (P relative_to S) D; ∧X Y. [P X; P Y] ==> P(X ∩ Y)]
         ==> (P relative_to S) (C ∩ D)"
  unfolding relative_to_def by auto

lemma relative_to_Un:
   "[(P relative_to S) C; (P relative_to S) D; ∧X Y. [P X; P Y] ==> P(X ∪ Y)]
         ==> (P relative_to S) (C ∪ D)"
  unfolding relative_to_def by auto

lemma arbitrary_union_of_relative_to:
  "((arbitrary union_of P) relative_to U) = (arbitrary union_of (P relative_to U))" (is "?lhs = ?rhs")
proof -
  have "?rhs S" if L: "?lhs S" for S
  proof -
    obtain U where "S = U ∩ ∪U" "U ⊆ Collect P"
      using L unfolding relative_to_def union_of_def by auto
    then show ?thesis
      unfolding relative_to_def union_of_def arbitrary_def
      by (rule_tac x="(λX. U ∩ X) ` U" in exI) auto
  qed
  moreover have "?lhs S" if R: "?rhs S" for S
  proof -
    obtain U where "S = ∪U" "∀T∈U. ∃V. P V ∧ U ∩ V = T"
      using R unfolding relative_to_def union_of_def by auto
    then obtain f where f: "∧T. T ∈ U ==> P (f T)" "∧T. T ∈ U ==> U ∩ (f T) = T"
      by metis
    then have "∃U'⊆Collect P. ∪U' = ∪ (f ` U)"
      by (metis image_subset_iff mem_Collect_eq)
    moreover have eq: "U ∩ ∪ (f ` U) = ∪U"
      using f by auto
    ultimately show ?thesis
      unfolding relative_to_def union_of_def arbitrary_def ‹S = ∪U›
      by metis
  qed
  ultimately show ?thesis
    by blast
qed

lemma finite_union_of_relative_to:
  "((finite union_of P) relative_to U) = (finite union_of (P relative_to U))" (is "?lhs = ?rhs")
proof -
  have "?rhs S" if L: "?lhs S" for S
  proof -
    obtain U where "S = U ∩ ∪U" "U ⊆ Collect P" "finite U"
      using L unfolding relative_to_def union_of_def by auto
    then show ?thesis
      unfolding relative_to_def union_of_def
      by (rule_tac x="(λX. U ∩ X) ` U" in exI) auto
  qed
  moreover have "?lhs S" if R: "?rhs S" for S
  proof -
    obtain U where "S = ∪U" "∀T∈U. ∃V. P V ∧ U ∩ V = T" "finite U"
      using R unfolding relative_to_def union_of_def by auto
    then obtain f where f: "∧T. T ∈ U ==> P (f T)" "∧T. T ∈ U ==> U ∩ (f T) = T"
      by metis
    then have "∃U'⊆Collect P. ∪U' = ∪ (f ` U)"
      by (metis image_subset_iff mem_Collect_eq)
    moreover have eq: "U ∩ ∪ (f ` U) = ∪U"
      using f by auto
    ultimately show ?thesis
      using ‹finite U› f
      unfolding relative_to_def union_of_def ‹S = ∪U›
      by (rule_tac x="∪ (f ` U)" in exI) (metis finite_imageI image_subsetI mem_Collect_eq)
  qed
  ultimately show ?thesis
    by blast
qed

lemma countable_union_of_relative_to:
  "((countable union_of P) relative_to U) = (countable union_of (P relative_to U))" (is "?lhs = ?rhs")
proof -
  have "?rhs S" if L: "?lhs S" for S
  proof -
    obtain U where "S = U ∩ ∪U" "U ⊆ Collect P" "countable U"
      using L unfolding relative_to_def union_of_def by auto
    then show ?thesis
      unfolding relative_to_def union_of_def
      by (rule_tac x="(λX. U ∩ X) ` U" in exI) auto
  qed
  moreover have "?lhs S" if R: "?rhs S" for S
  proof -
    obtain U where "S = ∪U" "∀T∈U. ∃V. P V ∧ U ∩ V = T" "countable U"
      using R unfolding relative_to_def union_of_def by auto
    then obtain f where f: "∧T. T ∈ U ==> P (f T)" "∧T. T ∈ U ==> U ∩ (f T) = T"
      by metis
    then have "∃U'⊆Collect P. ∪U' = ∪ (f ` U)"
      by (metis image_subset_iff mem_Collect_eq)
    moreover have eq: "U ∩ ∪ (f ` U) = ∪U"
      using f by auto
    ultimately show ?thesis
      using ‹countable U› f
      unfolding relative_to_def union_of_def ‹S = ∪U›
      by (rule_tac x="∪ (f ` U)" in exI) (metis countable_image image_subsetI mem_Collect_eq)
  qed
  ultimately show ?thesis
    by blast
qed


lemma arbitrary_intersection_of_relative_to:
  "((arbitrary intersection_of P) relative_to U) = ((arbitrary intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs")
proof -
  have "?rhs S" if L: "?lhs S" for S
  proof -
    obtain U where U: "S = U ∩ ∩U" "U ⊆ Collect P"
      using L unfolding relative_to_def intersection_of_def by auto
    show ?thesis
      unfolding relative_to_def intersection_of_def arbitrary_def
    proof (intro exI conjI)
      show "U ∩ (∩X∈U. U ∩ X) = S" "(∩) U ` U ⊆ {T. ∃Ua. P Ua ∧ U ∩ Ua = T}"
        using U by blast+
    qed auto
  qed
  moreover have "?lhs S" if R: "?rhs S" for S
  proof -
    obtain U where "S = U ∩ ∩U" "∀T∈U. ∃V. P V ∧ U ∩ V = T"
      using R unfolding relative_to_def intersection_of_def  by auto
    then obtain f where f: "∧T. T ∈ U ==> P (f T)" "∧T. T ∈ U ==> U ∩ (f T) = T"
      by metis
    then have "f ` U ⊆ Collect P"
      by auto
    moreover have eq: "U ∩ ∩(f ` U) = U ∩ ∩U"
      using f by auto
    ultimately show ?thesis
      unfolding relative_to_def intersection_of_def arbitrary_def ‹S = U ∩ ∩U›
      by auto
  qed
  ultimately show ?thesis
    by blast
qed

lemma finite_intersection_of_relative_to:
  "((finite intersection_of P) relative_to U) = ((finite intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs")
proof -
  have "?rhs S" if L: "?lhs S" for S
  proof -
    obtain U where U: "S = U ∩ ∩U" "U ⊆ Collect P" "finite U"
      using L unfolding relative_to_def intersection_of_def by auto
    show ?thesis
      unfolding relative_to_def intersection_of_def
    proof (intro exI conjI)
      show "U ∩ (∩X∈U. U ∩ X) = S" "(∩) U ` U ⊆ {T. ∃Ua. P Ua ∧ U ∩ Ua = T}"
        using U by blast+
      show "finite ((∩) U ` U)"
        by (simp add: ‹finite U›)
    qed auto
  qed
  moreover have "?lhs S" if R: "?rhs S" for S
  proof -
    obtain U where "S = U ∩ ∩U" "∀T∈U. ∃V. P V ∧ U ∩ V = T" "finite U"
      using R unfolding relative_to_def intersection_of_def  by auto
    then obtain f where f: "∧T. T ∈ U ==> P (f T)" "∧T. T ∈ U ==> U ∩ (f T) = T"
      by metis
    then have "f ` U ⊆ Collect P"
      by auto
    moreover have eq: "U ∩ ∩ (f ` U) = U ∩ ∩ U"
      using f by auto
    ultimately show ?thesis
      unfolding relative_to_def intersection_of_def ‹S = U ∩ ∩U›
      using ‹finite U›
      by auto
  qed
  ultimately show ?thesis
    by blast
qed

lemma countable_intersection_of_relative_to:
  "((countable intersection_of P) relative_to U) = ((countable intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs")
proof -
  have "?rhs S" if L: "?lhs S" for S
  proof -
    obtain U where U: "S = U ∩ ∩U" "U ⊆ Collect P" "countable U"
      using L unfolding relative_to_def intersection_of_def by auto
    show ?thesis
      unfolding relative_to_def intersection_of_def
    proof (intro exI conjI)
      show "U ∩ (∩X∈U. U ∩ X) = S" "(∩) U ` U ⊆ {T. ∃Ua. P Ua ∧ U ∩ Ua = T}"
        using U by blast+
      show "countable ((∩) U ` U)"
        by (simp add: ‹countable U›)
    qed auto
  qed
  moreover have "?lhs S" if R: "?rhs S" for S
  proof -
    obtain U where "S = U ∩ ∩U" "∀T∈U. ∃V. P V ∧ U ∩ V = T" "countable U"
      using R unfolding relative_to_def intersection_of_def  by auto
    then obtain f where f: "∧T. T ∈ U ==> P (f T)" "∧T. T ∈ U ==> U ∩ (f T) = T"
      by metis
    then have "f ` U ⊆ Collect P"
      by auto
    moreover have eq: "U ∩ ∩ (f ` U) = U ∩ ∩ U"
      using f by auto
    ultimately show ?thesis
      unfolding relative_to_def intersection_of_def ‹S = U ∩ ∩U›
      using ‹countable U› countable_image
      by auto
  qed
  ultimately show ?thesis
    by blast
qed

lemma countable_union_of_empty [simp]: "(countable union_of P) {}"
  by (simp add: union_of_empty)

lemma countable_intersection_of_empty [simp]: "(countable intersection_of P) UNIV"
  by (simp add: intersection_of_empty)

lemma countable_union_of_inc: "P S ==> (countable union_of P) S"
  by (simp add: union_of_inc)

lemma countable_intersection_of_inc: "P S ==> (countable intersection_of P) S"
  by (simp add: intersection_of_inc)

lemma countable_union_of_complement:
  "(countable union_of P) S ⟷ (countable intersection_of (λS. P(-S))) (-S)" 
  (is "?lhs=?rhs")
proof
  assume ?lhs
  then obtain U where "countable U" and U: "U ⊆ Collect P" "∪U = S"
    by (metis union_of_def)
  define U' where "U' ≡ (λC. -C) ` U"
  have "U' ⊆ {S. P (- S)}" "∩U' = -S"
    using U'_def U by auto
  then show ?rhs
    unfolding intersection_of_def by (metis U'_def ‹countable U› countable_image)
next
  assume ?rhs
  then obtain U where "countable U" and U: "U ⊆ {S. P (- S)}" "∩U = -S"
    by (metis intersection_of_def)
  define U' where "U' ≡ (λC. -C) ` U"
  have "U' ⊆ Collect P" "∪ U' = S"
    using U'_def U by auto
  then show ?lhs
    unfolding union_of_def
    by (metis U'_def ‹countable U› countable_image)
qed

lemma countable_intersection_of_complement:
   "(countable intersection_of P) S ⟷ (countable union_of (λS. P(- S))) (- S)"
  by (simp add: countable_union_of_complement)

lemma countable_union_of_explicit:
  assumes "P {}"
  shows "(countable union_of P) S ⟷
         (∃T. (∀n::nat. P(T n)) ∧ ∪(range T) = S)" (is "?lhs=?rhs")
proof
  assume ?lhs
  then obtain U where "countable U" and U: "U ⊆ Collect P" "∪U = S"
    by (metis union_of_def)
  then show ?rhs
    by (metis SUP_bot Sup_empty assms from_nat_into mem_Collect_eq range_from_nat_into subsetD)
next
  assume ?rhs
  then show ?lhs
    by (metis countableI_type countable_image image_subset_iff mem_Collect_eq union_of_def)
qed

lemma countable_union_of_ascending:
  assumes empty: "P {}" and Un: "∧T U. [P T; P U] ==> P(T ∪ U)"
  shows "(countable union_of P) S ⟷
         (∃T. (∀n. P(T n)) ∧ (∀n. T n ⊆ T(Suc n)) ∧ ∪(range T) = S)" (is "?lhs=?rhs")
proof
  assume ?lhs
  then obtain T where T: "∧n::nat. P(T n)" "∪(range T) = S"
    by (meson empty countable_union_of_explicit)
  have "P (∪ (T ` {..n}))" for n
    by (induction n) (auto simp: atMost_Suc Un T)
  with T show ?rhs
    by (rule_tac x="λn. ∪k≤n. T k" in exI) force
next
  assume ?rhs
  then show ?lhs
    using empty countable_union_of_explicit by auto
qed

lemma countable_union_of_idem [simp]:
  "countable union_of countable union_of P = countable union_of P"  (is "?lhs=?rhs")
proof
  fix S
  show "(countable union_of countable union_of P) S = (countable union_of P) S"
  proof
    assume L: "?lhs S"
    then obtain U where "countable U" and U: "U ⊆ Collect (countable union_of P)" "∪U = S"
      by (metis union_of_def)
    then have "∀U ∈ U. ∃V. countable V ∧ V ⊆ Collect P ∧ U = ∪V"
      by (metis Ball_Collect union_of_def)
    then obtain F where F: "∀U ∈ U. countable (F U) ∧ F U ⊆ Collect P ∧ U = ∪(F U)"
      by metis
    have "countable (∪ (F ` U))"
      using F ‹countable U› by blast
    moreover have "∪ (F ` U) ⊆ Collect P"
      by (simp add: Sup_le_iff F)
    moreover have "∪ (∪ (F ` U)) = S"
      by auto (metis Union_iff F U(2))+
    ultimately show "?rhs S"
      by (meson union_of_def)
  qed (simp add: countable_union_of_inc)
qed

lemma countable_intersection_of_idem [simp]:
   "countable intersection_of countable intersection_of P =
        countable intersection_of P"
  by (force simp: countable_intersection_of_complement)

lemma countable_union_of_Union:
   "[countable U; ∧S. S ∈ U ==> (countable union_of P) S]
        ==> (countable union_of P) (∪ U)"
  by (metis Ball_Collect countable_union_of_idem union_of_def)

lemma countable_union_of_UN:
   "[countable I; ∧i. i ∈ I ==> (countable union_of P) (U i)]
        ==> (countable union_of P) (∪i∈I. U i)"
  by (metis (mono_tags, lifting) countable_image countable_union_of_Union imageE)

lemma countable_union_of_Un:
  "[(countable union_of P) S; (countable union_of P) T]
           ==> (countable union_of P) (S ∪ T)"
  by (smt (verit) Union_Un_distrib countable_Un le_sup_iff union_of_def)

lemma countable_intersection_of_Inter:
   "[countable U; ∧S. S ∈ U ==> (countable intersection_of P) S]
        ==> (countable intersection_of P) (∩ U)"
  by (metis countable_intersection_of_idem intersection_of_def mem_Collect_eq subsetI)

lemma countable_intersection_of_INT:
   "[countable I; ∧i. i ∈ I ==> (countable intersection_of P) (U i)]
        ==> (countable intersection_of P) (∩i∈I. U i)"
  by (metis (mono_tags, lifting) countable_image countable_intersection_of_Inter imageE)

lemma countable_intersection_of_inter:
   "[(countable intersection_of P) S; (countable intersection_of P) T]
           ==> (countable intersection_of P) (S ∩ T)"
  by (simp add: countable_intersection_of_complement countable_union_of_Un)

lemma countable_union_of_Int:
  assumes S: "(countable union_of P) S" and T: "(countable union_of P) T"
    and Int: "∧S T. P S ∧ P T ==> P(S ∩ T)"
  shows "(countable union_of P) (S ∩ T)"
proof -
  obtain U where "countable U" and U: "U ⊆ Collect P" "∪U = S"
    using S by (metis union_of_def)
  obtain V where "countable V" and V: "V ⊆ Collect P" "∪V = T"
    using T by (metis union_of_def)
  have "∧U V. [U ∈ U; V ∈ V] ==> (countable union_of P) (U ∩ V)"
    using U V by (metis Ball_Collect countable_union_of_inc local.Int)
  then have "(countable union_of P) (∪U∈U. ∪V∈V. U ∩ V)"
    by (meson ‹countable U› ‹countable V› countable_union_of_UN)
  moreover have "S ∩ T = (∪U∈U. ∪V∈V. U ∩ V)"
    by (simp add: U V)
  ultimately show ?thesis
    by presburger
qed

lemma countable_intersection_of_union:
  assumes S: "(countable intersection_of P) S" and T: "(countable intersection_of P) T"
    and Un: "∧S T. P S ∧ P T ==> P(S ∪ T)"
  shows "(countable intersection_of P) (S ∪ T)"
  by (metis (mono_tags, lifting) Compl_Int S T Un compl_sup countable_intersection_of_complement countable_union_of_Int)

end