# Theory Lucas_Lehmer_Auxiliary

theory Lucas_Lehmer_Auxiliary
imports Jacobi_Symbol
```section ‹Auxiliary material›
theory Lucas_Lehmer_Auxiliary
imports
"HOL-Algebra.Ring"
"Probabilistic_Prime_Tests.Jacobi_Symbol"
begin

(* TODO: Much of this belongs in the library *)

subsection ‹Auxiliary  number-theoretic material›

lemma congD: "[a = b] (mod n) ⟹ a mod n = b mod n"
by (auto simp: cong_def)

lemma eval_coprime:
"(b :: 'a :: euclidean_semiring_gcd) ≠ 0 ⟹ coprime a b ⟷ coprime b (a mod b)"

lemma two_power_odd_mod_12:
assumes "odd n" "n > 1"
shows   "[2 ^ n = 8] (mod (12 :: nat))"
using assms
proof (induction n rule: less_induct)
case (less n)
show ?case
proof (cases "n = 3")
case False
with less.prems have "n > 3" by (auto elim!: oddE)
hence "[2 ^ (n - 2 + 2) = (8 * 4 :: nat)] (mod 12)"
unfolding power_add using less.prems by (intro cong_mult less) auto
also have "n - 2 + 2 = n"
using ‹n > 3› by simp
finally show ?thesis by (simp add: cong_def)
qed auto
qed

lemma Legendre_3_right:
fixes p :: nat
assumes p: "prime p" "p > 3"
shows   "p mod 12 ∈ {1, 5, 7, 11}" and "Legendre p 3 = (if p mod 12 ∈ {1, 7} then 1 else -1)"
proof -
have "coprime p 2" using p prime_nat_not_dvd[of p 2]
by (intro prime_imp_coprime) (auto dest: dvd_imp_le)
moreover have "coprime p 3" using p
by (intro prime_imp_coprime) auto
ultimately have "coprime p (2 * 2 * 3)"
unfolding coprime_mult_right_iff by auto
hence "coprime 12 p"

hence "p mod 12 ∈ {p∈{..11}. coprime 12 p}" by auto
also have "{p∈{..11}. coprime 12 p} = {1::nat, 5, 7, 11}"
unfolding atMost_nat_numeral pred_numeral_simps arith_simps
by (auto simp del: coprime_imp_gcd_eq_1 simp: eval_coprime)
finally show "p mod 12 ∈ {1, 5, 7, 11}" by auto
hence "p mod 12 = 1 ∨ p mod 12 = 5 ∨ p mod 12 = 7 ∨ p mod 12 = 11"
by auto
thus "Legendre p 3 = (if p mod 12 ∈ {1, 7} then 1 else -1)"
proof safe
assume "p mod 12 = 1"
have "Legendre (int p) 3 = Legendre (int p mod 3) 3"
by (intro Legendre_mod [symmetric]) auto
also from ‹p mod 12 = 1› have "p mod 12 mod 3 = 1" by simp
hence "p mod 3 = 1" by (simp add: mod_mod_cancel)
hence "int p mod 3 = 1" by presburger
finally have "Legendre p 3 = 1" by simp
thus ?thesis using ‹p mod 12 = 1› by simp
next
assume "p mod 12 = 5"
have "Legendre (int p) 3 = Legendre (int p mod 3) 3"
by (intro Legendre_mod [symmetric]) auto
also from ‹p mod 12 = 5› have "p mod 12 mod 3 = 2" by simp
hence "p mod 3 = 2" by (simp add: mod_mod_cancel)
hence "int p mod 3 = 2" by presburger
finally have "Legendre p 3 = -1" by (simp add: supplement2_Legendre)
thus ?thesis using ‹p mod 12 = 5› by simp
next
assume "p mod 12 = 7"
have "Legendre (int p) 3 = Legendre (int p mod 3) 3"
by (intro Legendre_mod [symmetric]) auto
also from ‹p mod 12 = 7› have "p mod 12 mod 3 = 1" by simp
hence "p mod 3 = 1" by (simp add: mod_mod_cancel)
hence "int p mod 3 = 1" by presburger
finally have "Legendre p 3 = 1" by simp
thus ?thesis using ‹p mod 12 = 7› by simp
next
assume "p mod 12 = 11"
have "Legendre (int p) 3 = Legendre (int p mod 3) 3"
by (intro Legendre_mod [symmetric]) auto
also from ‹p mod 12 = 11› have "p mod 12 mod 3 = 2" by simp
hence "p mod 3 = 2" by (simp add: mod_mod_cancel)
hence "int p mod 3 = 2" by presburger
finally have "Legendre p 3 = -1" by (simp add: supplement2_Legendre)
thus ?thesis using ‹p mod 12 = 11› by simp
qed
qed

lemma Legendre_3_left:
fixes p :: nat
assumes p: "prime p" "p > 3"
shows   "Legendre 3 p = (if p mod 12 ∈ {1, 11} then 1 else -1)"
proof (cases "p mod 12 = 1 ∨ p mod 12 = 5")
case True
hence "p mod 12 mod 4 = 1" by auto
hence "even ((p - Suc 0) div 2)"
by (intro even_mod_4_div_2) (auto simp: mod_mod_cancel)
with Quadratic_Reciprocity[of p 3] Legendre_3_right(2)[of p] assms True show ?thesis
by auto
next
case False
with Legendre_3_right(1)[OF assms] have *: "p mod 12 = 7 ∨ p mod 12 = 11" by auto
hence "p mod 12 mod 4 = 3" by auto
hence "odd ((p - Suc 0) div 2)"
by (intro odd_mod_4_div_2) (auto simp: mod_mod_cancel)
with Quadratic_Reciprocity[of p 3] Legendre_3_right(2)[of p] assms * show ?thesis
by fastforce
qed

lemma supplement2_Legendre':
assumes "prime p" "p ≠ 2"
shows "Legendre 2 p = (if p mod 8 = 1 ∨ p mod 8 = 7 then 1 else -1)"
proof -
from assms have "p > 2"
using prime_gt_1_int[of p] by auto
moreover from this and assms have "odd p"
by (auto simp: prime_odd_int)
ultimately show ?thesis
using supplement2_Jacobi'[of p] assms prime_odd_int[of p]
qed

lemma little_Fermat_nat:
fixes a :: nat
assumes "prime p" "¬p dvd a"
shows   "[a ^ p = a] (mod p)"
proof -
have "p = Suc (p - 1)"
using prime_gt_0_nat[OF assms(1)] by simp
also have "p - 1 = totient p"
using assms by (simp add: totient_prime)
also have "a ^ (Suc …) = a * a ^ totient p"
by simp
also have "[… = a * 1] (mod p)"
using prime_imp_coprime[of p a] assms
by (intro cong_mult cong_refl euler_theorem) (auto simp: coprime_commute)
finally show ?thesis by simp
qed

lemma little_Fermat_int:
fixes a :: int and p :: nat
assumes "prime p" "¬p dvd a"
shows   "[a ^ p = a] (mod p)"
proof -
have "p > 1" using prime_gt_1_nat assms by simp
have "¬int p dvd a mod int p"
using assms by (simp add: dvd_mod_iff)
also from ‹p > 1› have "a mod int p = int (nat (a mod int p))"
by simp
finally have not_dvd: "¬p dvd nat (a mod int p)"
by (subst (asm) int_dvd_int_iff)

have "[a ^ p = (a mod p) ^ p] (mod p)"
by (intro cong_pow) (auto simp: cong_def)
also have "(a mod p) ^ p = (int (nat (a mod p))) ^ p"
using ‹p > 1› by (subst of_nat_nat) auto
also have "… = int (nat (a mod p) ^ p)"
by simp
also have "[… = int (nat (a mod p))] (mod p)"
by (subst cong_int_iff, rule little_Fermat_nat) (use assms not_dvd in auto)
also have "int (nat (a mod p)) = a mod p"
using ‹p > 1› by simp
also have "[a mod p = a] (mod p)"
by (auto simp: cong_def)
finally show ?thesis .
qed

lemma prime_dvd_choose:
assumes "0 < k" "k < p" "prime p"
shows "p dvd (p choose k)"
proof -
have "k ≤ p" using ‹k < p› by auto

have "p dvd fact p" using assms by (simp add: prime_dvd_fact_iff)

moreover have "¬ p dvd fact k * fact (p - k)"
unfolding prime_dvd_mult_iff[OF assms(3)] prime_dvd_fact_iff[OF assms(3)]
using assms by simp

ultimately show ?thesis
unfolding binomial_fact_lemma[OF ‹k ≤ p›, symmetric]
using assms prime_dvd_multD by blast
qed

lemma prime_natD:
assumes "prime (p :: nat)" "a dvd p"
shows   "a = 1 ∨ a = p"
using assms by (auto simp: prime_nat_iff)

lemma not_prime_imp_ex_prod_nat:
assumes "m > 1" "¬ prime (m::nat)"
shows   "∃n k. m = n * k ∧ 1 < n ∧ n < m ∧ 1 < k ∧ k < m"
proof -
from assms have "¬Factorial_Ring.irreducible m"
by (simp flip: prime_elem_iff_irreducible)
with assms obtain n k where nk: "m = n * k" "n ≠ 1" "k ≠ 1"
by (auto simp: Factorial_Ring.irreducible_def)
moreover from this assms have "n > 0" "k > 0"
by auto
with nk have "n > 1" "k > 1" by auto
moreover {
from assms nk have "n dvd m" "k dvd m" by auto
with assms have "n ≤ m" "k ≤ m"
by (auto intro!: dvd_imp_le)
moreover from nk ‹n > 1› ‹k > 1› have "n ≠ m" "k ≠ m"
by auto
ultimately have "n < m" "k < m" by auto
}
ultimately show ?thesis by blast
qed

subsection ‹Auxiliary algebraic material›

lemma (in group) ord_eqI_prime_factors:
assumes "⋀p. p ∈ prime_factors n ⟹ x [^] (n div p) ≠ 𝟭" and "x [^] n = 𝟭"
assumes "x ∈ carrier G" "n > 0"
shows   "group.ord G x = n"
proof -
have "group.ord G x dvd n"
using assms by (subst pow_eq_id [symmetric]) auto
then obtain k where k: "n = group.ord G x * k"
by auto
have "k = 1"
proof (rule ccontr)
assume "k ≠ 1"
then obtain p where p: "prime p" "p dvd k"
using prime_factor_nat by blast
have "x [^] (group.ord G x * (k div p)) = 𝟭"
by (subst pow_eq_id) (use assms in auto)
also have "group.ord G x * (k div p) = n div p"
using p by (auto simp: k)
finally have "x [^] (n div p) = 𝟭" .
moreover have "x [^] (n div p) ≠ 𝟭"
using p k assms by (intro assms) (auto simp: in_prime_factors_iff)
qed
with k show ?thesis by simp
qed

lemma (in monoid) pow_nat_eq_1_imp_unit:
fixes n :: nat
assumes "x [^] n = 𝟭" and "n > 0" and [simp]: "x ∈ carrier G"
shows   "x ∈ Units G"
proof -
from ‹n > 0› have "x [^] (1 :: nat) ⊗ x [^] (n - 1) = x [^] n"
by (subst nat_pow_mult) auto
with assms have "x ⊗ x [^] (n - 1) = 𝟭"
by simp
moreover from ‹n > 0› have "x [^] (n - 1) ⊗ x [^] (1 :: nat) = x [^] n"
by (subst nat_pow_mult) auto
with assms have "x [^] (n - 1) ⊗ x = 𝟭"
by simp
ultimately show ?thesis by (auto simp: Units_def)
qed

lemma (in cring) finsum_reindex_bij_betw:
assumes "bij_betw h S T" "g ∈ T → carrier R"
shows   "finsum R (λx. g (h x)) S = finsum R g T"
using assms by (auto simp: bij_betw_def finsum_reindex)

lemma (in cring) finsum_reindex_bij_witness:
assumes witness:
"⋀a. a ∈ S ⟹ i (j a) = a"
"⋀a. a ∈ S ⟹ j a ∈ T"
"⋀b. b ∈ T ⟹ j (i b) = b"
"⋀b. b ∈ T ⟹ i b ∈ S"
"⋀b. b ∈ S ⟹ g b ∈ carrier R"
assumes eq:
"⋀a. a ∈ S ⟹ h (j a) = g a"
shows "finsum R g S = finsum R h T"
proof -
have bij: "bij_betw j S T"
using bij_betw_byWitness[where A=S and f=j and f'=i and A'=T] witness by auto
hence T_eq: "T = j ` S" by (auto simp: bij_betw_def)
from assms have "h ∈ T → carrier R"
by (subst T_eq) auto
moreover have "finsum R g S = finsum R (λx. h (j x)) S"
using assms by (intro finsum_cong) (auto simp: eq)
ultimately show ?thesis using assms(5)
using finsum_reindex_bij_betw[OF bij, of h] by simp
qed

