# HG changeset patch
# User haftmann
# Date 1660768636 0
# Node ID 48d0320357449414e9591059303d4454ddbd92c7
# Parent  77cbf472fcc9e2b0c3c977590b2e6c9bfdaa2e47
streamlined primitive definitions for integer division

diff -r 77cbf472fcc9 -r 48d032035744 NEWS
--- a/NEWS	Thu Aug 18 09:29:11 2022 +0200
+++ b/NEWS	Wed Aug 17 20:37:16 2022 +0000
@@ -39,7 +39,7 @@
 
 * New Theory Code_Abstract_Char implements characters by target language
 integers, sacrificing pattern patching in exchange for dramatically
-increased performance for comparisions.
+increased performance for comparisons.
 
 * New theory HOL-Library.NList of fixed length lists
 
@@ -49,6 +49,9 @@
 * Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
 longer. INCOMPATIBILITY.
 
+* Streamlined primitive definitions of division and modulus on integers.
+INCOMPATIBILITY.
+
 * Theory "HOL.Fun":
   - Added predicate monotone_on and redefined monotone to be an
     abbreviation. Lemma monotone_def is explicitly provided for backward
diff -r 77cbf472fcc9 -r 48d032035744 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Thu Aug 18 09:29:11 2022 +0200
+++ b/src/HOL/Bit_Operations.thy	Wed Aug 17 20:37:16 2022 +0000
@@ -7,6 +7,15 @@
   imports Presburger Groups_List
 begin
 
+lemma half_nonnegative_int_iff [simp]:
+  \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+  by auto
+
+lemma half_negative_int_iff [simp]:
+  \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+  by auto
+
+
 subsection \<open>Abstract bit structures\<close>
 
 class semiring_bits = semiring_parity +
@@ -1465,7 +1474,7 @@
 
 lemma not_int_div_2:
   \<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
-  by (cases k) (simp_all add: not_int_def divide_int_def nat_add_distrib)
+  by (simp add: not_int_def)
 
 lemma bit_not_int_iff:
   \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
@@ -1729,7 +1738,7 @@
   case (odd k)
   from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems
   show ?case
-    by (simp add: and_int_rec [of _ l]) linarith
+    by (simp add: and_int_rec [of _ l])
 qed
 
 lemma or_nonnegative_int_iff [simp]:
@@ -1754,7 +1763,7 @@
   case (even k)
   from even.IH [of \<open>l div 2\<close>] even.hyps even.prems
   show ?case
-    by (simp add: or_int_rec [of _ l]) linarith
+    by (simp add: or_int_rec [of _ l])
 next
   case (odd k)
   from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems
@@ -2173,22 +2182,6 @@
   \<open>\<not> 2 ^ n \<le> (0::int)\<close>
   by (simp add: power_le_zero_eq)
 
-lemma half_nonnegative_int_iff [simp]:
-  \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
-proof (cases \<open>k \<ge> 0\<close>)
-  case True
-  then show ?thesis
-    by (auto simp add: divide_int_def sgn_1_pos)
-next
-  case False
-  then show ?thesis
-    by (auto simp add: divide_int_def not_le elim!: evenE)
-qed
-
-lemma half_negative_int_iff [simp]:
-  \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
-  by (subst Not_eq_iff [symmetric]) (simp add: not_less)
-
 lemma int_bit_bound:
   fixes k :: int
   obtains n where \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
diff -r 77cbf472fcc9 -r 48d032035744 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Aug 18 09:29:11 2022 +0200
+++ b/src/HOL/Divides.thy	Wed Aug 17 20:37:16 2022 +0000
@@ -11,6 +11,43 @@
 
 subsection \<open>More on division\<close>
 
