[isabelle] Proving that a function is injection

I have the following problem (I may attempt to solve it myself but I think that would lead to a messy non-optimal solution, but I want to see the best way to solve it):
How to prove that a given function is injection?
theory test
  imports Main_ZF

theorem assumes "f: A->B" and "w:A & x:A ==> (f`w=f`x --> w=x)"
  shows "f: inj(A,B)"

Victor Porton - http://portonvictor.org

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.