1.1 --- a/src/HOL/Finite_Set.thy	Sun Nov 29 11:31:39 2009 -0800
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu Dec 17 07:02:13 2009 -0800
     1.3 @@ -204,6 +204,9 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma rev_finite_subset: "finite B ==> A \<subseteq> B ==> finite A"
     1.8 +by (rule finite_subset)
     1.9 +
    1.10  lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
    1.11  by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
    1.12  
    1.13 @@ -355,6 +358,18 @@
    1.14    apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
    1.15    done
    1.16  
    1.17 +lemma finite_vimageD:
    1.18 +  assumes fin: "finite (h -` F)" and surj: "surj h"
    1.19 +  shows "finite F"
    1.20 +proof -
    1.21 +  have "finite (h ` (h -` F))" using fin by (rule finite_imageI)
    1.22 +  also have "h ` (h -` F) = F" using surj by (rule surj_image_vimage_eq)
    1.23 +  finally show "finite F" .
    1.24 +qed
    1.25 +
    1.26 +lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
    1.27 +  unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
    1.28 +
    1.29  
    1.30  text {* The finite UNION of finite sets *}
    1.31