# HG changeset patch
# User haftmann
# Date 1694846324 0
# Node ID d52934f126d4596fc2ae15f0fde8e95194671a5b
# Parent  d900ff3f314a557ee2d1c738c1d29c6d6f075de0
new formulation of an auxiliary lemma

diff -r d900ff3f314a -r d52934f126d4 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Sep 15 20:46:50 2023 +0100
+++ b/src/HOL/Divides.thy	Sat Sep 16 06:38:44 2023 +0000
@@ -23,9 +23,6 @@
 context unique_euclidean_semiring_numeral
 begin
 
-context
-begin
-
 lemma divmod_digit_1 [no_atp]:
   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")
@@ -75,7 +72,7 @@
     by (simp_all add: div mod)
 qed
 
-lemma mod_double_modulus: \<comment>\<open>This is actually useful and should be transferred to a suitable type class\<close>
+lemma mod_double_modulus [no_atp]:
   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")
@@ -92,8 +89,6 @@
 
 end
 
-end
-
 instance nat :: unique_euclidean_semiring_numeral
   by standard
     (auto simp add: div_greater_zero_iff div_mult2_eq mod_mult2_eq)
diff -r d900ff3f314a -r d52934f126d4 src/HOL/Euclidean_Rings.thy
--- a/src/HOL/Euclidean_Rings.thy	Fri Sep 15 20:46:50 2023 +0100
+++ b/src/HOL/Euclidean_Rings.thy	Sat Sep 16 06:38:44 2023 +0000
@@ -1651,7 +1651,6 @@
 qed
 
 
-
 subsection \<open>Division on \<^typ>\<open>int\<close>\<close>
 
 text \<open>
diff -r d900ff3f314a -r d52934f126d4 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Fri Sep 15 20:46:50 2023 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy	Sat Sep 16 06:38:44 2023 +0000
@@ -692,7 +692,7 @@
     case 2
     from assms have "x mod 8 = 3 \<or> x mod 8 = 5" by auto
     then have x': "x mod 16 = 3 \<or> x mod 16 = 5 \<or> x mod 16 = 11 \<or> x mod 16 = 13"
-      using mod_double_modulus [of 8 x] by auto
+      using mod_double_nat [of x 8] by auto
     hence "[x ^ 4 = 1] (mod 16)" using assms
       by (auto simp: cong_def simp flip: power_mod[of x])
     hence "ord 16 x dvd 2\<^sup>2" by (simp add: ord_divides')
@@ -729,11 +729,11 @@
     have "2 ^ k' + 1 < 2 ^ k' + (2 ^ k' :: nat)"
       using one_less_power[of "2::nat" k'] k' by (intro add_strict_left_mono) auto
     with cong notcong have cong': "x ^ (2 ^ (k' - 2)) mod 2 ^ Suc k' = 1 + 2 ^ k'"
-      using mod_double_modulus [of "2 ^ k'" "x ^ 2 ^ (k' - 2)"] k' by (auto simp: cong_def)
+      using mod_double_nat [of \<open>x ^ 2 ^ (k' - 2)\<close> \<open>2 ^ k'\<close>] k' by (auto simp: cong_def)
 
     hence "x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' \<or>
            x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' + 2 ^ Suc k'"
-      using mod_double_modulus [of "2 ^ Suc k'" "x ^ 2 ^ (k' - 2)"] by auto
+      using mod_double_nat [of \<open>x ^ 2 ^ (k' - 2)\<close> \<open>2 ^ Suc k'\<close>] by auto
     hence eq: "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
     proof
       assume *: "x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 2 ^ k'"
diff -r d900ff3f314a -r d52934f126d4 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Fri Sep 15 20:46:50 2023 +0100
+++ b/src/HOL/Parity.thy	Sat Sep 16 06:38:44 2023 +0000
@@ -307,6 +307,12 @@
   qed
 qed
 
+lemma mod_double_nat:
+  \<open>n mod (2 * m) = n mod m \<or> n mod (2 * m) = n mod m + m\<close>
+  for m n :: nat
+  by (cases \<open>even (n div m)\<close>)
+    (simp_all add: mod_mult2_eq ac_simps even_iff_mod_2_eq_zero)
+
 context semiring_parity
 begin
 
@@ -789,6 +795,10 @@
   \<open>of_bool b div 2 = 0\<close>
   by simp
 
+lemma of_nat_mod_double:
+  \<open>of_nat n mod (2 * of_nat m) = of_nat n mod of_nat m \<or> of_nat n mod (2 * of_nat m) = of_nat n mod of_nat m + of_nat m\<close>
+  by (simp add: mod_double_nat flip: of_nat_mod of_nat_add of_nat_mult of_nat_numeral)
+
 end
 
 class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat