# Theory Euler_Criterion

```(* Author: Jaime Mendizabal Roche *)

theory Euler_Criterion
imports Residues
begin

context
fixes p :: "nat"
fixes a :: "int"

assumes p_prime: "prime p"
assumes p_ge_2: "2 < p"
assumes p_a_relprime: "[a ≠ 0](mod p)"
begin

private lemma odd_p: "odd p"
using p_ge_2 p_prime prime_odd_nat by blast

private lemma p_minus_1_int:
"int (p - 1) = int p - 1"
by (metis of_nat_1 of_nat_diff p_prime prime_ge_1_nat)

private lemma p_not_eq_Suc_0 [simp]:
"p ≠ Suc 0"
using p_ge_2 by simp

private lemma one_mod_int_p_eq [simp]:
"1 mod int p = 1"
proof -
from p_ge_2 have "int 1 mod int p = int 1"
by simp
then show ?thesis
by simp
qed

private lemma E_1:
shows "[a ^ ((p - 1) div 2) = 1] (mod int p)"
proof -
from assms obtain b where b: "[b ^ 2 = a] (mod int p)"
then have "[a ^ ((p - 1) div 2) = b ^ (2 * ((p - 1) div 2))] (mod int p)"
by (simp add: cong_pow cong_sym power_mult)
then have "[a ^ ((p - 1) div 2) = b ^ (p - 1)] (mod int p)"
using odd_p by force
moreover have "[b ^ (p - 1) = 1] (mod int p)"
proof -
have "[nat ¦b¦ ^ (p - 1) = 1] (mod p)"
using p_prime proof (rule fermat_theorem)
from b p_a_relprime show "¬ p dvd nat ¦b¦"
by (auto simp add: cong_iff_dvd_diff power2_eq_square)
(metis cong_iff_dvd_diff cong_dvd_iff dvd_mult2)
qed
then have "nat ¦b¦ ^ (p - 1) mod p = 1 mod p"
then have "int (nat ¦b¦ ^ (p - 1) mod p) = int (1 mod p)"
by simp
moreover from odd_p have "¦b¦ ^ (p - Suc 0) = b ^ (p - Suc 0)"
ultimately show ?thesis
by (auto simp add: cong_def zmod_int)
qed
ultimately show ?thesis
by (auto intro: cong_trans)
qed

private definition S1 :: "int set" where "S1 = {0 <.. int p - 1}"

private definition P :: "int ⇒ int ⇒ bool" where
"P x y ⟷ [x * y = a] (mod p) ∧ y ∈ S1"

private definition f_1 :: "int ⇒ int" where
"f_1 x = (THE y. P x y)"

private definition f :: "int ⇒ int set" where
"f x = {x, f_1 x}"

private definition S2 :: "int set set" where "S2 = f ` S1"

private lemma P_lemma: assumes "x ∈ S1"
shows "∃! y. P x y"
proof -
have "¬ p dvd x" using assms zdvd_not_zless S1_def by auto
hence co_xp: "coprime x p" using p_prime prime_imp_coprime_int[of p x]
then obtain y' where y': "[x * y' = 1] (mod p)" using cong_solve_coprime_int by blast
moreover define y where "y = y' * a mod p"
ultimately have "[x * y = a] (mod p)"
using mod_mult_right_eq [of x "y' * a" p]
cong_scalar_right [of "x * y'" 1 "int p" a]
by (auto simp add: cong_def ac_simps)
moreover have "y ∈ {0 .. int p - 1}" unfolding y_def using p_ge_2 by auto
hence "y ∈ S1" using calculation cong_iff_dvd_diff p_a_relprime S1_def cong_dvd_iff by fastforce
ultimately have "P x y" unfolding P_def by blast
moreover {
fix y1 y2
assume "P x y1" "P x y2"
moreover hence "[y1 = y2] (mod p)" unfolding P_def
using co_xp cong_mult_lcancel[of x p y1 y2] cong_sym cong_trans by blast
ultimately have "y1 = y2" unfolding P_def S1_def using cong_less_imp_eq_int by auto
}
ultimately show ?thesis by blast
qed

private lemma f_1_lemma_1: assumes "x ∈ S1"
shows "P x (f_1 x)" using assms P_lemma theI'[of "P x"] f_1_def by presburger

private lemma f_1_lemma_2: assumes "x ∈ S1"
shows "f_1 (f_1 x) = x"
using assms f_1_lemma_1[of x] f_1_def P_lemma[of "f_1 x"] P_def by (auto simp: mult.commute)

private lemma f_lemma_1: assumes "x ∈ S1"
shows "f x = f (f_1 x)" using f_def f_1_lemma_2[of x] assms by auto

