src/HOL/Library/Countable_Set.thy
changeset 57025 e7fd64f82876
parent 54410 0a578fb7fb73
child 57234 596a499318ab
     1.1 --- a/src/HOL/Library/Countable_Set.thy	Tue May 20 16:52:59 2014 +0200
     1.2 +++ b/src/HOL/Library/Countable_Set.thy	Tue May 20 19:24:39 2014 +0200
     1.3 @@ -283,4 +283,17 @@
     1.4    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))"
     1.5    using S[THEN subset_range_from_nat_into] by auto
     1.6  
     1.7 +lemma finite_sequence_to_countable_set:
     1.8 +   assumes "countable X" obtains F where "\<And>i. F i \<subseteq> X" "\<And>i. F i \<subseteq> F (Suc i)" "\<And>i. finite (F i)" "(\<Union>i. F i) = X"
     1.9 +proof -  show thesis
    1.10 +    apply (rule that[of "\<lambda>i. if X = {} then {} else from_nat_into X ` {..i}"])
    1.11 +    apply (auto simp: image_iff Ball_def intro: from_nat_into split: split_if_asm)
    1.12 +  proof -
    1.13 +    fix x n assume "x \<in> X" "\<forall>i m. m \<le> i \<longrightarrow> x \<noteq> from_nat_into X m"
    1.14 +    with from_nat_into_surj[OF `countable X` `x \<in> X`]
    1.15 +    show False
    1.16 +      by auto
    1.17 +  qed
    1.18 +qed
    1.19 +
    1.20  end