# HG changeset patch
# User haftmann
# Date 1184874463 -7200
# Node ID ebec38420a85e190f4f9fb7bc86772317934f9cc
# Parent  b1a754e544b6f2b51de6cc7e28052cef1c8fa96a
code lemma for of_int

diff -r b1a754e544b6 -r ebec38420a85 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Jul 19 21:47:42 2007 +0200
+++ b/src/HOL/Presburger.thy	Thu Jul 19 21:47:43 2007 +0200
@@ -703,4 +703,37 @@
   less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   less_number_of
 
+
+lemma of_int_num [code func]:
+  "of_int k = (if k = 0 then 0 else if k < 0 then
+     - of_int (- k) else let
+       (l, m) = divAlg (k, 2);
+       l' = of_int l
+     in if m = 0 then l' + l' else l' + l' + 1)"
+proof -
+  have aux1: "k mod (2\<Colon>int) \<noteq> (0\<Colon>int) \<Longrightarrow> 
+    of_int k = of_int (k div 2 * 2 + 1)"
+  proof -
+    assume "k mod 2 \<noteq> 0"
+    then have "k mod 2 = 1" by arith
+    moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
+    ultimately show ?thesis by auto
+  qed
+  have aux2: "\<And>x. of_int 2 * x = x + x"
+  proof -
+    fix x
+    have int2: "(2::int) = 1 + 1" by arith
+    show "of_int 2 * x = x + x"
+    unfolding int2 of_int_add left_distrib by simp
+  qed
+  have aux3: "\<And>x. x * of_int 2 = x + x"
+  proof -
+    fix x
+    have int2: "(2::int) = 1 + 1" by arith
+    show "x * of_int 2 = x + x" 
+    unfolding int2 of_int_add right_distrib by simp
+  qed
+  from aux1 show ?thesis by (auto simp add: divAlg_mod_div Let_def aux2 aux3)
+qed
+
 end