private lemma l1: assumes "¬ QuadRes p a" "x ∈ S1"
shows "x ≠ f_1 x"
using f_1_lemma_1[of x] assms unfolding P_def QuadRes_def power2_eq_square by fastforce

private lemma l2: assumes "¬ QuadRes p a" "x ∈ S1"
shows "[∏ (f x) = a] (mod p)"
using assms l1 f_1_lemma_1 P_def f_def by auto

private lemma l3: assumes "x ∈ S2"
shows "finite x" using assms f_def S2_def by auto

private lemma l4: "S1 = ⋃ S2" using f_1_lemma_1 P_def f_def S2_def by auto

private lemma l5: assumes "x ∈ S2" "y ∈ S2" "x ≠ y"
shows "x ∩ y = {}"
proof -
obtain a b where ab: "x = f a" "a ∈ S1" "y = f b" "b ∈ S1" using assms S2_def by auto
hence "a ≠ b" "a ≠ f_1 b" "f_1 a ≠ b" using assms(3) f_lemma_1 by blast+
moreover hence "f_1 a ≠ f_1 b" using f_1_lemma_2[of a] f_1_lemma_2[of b] ab by force
ultimately show ?thesis using f_def ab by fastforce
qed

private lemma l6: "prod Prod S2 = ∏ S1"
using prod.Union_disjoint[of S2 "λx. x"] l3 l4 l5 unfolding comp_def by auto

private lemma l7: "fact n = ∏ {0 <.. int n}"
proof (induction n)
case (Suc n)
have "int (Suc n) = int n + 1" by simp
hence "insert (int (Suc n)) {0<..int n} = {0<..int (Suc n)}" by auto
thus ?case using prod.insert[of "{0<..int n}" "int (Suc n)" "λx. x"] Suc fact_Suc by auto
qed simp

private lemma l8: "fact (p - 1) = ∏ S1" using l7[of "p - 1"] S1_def p_minus_1_int by presburger

private lemma l9: "[prod Prod S2 = -1] (mod p)"
using l6 l8 wilson_theorem[of p] p_prime by presburger

private lemma l10: assumes "card S = n" "⋀x. x ∈ S ⟹ [g x = a] (mod p)"
shows "[prod g S = a ^ n] (mod p)" using assms
proof (induction n arbitrary: S)
case 0
thus ?case using card_0_eq[of S] prod.empty prod.infinite by fastforce
next
case (Suc n)
then obtain x where x: "x ∈ S" by force
define S' where "S' = S - {x}"
hence "[prod g S' = a ^ n] (mod int p)"
using x Suc(1)[of S'] Suc(2) Suc(3) by (simp add: card_ge_0_finite)
moreover have "prod g S = g x * prod g S'"
using x S'_def Suc(2) prod.remove[of S x g] by fastforce
ultimately show ?case using x Suc(3) cong_mult
by simp blast
qed

private lemma l11: assumes "¬ QuadRes p a"
shows "card S2 = (p - 1) div 2"
proof -
have "sum card S2 = 2 * card S2"
using sum.cong[of S2 S2 card "λx. 2"] l1 f_def S2_def assms by fastforce
moreover have "p - 1 = sum card S2"
using l4 card_UN_disjoint[of S2 "λx. x"] l3 l5 S1_def S2_def by auto
ultimately show ?thesis by linarith
qed

private lemma l12: assumes "¬ QuadRes p a"
shows "[prod Prod S2 = a ^ ((p - 1) div 2)] (mod p)"
using assms l2 l10 l11 unfolding S2_def by blast

private lemma E_2: assumes "¬ QuadRes p a"
shows "[a ^ ((p - 1) div 2) = -1] (mod p)" using l9 l12 cong_trans cong_sym assms by blast

lemma euler_criterion_aux: "[(Legendre a p) = a ^ ((p - 1) div 2)] (mod p)"
using p_a_relprime by (auto simp add: Legendre_def
intro!: cong_sym [of _ 1] cong_sym [of _ "- 1"]
dest: E_1 E_2)

end

theorem euler_criterion: assumes "prime p" "2 < p"
shows "[(Legendre a p) = a ^ ((p - 1) div 2)] (mod p)"
proof (cases "[a = 0] (mod p)")
case True
then have "[a ^ ((p - 1) div 2) = 0 ^ ((p - 1) div 2)] (mod p)"
using cong_pow by blast
moreover have "(0::int) ^ ((p - 1) div 2) = 0"
using zero_power [of "(p - 1) div 2"] assms(2) by simp
ultimately have "[a ^ ((p - 1) div 2) = 0] (mod p)"
using True assms(1) prime_dvd_power_int_iff