Theory SG_Preliminaries
theory SG_Preliminaries
imports "HOL-Number_Theory.Number_Theory" Wlog.Wlog
begin
section ‹Preliminaries›
subsection ‹Coprimality›
text ‹We start with this useful elimination rule: when ‹a› and ‹b› are
not \<^const>‹coprime› and are not both equal to \<^term>‹0 :: 'a :: factorial_semiring_gcd›,
there exists some common \<^const>‹prime› factor.›
lemma (in factorial_semiring_gcd) not_coprime_nonzeroE :
‹⟦¬ coprime a b; a ≠ 0 ∨ b ≠ 0; ⋀p. prime p ⟹ p dvd a ⟹ p dvd b ⟹ thesis⟧ ⟹ thesis›
by (metis gcd_eq_0_iff gcd_greatest_iff is_unit_gcd prime_divisor_exists)
text ‹Still referring to the notion of \<^const>‹coprime› (but generalized to a set),
we prove that when \<^term>‹Gcd A ≠ 0›, the elements of \<^term>‹{a div Gcd A |a. a ∈ A}›
are setwise \<^const>‹coprime›.›
lemma (in semiring_Gcd) GCD_div_Gcd_is_one :
‹(GCD a ∈ A. a div Gcd A) = 1› if ‹Gcd A ≠ 0›
proof (rule ccontr)
assume ‹(GCD a∈A. a div Gcd A) ≠ 1›
then obtain d where ‹¬ is_unit d› ‹∀a∈A. d dvd (a div Gcd A)›
by (metis (no_types, lifting) Gcd_dvd associated_eqI
image_eqI normalize_1 normalize_Gcd one_dvd)
from ‹∀a∈A. d dvd (a div Gcd A)› have ‹∀a∈A. d * Gcd A dvd a›
by (meson Gcd_dvd dvd_div_iff_mult ‹Gcd A ≠ 0›)
with Gcd_greatest have ‹d * Gcd A dvd Gcd A› by blast
with ‹¬ is_unit d› show False by (metis div_self dvd_mult_imp_div that)
qed
subsection ‹Power›
text ‹Now we want to characterize the fact of admitting an ‹n›-th root
with a condition on the \<^const>‹multiplicity› of each prime factor.›
lemma exists_nth_root_iff :
‹(∃x. normalize y = x ^ n) ⟷ (∀p∈prime_factors y. n dvd multiplicity p y)›
if ‹y ≠ 0› for y :: ‹'a :: factorial_semiring_multiplicative›
proof (rule iffI)
show ‹∃x. normalize y = x ^ n ⟹ ∀p∈prime_factors y. n dvd multiplicity p y›
proof (elim exE, rule ballI)
fix x p assume ‹normalize y = x ^ n› and ‹p ∈ prime_factors y›
hence ‹p ∈ prime_factors x›
by (metis prime_factorization_normalize empty_iff power_0 prime_factorization_1
prime_factors_power set_mset_empty zero_less_iff_neq_zero)
with ‹normalize y = x ^ n› show ‹n dvd multiplicity p y›
by (metis dvd_def in_prime_factors_iff multiplicity_normalize_right
normalization_semidom_class.prime_def prime_elem_multiplicity_power_distrib)
qed
next
assume * : ‹∀p∈prime_factors y. n dvd multiplicity p y›
define f where ‹f p ≡ multiplicity p y div n› for p
have ‹normalize y = (∏p∈prime_factors y. p ^ multiplicity p y)›
by (fact prod_prime_factors[OF ‹y ≠ 0›, symmetric])
also have ‹… = (∏p∈prime_factors y. p ^ (f p * n))›
by (rule prod.cong[OF refl]) (simp add: "*" f_def)
also have ‹… = (∏p∈prime_factors y. p ^ f p) ^ n›
by (simp add: power_mult prod_power_distrib)
finally show ‹∃x. normalize y = x ^ n› ..
qed
text ‹We use this result to obtain the following elimination rule.›
corollary prod_is_some_powerE :
fixes a b :: ‹'a :: factorial_semiring_multiplicative›
assumes ‹coprime a b› and ‹a * b = x ^ n›
obtains α where ‹normalize a = α ^ n›
proof (cases ‹a = 0›)
from ‹a * b = x ^ n› show ‹(⋀α. normalize a = α ^ n ⟹ thesis) ⟹ a = 0 ⟹ thesis› by simp
next
assume ‹a ≠ 0› and hyp : ‹normalize a = α ^ n ⟹ thesis› for α
from ‹a ≠ 0› have ‹∃α. normalize a = α ^ n›
proof (rule exists_nth_root_iff[THEN iffD2, rule_format])
fix p assume ‹p ∈ prime_factors a›
with ‹a * b = x ^ n› have ‹p dvd x›
by (metis dvd_mult2 in_prime_factors_iff prime_dvd_power)
hence ‹p ^ n dvd x ^ n› by (simp add: dvd_power_same)
with ‹p ∈ prime_factors a› ‹a * b = x ^ n› have ‹n dvd multiplicity p (x ^ n)›
by (metis dvd_triv_left gcd_nat.extremum in_prime_factors_iff multiplicity_unit_left
multiplicity_zero not_dvd_imp_multiplicity_0 power_0_left
prime_elem_multiplicity_power_distrib prime_imp_prime_elem)
also from ‹p ∈ prime_factors a› ‹coprime a b› ‹a * b = x ^ n›
have ‹multiplicity p (x ^ n) = multiplicity p a›
by (metis (no_types, opaque_lifting) add.right_neutral coprime_0_right_iff coprime_def
in_prime_factors_iff normalization_semidom_class.prime_def prime_factorization_empty_iff
prime_elem_multiplicity_eq_zero_iff prime_elem_multiplicity_mult_distrib)
finally show ‹n dvd multiplicity p a› .
qed
with hyp show thesis by blast
qed
subsection ‹Sophie Germain Prime›
text ‹Finally, we introduce Sophie Germain primes.›
definition SophGer_prime :: ‹nat ⇒ bool› (‹SG›)
where ‹SG p ≡ odd p ∧ prime p ∧ prime (2 * p + 1)›
lemma SophGer_primeI : ‹odd p ⟹ prime p ⟹ prime (2 * p + 1) ⟹ SG p›
unfolding SophGer_prime_def by simp
lemma SophGer_primeD : ‹odd p› ‹prime p› ‹prime (2 * p + 1)› if ‹SG p›
using that unfolding SophGer_prime_def by simp_all
text ‹We can easily compute Sophie Germain primes less than \<^term>‹2000 :: nat›.›
value ‹[p. p ← [0..2000], SG (nat p)]›
context fixes p assumes ‹SG p› begin
local_setup ‹Local_Theory.map_background_naming (Name_Space.mandatory_path "SG_simps")›
lemma nonzero : ‹p ≠ 0› using ‹SG p› by (simp add: odd_pos SophGer_primeD(1))
lemma pos : ‹0 < p› using nonzero by blast
lemma ge_3 : ‹3 ≤ p›
by (metis ‹SG p› SophGer_prime_def gcd_nat.order_iff_strict not_less_eq_eq
numeral_2_eq_2 numeral_3_eq_3 order_antisym_conv prime_ge_2_nat)
lemma ge_7 : ‹7 ≤ 2 * p + 1› using ge_3 by auto
lemma notcong_zero :
‹[- 3 ≠ 0 :: int] (mod 2 * p + 1)› ‹[- 1 ≠ 0 :: int] (mod 2 * p + 1)›
‹[ 1 ≠ 0 :: int] (mod 2 * p + 1)› ‹[ 3 ≠ 0 :: int] (mod 2 * p + 1)›
using SophGer_primeD(2)[OF ‹SG p›]
by (simp_all add: cong_def zmod_zminus1_not_zero prime_nat_iff'')
lemma notcong_p :
‹[- 1 ≠ p :: int] (mod 2 * p + 1)›
‹[ 0 ≠ p :: int] (mod 2 * p + 1)›
‹[ 1 ≠ p :: int] (mod 2 * p + 1)›
using SophGer_primeD(2)[OF ‹SG p›]
by (auto simp add: pos cong_def zmod_zminus1_eq_if)
lemma p_th_power_mod_q :
‹[m ^ p = 1] (mod 2 * p + 1) ∨ [m ^ p = - 1] (mod 2 * p + 1)›
if ‹¬ 2 * p + 1 dvd m› for m :: int
proof -
wlog ‹0 < m› generalizing m keeping that
by (cases ‹0 < - m›)
(metis (no_types, opaque_lifting) ‹¬ 2 * p + 1 dvd m› add.inverse_inverse
cong_minus_minus_iff dvd_minus_iff hypothesis uminus_power_if,
use ‹¬ 2 * p + 1 dvd m› ‹¬ 0 < m› in auto)
with ‹¬ 2 * p + 1 dvd m› obtain n where ‹m = int n› ‹¬ 2 * p + 1 dvd n›
by (metis int_dvd_int_iff pos_int_cases)
from ‹0 < m› have ‹0 < m ^ p› by simp
have ‹[m ^ (2 * p) = n ^ (2 * p)] (mod 2 * p + 1)› by (simp add: ‹m = int n›)
moreover have ‹[n ^ (2 * p) = 1] (mod 2 * p + 1)›
by (metis SophGer_prime_def ‹SG p› ‹¬ 2 * p + 1 dvd n› add_implies_diff fermat_theorem)
ultimately have ‹[m ^ (2 * p) = 1] (mod 2 * p + 1)› by (metis cong_def int_ops(2) zmod_int)
also have ‹m ^ (2 * p) = m ^ p * m ^ p› by (simp add: mult_2 power_add)
finally have ‹[m ^ p * m ^ p = 1] (mod 2 * p + 1)› .
thus ‹[m ^ p = 1] (mod 2 * p + 1) ∨ [m ^ p = - 1] (mod 2 * p + 1)›
by (meson SophGer_primeD(3) ‹0 < m ^ p› ‹SG p› cong_square prime_nat_int_transfer)
qed
end
subsection ‹Fermat's little Theorem for Integers›
lemma fermat_theorem_int :
‹[a ^ (p - 1) = 1] (mod p)› if ‹prime p› and ‹¬ p dvd a›
for p :: nat and a :: int
proof (cases a)
show ‹a = int n ⟹ [a ^ (p - 1) = 1] (mod p)› for n
by (metis cong_int_iff fermat_theorem int_dvd_int_iff of_nat_1 of_nat_power that)
next
fix n assume ‹a = - int (Suc n)›
from ‹prime p› have ‹p = 2 ∨ odd p›
by (metis prime_prime_factor two_is_prime_nat)
thus ‹[a ^ (p - 1) = 1] (mod p)›
proof (elim disjE)
assume ‹p = 2›
with ‹¬ p dvd a› have ‹[a = 1] (mod p)› by (simp add: cong_iff_dvd_diff)
with ‹p = 2› show ‹[a ^ (p - 1) = 1] (mod p)› by simp
next
assume ‹odd p›
hence ‹even (p - 1)› by simp
hence ‹a ^ (p - 1) = (int (Suc n)) ^ (p - 1)›
by (metis ‹a = - int (Suc n)› uminus_power_if)
also have ‹[… = 1] (mod p)›
by (metis ‹a = - int (Suc n)› cong_int_iff dvd_minus_iff
fermat_theorem int_dvd_int_iff of_nat_1 of_nat_power that)
finally show ‹[a ^ (p - 1) = 1] (mod p)› .
qed
qed
end