src/HOL/Fun.thy
changeset 53927 abe2b313f0e5
parent 52435 6646bb548c6b
child 54147 97a8ff4e4ac9
     1.1 --- a/src/HOL/Fun.thy	Thu Sep 26 13:51:08 2013 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Sep 26 15:50:33 2013 +0200
     1.3 @@ -491,8 +491,11 @@
     1.4  apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
     1.5  done
     1.6  
     1.7 +lemma inj_on_image_eq_iff: "\<lbrakk> inj_on f C; A \<subseteq> C; B \<subseteq> C \<rbrakk> \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
     1.8 +by(fastforce simp add: inj_on_def)
     1.9 +
    1.10  lemma inj_on_Un_image_eq_iff: "inj_on f (A \<union> B) \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
    1.11 -by(blast dest: inj_onD)
    1.12 +by(erule inj_on_image_eq_iff) simp_all
    1.13  
    1.14  lemma inj_on_image_Int:
    1.15     "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A Int B) = f`A Int f`B"