# HG changeset patch
# User haftmann
# Date 1507494501 -7200
# Node ID a4e82b58d8336c3a0b434724927c7c71b28864a7
# Parent  274b4edca85954b0f5ffcdb14276747dc1eb835a
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel

diff -r 274b4edca859 -r a4e82b58d833 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Binomial.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -1011,7 +1011,7 @@
   by (subst binomial_fact_lemma [symmetric]) auto
 
 lemma choose_dvd:
-  "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd (fact n :: 'a::{semiring_div,linordered_semidom})"
+  "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd (fact n :: 'a::linordered_semidom)"
   unfolding dvd_def
   apply (rule exI [where x="of_nat (n choose k)"])
   using binomial_fact_lemma [of k n, THEN arg_cong [where f = of_nat and 'b='a]]
@@ -1019,7 +1019,7 @@
   done
 
 lemma fact_fact_dvd_fact:
-  "fact k * fact n dvd (fact (k + n) :: 'a::{semiring_div,linordered_semidom})"
+  "fact k * fact n dvd (fact (k + n) :: 'a::linordered_semidom)"
   by (metis add.commute add_diff_cancel_left' choose_dvd le_add2)
 
 lemma choose_mult_lemma:
diff -r 274b4edca859 -r a4e82b58d833 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -247,7 +247,7 @@
 
 end
 
-instantiation integer :: ring_div
+instantiation integer :: unique_euclidean_ring
 begin
   
 lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
@@ -256,12 +256,33 @@
 
 declare modulo_integer.rep_eq [simp]
 
+lift_definition euclidean_size_integer :: "integer \<Rightarrow> nat"
+  is "euclidean_size :: int \<Rightarrow> nat"
+  .
+
+declare euclidean_size_integer.rep_eq [simp]
+
+lift_definition uniqueness_constraint_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+  is "uniqueness_constraint :: int \<Rightarrow> int \<Rightarrow> bool"
+  .
+
+declare uniqueness_constraint_integer.rep_eq [simp]
+
 instance
-  by (standard; transfer) simp_all
+  by (standard; transfer)
+    (use mult_le_mono2 [of 1] in \<open>auto simp add: sgn_mult_abs abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>, rule div_eqI, simp_all)
 
 end
 
-instantiation integer :: semiring_numeral_div
+lemma [code]:
+  "euclidean_size = nat_of_integer \<circ> abs"
+  by (simp add: fun_eq_iff nat_of_integer.rep_eq)
+
+lemma [code]:
+  "uniqueness_constraint (k :: integer) l \<longleftrightarrow> unit_factor k = unit_factor l"
+  by (simp add: integer_eq_iff)
+
+instantiation integer :: unique_euclidean_semiring_numeral
 begin
 
 definition divmod_integer :: "num \<Rightarrow> num \<Rightarrow> integer \<times> integer"
@@ -283,15 +304,15 @@
     by (fact divmod_step_integer_def)
 qed (transfer,
   fact le_add_diff_inverse2
-  semiring_numeral_div_class.div_less
-  semiring_numeral_div_class.mod_less
-  semiring_numeral_div_class.div_positive
-  semiring_numeral_div_class.mod_less_eq_dividend
-  semiring_numeral_div_class.pos_mod_bound
-  semiring_numeral_div_class.pos_mod_sign
-  semiring_numeral_div_class.mod_mult2_eq
-  semiring_numeral_div_class.div_mult2_eq
-  semiring_numeral_div_class.discrete)+
+  unique_euclidean_semiring_numeral_class.div_less
+  unique_euclidean_semiring_numeral_class.mod_less
+  unique_euclidean_semiring_numeral_class.div_positive
+  unique_euclidean_semiring_numeral_class.mod_less_eq_dividend
+  unique_euclidean_semiring_numeral_class.pos_mod_bound
+  unique_euclidean_semiring_numeral_class.pos_mod_sign
+  unique_euclidean_semiring_numeral_class.mod_mult2_eq
+  unique_euclidean_semiring_numeral_class.div_mult2_eq
+  unique_euclidean_semiring_numeral_class.discrete)+
 
 end
 
@@ -853,7 +874,7 @@
   "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
   by transfer rule
 
-instantiation natural :: "{semiring_div, normalization_semidom}"
+instantiation natural :: unique_euclidean_semiring
 begin
 
 lift_definition normalize_natural :: "natural \<Rightarrow> natural"
@@ -880,11 +901,32 @@
 
 declare modulo_natural.rep_eq [simp]
 
+lift_definition euclidean_size_natural :: "natural \<Rightarrow> nat"
+  is "euclidean_size :: nat \<Rightarrow> nat"
+  .
+
+declare euclidean_size_natural.rep_eq [simp]
+
+lift_definition uniqueness_constraint_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+  is "uniqueness_constraint :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  .
+
+declare uniqueness_constraint_natural.rep_eq [simp]
+
 instance
-  by standard (transfer, auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)+
+  by (standard; transfer)
+    (auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)
 
 end
 
+lemma [code]:
+  "euclidean_size = nat_of_natural"
+  by (simp add: fun_eq_iff)
+
+lemma [code]:
+  "uniqueness_constraint = (\<top> :: natural \<Rightarrow> natural \<Rightarrow> bool)"
+  by (simp add: fun_eq_iff)
+
 lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
   is "nat :: int \<Rightarrow> nat"
   .
diff -r 274b4edca859 -r a4e82b58d833 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -1181,7 +1181,7 @@
 
 end
 
-instantiation fps :: (field) ring_div
+instantiation fps :: (field) idom_modulo
 begin
 
 definition fps_mod_def:
@@ -1224,39 +1224,6 @@
   from assms show "f mod g = 0" by (intro fps_mod_eq_zero) auto
 qed
 
-context
-begin
-private lemma fps_divide_cancel_aux1:
-  assumes "h$0 \<noteq> (0 :: 'a :: field)"
-  shows   "(h * f) div (h * g) = f div g"
-proof (cases "g = 0")
-  assume "g \<noteq> 0"
-  from assms have "h \<noteq> 0" by auto
-  note nz [simp] = \<open>g \<noteq> 0\<close> \<open>h \<noteq> 0\<close>
-  from assms have [simp]: "subdegree h = 0" by (simp add: subdegree_eq_0_iff)
-
-  have "(h * f) div (h * g) =
-          fps_shift (subdegree g) (h * f * inverse (fps_shift (subdegree g) (h*g)))"
-    by (simp add: fps_divide_def Let_def)
-  also have "h * f * inverse (fps_shift (subdegree g) (h*g)) =
-               (inverse h * h) * f * inverse (fps_shift (subdegree g) g)"
-    by (subst fps_shift_mult) (simp_all add: algebra_simps fps_inverse_mult)
-  also from assms have "inverse h * h = 1" by (rule inverse_mult_eq_1)
-  finally show "(h * f) div (h * g) = f div g" by (simp_all add: fps_divide_def Let_def)
-qed (simp_all add: fps_divide_def)
-
-private lemma fps_divide_cancel_aux2:
-  "(f * fps_X^m) div (g * fps_X^m) = f div (g :: 'a :: field fps)"
-proof (cases "g = 0")
-  assume [simp]: "g \<noteq> 0"
-  have "(f * fps_X^m) div (g * fps_X^m) =
-          fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*fps_X^m))*fps_X^m)"
-    by (simp add: fps_divide_def Let_def algebra_simps)
-  also have "... = f div g"
-    by (simp add: fps_shift_times_fps_X_power'' fps_divide_def Let_def)
-  finally show ?thesis .
-qed (simp_all add: fps_divide_def)
-
 instance proof
   fix f g :: "'a fps"
   define n where "n = subdegree g"
@@ -1284,39 +1251,9 @@
       finally show ?thesis by simp
     qed
   qed (auto simp: fps_mod_def fps_divide_def Let_def)
