# HG changeset patch
# User haftmann
# Date 1507494501 -7200
# Node ID c3631f32dfeb81f1bcd5eccefde5d17116583c9f
# Parent  a4e82b58d8336c3a0b434724927c7c71b28864a7
tuned structure

diff -r a4e82b58d833 -r c3631f32dfeb src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -9,82 +9,6 @@
   imports Nat_Transfer
 begin
 
-subsection \<open>Quotient and remainder in integral domains\<close>
-
-class semidom_modulo = algebraic_semidom + semiring_modulo
-begin
-
-lemma mod_0 [simp]: "0 mod a = 0"
-  using div_mult_mod_eq [of 0 a] by simp
-
-lemma mod_by_0 [simp]: "a mod 0 = a"
-  using div_mult_mod_eq [of a 0] by simp
-
-lemma mod_by_1 [simp]:
-  "a mod 1 = 0"
-proof -
-  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
-  then have "a + a mod 1 = a + 0" by simp
-  then show ?thesis by (rule add_left_imp_eq)
-qed
-
-lemma mod_self [simp]:
-  "a mod a = 0"
-  using div_mult_mod_eq [of a a] by simp
-
-lemma dvd_imp_mod_0 [simp]:
-  assumes "a dvd b"
-  shows "b mod a = 0"
-  using assms minus_div_mult_eq_mod [of b a] by simp
-
-lemma mod_0_imp_dvd: 
-  assumes "a mod b = 0"
-  shows   "b dvd a"
-proof -
-  have "b dvd ((a div b) * b)" by simp
-  also have "(a div b) * b = a"
-    using div_mult_mod_eq [of a b] by (simp add: assms)
-  finally show ?thesis .
-qed
-
-lemma mod_eq_0_iff_dvd:
-  "a mod b = 0 \<longleftrightarrow> b dvd a"
-  by (auto intro: mod_0_imp_dvd)
-
-lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
-  "a dvd b \<longleftrightarrow> b mod a = 0"
-  by (simp add: mod_eq_0_iff_dvd)
-
-lemma dvd_mod_iff: 
-  assumes "c dvd b"
-  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
-proof -
-  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
-    by (simp add: dvd_add_right_iff)
-  also have "(a div b) * b + a mod b = a"
-    using div_mult_mod_eq [of a b] by simp
-  finally show ?thesis .
-qed
-
-lemma dvd_mod_imp_dvd:
-  assumes "c dvd a mod b" and "c dvd b"
-  shows "c dvd a"
-  using assms dvd_mod_iff [of c b a] by simp
-
-end
-
-class idom_modulo = idom + semidom_modulo
-begin
-
-subclass idom_divide ..
-
-lemma div_diff [simp]:
-  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
-  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
-
-end
-
-  
 subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
   
 class euclidean_semiring = semidom_modulo + normalization_semidom + 
diff -r a4e82b58d833 -r c3631f32dfeb src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -1558,6 +1558,82 @@
 end
 
 
+text \<open>Quotient and remainder in integral domains\<close>
+
+class semidom_modulo = algebraic_semidom + semiring_modulo
+begin
+
+lemma mod_0 [simp]: "0 mod a = 0"
+  using div_mult_mod_eq [of 0 a] by simp
+
+lemma mod_by_0 [simp]: "a mod 0 = a"
+  using div_mult_mod_eq [of a 0] by simp
+
+lemma mod_by_1 [simp]:
+  "a mod 1 = 0"
+proof -
+  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
+  then have "a + a mod 1 = a + 0" by simp
+  then show ?thesis by (rule add_left_imp_eq)
+qed
+
+lemma mod_self [simp]:
+  "a mod a = 0"
+  using div_mult_mod_eq [of a a] by simp
+
+lemma dvd_imp_mod_0 [simp]:
+  assumes "a dvd b"
+  shows "b mod a = 0"
+  using assms minus_div_mult_eq_mod [of b a] by simp
+
+lemma mod_0_imp_dvd: 
+  assumes "a mod b = 0"
+  shows   "b dvd a"
+proof -
+  have "b dvd ((a div b) * b)" by simp
+  also have "(a div b) * b = a"
+    using div_mult_mod_eq [of a b] by (simp add: assms)
+  finally show ?thesis .
+qed
+
+lemma mod_eq_0_iff_dvd:
+  "a mod b = 0 \<longleftrightarrow> b dvd a"
+  by (auto intro: mod_0_imp_dvd)
+
+lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
+  "a dvd b \<longleftrightarrow> b mod a = 0"
+  by (simp add: mod_eq_0_iff_dvd)
+
+lemma dvd_mod_iff: 
+  assumes "c dvd b"
+  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
+proof -
+  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
+    by (simp add: dvd_add_right_iff)
+  also have "(a div b) * b + a mod b = a"
+    using div_mult_mod_eq [of a b] by simp
+  finally show ?thesis .
+qed
+
+lemma dvd_mod_imp_dvd:
+  assumes "c dvd a mod b" and "c dvd b"
+  shows "c dvd a"
+  using assms dvd_mod_iff [of c b a] by simp
+
+end
+
+class idom_modulo = idom + semidom_modulo
+begin
+
+subclass idom_divide ..
+
+lemma div_diff [simp]:
+  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
+  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
+
+end
+
+
 class ordered_semiring = semiring + ordered_comm_monoid_add +
   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"