Theory Generalized_Primality_Test

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

  Generic probabilistic primality test
section ‹A Generic View on Probabilistic Prime Tests›
theory Generalized_Primality_Test

definition primality_test :: "(nat  nat  bool)  nat  bool pmf" where
  "primality_test P n = 
    (if n < 3  even n then return_pmf (n = 2) else
      do {
        a  pmf_of_set {2..< n};
        return_pmf (P n a)

(* TODO Move *)
lemma expectation_of_bool_is_pmf: "measure_pmf.expectation M of_bool = pmf M True"
  by (simp add: integral_measure_pmf_real[where A=UNIV] UNIV_bool)

lemma eq_bernoulli_pmfI:
  assumes "pmf p True = x"
  shows   "p = bernoulli_pmf x"
proof (intro pmf_eqI)
  fix b :: bool
  from assms have "x  {0..1}" by (auto simp: pmf_le_1)
  thus "pmf p b = pmf (bernoulli_pmf x) b"
    using assms by (cases b) (auto simp: pmf_False_conv_True)

text ‹
  We require a probabilistic primality test to never classify a prime as composite.
  It may, however, mistakenly classify composites as primes.
locale prob_primality_test =
  fixes P :: "nat  nat  bool" and n :: nat
  assumes P_works: "odd n  2  a  a < n  prime n  P n a"

lemma FalseD:
  assumes false: "False  set_pmf (primality_test P n)"
  shows   "¬ prime n"
proof -
  from false consider "n  2" "n < 3" | "n  2" "even n" | 
      a where "¬ P n a" "odd n" "2  a" "a < n"
    by (auto simp: primality_test_def not_less split: if_splits)

  then show ?thesis proof cases
  case 1
  then show ?thesis 
    by (cases rule: linorder_neqE_nat) (use prime_ge_2_nat[of n] in auto)
    case 2
    then show ?thesis using primes_dvd_imp_eq two_is_prime_nat by blast
    case 3
    then show ?thesis using P_works by blast

theorem prime:
  assumes odd_prime: "prime n"
  shows   "primality_test P n = return_pmf True"
proof -
  have "set_pmf (primality_test P n)  {True, False}"
    by auto
  moreover from assms have "False  set_pmf (primality_test P n)"
    using FalseD by auto
  ultimately have "set_pmf (primality_test P n)  {True}"
    by auto
  thus ?thesis
    by (subst (asm) set_pmf_subset_singleton)


text ‹
  We call a primality test q›-good for a fixed positive real number q› if the probability
  that it mistakenly classifies a composite as a prime is less than q›.
locale good_prob_primality_test = prob_primality_test +
  fixes q :: real
  assumes q_pos: "q > 0"
  assumes composite_witness_bound:
            "¬prime n  2 < n  odd n 
               real (card {a . 2  a  a < n  P n a}) < q * real (n - 2)"

lemma composite_aux:
  assumes "¬prime n"
  shows   "measure_pmf.expectation (primality_test P n) of_bool < q"
  unfolding primality_test_def using assms composite_witness_bound q_pos
  by (clarsimp simp add: pmf_expectation_bind[where A = "{2..< n}"] sum_of_bool_eq_card field_simps Int_def
    simp flip: sum_divide_distrib)

theorem composite:
  assumes "¬prime n"
  shows   "pmf (primality_test P n) True < q"
  using composite_aux[OF assms] by (simp add: expectation_of_bool_is_pmf)