# HG changeset patch
# User haftmann
# Date 1661062703 0
# Node ID 02b18f59f903a80c9c69216a4b1ebb9c61f46824
# Parent  d2e6a1342c90aa18404587cbd2e5a0cd53529bc1
streamlined

diff -r d2e6a1342c90 -r 02b18f59f903 NEWS
--- a/NEWS	Sun Aug 21 06:18:23 2022 +0000
+++ b/NEWS	Sun Aug 21 06:18:23 2022 +0000
@@ -34,6 +34,9 @@
 
 *** HOL ***
 
+* Moved auxiliary computation constant "divmod_nat" to theory
+"Euclidean_Division".  Minor INCOMPATIBILITY.
+
 * Renamed attribute "arith_split" to "linarith_split".  Minor
 INCOMPATIBILITY.
 
@@ -44,7 +47,7 @@
 integers, sacrificing pattern patching in exchange for dramatically
 increased performance for comparisons.
 
-* New theory HOL-Library.NList of fixed length lists
+* New theory HOL-Library.NList of fixed length lists.
 
 * Rule split_of_bool_asm is not split any longer, analogously to
 split_if_asm.  INCOMPATIBILITY.
diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Divides.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -541,439 +541,6 @@
 qed
 
 
-subsection \<open>Numeral division with a pragmatic type class\<close>
-
-text \<open>
-  The following type class contains everything necessary to formulate
-  a division algorithm in ring structures with numerals, restricted
-  to its positive segments.
-\<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 fst_divmod:
-  \<open>fst (divmod m n) = numeral m div numeral n\<close>
-  by (simp add: divmod_def)
-
-lemma snd_divmod:
-  \<open>snd (divmod m n) = numeral m mod numeral n\<close>
-  by (simp add: divmod_def)
-
-text \<open>
-  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
-  opposite direction.
-\<close>
-
-lemma divmod_divmod_step:
-  \<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 fst_divmod snd_divmod flip: of_nat_numeral of_nat_div of_nat_mod)
-next
-  case False
-  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>
-
-lemma divmod_trivial [simp]:
-  "divmod m Num.One = (numeral m, 0)"
-  "divmod num.One (num.Bit0 n) = (0, Numeral1)"
-  "divmod num.One (num.Bit1 n) = (0, Numeral1)"
-  using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
-
-text \<open>Division by an even number is a right-shift\<close>
-
-lemma divmod_cancel [simp]:
-  \<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 -
-  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>
-
-lemma divmod_steps [simp]:
-  "divmod (num.Bit0 m) (num.Bit1 n) =
-      (if m \<le> n then (0, numeral (num.Bit0 m))
-       else divmod_step (numeral (num.Bit1 n))
-             (divmod (num.Bit0 m)
-               (num.Bit0 (num.Bit1 n))))"
-  "divmod (num.Bit1 m) (num.Bit1 n) =
-      (if m < n then (0, numeral (num.Bit1 m))
-       else divmod_step (numeral (num.Bit1 n))
-             (divmod (num.Bit1 m)
-               (num.Bit0 (num.Bit1 n))))"
-  by (simp_all add: divmod_divmod_step)
-
-lemmas divmod_algorithm_code = divmod_trivial divmod_cancel divmod_steps
-
-text \<open>Special case: divisibility\<close>
-
-definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
-where
-  "divides_aux qr \<longleftrightarrow> snd qr = 0"
-
-lemma divides_aux_eq [simp]:
-  "divides_aux (q, r) \<longleftrightarrow> r = 0"
-  by (simp add: divides_aux_def)
-
-lemma dvd_numeral_simp [simp]:
-  "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
-  by (simp add: divmod_def mod_eq_0_iff_dvd)
-
-text \<open>Generic computation of quotient and remainder\<close>  
-
-lemma numeral_div_numeral [simp]: 
-  "numeral k div numeral l = fst (divmod k l)"
-  by (simp add: fst_divmod)
-
-lemma numeral_mod_numeral [simp]: 
-  "numeral k mod numeral l = snd (divmod k l)"
-  by (simp add: snd_divmod)
-
-lemma one_div_numeral [simp]:
-  "1 div numeral n = fst (divmod num.One n)"
-  by (simp add: fst_divmod)
-
-lemma one_mod_numeral [simp]:
-  "1 mod numeral n = snd (divmod num.One n)"
-  by (simp add: snd_divmod)
-
-text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
-
-lemma cong_exp_iff_simps:
-  "numeral n mod numeral Num.One = 0
-    \<longleftrightarrow> True"
-  "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
-    \<longleftrightarrow> numeral n mod numeral q = 0"
-  "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
-    \<longleftrightarrow> False"
-  "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
-    \<longleftrightarrow> True"
-  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> True"
-  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> False"
-  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> (numeral n mod numeral q) = 0"
-  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> False"
-  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
-  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> False"
-  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> (numeral m mod numeral q) = 0"
-  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> False"
-  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
-  by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
-
-end
-
-instantiation nat :: unique_euclidean_semiring_with_nat_division
-begin
-
-definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
-where
-  divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
-
-definition divmod_step_nat :: "nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
-where
-  "divmod_step_nat l qr = (let (q, r) = qr
-    in if r \<ge> l then (2 * q + 1, r - l)
-    else (2 * q, r))"
-
-instance
-  by standard (simp_all add: divmod'_nat_def divmod_step_nat_def)
-
-end
-
-declare divmod_algorithm_code [where ?'a = nat, code]
-
-lemma Suc_0_div_numeral [simp]:
-  fixes k l :: num
-  shows "Suc 0 div numeral k = fst (divmod Num.One k)"
-  by (simp_all add: fst_divmod)
-
-lemma Suc_0_mod_numeral [simp]:
-  fixes k l :: num
-  shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
-  by (simp_all add: snd_divmod)
-
-instantiation int :: unique_euclidean_semiring_with_nat_division
-begin
-
-definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
-where
-  "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
-
-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 \<bar>l\<bar> \<le> \<bar>r\<bar> then (2 * q + 1, r - l)
-    else (2 * q, r))"
-
-instance
-  by standard (auto simp add: divmod_int_def divmod_step_int_def)
-
-end
-
-declare divmod_algorithm_code [where ?'a = int, code]
-
-context
-begin
-  
-qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
-where
-  "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
-
-qualified lemma adjust_div_eq [simp, code]:
-  "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
-  by (simp add: adjust_div_def)
-
-qualified definition adjust_mod :: "num \<Rightarrow> int \<Rightarrow> int"
-where
-  [simp]: "adjust_mod l r = (if r = 0 then 0 else numeral l - r)"
-
-lemma minus_numeral_div_numeral [simp]:
-  "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
-proof -
-  have "int (fst (divmod m n)) = fst (divmod m n)"
-    by (simp only: fst_divmod divide_int_def) auto
-  then show ?thesis
-    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
-qed
-
-lemma minus_numeral_mod_numeral [simp]:
-  "- numeral m mod numeral n = adjust_mod n (snd (divmod m n) :: int)"
-proof (cases "snd (divmod m n) = (0::int)")
-  case True
-  then show ?thesis
-    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
-next
-  case False
-  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
-    by (simp only: snd_divmod modulo_int_def) auto
-  then show ?thesis
-    by (simp add: divides_aux_def adjust_div_def)
-      (simp add: divides_aux_def modulo_int_def)
-qed
-
-lemma numeral_div_minus_numeral [simp]:
-  "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
-proof -
-  have "int (fst (divmod m n)) = fst (divmod m n)"
-    by (simp only: fst_divmod divide_int_def) auto
-  then show ?thesis
-    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
-qed
-  
-lemma numeral_mod_minus_numeral [simp]:
-  "numeral m mod - numeral n = - adjust_mod n (snd (divmod m n) :: int)"
-proof (cases "snd (divmod m n) = (0::int)")
-  case True
-  then show ?thesis
-    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
-next
-  case False
-  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
-    by (simp only: snd_divmod modulo_int_def) auto
-  then show ?thesis
-    by (simp add: divides_aux_def adjust_div_def)
-      (simp add: divides_aux_def modulo_int_def)
-qed
-
-lemma minus_one_div_numeral [simp]:
-  "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
-  using minus_numeral_div_numeral [of Num.One n] by simp  
-
-lemma minus_one_mod_numeral [simp]:
-  "- 1 mod numeral n = adjust_mod n (snd (divmod Num.One n) :: int)"
-  using minus_numeral_mod_numeral [of Num.One n] by simp
-
-lemma one_div_minus_numeral [simp]:
-  "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
-  using numeral_div_minus_numeral [of Num.One n] by simp
-  
-lemma one_mod_minus_numeral [simp]:
-  "1 mod - numeral n = - adjust_mod n (snd (divmod Num.One n) :: int)"
-  using numeral_mod_minus_numeral [of Num.One n] by simp
-
-end
-
-lemma divmod_BitM_2_eq [simp]:
-  \<open>divmod (Num.BitM m) (Num.Bit0 Num.One) = (numeral m - 1, (1 :: int))\<close>
-  by (cases m) simp_all
-
-lemma div_positive_int:
-  "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
-  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
-  (simplifier setup) for generic calculation would be helpful. 
-\<close>
-
-simproc_setup numeral_divmod
-  ("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_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_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_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_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_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" |
-   "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
-   "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
-   "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") =
-\<open> let
-    val if_cong = the (Code.get_case_cong \<^theory> \<^const_name>\<open>If\<close>);
-    fun successful_rewrite ctxt ct =
-      let
-        val thm = Simplifier.rewrite ctxt ct
-      in if Thm.is_reflexive thm then NONE else SOME thm end;
-  in fn phi =>
-    let
-      val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
-        one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
-        one_div_minus_numeral one_mod_minus_numeral
-        numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
-        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_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
-        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)
-    in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
-  end
-\<close>
-
-
-subsubsection \<open>Code generation\<close>
-
-definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
-  where "divmod_nat m n = (m div n, m mod n)"
-
-lemma fst_divmod_nat [simp]:
-  "fst (divmod_nat m n) = m div n"
-  by (simp add: divmod_nat_def)
-
-lemma snd_divmod_nat [simp]:
-  "snd (divmod_nat m n) = m mod n"
-  by (simp add: divmod_nat_def)
-
-lemma divmod_nat_if [code]:
-  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
-    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
-  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
-
-lemma [code]:
-  "m div n = fst (divmod_nat m n)"
-  "m mod n = snd (divmod_nat m n)"
-  by simp_all
-
-lemma [code]:
-  fixes k :: int
-  shows 
-    "k div 0 = 0"
-    "k mod 0 = k"
-    "0 div k = 0"
-    "0 mod k = 0"
-    "k div Int.Pos Num.One = k"
-    "k mod Int.Pos Num.One = 0"
-    "k div Int.Neg Num.One = - k"
-    "k mod Int.Neg Num.One = 0"
-    "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
-    "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
-    "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
-    "Int.Neg m mod Int.Pos n = Divides.adjust_mod n (snd (divmod m n) :: int)"
-    "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
-    "Int.Pos m mod Int.Neg n = - Divides.adjust_mod n (snd (divmod m n) :: int)"
-    "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
-    "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
-  by simp_all
-
 code_identifier
   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
@@ -1090,4 +657,8 @@
 lemma zmod_eq_0D [dest!]: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: int
   using that by auto
 
+lemma div_positive_int:
+  "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
+  using that by (simp add: nonneg1_imp_zdiv_pos_iff)
+
 end
diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Euclidean_Division.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -2290,7 +2290,402 @@
   using that by (simp add: modulo_int_def sgn_if)
 
 
-subsection \<open>Code generation\<close>
+subsection \<open>Generic symbolic computations\<close>
+
+text \<open>
+  The following type class contains everything necessary to formulate
+  a division algorithm in ring structures with numerals, restricted
+  to its positive segments.
+\<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 fst_divmod:
+  \<open>fst (divmod m n) = numeral m div numeral n\<close>
+  by (simp add: divmod_def)
+
+lemma snd_divmod:
+  \<open>snd (divmod m n) = numeral m mod numeral n\<close>
+  by (simp add: divmod_def)
+
+text \<open>
+  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
+  opposite direction.
+\<close>
+
+lemma divmod_divmod_step:
+  \<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 fst_divmod snd_divmod flip: of_nat_numeral of_nat_div of_nat_mod)
+next
+  case False
+  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>
+
+lemma divmod_trivial [simp]:
+  "divmod m Num.One = (numeral m, 0)"
+  "divmod num.One (num.Bit0 n) = (0, Numeral1)"
+  "divmod num.One (num.Bit1 n) = (0, Numeral1)"
+  using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
+
+text \<open>Division by an even number is a right-shift\<close>
+
+lemma divmod_cancel [simp]:
+  \<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 -
+  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
+  have **: \<open>Suc (2 * r) div 2 = r\<close>
+    by simp
+  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>
+
+lemma divmod_steps [simp]:
+  "divmod (num.Bit0 m) (num.Bit1 n) =
+      (if m \<le> n then (0, numeral (num.Bit0 m))
+       else divmod_step (numeral (num.Bit1 n))
+             (divmod (num.Bit0 m)
+               (num.Bit0 (num.Bit1 n))))"
+  "divmod (num.Bit1 m) (num.Bit1 n) =
+      (if m < n then (0, numeral (num.Bit1 m))
+       else divmod_step (numeral (num.Bit1 n))
+             (divmod (num.Bit1 m)
+               (num.Bit0 (num.Bit1 n))))"
+  by (simp_all add: divmod_divmod_step)
+
+lemmas divmod_algorithm_code = divmod_trivial divmod_cancel divmod_steps
+
+text \<open>Special case: divisibility\<close>
+
+definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
+where
+  "divides_aux qr \<longleftrightarrow> snd qr = 0"
+
+lemma divides_aux_eq [simp]:
+  "divides_aux (q, r) \<longleftrightarrow> r = 0"
+  by (simp add: divides_aux_def)
+
+lemma dvd_numeral_simp [simp]:
+  "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
+  by (simp add: divmod_def mod_eq_0_iff_dvd)
+
+text \<open>Generic computation of quotient and remainder\<close>  
+
+lemma numeral_div_numeral [simp]: 
+  "numeral k div numeral l = fst (divmod k l)"
+  by (simp add: fst_divmod)
+
+lemma numeral_mod_numeral [simp]: 
+  "numeral k mod numeral l = snd (divmod k l)"
+  by (simp add: snd_divmod)
+
+lemma one_div_numeral [simp]:
+  "1 div numeral n = fst (divmod num.One n)"
+  by (simp add: fst_divmod)
+
+lemma one_mod_numeral [simp]:
+  "1 mod numeral n = snd (divmod num.One n)"
+  by (simp add: snd_divmod)
+
+end
+
+instantiation nat :: unique_euclidean_semiring_with_nat_division
+begin
+
+definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
+where
+  divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
+
+definition divmod_step_nat :: "nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
+where
+  "divmod_step_nat l qr = (let (q, r) = qr
+    in if r \<ge> l then (2 * q + 1, r - l)
+    else (2 * q, r))"
+
+instance
+  by standard (simp_all add: divmod'_nat_def divmod_step_nat_def)
+
+end
+
+declare divmod_algorithm_code [where ?'a = nat, code]
+
+lemma Suc_0_div_numeral [simp]:
+  \<open>Suc 0 div numeral Num.One = 1\<close>
+  \<open>Suc 0 div numeral (Num.Bit0 n) = 0\<close>
+  \<open>Suc 0 div numeral (Num.Bit1 n) = 0\<close>
+  by simp_all
+
+lemma Suc_0_mod_numeral [simp]:
+  \<open>Suc 0 mod numeral Num.One = 0\<close>
+  \<open>Suc 0 mod numeral (Num.Bit0 n) = 1\<close>
+  \<open>Suc 0 mod numeral (Num.Bit1 n) = 1\<close>
+  by simp_all
+
+instantiation int :: unique_euclidean_semiring_with_nat_division
+begin
+
+definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
+where
+  "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
+
+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 \<bar>l\<bar> \<le> \<bar>r\<bar> then (2 * q + 1, r - l)
+    else (2 * q, r))"
+
+instance
+  by standard (auto simp add: divmod_int_def divmod_step_int_def)
+
+end
+
+declare divmod_algorithm_code [where ?'a = int, code]
+
+context
+begin
+  
+qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
+where
+  "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
+
+qualified lemma adjust_div_eq [simp, code]:
+  "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
+  by (simp add: adjust_div_def)
+
+qualified definition adjust_mod :: "num \<Rightarrow> int \<Rightarrow> int"
+where
+  [simp]: "adjust_mod l r = (if r = 0 then 0 else numeral l - r)"
+
+lemma minus_numeral_div_numeral [simp]:
+  "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
+proof -
+  have "int (fst (divmod m n)) = fst (divmod m n)"
+    by (simp only: fst_divmod divide_int_def) auto
+  then show ?thesis
+    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
+qed
+
+lemma minus_numeral_mod_numeral [simp]:
+  "- numeral m mod numeral n = adjust_mod n (snd (divmod m n) :: int)"
+proof (cases "snd (divmod m n) = (0::int)")
+  case True
+  then show ?thesis
+    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
+next
+  case False
+  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
+    by (simp only: snd_divmod modulo_int_def) auto
+  then show ?thesis
+    by (simp add: divides_aux_def adjust_div_def)
+      (simp add: divides_aux_def modulo_int_def)
+qed
+
+lemma numeral_div_minus_numeral [simp]:
+  "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
+proof -
+  have "int (fst (divmod m n)) = fst (divmod m n)"
+    by (simp only: fst_divmod divide_int_def) auto
+  then show ?thesis
+    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
+qed
+  
+lemma numeral_mod_minus_numeral [simp]:
+  "numeral m mod - numeral n = - adjust_mod n (snd (divmod m n) :: int)"
+proof (cases "snd (divmod m n) = (0::int)")
+  case True
+  then show ?thesis
+    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
+next
+  case False
+  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
+    by (simp only: snd_divmod modulo_int_def) auto
+  then show ?thesis
+    by (simp add: divides_aux_def adjust_div_def)
+      (simp add: divides_aux_def modulo_int_def)
+qed
+
+lemma minus_one_div_numeral [simp]:
+  "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
+  using minus_numeral_div_numeral [of Num.One n] by simp  
+
+lemma minus_one_mod_numeral [simp]:
+  "- 1 mod numeral n = adjust_mod n (snd (divmod Num.One n) :: int)"
+  using minus_numeral_mod_numeral [of Num.One n] by simp
+
+lemma one_div_minus_numeral [simp]:
+  "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
+  using numeral_div_minus_numeral [of Num.One n] by simp
+  
+lemma one_mod_minus_numeral [simp]:
+  "1 mod - numeral n = - adjust_mod n (snd (divmod Num.One n) :: int)"
+  using numeral_mod_minus_numeral [of Num.One n] by simp
+
+lemma [code]:
+  fixes k :: int
+  shows 
+    "k div 0 = 0"
+    "k mod 0 = k"
+    "0 div k = 0"
+    "0 mod k = 0"
+    "k div Int.Pos Num.One = k"
+    "k mod Int.Pos Num.One = 0"
+    "k div Int.Neg Num.One = - k"
+    "k mod Int.Neg Num.One = 0"
+    "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
+    "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
+    "Int.Neg m div Int.Pos n = - (adjust_div (divmod m n) :: int)"
+    "Int.Neg m mod Int.Pos n = adjust_mod n (snd (divmod m n) :: int)"
+    "Int.Pos m div Int.Neg n = - (adjust_div (divmod m n) :: int)"
+    "Int.Pos m mod Int.Neg n = - adjust_mod n (snd (divmod m n) :: int)"
+    "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
+    "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
+  by simp_all
+
+end
+
+lemma divmod_BitM_2_eq [simp]:
+  \<open>divmod (Num.BitM m) (Num.Bit0 Num.One) = (numeral m - 1, (1 :: int))\<close>
+  by (cases m) simp_all
+
+
+subsubsection \<open>Computation by simplification\<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
+
+simproc_setup numeral_divmod
+  ("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_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_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_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_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_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" |
+   "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
+   "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
+   "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") = \<open>
+  let
+    val if_cong = the (Code.get_case_cong \<^theory> \<^const_name>\<open>If\<close>);
+    fun successful_rewrite ctxt ct =
+      let
+        val thm = Simplifier.rewrite ctxt ct
+      in if Thm.is_reflexive thm then NONE else SOME thm end;
+  in fn phi =>
+    let
+      val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
+        one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
+        one_div_minus_numeral one_mod_minus_numeral
+        numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
+        numeral_div_minus_numeral numeral_mod_minus_numeral
+        div_minus_minus mod_minus_minus Euclidean_Division.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_def fst_conv snd_conv numeral_One
+        case_prod_beta rel_simps Euclidean_Division.adjust_mod_def div_minus1_right mod_minus1_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)
+    in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
+  end
+\<close> \<comment> \<open>
+  There is space for improvement here: the calculation itself
+  could be carried out outside the logic, and a generic simproc
+  (simplifier setup) for generic calculation would be helpful. 
+\<close>
+
+
+subsubsection \<open>Code generation\<close>
+
+context
+begin
+
+qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
+  where "divmod_nat m n = (m div n, m mod n)"
+
+qualified lemma divmod_nat_if [code]:
+  "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
+    let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
+  by (simp add: divmod_nat_def prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
+
+qualified lemma [code]:
+  "m div n = fst (divmod_nat m n)"
+  "m mod n = snd (divmod_nat m n)"
+  by (simp_all add: divmod_nat_def)
+
+end
 
 code_identifier
   code_module Euclidean_Division \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/Library/Code_Abstract_Char.thy
--- a/src/HOL/Library/Code_Abstract_Char.thy	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Library/Code_Abstract_Char.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -18,7 +18,7 @@
 
 lemma char_of_integer_code [code]:
   \<open>integer_of_char (char_of_integer k) = (if 0 \<le> k \<and> k < 256 then k else k mod 256)\<close>
-  by (simp add: integer_of_char_def char_of_integer_def take_bit_eq_mod unique_euclidean_semiring_numeral_class.mod_less)
+  by (simp add: integer_of_char_def char_of_integer_def integer_eq_iff integer_less_eq_iff integer_less_iff)
 
 lemma of_char_code [code]:
   \<open>of_char c = of_nat (nat_of_integer (integer_of_char c))\<close>
@@ -104,7 +104,7 @@
   then have \<open>(0 :: integer) \<le> of_char c\<close>
     by (simp only: of_nat_0 of_nat_of_char)
   ultimately show ?thesis
-    by (simp add: Let_def integer_of_char_def take_bit_eq_mod unique_euclidean_semiring_numeral_class.mod_less)
+    by (simp add: Let_def integer_of_char_def take_bit_eq_mod integer_eq_iff integer_less_eq_iff integer_less_iff)
 next
   case False
   then have \<open>(128 :: integer) \<le> of_char c\<close>
@@ -117,7 +117,7 @@
   then have \<open>of_char c = k + 128\<close>
     by simp
   ultimately show ?thesis
-    by (simp add: Let_def integer_of_char_def take_bit_eq_mod unique_euclidean_semiring_numeral_class.mod_less)
+    by (simp add: Let_def integer_of_char_def take_bit_eq_mod integer_eq_iff integer_less_eq_iff integer_less_iff)
 qed    
 
 lemma equal_char_code [code]:
diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/Library/Code_Binary_Nat.thy
--- a/src/HOL/Library/Code_Binary_Nat.thy	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Library/Code_Binary_Nat.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -127,13 +127,13 @@
   "nat_of_num k < nat_of_num l \<longleftrightarrow> k < l"
   by (simp_all add: nat_of_num_numeral)
 
-declare [[code drop: Divides.divmod_nat]]
+declare [[code drop: Euclidean_Division.divmod_nat]]
   
 lemma divmod_nat_code [code]:
-  "Divides.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
-  "Divides.divmod_nat m 0 = (0, m)"
-  "Divides.divmod_nat 0 n = (0, 0)"
-  by (simp_all add: prod_eq_iff nat_of_num_numeral)
+  "Euclidean_Division.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
+  "Euclidean_Division.divmod_nat m 0 = (0, m)"
+  "Euclidean_Division.divmod_nat 0 n = (0, 0)"
+  by (simp_all add: Euclidean_Division.divmod_nat_def nat_of_num_numeral)
 
 end
 
diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Library/Code_Target_Nat.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -98,13 +98,13 @@
 begin
 
 lemma divmod_nat_code [code]: \<^marker>\<open>contributor \<open>René Thiemann\<close>\<close> \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
-  "Divides.divmod_nat m n = (
+  "Euclidean_Division.divmod_nat m n = (
      let k = integer_of_nat m; l = integer_of_nat n
      in map_prod nat_of_integer nat_of_integer
        (if k = 0 then (0, 0)
         else if l = 0 then (0, k) else
           Code_Numeral.divmod_abs k l))"
-  by (simp add: prod_eq_iff Let_def; transfer)
+  by (simp add: prod_eq_iff Let_def Euclidean_Division.divmod_nat_def; transfer)
     (simp add: nat_div_distrib nat_mod_distrib)
 
 end
@@ -136,15 +136,12 @@
 lemma (in semiring_1) of_nat_code_if:
   "of_nat n = (if n = 0 then 0
      else let
-       (m, q) = Divides.divmod_nat n 2;
+       (m, q) = Euclidean_Division.divmod_nat n 2;
        m' = 2 * of_nat m
      in if q = 0 then m' else m' + 1)"
