Quelle  Lehmer.thy

theory Lehmer
imports
  Main
  "HOL-Number_Theory.Residues"
begin

section ‹Lehmer's Theorem›
text_raw ‹\label{sec:lehmer}›

text ‹
 In this section we prove Lehmer's Theorem~cite‹"lehmer1927fermat_converse"› and its converse.
 These two theorems characterize a necessary and complete criterion for primality. This criterion
 is the basis of the Lucas-Lehmer primality test and the primality certificates of
 Pratt~cite‹"pratt1975certificate"›.
 ›

lemma mod_1_coprime_nat:
  "coprime a b" if "0 < n" "[a ^ n = 1] (mod b)" for a b :: nat
proof -
  from that coprime_1_left have "coprime (a ^ n) b"
    using cong_imp_coprime cong_sym by blast
  with ‹0 < n› show ?thesis
    by simp
qed

text ‹
 This is a weak variant of Lehmer's theorem: All numbers less then @{term "p - 1 :: nat"}
 must be considered.
 ›

lemma lehmers_weak_theorem:
  assumes "2 ≤ p"
  assumes min_cong1: "∧x. 0 < x ==> x < p - 1 ==> [a ^ x ≠ 1] (mod p)"
  assumes cong1: "[a ^ (p - 1) = 1] (mod p)"
  shows "prime p"
proof (rule totient_imp_prime)
  from ‹2 ≤ p› cong1 have "coprime a p"
    by (intro mod_1_coprime_nat[of "p - 1"]) auto
  then have "[a ^ totient p = 1] (mod p)"
    by (intro euler_theorem) auto
  then have "totient p ≥ p - 1 ∨ totient p = 0"
    using min_cong1[of "totient p"] by fastforce
  moreover have "totient p > 0"
    using ‹2 ≤ p› by simp
  moreover from ‹p ≥ 2› have "totient p < p" by (intro totient_less) auto
  ultimately show "totient p = p - 1" by presburger
qed (insert ‹p ≥ 2›, auto)

lemma prime_factors_elem:
  fixes n :: nat assumes "1 < n" shows "∃p. p ∈ prime_factors n"
  using assms by (cases "prime n") (auto simp: prime_factors_dvd prime_factor_nat)

lemma cong_pow_1_nat:
  "[a ^ x = 1] (mod b)" if "[a = 1] (mod b)" for a b :: nat
  using cong_pow [of a 1 b x] that by simp

lemma cong_gcd_eq_1_nat:
  fixes a b :: nat
  assumes "0 < m" and cong_props: "[a ^ m = 1] (mod b)" "[a ^ n = 1] (mod b)"
  shows "[a ^ gcd m n = 1] (mod b)"
proof -
  obtain c d where gcd: "m * c = n * d + gcd m n" using bezout_nat[of m n] ‹0 < m›
    by auto
  have cong_m: "[a ^ (m * c) = 1] (mod b)" and cong_n: "[a ^ (n * d) = 1] (mod b)"
    using cong_props by (simp_all only: cong_pow_1_nat power_mult)
  have "[1 * a ^ gcd m n = a ^ (n * d) * a ^ gcd m n] (mod b)"
    by (rule cong_scalar_right, rule cong_sym) (fact cong_n)
  also have "[a ^ (n * d) * a ^ gcd m n = a ^ (m * c)] (mod b)"
    using gcd by (simp add: power_add)
  also have "[a ^ (m * c) = 1] (mod b)" using cong_m by simp
  finally show "[a ^ gcd m n = 1] (mod b)" by simp
qed

lemma One_leq_div:
  "1 < b div a" if "a dvd b" "a < b" for a b :: nat
  using that by (metis dvd_div_mult_self mult.left_neutral mult_less_cancel2)

theorem lehmers_theorem:
  assumes "2 ≤ p"
  assumes pf_notcong1: "∧x. x ∈ prime_factors (p - 1) ==> [a ^ ((p - 1) div x) ≠ 1] (mod p)"
  assumes cong1: "[a ^ (p - 1) = 1] (mod p)"
  shows "prime p"