+subsubsection \<open>Laws for div and mod with Unary Minus\<close>
+
+lemma zmod_zminus1_not_zero:
+  fixes k l :: int
+  shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+  by (simp add: mod_eq_0_iff_dvd)
+
+lemma zmod_zminus2_not_zero:
+  fixes k l :: int
+  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+  by (simp add: mod_eq_0_iff_dvd)
+
+lemma zdiv_zminus1_eq_if:
+  \<open>(- a) div b = (if a mod b = 0 then - (a div b) else - (a div b) - 1)\<close>
+  if \<open>b \<noteq> 0\<close> for a b :: int
+  using that sgn_not_eq_imp [of b \<open>- a\<close>]
+  by (cases \<open>a = 0\<close>) (auto simp add: div_eq_div_abs [of \<open>- a\<close> b] div_eq_div_abs [of a b] sgn_eq_0_iff)
+
+lemma zdiv_zminus2_eq_if:
+  \<open>a div (- b) = (if a mod b = 0 then - (a div b) else - (a div b) - 1)\<close>
+  if \<open>b \<noteq> 0\<close> for a b :: int
+  using that by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
+
+lemma zmod_zminus1_eq_if:
+  \<open>(- a) mod b = (if a mod b = 0 then 0 else b - (a mod b))\<close>
+  for a b :: int
+  by (cases \<open>b = 0\<close>)
+    (auto simp flip: minus_div_mult_eq_mod simp add: zdiv_zminus1_eq_if algebra_simps)
+
+lemma zmod_zminus2_eq_if:
+  \<open>a mod (- b) = (if a mod b = 0 then 0 else (a mod b) - b)\<close>
+  for a b :: int
+  by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
+
+
+subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
+
 inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
   where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
   | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
@@ -91,139 +128,20 @@
   using unique_quotient [of k l] unique_remainder [of k l]
   by auto
 
-lemma div_abs_eq_div_nat:
-  "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
-  by (simp add: divide_int_def)
-
-lemma mod_abs_eq_div_nat:
-  "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
-  by (simp add: modulo_int_def)
-
-lemma zdiv_int:
-  "int (a div b) = int a div int b"
-  by (simp add: divide_int_def)
-
-lemma zmod_int:
-  "int (a mod b) = int a mod int b"
-  by (simp add: modulo_int_def)
-
-lemma div_sgn_abs_cancel:
-  fixes k l v :: int
-  assumes "v \<noteq> 0"
-  shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
-proof -
-  from assms have "sgn v = - 1 \<or> sgn v = 1"
-    by (cases "v \<ge> 0") auto
-  then show ?thesis
-    using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
-    by (fastforce simp add: not_less div_abs_eq_div_nat)
-qed
-
-lemma div_eq_sgn_abs:
-  fixes k l v :: int
-  assumes "sgn k = sgn l"
-  shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
-proof (cases "l = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
-    using div_sgn_abs_cancel [of l k l] by simp
-  then show ?thesis
-    by (simp add: sgn_mult_abs)
-qed
-
-lemma div_dvd_sgn_abs:
-  fixes k l :: int
-  assumes "l dvd k"
-  shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
-proof (cases "k = 0 \<or> l = 0")
-  case True
-  then show ?thesis
-    by auto
-next
-  case False
-  then have "k \<noteq> 0" and "l \<noteq> 0"
-    by auto
-  show ?thesis
-  proof (cases "sgn l = sgn k")
-    case True
-    then show ?thesis
-      by (auto simp add: div_eq_sgn_abs)
-  next
-    case False
-    with \<open>k \<noteq> 0\<close> \<open>l \<noteq> 0\<close>
-    have "sgn l * sgn k = - 1"
-      by (simp add: sgn_if split: if_splits)
-    with assms show ?thesis
-      unfolding divide_int_def [of k l]
-      by (auto simp add: zdiv_int ac_simps)
-  qed
-qed
-
-lemma div_noneq_sgn_abs:
-  fixes k l :: int
-  assumes "l \<noteq> 0"
-  assumes "sgn k \<noteq> sgn l"
-  shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
-  using assms
-  by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
-  
-
-subsubsection \<open>Laws for div and mod with Unary Minus\<close>
-
 lemma zminus1_lemma:
      "eucl_rel_int a b (q, r) ==> b \<noteq> 0
       ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
                           if r=0 then 0 else b-r)"
 by (force simp add: eucl_rel_int_iff right_diff_distrib)
 
-
-lemma zdiv_zminus1_eq_if:
-     "b \<noteq> (0::int)
-      \<Longrightarrow> (-a) div b = (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
-by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
-
-lemma zmod_zminus1_eq_if:
-     "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
-proof (cases "b = 0")
-  case False
-  then show ?thesis
-    by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
-qed auto
-
-lemma zmod_zminus1_not_zero:
-  fixes k l :: int
-  shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
-  by (simp add: mod_eq_0_iff_dvd)
-
-lemma zmod_zminus2_not_zero:
-  fixes k l :: int
-  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
-  by (simp add: mod_eq_0_iff_dvd)
-
-lemma zdiv_zminus2_eq_if:
-  "b \<noteq> (0::int)
-      ==> a div (-b) =
-          (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
-  by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
-
-lemma zmod_zminus2_eq_if:
-  "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
-  by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
-
-
-subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
-
 lemma zdiv_mono1:
-  fixes b::int
-  assumes "a \<le> a'" "0 < b" shows "a div b \<le> a' div b"
+  \<open>a div b \<le> a' div b\<close>
+  if \<open>a \<le> a'\<close> \<open>0 < b\<close>
+  for a b b' :: int
 proof (rule unique_quotient_lemma)
   show "b * (a div b) + a mod b \<le> b * (a' div b) + a' mod b"
-    using assms(1) by auto
-qed (use assms in auto)
+    using \<open>a \<le> a'\<close> by auto
+qed (use that in auto)
 
 lemma zdiv_mono1_neg:
   fixes b::int
diff -r 77cbf472fcc9 -r 48d032035744 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Thu Aug 18 09:29:11 2022 +0200
+++ b/src/HOL/Euclidean_Division.thy	Wed Aug 17 20:37:16 2022 +0000
@@ -321,7 +321,7 @@
 
 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)
+  by (cases "c = 0") auto
 
 lemma div_plus_div_distrib_dvd_right:
   "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
@@ -603,7 +603,7 @@
 
   
 subsection \<open>Uniquely determined division\<close>
-  
+
 class unique_euclidean_semiring = euclidean_semiring + 
   assumes euclidean_size_mult: "euclidean_size (a * b) = euclidean_size a * euclidean_size b"
   fixes division_segment :: "'a \<Rightarrow> 'a"
@@ -1499,26 +1499,20 @@
 instantiation int :: normalization_semidom
 begin
 
-definition normalize_int :: "int \<Rightarrow> int"
-  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
-
-definition unit_factor_int :: "int \<Rightarrow> int"
-  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
+definition normalize_int :: \<open>int \<Rightarrow> int\<close>
+  where [simp]: \<open>normalize = (abs :: int \<Rightarrow> int)\<close>
 
-definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
-  where "k div l = (if l = 0 then 0
-    else if sgn k = sgn l
-      then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
-      else - int (nat \<bar>k\<bar> div nat \<bar>l\<bar> + of_bool (\<not> l dvd k)))"
+definition unit_factor_int :: \<open>int \<Rightarrow> int\<close>
+  where [simp]: \<open>unit_factor = (sgn :: int \<Rightarrow> int)\<close>
+
+definition divide_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>k div l = (sgn k * sgn l * int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
+    - of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k))\<close>
 
 lemma divide_int_unfold:
-  "(sgn k * int m) div (sgn l * int n) =
-   (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then 0
-    else if sgn k = sgn l
-      then int (m div n)
-      else - int (m div n + of_bool (\<not> n dvd m)))"
-  by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
-    nat_mult_distrib)
+  \<open>(sgn k * int m) div (sgn l * int n) = (sgn k * sgn l * int (m div n)
+    - of_bool ((k = 0 \<longleftrightarrow> m = 0) \<and> l \<noteq> 0 \<and> n \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> n dvd m))\<close>
+  by (simp add: divide_int_def sgn_mult nat_mult_distrib abs_mult sgn_eq_0_iff ac_simps)
 
 instance proof
   fix k :: int show "k div 0 = 0"
