lp15@55730: (* Authors: Jeremy Avigad, David Gray, and Adam Kramer lp15@55730: lp15@55730: Ported by lcp but unfinished lp15@55730: *) lp15@55730: lp15@55730: header {* Gauss' Lemma *} lp15@55730: lp15@55730: theory Gauss lp15@55730: imports Residues lp15@55730: begin lp15@55730: lp15@55730: lemma cong_prime_prod_zero_nat: lp15@55730: fixes a::nat lp15@55730: shows "\[a * b = 0] (mod p); prime p\ \ [a = 0] (mod p) | [b = 0] (mod p)" lp15@55730: by (auto simp add: cong_altdef_nat) lp15@55730: lp15@55730: lemma cong_prime_prod_zero_int: lp15@55730: fixes a::int lp15@55730: shows "\[a * b = 0] (mod p); prime p\ \ [a = 0] (mod p) | [b = 0] (mod p)" lp15@55730: by (auto simp add: cong_altdef_int) lp15@55730: lp15@55730: lp15@55730: locale GAUSS = lp15@55730: fixes p :: "nat" lp15@55730: fixes a :: "int" lp15@55730: lp15@55730: assumes p_prime: "prime p" lp15@55730: assumes p_ge_2: "2 < p" lp15@55730: assumes p_a_relprime: "[a \ 0](mod p)" lp15@55730: assumes a_nonzero: "0 < a" lp15@55730: begin lp15@55730: lp15@55730: definition "A = {0::int <.. ((int p - 1) div 2)}" lp15@55730: definition "B = (\x. x * a) ` A" lp15@55730: definition "C = (\x. x mod p) ` B" lp15@55730: definition "D = C \ {.. (int p - 1) div 2}" lp15@55730: definition "E = C \ {(int p - 1) div 2 <..}" lp15@55730: definition "F = (\x. (int p - x)) ` E" lp15@55730: lp15@55730: lp15@55730: subsection {* Basic properties of p *} lp15@55730: lp15@55730: lemma odd_p: "odd p" lp15@55730: by (metis p_prime p_ge_2 prime_odd_nat) lp15@55730: lp15@55730: lemma p_minus_one_l: "(int p - 1) div 2 < p" lp15@55730: proof - lp15@55730: have "(p - 1) div 2 \ (p - 1) div 1" lp15@55730: by (metis div_by_1 div_le_dividend) lp15@55730: also have "\ = p - 1" by simp lp15@55730: finally show ?thesis using p_ge_2 by arith lp15@55730: qed lp15@55730: lp15@55730: lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1" lp15@55730: using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"] lp15@55730: by auto presburger lp15@55730: lp15@55730: lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0 E" lp15@55730: by (auto simp add: C_def D_def E_def) lp15@55730: lp15@55730: lemma A_card_eq: "card A = nat ((int p - 1) div 2)" lp15@55730: by (auto simp add: A_def) lp15@55730: lp15@55730: lemma inj_on_xa_A: "inj_on (\x. x * a) A" lp15@55730: using a_nonzero by (simp add: A_def inj_on_def) lp15@55730: lp15@55730: definition ResSet :: "int => int set => bool" lp15@55730: where "ResSet m X = (\y1 y2. (y1 \ X & y2 \ X & [y1 = y2] (mod m) --> y1 = y2))" lp15@55730: lp15@55730: lemma ResSet_image: lp15@55730: "\ 0 < m; ResSet m A; \x \ A. \y \ A. ([f x = f y](mod m) --> x = y) \ \ lp15@55730: ResSet m (f ` A)" lp15@55730: by (auto simp add: ResSet_def) lp15@55730: lp15@55730: lemma A_res: "ResSet p A" lp15@55730: using p_ge_2 lp15@55730: by (auto simp add: A_def ResSet_def intro!: cong_less_imp_eq_int) lp15@55730: lp15@55730: lemma B_res: "ResSet p B" lp15@55730: proof - lp15@55730: {fix x fix y lp15@55730: assume a: "[x * a = y * a] (mod p)" lp15@55730: assume b: "0 < x" lp15@55730: assume c: "x \ (int p - 1) div 2" lp15@55730: assume d: "0 < y" lp15@55730: assume e: "y \ (int p - 1) div 2" lp15@55730: from a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y] lp15@55730: have "[x = y](mod p)" lp15@55730: by (metis comm_monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int lp15@55730: cong_mult_self_int gcd_int.commute prime_imp_coprime_int) lp15@55730: with cong_less_imp_eq_int [of x y p] p_minus_one_l lp15@55730: order_le_less_trans [of x "(int p - 1) div 2" p] lp15@55730: order_le_less_trans [of y "(int p - 1) div 2" p] lp15@55730: have "x = y" lp15@55730: by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int) lp15@55730: } note xy = this lp15@55730: show ?thesis lp15@55730: apply (insert p_ge_2 p_a_relprime p_minus_one_l) lp15@55730: apply (auto simp add: B_def) lp15@55730: apply (rule ResSet_image) lp15@55730: apply (auto simp add: A_res) lp15@55730: apply (auto simp add: A_def xy) lp15@55730: done lp15@55730: qed lp15@55730: lp15@55730: lemma SR_B_inj: "inj_on (\x. x mod p) B" lp15@55730: proof - lp15@55730: { fix x fix y lp15@55730: assume a: "x * a mod p = y * a mod p" lp15@55730: assume b: "0 < x" lp15@55730: assume c: "x \ (int p - 1) div 2" lp15@55730: assume d: "0 < y" lp15@55730: assume e: "y \ (int p - 1) div 2" lp15@55730: assume f: "x \ y" lp15@55730: from a have "[x * a = y * a](mod p)" lp15@55730: by (metis cong_int_def) lp15@55730: with p_a_relprime p_prime cong_mult_rcancel_int [of a p x y] lp15@55730: have "[x = y](mod p)" lp15@55730: by (metis cong_mult_self_int dvd_div_mult_self gcd_commute_int prime_imp_coprime_int) lp15@55730: with cong_less_imp_eq_int [of x y p] p_minus_one_l lp15@55730: order_le_less_trans [of x "(int p - 1) div 2" p] lp15@55730: order_le_less_trans [of y "(int p - 1) div 2" p] lp15@55730: have "x = y" lp15@55730: by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int) lp15@55730: then have False lp15@55730: by (simp add: f)} lp15@55730: then show ?thesis lp15@55730: by (auto simp add: B_def inj_on_def A_def) metis lp15@55730: qed lp15@55730: lp15@55730: lemma inj_on_pminusx_E: "inj_on (\x. p - x) E" lp15@55730: apply (auto simp add: E_def C_def B_def A_def) lp15@55730: apply (rule_tac g = "(op - (int p))" in inj_on_inverseI) lp15@55730: apply auto lp15@55730: done lp15@55730: lp15@55730: lemma nonzero_mod_p: lp15@55730: fixes x::int shows "\0 < x; x < int p\ \ [x \ 0](mod p)" lp15@55730: by (metis Nat_Transfer.transfer_nat_int_function_closures(9) cong_less_imp_eq_int lp15@55730: inf.semilattice_strict_iff_order int_less_0_conv le_numeral_extra(3) zero_less_imp_eq_int) lp15@55730: lp15@55730: lemma A_ncong_p: "x \ A \ [x \ 0](mod p)" lp15@55730: by (rule nonzero_mod_p) (auto simp add: A_def) lp15@55730: lp15@55730: lemma A_greater_zero: "x \ A \ 0 < x" lp15@55730: by (auto simp add: A_def) lp15@55730: lp15@55730: lemma B_ncong_p: "x \ B \ [x \ 0](mod p)" lp15@55730: by (auto simp add: B_def) (metis cong_prime_prod_zero_int A_ncong_p p_a_relprime p_prime) lp15@55730: lp15@55730: lemma B_greater_zero: "x \ B \ 0 < x" nipkow@56544: using a_nonzero by (auto simp add: B_def A_greater_zero) lp15@55730: lp15@55730: lemma C_greater_zero: "y \ C \ 0 < y" lp15@55730: proof (auto simp add: C_def) lp15@55730: fix x :: int lp15@55730: assume a1: "x \ B" lp15@55730: have f2: "\x\<^sub>1. int x\<^sub>1 = 0 \ 0 < int x\<^sub>1" by linarith lp15@55730: have "x mod int p \ 0" using a1 B_ncong_p cong_int_def by simp lp15@55730: thus "0 < x mod int p" using a1 f2 lp15@55730: by (metis (no_types) B_greater_zero Divides.transfer_int_nat_functions(2) zero_less_imp_eq_int) lp15@55730: qed lp15@55730: lp15@55730: lemma F_subset: "F \ {x. 0 < x & x \ ((int p - 1) div 2)}" lp15@55730: apply (auto simp add: F_def E_def C_def) lp15@55730: apply (metis p_ge_2 Divides.pos_mod_bound less_diff_eq nat_int plus_int_code(2) zless_nat_conj) lp15@55730: apply (auto intro: p_odd_int) lp15@55730: done lp15@55730: lp15@55730: lemma D_subset: "D \ {x. 0 < x & x \ ((p - 1) div 2)}" lp15@55730: by (auto simp add: D_def C_greater_zero) lp15@55730: lp15@55730: lemma F_eq: "F = {x. \y \ A. ( x = p - ((y*a) mod p) & (int p - 1) div 2 < (y*a) mod p)}" lp15@55730: by (auto simp add: F_def E_def D_def C_def B_def A_def) lp15@55730: lp15@55730: lemma D_eq: "D = {x. \y \ A. ( x = (y*a) mod p & (y*a) mod p \ (int p - 1) div 2)}" lp15@55730: by (auto simp add: D_def C_def B_def A_def) lp15@55730: lp15@55730: lemma all_A_relprime: assumes "x \ A" shows "gcd x p = 1" lp15@55730: using p_prime A_ncong_p [OF assms] lp15@55730: by (simp add: cong_altdef_int) (metis gcd_int.commute prime_imp_coprime_int) lp15@55730: lp15@55730: lemma A_prod_relprime: "gcd (setprod id A) p = 1" lp15@55730: by (metis DEADID.map_id all_A_relprime setprod_coprime_int) lp15@55730: lp15@55730: lp15@55730: subsection {* Relationships Between Gauss Sets *} lp15@55730: lp15@55730: lemma StandardRes_inj_on_ResSet: "ResSet m X \ (inj_on (\b. b mod m) X)" lp15@55730: by (auto simp add: ResSet_def inj_on_def cong_int_def) lp15@55730: lp15@55730: lemma B_card_eq_A: "card B = card A" lp15@55730: using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image) lp15@55730: lp15@55730: lemma B_card_eq: "card B = nat ((int p - 1) div 2)" lp15@55730: by (simp add: B_card_eq_A A_card_eq) lp15@55730: lp15@55730: lemma F_card_eq_E: "card F = card E" lp15@55730: using finite_E lp15@55730: by (simp add: F_def inj_on_pminusx_E card_image) lp15@55730: lp15@55730: lemma C_card_eq_B: "card C = card B" lp15@55730: proof - lp15@55730: have "inj_on (\x. x mod p) B" lp15@55730: by (metis SR_B_inj) lp15@55730: then show ?thesis lp15@55730: by (metis C_def card_image) lp15@55730: qed lp15@55730: lp15@55730: lemma D_E_disj: "D \ E = {}" lp15@55730: by (auto simp add: D_def E_def) lp15@55730: lp15@55730: lemma C_card_eq_D_plus_E: "card C = card D + card E" lp15@55730: by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E) lp15@55730: lp15@55730: lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C" haftmann@57418: by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod.union_disjoint sup_commute) lp15@55730: lp15@55730: lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)" lp15@55730: apply (auto simp add: C_def) lp15@55730: apply (insert finite_B SR_B_inj) haftmann@57418: apply (drule setprod.reindex [of "\x. x mod int p" B id]) haftmann@57418: apply auto lp15@55730: apply (rule cong_setprod_int) lp15@55730: apply (auto simp add: cong_int_def) lp15@55730: done lp15@55730: lp15@55730: lemma F_Un_D_subset: "(F \ D) \ A" lp15@55730: apply (intro Un_least subset_trans [OF F_subset] subset_trans [OF D_subset]) lp15@55730: apply (auto simp add: A_def) lp15@55730: done lp15@55730: lp15@55730: lemma F_D_disj: "(F \ D) = {}" lp15@55730: proof (auto simp add: F_eq D_eq) lp15@55730: fix y::int and z::int lp15@55730: assume "p - (y*a) mod p = (z*a) mod p" lp15@55730: then have "[(y*a) mod p + (z*a) mod p = 0] (mod p)" lp15@55730: by (metis add_commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0) lp15@55730: moreover have "[y * a = (y*a) mod p] (mod p)" lp15@55730: by (metis cong_int_def mod_mod_trivial) lp15@55730: ultimately have "[a * (y + z) = 0] (mod p)" lp15@55730: by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult_commute ring_class.ring_distribs(1)) lp15@55730: with p_prime a_nonzero p_a_relprime lp15@55730: have a: "[y + z = 0] (mod p)" lp15@55730: by (metis cong_prime_prod_zero_int) lp15@55730: assume b: "y \ A" and c: "z \ A" lp15@55730: with A_def have "0 < y + z" lp15@55730: by auto lp15@55730: moreover from b c p_eq2 A_def have "y + z < p" lp15@55730: by auto lp15@55730: ultimately show False lp15@55730: by (metis a nonzero_mod_p) lp15@55730: qed lp15@55730: lp15@55730: lemma F_Un_D_card: "card (F \ D) = nat ((p - 1) div 2)" lp15@55730: proof - lp15@55730: have "card (F \ D) = card E + card D" lp15@55730: by (auto simp add: finite_F finite_D F_D_disj card_Un_disjoint F_card_eq_E) lp15@55730: then have "card (F \ D) = card C" lp15@55730: by (simp add: C_card_eq_D_plus_E) lp15@55730: then show "card (F \ D) = nat ((p - 1) div 2)" lp15@55730: by (simp add: C_card_eq_B B_card_eq) lp15@55730: qed lp15@55730: lp15@55730: lemma F_Un_D_eq_A: "F \ D = A" lp15@55730: using finite_A F_Un_D_subset A_card_eq F_Un_D_card lp15@55730: by (auto simp add: card_seteq) lp15@55730: lp15@55730: lemma prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A" haftmann@57418: by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod.union_disjoint) lp15@55730: lp15@55730: lemma prod_F_zcong: "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)" lp15@55730: proof - lp15@55730: have FE: "setprod id F = setprod (op - p) E" lp15@55730: apply (auto simp add: F_def) lp15@55730: apply (insert finite_E inj_on_pminusx_E) haftmann@57418: apply (drule setprod.reindex, auto) lp15@55730: done lp15@55730: then have "\x \ E. [(p-x) mod p = - x](mod p)" lp15@55730: by (metis cong_int_def minus_mod_self1 mod_mod_trivial) lp15@55730: then have "[setprod ((\x. x mod p) o (op - p)) E = setprod (uminus) E](mod p)" lp15@55730: using finite_E p_ge_2 lp15@55730: cong_setprod_int [of E "(\x. x mod p) o (op - p)" uminus p] lp15@55730: by auto lp15@55730: then have two: "[setprod id F = setprod (uminus) E](mod p)" lp15@55730: by (metis FE cong_cong_mod_int cong_refl_int cong_setprod_int minus_mod_self1) lp15@55730: have "setprod uminus E = (-1) ^ (card E) * (setprod id E)" lp15@55730: using finite_E by (induct set: finite) auto lp15@55730: with two show ?thesis lp15@55730: by simp lp15@55730: qed lp15@55730: lp15@55730: lp15@55730: subsection {* Gauss' Lemma *} lp15@55730: lp15@55730: lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A" lp15@55730: by (metis (no_types) minus_minus mult_commute mult_left_commute power_minus power_one) lp15@55730: lp15@55730: theorem pre_gauss_lemma: lp15@55730: "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)" lp15@55730: proof - lp15@55730: have "[setprod id A = setprod id F * setprod id D](mod p)" haftmann@57418: by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod.cong) lp15@55730: then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)" lp15@55730: apply (rule cong_trans_int) lp15@55730: apply (metis cong_scalar_int prod_F_zcong) lp15@55730: done lp15@55730: then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)" lp15@55730: by (metis C_prod_eq_D_times_E mult_commute mult_left_commute) lp15@55730: then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)" lp15@55730: by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int) lp15@55730: then have "[setprod id A = ((-1)^(card E) * lp15@55730: (setprod id ((\x. x * a) ` A)))] (mod p)" lp15@55730: by (simp add: B_def) lp15@55730: then have "[setprod id A = ((-1)^(card E) * (setprod (\x. x * a) A))] lp15@55730: (mod p)" haftmann@57418: by (simp add: inj_on_xa_A setprod.reindex) lp15@55730: moreover have "setprod (\x. x * a) A = lp15@55730: setprod (\x. a) A * setprod id A" lp15@55730: using finite_A by (induct set: finite) auto lp15@55730: ultimately have "[setprod id A = ((-1)^(card E) * (setprod (\x. a) A * lp15@55730: setprod id A))] (mod p)" lp15@55730: by simp lp15@55730: then have "[setprod id A = ((-1)^(card E) * a^(card A) * lp15@55730: setprod id A)](mod p)" lp15@55730: apply (rule cong_trans_int) lp15@55730: apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult_assoc) lp15@55730: done lp15@55730: then have a: "[setprod id A * (-1)^(card E) = lp15@55730: ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)" lp15@55730: by (rule cong_scalar_int) lp15@55730: then have "[setprod id A * (-1)^(card E) = setprod id A * lp15@55730: (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)" lp15@55730: apply (rule cong_trans_int) lp15@55730: apply (simp add: a mult_commute mult_left_commute) lp15@55730: done lp15@55730: then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)" lp15@55730: apply (rule cong_trans_int) haftmann@57418: apply (simp add: aux cong del:setprod.cong) lp15@55730: done lp15@55730: with A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)" lp15@55730: by (metis cong_mult_lcancel_int) lp15@55730: then show ?thesis lp15@55730: by (simp add: A_card_eq cong_sym_int) lp15@55730: qed lp15@55730: lp15@55730: (*NOT WORKING. Old_Number_Theory/Euler.thy needs to be translated, but it's lp15@55730: quite a mess and should better be completely redone. lp15@55730: lp15@55730: theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)" lp15@55730: proof - lp15@55730: from Euler_Criterion p_prime p_ge_2 have lp15@55730: "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)" lp15@55730: by auto lp15@55730: moreover note pre_gauss_lemma lp15@55730: ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)" lp15@55730: by (rule cong_trans_int) lp15@55730: moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)" lp15@55730: by (auto simp add: Legendre_def) lp15@55730: moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1" lp15@55730: by (rule neg_one_power) lp15@55730: ultimately show ?thesis lp15@55730: by (auto simp add: p_ge_2 one_not_neg_one_mod_m zcong_sym) lp15@55730: qed lp15@55730: *) lp15@55730: lp15@55730: end lp15@55730: lp15@55730: end