dropped references to theorems from transitional theory Divides.thy

--- a/src/Doc/Tutorial/Rules/Forward.thy	Wed Jun 19 12:13:16 2024 +0200
+++ b/src/Doc/Tutorial/Rules/Forward.thy	Thu Jun 20 14:28:46 2024 +0000
@@ -187,10 +187,6 @@
 \rulename{div_mult_mod_eq}
 \<close>
 
-(*MOVED to Force.thy, which now depends only on Divides.thy
-lemma div_mult_self_is_m: "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
-*)
-
 lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)"
 by (auto intro: relprime_dvd_mult elim: dvdE)
 

--- a/src/HOL/Library/Word.thy	Wed Jun 19 12:13:16 2024 +0200
+++ b/src/HOL/Library/Word.thy	Thu Jun 20 14:28:46 2024 +0000
@@ -1224,7 +1224,7 @@
 
 end
 
-context unique_euclidean_semiring_numeral
+context linordered_euclidean_semiring
 begin
 
 lemma unsigned_greater_eq [simp]:
@@ -2915,7 +2915,7 @@
   by (metis mod_pos_pos_trivial uint_lt2p uint_mult_ge0 uint_word_ariths(3))
 
 lemma uint_sub_lem: "uint x \<ge> uint y \<longleftrightarrow> uint (x - y) = uint x - uint y"
-  by (metis diff_ge_0_iff_ge of_nat_0_le_iff uint_nat uint_sub_lt2p uint_word_of_int unique_euclidean_semiring_numeral_class.mod_less word_sub_wi)
+  by (simp add: uint_word_arith_bintrs take_bit_int_eq_self_iff)
 
 lemma uint_add_le: "uint (x + y) \<le> uint x + uint y"
   unfolding uint_word_ariths by (simp add: zmod_le_nonneg_dividend) 
@@ -3728,6 +3728,15 @@
 lemma word_rev_gal': "u = word_reverse w \<Longrightarrow> w = word_reverse u"
   by simp
 
