Theory Lucas_Lehmer_Auxiliary

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)"
  by (simp add: coprime_commute)

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"
    by (simp add: coprime_commute)
  
  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]
    by (simp add: prime_p_Jacobi_eq_Legendre)
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)
    ultimately show False by contradiction
  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"
    by (simp add: semiring_simprules Suc)
  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)"
    by (simp add: cring_simprules)
  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))"
      by (simp add: add_pow_ldistr)
    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

lemma (in ring_hom_cring) hom_add_pow_nat:
  "x ∈ carrier R ⟹ h (add_pow R (n::nat) x) = add_pow S n (h x)"
  by (induction n) auto

end