Bilddatei Set_Idioms.thy Sprache: Isabelle

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

section \<open>Set Idioms\<close>

theory Set_Idioms
imports Countable_Set

begin

subsection\<open>Idioms for being a suitable union/intersection of something\<close>

definition union_of :: "('a set set \ bool) \ ('a set \ bool) \ 'a set \ bool"
 (infixr \<open>union'_of\<close> 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 \<open>intersection'_of\<close> 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\<open> The arbitrary and finite cases\<close>

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 "\ \<subseteq> Collect P" "S = \<Union>\"
 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 "\ \<subseteq> {S. P (- S)}" "\<Inter>\ = - 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 ?\<W> = "{V. \<exists>\<V>. \<V>\<subseteq>Collect P \<and> V \<in> \<V> \<and> (\<exists>S \<in> \. \<Union>\<V> = 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\
 \<Longrightarrow> (arbitrary union_of P) (S \<union> 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\
 \<Longrightarrow> (arbitrary intersection_of P) (S \<inter> 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
 \<longrightarrow> (arbitrary union_of P) (S \<inter> T))
 \<longleftrightarrow> (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary union_of P) (S \<inter> 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 \ \<V> where *: "\ \<subseteq> Collect P" "\<Union>\ = S" "\<V> \<subseteq> Collect P" "\<Union>\<V> = 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
 \<longrightarrow> (arbitrary intersection_of P) (S \<union> T)) \<longleftrightarrow>
 (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary intersection_of P) (S \<union> 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 = \<Union>\" and \: "\<forall>U\<in>\. \<exists>\. finite \ \<and> (\ \<subseteq> Collect P) \<and> \<Union>\ = 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 \<open>S = \<Union>\\<close>
 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\
 \<Longrightarrow> (finite intersection_of P) (S \<inter> 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))
 \<longleftrightarrow> (\<forall>S T. P S \<and> P T \<longrightarrow> (finite union_of P) (S \<inter> 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 \ \<V> where *: "\ \<subseteq> Collect P" "\<Union>\ = S" "finite \" "\<V> \<subseteq> Collect P" "\<Union>\<V> = T" "finite \<V>"
 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
 \<longrightarrow> (finite intersection_of P) (S \<union> T)) \<longleftrightarrow>
 (\<forall>S T. P S \<and> P T \<longrightarrow> (finite intersection_of P) (S \<union> 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 \<Rightarrow> bool"
 where "finite' A \ finite A \ A \ {}"

lemma finite'_intersection_of_Int:
 "\(finite' intersection_of P) S; (finite' intersection_of P) T\
 \<Longrightarrow> (finite' intersection_of P) (S \<inter> 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 \<open>The ``Relative to'' operator\<close>

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

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)\
 \<Longrightarrow> (P relative_to S) (C \<inter> 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)\
 \<Longrightarrow> (P relative_to S) (C \<union> 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 \<inter> \<Union>\" "\ \<subseteq> 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 = \<Union>\" "\<forall>T\<in>\. \<exists>V. P V \<and> U \<inter> 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 \<open>S = \<Union>\\<close>
 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 \<inter> \<Union>\" "\ \<subseteq> 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 = \<Union>\" "\<forall>T\<in>\. \<exists>V. P V \<and> U \<inter> 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 \<open>finite \\<close> f
 unfolding relative_to_def union_of_def \<open>S = \<Union>\\<close>
 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 \<inter> \<Union>\" "\ \<subseteq> 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 = \<Union>\" "\<forall>T\<in>\. \<exists>V. P V \<and> U \<inter> 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 \<open>countable \\<close> f
 unfolding relative_to_def union_of_def \<open>S = \<Union>\\<close>
 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 \<inter> \<Inter>\" "\ \<subseteq> 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 \<inter> \<Inter>\" "\<forall>T\<in>\. \<exists>V. P V \<and> U \<inter> 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 \<open>S = U \<inter> \<Inter>\\<close>
 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 \<inter> \<Inter>\" "\ \<subseteq> 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: \<open>finite \\<close>)
 qed auto
 qed
 moreover have "?lhs S" if R: "?rhs S" for S
 proof -
 obtain \ where "S = U \<inter> \<Inter>\" "\<forall>T\<in>\. \<exists>V. P V \<and> U \<inter> 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 \<open>S = U \<inter> \<Inter>\\<close>
 using \<open>finite \\<close>
 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 \<inter> \<Inter>\" "\ \<subseteq> 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: \<open>countable \\<close>)
 qed auto
 qed
 moreover have "?lhs S" if R: "?rhs S" for S
 proof -
 obtain \ where "S = U \<inter> \<Inter>\" "\<forall>T\<in>\. \<exists>V. P V \<and> U \<inter> 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 \<open>S = U \<inter> \<Inter>\\<close>
 using \<open>countable \\<close> 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 \: "\ \<subseteq> Collect P" "\<Union>\ = S"
 by (metis union_of_def)
 define \' where "\' \<equiv> (\<lambda>C. -C) ` \"
 have "\' \ {S. P (- S)}" "\\' = -S"
 using \'_def \ by auto
 then show ?rhs
 unfolding intersection_of_def by (metis \'_def \<open>countable \\<close> countable_image)
next
 assume ?rhs
 then obtain \ where "countable \" and \: "\ \<subseteq> {S. P (- S)}" "\<Inter>\ = -S"
 by (metis intersection_of_def)
 define \' where "\' \<equiv> (\<lambda>C. -C) ` \"
 have "\' \ Collect P" "\ \' = S"
 using \'_def \ by auto
 then show ?lhs
 unfolding union_of_def
 by (metis \'_def \<open>countable \\<close> 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 \
 (\<exists>T. (\<forall>n::nat. P(T n)) \<and> \<Union>(range T) = S)" (is "?lhs=?rhs")
proof
 assume ?lhs
 then obtain \ where "countable \" and \: "\ \<subseteq> Collect P" "\<Union>\ = 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 \
 (\<exists>T. (\<forall>n. P(T n)) \<and> (\<forall>n. T n \<subseteq> T(Suc n)) \<and> \<Union>(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 \: "\ \<subseteq> Collect (countable union_of P)" "\<Union>\ = S"
 by (metis union_of_def)
 then have "\U \ \. \\. countable \ \ \ \ Collect P \ U = \\"
 by (metis Ball_Collect union_of_def)
 then obtain \<F> where \<F>: "\<forall>U \<in> \. countable (\<F> U) \<and> \<F> U \<subseteq> Collect P \<and> U = \<Union>(\<F> U)"
 by metis
 have "countable (\ (\ ` \))"
 using \<F> \<open>countable \\<close> by blast
 moreover have "\ (\ ` \) \ Collect P"
 by (simp add: Sup_le_iff \<F>)
 moreover have "\ (\ (\ ` \)) = S"
 by auto (metis Union_iff \<F> \(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\
 \<Longrightarrow> (countable union_of P) (\<Union> \)"
 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)\
 \<Longrightarrow> (countable union_of P) (\<Union>i\<in>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\
 \<Longrightarrow> (countable union_of P) (S \<union> 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\
 \<Longrightarrow> (countable intersection_of P) (\<Inter> \)"
 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)\
 \<Longrightarrow> (countable intersection_of P) (\<Inter>i\<in>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\
 \<Longrightarrow> (countable intersection_of P) (S \<inter> 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 \: "\ \<subseteq> Collect P" "\<Union>\ = S"
 using S by (metis union_of_def)
 obtain \<V> where "countable \<V>" and \<V>: "\<V> \<subseteq> Collect P" "\<Union>\<V> = T"
 using T by (metis union_of_def)
 have "\U V. \U \ \; V \ \\ \ (countable union_of P) (U \ V)"
 using \ \<V> by (metis Ball_Collect countable_union_of_inc local.Int)
 then have "(countable union_of P) (\U\\. \V\\. U \ V)"
 by (meson \<open>countable \\<close> \<open>countable \<V>\<close> countable_union_of_UN)
 moreover have "S \ T = (\U\\. \V\\. U \ V)"
 by (simp add: \ \<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

quality100%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.