lemma (in cring) binomial:
fixes n :: nat
assumes [simp]: "x ∈ carrier R" "y ∈ carrier R"
shows   "(x ⊕ y) [^] n = (⨁i∈{..n}. add_pow R (n choose i) (x [^] i ⊗ y [^] (n - i)))"
proof (induction n)
case (Suc n)
have binomial_Suc: "Suc n choose i = (n choose (i - 1)) + (n choose i)" if "i ∈ {1..n}" for i
using that by (cases i) auto
have Suc_diff: "Suc n - i = Suc (n - i)" if "i ≤ n" for i
using that by linarith
have "(x ⊕ y) [^] Suc n =
(⨁i∈{..n}. add_pow R (n choose i) (x [^] i ⊗ y [^] (n - i))) ⊗ x ⊕
(⨁i∈{..n}. add_pow R (n choose i) (x [^] i ⊗ y [^] (n - i))) ⊗ y"
also have "(⨁i∈{..n}. add_pow R (n choose i) (x [^] i ⊗ y [^] (n - i))) ⊗ x =
(⨁i∈{..n}. add_pow R (n choose i) (x [^] Suc i ⊗ y [^] (n - i)))"
by (subst finsum_ldistr)
(auto simp: cring_simprules Suc add_pow_rdistr intro!: finsum_cong)
also have "… = (⨁i∈{1..Suc n}. add_pow R (n choose (i - 1)) (x [^] i ⊗ y [^] (Suc n - i)))"
by (intro finsum_reindex_bij_witness[of _ "λi. i - 1" Suc]) auto
also have "{1..Suc n} = insert (Suc n) {1..n}" by auto
also have "(⨁i∈…. add_pow R (n choose (i - 1)) (x [^] i ⊗ y [^] (Suc n - i))) =
x [^] Suc n ⊕ (⨁i∈{1..n}. add_pow R (n choose (i - 1)) (x [^] i ⊗ y [^] (Suc n - i)))"
(is "_ = _ ⊕ ?S1") by (subst finsum_insert) auto
also have "(⨁i∈{..n}. add_pow R (n choose i) (x [^] i ⊗ y [^] (n - i))) ⊗ y =
(⨁i∈{..n}. add_pow R (n choose i) (x [^] i ⊗ y [^] (Suc n - i)))"
by (subst finsum_ldistr)
(auto simp: cring_simprules Suc add_pow_rdistr Suc_diff intro!: finsum_cong)
also have "{..n} = insert 0 {1..n}" by auto
also have "(⨁i∈…. add_pow R (n choose i) (x [^] i ⊗ y [^] (Suc n - i))) =
y [^] Suc n ⊕ (⨁i∈{1..n}. add_pow R (n choose i) (x [^] i ⊗ y [^] (Suc n - i)))"
(is "_ = _ ⊕ ?S2") by (subst finsum_insert) auto
also have "(x [^] Suc n ⊕ ?S1) ⊕ (y [^] Suc n ⊕ ?S2) =
x [^] Suc n ⊕ y [^] Suc n ⊕ (?S1 ⊕ ?S2)"
also have "?S1 ⊕ ?S2 = (⨁i∈{1..n}. add_pow R (Suc n choose i) (x [^] i ⊗ y [^] (Suc n - i)))"
by (subst finsum_addf [symmetric], simp, simp, rule finsum_cong')
(auto intro!: finsum_cong simp: binomial_Suc add.nat_pow_mult)
also have "x [^] Suc n ⊕ y [^] Suc n ⊕ … =
(⨁i∈{0, Suc n} ∪ {1..n}. add_pow R (Suc n choose i) (x [^] i ⊗ y [^] (Suc n - i)))"
by (subst finsum_Un_disjoint) (auto simp: cring_simprules)
also have "{0, Suc n} ∪ {1..n} = {..Suc n}" by auto
finally show ?case .
qed auto

lemma (in cring) binomial_finite_char:
fixes p :: nat
assumes [simp]: "x ∈ carrier R" "y ∈ carrier R" and "add_pow R p 𝟭 = 𝟬" "prime p"
shows   "(x ⊕ y) [^] p = x [^] p ⊕ y [^] p"
proof -
have *: "add_pow R (p choose i) (x [^] i ⊗ y [^] (p - i)) = 𝟬" if "i ∈ {1..<p}" for i
proof -
have "p dvd (p choose i)"
by (rule prime_dvd_choose) (use that assms in auto)
then obtain k where [simp]: "(p choose i) = p * k"
by auto
have "add_pow R (p choose i) (x [^] i ⊗ y [^] (p - i)) =
add_pow R (p choose i) 𝟭 ⊗ (x [^] i ⊗ y [^] (p - i))"
also have "add_pow R (p choose i) 𝟭 = 𝟬"
using assms by (simp flip: add.nat_pow_pow)
finally show ?thesis by simp
qed

have "(x ⊕ y) [^] p = (⨁i∈{..p}. add_pow R (p choose i) (x [^] i ⊗ y [^] (p - i)))"
by (rule binomial) auto
also have "… = (⨁i∈{0, p}. add_pow R (p choose i) (x [^] i ⊗ y [^] (p - i)))"
using * by (intro add.finprod_mono_neutral_cong_right) auto
also have "… = x [^] p ⊕ y [^] p"
using assms prime_gt_0_nat[of p] by (simp add: cring_simprules)
finally show ?thesis .
qed