Quelle Countable_Set.thy Sprache: Isabelle

(*  Title:      HOL/Library/Countable_Set.thy
    Author:     Johannes Hölzl
    Author:     Andrei Popescu
*)

section \<open>Countable sets\<close>

theory Countable_Set
imports Countable Infinite_Set
begin

subsection \<open>Predicate for countable sets\<close>

definition countable :: "'a set \ bool" where
  "countable S \ (\f::'a \ nat. inj_on f S)"

lemma countable_as_injective_image_subset: "countable S \ (\f. \K::nat set. S = f ` K \ inj_on f K)"
  by (metis countable_def inj_on_the_inv_into the_inv_into_onto)

lemma countableE:
  assumes S: "countable S" obtains f :: "'a \ nat" where "inj_on f S"
  using S by (auto simp: countable_def)

lemma countableI: "inj_on (f::'a \ nat) S \ countable S"
  by (auto simp: countable_def)

lemma countableI': "inj_on (f::'a \<Rightarrow> 'b::countable) S \<Longrightarrow> countable S"
  using comp_inj_on[of f S to_nat] by (auto intro: countableI)

lemma countableE_bij:
  assumes S: "countable S" obtains f :: "nat \ 'a" and C :: "nat set" where "bij_betw f C S"
  using S by (blast elim: countableE dest: inj_on_imp_bij_betw bij_betw_inv)

lemma countableI_bij: "bij_betw f (C::nat set) S \ countable S"
  by (blast intro: countableI bij_betw_inv_into bij_betw_imp_inj_on)

lemma countable_finite: "finite S \ countable S"
  by (blast dest: finite_imp_inj_to_nat_seg countableI)

lemma countableI_bij1: "bij_betw f A B \ countable A \ countable B"
  by (blast elim: countableE_bij intro: bij_betw_trans countableI_bij)

lemma countableI_bij2: "bij_betw f B A \ countable A \ countable B"
  by (blast elim: countableE_bij intro: bij_betw_trans bij_betw_inv_into countableI_bij)

lemma countable_iff_bij[simp]: "bij_betw f A B \ countable A \ countable B"
  by (blast intro: countableI_bij1 countableI_bij2)

lemma countable_subset: "A \ B \ countable B \ countable A"
  by (auto simp: countable_def intro: inj_on_subset)

lemma countableI_type[intro, simp]: "countable (A:: 'a :: countable set)"
  using countableI[of to_nat A] by auto

subsection \<open>Enumerate a countable set\<close>

lemma countableE_infinite:
  assumes "countable S" "infinite S"
  obtains e :: "'a \ nat" where "bij_betw e S UNIV"
proof -
  obtain f :: "'a \ nat" where "inj_on f S"
    using \<open>countable S\<close> by (rule countableE)
  then have "bij_betw f S (f`S)"
    unfolding bij_betw_def by simp
  moreover
  from \<open>inj_on f S\<close> \<open>infinite S\<close> have inf_fS: "infinite (f`S)"
    by (auto dest: finite_imageD)
  then have "bij_betw (the_inv_into UNIV (enumerate (f`S))) (f`S) UNIV"
    by (intro bij_betw_the_inv_into bij_enumerate)
  ultimately have "bij_betw (the_inv_into UNIV (enumerate (f`S)) \ f) S UNIV"
    by (rule bij_betw_trans)
  then show thesis ..
qed

lemma countable_infiniteE':
  assumes "countable A" "infinite A"
  obtains g where "bij_betw g (UNIV :: nat set) A"
  by (meson assms bij_betw_inv countableE_infinite)

lemma countable_enum_cases:
  assumes "countable S"
  obtains (finite) f :: "'a \ nat" where "finite S" "bij_betw f S {..
        | (infinite) f :: "'a \ nat" where "infinite S" "bij_betw f S UNIV"
  using ex_bij_betw_finite_nat[of S] countableE_infinite \<open>countable S\<close>
  by (cases "finite S") (auto simp add: atLeast0LessThan)

definition to_nat_on :: "'a set \ 'a \ nat" where
  "to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)"

definition from_nat_into :: "'a set \ nat \ 'a" where
  "from_nat_into S n = (if n \ to_nat_on S ` S then inv_into S (to_nat_on S) n else SOME s. s\S)"

