src/HOL/Library/Countable_Set.thy

--- a/src/HOL/Library/Countable_Set.thy	Wed Nov 21 10:51:12 2012 +0100
+++ b/src/HOL/Library/Countable_Set.thy	Wed Nov 21 12:05:05 2012 +0100
@@ -79,7 +79,7 @@
   "to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)"
 
 definition from_nat_into :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
-  "from_nat_into S = inv_into S (to_nat_on S)"
+  "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)"
 
 lemma to_nat_on_finite: "finite S \<Longrightarrow> bij_betw (to_nat_on S) S {..< card S}"
   using ex_bij_betw_finite_nat unfolding to_nat_on_def
@@ -90,10 +90,19 @@
   by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto
 
 lemma from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
-  by (auto simp add: from_nat_into_def intro: bij_betw_inv_into to_nat_on_finite)
+  unfolding from_nat_into_def[abs_def]
+  using to_nat_on_finite[of S]
+  apply (subst bij_betw_cong)
+  apply (split split_if)
+  apply (simp add: bij_betw_def)
+  apply (auto cong: bij_betw_cong
+              intro: bij_betw_inv_into to_nat_on_finite)
+  done
 
 lemma from_nat_into_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
-  by (auto simp add: from_nat_into_def intro: bij_betw_inv_into to_nat_on_infinite)
+  unfolding from_nat_into_def[abs_def]
+  using to_nat_on_infinite[of S, unfolded bij_betw_def]
+  by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)
 
 lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A"
   using to_nat_on_infinite[of A] to_nat_on_finite[of A]
@@ -103,12 +112,57 @@
   "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> to_nat_on A a = to_nat_on A b \<longleftrightarrow> a = b"
   using inj_on_to_nat_on[of A] by (auto dest: inj_onD)
 
-lemma from_nat_into_to_nat_on: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> from_nat_into A (to_nat_on A a) = a"
+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"
   by (auto simp: from_nat_into_def intro!: inv_into_f_f)
 
 lemma subset_range_from_nat_into: "countable A \<Longrightarrow> A \<subseteq> range (from_nat_into A)"
   by (auto intro: from_nat_into_to_nat_on[symmetric])
 
+lemma from_nat_into: "A \<noteq> {} \<Longrightarrow> from_nat_into A n \<in> A"
+  unfolding from_nat_into_def by (metis equals0I inv_into_into someI_ex)
+
+lemma range_from_nat_into_subset: "A \<noteq> {} \<Longrightarrow> range (from_nat_into A) \<subseteq> A"
+  using from_nat_into[of A] by auto
+
+lemma from_nat_into_image[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> from_nat_into A ` UNIV = A"
+  by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into)
+
+lemma image_to_nat_on: "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A ` A = UNIV"
+  using to_nat_on_infinite[of A] by (simp add: bij_betw_def)
+
+lemma to_nat_on_surj: "countable A \<Longrightarrow> infinite A \<Longrightarrow> \<exists>a\<in>A. to_nat_on A a = n"
+  by (metis (no_types) image_iff iso_tuple_UNIV_I image_to_nat_on)
+
+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"
+  by (simp add: f_inv_into_f from_nat_into_def)
+
+lemma infinite_to_nat_on_from_nat_into[simp]:
+  "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n"
+  by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into)
+
+lemma from_nat_into_inj:
+  assumes c: "countable A" and i: "infinite A"
+  shows "from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n" (is "?L = ?R \<longleftrightarrow> ?K")
+proof-
+  have "?L = ?R \<longleftrightarrow> to_nat_on A ?L = to_nat_on A ?R"
+  unfolding to_nat_on_inj[OF c from_nat_into[OF infinite_imp_nonempty[OF i]]
+                               from_nat_into[OF infinite_imp_nonempty[OF i]]] ..
+  also have "... \<longleftrightarrow> ?K" using c i by simp
+  finally show ?thesis .
+qed
+
+lemma from_nat_into_surj: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>n. from_nat_into A n = a"
+  by (rule exI[of _ "to_nat_on A a"]) simp
+
+lemma from_nat_into_inject[simp]:
+assumes A: "A \<noteq> {}" "countable A" and B: "B \<noteq> {}" "countable B"
+shows "from_nat_into A = from_nat_into B \<longleftrightarrow> A = B"
+by (metis assms from_nat_into_image)
+
+lemma inj_on_from_nat_into:
+"inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})"
+unfolding inj_on_def by auto
+
 subsection {* Closure properties of countability *}
 
 lemma countable_SIGMA[intro, simp]:
@@ -169,6 +223,9 @@
 lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
   by (metis countable_vimage top_greatest)
 
+lemma countable_Collect[simp]: "countable A \<Longrightarrow> countable {a \<in> A. \<phi> a}"
+  by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1)
+
 lemma countable_lists[intro, simp]:
   assumes A: "countable A" shows "countable (lists A)"
 proof -