countability of the image of a reflexive transitive closure

--- a/src/HOL/Library/Countable_Set.thy	Tue Nov 12 19:28:51 2013 +0100
+++ b/src/HOL/Library/Countable_Set.thy	Tue Nov 12 19:28:51 2013 +0100
@@ -230,6 +230,27 @@
 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_Image:
+  assumes "\<And>y. y \<in> Y \<Longrightarrow> countable (X `` {y})"
+  assumes "countable Y"
+  shows "countable (X `` Y)"
+proof -
+  have "countable (X `` (\<Union>y\<in>Y. {y}))"
+    unfolding Image_UN by (intro countable_UN assms)
+  then show ?thesis by simp
+qed
+
+lemma countable_relpow:
+  fixes X :: "'a rel"
+  assumes Image_X: "\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)"
+  assumes Y: "countable Y"
+  shows "countable ((X ^^ i) `` Y)"
+  using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X)
+
+lemma countable_rtrancl:
+  "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X^* `` Y)"
+  unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow)
+
 lemma countable_lists[intro, simp]:
   assumes A: "countable A" shows "countable (lists A)"
 proof -

--- a/src/HOL/Relation.thy	Tue Nov 12 19:28:51 2013 +0100
+++ b/src/HOL/Relation.thy	Tue Nov 12 19:28:51 2013 +0100
@@ -994,6 +994,9 @@
 lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))"
   by blast
 
+lemma UN_Image: "(\<Union>i\<in>I. X i) `` S = (\<Union>i\<in>I. X i `` S)"
+  by auto
+
 lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))"
   by blast
 
@@ -1011,6 +1014,11 @@
 lemma Image_Collect_split [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}"
   by auto
 
+lemma Sigma_Image: "(SIGMA x:A. B x) `` X = (\<Union>x\<in>X \<inter> A. B x)"
+  by auto
+
+lemma relcomp_Image: "(X O Y) `` Z = Y `` (X `` Z)"
+  by auto
 
 subsubsection {* Inverse image *}