clarified uniqueness criterion for euclidean rings

--- a/src/HOL/Code_Numeral.thy	Mon Oct 09 19:10:48 2017 +0200
+++ b/src/HOL/Code_Numeral.thy	Mon Oct 09 19:10:49 2017 +0200
@@ -241,15 +241,16 @@
 
 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"
+lift_definition division_segment_integer :: "integer \<Rightarrow> integer"
+  is "division_segment :: int \<Rightarrow> int"
   .
 
-declare uniqueness_constraint_integer.rep_eq [simp]
+declare division_segment_integer.rep_eq [simp]
 
 instance
   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)
+    (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
+     division_segment_mult division_segment_mod intro: div_eqI\<close>)
 
 end
 
@@ -258,8 +259,8 @@
   by (simp add: fun_eq_iff nat_of_integer.rep_eq)
 
 lemma [code]:
-  "uniqueness_constraint (k :: integer) l \<longleftrightarrow> sgn k = sgn l"
-  by (simp add: integer_eq_iff)
+  "division_segment (k :: integer) = (if k \<ge> 0 then 1 else - 1)"
+  by transfer (simp add: division_segment_int_def)
 
 instance integer :: ring_parity
   by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
@@ -869,11 +870,11 @@
 
 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"
+lift_definition division_segment_natural :: "natural \<Rightarrow> natural"
+  is "division_segment :: nat \<Rightarrow> nat"
   .
 
-declare uniqueness_constraint_natural.rep_eq [simp]
+declare division_segment_natural.rep_eq [simp]
 
 instance
   by (standard; transfer)
@@ -886,8 +887,8 @@
   by (simp add: fun_eq_iff)
 
 lemma [code]:
-  "uniqueness_constraint = (\<top> :: natural \<Rightarrow> natural \<Rightarrow> bool)"
-  by (simp add: fun_eq_iff)
+  "division_segment (n::natural) = 1"
+  by (simp add: natural_eq_iff)
 
 instance natural :: semiring_parity
   by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)

--- a/src/HOL/Computational_Algebra/Field_as_Ring.thy	Mon Oct 09 19:10:48 2017 +0200
+++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy	Mon Oct 09 19:10:49 2017 +0200
@@ -29,9 +29,9 @@
 
 definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
 definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
+definition [simp]: "modulo_real = (mod_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> _)"
+definition [simp]: "division_segment (x :: real) = 1"
 
 instance
   by standard
@@ -60,9 +60,9 @@
 
 definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
 definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
+definition [simp]: "modulo_rat = (mod_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> _)"
+definition [simp]: "division_segment (x :: rat) = 1"
 
 instance
   by standard
@@ -91,9 +91,9 @@
 
 definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
 definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
+definition [simp]: "modulo_complex = (mod_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> _)"
+definition [simp]: "division_segment (x :: complex) = 1"
 
 instance
   by standard

--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Mon Oct 09 19:10:48 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Mon Oct 09 19:10:49 2017 +0200
@@ -745,8 +745,8 @@
 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"
+definition division_segment_poly :: "'a poly \<Rightarrow> 'a poly"
+  where [simp]: "division_segment_poly p = 1"
 
 instance proof
   show "(q * p + r) div p = q" if "p \<noteq> 0"

--- a/src/HOL/Enum.thy	Mon Oct 09 19:10:48 2017 +0200
+++ b/src/HOL/Enum.thy	Mon Oct 09 19:10:49 2017 +0200
@@ -716,7 +716,7 @@
 definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
 definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
 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> _)"
+definition [simp]: "division_segment (x :: finite_2) = 1"
 instance
   by standard
     (auto simp add: divide_finite_2_def times_finite_2_def dvd_finite_2_unfold
@@ -868,7 +868,7 @@
 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 [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | _ \<Rightarrow> 1)"
-definition [simp]: "uniqueness_constraint = (\<top> :: finite_3 \<Rightarrow> _)"
+definition [simp]: "division_segment (x :: finite_3) = 1"
 instance proof
   fix x :: finite_3
   assume "x \<noteq> 0"

--- a/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:48 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:49 2017 +0200
@@ -506,17 +506,18 @@
 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"
+  fixes division_segment :: "'a \<Rightarrow> 'a"
+  assumes is_unit_division_segment: "is_unit (division_segment a)"
+    and division_segment_mult:
+    "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> division_segment (a * b) = division_segment a * division_segment b"
+    and division_segment_mod:
+    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> division_segment (a mod b) = division_segment b"
   assumes div_bounded:
-    "b \<noteq> 0 \<Longrightarrow> uniqueness_constraint r b
+    "b \<noteq> 0 \<Longrightarrow> division_segment r = division_segment b
     \<Longrightarrow> euclidean_size r < euclidean_size b
     \<Longrightarrow> (q * b + r) div b = q"
 begin
@@ -528,7 +529,7 @@
       and "a mod b = 0"
       and "a = q * b"
   | (remainder) q r where "b \<noteq> 0"
-      and "uniqueness_constraint r b"
+      and "division_segment r = division_segment b"
       and "euclidean_size r < euclidean_size b"
       and "r \<noteq> 0"
       and "a div b = q"
@@ -552,19 +553,19 @@
     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 from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "division_segment (a mod b) = division_segment b"
+      by (rule division_segment_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)
+      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"
+  "a div b = q" if "b \<noteq> 0" "division_segment r = division_segment b"
     "euclidean_size r < euclidean_size b" "q * b + r = a"
 proof -
   from that have "(q * b + r) div b = q"
@@ -574,7 +575,7 @@
 qed
 
 lemma mod_eqI:
-  "a mod b = r" if "b \<noteq> 0" "uniqueness_constraint r b"
+  "a mod b = r" if "b \<noteq> 0" "division_segment r = division_segment b"
     "euclidean_size r < euclidean_size b" "q * b + r = a" 
 proof -
   from that have "a div b = q"
@@ -618,9 +619,9 @@
     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)"
