(* 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. ∃𝒰. P 𝒰 ∧ 𝒰 ⊆ Collect Q ∧ ⋃𝒰 = S" definition intersection_of :: "('a set set ⇒ bool) ⇒ ('a set ⇒ bool) ⇒ 'a set ⇒ bool" (infixr "intersection'_of" 60) where "P intersection_of Q ≡ λS. ∃𝒰. P 𝒰 ∧ 𝒰 ⊆ Collect Q ∧ ⋂𝒰 = S" definition arbitrary:: "'a set set ⇒ bool" where "arbitrary 𝒰 ≡ 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 𝒰 where "𝒰 ⊆ Collect P" "S = ⋃𝒰" by (auto simp: union_of_def arbitrary_def) then show ?rhs unfolding intersection_of_def arbitrary_def by (rule_tac x="uminus ` 𝒰" in exI) auto next assume ?rhs then obtain 𝒰 where "𝒰 ⊆ {S. P (- S)}" "⋂𝒰 = - 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 ` 𝒰" 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: "∃𝒰'⊆Collect P. ⋃𝒰' = ⋃𝒰" if "𝒰 ⊆ {S. ∃𝒱⊆Collect P. ⋃𝒱 = S}" for 𝒰 proof - let ?𝒲 = "{V. ∃𝒱. 𝒱⊆Collect P ∧ V ∈ 𝒱 ∧ (∃S ∈ 𝒰. ⋃𝒱 = S)}" have *: "⋀x U. ⟦x ∈ U; U ∈ 𝒰⟧ ⟹ x ∈ ⋃?𝒲" using that apply simp apply (drule subsetD, assumption, auto) done show ?thesis apply (rule_tac x="{V. ∃𝒱. 𝒱⊆Collect P ∧ V ∈ 𝒱 ∧ (∃S ∈ 𝒰. ⋃𝒱 = S)}" in exI) using that by (blast intro: *) qed have 2: "∃𝒰'⊆{S. ∃𝒰⊆Collect P. ⋃𝒰 = S}. ⋃𝒰' = ⋃𝒰" if "𝒰 ⊆ Collect P" for 𝒰 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 ∈ 𝒰 ⟹ (arbitrary union_of P) S) ⟹ (arbitrary union_of P) (⋃𝒰)" 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 ∈ 𝒰 ⟹ (arbitrary intersection_of P) S) ⟹ (arbitrary intersection_of P) (⋂𝒰)" 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 𝒰 𝒱 where *: "𝒰 ⊆ Collect P" "⋃𝒰 = S" "𝒱 ⊆ Collect P" "⋃𝒱 = T" by (auto simp: union_of_def) then have "(arbitrary union_of P) (⋃C∈𝒰. ⋃D∈𝒱. 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 ` 𝒰" 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 𝒰 where "finite 𝒰" "S = ⋃𝒰" and 𝒰: "∀U∈𝒰. ∃𝒰. finite 𝒰 ∧ (𝒰 ⊆ Collect P) ∧ ⋃𝒰 = U" using S unfolding union_of_def by (auto simp: subset_eq) then obtain f where "∀U∈𝒰. finite (f U) ∧ (f U ⊆ Collect P) ∧ ⋃(f U) = U" by metis then show ?thesis unfolding union_of_def ‹S = ⋃𝒰› by (rule_tac x = "snd ` Sigma 𝒰 f" in exI) (fastforce simp: ‹finite 𝒰›) 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 𝒰; ⋀S. S ∈ 𝒰 ⟹ (finite union_of P) S⟧ ⟹ (finite union_of P) (⋃𝒰)" 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 𝒰; ⋀S. S ∈ 𝒰 ⟹ (finite intersection_of P) S⟧ ⟹ (finite intersection_of P) (⋂𝒰)" 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 𝒰 𝒱 where *: "𝒰 ⊆ Collect P" "⋃𝒰 = S" "finite 𝒰" "𝒱 ⊆ Collect P" "⋃𝒱 = T" "finite 𝒱" by (auto simp: union_of_def) then have "(finite union_of P) (⋃C∈𝒰. ⋃D∈𝒱. 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 𝒰 where "S = 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) ` 𝒰" in exI) auto qed moreover have "?lhs S" if R: "?rhs S" for S proof - obtain 𝒰 where "S = ⋃𝒰" "∀T∈𝒰. ∃V. P V ∧ U ∩ V = T" using R unfolding relative_to_def union_of_def by auto then obtain f where f: "⋀T. T ∈ 𝒰 ⟹ P (f T)" "⋀T. T ∈ 𝒰 ⟹ U ∩ (f T) = T" by metis then have "∃𝒰'⊆Collect P. ⋃𝒰' = ⋃ (f ` 𝒰)" by (metis image_subset_iff mem_Collect_eq) moreover have eq: "U ∩ ⋃ (f ` 𝒰) = ⋃𝒰" using f by auto ultimately show ?thesis unfolding relative_to_def union_of_def arbitrary_def ‹S = ⋃𝒰› 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 𝒰 where "S = U ∩ ⋃𝒰" "𝒰 ⊆ Collect P" "finite 𝒰" 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) ` 𝒰" in exI) auto qed moreover have "?lhs S" if R: "?rhs S" for S proof - obtain 𝒰 where "S = ⋃𝒰" "∀T∈𝒰. ∃V. P V ∧ U ∩ V = T" "finite 𝒰" using R unfolding relative_to_def union_of_def by auto then obtain f where f: "⋀T. T ∈ 𝒰 ⟹ P (f T)" "⋀T. T ∈ 𝒰 ⟹ U ∩ (f T) = T" by metis then have "∃𝒰'⊆Collect P. ⋃𝒰' = ⋃ (f ` 𝒰)" by (metis image_subset_iff mem_Collect_eq) moreover have eq: "U ∩ ⋃ (f ` 𝒰) = ⋃𝒰" using f by auto ultimately show ?thesis using ‹finite 𝒰› f unfolding relative_to_def union_of_def ‹S = ⋃𝒰› by (rule_tac x="⋃ (f ` 𝒰)" 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 𝒰 where "S = U ∩ ⋃𝒰" "𝒰 ⊆ Collect P" "countable 𝒰" 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) ` 𝒰" in exI) auto qed moreover have "?lhs S" if R: "?rhs S" for S proof - obtain 𝒰 where "S = ⋃𝒰" "∀T∈𝒰. ∃V. P V ∧ U ∩ V = T" "countable 𝒰" using R unfolding relative_to_def union_of_def by auto then obtain f where f: "⋀T. T ∈ 𝒰 ⟹ P (f T)" "⋀T. T ∈ 𝒰 ⟹ U ∩ (f T) = T" by metis then have "∃𝒰'⊆Collect P. ⋃𝒰' = ⋃ (f ` 𝒰)" by (metis image_subset_iff mem_Collect_eq) moreover have eq: "U ∩ ⋃ (f ` 𝒰) = ⋃𝒰" using f by auto ultimately show ?thesis using ‹countable 𝒰› f unfolding relative_to_def union_of_def ‹S = ⋃𝒰› by (rule_tac x="⋃ (f ` 𝒰)" 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 𝒰 where 𝒰: "S = 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 ∩ X) = S" "(∩) U ` 𝒰 ⊆ {T. ∃Ua. P Ua ∧ U ∩ Ua = T}" using 𝒰 by blast+ qed auto qed moreover have "?lhs S" if R: "?rhs S" for S proof - obtain 𝒰 where "S = U ∩ ⋂𝒰" "∀T∈𝒰. ∃V. P V ∧ U ∩ V = T" using R unfolding relative_to_def intersection_of_def by auto then obtain f where f: "⋀T. T ∈ 𝒰 ⟹ P (f T)" "⋀T. T ∈ 𝒰 ⟹ U ∩ (f T) = T" by metis then have "f ` 𝒰 ⊆ Collect P" by auto moreover have eq: "U ∩ ⋂(f ` 𝒰) = U ∩ ⋂𝒰" using f by auto ultimately show ?thesis unfolding relative_to_def intersection_of_def arbitrary_def ‹S = 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 𝒰 where 𝒰: "S = U ∩ ⋂𝒰" "𝒰 ⊆ Collect P" "finite 𝒰" 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 ∩ X) = S" "(∩) U ` 𝒰 ⊆ {T. ∃Ua. P Ua ∧ U ∩ Ua = T}" using 𝒰 by blast+ show "finite ((∩) U ` 𝒰)" by (simp add: ‹finite 𝒰›) qed auto qed moreover have "?lhs S" if R: "?rhs S" for S proof - obtain 𝒰 where "S = U ∩ ⋂𝒰" "∀T∈𝒰. ∃V. P V ∧ U ∩ V = T" "finite 𝒰" using R unfolding relative_to_def intersection_of_def by auto then obtain f where f: "⋀T. T ∈ 𝒰 ⟹ P (f T)" "⋀T. T ∈ 𝒰 ⟹ U ∩ (f T) = T" by metis then have "f ` 𝒰 ⊆ Collect P" by auto moreover have eq: "U ∩ ⋂ (f ` 𝒰) = U ∩ ⋂ 𝒰" using f by auto ultimately show ?thesis unfolding relative_to_def intersection_of_def ‹S = U ∩ ⋂𝒰› using ‹finite 𝒰› 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 𝒰 where 𝒰: "S = U ∩ ⋂𝒰" "𝒰 ⊆ Collect P" "countable 𝒰" 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 ∩ X) = S" "(∩) U ` 𝒰 ⊆ {T. ∃Ua. P Ua ∧ U ∩ Ua = T}" using 𝒰 by blast+ show "countable ((∩) U ` 𝒰)" by (simp add: ‹countable 𝒰›) qed auto qed moreover have "?lhs S" if R: "?rhs S" for S proof - obtain 𝒰 where "S = U ∩ ⋂𝒰" "∀T∈𝒰. ∃V. P V ∧ U ∩ V = T" "countable 𝒰" using R unfolding relative_to_def intersection_of_def by auto then obtain f where f: "⋀T. T ∈ 𝒰 ⟹ P (f T)" "⋀T. T ∈ 𝒰 ⟹ U ∩ (f T) = T" by metis then have "f ` 𝒰 ⊆ Collect P" by auto moreover have eq: "U ∩ ⋂ (f ` 𝒰) = U ∩ ⋂ 𝒰" using f by auto ultimately show ?thesis unfolding relative_to_def intersection_of_def ‹S = U ∩ ⋂𝒰› using ‹countable 𝒰› 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 𝒰 where "countable 𝒰" and 𝒰: "𝒰 ⊆ Collect P" "⋃𝒰 = S" by (metis union_of_def) define 𝒰' where "𝒰' ≡ (λC. -C) ` 𝒰" have "𝒰' ⊆ {S. P (- S)}" "⋂𝒰' = -S" using 𝒰'_def 𝒰 by auto then show ?rhs unfolding intersection_of_def by (metis 𝒰'_def ‹countable 𝒰› countable_image) next assume ?rhs then obtain 𝒰 where "countable 𝒰" and 𝒰: "𝒰 ⊆ {S. P (- S)}" "⋂𝒰 = -S" by (metis intersection_of_def) define 𝒰' where "𝒰' ≡ (λC. -C) ` 𝒰" have "𝒰' ⊆ Collect P" "⋃ 𝒰' = S" using 𝒰'_def 𝒰 by auto then show ?lhs unfolding union_of_def by (metis 𝒰'_def ‹countable 𝒰› 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 𝒰 where "countable 𝒰" and 𝒰: "𝒰 ⊆ Collect P" "⋃𝒰 = 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 𝒰 where "countable 𝒰" and 𝒰: "𝒰 ⊆ Collect (countable union_of P)" "⋃𝒰 = S" by (metis union_of_def) then have "∀U ∈ 𝒰. ∃𝒱. countable 𝒱 ∧ 𝒱 ⊆ Collect P ∧ U = ⋃𝒱" by (metis Ball_Collect union_of_def) then obtain ℱ where ℱ: "∀U ∈ 𝒰. countable (ℱ U) ∧ ℱ U ⊆ Collect P ∧ U = ⋃(ℱ U)" by metis have "countable (⋃ (ℱ ` 𝒰))" using ℱ ‹countable 𝒰› by blast moreover have "⋃ (ℱ ` 𝒰) ⊆ Collect P" by (simp add: Sup_le_iff ℱ) moreover have "⋃ (⋃ (ℱ ` 𝒰)) = S" by auto (metis Union_iff ℱ 𝒰(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 𝒰; ⋀S. S ∈ 𝒰 ⟹ (countable union_of P) S⟧ ⟹ (countable union_of P) (⋃ 𝒰)" 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 𝒰; ⋀S. S ∈ 𝒰 ⟹ (countable intersection_of P) S⟧ ⟹ (countable intersection_of P) (⋂ 𝒰)" 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 𝒰 where "countable 𝒰" and 𝒰: "𝒰 ⊆ Collect P" "⋃𝒰 = S" using S by (metis union_of_def) obtain 𝒱 where "countable 𝒱" and 𝒱: "𝒱 ⊆ Collect P" "⋃𝒱 = T" using T by (metis union_of_def) have "⋀U V. ⟦U ∈ 𝒰; V ∈ 𝒱⟧ ⟹ (countable union_of P) (U ∩ V)" using 𝒰 𝒱 by (metis Ball_Collect countable_union_of_inc local.Int) then have "(countable union_of P) (⋃U∈𝒰. ⋃V∈𝒱. U ∩ V)" by (meson ‹countable 𝒰› ‹countable 𝒱› countable_union_of_UN) moreover have "S ∩ T = (⋃U∈𝒰. ⋃V∈𝒱. U ∩ V)" by (simp add: 𝒰 𝒱) 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