# HG changeset patch
# User hoelzl
# Date 1311788070 -7200
# Node ID f4a7697011c587ef27361c1e078d21c254fdf0bf
# Parent  3928b3448f38b6d688f0c6e2820c14e5e7cf9ee9
finite vimage on arbitrary domains

diff -r 3928b3448f38 -r f4a7697011c5 src/HOL/Finite_Set.thy
--- 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"
diff -r 3928b3448f38 -r f4a7697011c5 src/HOL/Fun.thy
--- 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)