src/HOL/Fun.thy
 changeset 32988 d1d4d7a08a66 parent 32961 61431a41ddd5 child 32998 31b19fa0de0b
```     1.1 --- a/src/HOL/Fun.thy	Sat Oct 17 13:46:55 2009 +0200
1.2 +++ b/src/HOL/Fun.thy	Sun Oct 18 12:07:25 2009 +0200
1.3 @@ -145,10 +145,12 @@
1.4  lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y"
1.5  by (simp add: inj_on_def)
1.6
1.7 -(*Useful with the simplifier*)
1.8 -lemma inj_eq: "inj(f) ==> (f(x) = f(y)) = (x=y)"
1.9 +lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
1.10  by (force simp add: inj_on_def)
1.11
1.12 +lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)"
1.13 +by (simp add: inj_on_eq_iff)
1.14 +
1.15  lemma inj_on_id[simp]: "inj_on id A"
1.16    by (simp add: inj_on_def)
1.17
1.18 @@ -511,7 +513,7 @@
1.19    shows "inv f (f x) = x"
1.20  proof -
1.21    from assms have "(THE x'. f x' = f x) = (THE x'. x' = x)"
1.22 -    by (simp only: inj_eq)
1.23 +    by (simp add: inj_on_eq_iff)
1.24    also have "... = x" by (rule the_eq_trivial)
1.25    finally show ?thesis by (unfold inv_def)
1.26  qed
```