# HG changeset patch
# User haftmann
# Date 1184874456 -7200
# Node ID 7921b81baf96d5b90a23efd1c107b15d4fbcd597
# Parent  f1434532a562fd06d67bfd0124cc8b8d4b07e37a
added of_int_of_nat

diff -r f1434532a562 -r 7921b81baf96 src/HOL/IntArith.thy
--- 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'")