lemma to_nat_on_finite: "finite S \ bij_betw (to_nat_on S) S {..< card S}"
  using ex_bij_betw_finite_nat unfolding to_nat_on_def
  by (intro someI2_ex[where Q="\f. bij_betw f S {..

lemma to_nat_on_infinite: "countable S \ infinite S \ bij_betw (to_nat_on S) S UNIV"
  using countableE_infinite unfolding to_nat_on_def
  by (intro someI2_ex[where Q="\f. bij_betw f S UNIV"]) auto

lemma bij_betw_from_nat_into_finite: "finite S \ bij_betw (from_nat_into S) {..< card S} S"
  unfolding from_nat_into_def[abs_def]
  using to_nat_on_finite[of S]
  apply (subst bij_betw_cong)
  apply (split if_split)
  apply (simp add: bij_betw_def)
  apply (auto cong: bij_betw_cong
              intro: bij_betw_inv_into to_nat_on_finite)
  done

lemma bij_betw_from_nat_into: "countable S \ infinite S \ bij_betw (from_nat_into S) UNIV S"
  unfolding from_nat_into_def[abs_def]
  using to_nat_on_infinite[of S, unfolded bij_betw_def]
  by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)

text \<open>
  The sum/product over the enumeration of a finite set equals simply the sum/product over the set
\<close>
context comm_monoid_set
begin

lemma card_from_nat_into:
  "F (\i. h (from_nat_into A i)) {..
proof (cases "finite A")
  case True
  have "F (\i. h (from_nat_into A i)) {..
    by (metis True bij_betw_def bij_betw_from_nat_into_finite reindex_cong)
  also have "... = F h A"
    by (metis True bij_betw_def bij_betw_from_nat_into_finite)
  finally show ?thesis .
qed auto

end

lemma countable_as_injective_image:
  assumes "countable A" "infinite A"
  obtains f :: "nat \ 'a" where "A = range f" "inj f"
by (metis bij_betw_def bij_betw_from_nat_into [OF assms])

lemma inj_on_to_nat_on[intro]: "countable A \ inj_on (to_nat_on A) A"
  using to_nat_on_infinite[of A] to_nat_on_finite[of A]
  by (cases "finite A") (auto simp: bij_betw_def)

lemma to_nat_on_inj[simp]:
  "countable A \ a \ A \ b \ A \ to_nat_on A a = to_nat_on A b \ a = b"
  using inj_on_to_nat_on[of A] by (auto dest: inj_onD)

lemma from_nat_into_to_nat_on[simp]: "countable A \ a \ A \ from_nat_into A (to_nat_on A a) = a"
  by (auto simp: from_nat_into_def intro!: inv_into_f_f)

lemma subset_range_from_nat_into: "countable A \ A \ range (from_nat_into A)"
  by (auto intro: from_nat_into_to_nat_on[symmetric])

lemma from_nat_into: "A \ {} \ from_nat_into A n \ A"
  unfolding from_nat_into_def by (metis equals0I inv_into_into someI_ex)

lemma range_from_nat_into_subset: "A \ {} \ range (from_nat_into A) \ A"
  using from_nat_into[of A] by auto

lemma range_from_nat_into[simp]: "A \ {} \ countable A \ range (from_nat_into A) = A"
  by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into)

lemma image_to_nat_on: "countable A \ infinite A \ to_nat_on A ` A = UNIV"
  using to_nat_on_infinite[of A] by (simp add: bij_betw_def)

lemma to_nat_on_surj: "countable A \ infinite A \ \a\A. to_nat_on A a = n"
  by (metis (no_types) image_iff iso_tuple_UNIV_I image_to_nat_on)

lemma to_nat_on_from_nat_into[simp]: "n \ to_nat_on A ` A \ to_nat_on A (from_nat_into A n) = n"
  by (simp add: f_inv_into_f from_nat_into_def)

lemma to_nat_on_from_nat_into_infinite[simp]:
  "countable A \ infinite A \ to_nat_on A (from_nat_into A n) = n"
  by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into)

lemma from_nat_into_inj:
  "countable A \ m \ to_nat_on A ` A \ n \ to_nat_on A ` A \
    from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
  by (subst to_nat_on_inj[symmetric, of A]) auto

