# HG changeset patch
# User hoelzl
# Date 1353495905 -3600
# Node ID 885deccc264e0093cd1b19e49a766f5756f97116
# Parent  4ff5d795ed0841b6ef052436c1c049feeecbce50
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set

diff -r 4ff5d795ed08 -r 885deccc264e src/HOL/BNF/Countable_Set.thy
--- a/src/HOL/BNF/Countable_Set.thy	Wed Nov 21 10:51:12 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,366 +0,0 @@
-(*  Title:      HOL/BNF/Countable_Set.thy
-    Author:     Andrei Popescu, TU Muenchen
-    Copyright   2012
-
-(At most) countable sets.
-*)
-
-header {* (At Most) Countable Sets *}
-
-theory Countable_Set
-imports "../Cardinals/Cardinals" "~~/src/HOL/Library/Countable"
-begin
-
-
-subsection{* Basics  *}
-
-definition "countable A \<equiv> |A| \<le>o natLeq"
-
-lemma countable_card_of_nat:
-"countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|"
-unfolding countable_def using card_of_nat
-using ordLeq_ordIso_trans ordIso_symmetric by blast
-
-lemma countable_ex_to_nat:
-fixes A :: "'a set"
-shows "countable A \<longleftrightarrow> (\<exists> f::'a\<Rightarrow>nat. inj_on f A)"
-unfolding countable_card_of_nat card_of_ordLeq[symmetric] by auto
-
-lemma countable_or_card_of:
-assumes "countable A"
-shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
-       (infinite A  \<and> |A| =o |UNIV::nat set| )"
-apply (cases "finite A")
-  apply(metis finite_iff_cardOf_nat)
-  by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq)
-
-lemma countable_or:
-assumes "countable A"
-shows "(\<exists> f::'a\<Rightarrow>nat. finite A \<and> inj_on f A) \<or>
-       (\<exists> f::'a\<Rightarrow>nat. infinite A \<and> bij_betw f A UNIV)"
-using countable_or_card_of[OF assms]
-by (metis assms card_of_ordIso countable_ex_to_nat)
-
-lemma countable_cases_card_of[elim, consumes 1, case_names Fin Inf]:
-assumes "countable A"
-and "\<lbrakk>finite A; |A| <o |UNIV::nat set|\<rbrakk> \<Longrightarrow> phi"
-and "\<lbrakk>infinite A; |A| =o |UNIV::nat set|\<rbrakk> \<Longrightarrow> phi"
-shows phi
-using assms countable_or_card_of by blast
-
-lemma countable_cases[elim, consumes 1, case_names Fin Inf]:
-assumes "countable A"
-and "\<And> f::'a\<Rightarrow>nat. \<lbrakk>finite A; inj_on f A\<rbrakk> \<Longrightarrow> phi"
-and "\<And> f::'a\<Rightarrow>nat. \<lbrakk>infinite A; bij_betw f A UNIV\<rbrakk> \<Longrightarrow> phi"
-shows phi
-using assms countable_or by metis
-
-definition toNat_pred :: "'a set \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"
-where
-"toNat_pred (A::'a set) f \<equiv>
- (finite A \<and> inj_on f A) \<or> (infinite A \<and> bij_betw f A UNIV)"
-definition toNat where "toNat A \<equiv> SOME f. toNat_pred A f"
-
-lemma toNat_pred:
-assumes "countable A"
-shows "\<exists> f. toNat_pred A f"
-using assms countable_ex_to_nat toNat_pred_def by (cases rule: countable_cases) auto
-
-lemma toNat_pred_toNat:
-assumes "countable A"
-shows "toNat_pred A (toNat A)"
-unfolding toNat_def apply(rule someI_ex[of "toNat_pred A"])
-using toNat_pred[OF assms] .
-
-lemma bij_betw_toNat:
-assumes c: "countable A" and i: "infinite A"
-shows "bij_betw (toNat A) A (UNIV::nat set)"
-using toNat_pred_toNat[OF c] unfolding toNat_pred_def using i by auto
-
-lemma inj_on_toNat:
-assumes c: "countable A"
-shows "inj_on (toNat A) A"
-using c apply(cases rule: countable_cases)
-using bij_betw_toNat[OF c] toNat_pred_toNat[OF c]
-unfolding toNat_pred_def unfolding bij_betw_def by auto
-
-lemma toNat_inj[simp]:
-assumes c: "countable A" and a: "a \<in> A" and b: "b \<in> A"
-shows "toNat A a = toNat A b \<longleftrightarrow> a = b"
-using inj_on_toNat[OF c] using a b unfolding inj_on_def by auto
-
-lemma image_toNat:
-assumes c: "countable A" and i: "infinite A"
-shows "toNat A ` A = UNIV"
-using bij_betw_toNat[OF assms] unfolding bij_betw_def by simp
-
-lemma toNat_surj:
-assumes "countable A" and i: "infinite A"
-shows "\<exists> a. a \<in> A \<and> toNat A a = n"
-using image_toNat[OF assms]
-by (metis (no_types) image_iff iso_tuple_UNIV_I)
-
-definition
-"fromNat A n \<equiv>
- if n \<in> toNat A ` A then inv_into A (toNat A) n
- else (SOME a. a \<in> A)"
-
-lemma fromNat:
-assumes "A \<noteq> {}"
-shows "fromNat A n \<in> A"
-unfolding fromNat_def by (metis assms equals0I inv_into_into someI_ex)
-
-lemma toNat_fromNat[simp]:
-assumes "n \<in> toNat A ` A"
-shows "toNat A (fromNat A n) = n"
-by (metis assms f_inv_into_f fromNat_def)
-
-lemma infinite_toNat_fromNat[simp]:
-assumes c: "countable A" and i: "infinite A"
-shows "toNat A (fromNat A n) = n"
-apply(rule toNat_fromNat) using toNat_surj[OF assms]
-by (metis image_iff)
-
-lemma fromNat_toNat[simp]:
-assumes c: "countable A" and a: "a \<in> A"
-shows "fromNat A (toNat A a) = a"
-by (metis a c equals0D fromNat imageI toNat_fromNat toNat_inj)
-
-lemma fromNat_inj:
-assumes c: "countable A" and i: "infinite A"
-shows "fromNat A m = fromNat A n \<longleftrightarrow> m = n" (is "?L = ?R \<longleftrightarrow> ?K")
-proof-
-  have "?L = ?R \<longleftrightarrow> toNat A ?L = toNat A ?R"
-  unfolding toNat_inj[OF c fromNat[OF infinite_imp_nonempty[OF i]]
-                           fromNat[OF infinite_imp_nonempty[OF i]]] ..
-  also have "... \<longleftrightarrow> ?K" using c i by simp
-  finally show ?thesis .
-qed
-
-lemma fromNat_surj:
-assumes c: "countable A" and a: "a \<in> A"
-shows "\<exists> n. fromNat A n = a"
-apply(rule exI[of _ "toNat A a"]) using assms by simp
-
-lemma fromNat_image_incl:
-assumes "A \<noteq> {}"
-shows "fromNat A ` UNIV \<subseteq> A"
-using fromNat[OF assms] by auto
-
-lemma incl_fromNat_image:
-assumes "countable A"
-shows "A \<subseteq> fromNat A ` UNIV"
-unfolding image_def using fromNat_surj[OF assms] by auto
-
-lemma fromNat_image[simp]:
-assumes "A \<noteq> {}" and "countable A"
-shows "fromNat A ` UNIV = A"
-by (metis assms equalityI fromNat_image_incl incl_fromNat_image)
-
-lemma fromNat_inject[simp]:
-assumes A: "A \<noteq> {}" "countable A" and B: "B \<noteq> {}" "countable B"
-shows "fromNat A = fromNat B \<longleftrightarrow> A = B"
-by (metis assms fromNat_image)
-
-lemma inj_on_fromNat:
-"inj_on fromNat ({A. A \<noteq> {} \<and> countable A})"
-unfolding inj_on_def by auto
-
-
-subsection {* Preservation under the set theoretic operations *}
-
-lemma contable_empty[simp,intro]:
-"countable {}"
-by (metis countable_ex_to_nat inj_on_empty)
-
-lemma incl_countable:
-assumes "A \<subseteq> B" and "countable B"
-shows "countable A"
-by (metis assms countable_ex_to_nat subset_inj_on)
-
-lemma countable_diff:
-assumes "countable A"
-shows "countable (A - B)"
-by (metis Diff_subset assms incl_countable)
-
-lemma finite_countable[simp]:
-assumes "finite A"
-shows "countable A"
-by (metis assms countable_ex_to_nat finite_imp_inj_to_nat_seg)
-
-lemma countable_singl[simp]:
-"countable {a}"
-by simp
-
-lemma countable_insert[simp]:
-"countable (insert a A) \<longleftrightarrow> countable A"
-proof
-  assume c: "countable A"
-  thus "countable (insert a A)"
-  apply (cases rule: countable_cases_card_of)
-    apply (metis finite_countable finite_insert)
-    unfolding countable_card_of_nat
-    by (metis infinite_card_of_insert ordIso_imp_ordLeq ordIso_transitive)
-qed(insert incl_countable, metis incl_countable subset_insertI)
-
-lemma contable_IntL[simp]:
-assumes "countable A"
-shows "countable (A \<inter> B)"
-by (metis Int_lower1 assms incl_countable)
-
-lemma contable_IntR[simp]:
-assumes "countable B"
-shows "countable (A \<inter> B)"
-by (metis assms contable_IntL inf.commute)
-
-lemma countable_UN[simp]:
-assumes cI: "countable I" and cA: "\<And> i. i \<in> I \<Longrightarrow> countable (A i)"
-shows "countable (\<Union> i \<in> I. A i)"
-using assms unfolding countable_card_of_nat
-apply(intro card_of_UNION_ordLeq_infinite) by auto
-
-lemma contable_Un[simp]:
-"countable (A \<union> B) \<longleftrightarrow> countable A \<and> countable B"
-proof safe
-  assume cA: "countable A" and cB: "countable B"
-  let ?I = "{0,Suc 0}"  let ?As = "\<lambda> i. case i of 0 \<Rightarrow> A|Suc 0 \<Rightarrow> B"
-  have AB: "A \<union> B = (\<Union> i \<in> ?I. ?As i)" by simp
-  show "countable (A \<union> B)" unfolding AB apply(rule countable_UN)
-  using cA cB by auto
-qed (metis Un_upper1 incl_countable, metis Un_upper2 incl_countable)
-
-lemma countable_INT[simp]:
-assumes "i \<in> I" and "countable (A i)"
-shows "countable (\<Inter> i \<in> I. A i)"
-by (metis INF_insert assms contable_IntL insert_absorb)
-
-lemma countable_class[simp]:
-fixes A :: "('a::countable) set"
-shows "countable A"
-proof-
-  have "inj_on to_nat A" by (metis inj_on_to_nat)
-  thus ?thesis by (metis countable_ex_to_nat)
-qed
-
-lemma countable_image[simp]:
-assumes "countable A"
-shows "countable (f ` A)"
-using assms unfolding countable_card_of_nat
-by (metis card_of_image ordLeq_transitive)
-
-lemma countable_ordLeq:
-assumes "|A| \<le>o |B|" and "countable B"
-shows "countable A"
-using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
-
-lemma countable_ordLess:
-assumes AB: "|A| <o |B|" and B: "countable B"
-shows "countable A"
-using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
-
-lemma countable_vimage:
-assumes "B \<subseteq> range f" and "countable (f -` B)"
-shows "countable B"
-by (metis Int_absorb2 assms countable_image image_vimage_eq)
-
-lemma surj_countable_vimage:
-assumes s: "surj f" and c: "countable (f -` B)"
-shows "countable B"
-apply(rule countable_vimage[OF _ c]) using s by auto
-
-lemma countable_Collect[simp]:
-assumes "countable A"
-shows "countable {a \<in> A. \<phi> a}"
-by (metis Collect_conj_eq Int_absorb Int_commute Int_def assms contable_IntR)
-
-lemma countable_Plus[simp]:
-assumes A: "countable A" and B: "countable B"
-shows "countable (A <+> B)"
-proof-
-  let ?U = "UNIV::nat set"
-  have "|A| \<le>o |?U|" and "|B| \<le>o |?U|" using A B
-  using card_of_nat[THEN ordIso_symmetric] ordLeq_ordIso_trans
-  unfolding countable_def by blast+
-  hence "|A <+> B| \<le>o |?U|" by (intro card_of_Plus_ordLeq_infinite) auto
-  thus ?thesis using card_of_nat unfolding countable_def by(rule ordLeq_ordIso_trans)
-qed
-
-lemma countable_Times[simp]:
-assumes A: "countable A" and B: "countable B"
-shows "countable (A \<times> B)"
-proof-
-  let ?U = "UNIV::nat set"
-  have "|A| \<le>o |?U|" and "|B| \<le>o |?U|" using A B
-  using card_of_nat[THEN ordIso_symmetric] ordLeq_ordIso_trans
-  unfolding countable_def by blast+
-  hence "|A \<times> B| \<le>o |?U|" by (intro card_of_Times_ordLeq_infinite) auto
-  thus ?thesis using card_of_nat unfolding countable_def by(rule ordLeq_ordIso_trans)
-qed
-
-lemma ordLeq_countable:
-assumes "|A| \<le>o |B|" and "countable B"
-shows "countable A"
-using assms unfolding countable_def by(rule ordLeq_transitive)
-
-lemma ordLess_countable:
-assumes A: "|A| <o |B|" and B: "countable B"
-shows "countable A"
-by (rule ordLeq_countable[OF ordLess_imp_ordLeq[OF A] B])
-
-lemma countable_def2: "countable A \<longleftrightarrow> |A| \<le>o |UNIV :: nat set|"
-unfolding countable_def using card_of_nat[THEN ordIso_symmetric]
-by (metis (lifting) Field_card_of Field_natLeq card_of_mono2 card_of_nat
-          countable_def ordIso_imp_ordLeq ordLeq_countable)
-
-
-subsection{*  The type of countable sets *}
-
-typedef 'a cset = "{A :: 'a set. countable A}"
-apply(rule exI[of _ "{}"]) by simp
-
-abbreviation rcset where "rcset \<equiv> Rep_cset"
-abbreviation acset where "acset \<equiv> Abs_cset"
-
-lemmas acset_rcset = Rep_cset_inverse
-declare acset_rcset[simp]
-
-lemma acset_surj:
-"\<exists> A. countable A \<and> acset A = C"
-apply(cases rule: Abs_cset_cases[of C]) by auto
-
-lemma rcset_acset[simp]:
-assumes "countable A"
-shows "rcset (acset A) = A"
-using Abs_cset_inverse assms by auto
-
-lemma acset_inj[simp]:
-assumes "countable A" and "countable B"
-shows "acset A = acset B \<longleftrightarrow> A = B"
-using assms Abs_cset_inject by auto
-
-lemma rcset[simp]:
-"countable (rcset C)"
-using Rep_cset by simp
-
-lemma rcset_inj[simp]:
-"rcset C = rcset D \<longleftrightarrow> C = D"
-by (metis acset_rcset)
-
-lemma rcset_surj:
-assumes "countable A"
-shows "\<exists> C. rcset C = A"
-apply(cases rule: Rep_cset_cases[of A])
-using assms by auto
-
-definition "cIn a C \<equiv> (a \<in> rcset C)"
-definition "cEmp \<equiv> acset {}"
-definition "cIns a C \<equiv> acset (insert a (rcset C))"
-abbreviation cSingl where "cSingl a \<equiv> cIns a cEmp"
-definition "cUn C D \<equiv> acset (rcset C \<union> rcset D)"
-definition "cInt C D \<equiv> acset (rcset C \<inter> rcset D)"
-definition "cDif C D \<equiv> acset (rcset C - rcset D)"
-definition "cIm f C \<equiv> acset (f ` rcset C)"
-definition "cVim f D \<equiv> acset (f -` rcset D)"
-(* TODO eventually: nice setup for these operations, copied from the set setup *)
-
-end
diff -r 4ff5d795ed08 -r 885deccc264e src/HOL/BNF/Countable_Type.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Countable_Type.thy	Wed Nov 21 12:05:05 2012 +0100
@@ -0,0 +1,116 @@
+(*  Title:      HOL/BNF/Countable_Type.thy
+    Author:     Andrei Popescu, TU Muenchen
+    Copyright   2012
+
+(At most) countable sets.
+*)
+
+header {* (At Most) Countable Sets *}
+
+theory Countable_Type
+imports "../Cardinals/Cardinals" "~~/src/HOL/Library/Countable_Set"
+begin
+
+subsection{* Cardinal stuff *}
+
+lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|"
+  unfolding countable_def card_of_ordLeq[symmetric] by auto
+
+lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq"
+  unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast
+
+lemma countable_or_card_of:
+assumes "countable A"
+shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
+       (infinite A  \<and> |A| =o |UNIV::nat set| )"
+apply (cases "finite A")
+  apply(metis finite_iff_cardOf_nat)
+  by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq)
+
+lemma countable_cases_card_of[elim]:
+  assumes "countable A"
+  obtains (Fin) "finite A" "|A| <o |UNIV::nat set|"
+        | (Inf) "infinite A" "|A| =o |UNIV::nat set|"
+  using assms countable_or_card_of by blast
+
+lemma countable_or:
+  "countable A \<Longrightarrow> (\<exists> f::'a\<Rightarrow>nat. finite A \<and> inj_on f A) \<or> (\<exists> f::'a\<Rightarrow>nat. infinite A \<and> bij_betw f A UNIV)"
+  by (auto elim: countable_enum_cases)
+
+lemma countable_cases[elim]:
+  assumes "countable A"
+  obtains (Fin) f :: "'a\<Rightarrow>nat" where "finite A" "inj_on f A"
+        | (Inf) f :: "'a\<Rightarrow>nat" where "infinite A" "bij_betw f A UNIV"
+  using assms countable_or by metis
+
+lemma countable_ordLeq:
+assumes "|A| \<le>o |B|" and "countable B"
+shows "countable A"
+using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
+
+lemma countable_ordLess:
+assumes AB: "|A| <o |B|" and B: "countable B"
+shows "countable A"
+using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
+
+lemma ordLeq_countable:
+assumes "|A| \<le>o |B|" and "countable B"
+shows "countable A"
+using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
+
+lemma ordLess_countable:
+assumes A: "|A| <o |B|" and B: "countable B"
+shows "countable A"
+by (rule ordLeq_countable[OF ordLess_imp_ordLeq[OF A] B])
+
+subsection{*  The type of countable sets *}
+
+typedef 'a cset = "{A :: 'a set. countable A}"
+apply(rule exI[of _ "{}"]) by simp
+
+abbreviation rcset where "rcset \<equiv> Rep_cset"
+abbreviation acset where "acset \<equiv> Abs_cset"
+
+lemmas acset_rcset = Rep_cset_inverse
+declare acset_rcset[simp]
+
+lemma acset_surj:
+"\<exists> A. countable A \<and> acset A = C"
+apply(cases rule: Abs_cset_cases[of C]) by auto
+
+lemma rcset_acset[simp]:
+assumes "countable A"
+shows "rcset (acset A) = A"
+using Abs_cset_inverse assms by auto
+
+lemma acset_inj[simp]:
+assumes "countable A" and "countable B"
+shows "acset A = acset B \<longleftrightarrow> A = B"
+using assms Abs_cset_inject by auto
+
+lemma rcset[simp]:
+"countable (rcset C)"
+using Rep_cset by simp
+
+lemma rcset_inj[simp]:
+"rcset C = rcset D \<longleftrightarrow> C = D"
+by (metis acset_rcset)
+
+lemma rcset_surj:
+assumes "countable A"
+shows "\<exists> C. rcset C = A"
+apply(cases rule: Rep_cset_cases[of A])
+using assms by auto
+
+definition "cIn a C \<equiv> (a \<in> rcset C)"
+definition "cEmp \<equiv> acset {}"
+definition "cIns a C \<equiv> acset (insert a (rcset C))"
+abbreviation cSingl where "cSingl a \<equiv> cIns a cEmp"
+definition "cUn C D \<equiv> acset (rcset C \<union> rcset D)"
+definition "cInt C D \<equiv> acset (rcset C \<inter> rcset D)"
+definition "cDif C D \<equiv> acset (rcset C - rcset D)"
+definition "cIm f C \<equiv> acset (f ` rcset C)"
+definition "cVim f D \<equiv> acset (f -` rcset D)"
+(* TODO eventually: nice setup for these operations, copied from the set setup *)
+
+end
diff -r 4ff5d795ed08 -r 885deccc264e src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Wed Nov 21 10:51:12 2012 +0100
+++ b/src/HOL/BNF/More_BNFs.thy	Wed Nov 21 12:05:05 2012 +0100
@@ -16,7 +16,7 @@
   BNF_GFP
   "~~/src/HOL/Quotient_Examples/FSet"
   "~~/src/HOL/Library/Multiset"
-  Countable_Set
+  Countable_Type
 begin
 
 lemma option_rec_conv_option_case: "option_rec = option_case"
@@ -478,7 +478,7 @@
 lemma card_of_countable_sets_range:
 fixes A :: "'a set"
 shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|"
-apply(rule card_of_ordLeqI[of fromNat]) using inj_on_fromNat
+apply(rule card_of_ordLeqI[of from_nat_into]) using inj_on_from_nat_into
 unfolding inj_on_def by auto
 
 lemma card_of_countable_sets_Func:
@@ -592,7 +592,7 @@
 next
   show "cinfinite natLeq" by (rule natLeq_cinfinite)
 next
-  fix C show "|rcset C| \<le>o natLeq" using rcset unfolding countable_def .
+  fix C show "|rcset C| \<le>o natLeq" using rcset unfolding countable_card_le_natLeq .
 next
   fix A :: "'a set"
   have "|{Z. rcset Z \<subseteq> A}| \<le>o |acset ` {X. X \<subseteq> A \<and> countable X}|"
diff -r 4ff5d795ed08 -r 885deccc264e 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 -