[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
begin

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

end
 
 
--
Victor Porton - http://portonvictor.org


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