1.1 --- a/src/HOL/Finite_Set.thy	Tue Jul 26 22:53:06 2011 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Jul 27 19:34:30 2011 +0200
     1.3 @@ -280,14 +280,18 @@
     1.4         blast
     1.5  qed
     1.6  
     1.7 -lemma finite_vimageI:
     1.8 -  "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
     1.9 +lemma finite_vimage_IntI:
    1.10 +  "finite F \<Longrightarrow> inj_on h A \<Longrightarrow> finite (h -` F \<inter> A)"
    1.11    apply (induct rule: finite_induct)
    1.12     apply simp_all
    1.13    apply (subst vimage_insert)
    1.14 -  apply (simp add: finite_subset [OF inj_vimage_singleton])
    1.15 +  apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
    1.16    done
    1.17  
    1.18 +lemma finite_vimageI:
    1.19 +  "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
    1.20 +  using finite_vimage_IntI[of F h UNIV] by auto
    1.21 +
    1.22  lemma finite_vimageD:
    1.23    assumes fin: "finite (h -` F)" and surj: "surj h"
    1.24    shows "finite F"

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