src/HOL/Fun.thy
changeset 61520 8f85bb443d33
parent 61378 3e04c9ca001a
child 61630 608520e0e8e2
     1.1 --- a/src/HOL/Fun.thy	Mon Oct 26 23:42:01 2015 +0000
     1.2 +++ b/src/HOL/Fun.thy	Tue Oct 27 15:17:02 2015 +0000
     1.3 @@ -171,7 +171,7 @@
     1.4  lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y"
     1.5  by (simp add: inj_on_def)
     1.6  
     1.7 -lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
     1.8 +lemma inj_on_eq_iff: "\<lbrakk>inj_on f A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y)"
     1.9  by (force simp add: inj_on_def)
    1.10  
    1.11  lemma inj_on_cong:
    1.12 @@ -217,9 +217,6 @@
    1.13  lemma inj_onD: "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y"
    1.14  by (unfold inj_on_def, blast)
    1.15  
    1.16 -lemma inj_on_iff: "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)"
    1.17 -  by (fact inj_on_eq_iff)
    1.18 -
    1.19  lemma comp_inj_on:
    1.20       "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A"
    1.21  by (simp add: comp_def inj_on_def)
    1.22 @@ -498,6 +495,10 @@
    1.23  lemma inj_on_image_mem_iff: "\<lbrakk>inj_on f B; a \<in> B; A \<subseteq> B\<rbrakk> \<Longrightarrow> f a \<in> f`A \<longleftrightarrow> a \<in> A"
    1.24    by (auto simp: inj_on_def)
    1.25  
    1.26 +(*FIXME DELETE*)
    1.27 +lemma inj_on_image_mem_iff_alt: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f a \<in> f`A \<Longrightarrow> a \<in> B \<Longrightarrow> a \<in> A"
    1.28 +  by (blast dest: inj_onD)
    1.29 +
    1.30  lemma inj_image_mem_iff: "inj f \<Longrightarrow> f a \<in> f`A \<longleftrightarrow> a \<in> A"
    1.31    by (blast dest: injD)
    1.32