--- a/src/HOL/Fun.thy Sat Oct 17 13:46:55 2009 +0200
+++ b/src/HOL/Fun.thy Sun Oct 18 12:07:25 2009 +0200
@@ -145,10 +145,12 @@
lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y"
by (simp add: inj_on_def)
-(*Useful with the simplifier*)
-lemma inj_eq: "inj(f) ==> (f(x) = f(y)) = (x=y)"
+lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
by (force simp add: inj_on_def)
+lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)"
+by (simp add: inj_on_eq_iff)
+
lemma inj_on_id[simp]: "inj_on id A"
by (simp add: inj_on_def)
@@ -511,7 +513,7 @@
shows "inv f (f x) = x"
proof -
from assms have "(THE x'. f x' = f x) = (THE x'. x' = x)"
- by (simp only: inj_eq)
+ by (simp add: inj_on_eq_iff)
also have "... = x" by (rule the_eq_trivial)
finally show ?thesis by (unfold inv_def)
qed