proof cases
  assume "[a = 1] (mod p)" with ‹2 ≤p› pf_notcong1 show ?thesis
    by (metis cong_pow_1_nat less_diff_conv linorder_neqE_nat linorder_not_less
      one_add_one prime_factors_elem two_is_prime_nat)
next
  assume A_notcong_1: "[a ≠ 1] (mod p)"
  { fix x assume "0 < x" "x < p - 1"
    have "[a ^ x ≠ 1] (mod p)"
    proof
      assume "[a ^ x = 1] (mod p)"
      then have gcd_cong_1: "[a ^ gcd x (p - 1) = 1] (mod p)"
        by (rule cong_gcd_eq_1_nat[OF ‹0 < x› _ cong1])

      have "gcd x (p - 1) = p - 1"
      proof (rule ccontr)
        assume "¬?thesis"
        then have gcd_p1: "gcd x (p - 1) dvd (p - 1)" "gcd x (p - 1) < p - 1"
          using gcd_le2_nat[of "p - 1" x] ‹2 ≤ p› by (simp, linarith)

        define c where "c = (p - 1) div (gcd x (p - 1))"
        then have p_1_eq: "p - 1 = gcd x (p - 1) * c" unfolding c_def using gcd_p1
          by (metis dvd_mult_div_cancel)

        from gcd_p1 have "1 < c" unfolding c_def by (rule One_leq_div)
        then obtain q where q_pf: "q ∈ prime_factors c"
          using prime_factors_elem by auto
        then have "q dvd c" by auto

        have "q ∈ prime_factors (p - 1)" using q_pf ‹1 < c› ‹2 ≤ p›
          by (subst p_1_eq) (simp add: prime_factors_product)
        moreover
        have "[a ^ ((p - 1) div q) = 1] (mod p)"
          by (subst p_1_eq,subst dvd_div_mult_self[OF ‹q dvd c›,symmetric])
             (simp del: One_nat_def add: power_mult gcd_cong_1 cong_pow_1_nat)
        ultimately
        show False using pf_notcong1 by metis
      qed
      then show False using ‹x < p - 1›
        by (metis ‹0 < x› gcd_le1_nat gr_implies_not0 linorder_not_less)
    qed
  }
  with lehmers_weak_theorem[OF ‹2 ≤ p› _ cong1] show ?thesis by metis
qed

text ‹
 The converse of Lehmer's theorem is also true.
 ›

