src/HOL/Library/Countable_Set.thy
changeset 50144 885deccc264e
parent 50134 13211e07d931
child 50148 b8cff6a8fda2
     1.1 --- a/src/HOL/Library/Countable_Set.thy	Wed Nov 21 10:51:12 2012 +0100
     1.2 +++ b/src/HOL/Library/Countable_Set.thy	Wed Nov 21 12:05:05 2012 +0100
     1.3 @@ -79,7 +79,7 @@
     1.4    "to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)"
     1.5  
     1.6  definition from_nat_into :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
     1.7 -  "from_nat_into S = inv_into S (to_nat_on S)"
     1.8 +  "from_nat_into S n = (if n \<in> to_nat_on S ` S then inv_into S (to_nat_on S) n else SOME s. s\<in>S)"
     1.9  
    1.10  lemma to_nat_on_finite: "finite S \<Longrightarrow> bij_betw (to_nat_on S) S {..< card S}"
    1.11    using ex_bij_betw_finite_nat unfolding to_nat_on_def
    1.12 @@ -90,10 +90,19 @@
    1.13    by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto
    1.14  
    1.15  lemma from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
    1.16 -  by (auto simp add: from_nat_into_def intro: bij_betw_inv_into to_nat_on_finite)
    1.17 +  unfolding from_nat_into_def[abs_def]
    1.18 +  using to_nat_on_finite[of S]
    1.19 +  apply (subst bij_betw_cong)
    1.20 +  apply (split split_if)
    1.21 +  apply (simp add: bij_betw_def)
    1.22 +  apply (auto cong: bij_betw_cong
    1.23 +              intro: bij_betw_inv_into to_nat_on_finite)
    1.24 +  done
    1.25  
    1.26  lemma from_nat_into_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
    1.27 -  by (auto simp add: from_nat_into_def intro: bij_betw_inv_into to_nat_on_infinite)
    1.28 +  unfolding from_nat_into_def[abs_def]
    1.29 +  using to_nat_on_infinite[of S, unfolded bij_betw_def]
    1.30 +  by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)
    1.31  
    1.32  lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A"
    1.33    using to_nat_on_infinite[of A] to_nat_on_finite[of A]
    1.34 @@ -103,12 +112,57 @@
    1.35    "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> to_nat_on A a = to_nat_on A b \<longleftrightarrow> a = b"
    1.36    using inj_on_to_nat_on[of A] by (auto dest: inj_onD)
    1.37  
    1.38 -lemma from_nat_into_to_nat_on: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> from_nat_into A (to_nat_on A a) = a"
    1.39 +lemma from_nat_into_to_nat_on[simp]: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> from_nat_into A (to_nat_on A a) = a"
    1.40    by (auto simp: from_nat_into_def intro!: inv_into_f_f)
    1.41  
    1.42  lemma subset_range_from_nat_into: "countable A \<Longrightarrow> A \<subseteq> range (from_nat_into A)"
    1.43    by (auto intro: from_nat_into_to_nat_on[symmetric])
    1.44  
    1.45 +lemma from_nat_into: "A \<noteq> {} \<Longrightarrow> from_nat_into A n \<in> A"
    1.46 +  unfolding from_nat_into_def by (metis equals0I inv_into_into someI_ex)
    1.47 +
    1.48 +lemma range_from_nat_into_subset: "A \<noteq> {} \<Longrightarrow> range (from_nat_into A) \<subseteq> A"
    1.49 +  using from_nat_into[of A] by auto
    1.50 +
    1.51 +lemma from_nat_into_image[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> from_nat_into A ` UNIV = A"
    1.52 +  by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into)
    1.53 +
    1.54 +lemma image_to_nat_on: "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A ` A = UNIV"
    1.55 +  using to_nat_on_infinite[of A] by (simp add: bij_betw_def)
    1.56 +
    1.57 +lemma to_nat_on_surj: "countable A \<Longrightarrow> infinite A \<Longrightarrow> \<exists>a\<in>A. to_nat_on A a = n"
    1.58 +  by (metis (no_types) image_iff iso_tuple_UNIV_I image_to_nat_on)
    1.59 +
    1.60 +lemma to_nat_on_from_nat_into[simp]: "n \<in> to_nat_on A ` A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n"
    1.61 +  by (simp add: f_inv_into_f from_nat_into_def)
    1.62 +
    1.63 +lemma infinite_to_nat_on_from_nat_into[simp]:
    1.64 +  "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n"
    1.65 +  by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into)
    1.66 +
    1.67 +lemma from_nat_into_inj:
    1.68 +  assumes c: "countable A" and i: "infinite A"
    1.69 +  shows "from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n" (is "?L = ?R \<longleftrightarrow> ?K")
    1.70 +proof-
    1.71 +  have "?L = ?R \<longleftrightarrow> to_nat_on A ?L = to_nat_on A ?R"
    1.72 +  unfolding to_nat_on_inj[OF c from_nat_into[OF infinite_imp_nonempty[OF i]]
    1.73 +                               from_nat_into[OF infinite_imp_nonempty[OF i]]] ..
    1.74 +  also have "... \<longleftrightarrow> ?K" using c i by simp
    1.75 +  finally show ?thesis .
    1.76 +qed
    1.77 +
    1.78 +lemma from_nat_into_surj: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>n. from_nat_into A n = a"
    1.79 +  by (rule exI[of _ "to_nat_on A a"]) simp
    1.80 +
    1.81 +lemma from_nat_into_inject[simp]:
    1.82 +assumes A: "A \<noteq> {}" "countable A" and B: "B \<noteq> {}" "countable B"
    1.83 +shows "from_nat_into A = from_nat_into B \<longleftrightarrow> A = B"
    1.84 +by (metis assms from_nat_into_image)
    1.85 +
    1.86 +lemma inj_on_from_nat_into:
    1.87 +"inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})"
    1.88 +unfolding inj_on_def by auto
    1.89 +
    1.90  subsection {* Closure properties of countability *}
    1.91  
    1.92  lemma countable_SIGMA[intro, simp]:
    1.93 @@ -169,6 +223,9 @@
    1.94  lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
    1.95    by (metis countable_vimage top_greatest)
    1.96  
    1.97 +lemma countable_Collect[simp]: "countable A \<Longrightarrow> countable {a \<in> A. \<phi> a}"
    1.98 +  by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1)
    1.99 +
   1.100  lemma countable_lists[intro, simp]:
   1.101    assumes A: "countable A" shows "countable (lists A)"
   1.102  proof -