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'"
```