src/HOL/Library/Countable_Set.thy
author hoelzl
Tue Nov 20 18:59:35 2012 +0100 (2012-11-20)
changeset 50134 13211e07d931
child 50144 885deccc264e
permissions -rw-r--r--
add Countable_Set theory
     1 (*  Title:      HOL/Library/Countable_Set.thy
     2     Author:     Johannes Hölzl
     3     Author:     Andrei Popescu
     4 *)
     5 
     6 header {* Countable sets *}
     7 
     8 theory Countable_Set
     9   imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/Infinite_Set"
    10 begin
    11 
    12 subsection {* Predicate for countable sets *}
    13 
    14 definition countable :: "'a set \<Rightarrow> bool" where
    15   "countable S \<longleftrightarrow> (\<exists>f::'a \<Rightarrow> nat. inj_on f S)"
    16 
    17 lemma countableE:
    18   assumes S: "countable S" obtains f :: "'a \<Rightarrow> nat" where "inj_on f S"
    19   using S by (auto simp: countable_def)
    20 
    21 lemma countableI: "inj_on (f::'a \<Rightarrow> nat) S \<Longrightarrow> countable S"
    22   by (auto simp: countable_def)
    23 
    24 lemma countableI': "inj_on (f::'a \<Rightarrow> 'b::countable) S \<Longrightarrow> countable S"
    25   using comp_inj_on[of f S to_nat] by (auto intro: countableI)
    26 
    27 lemma countableE_bij:
    28   assumes S: "countable S" obtains f :: "nat \<Rightarrow> 'a" and C :: "nat set" where "bij_betw f C S"
    29   using S by (blast elim: countableE dest: inj_on_imp_bij_betw bij_betw_inv)
    30 
    31 lemma countableI_bij: "bij_betw f (C::nat set) S \<Longrightarrow> countable S"
    32   by (blast intro: countableI bij_betw_inv_into bij_betw_imp_inj_on)
    33 
    34 lemma countable_finite: "finite S \<Longrightarrow> countable S"
    35   by (blast dest: finite_imp_inj_to_nat_seg countableI)
    36 
    37 lemma countableI_bij1: "bij_betw f A B \<Longrightarrow> countable A \<Longrightarrow> countable B"
    38   by (blast elim: countableE_bij intro: bij_betw_trans countableI_bij)
    39 
    40 lemma countableI_bij2: "bij_betw f B A \<Longrightarrow> countable A \<Longrightarrow> countable B"
    41   by (blast elim: countableE_bij intro: bij_betw_trans bij_betw_inv_into countableI_bij)
    42 
    43 lemma countable_iff_bij[simp]: "bij_betw f A B \<Longrightarrow> countable A \<longleftrightarrow> countable B"
    44   by (blast intro: countableI_bij1 countableI_bij2)
    45 
    46 lemma countable_subset: "A \<subseteq> B \<Longrightarrow> countable B \<Longrightarrow> countable A"
    47   by (auto simp: countable_def intro: subset_inj_on)
    48 
    49 lemma countableI_type[intro, simp]: "countable (A:: 'a :: countable set)"
    50   using countableI[of to_nat A] by auto
    51 
    52 subsection {* Enumerate a countable set *}
    53 
    54 lemma countableE_infinite:
    55   assumes "countable S" "infinite S"
    56   obtains e :: "'a \<Rightarrow> nat" where "bij_betw e S UNIV"
    57 proof -
    58   from `countable S`[THEN countableE] guess f .
    59   then have "bij_betw f S (f`S)"
    60     unfolding bij_betw_def by simp
    61   moreover
    62   from `inj_on f S` `infinite S` have inf_fS: "infinite (f`S)"
    63     by (auto dest: finite_imageD)
    64   then have "bij_betw (the_inv_into UNIV (enumerate (f`S))) (f`S) UNIV"
    65     by (intro bij_betw_the_inv_into bij_enumerate)
    66   ultimately have "bij_betw (the_inv_into UNIV (enumerate (f`S)) \<circ> f) S UNIV"
    67     by (rule bij_betw_trans)
    68   then show thesis ..
    69 qed
    70 
    71 lemma countable_enum_cases:
    72   assumes "countable S"
    73   obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}"
    74         | (infinite) f :: "'a \<Rightarrow> nat" where "infinite S" "bij_betw f S UNIV"
    75   using ex_bij_betw_finite_nat[of S] countableE_infinite `countable S`
    76   by (cases "finite S") (auto simp add: atLeast0LessThan)
    77 
    78 definition to_nat_on :: "'a set \<Rightarrow> 'a \<Rightarrow> nat" where
    79   "to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)"
    80 
    81 definition from_nat_into :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
    82   "from_nat_into S = inv_into S (to_nat_on S)"
    83 
    84 lemma to_nat_on_finite: "finite S \<Longrightarrow> bij_betw (to_nat_on S) S {..< card S}"
    85   using ex_bij_betw_finite_nat unfolding to_nat_on_def
    86   by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S {..<card S}"]) (auto simp add: atLeast0LessThan)
    87 
    88 lemma to_nat_on_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (to_nat_on S) S UNIV"
    89   using countableE_infinite unfolding to_nat_on_def
    90   by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto
    91 
    92 lemma from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
    93   by (auto simp add: from_nat_into_def intro: bij_betw_inv_into to_nat_on_finite)
    94 
    95 lemma from_nat_into_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
    96   by (auto simp add: from_nat_into_def intro: bij_betw_inv_into to_nat_on_infinite)
    97 
    98 lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A"
    99   using to_nat_on_infinite[of A] to_nat_on_finite[of A]
   100   by (cases "finite A") (auto simp: bij_betw_def)
   101 
   102 lemma to_nat_on_inj[simp]:
   103   "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> to_nat_on A a = to_nat_on A b \<longleftrightarrow> a = b"
   104   using inj_on_to_nat_on[of A] by (auto dest: inj_onD)
   105 
   106 lemma from_nat_into_to_nat_on: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> from_nat_into A (to_nat_on A a) = a"
   107   by (auto simp: from_nat_into_def intro!: inv_into_f_f)
   108 
   109 lemma subset_range_from_nat_into: "countable A \<Longrightarrow> A \<subseteq> range (from_nat_into A)"
   110   by (auto intro: from_nat_into_to_nat_on[symmetric])
   111 
   112 subsection {* Closure properties of countability *}
   113 
   114 lemma countable_SIGMA[intro, simp]:
   115   "countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)"
   116   by (intro countableI'[of "\<lambda>(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def)
   117 
   118 lemma countable_image[intro, simp]: assumes A: "countable A" shows "countable (f`A)"
   119 proof -
   120   from A guess g by (rule countableE)
   121   moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A"
   122     by (auto intro: inj_on_inv_into inv_into_into)
   123   ultimately show ?thesis
   124     by (blast dest: comp_inj_on subset_inj_on intro: countableI)
   125 qed
   126 
   127 lemma countable_UN[intro, simp]:
   128   fixes I :: "'i set" and A :: "'i => 'a set"
   129   assumes I: "countable I"
   130   assumes A: "\<And>i. i \<in> I \<Longrightarrow> countable (A i)"
   131   shows "countable (\<Union>i\<in>I. A i)"
   132 proof -
   133   have "(\<Union>i\<in>I. A i) = snd ` (SIGMA i : I. A i)" by (auto simp: image_iff)
   134   then show ?thesis by (simp add: assms)
   135 qed
   136 
   137 lemma countable_Un[intro]: "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A \<union> B)"
   138   by (rule countable_UN[of "{True, False}" "\<lambda>True \<Rightarrow> A | False \<Rightarrow> B", simplified])
   139      (simp split: bool.split)
   140 
   141 lemma countable_Un_iff[simp]: "countable (A \<union> B) \<longleftrightarrow> countable A \<and> countable B"
   142   by (metis countable_Un countable_subset inf_sup_ord(3,4))
   143 
   144 lemma countable_Plus[intro, simp]:
   145   "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A <+> B)"
   146   by (simp add: Plus_def)
   147 
   148 lemma countable_empty[intro, simp]: "countable {}"
   149   by (blast intro: countable_finite)
   150 
   151 lemma countable_insert[intro, simp]: "countable A \<Longrightarrow> countable (insert a A)"
   152   using countable_Un[of "{a}" A] by (auto simp: countable_finite)
   153 
   154 lemma countable_Int1[intro, simp]: "countable A \<Longrightarrow> countable (A \<inter> B)"
   155   by (force intro: countable_subset)
   156 
   157 lemma countable_Int2[intro, simp]: "countable B \<Longrightarrow> countable (A \<inter> B)"
   158   by (blast intro: countable_subset)
   159 
   160 lemma countable_INT[intro, simp]: "i \<in> I \<Longrightarrow> countable (A i) \<Longrightarrow> countable (\<Inter>i\<in>I. A i)"
   161   by (blast intro: countable_subset)
   162 
   163 lemma countable_Diff[intro, simp]: "countable A \<Longrightarrow> countable (A - B)"
   164   by (blast intro: countable_subset)
   165 
   166 lemma countable_vimage: "B \<subseteq> range f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
   167   by (metis Int_absorb2 assms countable_image image_vimage_eq)
   168 
   169 lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
   170   by (metis countable_vimage top_greatest)
   171 
   172 lemma countable_lists[intro, simp]:
   173   assumes A: "countable A" shows "countable (lists A)"
   174 proof -
   175   have "countable (lists (range (from_nat_into A)))"
   176     by (auto simp: lists_image)
   177   with A show ?thesis
   178     by (auto dest: subset_range_from_nat_into countable_subset lists_mono)
   179 qed
   180 
   181 subsection {* Misc lemmas *}
   182 
   183 lemma countable_all:
   184   assumes S: "countable S"
   185   shows "(\<forall>s\<in>S. P s) \<longleftrightarrow> (\<forall>n::nat. from_nat_into S n \<in> S \<longrightarrow> P (from_nat_into S n))"
   186   using S[THEN subset_range_from_nat_into] by auto
   187 
   188 end