(* 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