# HG changeset patch
# User haftmann
# Date 1661062703 0
# Node ID d2e6a1342c90aa18404587cbd2e5a0cd53529bc1
# Parent  06eb4d0031e32b36419341b1b5fa8ce96b92b7ff
simplified computation algorithm construction

diff -r 06eb4d0031e3 -r d2e6a1342c90 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sat Aug 20 21:34:55 2022 +0200
+++ b/src/HOL/Code_Numeral.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -378,7 +378,7 @@
 
 end
 
-instantiation integer :: unique_euclidean_semiring_numeral
+instantiation integer :: unique_euclidean_semiring_with_nat_division
 begin
 
 definition divmod_integer :: "num \<Rightarrow> num \<Rightarrow> integer \<times> integer"
@@ -388,27 +388,11 @@
 definition divmod_step_integer :: "integer \<Rightarrow> integer \<times> integer \<Rightarrow> integer \<times> integer"
 where
   "divmod_step_integer l qr = (let (q, r) = qr
-    in if r \<ge> l then (2 * q + 1, r - l)
+    in if \<bar>l\<bar> \<le> \<bar>r\<bar> then (2 * q + 1, r - l)
     else (2 * q, r))"
 
-instance proof
-  show "divmod m n = (numeral m div numeral n :: integer, numeral m mod numeral n)"
-    for m n by (fact divmod_integer'_def)
-  show "divmod_step l qr = (let (q, r) = qr
-    in if r \<ge> l then (2 * q + 1, r - l)
-    else (2 * q, r))" for l and qr :: "integer \<times> integer"
-    by (fact divmod_step_integer_def)
-qed (transfer,
-  fact le_add_diff_inverse2
-  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)+
+instance by standard
+  (auto simp add: divmod_integer'_def divmod_step_integer_def integer_less_eq_iff)
 
 end
 
diff -r 06eb4d0031e3 -r d2e6a1342c90 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat Aug 20 21:34:55 2022 +0200
+++ b/src/HOL/Divides.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -546,118 +546,35 @@
 text \<open>
   The following type class contains everything necessary to formulate
   a division algorithm in ring structures with numerals, restricted
-  to its positive segments.  This is its primary motivation, and it
-  could surely be formulated using a more fine-grained, more algebraic
-  and less technical class hierarchy.
+  to its positive segments.
 \<close>
 
-class unique_euclidean_semiring_numeral = unique_euclidean_semiring_with_nat + 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"
-    and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
-    and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
-    and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
-    and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
-    and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
-  assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
-  fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
-    and divmod_step :: "'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
-  assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
-    and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
-    in if r \<ge> l then (2 * q + 1, r - l)
-    else (2 * q, r))"
-    \<comment> \<open>These are conceptually definitions but force generated code
-    to be monomorphic wrt. particular instances of this class which
-    yields a significant speedup.\<close>
+class unique_euclidean_semiring_with_nat_division = unique_euclidean_semiring_with_nat +
+  fixes divmod :: \<open>num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a\<close>
+    and divmod_step :: \<open>'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a\<close> \<comment> \<open>
+      These are conceptually definitions but force generated code
+      to be monomorphic wrt. particular instances of this class which
+      yields a significant speedup.\<close>
+  assumes divmod_def: \<open>divmod m n = (numeral m div numeral n, numeral m mod numeral n)\<close>
+    and divmod_step_def [simp]: \<open>divmod_step l (q, r) =
+      (if euclidean_size l \<le> euclidean_size r then (2 * q + 1, r - l)
+       else (2 * q, r))\<close> \<comment> \<open>
+         This is a formulation of one step (referring to one digit position)
+         in school-method division: compare the dividend at the current
+         digit position with the remainder from previous division steps
+         and evaluate accordingly.\<close>
 begin
 
