finite vimage on arbitrary domains

--- a/src/HOL/Finite_Set.thy	Tue Jul 26 22:53:06 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Jul 27 19:34:30 2011 +0200
@@ -280,14 +280,18 @@
        blast
 qed
 
-lemma finite_vimageI:
-  "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
+lemma finite_vimage_IntI:
+  "finite F \<Longrightarrow> inj_on h A \<Longrightarrow> finite (h -` F \<inter> A)"
   apply (induct rule: finite_induct)
    apply simp_all
   apply (subst vimage_insert)
-  apply (simp add: finite_subset [OF inj_vimage_singleton])
+  apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
   done
 
+lemma finite_vimageI:
+  "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"

--- a/src/HOL/Fun.thy	Tue Jul 26 22:53:06 2011 +0200
+++ b/src/HOL/Fun.thy	Wed Jul 27 19:34:30 2011 +0200
@@ -556,6 +556,10 @@
   apply (blast intro: the_equality [symmetric])
   done
 
+lemma inj_on_vimage_singleton:
+  "inj_on f A \<Longrightarrow> f -` {a} \<inter> A \<subseteq> {THE x. x \<in> A \<and> f x = a}"
+  by (auto simp add: inj_on_def intro: the_equality [symmetric])
+
 lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A"
   by (auto intro!: inj_onI)