# 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
imports
"HOL-Probability.Probability"
Algebraic_Auxiliaries
begin

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)
qed

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"
begin

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)
next
case 2
then show ?thesis using primes_dvd_imp_eq two_is_prime_nat by blast
next
case 3
then show ?thesis using P_works by blast
qed
qed

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)
qed

end

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)"
begin

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)

end

end```