reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion

--- a/src/HOL/Library/Field_as_Ring.thy	Wed Jan 04 22:57:39 2017 +0100
+++ b/src/HOL/Library/Field_as_Ring.thy	Wed Jan 04 21:28:28 2017 +0100
@@ -24,15 +24,19 @@
 
 end
 
-instantiation real :: euclidean_ring
+instantiation real :: unique_euclidean_ring
 begin
 
 definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
 definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
 definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
+definition [simp]: "uniqueness_constraint_real = (top :: real \<Rightarrow> real \<Rightarrow> bool)"
 definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
 
-instance by standard (simp_all add: dvd_field_iff divide_simps)
+instance
+  by standard
+    (simp_all add: dvd_field_iff divide_simps split: if_splits)
+
 end
 
 instantiation real :: euclidean_ring_gcd
@@ -51,15 +55,19 @@
 
 end
 
-instantiation rat :: euclidean_ring
+instantiation rat :: unique_euclidean_ring
 begin
 
 definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
 definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
 definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
+definition [simp]: "uniqueness_constraint_rat = (top :: rat \<Rightarrow> rat \<Rightarrow> bool)"
 definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
 
-instance by standard (simp_all add: dvd_field_iff divide_simps)
+instance
+  by standard
+    (simp_all add: dvd_field_iff divide_simps split: if_splits)
+
 end
 
 instantiation rat :: euclidean_ring_gcd
@@ -78,15 +86,19 @@
 
 end
 
-instantiation complex :: euclidean_ring
+instantiation complex :: unique_euclidean_ring
 begin
 
 definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
 definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
 definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
+definition [simp]: "uniqueness_constraint_complex = (top :: complex \<Rightarrow> complex \<Rightarrow> bool)"
 definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
 
-instance by standard (simp_all add: dvd_field_iff divide_simps)
+instance
+  by standard
+    (simp_all add: dvd_field_iff divide_simps split: if_splits)
+
 end
 
 instantiation complex :: euclidean_ring_gcd

--- a/src/HOL/Library/Formal_Power_Series.thy	Wed Jan 04 22:57:39 2017 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Jan 04 21:28:28 2017 +0100
@@ -1400,7 +1400,7 @@
 
 subsection \<open>Formal power series form a Euclidean ring\<close>
 
-instantiation fps :: (field) euclidean_ring
+instantiation fps :: (field) euclidean_ring_cancel
 begin
 
 definition fps_euclidean_size_def:

--- a/src/HOL/Library/Polynomial_Factorial.thy	Wed Jan 04 22:57:39 2017 +0100
+++ b/src/HOL/Library/Polynomial_Factorial.thy	Wed Jan 04 21:28:28 2017 +0100
@@ -676,14 +676,15 @@
   "euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)" 
 
 lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \<Rightarrow> _) = op dvd"
-    by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
+  by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
 
 interpretation field_poly: 
-  euclidean_ring where zero = "0 :: 'a :: field poly"
+  unique_euclidean_ring where zero = "0 :: 'a :: field poly"
     and one = 1 and plus = plus and uminus = uminus and minus = minus
     and times = times
     and normalize = normalize_field_poly and unit_factor = unit_factor_field_poly
     and euclidean_size = euclidean_size_field_poly
+    and uniqueness_constraint = top
     and divide = divide and modulo = modulo
 proof (standard, unfold dvd_field_poly)
   fix p :: "'a poly"
@@ -698,6 +699,17 @@
   fix p :: "'a poly" assume "p \<noteq> 0"
   thus "is_unit (unit_factor_field_poly p)"
     by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff)
+next
+  fix p q s :: "'a poly" assume "s \<noteq> 0"
+  moreover assume "euclidean_size_field_poly p < euclidean_size_field_poly q"
+  ultimately show "euclidean_size_field_poly (p * s) < euclidean_size_field_poly (q * s)"
+    by (auto simp add: euclidean_size_field_poly_def degree_mult_eq)
+next
+  fix p q r :: "'a poly" assume "p \<noteq> 0"
+  moreover assume "euclidean_size_field_poly r < euclidean_size_field_poly p"
+  ultimately show "(q * p + r) div p = q"
+    by (cases "r = 0")
+      (auto simp add: unit_factor_field_poly_def euclidean_size_field_poly_def div_poly_less)
 qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 
        euclidean_size_field_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
 
@@ -1011,17 +1023,22 @@
 
 end
 
-instantiation poly :: ("{field,factorial_ring_gcd}") euclidean_ring
+instantiation poly :: ("{field,factorial_ring_gcd}") unique_euclidean_ring
 begin
 
-definition euclidean_size_poly :: "'a poly \<Rightarrow> nat" where
-  "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
+definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
+  where "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
+
+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 intro!: degree_mod_less' degree_mult_right_le)
+  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
+    split: if_splits)
+
 end
 
