added of_int_of_nat

--- a/src/HOL/IntArith.thy	Thu Jul 19 21:47:34 2007 +0200
+++ b/src/HOL/IntArith.thy	Thu Jul 19 21:47:36 2007 +0200
@@ -212,6 +212,9 @@
   with False show ?thesis by simp
 qed
 
+lemma of_int_of_nat: "of_int k = (if k < 0 then - of_nat (nat (- k))
+  else of_nat (nat k))"
+  by (auto simp add: of_nat_nat)
 
 lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
 apply (cases "0 \<le> z'")