# HG changeset patch
# User haftmann
# Date 1268146035 -3600
# Node ID 178caf872f957af049ecae2410013731330f3857
# Parent  4b01ddafc8a954b7446f83adaf7e313620905a06
weakend class ring_div; tuned

diff -r 4b01ddafc8a9 -r 178caf872f95 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Mar 08 14:41:56 2010 +0100
+++ b/src/HOL/Divides.thy	Tue Mar 09 15:47:15 2010 +0100
@@ -376,7 +376,7 @@
 
 end
 
-class ring_div = semiring_div + idom
+class ring_div = semiring_div + comm_ring_1
 begin
 
 text {* Negation respects modular equivalence. *}
@@ -2353,47 +2353,6 @@
 apply (rule Divides.div_less_dividend, simp_all)
 done
 
-text {* code generator setup *}
-
-context ring_1
-begin
-
-lemma of_int_num [code]:
-  "of_int k = (if k = 0 then 0 else if k < 0 then
-     - of_int (- k) else let
-       (l, m) = divmod_int 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: divmod_int_mod_div Let_def aux2 aux3)
-qed
-
-end
-
 lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
 proof
   assume H: "x mod n = y mod n"
@@ -2482,6 +2441,7 @@
                        mod_div_equality' [THEN eq_reflection]
                        zmod_zdiv_equality' [THEN eq_reflection]
 
+
 subsubsection {* Code generation *}
 
 definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
@@ -2515,6 +2475,45 @@
   then show ?thesis by (simp add: divmod_int_pdivmod)
 qed
 
+context ring_1
+begin
+
+lemma of_int_num [code]:
+  "of_int k = (if k = 0 then 0 else if k < 0 then
+     - of_int (- k) else let
+       (l, m) = divmod_int 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: divmod_int_mod_div Let_def aux2 aux3)
+qed
+
+end
+
 code_modulename SML
   Divides Arith