-
 instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd
   by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def eucl_eq_factorial)
 

--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jan 04 22:57:39 2017 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jan 04 21:28:28 2017 +0100
@@ -1,133 +1,17 @@
-(* Author: Manuel Eberl *)
+(*  Title:      HOL/Number_Theory/Euclidean_Algorithm.thy
+    Author:     Manuel Eberl, TU Muenchen
+*)
 
-section \<open>Abstract euclidean algorithm\<close>
+section \<open>Abstract euclidean algorithm in euclidean (semi)rings\<close>
 
 theory Euclidean_Algorithm
-imports "~~/src/HOL/GCD" Factorial_Ring
-begin
-
-text \<open>
-  A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
-  implemented. It must provide:
-  \begin{itemize}
-  \item division with remainder
-  \item a size function such that @{term "size (a mod b) < size b"} 
-        for any @{term "b \<noteq> 0"}
-  \end{itemize}
-  The existence of these functions makes it possible to derive gcd and lcm functions 
-  for any Euclidean semiring.
-\<close> 
-class euclidean_semiring = semidom_modulo + normalization_semidom + 
-  fixes euclidean_size :: "'a \<Rightarrow> nat"
-  assumes size_0 [simp]: "euclidean_size 0 = 0"
-  assumes mod_size_less: 
-    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
-  assumes size_mult_mono:
-    "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
+  imports "~~/src/HOL/GCD"
+    "~~/src/HOL/Number_Theory/Factorial_Ring"
+    "~~/src/HOL/Number_Theory/Euclidean_Division"
 begin
 
-lemma euclidean_size_normalize [simp]:
-  "euclidean_size (normalize a) = euclidean_size a"
-proof (cases "a = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case [simp]: False
-  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
-    by (rule size_mult_mono) simp
-  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
-    by (rule size_mult_mono) simp
-  ultimately show ?thesis
-    by simp
-qed
-
-lemma euclidean_division:
-  fixes a :: 'a and b :: 'a
-  assumes "b \<noteq> 0"
-  obtains s and t where "a = s * b + t" 
-    and "euclidean_size t < euclidean_size b"
-proof -
-  from div_mult_mod_eq [of a b] 
-     have "a = a div b * b + a mod b" by simp
-  with that and assms show ?thesis by (auto simp add: mod_size_less)
-qed
-
-lemma dvd_euclidean_size_eq_imp_dvd:
-  assumes "a \<noteq> 0" and b_dvd_a: "b dvd a" and size_eq: "euclidean_size a = euclidean_size b"
-  shows "a dvd b"
-proof (rule ccontr)
-  assume "\<not> a dvd b"
-  hence "b mod a \<noteq> 0" using mod_0_imp_dvd[of b a] by blast
-  then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
-  from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff)
-  from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast
-    with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
-  with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
-      using size_mult_mono by force
-  moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
-  have "euclidean_size (b mod a) < euclidean_size a"
-      using mod_size_less by blast
-  ultimately show False using size_eq by simp
-qed
-
-lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
-  by (subst mult.commute) (rule size_mult_mono)
-
-lemma euclidean_size_times_unit:
-  assumes "is_unit a"
-  shows   "euclidean_size (a * b) = euclidean_size b"
-proof (rule antisym)
-  from assms have [simp]: "a \<noteq> 0" by auto
-  thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
-  from assms have "is_unit (1 div a)" by simp
-  hence "1 div a \<noteq> 0" by (intro notI) simp_all
-  hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
-    by (rule size_mult_mono')
-  also from assms have "(1 div a) * (a * b) = b"
-    by (simp add: algebra_simps unit_div_mult_swap)
-  finally show "euclidean_size (a * b) \<le> euclidean_size b" .
-qed
-
-lemma euclidean_size_unit: "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
-  using euclidean_size_times_unit[of a 1] by simp
-
-lemma unit_iff_euclidean_size: 
-  "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
-proof safe
-  assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
-  show "is_unit a" by (rule dvd_euclidean_size_eq_imp_dvd[OF A _ B]) simp_all
-qed (auto intro: euclidean_size_unit)
-
-lemma euclidean_size_times_nonunit:
-  assumes "a \<noteq> 0" "b \<noteq> 0" "\<not>is_unit a"
-  shows   "euclidean_size b < euclidean_size (a * b)"
-proof (rule ccontr)
-  assume "\<not>euclidean_size b < euclidean_size (a * b)"
-  with size_mult_mono'[OF assms(1), of b] 
-    have eq: "euclidean_size (a * b) = euclidean_size b" by simp
-  have "a * b dvd b"
-    by (rule dvd_euclidean_size_eq_imp_dvd[OF _ _ eq]) (insert assms, simp_all)
-  hence "a * b dvd 1 * b" by simp
-  with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
-  with assms(3) show False by contradiction
-qed
-
-lemma dvd_imp_size_le:
-  assumes "a dvd b" "b \<noteq> 0" 
-  shows   "euclidean_size a \<le> euclidean_size b"
-  using assms by (auto elim!: dvdE simp: size_mult_mono)
-
-lemma dvd_proper_imp_size_less:
-  assumes "a dvd b" "\<not>b dvd a" "b \<noteq> 0" 
-  shows   "euclidean_size a < euclidean_size b"
-proof -
-  from assms(1) obtain c where "b = a * c" by (erule dvdE)
-  hence z: "b = c * a" by (simp add: mult.commute)
-  from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
-  with z assms show ?thesis
-    by (auto intro!: euclidean_size_times_nonunit simp: )
-qed
+context euclidean_semiring
+begin
 
 function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 where
@@ -432,7 +316,7 @@
   
 end
 
-class euclidean_ring = euclidean_semiring + idom
+context euclidean_ring
 begin
 
 function euclid_ext_aux :: "'a \<Rightarrow> _" where
@@ -680,27 +564,6 @@
 
 subsection \<open>Typical instances\<close>
 
-instantiation nat :: euclidean_semiring
-begin
-
-definition [simp]:
-  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
-
-instance by standard simp_all
-
-end
-
-
-instantiation int :: euclidean_ring
-begin
-
-definition [simp]:
-  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
-
-instance by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split)
-
-end
-
 instance nat :: euclidean_semiring_gcd
 proof
   show [simp]: "gcd = (gcd_eucl :: nat \<Rightarrow> _)" "Lcm = (Lcm_eucl :: nat set \<Rightarrow> _)"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Number_Theory/Euclidean_Division.thy	Wed Jan 04 21:28:28 2017 +0100
