# HG changeset patch
# User hoelzl
# Date 1353509275 -3600
# Node ID b8cff6a8fda21ec2d739a746185208796b734941
# Parent  8d2251b9a2003bcf7ad19cb3b5439247ba478382
Countable_Set: tuned lemma names; more generic lemmas

diff -r 8d2251b9a200 -r b8cff6a8fda2 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Wed Nov 21 14:07:35 2012 +0100
+++ b/src/HOL/Library/Countable_Set.thy	Wed Nov 21 15:47:55 2012 +0100
@@ -89,7 +89,7 @@
   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)
@@ -99,7 +99,7 @@
               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)
@@ -124,7 +124,7 @@
 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"
@@ -136,32 +136,32 @@
 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)
+  "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
+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 *}