-next
-
-  fix f g h :: "'a fps"
-  assume "h \<noteq> 0"
-  show "(h * f) div (h * g) = f div g"
-  proof -
-    define m where "m = subdegree h"
-    define h' where "h' = fps_shift m h"
-    have h_decomp: "h = h' * fps_X ^ m" unfolding h'_def m_def by (rule subdegree_decompose)
-    from \<open>h \<noteq> 0\<close> have [simp]: "h'$0 \<noteq> 0" by (simp add: h'_def m_def)
-    have "(h * f) div (h * g) = (h' * f * fps_X^m) div (h' * g * fps_X^m)"
-      by (simp add: h_decomp algebra_simps)
-    also have "... = f div g" by (simp add: fps_divide_cancel_aux1 fps_divide_cancel_aux2)
-    finally show ?thesis .
-  qed
-
-next
-  fix f g h :: "'a fps"
-  assume [simp]: "h \<noteq> 0"
-  define n h' where dfs: "n = subdegree h" "h' = fps_shift n h"
-  have "(f + g * h) div h = fps_shift n (f * inverse h') + fps_shift n (g * (h * inverse h'))"
-    by (simp add: fps_divide_def Let_def dfs[symmetric] algebra_simps fps_shift_add)
-  also have "h * inverse h' = (inverse h' * h') * fps_X^n"
-    by (subst subdegree_decompose) (simp_all add: dfs)
-  also have "... = fps_X^n" by (subst inverse_mult_eq_1) (simp_all add: dfs)
-  also have "fps_shift n (g * fps_X^n) = g" by simp
-  also have "fps_shift n (f * inverse h') = f div h"
-    by (simp add: fps_divide_def Let_def dfs)
-  finally show "(f + g * h) div h = g + f div h" by simp
 qed
 
 end
-end
 
 lemma subdegree_mod:
   assumes "f \<noteq> 0" "subdegree f < subdegree g"
@@ -1411,6 +1348,40 @@
 definition fps_euclidean_size_def:
   "euclidean_size f = (if f = 0 then 0 else 2 ^ subdegree f)"
 
+context
+begin
+
+private lemma fps_divide_cancel_aux1:
+  assumes "h$0 \<noteq> (0 :: 'a :: field)"
+  shows   "(h * f) div (h * g) = f div g"
+proof (cases "g = 0")
+  assume "g \<noteq> 0"
+  from assms have "h \<noteq> 0" by auto
+  note nz [simp] = \<open>g \<noteq> 0\<close> \<open>h \<noteq> 0\<close>
+  from assms have [simp]: "subdegree h = 0" by (simp add: subdegree_eq_0_iff)
+
+  have "(h * f) div (h * g) =
+          fps_shift (subdegree g) (h * f * inverse (fps_shift (subdegree g) (h*g)))"
+    by (simp add: fps_divide_def Let_def)
+  also have "h * f * inverse (fps_shift (subdegree g) (h*g)) =
+               (inverse h * h) * f * inverse (fps_shift (subdegree g) g)"
+    by (subst fps_shift_mult) (simp_all add: algebra_simps fps_inverse_mult)
+  also from assms have "inverse h * h = 1" by (rule inverse_mult_eq_1)
+  finally show "(h * f) div (h * g) = f div g" by (simp_all add: fps_divide_def Let_def)
+qed (simp_all add: fps_divide_def)
+
+private lemma fps_divide_cancel_aux2:
+  "(f * fps_X^m) div (g * fps_X^m) = f div (g :: 'a :: field fps)"
+proof (cases "g = 0")
+  assume [simp]: "g \<noteq> 0"
+  have "(f * fps_X^m) div (g * fps_X^m) =
+          fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*fps_X^m))*fps_X^m)"
+    by (simp add: fps_divide_def Let_def algebra_simps)
+  also have "... = f div g"
+    by (simp add: fps_shift_times_fps_X_power'' fps_divide_def Let_def)
+  finally show ?thesis .
+qed (simp_all add: fps_divide_def)
+
 instance proof
   fix f g :: "'a fps" assume [simp]: "g \<noteq> 0"
   show "euclidean_size f \<le> euclidean_size (f * g)"
@@ -1420,10 +1391,40 @@
     apply (rule disjE[OF le_less_linear[of "subdegree g" "subdegree f"]])
     apply (simp_all add: fps_mod_eq_zero fps_euclidean_size_def subdegree_mod)
     done