+lemma word_eq_reverseI:
+  \<open>v = w\<close> if \<open>word_reverse v = word_reverse w\<close>
+proof -
+  from that have \<open>word_reverse (word_reverse v) = word_reverse (word_reverse w)\<close>
+    by simp
+  then show ?thesis
+    by simp
+qed
+
 lemma uint_2p: "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
   by (cases \<open>n < LENGTH('a)\<close>; transfer; force)
 
@@ -4162,35 +4171,38 @@
   \<open>w = word_rotr n v \<longleftrightarrow> v = word_rotl n w\<close>
   by auto
 
-lemma word_rotr_rev:
-  \<open>word_rotr n w = word_reverse (word_rotl n (word_reverse w))\<close>
+lemma word_reverse_word_rotl:
+  \<open>word_reverse (word_rotl n w) = word_rotr n (word_reverse w)\<close> (is \<open>?lhs = ?rhs\<close>)
 proof (rule bit_word_eqI)
   fix m
   assume \<open>m < LENGTH('a)\<close>
-  moreover have \<open>1 +
-    ((int m + int n mod int LENGTH('a)) mod int LENGTH('a) +
-     ((int LENGTH('a) * 2) mod int LENGTH('a) - (1 + (int m + int n mod int LENGTH('a)))) mod int LENGTH('a)) =
-    int LENGTH('a)\<close>
-    apply (cases \<open>(1 + (int m + int n mod int LENGTH('a))) mod
-         int LENGTH('a) = 0\<close>)
-    using zmod_zminus1_eq_if [of \<open>1 + (int m + int n mod int LENGTH('a))\<close> \<open>int LENGTH('a)\<close>]
-    apply simp_all
-     apply (auto simp add: algebra_simps)
-    apply (metis (mono_tags, opaque_lifting) Abs_fnat_hom_add mod_Suc mod_mult_self2_is_0 of_nat_Suc of_nat_mod semiring_char_0_class.of_nat_neq_0)
-    apply (metis (no_types, opaque_lifting) Abs_fnat_hom_add less_not_refl mod_Suc of_nat_Suc of_nat_gt_0 of_nat_mod)
+  then have \<open>int (LENGTH('a) - Suc ((m + n) mod LENGTH('a))) =
+    int ((LENGTH('a) + LENGTH('a) - Suc (m + n mod LENGTH('a))) mod LENGTH('a))\<close>
+    apply (simp only: of_nat_diff of_nat_mod)
+    apply (simp add: Suc_le_eq add_less_le_mono of_nat_mod algebra_simps)
+    apply (simp only: mod_diff_left_eq [symmetric, of \<open>int LENGTH('a) * 2\<close>] mod_mult_self1_is_0 diff_0 minus_mod_int_eq)
+    apply (simp add: mod_simps)
     done
-  then have \<open>int ((m + n) mod LENGTH('a)) =
-    int (LENGTH('a) - Suc ((LENGTH('a) - Suc m + LENGTH('a) - n mod LENGTH('a)) mod LENGTH('a)))\<close>
-    using \<open>m < LENGTH('a)\<close>
-    by (simp only: of_nat_mod mod_simps)
-      (simp add: of_nat_diff of_nat_mod Suc_le_eq add_less_mono algebra_simps mod_simps)
-  then have \<open>(m + n) mod LENGTH('a) =
-    LENGTH('a) - Suc ((LENGTH('a) - Suc m + LENGTH('a) - n mod LENGTH('a)) mod LENGTH('a))\<close>
+  then have \<open>LENGTH('a) - Suc ((m + n) mod LENGTH('a)) =
+    (LENGTH('a) + LENGTH('a) - Suc (m + n mod LENGTH('a))) mod
+    LENGTH('a)\<close>
     by simp
-  ultimately show \<open>bit (word_rotr n w) m \<longleftrightarrow> bit (word_reverse (word_rotl n (word_reverse w))) m\<close>
-    by (simp add: word_rotl_eq_word_rotr bit_word_rotr_iff bit_word_reverse_iff)
+  with \<open>m < LENGTH('a)\<close> show \<open>bit ?lhs m \<longleftrightarrow> bit ?rhs m\<close>
+    by (simp add: bit_simps)
 qed
 
+lemma word_reverse_word_rotr:
+  \<open>word_reverse (word_rotr n w) = word_rotl n (word_reverse w)\<close>
+  by (rule word_eq_reverseI) (simp add: word_reverse_word_rotl)
+
+lemma word_rotl_rev:
+  \<open>word_rotl n w = word_reverse (word_rotr n (word_reverse w))\<close>
+  by (simp add: word_reverse_word_rotr)
+
+lemma word_rotr_rev:
+  \<open>word_rotr n w = word_reverse (word_rotl n (word_reverse w))\<close>
+  by (simp add: word_reverse_word_rotl)
+
 lemma word_roti_0 [simp]: "word_roti 0 w = w"
   by transfer simp
 

--- a/src/HOL/Number_Theory/Gauss.thy	Wed Jun 19 12:13:16 2024 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Thu Jun 20 14:28:46 2024 +0000
@@ -196,10 +196,7 @@
   by (auto simp add: C_def B_mod_greater_zero)
 
 lemma F_subset: "F \<subseteq> {x. 0 < x \<and> x \<le> ((int p - 1) div 2)}"
-  apply (auto simp add: F_def E_def C_def)
-   apply (metis p_ge_2 Divides.pos_mod_bound nat_int zless_nat_conj)
-  apply (auto intro: p_odd_int)
-  done
+  using p_ge_2 by (auto simp add: F_def E_def C_def intro: p_odd_int)
 
 lemma D_subset: "D \<subseteq> {x. 0 < x \<and> x \<le> ((p - 1) div 2)}"
   by (auto simp add: D_def C_greater_zero)

--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Wed Jun 19 12:13:16 2024 +0200
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Thu Jun 20 14:28:46 2024 +0000
@@ -189,10 +189,8 @@
     using assms by (simp add: mod_mod_cancel yk(1))
   moreover have "(y mod (int p * int q)) mod int q = snd res"
     using assms by (simp add: mod_mod_cancel yk(2))
-  ultimately obtain x where "P_1 res x"
-    unfolding P_1_def
-    using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0
-    by (metis atLeastAtMost_iff zle_diff1_eq)
+  ultimately have "P_1 res (int y mod (int p * int q))"
+    using pq_ge_0 by (simp add: P_1_def)
   moreover have "a = b" if "P_1 res a" "P_1 res b" for a b
   proof -
     from that have "int p * int q dvd a - b"