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