# HG changeset patch
# User haftmann
# Date 1207144706 -7200
# Node ID 6da615cef733f19780a791443e4e41bc01d840e5
# Parent  c4202c67fe3e16b9f59402ec2b5d2888a444921a
moved some code lemmas for Numerals here

diff -r c4202c67fe3e -r 6da615cef733 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Apr 02 12:32:53 2008 +0200
+++ b/src/HOL/Int.thy	Wed Apr 02 15:58:26 2008 +0200
@@ -1797,9 +1797,125 @@
 
 subsection {* Configuration of the code generator *}
 
-instance int :: eq ..
+code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
+
+lemmas pred_succ_numeral_code [code func] =
+  pred_bin_simps succ_bin_simps
+
+lemmas plus_numeral_code [code func] =
+  add_bin_simps
+  arith_extra_simps(1) [where 'a = int]
+
+lemmas minus_numeral_code [code func] =
+  minus_bin_simps
+  arith_extra_simps(2) [where 'a = int]
+  arith_extra_simps(5) [where 'a = int]
+
+lemmas times_numeral_code [code func] =
+  mult_bin_simps
+  arith_extra_simps(4) [where 'a = int]
+
+instantiation int :: eq
+begin
+
+definition [code func del]: "eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
+
+instance by default (simp add: eq_int_def)
+
+end
+
+lemma eq_number_of_int_code [code func]:
+  "eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq k l"
+  unfolding eq_int_def number_of_is_id ..
+
+lemma eq_int_code [code func]:
+  "eq Int.Pls Int.Pls \<longleftrightarrow> True"
+  "eq Int.Pls Int.Min \<longleftrightarrow> False"
+  "eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq Int.Pls k2"
+  "eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
+  "eq Int.Min Int.Pls \<longleftrightarrow> False"
+  "eq Int.Min Int.Min \<longleftrightarrow> True"
+  "eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
+  "eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq Int.Min k2"
+  "eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq Int.Pls k1"
+  "eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
+  "eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
+  "eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq Int.Min k1"
+  "eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq k1 k2"
+  "eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
+  "eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
+  "eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq k1 k2"
+  unfolding eq_number_of_int_code [symmetric, of Int.Pls] 
+    eq_number_of_int_code [symmetric, of Int.Min]
+    eq_number_of_int_code [symmetric, of "Int.Bit0 k1"]
+    eq_number_of_int_code [symmetric, of "Int.Bit1 k1"]
+    eq_number_of_int_code [symmetric, of "Int.Bit0 k2"]
+    eq_number_of_int_code [symmetric, of "Int.Bit1 k2"]
+  by (simp_all add: eq Pls_def,
+    simp_all only: Min_def succ_def pred_def number_of_is_id)
+    (auto simp add: iszero_def)
 
-code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
+lemma less_eq_number_of_int_code [code func]:
+  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
+  unfolding number_of_is_id ..
+
+lemma less_eq_int_code [code func]:
+  "Int.Pls \<le> Int.Pls \<longleftrightarrow> True"
+  "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
+  "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
+  "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
+  "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
+  "Int.Min \<le> Int.Min \<longleftrightarrow> True"
+  "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
+  "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
+  "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
+  "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
+  "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
+  "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
+  "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
+  "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
+  "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
+  "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
+  unfolding less_eq_number_of_int_code [symmetric, of Int.Pls] 
+    less_eq_number_of_int_code [symmetric, of Int.Min]
+    less_eq_number_of_int_code [symmetric, of "Int.Bit0 k1"]
+    less_eq_number_of_int_code [symmetric, of "Int.Bit1 k1"]
+    less_eq_number_of_int_code [symmetric, of "Int.Bit0 k2"]
+    less_eq_number_of_int_code [symmetric, of "Int.Bit1 k2"]
+  by (simp_all add: Pls_def, simp_all only: Min_def succ_def pred_def number_of_is_id)
+    (auto simp add: neg_def linorder_not_less group_simps
+      zle_add1_eq_le [symmetric] del: iffI , auto simp only: Bit0_def Bit1_def)
+
+lemma less_number_of_int_code [code func]:
+  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
+  unfolding number_of_is_id ..
+
+lemma less_int_code [code func]:
+  "Int.Pls < Int.Pls \<longleftrightarrow> False"
+  "Int.Pls < Int.Min \<longleftrightarrow> False"
+  "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
+  "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
+  "Int.Min < Int.Pls \<longleftrightarrow> True"
+  "Int.Min < Int.Min \<longleftrightarrow> False"
+  "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
+  "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
+  "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
+  "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
+  "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
+  "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
+  "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
+  "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
+  "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
+  "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
+  unfolding less_number_of_int_code [symmetric, of Int.Pls] 
+    less_number_of_int_code [symmetric, of Int.Min]
+    less_number_of_int_code [symmetric, of "Int.Bit0 k1"]
+    less_number_of_int_code [symmetric, of "Int.Bit1 k1"]
+    less_number_of_int_code [symmetric, of "Int.Bit0 k2"]
+    less_number_of_int_code [symmetric, of "Int.Bit1 k2"]
+  by (simp_all add: Pls_def, simp_all only: Min_def succ_def pred_def number_of_is_id)
+    (auto simp add: neg_def group_simps zle_add1_eq_le [symmetric] del: iffI,
+      auto simp only: Bit0_def Bit1_def)
 
 definition
   int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
diff -r c4202c67fe3e -r 6da615cef733 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Wed Apr 02 12:32:53 2008 +0200
+++ b/src/HOL/IntDiv.thy	Wed Apr 02 15:58:26 2008 +0200
@@ -1486,6 +1486,45 @@
 
 text {* code generator setup *}
 
+context ring_1
+begin
+
+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 -
+    have "k mod 2 < 2" by (auto intro: pos_mod_bound)
+    moreover have "0 \<le> k mod 2" by (auto intro: pos_mod_sign)
+    moreover assume "k mod 2 \<noteq> 0"
+    ultimately 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
+
 code_modulename SML
   IntDiv Integer