(* Title: HOL/Quadratic_Reciprocity/Euler.thy ID: $Id: Euler.thy,v 1.10 2005/08/01 17:20:28 wenzelm Exp $ Authors: Jeremy Avigad, David Gray, and Adam Kramer *) header {* Euler's criterion *} theory Euler imports Residues EvenOdd begin constdefs MultInvPair :: "int => int => int => int set" "MultInvPair a p j == {StandardRes p j, StandardRes p (a * (MultInv p j))}" SetS :: "int => int => int set set" "SetS a p == ((MultInvPair a p) ` (SRStar p))" (****************************************************************) (* *) (* Property for MultInvPair *) (* *) (****************************************************************) lemma MultInvPair_prop1a: "[| zprime p; 2 < p; ~([a = 0](mod p)); X ∈ (SetS a p); Y ∈ (SetS a p); ~((X ∩ Y) = {}) |] ==> X = Y" apply (auto simp add: SetS_def) apply (drule StandardRes_SRStar_prop1a)+ defer 1 apply (drule StandardRes_SRStar_prop1a)+ apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym) apply (drule notE, rule MultInv_zcong_prop1, auto) apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym) apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym) apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym) apply (drule MultInv_zcong_prop1, auto) apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym) apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym) apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym) done lemma MultInvPair_prop1b: "[| zprime p; 2 < p; ~([a = 0](mod p)); X ∈ (SetS a p); Y ∈ (SetS a p); X ≠ Y |] ==> X ∩ Y = {}" apply (rule notnotD) apply (rule notI) apply (drule MultInvPair_prop1a, auto) done lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> ∀X ∈ SetS a p. ∀Y ∈ SetS a p. X ≠ Y --> X∩Y = {}" by (auto simp add: MultInvPair_prop1b) lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> Union ( SetS a p) = SRStar p" apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4 SRStar_mult_prop2) apply (frule StandardRes_SRStar_prop3) apply (rule bexI, auto) done lemma MultInvPair_distinct: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~([j = 0] (mod p)); ~(QuadRes p a) |] ==> ~([j = a * MultInv p j] (mod p))" apply auto proof - assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~([j = 0] (mod p))" and "~(QuadRes p a)" assume "[j = a * MultInv p j] (mod p)" then have "[j * j = (a * MultInv p j) * j] (mod p)" by (auto simp add: zcong_scalar) then have a:"[j * j = a * (MultInv p j * j)] (mod p)" by (auto simp add: zmult_ac) have "[j * j = a] (mod p)" proof - from prems have b: "[MultInv p j * j = 1] (mod p)" by (simp add: MultInv_prop2a) from b a show ?thesis by (auto simp add: zcong_zmult_prop2) qed then have "[j^2 = a] (mod p)" apply(subgoal_tac "2 = Suc(Suc(0))") apply (erule ssubst) apply (auto simp only: power_Suc power_0) by auto with prems show False by (simp add: QuadRes_def) qed lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a); ~([j = 0] (mod p)) |] ==> card (MultInvPair a p j) = 2" apply (auto simp add: MultInvPair_def) apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))") apply auto apply (simp only: StandardRes_prop2) apply (drule MultInvPair_distinct) by auto (****************************************************************) (* *) (* Properties of SetS *) (* *) (****************************************************************) lemma SetS_finite: "2 < p ==> finite (SetS a p)" by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI) lemma SetS_elems_finite: "∀X ∈ SetS a p. finite X" by (auto simp add: SetS_def MultInvPair_def) lemma SetS_elems_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> ∀X ∈ SetS a p. card X = 2" apply (auto simp add: SetS_def) apply (frule StandardRes_SRStar_prop1a) apply (rule MultInvPair_card_two, auto) done lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))" by (auto simp add: SetS_finite SetS_elems_finite finite_Union) lemma card_setsum_aux: "[| finite S; ∀X ∈ S. finite (X::int set); ∀X ∈ S. card X = n |] ==> setsum card S = setsum (%x. n) S" by (induct set: Finites, auto) lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> int(card(SetS a p)) = (p - 1) div 2" proof - assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)" then have "(p - 1) = 2 * int(card(SetS a p))" proof - have "p - 1 = int(card(Union (SetS a p)))" by (auto simp add: prems MultInvPair_prop2 SRStar_card) also have "... = int (setsum card (SetS a p))" by (auto simp add: prems SetS_finite SetS_elems_finite MultInvPair_prop1c [of p a] card_Union_disjoint) also have "... = int(setsum (%x.2) (SetS a p))" apply (insert prems) apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite card_setsum_aux simp del: setsum_constant) done also have "... = 2 * int(card( SetS a p))" by (auto simp add: prems SetS_finite setsum_const2) finally show ?thesis . qed from this show ?thesis by auto qed lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a); x ∈ (SetS a p) |] ==> [∏x = a] (mod p)" apply (auto simp add: SetS_def MultInvPair_def) apply (frule StandardRes_SRStar_prop1a) apply (subgoal_tac "StandardRes p x ≠ StandardRes p (a * MultInv p x)") apply (auto simp add: StandardRes_prop2 MultInvPair_distinct) apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in StandardRes_prop4) apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)") apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and b = "x * (a * MultInv p x)" and c = "a * (x * MultInv p x)" in zcong_trans, force) apply (frule_tac p = p and x = x in MultInv_prop2, auto) apply (drule_tac a = "x * MultInv p x" and b = 1 in zcong_zmult_prop2) apply (auto simp add: zmult_ac) done lemma aux1: "[| 0 < x; (x::int) < a; x ≠ (a - 1) |] ==> x < a - 1" by arith lemma aux2: "[| (a::int) < c; b < c |] ==> (a ≤ b | b ≤ a)" by auto lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} ∪ (d22set (p - 1))" apply (induct p rule: d22set.induct, auto) apply (simp add: SRStar_def d22set.simps) apply (simp add: SRStar_def d22set.simps, clarify) apply (frule aux1) apply (frule aux2, auto) apply (simp_all add: SRStar_def) apply (simp add: d22set.simps) apply (frule d22set_le) apply (frule d22set_g_1, auto) done lemma Union_SetS_setprod_prop1: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> [∏(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)" proof - assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)" then have "[∏(Union (SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)" by (auto simp add: SetS_finite SetS_elems_finite MultInvPair_prop1c setprod_Union_disjoint) also have "[setprod (setprod (%x. x)) (SetS a p) = setprod (%x. a) (SetS a p)] (mod p)" apply (rule setprod_same_function_zcong) by (auto simp add: prems SetS_setprod_prop SetS_finite) also (zcong_trans) have "[setprod (%x. a) (SetS a p) = a^(card (SetS a p))] (mod p)" by (auto simp add: prems SetS_finite setprod_constant) finally (zcong_trans) show ?thesis apply (rule zcong_trans) apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto) apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force) apply (auto simp add: prems SetS_card) done qed lemma Union_SetS_setprod_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> ∏(Union (SetS a p)) = zfact (p - 1)" proof - assume "zprime p" and "2 < p" and "~([a = 0](mod p))" then have "∏(Union (SetS a p)) = ∏(SRStar p)" by (auto simp add: MultInvPair_prop2) also have "... = ∏({1} ∪ (d22set (p - 1)))" by (auto simp add: prems SRStar_d22set_prop) also have "... = zfact(p - 1)" proof - have "~(1 ∈ d22set (p - 1)) & finite( d22set (p - 1))" apply (insert prems, auto) apply (drule d22set_g_1) apply (auto simp add: d22set_fin) done then have "∏({1} ∪ (d22set (p - 1))) = ∏(d22set (p - 1))" by auto then show ?thesis by (auto simp add: d22set_prod_zfact) qed finally show ?thesis . qed lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)" apply (frule Union_SetS_setprod_prop1) apply (auto simp add: Union_SetS_setprod_prop2) done (****************************************************************) (* *) (* Prove the first part of Euler's Criterion: *) (* ~(QuadRes p x) |] ==> *) (* [x^(nat (((p) - 1) div 2)) = -1](mod p) *) (* *) (****************************************************************) lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); ~(QuadRes p x) |] ==> [x^(nat (((p) - 1) div 2)) = -1](mod p)" apply (frule zfact_prop, auto) apply (frule Wilson_Russ) apply (auto simp add: zcong_sym) apply (rule zcong_trans, auto) done (********************************************************************) (* *) (* Prove another part of Euler Criterion: *) (* [a = 0] (mod p) ==> [0 = a ^ nat ((p - 1) div 2)] (mod p) *) (* *) (********************************************************************) lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)" proof - assume "0 < p" then have "a ^ (nat p) = a ^ (1 + (nat p - 1))" by (auto simp add: diff_add_assoc) also have "... = (a ^ 1) * a ^ (nat(p) - 1)" by (simp only: zpower_zadd_distrib) also have "... = a * a ^ (nat(p) - 1)" by auto finally show ?thesis . qed lemma aux_2: "[| (2::int) < p; p ∈ zOdd |] ==> 0 < ((p - 1) div 2)" proof - assume "2 < p" and "p ∈ zOdd" then have "(p - 1):zEven" by (auto simp add: zEven_def zOdd_def) then have aux_1: "2 * ((p - 1) div 2) = (p - 1)" by (auto simp add: even_div_2_prop2) then have "1 < (p - 1)" by auto then have " 1 < (2 * ((p - 1) div 2))" by (auto simp add: aux_1) then have "0 < (2 * ((p - 1) div 2)) div 2" by auto then show ?thesis by auto qed lemma Euler_part2: "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)" apply (frule zprime_zOdd_eq_grt_2) apply (frule aux_2, auto) apply (frule_tac a = a in aux_1, auto) apply (frule zcong_zmult_prop1, auto) done (****************************************************************) (* *) (* Prove the final part of Euler's Criterion: *) (* QuadRes p x |] ==> *) (* [x^(nat (((p) - 1) div 2)) = 1](mod p) *) (* *) (****************************************************************) lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)" apply (subgoal_tac "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~([y ^ 2 = 0] (mod p))") apply (auto simp add: zcong_sym [of "y^2" x p] intro: zcong_trans) apply (auto simp add: zcong_eq_zdvd_prop intro: zpower_zdvd_prop1) done lemma aux__2: "2 * nat((p - 1) div 2) = nat (2 * ((p - 1) div 2))" by (auto simp add: nat_mult_distrib) lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==> [x^(nat (((p) - 1) div 2)) = 1](mod p)" apply (subgoal_tac "p ∈ zOdd") apply (auto simp add: QuadRes_def) apply (frule aux__1, auto) apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower) apply (auto simp add: zpower_zpower) apply (rule zcong_trans) apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"]) apply (simp add: aux__2) apply (frule odd_minus_one_even) apply (frule even_div_2_prop2) apply (auto intro: Little_Fermat simp add: zprime_zOdd_eq_grt_2) done (********************************************************************) (* *) (* Finally show Euler's Criterion *) (* *) (********************************************************************) theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)" apply (auto simp add: Legendre_def Euler_part2) apply (frule Euler_part3, auto simp add: zcong_sym) apply (frule Euler_part1, auto simp add: zcong_sym) done end
lemma MultInvPair_prop1a:
[| zprime p; 2 < p; ¬ [a = 0] (mod p); X ∈ SetS a p; Y ∈ SetS a p; X ∩ Y ≠ {} |] ==> X = Y
lemma MultInvPair_prop1b:
[| zprime p; 2 < p; ¬ [a = 0] (mod p); X ∈ SetS a p; Y ∈ SetS a p; X ≠ Y |] ==> X ∩ Y = {}
lemma MultInvPair_prop1c:
[| zprime p; 2 < p; ¬ [a = 0] (mod p) |] ==> ∀X∈SetS a p. ∀Y∈SetS a p. X ≠ Y --> X ∩ Y = {}
lemma MultInvPair_prop2:
[| zprime p; 2 < p; ¬ [a = 0] (mod p) |] ==> Union (SetS a p) = SRStar p
lemma MultInvPair_distinct:
[| zprime p; 2 < p; ¬ [a = 0] (mod p); ¬ [j = 0] (mod p); ¬ QuadRes p a |] ==> ¬ [j = a * MultInv p j] (mod p)
lemma MultInvPair_card_two:
[| zprime p; 2 < p; ¬ [a = 0] (mod p); ¬ QuadRes p a; ¬ [j = 0] (mod p) |] ==> card (MultInvPair a p j) = 2
lemma SetS_finite:
2 < p ==> finite (SetS a p)
lemma SetS_elems_finite:
∀X∈SetS a p. finite X
lemma SetS_elems_card:
[| zprime p; 2 < p; ¬ [a = 0] (mod p); ¬ QuadRes p a |] ==> ∀X∈SetS a p. card X = 2
lemma Union_SetS_finite:
2 < p ==> finite (Union (SetS a p))
lemma card_setsum_aux:
[| finite S; ∀X∈S. finite X; ∀X∈S. card X = n |] ==> setsum card S = (∑x∈S. n)
lemma SetS_card:
[| zprime p; 2 < p; ¬ [a = 0] (mod p); ¬ QuadRes p a |] ==> int (card (SetS a p)) = (p - 1) div 2
lemma SetS_setprod_prop:
[| zprime p; 2 < p; ¬ [a = 0] (mod p); ¬ QuadRes p a; x ∈ SetS a p |] ==> [∏x = a] (mod p)
lemma aux1:
[| 0 < x; x < a; x ≠ a - 1 |] ==> x < a - 1
lemma aux2:
[| a < c; b < c |] ==> a ≤ b ∨ b ≤ a
lemma SRStar_d22set_prop:
2 < p ==> SRStar p = {1} ∪ d22set (p - 1)
lemma Union_SetS_setprod_prop1:
[| zprime p; 2 < p; ¬ [a = 0] (mod p); ¬ QuadRes p a |] ==> [∏(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)
lemma Union_SetS_setprod_prop2:
[| zprime p; 2 < p; ¬ [a = 0] (mod p) |] ==> ∏(Union (SetS a p)) = zfact (p - 1)
lemma zfact_prop:
[| zprime p; 2 < p; ¬ [a = 0] (mod p); ¬ QuadRes p a |] ==> [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)
lemma Euler_part1:
[| 2 < p; zprime p; ¬ [x = 0] (mod p); ¬ QuadRes p x |] ==> [x ^ nat ((p - 1) div 2) = -1] (mod p)
lemma aux_1:
0 < p ==> a ^ nat p = a * a ^ (nat p - 1)
lemma aux_2:
[| 2 < p; p ∈ zOdd |] ==> 0 < (p - 1) div 2
lemma Euler_part2:
[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)
lemma aux__1:
[| ¬ [x = 0] (mod p); [y² = x] (mod p) |] ==> ¬ p dvd y
lemma aux__2:
2 * nat ((p - 1) div 2) = nat (2 * ((p - 1) div 2))
lemma Euler_part3:
[| 2 < p; zprime p; ¬ [x = 0] (mod p); QuadRes p x |] ==> [x ^ nat ((p - 1) div 2) = 1] (mod p)
theorem Euler_Criterion:
[| 2 < p; zprime p |] ==> [Legendre a p = a ^ nat ((p - 1) div 2)] (mod p)