Theory Fermat_Test

  File:     Fermat_Test.thy
  Authors:  Daniel Stüwe, Manuel Eberl

  The probabilistic prime test known as Fermat's test
section ‹Fermat's Test›
theory Fermat_Test

definition "fermat_test = primality_test (λn a. fermat_liar a n)"

text ‹
  The Fermat test is a good probabilistic primality test on non-Carmichael numbers.
locale fermat_test_not_Carmichael_number =
  fixes n :: nat
  assumes not_Carmichael_number: "¬Carmichael_number n  n < 3"

sublocale fermat_test: good_prob_primality_test "λa n. fermat_liar n a" n "1 / 2"
  rewrites "primality_test (λ a n. fermat_liar n a) = fermat_test"
proof -
  show "good_prob_primality_test (λa n. fermat_liar n a) n (1 / 2)"
    using not_Carmichael_number not_Carmichael_number_imp_card_fermat_witness_bound(3)[of n]
          prime_imp_fermat_liar[of n]
    by unfold_locales auto
qed (auto simp: fermat_test_def)


lemma not_coprime_imp_fermat_witness:
  fixes n :: nat
  assumes "n > 1" "¬coprime a n"
  shows   "fermat_witness a n"
  using assms lucas_coprime_lemma[of "n - 1" a n]
  by (auto simp: fermat_witness_def)

theorem fermat_test_prime:
  assumes "prime n"
  shows   "fermat_test n = return_pmf True"
proof -
  interpret fermat_test_not_Carmichael_number n
    using assms Carmichael_number_not_prime by unfold_locales auto
  from assms show ?thesis by (rule

theorem fermat_test_composite:
  assumes "¬prime n" "¬Carmichael_number n  n < 3"
  shows   "pmf (fermat_test n) True < 1 / 2"
proof -
  interpret fermat_test_not_Carmichael_number n by unfold_locales fact+
  from assms(1) show ?thesis by (rule fermat_test.composite)

text ‹
  For a Carmichael number $n$, Fermat's test as defined above mistakenly returns `True'
  with probability $(\varphi(n)-1) / (n - 2)$. This probability is close to 1 if n›
  has few and big prime factors; it is not quite as bad if it has many and/or small factors,
  but in that case, simple trial division can also detect compositeness.

  Moreover, Fermat's test only succeeds for a Carmichael number if it happens to guess a
  number that is not coprime to n›. In that case, the fact that we have found
  a number between 2 and n› that is not coprime to n› alone is 
  proof that n› is composite, and indeed we can even find a non-trivial factor
  by computing the GCD. This means that for Carmichael numbers, Fermat's test is essentially
  no better than the very crude method of attempting to guess numbers coprime to n›.

  This means that, in general, Fermat's test is not very helpful for Carmichael numbers.
theorem fermat_test_Carmichael_number:
  assumes "Carmichael_number n"
  shows   "fermat_test n = bernoulli_pmf (real (totient n - 1) / real (n - 2))"
proof (rule eq_bernoulli_pmfI)
  from assms have n: "n > 3" "odd n"
    using Carmichael_number_odd Carmichael_number_gt_3 by auto
  from n have "fermat_test n = pmf_of_set {2..<n}  (λa. return_pmf (fermat_liar a n))"
    by (simp add: fermat_test_def primality_test_def)
  also have " = pmf_of_set {2..<n}  (λa. return_pmf (coprime a n))"
    using n assms lucas_coprime_lemma[of "n - 1" _ n]
    by (intro bind_pmf_cong refl) (auto simp: Carmichael_number_def fermat_liar_def)
  also have "pmf  True = (a=2..<n. indicat_real {True} (coprime a n)) / real (n - 2)"
    using n by (auto simp: pmf_bind_pmf_of_set)
  also have "(a=2..<n. indicat_real {True} (coprime a n)) =
               (a | a  {2..<n}  coprime a n. 1)"
    by (intro sum.mono_neutral_cong_right) auto
  also have " = card {a{2..<n}. coprime a n}"
    by simp
  also have "{a{2..<n}. coprime a n} = totatives n - {1}"
    using n by (auto simp: totatives_def order.strict_iff_order[of _ n])
  also have "card  = totient n - 1"
    using n by (subst card_Diff_subset) (auto simp: totient_def)
  finally show "pmf (fermat_test n) True = real (totient n - 1) / real (n - 2)"
    using n by simp