add lemma inj_of_nat

--- a/src/HOL/Nat.thy	Tue Jun 12 21:59:40 2007 +0200
+++ b/src/HOL/Nat.thy	Tue Jun 12 23:14:29 2007 +0200
@@ -1368,6 +1368,9 @@
 lemma of_nat_eq_0_iff [simp]: "(of_nat m = (0::'a::semiring_char_0)) = (m = 0)"
   by (rule of_nat_eq_iff [of _ 0, simplified])
 
+lemma inj_of_nat: "inj (of_nat :: nat \<Rightarrow> 'a::semiring_char_0)"
+  by (simp add: inj_on_def)
+
 lemma of_nat_diff [simp]:
     "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
   by (simp del: of_nat_add