lemma converse_lehmer_weak:
 assumes prime_p: "prime p"
 shows "∃ a. [a^(p - 1) = 1] (mod p) ∧ (∀ x . 0 < x ⟶ x ≤ p - 2 ⟶ [a^x ≠ 1] (mod p))
             ∧ a > 0 ∧ a < p"
 proof -
   have "p ≥ 2" by (rule prime_ge_2_nat[OF prime_p])
   obtain a where a:"a ∈ {1 .. p - 1} ∧ {1 .. p - 1} = {a^i mod p | i . i ∈ UNIV}"
    using residue_prime_mult_group_has_gen[OF prime_p] by blast
  {
   { fix x::nat assume x:"0 < x ∧ x ≤ p - 2 ∧ [a^x = 1] (mod p)"
     have "{a^i mod p| i. i ∈ UNIV} = {a^i mod p | i. 0 < i ∧ i ≤ x}"
     proof
      show "{a ^ i mod p | i. 0 < i ∧ i ≤ x} ⊆ {a ^ i mod p | i. i ∈ UNIV}" by blast
      { fix y assume y:"y ∈ {a^i mod p| i . i ∈ UNIV}"
        then obtain i where i:"y = a^i mod p" by auto
        define q r where "q = i div x" and "r = i mod x"
        have "i = q*x + r" by (simp add: r_def q_def)
        hence y_q_r:"y = (((a ^ (q*x)) mod p) * ((a ^ r) mod p)) mod p"
          by (simp add: i power_add mod_mult_eq)
        have "a ^ (q*x) mod p = (a ^ x mod p) ^ q mod p"
          by (simp add: power_mod mult.commute power_mult[symmetric])
        then have y_r:"y = a ^ r mod p" using ‹p≥2› x
          by (simp add: cong_def y_q_r)
        have "y ∈ {a ^ i mod p | i. 0 < i ∧ i ≤ x}"
        proof (cases)
          assume "r = 0"
          then have "y = a^x mod p" using ‹p≥2› x
            by (simp add: cong_def y_r)
          thus ?thesis using x by blast
        next
          assume "r ≠ 0"
          thus ?thesis using x by (auto simp add: y_r r_def)
        qed
      }
      thus " {a ^ i mod p|i. i ∈ UNIV} ⊆ {a ^ i mod p | i. 0 < i ∧ i ≤ x}" by auto
    qed
    note X = this

    have "p - 1 = card {1 .. p - 1}" by auto
    also have "{1 .. p - 1} = {a^i mod p | i. 1 ≤ i ∧ i ≤ x}" using X a by auto
    also have "… = (λ i. a^i mod p) ` {1..x}" by auto
    also have "card … ≤ p - 2"
      using Finite_Set.card_image_le[of "{1..x}" "λ i. a^i mod p"] x by auto
    finally have False using ‹2 ≤ p› by arith
   }
   hence "∀ x . 0 < x ⟶ x ≤ p - 2 ⟶ [a^x ≠ 1] (mod p)" by auto
 } note a_is_gen = this
 {
    assume "a>1"
    have "¬ p dvd a "
    proof (rule ccontr)
      assume "¬ ¬ p dvd a"
      hence "p dvd a" by auto
      have "p ≤ a" using dvd_nat_bounds[OF _ ‹p dvd a›] a by simp
      thus False using ‹a>1› a by force
    qed
    hence "coprime a p"
      using prime_imp_coprime_nat [OF prime_p] by (simp add: ac_simps)
    then have "[a ^ totient p = 1] (mod p)"
      by (rule euler_theorem)
    also from prime_p have "totient p = p - 1"
      by (rule totient_prime)
    finally have "[a ^ (p - 1) = 1] (mod p)" .
  }
  hence "[a^(p - 1) = 1] (mod p)" using a by fastforce
  thus ?thesis using a_is_gen a by auto
 qed

theorem converse_lehmer:
 assumes prime_p:"prime(p)"
 shows "∃ a . [a^(p - 1) = 1] (mod p) ∧
              (∀ q. q ∈ prime_factors (p - 1) ⟶ [a^((p - 1) div q) ≠ 1] (mod p))
              ∧ a > 0 ∧ a < p"
 proof -
  have "p ≥ 2" by (rule prime_ge_2_nat[OF prime_p])
  obtain a where a:"[a^(p - 1) = 1] (mod p) ∧ (∀ x . 0 < x ⟶ x ≤ p - 2 ⟶ [a^x ≠ 1] (mod p))
                    ∧ a > 0 ∧ a < p"
    using converse_lehmer_weak[OF prime_p] by blast
  { fix q assume q:"q ∈ prime_factors (p - 1)"
    hence "0 < q ∧ q ≤ p - 1" using ‹p≥2›
      by (auto simp add: dvd_nat_bounds prime_factors_gt_0_nat)
    hence "(p - 1) div q ≥ 1" using div_le_mono[of "q" "p - 1" q] div_self[of q] by simp
    have "q ≥ 2" using q by (auto intro: prime_ge_2_nat)
    hence "(p - 1) div q < p - 1" using ‹p ≥ 2› by simp
    hence "[a^((p - 1) div q) ≠ 1] (mod p)" using a ‹(p - 1) div q ≥ 1›
      by (auto simp add: Suc_diff_Suc less_eq_Suc_le)
  }
  thus ?thesis using a by auto
 qed

end