Theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries
section ‹Auxiliary Material›
theory Algebraic_Auxiliaries
imports
"HOL-Algebra.Algebra"
"HOL-Computational_Algebra.Squarefree"
"HOL-Number_Theory.Number_Theory"
begin
hide_const (open) Divisibility.prime
lemma sum_of_bool_eq_card:
assumes "finite S"
shows "(∑a ∈ S. of_bool (P a)) = real (card {a ∈ S . P a })"
proof -
have "(∑a ∈ S. of_bool (P a) :: real) = (∑a ∈ {x∈S. P x}. 1)"
using assms by (intro sum.mono_neutral_cong_right) auto
thus ?thesis by simp
qed
lemma mod_natE:
fixes a n b :: nat
assumes "a mod n = b"
shows "∃ l. a = n * l + b"
using assms mod_mult_div_eq[of a n] by (metis add.commute)
lemma (in group) r_coset_is_image: "H #> a = (λ x. x ⊗ a) ` H"
unfolding r_coset_def image_def
by blast
lemma (in group) FactGroup_order:
assumes "subgroup H G" "finite H"
shows "order G = order (G Mod H) * card H"
using lagrange assms unfolding FactGroup_def order_def by simp
corollary (in group) FactGroup_order_div:
assumes "subgroup H G" "finite H"
shows "order (G Mod H) = order G div card H"
using assms FactGroup_order subgroupE(2)[OF ‹subgroup H G›] by (auto simp: order_def)
lemma group_hom_imp_group_hom_image:
assumes "group_hom G G h"
shows "group_hom G (G⦇carrier := h ` carrier G⦈) h"
using group_hom.axioms[OF assms] group_hom.img_is_subgroup[OF assms] group.subgroup_imp_group
by(auto intro!: group_hom.intro simp: group_hom_axioms_def hom_def)
theorem homomorphism_thm:
assumes "group_hom G G h"
shows "G Mod kernel G (G⦇carrier := h ` carrier G⦈) h ≅ G ⦇carrier := h ` carrier G⦈"
by (intro group_hom.FactGroup_iso group_hom_imp_group_hom_image assms) simp
lemma is_iso_imp_same_card:
assumes "H ≅ G "
shows "order H = order G"
proof -
from assms obtain h where "bij_betw h (carrier H) (carrier G)"
unfolding is_iso_def iso_def
by blast
then show ?thesis
unfolding order_def
by (rule bij_betw_same_card)
qed
corollary homomorphism_thm_order:
assumes "group_hom G G h"
shows "order (G⦇carrier := h ` carrier G⦈) * card (kernel G (G⦇carrier := h ` carrier G⦈) h) = order G "
proof -
have "order (G⦇carrier := h ` carrier G⦈) = order (G Mod (kernel G (G⦇carrier := h ` carrier G⦈) h))"
using is_iso_imp_same_card[OF homomorphism_thm] ‹group_hom G G h›
by fastforce
moreover have "group G" using ‹group_hom G G h› group_hom.axioms by blast
ultimately show ?thesis
using ‹group_hom G G h› and group_hom_imp_group_hom_image[OF ‹group_hom G G h›]
unfolding FactGroup_def
by (simp add: group.lagrange group_hom.subgroup_kernel order_def)
qed
lemma (in group_hom) kernel_subset: "kernel G H h ⊆ carrier G"
using subgroup_kernel G.subgroupE(1) by blast
lemma (in group) proper_subgroup_imp_bound_on_card:
assumes "H ⊂ carrier G" "subgroup H G" "finite (carrier G)"
shows "card H ≤ order G div 2"
proof -
from ‹finite (carrier G)› have "finite (rcosets H)"
by (simp add: RCOSETS_def)
note subgroup.subgroup_in_rcosets[OF ‹subgroup H G› is_group]
then obtain J where "J ≠ H" "J ∈ rcosets H"
using rcosets_part_G[OF ‹subgroup H G›] and ‹H ⊂ carrier G›
by (metis Sup_le_iff inf.absorb_iff2 inf.idem inf.strict_order_iff)
then have "2 ≤ card (rcosets H)"
using ‹H ∈ rcosets H› card_mono[OF ‹finite (rcosets H)›, of "{H, J}"]
by simp
then show ?thesis
using mult_le_mono[of 2 "card (rcosets H)" "card H" "card H"]
unfolding lagrange[OF ‹subgroup H G›]
by force
qed
lemma cong_exp_trans[trans]:
"[a ^ b = c] (mod n) ⟹ [a = d] (mod n) ⟹ [d ^ b = c] (mod n)"
"[c = a ^ b] (mod n) ⟹ [a = d] (mod n) ⟹ [c = d ^ b] (mod n)"
using cong_pow cong_sym cong_trans by blast+
lemma cong_exp_mod[simp]:
"[(a mod n) ^ b = c] (mod n) ⟷ [a ^ b = c] (mod n)"
"[c = (a mod n) ^ b] (mod n) ⟷ [c = a ^ b] (mod n)"
by (auto simp add: cong_def mod_simps)
lemma cong_mult_mod[simp]:
"[(a mod n) * b = c] (mod n) ⟷ [a * b = c] (mod n)"
"[a * (b mod n) = c] (mod n) ⟷ [a * b = c] (mod n)"
by (auto simp add: cong_def mod_simps)
lemma cong_add_mod[simp]:
"[(a mod n) + b = c] (mod n) ⟷ [a + b = c] (mod n)"
"[a + (b mod n) = c] (mod n) ⟷ [a + b = c] (mod n)"
"[∑i∈A. f i mod n = c] (mod n) ⟷ [∑i∈A. f i = c] (mod n)"
by (auto simp add: cong_def mod_simps)
lemma cong_add_trans[trans]:
"[a = b + x] (mod n) ⟹ [x = y] (mod n) ⟹ [a = b + y] (mod n)"
"[a = x + b] (mod n) ⟹ [x = y] (mod n) ⟹ [a = y + b] (mod n)"
"[b + x = a] (mod n) ⟹ [x = y] (mod n) ⟹ [b + y = a] (mod n)"
"[x + b = a] (mod n) ⟹ [x = y] (mod n) ⟹ [y + b = a] (mod n)"
unfolding cong_def
using mod_simps(1, 2)
by metis+
lemma cong_mult_trans[trans]:
"[a = b * x] (mod n) ⟹ [x = y] (mod n) ⟹ [a = b * y] (mod n)"
"[a = x * b] (mod n) ⟹ [x = y] (mod n) ⟹ [a = y * b] (mod n)"
"[b * x = a] (mod n) ⟹ [x = y] (mod n) ⟹ [b * y = a] (mod n)"
"[x * b = a] (mod n) ⟹ [x = y] (mod n) ⟹ [y * b = a] (mod n)"
unfolding cong_def
using mod_simps(4, 5)
by metis+
lemma cong_diff_trans[trans]:
"[a = b - x] (mod n) ⟹ [x = y] (mod n) ⟹ [a = b - y] (mod n)"
"[a = x - b] (mod n) ⟹ [x = y] (mod n) ⟹ [a = y - b] (mod n)"
"[b - x = a] (mod n) ⟹ [x = y] (mod n) ⟹ [b - y = a] (mod n)"
"[x - b = a] (mod n) ⟹ [x = y] (mod n) ⟹ [y - b = a] (mod n)"
for a :: "'a :: {unique_euclidean_semiring, euclidean_ring_cancel}"
unfolding cong_def
by (metis mod_diff_eq)+
lemma eq_imp_eq_mod_int: "a = b ⟹ [a = b] (mod m)" for a b :: int by simp
lemma eq_imp_eq_mod_nat: "a = b ⟹ [a = b] (mod m)" for a b :: nat by simp
lemma cong_pow_I: "a = b ⟹ [x^a = x^b](mod n)" by simp
lemma gre1I: "(n = 0 ⟹ False) ⟹ (1 :: nat) ≤ n"
by presburger
lemma gre1I_nat: "(n = 0 ⟹ False) ⟹ (Suc 0 :: nat) ≤ n"
by presburger
lemma totient_less_not_prime:
assumes "¬ prime n" "1 < n"
shows "totient n < n - 1"
using totient_imp_prime totient_less assms
by (metis One_nat_def Suc_pred le_less_trans less_SucE zero_le_one)
lemma power2_diff_nat: "x ≥ y ⟹ (x - y)⇧2 = x⇧2 + y⇧2 - 2 * x * y" for x y :: nat
by (simp add: algebra_simps power2_eq_square mult_2_right)
(meson Nat.diff_diff_right le_add2 le_trans mult_le_mono order_refl)
lemma square_inequality: "1 < n ⟹ (n + n) ≤ (n * n)" for n :: nat
by (metis Suc_eq_plus1_left Suc_leI mult_le_mono1 semiring_normalization_rules(4))
lemma square_one_cong_one:
assumes "[x = 1](mod n)"
shows "[x^2 = 1](mod n)"
using assms cong_pow by fastforce
lemma cong_square_alt_int:
"prime p ⟹ [a * a = 1] (mod p) ⟹ [a = 1] (mod p) ∨ [a = p - 1] (mod p)"
for a p :: "'a :: {normalization_semidom, linordered_idom, unique_euclidean_ring}"
using dvd_add_triv_right_iff[of p "a - (p - 1)"]
by (auto simp add: cong_iff_dvd_diff square_diff_one_factored dest!: prime_dvd_multD)
lemma cong_square_alt:
"prime p ⟹ [a * a = 1] (mod p) ⟹ [a = 1] (mod p) ∨ [a = p - 1] (mod p)"
for a p :: nat
using cong_square_alt_int[of "int p" "int a"] prime_nat_int_transfer[of p] prime_gt_1_nat[of p]
by (simp flip: cong_int_iff add: of_nat_diff)
lemma square_minus_one_cong_one:
fixes n x :: nat
assumes "1 < n" "[x = n - 1](mod n)"
shows "[x^2 = 1](mod n)"
proof -
have "[x^2 = (n - 1) * (n - 1)] (mod n)"
using cong_mult[OF assms(2) assms(2)]
by (simp add: algebra_simps power2_eq_square)
also have "[(n - 1) * (n - 1) = Suc (n * n) - (n + n)] (mod n)"
using power2_diff_nat[of 1 n] ‹1 < n›
by (simp add: algebra_simps power2_eq_square)
also have "[Suc (n * n) - (n + n) = Suc (n * n)] (mod n)"
proof -
have "n * n + 0 * n = n * n" by linarith
moreover have "n * n - (n + n) + (n + n) = n * n"
using square_inequality[OF ‹1 < n›] le_add_diff_inverse2 by blast
moreover have "(Suc 0 + 1) * n = n + n"
by simp
ultimately show ?thesis
using square_inequality[OF ‹1 < n›]
by (metis (no_types) Suc_diff_le add_Suc cong_iff_lin_nat)
qed
also have "[Suc (n * n) = 1] (mod n)"
using cong_to_1'_nat by auto
finally show ?thesis .
qed
lemma odd_prime_gt_2_int:
"2 < p" if "odd p" "prime p" for p :: int
using prime_ge_2_int[OF ‹prime p›] ‹odd p›
by (cases "p = 2") auto
lemma odd_prime_gt_2_nat:
"2 < p" if "odd p" "prime p" for p :: nat
using prime_ge_2_nat[OF ‹prime p›] ‹odd p›
by (cases "p = 2") auto
lemma gt_one_imp_gt_one_power_if_coprime:
"1 ≤ x ⟹ 1 < n ⟹ coprime x n ⟹ 1 ≤ x ^ (n - 1) mod n"
by (rule gre1I) (auto simp: coprime_commute dest: coprime_absorb_left)
lemma residue_one_dvd: "a mod n = 1 ⟹ n dvd a - 1" for a n :: nat
by (fastforce intro!: cong_to_1_nat simp: cong_def)
lemma coprimeI_power_mod:
fixes x r n :: nat
assumes "x ^ r mod n = 1" "r ≠ 0" "n ≠ 0"
shows "coprime x n"
proof -
have "coprime (x ^ r mod n) n"
using coprime_1_right ‹x ^ r mod n = 1›
by (simp add: coprime_commute)
thus ?thesis using ‹r ≠ 0› ‹n ≠ 0› by simp
qed
lemma prime_dvd_choose:
assumes "0 < k" "k < p" "prime p"
shows "p dvd (p choose k)"
proof -
have "k ≤ p" using ‹k < p› by auto
have "p dvd fact p" using ‹prime p› by (simp add: prime_dvd_fact_iff)
moreover have "¬ p dvd fact k * fact (p - k)"
unfolding prime_dvd_mult_iff[OF ‹prime p›] prime_dvd_fact_iff[OF ‹prime p›]
using assms by simp
ultimately show ?thesis
unfolding binomial_fact_lemma[OF ‹k ≤ p›, symmetric]
using assms prime_dvd_multD by blast
qed
lemma cong_eq_0_I: "(∀i∈A. [f i mod n = 0] (mod n)) ⟹ [∑i∈A. f i = 0] (mod n)"
using cong_sum by fastforce
lemma power_mult_cong:
assumes "[x^n = a](mod m)" "[y^n = b](mod m)"
shows "[(x*y)^n = a*b](mod m)"
using assms cong_mult[of "x^n" a m "y^n" b] power_mult_distrib
by metis
lemma
fixes n :: nat
assumes "n > 1"
shows odd_pow_cong: "odd m ⟹ [(n - 1) ^ m = n - 1] (mod n)"
and even_pow_cong: "even m ⟹ [(n - 1) ^ m = 1] (mod n)"
proof (induction m)
case (Suc m)
case 1
with Suc have IH: "[(n - 1) ^ m = 1] (mod n)" by auto
show ?case using ‹1 < n› cong_mult[OF cong_refl IH] by simp
next
case (Suc m)
case 2
with Suc have IH: "[(n - 1) ^ m = n - 1] (mod n)" by auto
show ?case
using cong_mult[OF cong_refl IH, of "(n - 1)"] and square_minus_one_cong_one[OF ‹1 < n›, of "n - 1"]
by (auto simp: power2_eq_square intro: cong_trans)
qed simp_all
lemma cong_mult_uneq':
fixes a :: "'a::{unique_euclidean_ring, ring_gcd}"
assumes "coprime d a"
shows "[b ≠ c] (mod a) ⟹ [d = e] (mod a) ⟹ [b * d ≠ c * e] (mod a)"
using cong_mult_rcancel[OF assms]
using cong_trans[of "b*d" "c*e" a "c*d"]
using cong_scalar_left cong_sym by blast
lemma p_coprime_right_nat: "prime p ⟹ coprime a p = (¬ p dvd a)" for p a :: nat
by (meson coprime_absorb_left coprime_commute not_prime_unit prime_imp_coprime_nat)
lemma squarefree_mult_imp_coprime:
assumes "squarefree (a * b :: 'a :: semiring_gcd)"
shows "coprime a b"
proof (rule coprimeI)
fix l assume "l dvd a" "l dvd b"
then obtain a' b' where "a = l * a'" "b = l * b'"
by (auto elim!: dvdE)
with assms have "squarefree (l⇧2 * (a' * b'))"
by (simp add: power2_eq_square mult_ac)
thus "l dvd 1" by (rule squarefreeD) auto
qed
lemma prime_divisor_exists_strong:
fixes m :: int
assumes "m > 1" "¬prime m"
shows "∃n k. m = n * k ∧ 1 < n ∧ n < m ∧ 1 < k ∧ k < m"
proof -
from assms obtain n k where nk: "n * k > 1" "n ≥ 0" "m = n * k" "n ≠ 1" "n ≠ 0" "k ≠ 1"
using assms unfolding prime_int_iff dvd_def by auto
from nk have "n > 1" by linarith
from nk assms have "n * k > 0" by simp
with ‹n ≥ 0› have "k > 0"
using zero_less_mult_pos by force
with ‹k ≠ 1› have "k > 1" by linarith
from nk have "n > 1" by linarith
from ‹k > 1› nk have "n < m" "k < m" by simp_all
with nk ‹k > 1› ‹n > 1› show ?thesis by blast
qed
lemma prime_divisor_exists_strong_nat:
fixes m :: nat
assumes "1 < m" "¬prime m"
shows "∃p k. m = p * k ∧ 1 < p ∧ p < m ∧ 1 < k ∧ k < m ∧ prime p"
proof -
obtain p where p_def: "prime p" "p dvd m" "p ≠ m" "1 < p"
using assms prime_prime_factor and prime_gt_1_nat
by blast
moreover define k where "k = m div p"
with ‹p dvd m› have "m = p * k" by simp
moreover have "p < m"
using ‹p ≠ m› dvd_imp_le[OF ‹p dvd m›] and ‹m > 1›
by simp
moreover have "1 < k" "k < m"
using ‹1 < m› ‹1 < p› and ‹p ≠ m›
unfolding ‹m = p * k›
by (force intro: Suc_lessI Nat.gr0I)+
ultimately show ?thesis using ‹1 < m› by blast
qed
lemma prime_factorization_eqI:
assumes "⋀p. p ∈# P ⟹ prime p" "prod_mset P = n"
shows "prime_factorization n = P"
using prime_factorization_prod_mset_primes[of P] assms by simp
lemma prime_factorization_prime_elem:
assumes "prime_elem p"
shows "prime_factorization p = {#normalize p#}"
proof -
have "prime_factorization p = prime_factorization (normalize p)"
by (metis normalize_idem prime_factorization_cong)
also have "… = {#normalize p#}"
by (rule prime_factorization_prime) (use assms in auto)
finally show ?thesis .
qed
lemma size_prime_factorization_eq_Suc_0_iff [simp]:
fixes n :: "'a :: factorial_semiring_multiplicative"
shows "size (prime_factorization n) = Suc 0 ⟷ prime_elem n"
proof
assume size: "size (prime_factorization n) = Suc 0"
hence [simp]: "n ≠ 0" by auto
from size obtain p where *: "prime_factorization n = {#p#}"
by (auto elim!: size_mset_SucE)
hence p: "p ∈ prime_factors n" by auto
have "prime_elem (normalize p)"
using p by (auto simp: in_prime_factors_iff)
also have "p = prod_mset (prime_factorization n)"
using * by simp
also have "normalize … = normalize n"
by (rule prod_mset_prime_factorization_weak) auto
finally show "prime_elem n" by simp
qed (auto simp: prime_factorization_prime_elem)
lemma squarefree_prime_elem [simp, intro]:
fixes p :: "'a :: algebraic_semidom"
assumes "prime_elem p"
shows "squarefree p"
proof (rule squarefreeI)
fix x assume "x⇧2 dvd p"
show "is_unit x"
proof (rule ccontr)
assume "¬is_unit x"
hence "¬is_unit (x⇧2)"
by (simp add: is_unit_power_iff)
from assms and this and ‹x⇧2 dvd p› have "prime_elem (x⇧2)"
by (rule prime_elem_mono)
thus False by (simp add: prime_elem_power_iff)
qed
qed
lemma squarefree_prime [simp, intro]: "prime p ⟹ squarefree p"
by auto
lemma not_squarefree_primepow:
assumes "primepow n"
shows "squarefree n ⟷ prime n"
using assms by (auto simp: primepow_def squarefree_power_iff prime_power_iff)
lemma prime_factorization_normalize [simp]:
"prime_factorization (normalize n) = prime_factorization n"
by (rule prime_factorization_cong) auto
lemma one_prime_factor_iff_primepow:
fixes n :: "'a :: factorial_semiring_multiplicative"
shows "card (prime_factors n) = Suc 0 ⟷ primepow (normalize n)"
proof
assume "primepow (normalize n)"
then obtain p k where pk: "prime p" "normalize n = p ^ k" "k > 0"
by (auto simp: primepow_def)
hence "card (prime_factors (normalize n)) = Suc 0"
by (subst pk) (simp add: prime_factors_power prime_factorization_prime)
thus "card (prime_factors n) = Suc 0"
by simp
next
assume *: "card (prime_factors n) = Suc 0"
from * have "(∏p∈prime_factors n. p ^ multiplicity p n) = normalize n"
by (intro prod_prime_factors) auto
also from * have "card (prime_factors n) = 1" by simp
then obtain p where p: "prime_factors n = {p}"
by (elim card_1_singletonE)
finally have "normalize n = p ^ multiplicity p n"
by simp
moreover from p have "prime p" "multiplicity p n > 0"
by (auto simp: prime_factors_multiplicity)
ultimately show "primepow (normalize n)"
unfolding primepow_def by blast
qed
lemma squarefree_imp_prod_prime_factors_eq:
fixes x :: "'a :: factorial_semiring_multiplicative"
assumes "squarefree x"
shows "∏(prime_factors x) = normalize x"
proof -
from assms have [simp]: "x ≠ 0" by auto
have "(∏p∈prime_factors x. p ^ multiplicity p x) = normalize x"
by (intro prod_prime_factors) auto
also have "(∏p∈prime_factors x. p ^ multiplicity p x) = (∏p∈prime_factors x. p)"
using assms by (intro prod.cong refl) (auto simp: squarefree_factorial_semiring')
finally show ?thesis by simp
qed
end