-proof -
-  from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
-  show ?thesis
-    by (simp add: Let_def divmod_nat_def of_nat_add [symmetric])
-      (simp add: * mult.commute of_nat_mult add.commute)
-qed
+  by (cases n)
+    (simp_all add: Let_def Euclidean_Division.divmod_nat_def ac_simps
+      flip: of_nat_numeral of_nat_mult minus_mod_eq_mult_div)
 
 declare of_nat_code_if [code]
 
diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Library/RBT_Impl.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -1154,24 +1154,24 @@
     else if n = 1 then
       case kvs of (k, v) # kvs' \<Rightarrow> 
         (Branch R Empty k v Empty, kvs')
-    else let (n', r) = Divides.divmod_nat n 2 in
+    else let (n', r) = Euclidean_Division.divmod_nat n 2 in
       if r = 0 then
         case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
       else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))"
-by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_def prod.case)
+by (subst rbtreeify_f.simps) (simp only: Let_def Euclidean_Division.divmod_nat_def prod.case)
 
 lemma rbtreeify_g_code [code]:
   "rbtreeify_g n kvs =
    (if n = 0 \<or> n = 1 then (Empty, kvs)
-    else let (n', r) = Divides.divmod_nat n 2 in
+    else let (n', r) = Euclidean_Division.divmod_nat n 2 in
       if r = 0 then
         case rbtreeify_g n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
       else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))"
-by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_def prod.case)
+by(subst rbtreeify_g.simps)(simp only: Let_def Euclidean_Division.divmod_nat_def prod.case)
 
 lemma Suc_double_half: "Suc (2 * n) div 2 = n"
 by simp
diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/Matrix_LP/ComputeNumeral.thy
--- a/src/HOL/Matrix_LP/ComputeNumeral.thy	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Matrix_LP/ComputeNumeral.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -51,10 +51,10 @@
   one_div_minus_numeral one_mod_minus_numeral
   numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
   numeral_div_minus_numeral numeral_mod_minus_numeral
-  div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
+  div_minus_minus mod_minus_minus Euclidean_Division.adjust_div_eq of_bool_eq one_neq_zero
   numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
-  divmod_steps divmod_cancel divmod_step_eq fst_conv snd_conv numeral_One
-  case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
+  divmod_steps divmod_cancel divmod_step_def fst_conv snd_conv numeral_One
+  case_prod_beta rel_simps Euclidean_Division.adjust_mod_def div_minus1_right mod_minus1_right
   minus_minus numeral_times_numeral mult_zero_right mult_1_right
 
 
diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Parity.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -669,6 +669,44 @@
 
 end
 
+
+subsection \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
+
+context unique_euclidean_semiring_with_nat_division
+begin
+
+lemma cong_exp_iff_simps:
+  "numeral n mod numeral Num.One = 0
+    \<longleftrightarrow> True"
+  "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
+    \<longleftrightarrow> numeral n mod numeral q = 0"
+  "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
+    \<longleftrightarrow> False"
+  "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
+    \<longleftrightarrow> True"
+  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> True"
+  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> False"
+  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> (numeral n mod numeral q) = 0"
+  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> False"
+  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
+  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> False"
+  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> (numeral m mod numeral q) = 0"
+  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> False"
+  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
+  by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
+
+end
+
+
 code_identifier
   code_module Parity \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/ROOT	Sun Aug 21 06:18:23 2022 +0000