-lemma divmod_digit_1:
-  assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
-  shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
-    and "a mod (2 * b) - b = a mod b" (is "?Q")
-proof -
-  from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
-    by (auto intro: trans)
-  with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
-  then have [simp]: "1 \<le> a div b" by (simp add: discrete)
-  with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
-  define w where "w = a div b mod 2"
-  then have w_exhaust: "w = 0 \<or> w = 1" by auto
-  have mod_w: "a mod (2 * b) = a mod b + b * w"
-    by (simp add: w_def mod_mult2_eq ac_simps)
-  from assms w_exhaust have "w = 1"
-    using mod_less by (auto simp add: mod_w)
-  with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
-  have "2 * (a div (2 * b)) = a div b - w"
-    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
-  with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
-  then show ?P and ?Q
-    by (simp_all add: div mod add_implies_diff [symmetric])
-qed
-
-lemma divmod_digit_0:
-  assumes "0 < b" and "a mod (2 * b) < b"
-  shows "2 * (a div (2 * b)) = a div b" (is "?P")
-    and "a mod (2 * b) = a mod b" (is "?Q")
-proof -
-  define w where "w = a div b mod 2"
-  then have w_exhaust: "w = 0 \<or> w = 1" by auto
-  have mod_w: "a mod (2 * b) = a mod b + b * w"
-    by (simp add: w_def mod_mult2_eq ac_simps)
-  moreover have "b \<le> a mod b + b"
-  proof -
-    from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
-    then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
-    then show ?thesis by simp
-  qed
-  moreover note assms w_exhaust
-  ultimately have "w = 0" by auto
-  with mod_w have mod: "a mod (2 * b) = a mod b" by simp
-  have "2 * (a div (2 * b)) = a div b - w"
-    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
-  with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
-  then show ?P and ?Q
-    by (simp_all add: div mod)
-qed
-
-lemma mod_double_modulus:
-  assumes "m > 0" "x \<ge> 0"
-  shows   "x mod (2 * m) = x mod m \<or> x mod (2 * m) = x mod m + m"
-proof (cases "x mod (2 * m) < m")
-  case True
-  thus ?thesis using assms using divmod_digit_0(2)[of m x] by auto
-next
-  case False
-  hence *: "x mod (2 * m) - m = x mod m"
-    using assms by (intro divmod_digit_1) auto
-  hence "x mod (2 * m) = x mod m + m"
-    by (subst * [symmetric], subst le_add_diff_inverse2) (use False in auto)
-  thus ?thesis by simp
-qed
-
 lemma fst_divmod:
-  "fst (divmod m n) = numeral m div numeral n"
+  \<open>fst (divmod m n) = numeral m div numeral n\<close>
   by (simp add: divmod_def)
 
 lemma snd_divmod:
-  "snd (divmod m n) = numeral m mod numeral n"
+  \<open>snd (divmod m n) = numeral m mod numeral n\<close>
   by (simp add: divmod_def)
 
 text \<open>
-  This is a formulation of one step (referring to one digit position)
-  in school-method division: compare the dividend at the current
-  digit position with the remainder from previous division steps
-  and evaluate accordingly.
-\<close>
-
-lemma divmod_step_eq [simp]:
-  "divmod_step l (q, r) = (if l \<le> r
-    then (2 * q + 1, r - l) else (2 * q, r))"
-  by (simp add: divmod_step_def)
-
-text \<open>
-  This is a formulation of school-method division.
+  Following a formulation of school-method division.
   If the divisor is smaller than the dividend, terminate.
   If not, shift the dividend to the right until termination
   occurs and then reiterate single division steps in the
@@ -665,48 +582,38 @@
 \<close>
 
 lemma divmod_divmod_step:
-  "divmod m n = (if m < n then (0, numeral m)
-    else divmod_step (numeral n) (divmod m (Num.Bit0 n)))"
-proof (cases "m < n")
-  case True then have "numeral m < numeral n" by simp
+  \<open>divmod m n = (if m < n then (0, numeral m)
+    else divmod_step (numeral n) (divmod m (Num.Bit0 n)))\<close>
+proof (cases \<open>m < n\<close>)
+  case True
   then show ?thesis
-    by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
+    by (simp add: prod_eq_iff fst_divmod snd_divmod flip: of_nat_numeral of_nat_div of_nat_mod)
 next
   case False
