src/HOL/Library/Countable_Set.thy

 
 lemma to_nat_on_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (to_nat_on S) S UNIV"
   using countableE_infinite unfolding to_nat_on_def
   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"
+lemma bij_betw_from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
   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"
+lemma bij_betw_from_nat_into: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
   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"

   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"
+lemma range_from_nat_into[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> range (from_nat_into A) = 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)
 

   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]:
+lemma to_nat_on_from_nat_into_infinite[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
+  "countable A \<Longrightarrow> m \<in> to_nat_on A ` A \<Longrightarrow> n \<in> to_nat_on A ` A \<Longrightarrow>
+    from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
+  by (subst to_nat_on_inj[symmetric, of A]) auto
+
+lemma from_nat_into_inj_infinite[simp]:
+  "countable A \<Longrightarrow> infinite A \<Longrightarrow> from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
+  using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp
+
+lemma eq_from_nat_into_iff:
+  "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> i \<in> to_nat_on A ` A \<Longrightarrow> x = from_nat_into A i \<longleftrightarrow> i = to_nat_on A x"
+  by auto
 
 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
+  "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> countable B \<Longrightarrow> from_nat_into A = from_nat_into B \<longleftrightarrow> A = B"
+  by (metis range_from_nat_into)
+
+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]:
   "countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)"