1.1 --- a/src/HOL/Library/Countable_Set.thy	Tue Nov 12 19:28:51 2013 +0100
     1.2 +++ b/src/HOL/Library/Countable_Set.thy	Tue Nov 12 19:28:51 2013 +0100
     1.3 @@ -230,6 +230,27 @@
     1.4  lemma countable_Collect[simp]: "countable A \<Longrightarrow> countable {a \<in> A. \<phi> a}"
     1.5    by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1)
     1.6  
     1.7 +lemma countable_Image:
     1.8 +  assumes "\<And>y. y \<in> Y \<Longrightarrow> countable (X `` {y})"
     1.9 +  assumes "countable Y"
    1.10 +  shows "countable (X `` Y)"
    1.11 +proof -
    1.12 +  have "countable (X `` (\<Union>y\<in>Y. {y}))"
    1.13 +    unfolding Image_UN by (intro countable_UN assms)
    1.14 +  then show ?thesis by simp
    1.15 +qed
    1.16 +
    1.17 +lemma countable_relpow:
    1.18 +  fixes X :: "'a rel"
    1.19 +  assumes Image_X: "\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)"
    1.20 +  assumes Y: "countable Y"
    1.21 +  shows "countable ((X ^^ i) `` Y)"
    1.22 +  using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X)
    1.23 +
    1.24 +lemma countable_rtrancl:
    1.25 +  "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X^* `` Y)"
    1.26 +  unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow)
    1.27 +
    1.28  lemma countable_lists[intro, simp]:
    1.29    assumes A: "countable A" shows "countable (lists A)"
    1.30  proof -

     2.1 --- a/src/HOL/Relation.thy	Tue Nov 12 19:28:51 2013 +0100
     2.2 +++ b/src/HOL/Relation.thy	Tue Nov 12 19:28:51 2013 +0100
     2.3 @@ -994,6 +994,9 @@
     2.4  lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))"
     2.5    by blast
     2.6  
     2.7 +lemma UN_Image: "(\<Union>i\<in>I. X i) `` S = (\<Union>i\<in>I. X i `` S)"
     2.8 +  by auto
     2.9 +
    2.10  lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))"
    2.11    by blast
    2.12  
    2.13 @@ -1011,6 +1014,11 @@
    2.14  lemma Image_Collect_split [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}"
    2.15    by auto
    2.16  
    2.17 +lemma Sigma_Image: "(SIGMA x:A. B x) `` X = (\<Union>x\<in>X \<inter> A. B x)"
    2.18 +  by auto
    2.19 +
    2.20 +lemma relcomp_Image: "(X O Y) `` Z = Y `` (X `` Z)"
    2.21 +  by auto
    2.22  
    2.23  subsubsection {* Inverse image *}
    2.24