-  have "divmod m n =
-    divmod_step (numeral n) (numeral m div (2 * numeral n),
-      numeral m mod (2 * numeral n))"
-  proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
-    case True
-    with divmod_step_eq
-      have "divmod_step (numeral n) (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
-        (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
-        by simp
-    moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
-      have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
-      and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
-      by simp_all
-    ultimately show ?thesis by (simp only: divmod_def)
-  next
-    case False then have *: "numeral m mod (2 * numeral n) < numeral n"
-      by (simp add: not_le)
-    with divmod_step_eq
-      have "divmod_step (numeral n) (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
-        (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
-        by auto
-    moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
-      have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
-      and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
-      by (simp_all only: zero_less_numeral)
-    ultimately show ?thesis by (simp only: divmod_def)
-  qed
-  then have "divmod m n =
-    divmod_step (numeral n) (numeral m div numeral (Num.Bit0 n),
-      numeral m mod numeral (Num.Bit0 n))"
-    by (simp only: numeral.simps distrib mult_1)
-  then have "divmod m n = divmod_step (numeral n) (divmod m (Num.Bit0 n))"
-    by (simp add: divmod_def)
-  with False show ?thesis by simp
+  define r s t where \<open>r = (numeral m :: nat)\<close> \<open>s = (numeral n :: nat)\<close> \<open>t = 2 * s\<close>
+  then have *: \<open>numeral m = of_nat r\<close> \<open>numeral n = of_nat s\<close> \<open>numeral (num.Bit0 n) = of_nat t\<close>
+    and \<open>\<not> s \<le> r mod s\<close>
+    by (simp_all add: not_le)
+  have t: \<open>2 * (r div t) = r div s - r div s mod 2\<close>
+    \<open>r mod t = s * (r div s mod 2) + r mod s\<close>
+    by (simp add: Rings.minus_mod_eq_mult_div Groups.mult.commute [of 2] Euclidean_Division.div_mult2_eq \<open>t = 2 * s\<close>)
+      (use mod_mult2_eq [of r s 2] in \<open>simp add: ac_simps \<open>t = 2 * s\<close>\<close>)
+  have rs: \<open>r div s mod 2 = 0 \<or> r div s mod 2 = Suc 0\<close>
+    by auto
+  from \<open>\<not> s \<le> r mod s\<close> have \<open>s \<le> r mod t \<Longrightarrow>
+     r div s = Suc (2 * (r div t)) \<and>
+     r mod s = r mod t - s\<close>
+    using rs
+    by (auto simp add: t)
+  moreover have \<open>r mod t < s \<Longrightarrow>
+     r div s = 2 * (r div t) \<and>
+     r mod s = r mod t\<close>
+    using rs
+    by (auto simp add: t)
+  ultimately show ?thesis
+    by (simp add: divmod_def prod_eq_iff split_def Let_def
+	    not_less mod_eq_0_iff_dvd Rings.mod_eq_0_iff_dvd False not_le *)
+    (simp add: flip: of_nat_numeral of_nat_mult add.commute [of 1] of_nat_div of_nat_mod of_nat_Suc of_nat_diff)
 qed
 
 text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
@@ -720,17 +627,18 @@
 text \<open>Division by an even number is a right-shift\<close>
 
 lemma divmod_cancel [simp]:
-  "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
-  "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
+  \<open>divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))\<close> (is ?P)
+  \<open>divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))\<close> (is ?Q)
 proof -
-  have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
-    "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
-    by (simp_all only: numeral_mult numeral.simps distrib) simp_all
-  have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
-  then show ?P and ?Q
-    by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
-      div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
-      add.commute del: numeral_times_numeral)
+  define r s where \<open>r = (numeral m :: nat)\<close> \<open>s = (numeral n :: nat)\<close>
+  then have *: \<open>numeral m = of_nat r\<close> \<open>numeral n = of_nat s\<close>
+    \<open>numeral (num.Bit0 m) = of_nat (2 * r)\<close> \<open>numeral (num.Bit0 n) = of_nat (2 * s)\<close>
+    \<open>numeral (num.Bit1 m) = of_nat (Suc (2 * r))\<close>
+    by simp_all
+  show ?P and ?Q
+    by (simp_all add: divmod_def *)
+      (simp_all flip: of_nat_numeral of_nat_div of_nat_mod of_nat_mult add.commute [of 1] of_nat_Suc
+       add: Euclidean_Division.mod_mult_mult1 div_mult2_eq [of _ 2] mod_mult2_eq [of _ 2])
 qed
 
 text \<open>The really hard work\<close>
@@ -748,7 +656,7 @@
                (num.Bit0 (num.Bit1 n))))"
   by (simp_all add: divmod_divmod_step)
 
-lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps  
+lemmas divmod_algorithm_code = divmod_trivial divmod_cancel divmod_steps
 
 text \<open>Special case: divisibility\<close>
 
@@ -815,9 +723,7 @@
 
 end
 
-hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
-
-instantiation nat :: unique_euclidean_semiring_numeral
+instantiation nat :: unique_euclidean_semiring_with_nat_division
 begin
 
 definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
