Countable_Set: tuned lemma names; more generic lemmas
authorhoelzl
Wed Nov 21 15:47:55 2012 +0100 (2012-11-21)
changeset 50148b8cff6a8fda2
parent 50147 8d2251b9a200
child 50150 2e0287c6bb61
Countable_Set: tuned lemma names; more generic lemmas
src/HOL/Library/Countable_Set.thy
     1.1 --- a/src/HOL/Library/Countable_Set.thy	Wed Nov 21 14:07:35 2012 +0100
     1.2 +++ b/src/HOL/Library/Countable_Set.thy	Wed Nov 21 15:47:55 2012 +0100
     1.3 @@ -89,7 +89,7 @@
     1.4    using countableE_infinite unfolding to_nat_on_def
     1.5    by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto
     1.6  
     1.7 -lemma from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
     1.8 +lemma bij_betw_from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
     1.9    unfolding from_nat_into_def[abs_def]
    1.10    using to_nat_on_finite[of S]
    1.11    apply (subst bij_betw_cong)
    1.12 @@ -99,7 +99,7 @@
    1.13                intro: bij_betw_inv_into to_nat_on_finite)
    1.14    done
    1.15  
    1.16 -lemma from_nat_into_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
    1.17 +lemma bij_betw_from_nat_into: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
    1.18    unfolding from_nat_into_def[abs_def]
    1.19    using to_nat_on_infinite[of S, unfolded bij_betw_def]
    1.20    by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)
    1.21 @@ -124,7 +124,7 @@
    1.22  lemma range_from_nat_into_subset: "A \<noteq> {} \<Longrightarrow> range (from_nat_into A) \<subseteq> A"
    1.23    using from_nat_into[of A] by auto
    1.24  
    1.25 -lemma from_nat_into_image[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> from_nat_into A ` UNIV = A"
    1.26 +lemma range_from_nat_into[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> range (from_nat_into A) = A"
    1.27    by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into)
    1.28  
    1.29  lemma image_to_nat_on: "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A ` A = UNIV"
    1.30 @@ -136,32 +136,32 @@
    1.31  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.32    by (simp add: f_inv_into_f from_nat_into_def)
    1.33  
    1.34 -lemma infinite_to_nat_on_from_nat_into[simp]:
    1.35 +lemma to_nat_on_from_nat_into_infinite[simp]:
    1.36    "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n"
    1.37    by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into)
    1.38  
    1.39  lemma from_nat_into_inj:
    1.40 -  assumes c: "countable A" and i: "infinite A"
    1.41 -  shows "from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n" (is "?L = ?R \<longleftrightarrow> ?K")
    1.42 -proof-
    1.43 -  have "?L = ?R \<longleftrightarrow> to_nat_on A ?L = to_nat_on A ?R"
    1.44 -  unfolding to_nat_on_inj[OF c from_nat_into[OF infinite_imp_nonempty[OF i]]
    1.45 -                               from_nat_into[OF infinite_imp_nonempty[OF i]]] ..
    1.46 -  also have "... \<longleftrightarrow> ?K" using c i by simp
    1.47 -  finally show ?thesis .
    1.48 -qed
    1.49 +  "countable A \<Longrightarrow> m \<in> to_nat_on A ` A \<Longrightarrow> n \<in> to_nat_on A ` A \<Longrightarrow>
    1.50 +    from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
    1.51 +  by (subst to_nat_on_inj[symmetric, of A]) auto
    1.52 +
    1.53 +lemma from_nat_into_inj_infinite[simp]:
    1.54 +  "countable A \<Longrightarrow> infinite A \<Longrightarrow> from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
    1.55 +  using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp
    1.56 +
    1.57 +lemma eq_from_nat_into_iff:
    1.58 +  "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"
    1.59 +  by auto
    1.60  
    1.61  lemma from_nat_into_surj: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>n. from_nat_into A n = a"
    1.62    by (rule exI[of _ "to_nat_on A a"]) simp
    1.63  
    1.64  lemma from_nat_into_inject[simp]:
    1.65 -assumes A: "A \<noteq> {}" "countable A" and B: "B \<noteq> {}" "countable B"
    1.66 -shows "from_nat_into A = from_nat_into B \<longleftrightarrow> A = B"
    1.67 -by (metis assms from_nat_into_image)
    1.68 +  "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> countable B \<Longrightarrow> from_nat_into A = from_nat_into B \<longleftrightarrow> A = B"
    1.69 +  by (metis range_from_nat_into)
    1.70  
    1.71 -lemma inj_on_from_nat_into:
    1.72 -"inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})"
    1.73 -unfolding inj_on_def by auto
    1.74 +lemma inj_on_from_nat_into: "inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})"
    1.75 +  unfolding inj_on_def by auto
    1.76  
    1.77  subsection {* Closure properties of countability *}
    1.78