# HG changeset patch
# User Andreas Lochbihler
# Date 1423660350 -3600
# Node ID 2fb0c0fc62a319cc16cc7bd810502a1f4943b73b
# Parent  28cfc60dea7acc06e58d8899bdb457c53b0edf4a
add more general version of finite_vimageD

diff -r 28cfc60dea7a -r 2fb0c0fc62a3 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Feb 11 14:07:28 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Feb 11 14:12:30 2015 +0100
@@ -315,14 +315,11 @@
   "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
   using finite_vimage_IntI[of F h UNIV] by auto
 
-lemma finite_vimageD:
-  assumes fin: "finite (h -` F)" and surj: "surj h"
-  shows "finite F"
-proof -
-  have "finite (h ` (h -` F))" using fin by (rule finite_imageI)
-  also have "h ` (h -` F) = F" using surj by (rule surj_image_vimage_eq)
-  finally show "finite F" .
-qed
+lemma finite_vimageD': "\<lbrakk> finite (f -` A); A \<subseteq> range f \<rbrakk> \<Longrightarrow> finite A"
+by(auto simp add: subset_image_iff intro: finite_subset[rotated])
+
+lemma finite_vimageD: "\<lbrakk> finite (h -` F); surj h \<rbrakk> \<Longrightarrow> finite F"
+by(auto dest: finite_vimageD')
 
 lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
   unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)