@@ -1537,6 +1531,21 @@
 
 end
 
+lemma div_abs_eq_div_nat:
+  "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
+  by (auto simp add: divide_int_def)
+
+lemma div_eq_div_abs:
+  \<open>k div l = sgn k * sgn l * (\<bar>k\<bar> div \<bar>l\<bar>)
+    - of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+  for k l :: int
+  by (simp add: divide_int_def [of k l] div_abs_eq_div_nat)
+
+lemma div_abs_eq:
+  \<open>\<bar>k\<bar> div \<bar>l\<bar> = sgn k * sgn l * (k div l + of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k))\<close>
+  for k l :: int
+  by (simp add: div_eq_div_abs [of k l] ac_simps)
+
 lemma coprime_int_iff [simp]:
   "coprime (int m) (int n) \<longleftrightarrow> coprime m n" (is "?P \<longleftrightarrow> ?Q")
 proof
@@ -1598,34 +1607,38 @@
 instantiation int :: idom_modulo
 begin
 
-definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
-  where "k mod l = (if l = 0 then k
-    else if sgn k = sgn l
-      then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
-      else sgn l * (\<bar>l\<bar> * of_bool (\<not> l dvd k) - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
+definition modulo_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>k mod l = sgn k * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>) + l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
 
 lemma modulo_int_unfold:
-  "(sgn k * int m) mod (sgn l * int n) =
-   (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then sgn k * int m
-    else if sgn k = sgn l
-      then sgn l * int (m mod n)
-      else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
-  by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
-    nat_mult_distrib)
+  \<open>(sgn k * int m) mod (sgn l * int n) =
+    sgn k * int (m mod (of_bool (l \<noteq> 0) * n)) + (sgn l * int n) * of_bool ((k = 0 \<longleftrightarrow> m = 0) \<and> sgn k \<noteq> sgn l \<and> \<not> n dvd m)\<close>
+  by (auto simp add: modulo_int_def sgn_mult abs_mult)
 
 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])
+    by (simp add: divide_int_unfold modulo_int_unfold algebra_simps modulo_nat_def of_nat_diff)
 qed
 
 end
 
+lemma mod_abs_eq_div_nat:
+  "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
+  by (simp add: modulo_int_def)
+
+lemma mod_eq_mod_abs:
+  \<open>k mod l = sgn k * (\<bar>k\<bar> mod \<bar>l\<bar>) + l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+  for k l :: int
+  by (simp add: modulo_int_def [of k l] mod_abs_eq_div_nat)
+
+lemma mod_abs_eq:
+  \<open>\<bar>k\<bar> mod \<bar>l\<bar> = sgn k * (k mod l - l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k))\<close>
+  for k l :: int
+  by (auto simp: mod_eq_mod_abs [of k l])
+
 instantiation int :: unique_euclidean_ring
 begin
 
@@ -1649,8 +1662,9 @@
   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)
   with that show ?thesis
-    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
-      abs_mult mod_greater_zero_iff_not_dvd)
+    by (auto simp add: modulo_int_unfold abs_mult mod_greater_zero_iff_not_dvd
+        simp flip: right_diff_distrib dest!: sgn_not_eq_imp)
+      (simp add: sgn_0_0)
 qed
 
 lemma sgn_mod:
@@ -1659,8 +1673,8 @@
   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)
   with that show ?thesis
-    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg sgn_mult)
-      (simp add: dvd_eq_mod_eq_0)
+    by (auto simp add: modulo_int_unfold sgn_mult mod_greater_zero_iff_not_dvd
+      simp flip: right_diff_distrib dest!: sgn_not_eq_imp)
 qed
 
 instance proof
@@ -1700,8 +1714,8 @@
       from \<open>r = 0\<close> have *: "q * l + r = sgn (t * s) * int (n * m)"
         using q l by (simp add: ac_simps sgn_mult)
       from \<open>s \<noteq> 0\<close> \<open>n > 0\<close> show ?thesis
