--- a/src/HOL/Library/Countable_Set.thy Mon May 25 22:52:17 2015 +0200
+++ b/src/HOL/Library/Countable_Set.thy Tue May 26 21:58:04 2015 +0100
@@ -182,6 +182,9 @@
by (blast dest: comp_inj_on subset_inj_on intro: countableI)
qed
+lemma countable_image_inj_on: "countable (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> countable A"
+ by (metis countable_image the_inv_into_onto)
+
lemma countable_UN[intro, simp]:
fixes I :: "'i set" and A :: "'i => 'a set"
assumes I: "countable I"
@@ -221,6 +224,9 @@
lemma countable_Diff[intro, simp]: "countable A \<Longrightarrow> countable (A - B)"
by (blast intro: countable_subset)
+lemma countable_insert_eq [simp]: "countable (insert x A) = countable A"
+ by auto (metis Diff_insert_absorb countable_Diff insert_absorb)
+
lemma countable_vimage: "B \<subseteq> range f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
by (metis Int_absorb2 assms countable_image image_vimage_eq)
@@ -325,4 +331,7 @@
"uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
using countable_Un[of B "A - B"] assms by auto
+lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A"
+ by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable)
+
end