+  show "(h * f) div (h * g) = f div g" if "h \<noteq> 0"
+    for f g h :: "'a fps"
+  proof -
+    define m where "m = subdegree h"
+    define h' where "h' = fps_shift m h"
+    have h_decomp: "h = h' * fps_X ^ m" unfolding h'_def m_def by (rule subdegree_decompose)
+    from \<open>h \<noteq> 0\<close> have [simp]: "h'$0 \<noteq> 0" by (simp add: h'_def m_def)
+    have "(h * f) div (h * g) = (h' * f * fps_X^m) div (h' * g * fps_X^m)"
+      by (simp add: h_decomp algebra_simps)
+    also have "... = f div g"
+      by (simp add: fps_divide_cancel_aux1 fps_divide_cancel_aux2)
+    finally show ?thesis .
+  qed
+  show "(f + g * h) div h = g + f div h"
+    if "h \<noteq> 0" for f g h :: "'a fps"
+  proof -
+    define n h' where dfs: "n = subdegree h" "h' = fps_shift n h"
+    have "(f + g * h) div h = fps_shift n (f * inverse h') + fps_shift n (g * (h * inverse h'))"
+      by (simp add: fps_divide_def Let_def dfs [symmetric] algebra_simps fps_shift_add that)
+    also have "h * inverse h' = (inverse h' * h') * fps_X^n"
+      by (subst subdegree_decompose) (simp_all add: dfs)
+    also have "... = fps_X^n"
+      by (subst inverse_mult_eq_1) (simp_all add: dfs that)
+    also have "fps_shift n (g * fps_X^n) = g" by simp
+    also have "fps_shift n (f * inverse h') = f div h"
+      by (simp add: fps_divide_def Let_def dfs)
+    finally show ?thesis by simp
+  qed
 qed (simp_all add: fps_euclidean_size_def)
 
 end
 
+end
+
 instantiation fps :: (field) euclidean_ring_gcd
 begin
 definition fps_gcd_def: "(gcd :: 'a fps \<Rightarrow> _) = Euclidean_Algorithm.gcd"
diff -r 274b4edca859 -r a4e82b58d833 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -3637,40 +3637,7 @@
   for x :: "'a::field poly"
   by (rule eucl_rel_poly_unique_mod [OF eucl_rel_poly])
 
-instance poly :: (field) ring_div
-proof
-  fix x y z :: "'a poly"
-  assume "y \<noteq> 0"
-  with eucl_rel_poly [of x y] have "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)"
-    by (simp add: eucl_rel_poly_iff distrib_right)
-  then show "(x + z * y) div y = z + x div y"
-    by (rule div_poly_eq)
-next
-  fix x y z :: "'a poly"
-  assume "x \<noteq> 0"
-  show "(x * y) div (x * z) = y div z"
-  proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
-    have "\<And>x::'a poly. eucl_rel_poly x 0 (0, x)"
-      by (rule eucl_rel_poly_by_0)
-    then have [simp]: "\<And>x::'a poly. x div 0 = 0"
-      by (rule div_poly_eq)
-    have "\<And>x::'a poly. eucl_rel_poly 0 x (0, 0)"
-      by (rule eucl_rel_poly_0)
-    then have [simp]: "\<And>x::'a poly. 0 div x = 0"
-      by (rule div_poly_eq)
-    case False
-    then show ?thesis by auto
-  next
-    case True
-    then have "y \<noteq> 0" and "z \<noteq> 0" by auto
-    with \<open>x \<noteq> 0\<close> have "\<And>q r. eucl_rel_poly y z (q, r) \<Longrightarrow> eucl_rel_poly (x * y) (x * z) (q, x * r)"
-      by (auto simp: eucl_rel_poly_iff algebra_simps) (rule classical, simp add: degree_mult_eq)
-    moreover from eucl_rel_poly have "eucl_rel_poly y z (y div z, y mod z)" .
-    ultimately have "eucl_rel_poly (x * y) (x * z) (y div z, x * (y mod z))" .
-    then show ?thesis
-      by (simp add: div_poly_eq)
-  qed
-qed
+instance poly :: (field) idom_modulo ..
 
 lemma div_pCons_eq:
   "pCons a p div q =
diff -r 274b4edca859 -r a4e82b58d833 src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -459,11 +459,17 @@
     ultimately show "(if p * s = 0 then (0::nat) else 2 ^ degree (p * s)) < (if q * s = 0 then 0 else 2 ^ degree (q * s))"
       by (auto simp add: degree_mult_eq)
   next
-    fix p q r :: "'a poly" assume "p \<noteq> 0"
+    fix p q r :: "'a poly"
+    assume "p \<noteq> 0"
+    with eucl_rel_poly [of r p] have "eucl_rel_poly (r + q * p) p (q + r div p, r mod p)"
+      by (simp add: eucl_rel_poly_iff distrib_right)
+    then have "(r + q * p) div p = q + r div p"
+      by (rule div_poly_eq)
     moreover assume "(if r = 0 then (0::nat) else 2 ^ degree r)
-    < (if p = 0 then 0 else 2 ^ degree p)"
+      < (if p = 0 then 0 else 2 ^ degree p)"
     ultimately show "(q * p + r) div p = q"
-      by (cases "r = 0") (auto simp add: div_poly_less)
+      using \<open>p \<noteq> 0\<close>
+      by (cases "r = 0") (simp_all add: div_poly_less ac_simps)
   qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
 qed
 
@@ -761,9 +767,18 @@
 definition uniqueness_constraint_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
   where [simp]: "uniqueness_constraint_poly = top"
 
-instance 
-  by standard
-   (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq intro!: degree_mod_less' degree_mult_right_le
+instance proof
+  show "(q * p + r) div p = q" if "p \<noteq> 0"
+    and "euclidean_size r < euclidean_size p" for q p r :: "'a poly"
+  proof -
+    from \<open>p \<noteq> 0\<close> eucl_rel_poly [of r p] have "eucl_rel_poly (r + q * p) p (q + r div p, r mod p)"
+      by (simp add: eucl_rel_poly_iff distrib_right)
+    then have "(r + q * p) div p = q + r div p"
+      by (rule div_poly_eq)
+    with that show ?thesis
+      by (cases "r = 0") (simp_all add: euclidean_size_poly_def div_poly_less ac_simps)
+  qed
+qed (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq intro!: degree_mod_less' degree_mult_right_le
     split: if_splits)
 
 end
diff -r 274b4edca859 -r a4e82b58d833 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -9,433 +9,9 @@
 imports Parity
 begin
 
-subsection \<open>Quotient and remainder in integral domains with additional properties\<close>
-
-class semiring_div = semidom_modulo +
-  assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
-    and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
-begin
-
-lemma div_mult_self2 [simp]:
-  assumes "b \<noteq> 0"
-  shows "(a + b * c) div b = c + a div b"
-  using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
-
-lemma div_mult_self3 [simp]:
-  assumes "b \<noteq> 0"
-  shows "(c * b + a) div b = c + a div b"
-  using assms by (simp add: add.commute)
-
-lemma div_mult_self4 [simp]:
-  assumes "b \<noteq> 0"
-  shows "(b * c + a) div b = c + a div b"
-  using assms by (simp add: add.commute)
-
-lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
-proof (cases "b = 0")
-  case True then show ?thesis by simp
-next
-  case False
-  have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
-    by (simp add: div_mult_mod_eq)
-  also from False div_mult_self1 [of b a c] have
-    "\<dots> = (c + a div b) * b + (a + c * b) mod b"
-      by (simp add: algebra_simps)
-  finally have "a = a div b * b + (a + c * b) mod b"
-    by (simp add: add.commute [of a] add.assoc distrib_right)
-  then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
-    by (simp add: div_mult_mod_eq)
-  then show ?thesis by simp
-qed
-
-lemma mod_mult_self2 [simp]:
-  "(a + b * c) mod b = a mod b"
-  by (simp add: mult.commute [of b])
-
-lemma mod_mult_self3 [simp]:
-  "(c * b + a) mod b = a mod b"
-  by (simp add: add.commute)
-
-lemma mod_mult_self4 [simp]:
-  "(b * c + a) mod b = a mod b"
-  by (simp add: add.commute)
-
-lemma mod_mult_self1_is_0 [simp]:
-  "b * a mod b = 0"
-  using mod_mult_self2 [of 0 b a] by simp
-
-lemma mod_mult_self2_is_0 [simp]:
-  "a * b mod b = 0"
-  using mod_mult_self1 [of 0 a b] by simp
-
-lemma div_add_self1:
-  assumes "b \<noteq> 0"
-  shows "(b + a) div b = a div b + 1"
-  using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
-
-lemma div_add_self2:
-  assumes "b \<noteq> 0"
-  shows "(a + b) div b = a div b + 1"
-  using assms div_add_self1 [of b a] by (simp add: add.commute)
-
-lemma mod_add_self1 [simp]:
-  "(b + a) mod b = a mod b"
-  using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
-
-lemma mod_add_self2 [simp]:
-  "(a + b) mod b = a mod b"
-  using mod_mult_self1 [of a 1 b] by simp
-
-lemma mod_div_trivial [simp]:
-  "a mod b div b = 0"
-proof (cases "b = 0")
-  assume "b = 0"
-  thus ?thesis by simp
-next
-  assume "b \<noteq> 0"
-  hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
-    by (rule div_mult_self1 [symmetric])
-  also have "\<dots> = a div b"
-    by (simp only: mod_div_mult_eq)
-  also have "\<dots> = a div b + 0"
-    by simp
-  finally show ?thesis
-    by (rule add_left_imp_eq)
-qed
-
-lemma mod_mod_trivial [simp]:
-  "a mod b mod b = a mod b"
-proof -
-  have "a mod b mod b = (a mod b + a div b * b) mod b"
-    by (simp only: mod_mult_self1)
-  also have "\<dots> = a mod b"
-    by (simp only: mod_div_mult_eq)
-  finally show ?thesis .
-qed
-
-lemma mod_mod_cancel:
-  assumes "c dvd b"
-  shows "a mod b mod c = a mod c"
-proof -
-  from \<open>c dvd b\<close> obtain k where "b = c * k"
-    by (rule dvdE)
-  have "a mod b mod c = a mod (c * k) mod c"
-    by (simp only: \<open>b = c * k\<close>)
-  also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
-    by (simp only: mod_mult_self1)
-  also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
-    by (simp only: ac_simps)
-  also have "\<dots> = a mod c"
-    by (simp only: div_mult_mod_eq)
-  finally show ?thesis .
-qed
-
-lemma div_mult_mult2 [simp]:
-  "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
-  by (drule div_mult_mult1) (simp add: mult.commute)
-
-lemma div_mult_mult1_if [simp]:
-  "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
-  by simp_all
-
-lemma mod_mult_mult1:
-  "(c * a) mod (c * b) = c * (a mod b)"
-proof (cases "c = 0")
-  case True then show ?thesis by simp
-next
-  case False
-  from div_mult_mod_eq
-  have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
-  with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
-    = c * a + c * (a mod b)" by (simp add: algebra_simps)
-  with div_mult_mod_eq show ?thesis by simp
-qed
-
-lemma mod_mult_mult2:
-  "(a * c) mod (b * c) = (a mod b) * c"
-  using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
-
-lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
-  by (fact mod_mult_mult2 [symmetric])
-
-lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
-  by (fact mod_mult_mult1 [symmetric])
-
-lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
-  unfolding dvd_def by (auto simp add: mod_mult_mult1)
-
-lemma div_plus_div_distrib_dvd_left:
-  "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
-  by (cases "c = 0") (auto elim: dvdE)
-
-lemma div_plus_div_distrib_dvd_right:
-  "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
-  using div_plus_div_distrib_dvd_left [of c b a]
-  by (simp add: ac_simps)
-
-named_theorems mod_simps
-
-text \<open>Addition respects modular equivalence.\<close>
-
-lemma mod_add_left_eq [mod_simps]:
-  "(a mod c + b) mod c = (a + b) mod c"
-proof -
-  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
-    by (simp only: div_mult_mod_eq)
-  also have "\<dots> = (a mod c + b + a div c * c) mod c"
-    by (simp only: ac_simps)
-  also have "\<dots> = (a mod c + b) mod c"
-    by (rule mod_mult_self1)
-  finally show ?thesis
-    by (rule sym)
-qed
-
-lemma mod_add_right_eq [mod_simps]:
-  "(a + b mod c) mod c = (a + b) mod c"
-  using mod_add_left_eq [of b c a] by (simp add: ac_simps)
-
-lemma mod_add_eq:
-  "(a mod c + b mod c) mod c = (a + b) mod c"
-  by (simp add: mod_add_left_eq mod_add_right_eq)
-
-lemma mod_sum_eq [mod_simps]:
-  "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
-proof (induct A rule: infinite_finite_induct)
-  case (insert i A)
-  then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
-    = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
-    by simp
-  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
-    by (simp add: mod_simps)
-  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
-    by (simp add: insert.hyps)
-  finally show ?case
-    by (simp add: insert.hyps mod_simps)
-qed simp_all
-
-lemma mod_add_cong:
-  assumes "a mod c = a' mod c"
-  assumes "b mod c = b' mod c"
-  shows "(a + b) mod c = (a' + b') mod c"
-proof -
-  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
-    unfolding assms ..
-  then show ?thesis
-    by (simp add: mod_add_eq)
-qed
-
-text \<open>Multiplication respects modular equivalence.\<close>
-
-lemma mod_mult_left_eq [mod_simps]:
-  "((a mod c) * b) mod c = (a * b) mod c"
-proof -
-  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
-    by (simp only: div_mult_mod_eq)
-  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
-    by (simp only: algebra_simps)
-  also have "\<dots> = (a mod c * b) mod c"
-    by (rule mod_mult_self1)
-  finally show ?thesis
-    by (rule sym)
-qed
-
-lemma mod_mult_right_eq [mod_simps]:
-  "(a * (b mod c)) mod c = (a * b) mod c"
-  using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
-
-lemma mod_mult_eq:
-  "((a mod c) * (b mod c)) mod c = (a * b) mod c"
-  by (simp add: mod_mult_left_eq mod_mult_right_eq)
-
-lemma mod_prod_eq [mod_simps]:
-  "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
-proof (induct A rule: infinite_finite_induct)
-  case (insert i A)
-  then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
-    = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
-    by simp
-  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
-    by (simp add: mod_simps)
-  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
-    by (simp add: insert.hyps)
-  finally show ?case
-    by (simp add: insert.hyps mod_simps)
-qed simp_all
-
-lemma mod_mult_cong:
-  assumes "a mod c = a' mod c"
-  assumes "b mod c = b' mod c"
-  shows "(a * b) mod c = (a' * b') mod c"
-proof -
-  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
-    unfolding assms ..
-  then show ?thesis
-    by (simp add: mod_mult_eq)
-qed
-
-text \<open>Exponentiation respects modular equivalence.\<close>
-
-lemma power_mod [mod_simps]: 
-  "((a mod b) ^ n) mod b = (a ^ n) mod b"
-proof (induct n)
-  case 0
-  then show ?case by simp
-next
-  case (Suc n)
-  have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
-    by (simp add: mod_mult_right_eq)
-  with Suc show ?case
-    by (simp add: mod_mult_left_eq mod_mult_right_eq)
-qed
-
-end
-
-class ring_div = comm_ring_1 + semiring_div
-begin
-
-subclass idom_divide ..
-
-lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
-  using div_mult_mult1 [of "- 1" a b] by simp
-
-lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
-  using mod_mult_mult1 [of "- 1" a b] by simp
-
-lemma div_minus_right: "a div (- b) = (- a) div b"
-  using div_minus_minus [of "- a" b] by simp
-
-lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
-  using mod_minus_minus [of "- a" b] by simp
-
-lemma div_minus1_right [simp]: "a div (- 1) = - a"
-  using div_minus_right [of a 1] by simp
-
-lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
-  using mod_minus_right [of a 1] by simp
-
-text \<open>Negation respects modular equivalence.\<close>
-
-lemma mod_minus_eq [mod_simps]:
-  "(- (a mod b)) mod b = (- a) mod b"
-proof -
-  have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
-    by (simp only: div_mult_mod_eq)
-  also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
-    by (simp add: ac_simps)
-  also have "\<dots> = (- (a mod b)) mod b"
-    by (rule mod_mult_self1)
-  finally show ?thesis
-    by (rule sym)
-qed
-
-lemma mod_minus_cong:
-  assumes "a mod b = a' mod b"
-  shows "(- a) mod b = (- a') mod b"
-proof -
-  have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
-    unfolding assms ..
-  then show ?thesis
-    by (simp add: mod_minus_eq)
-qed
-
-text \<open>Subtraction respects modular equivalence.\<close>
-
-lemma mod_diff_left_eq [mod_simps]:
-  "(a mod c - b) mod c = (a - b) mod c"
-  using mod_add_cong [of a c "a mod c" "- b" "- b"]
-  by simp
-
-lemma mod_diff_right_eq [mod_simps]:
-  "(a - b mod c) mod c = (a - b) mod c"
-  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
-  by simp
-
-lemma mod_diff_eq:
-  "(a mod c - b mod c) mod c = (a - b) mod c"
-  using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
-  by simp
-
-lemma mod_diff_cong:
-  assumes "a mod c = a' mod c"
-  assumes "b mod c = b' mod c"
-  shows "(a - b) mod c = (a' - b') mod c"
-  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
-  by simp
-
-lemma minus_mod_self2 [simp]:
-  "(a - b) mod b = a mod b"
-  using mod_diff_right_eq [of a b b]
-  by (simp add: mod_diff_right_eq)
-
-lemma minus_mod_self1 [simp]:
-  "(b - a) mod b = - a mod b"
-  using mod_add_self2 [of "- a" b] by simp
-
-end
-
-  
-subsection \<open>Euclidean (semi)rings with cancel rules\<close>
-
-class euclidean_semiring_cancel = euclidean_semiring + semiring_div
-
-class euclidean_ring_cancel = euclidean_ring + ring_div
-
-context unique_euclidean_semiring
-begin
-
-subclass euclidean_semiring_cancel
-proof
-  show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
-  proof (cases a b rule: divmod_cases)
-    case by0
-    with \<open>b \<noteq> 0\<close> show ?thesis
-      by simp
-  next
-    case (divides q)
-    then show ?thesis
-      by (simp add: ac_simps)
-  next
-    case (remainder q r)
-    then show ?thesis
-      by (auto intro: div_eqI simp add: algebra_simps)
-  qed
-next
-  show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
-  proof (cases a b rule: divmod_cases)
-    case by0
-    then show ?thesis
-      by simp
-  next
-    case (divides q)
-    with \<open>c \<noteq> 0\<close> show ?thesis
-      by (simp add: mult.left_commute [of c])
-  next
-    case (remainder q r)
-    from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
-      by simp
-    from remainder \<open>c \<noteq> 0\<close>
-    have "uniqueness_constraint (r * c) (b * c)"
-      and "euclidean_size (r * c) < euclidean_size (b * c)"
-      by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
-    with remainder show ?thesis
-      by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
-        (use \<open>b * c \<noteq> 0\<close> in simp)
-  qed
-qed
-
-end
-
-context unique_euclidean_ring
-begin
-
-subclass euclidean_ring_cancel ..
-
-end
-
-
 subsection \<open>Parity\<close>
 
-class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
+class unique_euclidean_semiring_parity = unique_euclidean_semiring +
   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
   assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
   assumes zero_not_eq_two: "0 \<noteq> 2"
@@ -532,7 +108,7 @@
   and less technical class hierarchy.
 \<close>
 
-class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom +
+class unique_euclidean_semiring_numeral = unique_euclidean_semiring + linordered_semidom +
   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
@@ -553,7 +129,7 @@
     yields a significant speedup.\<close>
 begin
 
-subclass semiring_div_parity
+subclass unique_euclidean_semiring_parity
 proof
   fix a
   show "a mod 2 = 0 \<or> a mod 2 = 1"
@@ -1050,58 +626,6 @@
 
 end
 
-instance nat :: semiring_div
-proof
-  fix m n q :: nat
-  assume "n \<noteq> 0"
-  then show "(q + m * n) div n = m + q div n"
-    by (induct m) (simp_all add: le_div_geq)
-next
-  fix m n q :: nat
-  assume "m \<noteq> 0"
-  show "(m * n) div (m * q) = n div q"
-  proof (cases "q = 0")
-    case True
-    then show ?thesis
-      by simp
-  next
-    case False
-    show ?thesis
-    proof (rule div_nat_unique [of _ _ _ "m * (n mod q)"])
-      show "eucl_rel_nat (m * n) (m * q) (n div q, m * (n mod q))"
-        by (rule eucl_rel_natI)
-          (use \<open>m \<noteq> 0\<close> \<open>q \<noteq> 0\<close> div_mult_mod_eq [of n q] in \<open>auto simp add: algebra_simps distrib_left [symmetric]\<close>)
-    qed          
-  qed
-qed
-
-lemma div_by_Suc_0 [simp]:
-  "m div Suc 0 = m"
-  using div_by_1 [of m] by simp
-
-lemma mod_by_Suc_0 [simp]:
-  "m mod Suc 0 = 0"
-  using mod_by_1 [of m] by simp
-
-lemma mod_greater_zero_iff_not_dvd:
-  fixes m n :: nat
-  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
-  by (simp add: dvd_eq_mod_eq_0)
-
-instantiation nat :: unique_euclidean_semiring
-begin
-
-definition [simp]:
-  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
-
-definition [simp]:
-  "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
-
-instance
-  by standard (use mult_le_mono2 [of 1] in \<open>simp_all add: unit_factor_nat_def mod_greater_zero_iff_not_dvd\<close>)
-
-end
-
 text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
 
 lemma (in semiring_modulo) cancel_div_mod_rules:
@@ -1142,6 +666,41 @@
 simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   \<open>K Cancel_Div_Mod_Nat.proc\<close>
 
+lemma div_by_Suc_0 [simp]:
+  "m div Suc 0 = m"
+  using div_by_1 [of m] by simp
+
+lemma mod_by_Suc_0 [simp]:
+  "m mod Suc 0 = 0"
+  using mod_by_1 [of m] by simp
+
+lemma mod_greater_zero_iff_not_dvd:
+  fixes m n :: nat
+  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
+  by (simp add: dvd_eq_mod_eq_0)
+
+instantiation nat :: unique_euclidean_semiring
+begin
+
+definition [simp]:
+  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
+
+definition [simp]:
+  "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+
+instance proof
+  fix n q r :: nat
+  assume "euclidean_size r < euclidean_size n"
+  then have "n > r"
+    by simp_all
+  then have "eucl_rel_nat (q * n + r) n (q, r)"
+    by (rule eucl_rel_natI) rule
+  then show "(q * n + r) div n = q"
+    by (rule div_nat_unique)
+qed (use mult_le_mono2 [of 1] in \<open>simp_all\<close>)
+
+end
+  
 lemma divmod_nat_if [code]:
   "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
     let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
@@ -1262,7 +821,7 @@
 lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
 by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
 
-instantiation nat :: semiring_numeral_div
+instantiation nat :: unique_euclidean_semiring_numeral
 begin
 
 definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
@@ -1820,6 +1379,25 @@
 
 end
 
+ML \<open>
+structure Cancel_Div_Mod_Int = Cancel_Div_Mod
+(
+  val div_name = @{const_name divide};
+  val mod_name = @{const_name modulo};
+  val mk_binop = HOLogic.mk_binop;
+  val mk_sum = Arith_Data.mk_sum HOLogic.intT;
+  val dest_sum = Arith_Data.dest_sum;
+
+  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
+
+  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
+    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
+)
+\<close>
+
+simproc_setup cancel_div_mod_int ("(k::int) + l") =
+  \<open>K Cancel_Div_Mod_Int.proc\<close>
+
 lemma is_unit_int:
   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
   by auto
@@ -1921,50 +1499,28 @@
   using assms unfolding modulo_int_def [of k l]
   by (auto simp add: not_less int_dvd_iff mod_greater_zero_iff_not_dvd elim: pos_int_cases neg_int_cases nonneg_int_cases nonpos_int_cases)
 
-instance int :: ring_div
-proof
-  fix k l s :: int
-  assume "l \<noteq> 0"
-  then have "eucl_rel_int (k + s * l) l (s + k div l, k mod l)"
-    using eucl_rel_int [of k l]
-    unfolding eucl_rel_int_iff by (auto simp: algebra_simps)
-  then show "(k + s * l) div l = s + k div l"
+instantiation int :: unique_euclidean_ring
+begin
+
+definition [simp]:
+  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
+
+definition [simp]:
+  "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
+  
+instance proof
+  fix l q r:: int
+  assume "uniqueness_constraint r l"
+    and "euclidean_size r < euclidean_size l"
+  then have "sgn r = sgn l" and "\<bar>r\<bar> < \<bar>l\<bar>"
+    by simp_all
+  then have "eucl_rel_int (q * l + r) l (q, r)"
+    by (rule eucl_rel_int_remainderI) simp
+  then show "(q * l + r) div l = q"
     by (rule div_int_unique)
-next
-  fix k l s :: int
-  assume "s \<noteq> 0"
-  have "\<And>q r. eucl_rel_int k l (q, r)
-    \<Longrightarrow> eucl_rel_int (s * k) (s * l) (q, s * r)"
-    unfolding eucl_rel_int_iff
-    by (rule linorder_cases [of 0 l])
-      (use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
-      mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
-      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
-  then have "eucl_rel_int (s * k) (s * l) (k div l, s * (k mod l))"
-    using eucl_rel_int [of k l] .
-  then show "(s * k) div (s * l) = k div l"
-    by (rule div_int_unique)
-qed
+qed (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
 
-ML \<open>
-structure Cancel_Div_Mod_Int = Cancel_Div_Mod
-(
-  val div_name = @{const_name divide};
-  val mod_name = @{const_name modulo};
-  val mk_binop = HOLogic.mk_binop;
-  val mk_sum = Arith_Data.mk_sum HOLogic.intT;
-  val dest_sum = Arith_Data.dest_sum;
-
-  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
-
-  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
-    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
-)
-\<close>
-
-simproc_setup cancel_div_mod_int ("(k::int) + l") =
-  \<open>K Cancel_Div_Mod_Int.proc\<close>
-
+end
 
 text\<open>Basic laws about division and remainder\<close>
 
@@ -2420,21 +1976,6 @@
     by simp
 qed
 
-instantiation int :: unique_euclidean_ring
-begin
-
-definition [simp]:
-  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
-
-definition [simp]:
-  "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
-  
-instance
-  by standard
-    (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult nat_mult_distrib sgn_mod zdiv_eq_0_iff sgn_1_pos sgn_mult split: abs_split\<close>)
-
-end
-
   
 subsubsection \<open>Quotients of Signs\<close>
 
@@ -2506,7 +2047,7 @@
 
 subsubsection \<open>Computation of Division and Remainder\<close>
 
-instantiation int :: semiring_numeral_div
+instantiation int :: unique_euclidean_semiring_numeral
 begin
 
 definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
@@ -2687,22 +2228,6 @@
 apply (rule Divides.div_less_dividend, simp_all)
 done
 
-lemma (in ring_div) mod_eq_dvd_iff:
-  "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
-proof
-  assume ?P
-  then have "(a mod c - b mod c) mod c = 0"
-    by simp
-  then show ?Q
-    by (simp add: dvd_eq_mod_eq_0 mod_simps)
-next
-  assume ?Q
-  then obtain d where d: "a - b = c * d" ..
-  then have "a = c * d + b"
-    by (simp add: algebra_simps)
-  then show ?P by simp
-qed
-
 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
   shows "\<exists>q. x = y + n * q"
 proof-
@@ -2742,23 +2267,23 @@
 \<close>
 
 simproc_setup numeral_divmod
-  ("0 div 0 :: 'a :: semiring_numeral_div" | "0 mod 0 :: 'a :: semiring_numeral_div" |
-   "0 div 1 :: 'a :: semiring_numeral_div" | "0 mod 1 :: 'a :: semiring_numeral_div" |
+  ("0 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
+   "0 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
    "0 div - 1 :: int" | "0 mod - 1 :: int" |
-   "0 div numeral b :: 'a :: semiring_numeral_div" | "0 mod numeral b :: 'a :: semiring_numeral_div" |
+   "0 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
    "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
-   "1 div 0 :: 'a :: semiring_numeral_div" | "1 mod 0 :: 'a :: semiring_numeral_div" |
-   "1 div 1 :: 'a :: semiring_numeral_div" | "1 mod 1 :: 'a :: semiring_numeral_div" |
+   "1 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
+   "1 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
    "1 div - 1 :: int" | "1 mod - 1 :: int" |
-   "1 div numeral b :: 'a :: semiring_numeral_div" | "1 mod numeral b :: 'a :: semiring_numeral_div" |
+   "1 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
    "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
    "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
    "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
    "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
-   "numeral a div 0 :: 'a :: semiring_numeral_div" | "numeral a mod 0 :: 'a :: semiring_numeral_div" |
-   "numeral a div 1 :: 'a :: semiring_numeral_div" | "numeral a mod 1 :: 'a :: semiring_numeral_div" |
+   "numeral a div 0 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
+   "numeral a div 1 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
    "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
-   "numeral a div numeral b :: 'a :: semiring_numeral_div" | "numeral a mod numeral b :: 'a :: semiring_numeral_div" |
+   "numeral a div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
    "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
    "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
    "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
@@ -2818,7 +2343,7 @@
   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 lemma dvd_eq_mod_eq_0_numeral:
-  "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
+  "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semidom_modulo)"
   by (fact dvd_eq_mod_eq_0)
 
 declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
diff -r 274b4edca859 -r a4e82b58d833 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Enum.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -683,7 +683,7 @@
 
 instance finite_2 :: complete_linorder ..
 
-instantiation finite_2 :: "{field, idom_abs_sgn}" begin
+instantiation finite_2 :: "{field, idom_abs_sgn, idom_modulo}" begin
 definition [simp]: "0 = a\<^sub>1"
 definition [simp]: "1 = a\<^sub>2"
 definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
@@ -692,12 +692,15 @@
 definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
 definition "inverse = (\<lambda>x :: finite_2. x)"
 definition "divide = (op * :: finite_2 \<Rightarrow> _)"
+definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
 definition "abs = (\<lambda>x :: finite_2. x)"
 definition "sgn = (\<lambda>x :: finite_2. x)"
 instance
   by standard
-    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
-      inverse_finite_2_def divide_finite_2_def abs_finite_2_def sgn_finite_2_def
+    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def
+      times_finite_2_def
+      inverse_finite_2_def divide_finite_2_def modulo_finite_2_def
+      abs_finite_2_def sgn_finite_2_def
       split: finite_2.splits)
 end
 
@@ -709,14 +712,15 @@
   "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> y = a\<^sub>1"
   by (auto simp add: dvd_def times_finite_2_def split: finite_2.splits)
 
-instantiation finite_2 :: "{ring_div, normalization_semidom}" begin
+instantiation finite_2 :: unique_euclidean_semiring begin
 definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
 definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
-definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
+definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | a\<^sub>2 \<Rightarrow> 1)"
+definition [simp]: "uniqueness_constraint = (\<top> :: finite_2 \<Rightarrow> _)"
 instance
   by standard
-    (simp_all add: dvd_finite_2_unfold times_finite_2_def
-      divide_finite_2_def modulo_finite_2_def split: finite_2.splits)
+    (auto simp add: divide_finite_2_def times_finite_2_def dvd_finite_2_unfold
+    split: finite_2.splits)
 end
 
  
@@ -826,7 +830,7 @@
 
 instance finite_3 :: complete_linorder ..
 
-instantiation finite_3 :: "{field, idom_abs_sgn}" begin
+instantiation finite_3 :: "{field, idom_abs_sgn, idom_modulo}" begin
 definition [simp]: "0 = a\<^sub>1"
 definition [simp]: "1 = a\<^sub>2"
 definition
@@ -839,12 +843,15 @@
 definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>3) \<Rightarrow> a\<^sub>2 | (a\<^sub>2, a\<^sub>3) \<Rightarrow> a\<^sub>3 | (a\<^sub>3, a\<^sub>2) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
 definition "inverse = (\<lambda>x :: finite_3. x)" 
 definition "x div y = x * inverse (y :: finite_3)"
+definition "x mod y = (case y of a\<^sub>1 \<Rightarrow> x | _ \<Rightarrow> a\<^sub>1)"
 definition "abs = (\<lambda>x. case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
 definition "sgn = (\<lambda>x :: finite_3. x)"
 instance
   by standard
-    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
-      inverse_finite_3_def divide_finite_3_def abs_finite_3_def sgn_finite_3_def
+    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def
+      times_finite_3_def
+      inverse_finite_3_def divide_finite_3_def modulo_finite_3_def
+      abs_finite_3_def sgn_finite_3_def
       less_finite_3_def
       split: finite_3.splits)
 end
@@ -857,20 +864,21 @@
   "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> x = a\<^sub>3 \<or> y = a\<^sub>1"
   by (cases x) (auto simp add: dvd_def times_finite_3_def split: finite_3.splits)
 
-instantiation finite_3 :: "{ring_div, normalization_semidom}" begin
-definition "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
+instantiation finite_3 :: unique_euclidean_semiring begin
+definition [simp]: "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
 definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
-definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
-instance
-  by standard
-    (auto simp add: finite_3_not_eq_unfold plus_finite_3_def
-      dvd_finite_3_unfold times_finite_3_def inverse_finite_3_def
-      normalize_finite_3_def divide_finite_3_def modulo_finite_3_def
-      split: finite_3.splits)
+definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | _ \<Rightarrow> 1)"
+definition [simp]: "uniqueness_constraint = (\<top> :: finite_3 \<Rightarrow> _)"
+instance proof
+  fix x :: finite_3
+  assume "x \<noteq> 0"
+  then show "is_unit (unit_factor x)"
+    by (cases x) (simp_all add: dvd_finite_3_unfold)
+qed (auto simp add: divide_finite_3_def times_finite_3_def
+  dvd_finite_3_unfold inverse_finite_3_def plus_finite_3_def
+  split: finite_3.splits)
 end
 
-
-
 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
 
 datatype (plugins only: code "quickcheck" extraction) finite_4 =
diff -r 274b4edca859 -r a4e82b58d833 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
@@ -201,6 +201,388 @@
 class euclidean_ring = idom_modulo + euclidean_semiring
 
   
+subsection \<open>Euclidean (semi)rings with cancel rules\<close>
+
+class euclidean_semiring_cancel = euclidean_semiring +
+  assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
+  and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
+begin
+
+lemma div_mult_self2 [simp]:
+  assumes "b \<noteq> 0"
+  shows "(a + b * c) div b = c + a div b"
+  using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
+
+lemma div_mult_self3 [simp]:
+  assumes "b \<noteq> 0"
+  shows "(c * b + a) div b = c + a div b"
+  using assms by (simp add: add.commute)
+
+lemma div_mult_self4 [simp]:
+  assumes "b \<noteq> 0"
+  shows "(b * c + a) div b = c + a div b"
+  using assms by (simp add: add.commute)
+
+lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
+proof (cases "b = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
+    by (simp add: div_mult_mod_eq)
+  also from False div_mult_self1 [of b a c] have
+    "\<dots> = (c + a div b) * b + (a + c * b) mod b"
+      by (simp add: algebra_simps)
+  finally have "a = a div b * b + (a + c * b) mod b"
+    by (simp add: add.commute [of a] add.assoc distrib_right)
+  then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
+    by (simp add: div_mult_mod_eq)
+  then show ?thesis by simp
+qed
+
+lemma mod_mult_self2 [simp]:
+  "(a + b * c) mod b = a mod b"
+  by (simp add: mult.commute [of b])
+
+lemma mod_mult_self3 [simp]:
+  "(c * b + a) mod b = a mod b"
+  by (simp add: add.commute)
+
+lemma mod_mult_self4 [simp]:
+  "(b * c + a) mod b = a mod b"
+  by (simp add: add.commute)
+
+lemma mod_mult_self1_is_0 [simp]:
+  "b * a mod b = 0"
+  using mod_mult_self2 [of 0 b a] by simp
+
+lemma mod_mult_self2_is_0 [simp]:
+  "a * b mod b = 0"
+  using mod_mult_self1 [of 0 a b] by simp
+
+lemma div_add_self1:
+  assumes "b \<noteq> 0"
+  shows "(b + a) div b = a div b + 1"
+  using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
+
+lemma div_add_self2:
+  assumes "b \<noteq> 0"
+  shows "(a + b) div b = a div b + 1"
+  using assms div_add_self1 [of b a] by (simp add: add.commute)
+
+lemma mod_add_self1 [simp]:
+  "(b + a) mod b = a mod b"
+  using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
+
+lemma mod_add_self2 [simp]:
+  "(a + b) mod b = a mod b"
+  using mod_mult_self1 [of a 1 b] by simp
+
+lemma mod_div_trivial [simp]:
+  "a mod b div b = 0"
+proof (cases "b = 0")
+  assume "b = 0"
+  thus ?thesis by simp
+next
+  assume "b \<noteq> 0"
+  hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
+    by (rule div_mult_self1 [symmetric])
+  also have "\<dots> = a div b"
+    by (simp only: mod_div_mult_eq)
+  also have "\<dots> = a div b + 0"
+    by simp
+  finally show ?thesis
+    by (rule add_left_imp_eq)
+qed
+
+lemma mod_mod_trivial [simp]:
+  "a mod b mod b = a mod b"
+proof -
+  have "a mod b mod b = (a mod b + a div b * b) mod b"
+    by (simp only: mod_mult_self1)
+  also have "\<dots> = a mod b"
+    by (simp only: mod_div_mult_eq)
+  finally show ?thesis .
+qed
+
+lemma mod_mod_cancel:
+  assumes "c dvd b"
+  shows "a mod b mod c = a mod c"
+proof -
+  from \<open>c dvd b\<close> obtain k where "b = c * k"
+    by (rule dvdE)
+  have "a mod b mod c = a mod (c * k) mod c"
+    by (simp only: \<open>b = c * k\<close>)
+  also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
+    by (simp only: mod_mult_self1)
+  also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
+    by (simp only: ac_simps)
+  also have "\<dots> = a mod c"
+    by (simp only: div_mult_mod_eq)
+  finally show ?thesis .
+qed
+
+lemma div_mult_mult2 [simp]:
+  "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
+  by (drule div_mult_mult1) (simp add: mult.commute)
+
+lemma div_mult_mult1_if [simp]:
+  "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
+  by simp_all
+
+lemma mod_mult_mult1:
+  "(c * a) mod (c * b) = c * (a mod b)"
+proof (cases "c = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  from div_mult_mod_eq
+  have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
+  with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
+    = c * a + c * (a mod b)" by (simp add: algebra_simps)
+  with div_mult_mod_eq show ?thesis by simp
+qed
+
+lemma mod_mult_mult2:
+  "(a * c) mod (b * c) = (a mod b) * c"
+  using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
+
+lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
+  by (fact mod_mult_mult2 [symmetric])
+
+lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
+  by (fact mod_mult_mult1 [symmetric])
+
+lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
+  unfolding dvd_def by (auto simp add: mod_mult_mult1)
+
+lemma div_plus_div_distrib_dvd_left:
+  "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
+  by (cases "c = 0") (auto elim: dvdE)
+
+lemma div_plus_div_distrib_dvd_right:
+  "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
+  using div_plus_div_distrib_dvd_left [of c b a]
+  by (simp add: ac_simps)
+
+named_theorems mod_simps
+
+text \<open>Addition respects modular equivalence.\<close>
+
+lemma mod_add_left_eq [mod_simps]:
+  "(a mod c + b) mod c = (a + b) mod c"
+proof -
+  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
+    by (simp only: div_mult_mod_eq)
+  also have "\<dots> = (a mod c + b + a div c * c) mod c"
+    by (simp only: ac_simps)
+  also have "\<dots> = (a mod c + b) mod c"
+    by (rule mod_mult_self1)
+  finally show ?thesis
+    by (rule sym)
+qed
+
+lemma mod_add_right_eq [mod_simps]:
+  "(a + b mod c) mod c = (a + b) mod c"
+  using mod_add_left_eq [of b c a] by (simp add: ac_simps)
+
+lemma mod_add_eq:
+  "(a mod c + b mod c) mod c = (a + b) mod c"
+  by (simp add: mod_add_left_eq mod_add_right_eq)
+
+lemma mod_sum_eq [mod_simps]:
+  "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
+proof (induct A rule: infinite_finite_induct)
+  case (insert i A)
+  then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
+    = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
+    by simp
+  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
+    by (simp add: mod_simps)
+  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
+    by (simp add: insert.hyps)
+  finally show ?case
+    by (simp add: insert.hyps mod_simps)
+qed simp_all
+
+lemma mod_add_cong:
+  assumes "a mod c = a' mod c"
+  assumes "b mod c = b' mod c"
+  shows "(a + b) mod c = (a' + b') mod c"
+proof -
+  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
+    unfolding assms ..
+  then show ?thesis
+    by (simp add: mod_add_eq)
+qed
+
+text \<open>Multiplication respects modular equivalence.\<close>
+
+lemma mod_mult_left_eq [mod_simps]:
+  "((a mod c) * b) mod c = (a * b) mod c"
+proof -
+  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
+    by (simp only: div_mult_mod_eq)
+  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
+    by (simp only: algebra_simps)
+  also have "\<dots> = (a mod c * b) mod c"
+    by (rule mod_mult_self1)
+  finally show ?thesis
+    by (rule sym)
+qed
+
+lemma mod_mult_right_eq [mod_simps]:
+  "(a * (b mod c)) mod c = (a * b) mod c"
+  using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
+
+lemma mod_mult_eq:
+  "((a mod c) * (b mod c)) mod c = (a * b) mod c"
+  by (simp add: mod_mult_left_eq mod_mult_right_eq)
+
+lemma mod_prod_eq [mod_simps]:
+  "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
+proof (induct A rule: infinite_finite_induct)
+  case (insert i A)
+  then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
+    = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
+    by simp
+  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
+    by (simp add: mod_simps)
+  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
+    by (simp add: insert.hyps)
+  finally show ?case
+    by (simp add: insert.hyps mod_simps)
+qed simp_all
+
+lemma mod_mult_cong:
+  assumes "a mod c = a' mod c"
+  assumes "b mod c = b' mod c"
+  shows "(a * b) mod c = (a' * b') mod c"
+proof -
+  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
+    unfolding assms ..
+  then show ?thesis
+    by (simp add: mod_mult_eq)
+qed
+
+text \<open>Exponentiation respects modular equivalence.\<close>
+
+lemma power_mod [mod_simps]: 
+  "((a mod b) ^ n) mod b = (a ^ n) mod b"
+proof (induct n)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
+    by (simp add: mod_mult_right_eq)
+  with Suc show ?case
+    by (simp add: mod_mult_left_eq mod_mult_right_eq)
+qed
+
+end
+
+
+class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel
+begin
+
+subclass idom_divide ..
+
+lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
+  using div_mult_mult1 [of "- 1" a b] by simp
+
+lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
+  using mod_mult_mult1 [of "- 1" a b] by simp
+
+lemma div_minus_right: "a div (- b) = (- a) div b"
+  using div_minus_minus [of "- a" b] by simp
+
+lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
+  using mod_minus_minus [of "- a" b] by simp
+
+lemma div_minus1_right [simp]: "a div (- 1) = - a"
+  using div_minus_right [of a 1] by simp
+
+lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
+  using mod_minus_right [of a 1] by simp
+
+text \<open>Negation respects modular equivalence.\<close>
+
+lemma mod_minus_eq [mod_simps]:
+  "(- (a mod b)) mod b = (- a) mod b"
+proof -
+  have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
+    by (simp only: div_mult_mod_eq)
+  also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
+    by (simp add: ac_simps)
+  also have "\<dots> = (- (a mod b)) mod b"
+    by (rule mod_mult_self1)
+  finally show ?thesis
+    by (rule sym)
+qed
+
+lemma mod_minus_cong:
+  assumes "a mod b = a' mod b"
+  shows "(- a) mod b = (- a') mod b"
+proof -
+  have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
+    unfolding assms ..
+  then show ?thesis
+    by (simp add: mod_minus_eq)
+qed
+
+text \<open>Subtraction respects modular equivalence.\<close>
+
+lemma mod_diff_left_eq [mod_simps]:
+  "(a mod c - b) mod c = (a - b) mod c"
+  using mod_add_cong [of a c "a mod c" "- b" "- b"]
+  by simp
+
+lemma mod_diff_right_eq [mod_simps]:
+  "(a - b mod c) mod c = (a - b) mod c"
+  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
+  by simp
+
+lemma mod_diff_eq:
+  "(a mod c - b mod c) mod c = (a - b) mod c"
+  using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
+  by simp
+
+lemma mod_diff_cong:
+  assumes "a mod c = a' mod c"
+  assumes "b mod c = b' mod c"
+  shows "(a - b) mod c = (a' - b') mod c"
+  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
+  by simp
+
+lemma minus_mod_self2 [simp]:
+  "(a - b) mod b = a mod b"
+  using mod_diff_right_eq [of a b b]
+  by (simp add: mod_diff_right_eq)
+
+lemma minus_mod_self1 [simp]:
+  "(b - a) mod b = - a mod b"
+  using mod_add_self2 [of "- a" b] by simp
+
+lemma mod_eq_dvd_iff:
+  "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P
+  then have "(a mod c - b mod c) mod c = 0"
+    by simp
+  then show ?Q
+    by (simp add: dvd_eq_mod_eq_0 mod_simps)
+next
+  assume ?Q
+  then obtain d where d: "a - b = c * d" ..
+  then have "a = c * d + b"
+    by (simp add: algebra_simps)
+  then show ?P by simp
+qed
+
+end
+
+  
 subsection \<open>Uniquely determined division\<close>
   
 class unique_euclidean_semiring = euclidean_semiring + 
@@ -284,8 +666,53 @@
     by simp
 qed
 
+subclass euclidean_semiring_cancel
+proof
+  show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
+  proof (cases a b rule: divmod_cases)
+    case by0
+    with \<open>b \<noteq> 0\<close> show ?thesis
+      by simp
+  next
+    case (divides q)
+    then show ?thesis
+      by (simp add: ac_simps)
+  next
+    case (remainder q r)
+    then show ?thesis
+      by (auto intro: div_eqI simp add: algebra_simps)
+  qed
+next
+  show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
+  proof (cases a b rule: divmod_cases)
+    case by0
+    then show ?thesis
+      by simp
+  next
+    case (divides q)
+    with \<open>c \<noteq> 0\<close> show ?thesis
+      by (simp add: mult.left_commute [of c])
+  next
+    case (remainder q r)
+    from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
+      by simp
+    from remainder \<open>c \<noteq> 0\<close>
+    have "uniqueness_constraint (r * c) (b * c)"
+      and "euclidean_size (r * c) < euclidean_size (b * c)"
+      by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
+    with remainder show ?thesis
+      by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
+        (use \<open>b * c \<noteq> 0\<close> in simp)
+  qed
+qed
+
 end
 
 class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
+begin
+  
+subclass euclidean_ring_cancel ..
 
 end
+
+end
diff -r 274b4edca859 -r a4e82b58d833 src/HOL/Factorial.thy
--- a/src/HOL/Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -130,11 +130,11 @@
 lemma fact_ge_self: "fact n \<ge> n"
   by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact)
 
-lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a::{semiring_div,linordered_semidom})"
+lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a::linordered_semidom)"
   by (induct m) (auto simp: le_Suc_eq)
 
-lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a::{semiring_div,linordered_semidom}) = 0"
-  by (auto simp add: fact_dvd)
+lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a::{semidom_modulo, linordered_semidom}) = 0"
+  by (simp add: mod_eq_0_iff_dvd fact_dvd)
 
 lemma fact_div_fact:
   assumes "m \<ge> n"
diff -r 274b4edca859 -r a4e82b58d833 src/HOL/Nonstandard_Analysis/StarDef.thy
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -772,9 +772,6 @@
 instance star :: (semidom_divide) semidom_divide
   by (intro_classes; transfer) simp_all
 
-instance star :: (semiring_div) semiring_div
-  by (intro_classes; transfer) (simp_all add: div_mult_mod_eq)
-
 instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
 instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
 instance star :: (idom) idom ..
@@ -821,6 +818,22 @@
 
 instance star :: (linordered_field) linordered_field ..
 
+instance star :: (algebraic_semidom) algebraic_semidom ..
+
+instantiation star :: (normalization_semidom) normalization_semidom
+begin
+
+definition unit_factor_star :: "'a star \<Rightarrow> 'a star"
+  where [transfer_unfold]: "unit_factor_star = *f* unit_factor"
+
+definition normalize_star :: "'a star \<Rightarrow> 'a star"
+  where [transfer_unfold]: "normalize_star = *f* normalize"
+
+instance
+  by standard (transfer; simp add: is_unit_unit_factor unit_factor_mult)+
+
+end
+
 
 subsection \<open>Power\<close>
 