-        by (simp only: *, simp only: q l divide_int_unfold)
-          (auto simp add: sgn_mult sgn_0_0 sgn_1_pos)
+        by (simp only: *, simp only: * q l divide_int_unfold)
+          (auto simp add: sgn_mult ac_simps)
     qed
   next
     case False
@@ -1728,6 +1742,12 @@
 
 end
 
+lemma div_sgn_abs_cancel:
+  fixes k l v :: int
+  assumes "v \<noteq> 0"
+  shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
+  using assms by (simp add: sgn_mult abs_mult sgn_0_0 of_nat_div divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"])
+
 lemma pos_mod_bound [simp]:
   "k mod l < l" if "l > 0" for k l :: int
 proof -
@@ -1739,7 +1759,7 @@
     by simp
   ultimately show ?thesis
     by (simp only: modulo_int_unfold)
-      (simp add: mod_greater_zero_iff_not_dvd)
+      (auto simp add: mod_greater_zero_iff_not_dvd sgn_1_pos)
 qed
 
 lemma neg_mod_bound [simp]:
@@ -1754,7 +1774,7 @@
     by simp
   ultimately show ?thesis
     by (simp only: modulo_int_unfold)
-      (simp add: mod_greater_zero_iff_not_dvd)
+      (auto simp add: mod_greater_zero_iff_not_dvd sgn_1_neg)
 qed
 
 lemma pos_mod_sign [simp]:
@@ -1767,7 +1787,7 @@
   moreover from this that have "n > 0"
     by simp
   ultimately show ?thesis
-    by (simp only: modulo_int_unfold) simp
+    by (simp only: modulo_int_unfold) (auto simp add: sgn_1_pos)
 qed
 
 lemma neg_mod_sign [simp]:
@@ -1780,8 +1800,12 @@
   moreover define n where "n = Suc q"
   then have "Suc q = n"
     by simp
+  moreover have \<open>int (m mod n) \<le> int n\<close>
+    using \<open>Suc q = n\<close> by simp
+  then have \<open>sgn s * int (m mod n) \<le> int n\<close>
+    by (cases s \<open>0::int\<close> rule: linorder_cases) simp_all
   ultimately show ?thesis
-    by (simp only: modulo_int_unfold) simp
+    by (simp only: modulo_int_unfold) auto
 qed
 
 lemma div_pos_pos_trivial [simp]:
@@ -2075,7 +2099,7 @@
   proof (cases \<open>n \<le> m\<close>)
     case True
     then show ?thesis
-      by (simp add: Suc_le_lessD min.absorb2)
+      by (simp add: Suc_le_lessD)
   next
     case False
     then have \<open>m < n\<close>
@@ -2109,7 +2133,27 @@
   by standard (simp_all add: dvd_eq_mod_eq_0)
 
 instance int :: unique_euclidean_ring_with_nat
-  by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def)
+  by standard (auto simp add: divide_int_def division_segment_int_def elim: contrapos_np)
+
+lemma div_eq_sgn_abs:
+  fixes k l v :: int
+  assumes "sgn k = sgn l"
+  shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
+  using assms by (auto simp add: divide_int_def [of k l] of_nat_div)
+
+lemma div_dvd_sgn_abs:
+  fixes k l :: int
+  assumes "l dvd k"
+  shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
+  using assms by (auto simp add: divide_int_def [of k l] of_nat_div)
+
+lemma div_noneq_sgn_abs:
+  fixes k l :: int
+  assumes "l \<noteq> 0"
+  assumes "sgn k \<noteq> sgn l"
+  shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
+  using assms
+  by (simp only: divide_int_def [of k l]) (auto simp add: of_nat_div sgn_0_0 dest!: sgn_not_eq_imp)
 
 lemma zdiv_zmult2_eq:
   \<open>a div (b * c) = (a div b) div c\<close> if \<open>c \<ge> 0\<close> for a b c :: int
@@ -2135,6 +2179,14 @@
     using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
 qed
 