lemma from_nat_into_inj_infinite[simp]:
  "countable A \ infinite A \ from_nat_into A m = from_nat_into A n \ m = n"
  using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp

lemma eq_from_nat_into_iff:
  "countable A \ x \ A \ i \ to_nat_on A ` A \ x = from_nat_into A i \ i = to_nat_on A x"
  by auto

lemma from_nat_into_surj: "countable A \ a \ A \ \n. from_nat_into A n = a"
  by (rule exI[of _ "to_nat_on A a"]) simp

lemma from_nat_into_inject[simp]:
  "A \ {} \ countable A \ B \ {} \ countable B \ from_nat_into A = from_nat_into B \ A = B"
  by (metis range_from_nat_into)

lemma inj_on_from_nat_into: "inj_on from_nat_into ({A. A \ {} \ countable A})"
  unfolding inj_on_def by auto

subsection \<open>Closure properties of countability\<close>

lemma countable_SIGMA[intro, simp]:
  "countable I \ (\i. i \ I \ countable (A i)) \ countable (SIGMA i : I. A i)"
  by (intro countableI'[of "\(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def)

lemma countable_image[intro, simp]:
  assumes "countable A"
  shows "countable (f`A)"
proof -
  obtain g :: "'a \ nat" where "inj_on g A"
    using assms by (rule countableE)
  moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \ A"
    by (auto intro: inj_on_inv_into inv_into_into)
  ultimately show ?thesis
    by (blast dest: comp_inj_on inj_on_subset intro: countableI)
qed

lemma countable_image_inj_on: "countable (f ` A) \ inj_on f A \ countable A"
  by (metis countable_image the_inv_into_onto)

lemma countable_image_inj_Int_vimage:
   "\inj_on f S; countable A\ \ countable (S \ f -` A)"
  by (meson countable_image_inj_on countable_subset image_subset_iff_subset_vimage inf_le2 inj_on_Int)

lemma countable_image_inj_gen:
   "\inj_on f S; countable A\ \ countable {x \ S. f x \ A}"
  using countable_image_inj_Int_vimage
  by (auto simp: vimage_def Collect_conj_eq)

lemma countable_image_inj_eq:
   "inj_on f S \ countable(f ` S) \ countable S"
  using countable_image_inj_on by blast

lemma countable_image_inj:
   "\countable A; inj f\ \ countable {x. f x \ A}"
  by (metis (mono_tags, lifting) countable_image_inj_eq countable_subset image_Collect_subsetI inj_on_inverseI the_inv_f_f)

lemma countable_UN[intro, simp]:
  fixes I :: "'i set" and A :: "'i => 'a set"
  assumes I: "countable I"
  assumes A: "\i. i \ I \ countable (A i)"
  shows "countable (\i\I. A i)"
proof -
  have "(\i\I. A i) = snd ` (SIGMA i : I. A i)" by (auto simp: image_iff)
  then show ?thesis by (simp add: assms)
qed

lemma countable_Un[intro]: "countable A \ countable B \ countable (A \ B)"
  by (rule countable_UN[of "{True, False}" "\True \ A | False \ B", simplified])
     (simp split: bool.split)

lemma countable_Un_iff[simp]: "countable (A \ B) \ countable A \ countable B"
  by (metis countable_Un countable_subset inf_sup_ord(3,4))

lemma countable_Plus[intro, simp]:
  "countable A \ countable B \ countable (A <+> B)"
  by (simp add: Plus_def)

lemma countable_empty[intro, simp]: "countable {}"
  by (blast intro: countable_finite)

lemma countable_insert[intro, simp]: "countable A \ countable (insert a A)"
  using countable_Un[of "{a}" A] by (auto simp: countable_finite)

lemma countable_Int1[intro, simp]: "countable A \ countable (A \ B)"
  by (force intro: countable_subset)

lemma countable_Int2[intro, simp]: "countable B \ countable (A \ B)"
  by (blast intro: countable_subset)

lemma countable_INT[intro, simp]: "i \ I \ countable (A i) \ countable (\i\I. A i)"
  by (blast intro: countable_subset)

lemma countable_Diff[intro, simp]: "countable A \ countable (A - B)"
  by (blast intro: countable_subset)

lemma countable_insert_eq [simp]: "countable (insert x A) = countable A"
    by auto (metis Diff_insert_absorb countable_Diff insert_absorb)

lemma countable_vimage: "B \ range f \ countable (f -` B) \ countable B"
  by (metis Int_absorb2 countable_image image_vimage_eq)

lemma surj_countable_vimage: "surj f \ countable (f -` B) \ countable B"
  by (metis countable_vimage top_greatest)

lemma countable_Collect[simp]: "countable A \ countable {a \ A. \ a}"
  by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1)