@@ -912,49 +925,6 @@
   apply (transfer, erule odd_ex_decrement)
   done
 
-instance star :: (semiring_div_parity) semiring_div_parity
-  apply intro_classes
-    apply (transfer, rule parity)
-   apply (transfer, rule one_mod_two_eq_one)
-  apply (transfer, rule zero_not_eq_two)
-  done
-
-instantiation star :: (semiring_numeral_div) semiring_numeral_div
-begin
-
-definition divmod_star :: "num \<Rightarrow> num \<Rightarrow> 'a star \<times> 'a star"
-  where divmod_star_def: "divmod_star m n = (numeral m div numeral n, numeral m mod numeral n)"
-
-definition divmod_step_star :: "num \<Rightarrow> 'a star \<times> 'a star \<Rightarrow> 'a star \<times> 'a star"
-  where "divmod_step_star l qr =
-    (let (q, r) = qr
-     in if r \<ge> numeral l then (2 * q + 1, r - numeral l) else (2 * q, r))"
-
-instance
-proof
-  show "divmod m n = (numeral m div numeral n :: 'a star, numeral m mod numeral n)" for m n
-    by (fact divmod_star_def)
-  show "divmod_step l qr =
-    (let (q, r) = qr
-     in if r \<ge> numeral l then (2 * q + 1, r - numeral l) else (2 * q, r))"
-    for l and qr :: "'a star \<times> 'a star"
-    by (fact divmod_step_star_def)
-qed (transfer,
-  fact
-  semiring_numeral_div_class.div_less
-  semiring_numeral_div_class.mod_less
-  semiring_numeral_div_class.div_positive
-  semiring_numeral_div_class.mod_less_eq_dividend
-  semiring_numeral_div_class.pos_mod_bound
-  semiring_numeral_div_class.pos_mod_sign
-  semiring_numeral_div_class.mod_mult2_eq
-  semiring_numeral_div_class.div_mult2_eq
-  semiring_numeral_div_class.discrete)+
-
-end
-
-declare divmod_algorithm_code [where ?'a = "'a::semiring_numeral_div star", code]
-
 
 subsection \<open>Finite class\<close>
 
diff -r 274b4edca859 -r a4e82b58d833 src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Numeral_Simprocs.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -169,8 +169,8 @@
 
 (* TODO: remove comm_ring_1 constraint if possible *)
 simproc_setup int_div_cancel_numeral_factors
-  ("((l::'a::{semiring_div,comm_ring_1,ring_char_0}) * m) div n"
-  |"(l::'a::{semiring_div,comm_ring_1,ring_char_0}) div (m * n)") =
+  ("((l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) * m) div n"
+  |"(l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) div (m * n)") =
   \<open>fn phi => Numeral_Simprocs.div_cancel_numeral_factor\<close>
 
 simproc_setup divide_cancel_numeral_factor
@@ -194,13 +194,13 @@
   \<open>fn phi => Numeral_Simprocs.less_cancel_factor\<close>
 
 simproc_setup int_div_cancel_factor
-  ("((l::'a::semiring_div) * m) div n"
-  |"(l::'a::semiring_div) div (m * n)") =
+  ("((l::'a::euclidean_semiring_cancel) * m) div n"
+  |"(l::'a::euclidean_semiring_cancel) div (m * n)") =
   \<open>fn phi => Numeral_Simprocs.div_cancel_factor\<close>
 
 simproc_setup int_mod_cancel_factor
-  ("((l::'a::semiring_div) * m) mod n"
-  |"(l::'a::semiring_div) mod (m * n)") =
+  ("((l::'a::euclidean_semiring_cancel) * m) mod n"
+  |"(l::'a::euclidean_semiring_cancel) mod (m * n)") =
   \<open>fn phi => Numeral_Simprocs.mod_cancel_factor\<close>
 
 simproc_setup dvd_cancel_factor
diff -r 274b4edca859 -r a4e82b58d833 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Rat.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -199,12 +199,12 @@
 
 (* We cannot state these two rules earlier because of pending sort hypotheses *)
 lemma div_add_self1_no_field [simp]:
-  assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: semiring_div) \<noteq> 0"
+  assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: euclidean_semiring_cancel) \<noteq> 0"
   shows "(b + a) div b = a div b + 1"
   using assms(2) by (fact div_add_self1)
 
 lemma div_add_self2_no_field [simp]:
-  assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: semiring_div) \<noteq> 0"
+  assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: euclidean_semiring_cancel) \<noteq> 0"
   shows "(a + b) div b = a div b + 1"
   using assms(2) by (fact div_add_self2)
 
diff -r 274b4edca859 -r a4e82b58d833 src/HOL/ex/Simproc_Tests.thy
--- a/src/HOL/ex/Simproc_Tests.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -199,7 +199,7 @@
 subsection \<open>\<open>int_div_cancel_numeral_factors\<close>\<close>
 
 notepad begin
-  fix x y z :: "'a::{semiring_div,comm_ring_1,ring_char_0}"
+  fix x y z :: "'a::{unique_euclidean_semiring,comm_ring_1,ring_char_0}"
   {
     assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z"
       by (tactic \<open>test @{context} [@{simproc int_div_cancel_numeral_factors}]\<close>) fact
@@ -325,7 +325,7 @@
 subsection \<open>\<open>int_div_cancel_factor\<close>\<close>
 
 notepad begin
-  fix a b c d k uu x y :: "'a::semiring_div"
+  fix a b c d k uu x y :: "'a::unique_euclidean_semiring"
   {
     assume "(if k = 0 then 0 else x div y) = uu"
     have "(x*k) div (k*y) = uu"
diff -r 274b4edca859 -r a4e82b58d833 src/HOL/ex/Word_Type.thy
--- a/src/HOL/ex/Word_Type.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/ex/Word_Type.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -11,7 +11,7 @@
 
 subsection \<open>Truncating bit representations of numeric types\<close>
 
-class semiring_bits = semiring_div_parity +
+class semiring_bits = unique_euclidean_semiring_parity +
   assumes semiring_bits: "(1 + 2 * a) mod of_nat (2 * n) = 1 + 2 * (a mod of_nat n)"
 begin