Quelle Set_Idioms.thy Sprache: Isabelle

(*  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 U 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 U 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 U
  proof -
    let ?W = "{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 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 \ \ \ (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 U V 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 U where "finite \" "S = \\" and U: "\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 = ∪U›
      by (rule_tac x = "snd ` Sigma \ 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 \; \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 U V 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 U 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 U 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 = ∪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 \ \\" "\ \ 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 U 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 U› f
      unfolding relative_to_def union_of_def ‹S = ∪U›
      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 U 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 U 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 U› f
      unfolding relative_to_def union_of_def ‹S = ∪U›
      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 U where U: "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 U by blast+
    qed auto
  qed
  moreover have "?lhs S" if R: "?rhs S" for S
  proof -
    obtain U 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 ∩ ∩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 \ \\" "\ \ 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 U by blast+
      show "finite ((\) 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 \ \\" "\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 ∩ ∩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 \ \\" "\ \ 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 U by blast+
      show "countable ((\) 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 \ \\" "\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 ∩ ∩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 \" and U: "\ \ Collect P" "\\ = S"
    by (metis union_of_def)
  define U' where "\' ≡ (λC. -C) ` U"
  have "\' \ {S. P (- S)}" "\\' = -S"
    using U'_def \ by auto
  then show ?rhs
    unfolding intersection_of_def by (metis U'_def \countable \\ countable_image)
next
  assume ?rhs
  then obtain U where "countable \" and U: "\ \ {S. P (- S)}" "\\ = -S"
    by (metis intersection_of_def)
  define U' where "\' ≡ (λC. -C) ` U"
  have "\' \ Collect P" "\ \' = S"
    using U'_def \ by auto
  then show ?lhs
    unfolding union_of_def
    by (metis U'_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 U where "countable \" and U: "\ \ 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 U where "countable \" and U: "\ \ 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 F where F: "\U \ \. countable (\ U) \ \ U \ Collect P \ U = \(\ U)"
      by metis
    have "countable (\ (\ ` \))"
      using F ‹countable U› by blast
    moreover have "\ (\ ` \) \ Collect P"
      by (simp add: Sup_le_iff F)
    moreover have "\ (\ (\ ` \)) = 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 \; \S. S \ \ \ (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 \; \S. S \ \ \ (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 \" and U: "\ \ Collect P" "\\ = S"
    using S by (metis union_of_def)
  obtain V where "countable \" and V: "\ \ Collect P" "\\ = T"
    using T by (metis union_of_def)
  have "\U V. \U \ \; 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\\. \V\\. U \ V)"
    by (meson ‹countable U› ‹countable V› countable_union_of_UN)
  moreover have "S \ T = (\U\\. \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

Messung V0.5

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

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 und die Messung sind noch experimentell.