lemma countable_Image:
  assumes "\y. y \ Y \ countable (X `` {y})"
  assumes "countable Y"
  shows "countable (X `` Y)"
proof -
  have "countable (X `` (\y\Y. {y}))"
    unfolding Image_UN by (intro countable_UN assms)
  then show ?thesis by simp
qed

lemma countable_relpow:
  fixes X :: "'a rel"
  assumes Image_X: "\Y. countable Y \ countable (X `` Y)"
  assumes Y: "countable Y"
  shows "countable ((X ^^ i) `` Y)"
  using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X)

lemma countable_funpow:
  fixes f :: "'a set \ 'a set"
  assumes "\A. countable A \ countable (f A)"
  and "countable A"
  shows "countable ((f ^^ n) A)"
by(induction n)(simp_all add: assms)

lemma countable_rtrancl:
  "(\Y. countable Y \ countable (X `` Y)) \ countable Y \ countable (X\<^sup>* `` Y)"
  unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow)

lemma countable_lists[intro, simp]:
  assumes A: "countable A" shows "countable (lists A)"
proof -
  have "countable (lists (range (from_nat_into A)))"
    by (auto simp: lists_image)
  with A show ?thesis
    by (auto dest: subset_range_from_nat_into countable_subset lists_mono)
qed

lemma Collect_finite_eq_lists: "Collect finite = set ` lists UNIV"
  using finite_list by auto

lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\bool))"
  by (simp add: Collect_finite_eq_lists)

lemma countable_int: "countable \"
  unfolding Ints_def by auto

lemma countable_rat: "countable \"
  unfolding Rats_def by auto

lemma Collect_finite_subset_eq_lists: "{A. finite A \ A \ T} = set ` lists T"
  using finite_list by (auto simp: lists_eq_set)

lemma countable_Collect_finite_subset:
  "countable T \ countable {A. finite A \ A \ T}"
  unfolding Collect_finite_subset_eq_lists by auto

lemma countable_Fpow: "countable S \ countable (Fpow S)"
  using countable_Collect_finite_subset
  by (force simp add: Fpow_def conj_commute)

lemma countable_set_option [simp]: "countable (set_option x)"
  by (cases x) auto

subsection \<open>Misc lemmas\<close>

lemma countable_subset_image:
   "countable B \ B \ (f ` A) \ (\A'. countable A' \ A' \ A \ (B = f ` A'))"
   (is "?lhs = ?rhs")
proof
  assume ?lhs
  show ?rhs
    by (rule exI [where x="inv_into A f ` B"])
      (use \<open>?lhs\<close> in \<open>auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into\<close>)
next
  assume ?rhs
  then show ?lhs by force
qed

lemma ex_subset_image_inj:
   "(\T. T \ f ` S \ P T) \ (\T. T \ S \ inj_on f T \ P (f ` T))"
  by (auto simp: subset_image_inj)

lemma all_subset_image_inj:
   "(\T. T \ f ` S \ P T) \ (\T. T \ S \ inj_on f T \ P(f ` T))"
  by (metis subset_image_inj)

lemma ex_countable_subset_image_inj:
   "(\T. countable T \ T \ f ` S \ P T) \
    (\<exists>T. countable T \<and> T \<subseteq> S \<and> inj_on f T \<and> P (f ` T))"
  by (metis countable_image_inj_eq subset_image_inj)

lemma all_countable_subset_image_inj:
   "(\T. countable T \ T \ f ` S \ P T) \ (\T. countable T \ T \ S \ inj_on f T \P(f ` T))"
  by (metis countable_image_inj_eq subset_image_inj)