@@ -830,8 +736,8 @@
     in if r \<ge> l then (2 * q + 1, r - l)
     else (2 * q, r))"
 
-instance by standard
-  (auto simp add: divmod'_nat_def divmod_step_nat_def div_greater_zero_iff div_mult2_eq mod_mult2_eq)
+instance
+  by standard (simp_all add: divmod'_nat_def divmod_step_nat_def)
 
 end
 
@@ -847,7 +753,7 @@
   shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
   by (simp_all add: snd_divmod)
 
-instantiation int :: unique_euclidean_semiring_numeral
+instantiation int :: unique_euclidean_semiring_with_nat_division
 begin
 
 definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
@@ -857,12 +763,11 @@
 definition divmod_step_int :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
 where
   "divmod_step_int l qr = (let (q, r) = qr
-    in if r \<ge> l then (2 * q + 1, r - l)
+    in if \<bar>l\<bar> \<le> \<bar>r\<bar> then (2 * q + 1, r - l)
     else (2 * q, r))"
 
 instance
-  by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
-    pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq)
+  by standard (auto simp add: divmod_int_def divmod_step_int_def)
 
 end
 
@@ -955,11 +860,19 @@
 
 lemma div_positive_int:
   "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
-  using that div_positive [of l k] by blast
+  using that by (simp add: nonneg1_imp_zdiv_pos_iff)
 
 
 subsubsection \<open>Dedicated simproc for calculation\<close>
 
+lemma euclidean_size_nat_less_eq_iff:
+  \<open>euclidean_size m \<le> euclidean_size n \<longleftrightarrow> m \<le> n\<close> for m n :: nat
+  by simp
+
+lemma euclidean_size_int_less_eq_iff:
+  \<open>euclidean_size k \<le> euclidean_size l \<longleftrightarrow> \<bar>k\<bar> \<le> \<bar>l\<bar>\<close> for k l :: int
+  by auto
+
 text \<open>
   There is space for improvement here: the calculation itself
   could be carried out outside the logic, and a generic simproc
@@ -967,23 +880,23 @@
 \<close>
 
 simproc_setup numeral_divmod