+lemma zdiv_int:
+  "int (a div b) = int a div int b"
+  by (fact of_nat_div)
+
+lemma zmod_int:
+  "int (a mod b) = int a mod int b"
+  by (fact of_nat_mod)
+
 
 subsection \<open>Code generation\<close>
 
diff -r 77cbf472fcc9 -r 48d032035744 src/HOL/Library/Signed_Division.thy
--- a/src/HOL/Library/Signed_Division.thy	Thu Aug 18 09:29:11 2022 +0200
+++ b/src/HOL/Library/Signed_Division.thy	Wed Aug 17 20:37:16 2022 +0000
@@ -7,9 +7,58 @@
   imports Main
 begin
 
-class signed_division =
-  fixes signed_divide :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl "sdiv" 70)
-  and signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl "smod" 70)
+lemma sgn_div_eq_sgn_mult:
+  \<open>sgn (a div b) = sgn (a * b)\<close>
+  if \<open>a div b \<noteq> 0\<close> for a b :: int
+proof -
+  have \<open>0 \<le> \<bar>a\<bar> div \<bar>b\<bar>\<close>
+    by (cases \<open>b = 0\<close>) (simp_all add: pos_imp_zdiv_nonneg_iff)
+  then have \<open>\<bar>a\<bar> div \<bar>b\<bar> \<noteq> 0 \<longleftrightarrow> 0 < \<bar>a\<bar> div \<bar>b\<bar>\<close>
+    by (simp add: less_le)
+  also have \<open>\<dots> \<longleftrightarrow> \<bar>a\<bar> \<ge> \<bar>b\<bar>\<close>
+    using that nonneg1_imp_zdiv_pos_iff by auto
+  finally have *: \<open>\<bar>a\<bar> div \<bar>b\<bar> \<noteq> 0 \<longleftrightarrow> \<bar>b\<bar> \<le> \<bar>a\<bar>\<close> .
+  show ?thesis
+    using \<open>0 \<le> \<bar>a\<bar> div \<bar>b\<bar>\<close> that
+  by (auto simp add: div_eq_div_abs [of a b] div_eq_sgn_abs [of a b]
+    sgn_mult sgn_1_pos sgn_1_neg sgn_eq_0_iff nonneg1_imp_zdiv_pos_iff * dest: sgn_not_eq_imp)
+qed
+
+class signed_division = comm_semiring_1_cancel +
+  fixes signed_divide :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>sdiv\<close> 70)
+  and signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>smod\<close> 70)
+  assumes sdiv_mult_smod_eq: \<open>a sdiv b * b + a smod b = a\<close>
+begin
+
+lemma mult_sdiv_smod_eq:
+  \<open>b * (a sdiv b) + a smod b = a\<close>
+  using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps)
+
+lemma smod_sdiv_mult_eq:
+  \<open>a smod b + a sdiv b * b = a\<close>
+  using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps)
+
+lemma smod_mult_sdiv_eq:
+  \<open>a smod b + b * (a sdiv b) = a\<close>
+  using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps)
+
+lemma minus_sdiv_mult_eq_smod:
+  \<open>a - a sdiv b * b = a smod b\<close>
+  by (rule add_implies_diff [symmetric]) (fact smod_sdiv_mult_eq)
+
+lemma minus_mult_sdiv_eq_smod:
+  \<open>a - b * (a sdiv b) = a smod b\<close>
+  by (rule add_implies_diff [symmetric]) (fact smod_mult_sdiv_eq)
+
+lemma minus_smod_eq_sdiv_mult:
+  \<open>a - a smod b = a sdiv b * b\<close>
+  by (rule add_implies_diff [symmetric]) (fact sdiv_mult_smod_eq)
+
+lemma minus_smod_eq_mult_sdiv:
+  \<open>a - a smod b = b * (a sdiv b)\<close>
+  by (rule add_implies_diff [symmetric]) (fact mult_sdiv_smod_eq)
+
+end
 
 instantiation int :: signed_division
 begin