@@ -74,6 +74,7 @@
     Datatype_Records
     (*data refinements and dependent applications*)
     AList_Mapping
+    Code_Abstract_Char
     Code_Binary_Nat
     Code_Prolog
     Code_Real_Approx_By_Float
diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/ex/Parallel_Example.thy
--- a/src/HOL/ex/Parallel_Example.thy	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/ex/Parallel_Example.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -41,11 +41,11 @@
 proof -
   fix ps qs q
   assume "dropWhile Not ps = q # qs"
-  then have "length (q # qs) = length (dropWhile Not ps)" by simp
-  then have "length qs < length (dropWhile Not ps)" by simp
-  moreover have "length (dropWhile Not ps) \<le> length ps"
+  then have "length qs < length (dropWhile Not ps)"
+    by simp
+  also have "length (dropWhile Not ps) \<le> length ps"
     by (simp add: length_dropWhile_le)
-  ultimately show "length qs < length ps" by auto
+  finally show "length qs < length ps" .
 qed
 
 primrec natify :: "nat \<Rightarrow> bool list \<Rightarrow> nat list" where
@@ -61,7 +61,7 @@
 function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
   "factorise_from k n = (if 1 < k \<and> k \<le> n
     then
-      let (q, r) = Divides.divmod_nat n k 
+      let (q, r) = Euclidean_Division.divmod_nat n k 
       in if r = 0 then k # factorise_from k q
         else factorise_from (Suc k) n
     else [])" 
@@ -69,9 +69,11 @@
 
 termination factorise_from \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close>
   apply (relation "measure (\<lambda>(k, n). 2 * n - k)")
-    apply (auto simp add: prod_eq_iff algebra_simps elim!: dvdE)
-  apply (case_tac "k \<le> ka * 2")
-   apply (auto intro: diff_less_mono)
+  apply (auto simp add: Euclidean_Division.divmod_nat_def algebra_simps elim!: dvdE)
+  subgoal for m n
+    apply (cases "m \<le> n * 2")
+     apply (auto intro: diff_less_mono)
+    done
   done
 
 definition factorise :: "nat \<Rightarrow> nat list" where