lemma ex_countable_subset_image:
   "(\T. countable T \ T \ f ` S \ P T) \ (\T. countable T \ T \ S \ P (f ` T))"
  by (metis countable_subset_image)

lemma all_countable_subset_image:
   "(\T. countable T \ T \ f ` S \ P T) \ (\T. countable T \ T \ S \ P(f ` T))"
  by (metis countable_subset_image)

lemma countable_image_eq:
   "countable(f ` S) \ (\T. countable T \ T \ S \ f ` S = f ` T)"
  by (metis countable_image countable_image_inj_eq order_refl subset_image_inj)

lemma countable_image_eq_inj:
   "countable(f ` S) \ (\T. countable T \ T \ S \ f ` S = f ` T \ inj_on f T)"
  by (metis countable_image_inj_eq order_refl subset_image_inj)

lemma infinite_countable_subset':
  assumes X: "infinite X" shows "\C\X. countable C \ infinite C"
proof -
  obtain f :: "nat \ 'a" where "inj f" "range f \ X"
    using infinite_countable_subset [OF X] by blast
  then show ?thesis
    by (intro exI[of _ "range f"]) (auto simp: range_inj_infinite)
qed

lemma countable_all:
  assumes S: "countable S"
  shows "(\s\S. P s) \ (\n::nat. from_nat_into S n \ S \ P (from_nat_into S n))"
  using S[THEN subset_range_from_nat_into] by auto

lemma finite_sequence_to_countable_set:
  assumes "countable X"
  obtains F where "\i. F i \ X" "\i. F i \ F (Suc i)" "\i. finite (F i)" "(\i. F i) = X"
proof -
  show thesis
    apply (rule that[of "\i. if X = {} then {} else from_nat_into X ` {..i}"])
       apply (auto simp add: image_iff intro: from_nat_into split: if_splits)
    using assms from_nat_into_surj by (fastforce cong: image_cong)
qed

lemma transfer_countable[transfer_rule]:
  "bi_unique R \ rel_fun (rel_set R) (=) countable countable"
  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma)
     (auto dest: countable_image_inj_on)

subsection \<open>Uncountable\<close>

abbreviation uncountable where
  "uncountable A \ \ countable A"

lemma uncountable_def: "uncountable A \ A \ {} \ \ (\f::(nat \ 'a). range f = A)"
  by (auto intro: inj_on_inv_into simp: countable_def)
     (metis all_not_in_conv inj_on_iff_surj subset_UNIV)

lemma uncountable_bij_betw: "bij_betw f A B \ uncountable B \ uncountable A"
  unfolding bij_betw_def by (metis countable_image)

lemma uncountable_infinite: "uncountable A \ infinite A"
  by (metis countable_finite)

lemma uncountable_minus_countable:
  "uncountable A \ countable B \ uncountable (A - B)"
  using countable_Un[of B "A - B"] by auto

lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A"
  by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable)

text \<open>Every infinite set can be covered by a pairwise disjoint family of infinite sets.
      This version doesn't achieve equality, as it only covers a countable subset\
lemma infinite_infinite_partition:
  assumes "infinite A"
  obtains C :: "nat \ 'a set"
    where "pairwise (\i j. disjnt (C i) (C j)) UNIV" "(\i. C i) \ A" "\i. infinite (C i)"
proof -
  obtain f :: "nat\'a" where "range f \ A" "inj f"
    using assms infinite_countable_subset by blast
  let ?C = "\i. range (\j. f (prod_encode (i,j)))"
  show thesis
  proof
    show "pairwise (\i j. disjnt (?C i) (?C j)) UNIV"
      by (auto simp: pairwise_def disjnt_def inj_on_eq_iff [OF \<open>inj f\<close>] inj_on_eq_iff [OF inj_prod_encode, of _ UNIV])
    show "(\i. ?C i) \ A"
      using \<open>range f \<subseteq> A\<close> by blast
    have "infinite (range (\j. f (prod_encode (i, j))))" for i
      by (rule range_inj_infinite) (meson Pair_inject \<open>inj f\<close> inj_def prod_encode_eq)
    then show "\i. infinite (?C i)"
      using that by auto
  qed
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.15 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 ist noch experimentell.