src/HOL/Hilbert_Choice.thy
changeset 54578 9387251b6a46
parent 54295 45a5523d4a63
child 54744 1e7f2d296e19
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Nov 25 08:22:29 2013 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Nov 25 10:14:29 2013 +0100
     1.3 @@ -272,6 +272,41 @@
     1.4    ultimately show "finite (UNIV :: 'a set)" by simp
     1.5  qed
     1.6  
     1.7 +text {*
     1.8 +  Every infinite set contains a countable subset. More precisely we
     1.9 +  show that a set @{text S} is infinite if and only if there exists an
    1.10 +  injective function from the naturals into @{text S}.
    1.11 +
    1.12 +  The ``only if'' direction is harder because it requires the
    1.13 +  construction of a sequence of pairwise different elements of an
    1.14 +  infinite set @{text S}. The idea is to construct a sequence of
    1.15 +  non-empty and infinite subsets of @{text S} obtained by successively
    1.16 +  removing elements of @{text S}.
    1.17 +*}
    1.18 +
    1.19 +lemma infinite_countable_subset:
    1.20 +  assumes inf: "\<not> finite (S::'a set)"
    1.21 +  shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
    1.22 +  -- {* Courtesy of Stephan Merz *}
    1.23 +proof -
    1.24 +  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
    1.25 +  def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
    1.26 +  { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
    1.27 +  moreover then have *: "\<And>n. pick n \<in> Sseq n" by (metis someI_ex pick_def ex_in_conv finite.simps)
    1.28 +  ultimately have "range pick \<subseteq> S" by auto
    1.29 +  moreover
    1.30 +  { fix n m                 
    1.31 +    have "pick n \<notin> Sseq (n + Suc m)" by (induct m) (auto simp add: Sseq_def pick_def)
    1.32 +    hence "pick n \<noteq> pick (n + Suc m)" by (metis *)
    1.33 +  }
    1.34 +  then have "inj pick" by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
    1.35 +  ultimately show ?thesis by blast
    1.36 +qed
    1.37 +
    1.38 +lemma infinite_iff_countable_subset: "\<not> finite S \<longleftrightarrow> (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
    1.39 +  -- {* Courtesy of Stephan Merz *}
    1.40 +  by (metis finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset)
    1.41 +
    1.42  lemma image_inv_into_cancel:
    1.43    assumes SURJ: "f`A=A'" and SUB: "B' \<le> A'"
    1.44    shows "f `((inv_into A f)`B') = B'"