@@ -18,12 +67,45 @@
   where \<open>k sdiv l = sgn k * sgn l * (\<bar>k\<bar> div \<bar>l\<bar>)\<close> for k l :: int
 
 definition signed_modulo_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
-  where \<open>k smod l = k - (k sdiv l) * l\<close> for k l :: int
+  where \<open>k smod l = sgn k * (\<bar>k\<bar> mod \<bar>l\<bar>)\<close> for k l :: int
 
-instance ..
+instance by standard
+  (simp add: signed_divide_int_def signed_modulo_int_def div_abs_eq mod_abs_eq algebra_simps)
 
 end
 
+lemma divide_int_eq_signed_divide_int:
+  \<open>k div l = k sdiv l - of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+  for k l :: int
+  by (simp add: div_eq_div_abs [of k l] signed_divide_int_def)
+
+lemma signed_divide_int_eq_divide_int:
+  \<open>k sdiv l = k div l + of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+  for k l :: int
+  by (simp add: divide_int_eq_signed_divide_int)
+
+lemma modulo_int_eq_signed_modulo_int:
+  \<open>k mod l = k smod l + l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+  for k l :: int
+  by (simp add: mod_eq_mod_abs [of k l] signed_modulo_int_def)
+
+lemma signed_modulo_int_eq_modulo_int:
+  \<open>k smod l = k mod l - l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+  for k l :: int
+  by (simp add: modulo_int_eq_signed_modulo_int)
+
+lemma sdiv_int_div_0:
+  "(x :: int) sdiv 0 = 0"
+  by (clarsimp simp: signed_divide_int_def)
+
+lemma sdiv_int_0_div [simp]:
+  "0 sdiv (x :: int) = 0"
+  by (clarsimp simp: signed_divide_int_def)
+
+lemma smod_int_alt_def:
+     "(a::int) smod b = sgn (a) * (abs a mod abs b)"
+  by (fact signed_modulo_int_def)
+
 lemma int_sdiv_simps [simp]:
     "(a :: int) sdiv 1 = a"
     "(a :: int) sdiv 0 = 0"
@@ -31,11 +113,13 @@
   apply (auto simp: signed_divide_int_def sgn_if)
   done
 
-lemma sgn_div_eq_sgn_mult:
-    "a div b \<noteq> 0 \<Longrightarrow> sgn ((a :: int) div b) = sgn (a * b)"
-  apply (clarsimp simp: sgn_if zero_le_mult_iff neg_imp_zdiv_nonneg_iff not_less)
-  apply (metis less_le mult_le_0_iff neg_imp_zdiv_neg_iff not_less pos_imp_zdiv_neg_iff zdiv_eq_0_iff)
-  done
+lemma smod_int_mod_0 [simp]:
+  "x smod (0 :: int) = x"
+  by (clarsimp simp: signed_modulo_int_def abs_mult_sgn ac_simps)
+
+lemma smod_int_0_mod [simp]:
+  "0 smod (x :: int) = 0"
+  by (clarsimp simp: smod_int_alt_def)
 
 lemma sgn_sdiv_eq_sgn_mult:
   "a sdiv b \<noteq> 0 \<Longrightarrow> sgn ((a :: int) sdiv b) = sgn (a * b)"
@@ -71,38 +155,17 @@
   done
 
 lemma sdiv_int_range:
-    "(a :: int) sdiv b \<in> { - (abs a) .. (abs a) }"
-  apply (unfold signed_divide_int_def)
-  apply (subgoal_tac "(abs a) div (abs b) \<le> (abs a)")
-   apply (auto simp add: sgn_if not_less)
-      apply (metis le_less le_less_trans neg_equal_0_iff_equal neg_less_iff_less not_le pos_imp_zdiv_neg_iff)
-     apply (metis add.inverse_neutral div_int_pos_iff le_less neg_le_iff_le order_trans)
-    apply (metis div_minus_right le_less_trans neg_imp_zdiv_neg_iff neg_less_0_iff_less not_le)
-  using div_int_pos_iff apply fastforce
-  apply (auto simp add: abs_if not_less)
-     apply (metis add.inverse_inverse add_0_left div_by_1 div_minus_right less_le neg_0_le_iff_le not_le not_one_le_zero zdiv_mono2 zless_imp_add1_zle)
-    apply (metis div_by_1 neg_0_less_iff_less pos_imp_zdiv_pos_iff zdiv_mono2 zero_less_one)
-   apply (metis add.inverse_neutral div_by_0 div_by_1 int_div_less_self int_one_le_iff_zero_less less_le less_minus_iff order_refl)
-  apply (metis div_by_1 divide_int_def int_div_less_self less_le linorder_neqE_linordered_idom order_refl unique_euclidean_semiring_numeral_class.div_less)
-  done
-
-lemma sdiv_int_div_0 [simp]:
-  "(x :: int) sdiv 0 = 0"
-  by (clarsimp simp: signed_divide_int_def)
-
-lemma sdiv_int_0_div [simp]:
-  "0 sdiv (x :: int) = 0"
-  by (clarsimp simp: signed_divide_int_def)
-
-lemma smod_int_alt_def:
-     "(a::int) smod b = sgn (a) * (abs a mod abs b)"
-  apply (clarsimp simp: signed_modulo_int_def signed_divide_int_def)
-  apply (clarsimp simp: minus_div_mult_eq_mod [symmetric] abs_sgn sgn_mult sgn_if algebra_split_simps)
-  done
+  \<open>a sdiv b \<in> {- \<bar>a\<bar>..\<bar>a\<bar>}\<close> for a b :: int
+  using zdiv_mono2 [of \<open>\<bar>a\<bar>\<close> 1 \<open>\<bar>b\<bar>\<close>]
+  by (cases \<open>b = 0\<close>; cases \<open>sgn b = sgn a\<close>)
+     (auto simp add: signed_divide_int_def pos_imp_zdiv_nonneg_iff
+     dest!: sgn_not_eq_imp intro: order_trans [of _ 0])
 
 lemma smod_int_range:
-  "b \<noteq> 0 \<Longrightarrow> (a::int) smod b \<in> { - abs b + 1 .. abs b - 1 }"
-  apply (case_tac  "b > 0")
+  \<open>a smod b \<in> {- \<bar>b\<bar> + 1..\<bar>b\<bar> - 1}\<close>
+  if \<open>b \<noteq> 0\<close> for a b :: int
+  using that
+  apply (cases \<open>b > 0\<close>)
    apply (insert pos_mod_conj [where a=a and b=b])[1]
    apply (insert pos_mod_conj [where a="-a" and b=b])[1]
    apply (auto simp: smod_int_alt_def algebra_simps sgn_if
@@ -129,14 +192,6 @@
   apply (auto simp: add1_zle_eq smod_int_alt_def sgn_if)
   done
 
-lemma smod_int_mod_0 [simp]:
-  "x smod (0 :: int) = x"
-  by (clarsimp simp: signed_modulo_int_def)
-
-lemma smod_int_0_mod [simp]:
-  "0 smod (x :: int) = 0"
-  by (clarsimp simp: smod_int_alt_def)
-
 lemma smod_mod_positive:
     "\<lbrakk> 0 \<le> (a :: int); 0 \<le> b \<rbrakk> \<Longrightarrow> a smod b = a mod b"
   by (clarsimp simp: smod_int_alt_def zsgn_def)
diff -r 77cbf472fcc9 -r 48d032035744 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Thu Aug 18 09:29:11 2022 +0200
+++ b/src/HOL/Rings.thy	Wed Aug 17 20:37:16 2022 +0000
@@ -2567,6 +2567,10 @@
   "sgn a * sgn a = of_bool (a \<noteq> 0)"
   by (cases "a > 0") simp_all
 
+lemma left_sgn_mult_self_eq [simp]:
+  \<open>sgn a * (sgn a * b) = of_bool (a \<noteq> 0) * b\<close>
+  by (simp flip: mult.assoc)
+
 lemma abs_mult_self_eq [simp]:
   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
   by (cases "a > 0") simp_all