@@ -0,0 +1,295 @@
+(*  Title:      HOL/Number_Theory/Euclidean_Division.thy
+    Author:     Manuel Eberl, TU Muenchen
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+section \<open>Division with remainder in euclidean (semi)rings\<close>
+
+theory Euclidean_Division
+  imports Main
+begin
+
+subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
+  
+class euclidean_semiring = semidom_modulo + normalization_semidom + 
+  fixes euclidean_size :: "'a \<Rightarrow> nat"
+  assumes size_0 [simp]: "euclidean_size 0 = 0"
+  assumes mod_size_less: 
+    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
+  assumes size_mult_mono:
+    "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
+begin
+
+lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
+  by (subst mult.commute) (rule size_mult_mono)
+
+lemma euclidean_size_normalize [simp]:
+  "euclidean_size (normalize a) = euclidean_size a"
+proof (cases "a = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case [simp]: False
+  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
+    by (rule size_mult_mono) simp
+  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
+    by (rule size_mult_mono) simp
+  ultimately show ?thesis
+    by simp
+qed
+
+lemma dvd_euclidean_size_eq_imp_dvd:
+  assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
+    and "b dvd a" 
+  shows "a dvd b"
+proof (rule ccontr)
+  assume "\<not> a dvd b"
+  hence "b mod a \<noteq> 0" using mod_0_imp_dvd [of b a] by blast
+  then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
+  from \<open>b dvd a\<close> have "b dvd b mod a" by (simp add: dvd_mod_iff)
+  then obtain c where "b mod a = b * c" unfolding dvd_def by blast
+    with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
+  with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
+    using size_mult_mono by force
+  moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
+  have "euclidean_size (b mod a) < euclidean_size a"
+    using mod_size_less by blast
+  ultimately show False using \<open>euclidean_size a = euclidean_size b\<close>
+    by simp
+qed
+
+lemma euclidean_size_times_unit:
+  assumes "is_unit a"
+  shows   "euclidean_size (a * b) = euclidean_size b"
+proof (rule antisym)
+  from assms have [simp]: "a \<noteq> 0" by auto
+  thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
+  from assms have "is_unit (1 div a)" by simp
+  hence "1 div a \<noteq> 0" by (intro notI) simp_all
+  hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
+    by (rule size_mult_mono')
+  also from assms have "(1 div a) * (a * b) = b"
+    by (simp add: algebra_simps unit_div_mult_swap)
+  finally show "euclidean_size (a * b) \<le> euclidean_size b" .
+qed
+
+lemma euclidean_size_unit:
+  "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
+  using euclidean_size_times_unit [of a 1] by simp
+
+lemma unit_iff_euclidean_size: 
+  "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
+proof safe
+  assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
+  show "is_unit a"
+    by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all
+qed (auto intro: euclidean_size_unit)
+
+lemma euclidean_size_times_nonunit:
+  assumes "a \<noteq> 0" "b \<noteq> 0" "\<not> is_unit a"
+  shows   "euclidean_size b < euclidean_size (a * b)"
+proof (rule ccontr)
+  assume "\<not>euclidean_size b < euclidean_size (a * b)"
+  with size_mult_mono'[OF assms(1), of b] 
+    have eq: "euclidean_size (a * b) = euclidean_size b" by simp
+  have "a * b dvd b"
+    by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all)
+  hence "a * b dvd 1 * b" by simp
+  with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
+  with assms(3) show False by contradiction
+qed
+
+lemma dvd_imp_size_le:
+  assumes "a dvd b" "b \<noteq> 0" 
+  shows   "euclidean_size a \<le> euclidean_size b"
+  using assms by (auto elim!: dvdE simp: size_mult_mono)
+
+lemma dvd_proper_imp_size_less:
+  assumes "a dvd b" "\<not> b dvd a" "b \<noteq> 0" 
+  shows   "euclidean_size a < euclidean_size b"
+proof -
+  from assms(1) obtain c where "b = a * c" by (erule dvdE)
+  hence z: "b = c * a" by (simp add: mult.commute)
+  from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
+  with z assms show ?thesis
+    by (auto intro!: euclidean_size_times_nonunit)
+qed
+
+end
+
+class euclidean_ring = idom_modulo + euclidean_semiring
+
+  
+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
+  
+  
+subsection \<open>Uniquely determined division\<close>
+  
+class unique_euclidean_semiring = euclidean_semiring + 
+  fixes uniqueness_constraint :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  assumes size_mono_mult:
+    "b \<noteq> 0 \<Longrightarrow> euclidean_size a < euclidean_size c
+      \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
+    -- \<open>FIXME justify\<close>
+  assumes uniqueness_constraint_mono_mult:
+    "uniqueness_constraint a b \<Longrightarrow> uniqueness_constraint (a * c) (b * c)"
+  assumes uniqueness_constraint_mod:
+    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> uniqueness_constraint (a mod b) b"
+  assumes div_bounded:
+    "b \<noteq> 0 \<Longrightarrow> uniqueness_constraint r b
+    \<Longrightarrow> euclidean_size r < euclidean_size b
+    \<Longrightarrow> (q * b + r) div b = q"
+begin
+
+lemma divmod_cases [case_names divides remainder by0]:
+  obtains 
+    (divides) q where "b \<noteq> 0"
+      and "a div b = q"
+      and "a mod b = 0"
+      and "a = q * b"
+  | (remainder) q r where "b \<noteq> 0" and "r \<noteq> 0"
+      and "uniqueness_constraint r b"
+      and "euclidean_size r < euclidean_size b"
+      and "a div b = q"
+      and "a mod b = r"
+      and "a = q * b + r"
+  | (by0) "b = 0"
+proof (cases "b = 0")
+  case True
+  then show thesis
+  by (rule by0)
+next
+  case False
+  show thesis
+  proof (cases "b dvd a")
+    case True
+    then obtain q where "a = b * q" ..
+    with \<open>b \<noteq> 0\<close> divides
+    show thesis
+      by (simp add: ac_simps)
+  next
+    case False
+    then have "a mod b \<noteq> 0"
+      by (simp add: mod_eq_0_iff_dvd)
+    moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "uniqueness_constraint (a mod b) b"
+      by (rule uniqueness_constraint_mod)
+    moreover have "euclidean_size (a mod b) < euclidean_size b"
+      using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
+    moreover have "a = a div b * b + a mod b"
+      by (simp add: div_mult_mod_eq)
+    ultimately show thesis
+      using \<open>b \<noteq> 0\<close> by (blast intro: remainder)
+  qed
+qed
+
+lemma div_eqI:
+  "a div b = q" if "b \<noteq> 0" "uniqueness_constraint r b"
+    "euclidean_size r < euclidean_size b" "q * b + r = a"
+proof -
+  from that have "(q * b + r) div b = q"
+    by (auto intro: div_bounded)
+  with that show ?thesis
+    by simp
+qed
+
+lemma mod_eqI:
+  "a mod b = r" if "b \<noteq> 0" "uniqueness_constraint r b"
+    "euclidean_size r < euclidean_size b" "q * b + r = a" 
+proof -
+  from that have "a div b = q"
+    by (rule div_eqI)
+  moreover have "a div b * b + a mod b = a"
+    by (fact div_mult_mod_eq)
+  ultimately have "a div b * b + a mod b = a div b * b + r"
+    using \<open>q * b + r = a\<close> by simp
+  then show ?thesis
+    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
+
+subsection \<open>Typical instances\<close>
+
+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
+    (simp_all add: unit_factor_nat_def mod_greater_zero_iff_not_dvd)
+
+end
+
+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
+    (auto simp add: abs_mult nat_mult_distrib sgn_mod zdiv_eq_0_iff sgn_1_pos sgn_mult split: abs_split)
+
+end
+
+end