--- 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)
--- 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>
--- 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'"
--- 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