-  ("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 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
+   "0 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
    "0 div - 1 :: int" | "0 mod - 1 :: int" |
-   "0 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
+   "0 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
    "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
-   "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 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
+   "1 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
    "1 div - 1 :: int" | "1 mod - 1 :: int" |
-   "1 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
+   "1 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
    "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 :: 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 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
+   "numeral a div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
    "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
-   "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 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
    "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" |
@@ -1005,9 +918,10 @@
         numeral_div_minus_numeral numeral_mod_minus_numeral
         div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
         numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
-        divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One
+        divmod_cancel divmod_steps divmod_step_def fst_conv snd_conv numeral_One
         case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
-        minus_minus numeral_times_numeral mult_zero_right mult_1_right}
+        minus_minus numeral_times_numeral mult_zero_right mult_1_right
+        euclidean_size_nat_less_eq_iff euclidean_size_int_less_eq_iff diff_nat_numeral nat_numeral}
         @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
       fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
         (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
@@ -1066,6 +980,94 @@
 
 subsection \<open>Lemmas of doubtful value\<close>
 
+class unique_euclidean_semiring_numeral = unique_euclidean_semiring_with_nat + 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"
+    and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
+    and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
+    and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
+    and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
+    and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
+  assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
+begin
+
+lemma divmod_digit_1:
+  assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
+  shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
+    and "a mod (2 * b) - b = a mod b" (is "?Q")
+proof -
+  from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
+    by (auto intro: trans)
+  with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
+  then have [simp]: "1 \<le> a div b" by (simp add: discrete)
+  with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
+  define w where "w = a div b mod 2"
+  then have w_exhaust: "w = 0 \<or> w = 1" by auto
+  have mod_w: "a mod (2 * b) = a mod b + b * w"
+    by (simp add: w_def mod_mult2_eq ac_simps)
+  from assms w_exhaust have "w = 1"
+    using mod_less by (auto simp add: mod_w)
+  with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
+  have "2 * (a div (2 * b)) = a div b - w"
+    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
+  with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
+  then show ?P and ?Q
+    by (simp_all add: div mod add_implies_diff [symmetric])
+qed
+
+lemma divmod_digit_0:
+  assumes "0 < b" and "a mod (2 * b) < b"
+  shows "2 * (a div (2 * b)) = a div b" (is "?P")
+    and "a mod (2 * b) = a mod b" (is "?Q")
+proof -
+  define w where "w = a div b mod 2"
+  then have w_exhaust: "w = 0 \<or> w = 1" by auto
+  have mod_w: "a mod (2 * b) = a mod b + b * w"
+    by (simp add: w_def mod_mult2_eq ac_simps)
+  moreover have "b \<le> a mod b + b"
+  proof -
+    from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
+    then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
+    then show ?thesis by simp
+  qed
+  moreover note assms w_exhaust
+  ultimately have "w = 0" by auto
+  with mod_w have mod: "a mod (2 * b) = a mod b" by simp
+  have "2 * (a div (2 * b)) = a div b - w"
+    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
+  with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
+  then show ?P and ?Q
+    by (simp_all add: div mod)
+qed
+
+lemma mod_double_modulus:
+  assumes "m > 0" "x \<ge> 0"
+  shows   "x mod (2 * m) = x mod m \<or> x mod (2 * m) = x mod m + m"
+proof (cases "x mod (2 * m) < m")
+  case True
+  thus ?thesis using assms using divmod_digit_0(2)[of m x] by auto
+next
+  case False
+  hence *: "x mod (2 * m) - m = x mod m"
+    using assms by (intro divmod_digit_1) auto
+  hence "x mod (2 * m) = x mod m + m"
+    by (subst * [symmetric], subst le_add_diff_inverse2) (use False in auto)
+  thus ?thesis by simp
+qed
+
+end
+
+hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
+
+instance nat :: unique_euclidean_semiring_numeral
+  by standard
+    (auto simp add: div_greater_zero_iff div_mult2_eq mod_mult2_eq)
+
+instance int :: unique_euclidean_semiring_numeral
+  by standard (auto intro: zmod_le_nonneg_dividend simp add:
+    pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq)
+
 lemma div_geq: "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
   by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
 
diff -r 06eb4d0031e3 -r d2e6a1342c90 src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Sat Aug 20 21:34:55 2022 +0200
+++ b/src/HOL/Library/IArray.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -148,8 +148,10 @@
     let l = k - 1 in p (sub' (as, l)) \<or> exists_upto p l as)"
 proof (cases "k \<ge> 1")
   case False
+  then have \<open>k \<le> 0\<close>
+    including integer.lifting by transfer simp
   then show ?thesis
-    by (auto simp add: not_le discrete)
+    by simp
 next
   case True
   then have less: "k \<le> 0 \<longleftrightarrow> False"
diff -r 06eb4d0031e3 -r d2e6a1342c90 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Sat Aug 20 21:34:55 2022 +0200
+++ b/src/HOL/SMT.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -445,7 +445,7 @@
 
 lemmas [smt_arith_simplify] =
     div_add dvd_numeral_simp divmod_steps less_num_simps le_num_simps if_True if_False divmod_cancel
-    dvd_mult dvd_mult2 less_irrefl prod.case numeral_plus_one divmod_step_eq order.refl le_zero_eq
+    dvd_mult dvd_mult2 less_irrefl prod.case numeral_plus_one divmod_step_def order.refl le_zero_eq
     le_numeral_simps less_numeral_simps mult.right_neutral simp_thms divides_aux_eq
     mult_nonneg_nonneg dvd_imp_mod_0 dvd_add zero_less_one mod_mult_self4 numeral_mod_numeral
     divmod_trivial prod.sel mult.left_neutral div_pos_pos_trivial arith_simps div_add div_mult_self1
@@ -453,7 +453,7 @@
     zero_neq_one zero_le_one le_num_simps add_Suc mod_div_trivial nat.distinct mult_minus_right
     add.inverse_inverse distrib_left_numeral mult_num_simps numeral_times_numeral add_num_simps
     divmod_steps rel_simps if_True if_False numeral_div_numeral divmod_cancel prod.case
-    add_num_simps one_plus_numeral fst_conv divmod_step_eq arith_simps sub_num_simps dbl_inc_simps
+    add_num_simps one_plus_numeral fst_conv arith_simps sub_num_simps dbl_inc_simps
     dbl_simps mult_1 add_le_cancel_right left_diff_distrib_numeral add_uminus_conv_diff zero_neq_one
     zero_le_one One_nat_def add_Suc mod_div_trivial nat.distinct of_int_1 numerals numeral_One
     of_int_numeral add_uminus_conv_diff zle_diff1_eq add_less_same_cancel2 minus_add_distrib