+    have "division_segment (r * c) = division_segment (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)
+      by (simp_all add: division_segment_mult division_segment_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)
@@ -728,8 +729,8 @@
 definition euclidean_size_nat :: "nat \<Rightarrow> nat"
   where [simp]: "euclidean_size_nat = id"
 
-definition uniqueness_constraint_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
-  where [simp]: "uniqueness_constraint_nat = \<top>"
+definition division_segment_nat :: "nat \<Rightarrow> nat"
+  where [simp]: "division_segment_nat n = 1"
 
 definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   where "m mod n = m - (m div n * (n::nat))"
@@ -1372,15 +1373,9 @@
 
 end
 
-instantiation int :: unique_euclidean_ring
+instantiation int :: idom_modulo
 begin
 
-definition euclidean_size_int :: "int \<Rightarrow> nat"
-  where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
-
-definition uniqueness_constraint_int :: "int \<Rightarrow> int \<Rightarrow> bool"
-  where [simp]: "uniqueness_constraint_int k l \<longleftrightarrow> unit_factor k = unit_factor l"
-
 definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
   where "k mod l = (if l = 0 then k
     else if sgn k = sgn l
@@ -1396,6 +1391,36 @@
   by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
     nat_mult_distrib dvd_int_iff)
 
+instance proof
+  fix k l :: int
+  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
+    by (blast intro: int_sgnE elim: that)
+  then show "k div l * l + k mod l = k"
+    by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
+       (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric]
+         distrib_left [symmetric] minus_mult_right
+         del: of_nat_mult minus_mult_right [symmetric])
+qed
+
+end
+
+instantiation int :: unique_euclidean_ring
+begin
+
+definition euclidean_size_int :: "int \<Rightarrow> nat"
+  where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
+
+definition division_segment_int :: "int \<Rightarrow> int"
+  where "division_segment_int k = (if k \<ge> 0 then 1 else - 1)"
+
+lemma division_segment_eq_sgn:
+  "division_segment k = sgn k" if "k \<noteq> 0" for k :: int
+  using that by (simp add: division_segment_int_def)
+
+lemma abs_division_segment [simp]:
+  "\<bar>division_segment k\<bar> = 1" for k :: int
+  by (simp add: division_segment_int_def)
+
 lemma abs_mod_less:
   "\<bar>k mod l\<bar> < \<bar>l\<bar>" if "l \<noteq> 0" for k l :: int
 proof -
@@ -1418,13 +1443,9 @@
 
 instance proof
   fix k l :: int
-  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
-    by (blast intro: int_sgnE elim: that)
-  then show "k div l * l + k mod l = k"
-    by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
-       (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric]
-         distrib_left [symmetric] minus_mult_right
-         del: of_nat_mult minus_mult_right [symmetric])
+  show "division_segment (k mod l) = division_segment l" if
+    "l \<noteq> 0" and "\<not> l dvd k"
+    using that by (simp add: division_segment_eq_sgn dvd_eq_mod_eq_0 sgn_mod)
 next
   fix l q r :: int
   obtain n m and s t
@@ -1433,12 +1454,12 @@
   assume \<open>l \<noteq> 0\<close>
   with l have "s \<noteq> 0" and "n > 0"
     by (simp_all add: sgn_0_0)
-  assume "uniqueness_constraint r l"
+  assume "division_segment r = division_segment l"
   moreover have "r = sgn r * \<bar>r\<bar>"
     by (simp add: sgn_mult_abs)
   moreover define u where "u = nat \<bar>r\<bar>"
   ultimately have "r = sgn l * int u"
-    by simp
+    using division_segment_eq_sgn \<open>l \<noteq> 0\<close> by (cases "r = 0") simp_all
   with l \<open>n > 0\<close> have r: "r = sgn s * int u"
     by (simp add: sgn_mult)
   assume "euclidean_size r < euclidean_size l"
@@ -1481,7 +1502,7 @@
       by (simp only: *, simp only: l q divide_int_unfold)
         (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
   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>)
+qed (use mult_le_mono2 [of 1] in \<open>auto simp add: division_segment_int_def not_le sign_simps abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
 
 end