src/HOL/Old_Number_Theory/Gauss.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 63566 e5abbdee461a child 64240 eabf80376aab permissions -rw-r--r--
tuned proofs;
 wenzelm@38159 ` 1` ```(* Title: HOL/Old_Number_Theory/Gauss.thy ``` wenzelm@38159 ` 2` ``` Authors: Jeremy Avigad, David Gray, and Adam Kramer ``` paulson@13871 ` 3` ```*) ``` paulson@13871 ` 4` wenzelm@61382 ` 5` ```section \Gauss' Lemma\ ``` paulson@13871 ` 6` haftmann@27556 ` 7` ```theory Gauss ``` haftmann@27556 ` 8` ```imports Euler ``` haftmann@27556 ` 9` ```begin ``` paulson@13871 ` 10` paulson@13871 ` 11` ```locale GAUSS = ``` paulson@13871 ` 12` ``` fixes p :: "int" ``` paulson@13871 ` 13` ``` fixes a :: "int" ``` paulson@13871 ` 14` nipkow@16663 ` 15` ``` assumes p_prime: "zprime p" ``` paulson@13871 ` 16` ``` assumes p_g_2: "2 < p" ``` paulson@13871 ` 17` ``` assumes p_a_relprime: "~[a = 0](mod p)" ``` paulson@13871 ` 18` ``` assumes a_nonzero: "0 < a" ``` wenzelm@21233 ` 19` ```begin ``` paulson@13871 ` 20` wenzelm@38159 ` 21` ```definition "A = {(x::int). 0 < x & x \ ((p - 1) div 2)}" ``` wenzelm@38159 ` 22` ```definition "B = (%x. x * a) ` A" ``` wenzelm@38159 ` 23` ```definition "C = StandardRes p ` B" ``` wenzelm@38159 ` 24` ```definition "D = C \ {x. x \ ((p - 1) div 2)}" ``` wenzelm@38159 ` 25` ```definition "E = C \ {x. ((p - 1) div 2) < x}" ``` wenzelm@38159 ` 26` ```definition "F = (%x. (p - x)) ` E" ``` wenzelm@21233 ` 27` paulson@13871 ` 28` wenzelm@61382 ` 29` ```subsection \Basic properties of p\ ``` paulson@13871 ` 30` wenzelm@21233 ` 31` ```lemma p_odd: "p \ zOdd" ``` paulson@13871 ` 32` ``` by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2) ``` paulson@13871 ` 33` wenzelm@21233 ` 34` ```lemma p_g_0: "0 < p" ``` wenzelm@18369 ` 35` ``` using p_g_2 by auto ``` paulson@13871 ` 36` wenzelm@21233 ` 37` ```lemma int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2" ``` wenzelm@26289 ` 38` ``` using ListMem.insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff) ``` paulson@13871 ` 39` wenzelm@21233 ` 40` ```lemma p_minus_one_l: "(p - 1) div 2 < p" ``` wenzelm@18369 ` 41` ```proof - ``` wenzelm@18369 ` 42` ``` have "(p - 1) div 2 \ (p - 1) div 1" ``` wenzelm@18369 ` 43` ``` by (rule zdiv_mono2) (auto simp add: p_g_0) ``` wenzelm@18369 ` 44` ``` also have "\ = p - 1" by simp ``` wenzelm@18369 ` 45` ``` finally show ?thesis by simp ``` wenzelm@18369 ` 46` ```qed ``` paulson@13871 ` 47` wenzelm@21233 ` 48` ```lemma p_eq: "p = (2 * (p - 1) div 2) + 1" ``` nipkow@30034 ` 49` ``` using div_mult_self1_is_id [of 2 "p - 1"] by auto ``` paulson@13871 ` 50` wenzelm@21233 ` 51` wenzelm@21288 ` 52` ```lemma (in -) zodd_imp_zdiv_eq: "x \ zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)" ``` paulson@13871 ` 53` ``` apply (frule odd_minus_one_even) ``` paulson@13871 ` 54` ``` apply (simp add: zEven_def) ``` paulson@13871 ` 55` ``` apply (subgoal_tac "2 \ 0") ``` nipkow@30034 ` 56` ``` apply (frule_tac b = "2 :: int" and a = "x - 1" in div_mult_self1_is_id) ``` wenzelm@18369 ` 57` ``` apply (auto simp add: even_div_2_prop2) ``` wenzelm@18369 ` 58` ``` done ``` paulson@13871 ` 59` wenzelm@21233 ` 60` wenzelm@21233 ` 61` ```lemma p_eq2: "p = (2 * ((p - 1) div 2)) + 1" ``` paulson@13871 ` 62` ``` apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto) ``` wenzelm@18369 ` 63` ``` apply (frule zodd_imp_zdiv_eq, auto) ``` wenzelm@18369 ` 64` ``` done ``` paulson@13871 ` 65` wenzelm@21233 ` 66` wenzelm@61382 ` 67` ```subsection \Basic Properties of the Gauss Sets\ ``` paulson@13871 ` 68` wenzelm@21233 ` 69` ```lemma finite_A: "finite (A)" ``` bulwahn@46756 ` 70` ```by (auto simp add: A_def) ``` paulson@13871 ` 71` wenzelm@21233 ` 72` ```lemma finite_B: "finite (B)" ``` nipkow@40786 ` 73` ```by (auto simp add: B_def finite_A) ``` paulson@13871 ` 74` wenzelm@21233 ` 75` ```lemma finite_C: "finite (C)" ``` nipkow@40786 ` 76` ```by (auto simp add: C_def finite_B) ``` paulson@13871 ` 77` wenzelm@21233 ` 78` ```lemma finite_D: "finite (D)" ``` wenzelm@41541 ` 79` ```by (auto simp add: D_def finite_C) ``` paulson@13871 ` 80` wenzelm@21233 ` 81` ```lemma finite_E: "finite (E)" ``` wenzelm@41541 ` 82` ```by (auto simp add: E_def finite_C) ``` paulson@13871 ` 83` wenzelm@21233 ` 84` ```lemma finite_F: "finite (F)" ``` nipkow@40786 ` 85` ```by (auto simp add: F_def finite_E) ``` paulson@13871 ` 86` wenzelm@21233 ` 87` ```lemma C_eq: "C = D \ E" ``` nipkow@40786 ` 88` ```by (auto simp add: C_def D_def E_def) ``` paulson@13871 ` 89` wenzelm@21233 ` 90` ```lemma A_card_eq: "card A = nat ((p - 1) div 2)" ``` wenzelm@18369 ` 91` ``` apply (auto simp add: A_def) ``` paulson@13871 ` 92` ``` apply (insert int_nat) ``` paulson@13871 ` 93` ``` apply (erule subst) ``` wenzelm@18369 ` 94` ``` apply (auto simp add: card_bdd_int_set_l_le) ``` wenzelm@18369 ` 95` ``` done ``` paulson@13871 ` 96` wenzelm@21233 ` 97` ```lemma inj_on_xa_A: "inj_on (%x. x * a) A" ``` wenzelm@18369 ` 98` ``` using a_nonzero by (simp add: A_def inj_on_def) ``` paulson@13871 ` 99` wenzelm@21233 ` 100` ```lemma A_res: "ResSet p A" ``` wenzelm@18369 ` 101` ``` apply (auto simp add: A_def ResSet_def) ``` wenzelm@18369 ` 102` ``` apply (rule_tac m = p in zcong_less_eq) ``` wenzelm@18369 ` 103` ``` apply (insert p_g_2, auto) ``` wenzelm@18369 ` 104` ``` done ``` paulson@13871 ` 105` wenzelm@21233 ` 106` ```lemma B_res: "ResSet p B" ``` paulson@13871 ` 107` ``` apply (insert p_g_2 p_a_relprime p_minus_one_l) ``` wenzelm@18369 ` 108` ``` apply (auto simp add: B_def) ``` paulson@13871 ` 109` ``` apply (rule ResSet_image) ``` wenzelm@18369 ` 110` ``` apply (auto simp add: A_res) ``` paulson@13871 ` 111` ``` apply (auto simp add: A_def) ``` wenzelm@18369 ` 112` ```proof - ``` wenzelm@18369 ` 113` ``` fix x fix y ``` wenzelm@18369 ` 114` ``` assume a: "[x * a = y * a] (mod p)" ``` wenzelm@18369 ` 115` ``` assume b: "0 < x" ``` wenzelm@18369 ` 116` ``` assume c: "x \ (p - 1) div 2" ``` wenzelm@18369 ` 117` ``` assume d: "0 < y" ``` wenzelm@18369 ` 118` ``` assume e: "y \ (p - 1) div 2" ``` wenzelm@18369 ` 119` ``` from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] ``` wenzelm@18369 ` 120` ``` have "[x = y](mod p)" ``` wenzelm@18369 ` 121` ``` by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) ``` wenzelm@18369 ` 122` ``` with zcong_less_eq [of x y p] p_minus_one_l ``` wenzelm@18369 ` 123` ``` order_le_less_trans [of x "(p - 1) div 2" p] ``` wenzelm@18369 ` 124` ``` order_le_less_trans [of y "(p - 1) div 2" p] show "x = y" ``` wenzelm@41541 ` 125` ``` by (simp add: b c d e p_minus_one_l p_g_0) ``` wenzelm@18369 ` 126` ```qed ``` paulson@13871 ` 127` wenzelm@21233 ` 128` ```lemma SR_B_inj: "inj_on (StandardRes p) B" ``` wenzelm@41541 ` 129` ``` apply (auto simp add: B_def StandardRes_def inj_on_def A_def) ``` wenzelm@18369 ` 130` ```proof - ``` wenzelm@18369 ` 131` ``` fix x fix y ``` wenzelm@18369 ` 132` ``` assume a: "x * a mod p = y * a mod p" ``` wenzelm@18369 ` 133` ``` assume b: "0 < x" ``` wenzelm@18369 ` 134` ``` assume c: "x \ (p - 1) div 2" ``` wenzelm@18369 ` 135` ``` assume d: "0 < y" ``` wenzelm@18369 ` 136` ``` assume e: "y \ (p - 1) div 2" ``` wenzelm@18369 ` 137` ``` assume f: "x \ y" ``` wenzelm@18369 ` 138` ``` from a have "[x * a = y * a](mod p)" ``` wenzelm@18369 ` 139` ``` by (simp add: zcong_zmod_eq p_g_0) ``` wenzelm@18369 ` 140` ``` with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] ``` wenzelm@18369 ` 141` ``` have "[x = y](mod p)" ``` wenzelm@18369 ` 142` ``` by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) ``` wenzelm@18369 ` 143` ``` with zcong_less_eq [of x y p] p_minus_one_l ``` wenzelm@18369 ` 144` ``` order_le_less_trans [of x "(p - 1) div 2" p] ``` wenzelm@18369 ` 145` ``` order_le_less_trans [of y "(p - 1) div 2" p] have "x = y" ``` wenzelm@41541 ` 146` ``` by (simp add: b c d e p_minus_one_l p_g_0) ``` wenzelm@18369 ` 147` ``` then have False ``` wenzelm@18369 ` 148` ``` by (simp add: f) ``` wenzelm@18369 ` 149` ``` then show "a = 0" ``` wenzelm@18369 ` 150` ``` by simp ``` wenzelm@18369 ` 151` ```qed ``` paulson@13871 ` 152` wenzelm@21233 ` 153` ```lemma inj_on_pminusx_E: "inj_on (%x. p - x) E" ``` paulson@13871 ` 154` ``` apply (auto simp add: E_def C_def B_def A_def) ``` wenzelm@18369 ` 155` ``` apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI) ``` wenzelm@18369 ` 156` ``` apply auto ``` wenzelm@18369 ` 157` ``` done ``` paulson@13871 ` 158` wenzelm@21233 ` 159` ```lemma A_ncong_p: "x \ A ==> ~[x = 0](mod p)" ``` paulson@13871 ` 160` ``` apply (auto simp add: A_def) ``` paulson@13871 ` 161` ``` apply (frule_tac m = p in zcong_not_zero) ``` paulson@13871 ` 162` ``` apply (insert p_minus_one_l) ``` wenzelm@18369 ` 163` ``` apply auto ``` wenzelm@18369 ` 164` ``` done ``` paulson@13871 ` 165` wenzelm@21233 ` 166` ```lemma A_greater_zero: "x \ A ==> 0 < x" ``` paulson@13871 ` 167` ``` by (auto simp add: A_def) ``` paulson@13871 ` 168` wenzelm@21233 ` 169` ```lemma B_ncong_p: "x \ B ==> ~[x = 0](mod p)" ``` paulson@13871 ` 170` ``` apply (auto simp add: B_def) ``` wenzelm@18369 ` 171` ``` apply (frule A_ncong_p) ``` paulson@13871 ` 172` ``` apply (insert p_a_relprime p_prime a_nonzero) ``` thomas@57492 ` 173` ``` apply (frule_tac a = xa and b = a in zcong_zprime_prod_zero_contra) ``` wenzelm@18369 ` 174` ``` apply (auto simp add: A_greater_zero) ``` wenzelm@18369 ` 175` ``` done ``` paulson@13871 ` 176` wenzelm@21233 ` 177` ```lemma B_greater_zero: "x \ B ==> 0 < x" ``` nipkow@56544 ` 178` ``` using a_nonzero by (auto simp add: B_def A_greater_zero) ``` paulson@13871 ` 179` wenzelm@21233 ` 180` ```lemma C_ncong_p: "x \ C ==> ~[x = 0](mod p)" ``` paulson@13871 ` 181` ``` apply (auto simp add: C_def) ``` paulson@13871 ` 182` ``` apply (frule B_ncong_p) ``` thomas@57492 ` 183` ``` apply (subgoal_tac "[xa = StandardRes p xa](mod p)") ``` wenzelm@18369 ` 184` ``` defer apply (simp add: StandardRes_prop1) ``` thomas@57492 ` 185` ``` apply (frule_tac a = xa and b = "StandardRes p xa" and c = 0 in zcong_trans) ``` wenzelm@18369 ` 186` ``` apply auto ``` wenzelm@18369 ` 187` ``` done ``` paulson@13871 ` 188` wenzelm@21233 ` 189` ```lemma C_greater_zero: "y \ C ==> 0 < y" ``` paulson@13871 ` 190` ``` apply (auto simp add: C_def) ``` wenzelm@18369 ` 191` ```proof - ``` wenzelm@18369 ` 192` ``` fix x ``` wenzelm@18369 ` 193` ``` assume a: "x \ B" ``` wenzelm@18369 ` 194` ``` from p_g_0 have "0 \ StandardRes p x" ``` wenzelm@18369 ` 195` ``` by (simp add: StandardRes_lbound) ``` wenzelm@18369 ` 196` ``` moreover have "~[x = 0] (mod p)" ``` wenzelm@18369 ` 197` ``` by (simp add: a B_ncong_p) ``` wenzelm@18369 ` 198` ``` then have "StandardRes p x \ 0" ``` wenzelm@18369 ` 199` ``` by (simp add: StandardRes_prop3) ``` wenzelm@18369 ` 200` ``` ultimately show "0 < StandardRes p x" ``` wenzelm@18369 ` 201` ``` by (simp add: order_le_less) ``` wenzelm@18369 ` 202` ```qed ``` paulson@13871 ` 203` wenzelm@21233 ` 204` ```lemma D_ncong_p: "x \ D ==> ~[x = 0](mod p)" ``` paulson@13871 ` 205` ``` by (auto simp add: D_def C_ncong_p) ``` paulson@13871 ` 206` wenzelm@21233 ` 207` ```lemma E_ncong_p: "x \ E ==> ~[x = 0](mod p)" ``` paulson@13871 ` 208` ``` by (auto simp add: E_def C_ncong_p) ``` paulson@13871 ` 209` wenzelm@21233 ` 210` ```lemma F_ncong_p: "x \ F ==> ~[x = 0](mod p)" ``` wenzelm@18369 ` 211` ``` apply (auto simp add: F_def) ``` wenzelm@18369 ` 212` ```proof - ``` wenzelm@18369 ` 213` ``` fix x assume a: "x \ E" assume b: "[p - x = 0] (mod p)" ``` wenzelm@18369 ` 214` ``` from E_ncong_p have "~[x = 0] (mod p)" ``` wenzelm@18369 ` 215` ``` by (simp add: a) ``` wenzelm@18369 ` 216` ``` moreover from a have "0 < x" ``` wenzelm@18369 ` 217` ``` by (simp add: a E_def C_greater_zero) ``` wenzelm@18369 ` 218` ``` moreover from a have "x < p" ``` wenzelm@18369 ` 219` ``` by (auto simp add: E_def C_def p_g_0 StandardRes_ubound) ``` wenzelm@18369 ` 220` ``` ultimately have "~[p - x = 0] (mod p)" ``` wenzelm@18369 ` 221` ``` by (simp add: zcong_not_zero) ``` wenzelm@18369 ` 222` ``` from this show False by (simp add: b) ``` wenzelm@18369 ` 223` ```qed ``` paulson@13871 ` 224` wenzelm@21233 ` 225` ```lemma F_subset: "F \ {x. 0 < x & x \ ((p - 1) div 2)}" ``` wenzelm@18369 ` 226` ``` apply (auto simp add: F_def E_def) ``` paulson@13871 ` 227` ``` apply (insert p_g_0) ``` paulson@13871 ` 228` ``` apply (frule_tac x = xa in StandardRes_ubound) ``` paulson@13871 ` 229` ``` apply (frule_tac x = x in StandardRes_ubound) ``` paulson@13871 ` 230` ``` apply (subgoal_tac "xa = StandardRes p xa") ``` paulson@13871 ` 231` ``` apply (auto simp add: C_def StandardRes_prop2 StandardRes_prop1) ``` wenzelm@18369 ` 232` ```proof - ``` wenzelm@18369 ` 233` ``` from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have ``` wenzelm@18369 ` 234` ``` "2 * (p - 1) div 2 = 2 * ((p - 1) div 2)" ``` wenzelm@18369 ` 235` ``` by simp ``` wenzelm@18369 ` 236` ``` with p_eq2 show " !!x. [| (p - 1) div 2 < StandardRes p x; x \ B |] ``` wenzelm@18369 ` 237` ``` ==> p - StandardRes p x \ (p - 1) div 2" ``` wenzelm@18369 ` 238` ``` by simp ``` wenzelm@18369 ` 239` ```qed ``` paulson@13871 ` 240` wenzelm@21233 ` 241` ```lemma D_subset: "D \ {x. 0 < x & x \ ((p - 1) div 2)}" ``` paulson@13871 ` 242` ``` by (auto simp add: D_def C_greater_zero) ``` paulson@13871 ` 243` wenzelm@21233 ` 244` ```lemma F_eq: "F = {x. \y \ A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}" ``` paulson@13871 ` 245` ``` by (auto simp add: F_def E_def D_def C_def B_def A_def) ``` paulson@13871 ` 246` wenzelm@21233 ` 247` ```lemma D_eq: "D = {x. \y \ A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \ (p - 1) div 2)}" ``` paulson@13871 ` 248` ``` by (auto simp add: D_def C_def B_def A_def) ``` paulson@13871 ` 249` wenzelm@21233 ` 250` ```lemma D_leq: "x \ D ==> x \ (p - 1) div 2" ``` paulson@13871 ` 251` ``` by (auto simp add: D_eq) ``` paulson@13871 ` 252` wenzelm@21233 ` 253` ```lemma F_ge: "x \ F ==> x \ (p - 1) div 2" ``` paulson@13871 ` 254` ``` apply (auto simp add: F_eq A_def) ``` wenzelm@18369 ` 255` ```proof - ``` wenzelm@18369 ` 256` ``` fix y ``` wenzelm@18369 ` 257` ``` assume "(p - 1) div 2 < StandardRes p (y * a)" ``` wenzelm@18369 ` 258` ``` then have "p - StandardRes p (y * a) < p - ((p - 1) div 2)" ``` wenzelm@18369 ` 259` ``` by arith ``` wenzelm@18369 ` 260` ``` also from p_eq2 have "... = 2 * ((p - 1) div 2) + 1 - ((p - 1) div 2)" ``` wenzelm@18369 ` 261` ``` by auto ``` wenzelm@18369 ` 262` ``` also have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1" ``` wenzelm@18369 ` 263` ``` by arith ``` wenzelm@18369 ` 264` ``` finally show "p - StandardRes p (y * a) \ (p - 1) div 2" ``` wenzelm@18369 ` 265` ``` using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto ``` wenzelm@18369 ` 266` ```qed ``` paulson@13871 ` 267` haftmann@27556 ` 268` ```lemma all_A_relprime: "\x \ A. zgcd x p = 1" ``` wenzelm@18369 ` 269` ``` using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime) ``` paulson@13871 ` 270` haftmann@27556 ` 271` ```lemma A_prod_relprime: "zgcd (setprod id A) p = 1" ``` nipkow@30837 ` 272` ```by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime]) ``` paulson@13871 ` 273` wenzelm@21233 ` 274` wenzelm@61382 ` 275` ```subsection \Relationships Between Gauss Sets\ ``` paulson@13871 ` 276` wenzelm@21233 ` 277` ```lemma B_card_eq_A: "card B = card A" ``` wenzelm@18369 ` 278` ``` using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image) ``` paulson@13871 ` 279` wenzelm@21233 ` 280` ```lemma B_card_eq: "card B = nat ((p - 1) div 2)" ``` wenzelm@18369 ` 281` ``` by (simp add: B_card_eq_A A_card_eq) ``` paulson@13871 ` 282` wenzelm@21233 ` 283` ```lemma F_card_eq_E: "card F = card E" ``` wenzelm@18369 ` 284` ``` using finite_E by (simp add: F_def inj_on_pminusx_E card_image) ``` paulson@13871 ` 285` wenzelm@21233 ` 286` ```lemma C_card_eq_B: "card C = card B" ``` paulson@13871 ` 287` ``` apply (insert finite_B) ``` wenzelm@18369 ` 288` ``` apply (subgoal_tac "inj_on (StandardRes p) B") ``` paulson@13871 ` 289` ``` apply (simp add: B_def C_def card_image) ``` paulson@13871 ` 290` ``` apply (rule StandardRes_inj_on_ResSet) ``` wenzelm@18369 ` 291` ``` apply (simp add: B_res) ``` wenzelm@18369 ` 292` ``` done ``` paulson@13871 ` 293` wenzelm@21233 ` 294` ```lemma D_E_disj: "D \ E = {}" ``` paulson@13871 ` 295` ``` by (auto simp add: D_def E_def) ``` paulson@13871 ` 296` wenzelm@21233 ` 297` ```lemma C_card_eq_D_plus_E: "card C = card D + card E" ``` paulson@13871 ` 298` ``` by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E) ``` paulson@13871 ` 299` wenzelm@21233 ` 300` ```lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C" ``` paulson@13871 ` 301` ``` apply (insert D_E_disj finite_D finite_E C_eq) ``` haftmann@57418 ` 302` ``` apply (frule setprod.union_disjoint [of D E id]) ``` wenzelm@18369 ` 303` ``` apply auto ``` wenzelm@18369 ` 304` ``` done ``` paulson@13871 ` 305` wenzelm@21233 ` 306` ```lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)" ``` paulson@13871 ` 307` ``` apply (auto simp add: C_def) ``` wenzelm@18369 ` 308` ``` apply (insert finite_B SR_B_inj) ``` haftmann@57418 ` 309` ``` apply (frule setprod.reindex [of "StandardRes p" B id]) ``` haftmann@57418 ` 310` ``` apply auto ``` nipkow@15392 ` 311` ``` apply (rule setprod_same_function_zcong) ``` wenzelm@18369 ` 312` ``` apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0) ``` wenzelm@18369 ` 313` ``` done ``` paulson@13871 ` 314` wenzelm@21233 ` 315` ```lemma F_Un_D_subset: "(F \ D) \ A" ``` paulson@13871 ` 316` ``` apply (rule Un_least) ``` wenzelm@18369 ` 317` ``` apply (auto simp add: A_def F_subset D_subset) ``` wenzelm@18369 ` 318` ``` done ``` paulson@13871 ` 319` wenzelm@21233 ` 320` ```lemma F_D_disj: "(F \ D) = {}" ``` paulson@13871 ` 321` ``` apply (simp add: F_eq D_eq) ``` paulson@13871 ` 322` ``` apply (auto simp add: F_eq D_eq) ``` wenzelm@18369 ` 323` ```proof - ``` wenzelm@18369 ` 324` ``` fix y fix ya ``` wenzelm@18369 ` 325` ``` assume "p - StandardRes p (y * a) = StandardRes p (ya * a)" ``` wenzelm@18369 ` 326` ``` then have "p = StandardRes p (y * a) + StandardRes p (ya * a)" ``` wenzelm@18369 ` 327` ``` by arith ``` wenzelm@18369 ` 328` ``` moreover have "p dvd p" ``` wenzelm@18369 ` 329` ``` by auto ``` wenzelm@18369 ` 330` ``` ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))" ``` wenzelm@18369 ` 331` ``` by auto ``` wenzelm@18369 ` 332` ``` then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)" ``` wenzelm@18369 ` 333` ``` by (auto simp add: zcong_def) ``` wenzelm@18369 ` 334` ``` have "[y * a = StandardRes p (y * a)] (mod p)" ``` wenzelm@18369 ` 335` ``` by (simp only: zcong_sym StandardRes_prop1) ``` wenzelm@18369 ` 336` ``` moreover have "[ya * a = StandardRes p (ya * a)] (mod p)" ``` wenzelm@18369 ` 337` ``` by (simp only: zcong_sym StandardRes_prop1) ``` wenzelm@18369 ` 338` ``` ultimately have "[y * a + ya * a = ``` wenzelm@18369 ` 339` ``` StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)" ``` wenzelm@18369 ` 340` ``` by (rule zcong_zadd) ``` wenzelm@18369 ` 341` ``` with a have "[y * a + ya * a = 0] (mod p)" ``` wenzelm@18369 ` 342` ``` apply (elim zcong_trans) ``` wenzelm@18369 ` 343` ``` by (simp only: zcong_refl) ``` wenzelm@18369 ` 344` ``` also have "y * a + ya * a = a * (y + ya)" ``` haftmann@57512 ` 345` ``` by (simp add: distrib_left mult.commute) ``` wenzelm@18369 ` 346` ``` finally have "[a * (y + ya) = 0] (mod p)" . ``` wenzelm@18369 ` 347` ``` with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"] ``` wenzelm@18369 ` 348` ``` p_a_relprime ``` wenzelm@18369 ` 349` ``` have a: "[y + ya = 0] (mod p)" ``` wenzelm@18369 ` 350` ``` by auto ``` wenzelm@18369 ` 351` ``` assume b: "y \ A" and c: "ya: A" ``` wenzelm@18369 ` 352` ``` with A_def have "0 < y + ya" ``` wenzelm@18369 ` 353` ``` by auto ``` wenzelm@18369 ` 354` ``` moreover from b c A_def have "y + ya \ (p - 1) div 2 + (p - 1) div 2" ``` wenzelm@18369 ` 355` ``` by auto ``` wenzelm@18369 ` 356` ``` moreover from b c p_eq2 A_def have "y + ya < p" ``` wenzelm@18369 ` 357` ``` by auto ``` wenzelm@18369 ` 358` ``` ultimately show False ``` wenzelm@18369 ` 359` ``` apply simp ``` wenzelm@18369 ` 360` ``` apply (frule_tac m = p in zcong_not_zero) ``` wenzelm@18369 ` 361` ``` apply (auto simp add: a) ``` wenzelm@18369 ` 362` ``` done ``` wenzelm@18369 ` 363` ```qed ``` paulson@13871 ` 364` wenzelm@21233 ` 365` ```lemma F_Un_D_card: "card (F \ D) = nat ((p - 1) div 2)" ``` wenzelm@18369 ` 366` ```proof - ``` wenzelm@18369 ` 367` ``` have "card (F \ D) = card E + card D" ``` wenzelm@18369 ` 368` ``` by (auto simp add: finite_F finite_D F_D_disj ``` wenzelm@18369 ` 369` ``` card_Un_disjoint F_card_eq_E) ``` wenzelm@18369 ` 370` ``` then have "card (F \ D) = card C" ``` wenzelm@18369 ` 371` ``` by (simp add: C_card_eq_D_plus_E) ``` wenzelm@18369 ` 372` ``` from this show "card (F \ D) = nat ((p - 1) div 2)" ``` wenzelm@18369 ` 373` ``` by (simp add: C_card_eq_B B_card_eq) ``` wenzelm@18369 ` 374` ```qed ``` paulson@13871 ` 375` wenzelm@21233 ` 376` ```lemma F_Un_D_eq_A: "F \ D = A" ``` wenzelm@18369 ` 377` ``` using finite_A F_Un_D_subset A_card_eq F_Un_D_card by (auto simp add: card_seteq) ``` paulson@13871 ` 378` wenzelm@21233 ` 379` ```lemma prod_D_F_eq_prod_A: ``` wenzelm@18369 ` 380` ``` "(setprod id D) * (setprod id F) = setprod id A" ``` paulson@13871 ` 381` ``` apply (insert F_D_disj finite_D finite_F) ``` haftmann@57418 ` 382` ``` apply (frule setprod.union_disjoint [of F D id]) ``` wenzelm@18369 ` 383` ``` apply (auto simp add: F_Un_D_eq_A) ``` wenzelm@18369 ` 384` ``` done ``` paulson@13871 ` 385` wenzelm@21233 ` 386` ```lemma prod_F_zcong: ``` wenzelm@18369 ` 387` ``` "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)" ``` wenzelm@18369 ` 388` ```proof - ``` wenzelm@18369 ` 389` ``` have "setprod id F = setprod id (op - p ` E)" ``` wenzelm@18369 ` 390` ``` by (auto simp add: F_def) ``` wenzelm@18369 ` 391` ``` then have "setprod id F = setprod (op - p) E" ``` wenzelm@18369 ` 392` ``` apply simp ``` wenzelm@18369 ` 393` ``` apply (insert finite_E inj_on_pminusx_E) ``` haftmann@57418 ` 394` ``` apply (frule setprod.reindex [of "minus p" E id]) ``` haftmann@57418 ` 395` ``` apply auto ``` wenzelm@18369 ` 396` ``` done ``` wenzelm@18369 ` 397` ``` then have one: ``` wenzelm@18369 ` 398` ``` "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)" ``` wenzelm@18369 ` 399` ``` apply simp ``` nipkow@30837 ` 400` ``` apply (insert p_g_0 finite_E StandardRes_prod) ``` nipkow@30837 ` 401` ``` by (auto) ``` wenzelm@18369 ` 402` ``` moreover have a: "\x \ E. [p - x = 0 - x] (mod p)" ``` wenzelm@18369 ` 403` ``` apply clarify ``` wenzelm@18369 ` 404` ``` apply (insert zcong_id [of p]) ``` wenzelm@18369 ` 405` ``` apply (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto) ``` wenzelm@18369 ` 406` ``` done ``` wenzelm@18369 ` 407` ``` moreover have b: "\x \ E. [StandardRes p (p - x) = p - x](mod p)" ``` wenzelm@18369 ` 408` ``` apply clarify ``` wenzelm@18369 ` 409` ``` apply (simp add: StandardRes_prop1 zcong_sym) ``` wenzelm@18369 ` 410` ``` done ``` wenzelm@18369 ` 411` ``` moreover have "\x \ E. [StandardRes p (p - x) = - x](mod p)" ``` wenzelm@18369 ` 412` ``` apply clarify ``` wenzelm@18369 ` 413` ``` apply (insert a b) ``` wenzelm@18369 ` 414` ``` apply (rule_tac b = "p - x" in zcong_trans, auto) ``` wenzelm@18369 ` 415` ``` done ``` wenzelm@18369 ` 416` ``` ultimately have c: ``` wenzelm@18369 ` 417` ``` "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)" ``` wenzelm@18369 ` 418` ``` apply simp ``` nipkow@30837 ` 419` ``` using finite_E p_g_0 ``` nipkow@30837 ` 420` ``` setprod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p] ``` nipkow@30837 ` 421` ``` by auto ``` wenzelm@18369 ` 422` ``` then have two: "[setprod id F = setprod (uminus) E](mod p)" ``` wenzelm@18369 ` 423` ``` apply (insert one c) ``` wenzelm@18369 ` 424` ``` apply (rule zcong_trans [of "setprod id F" ``` nipkow@15392 ` 425` ``` "setprod (StandardRes p o op - p) E" p ``` wenzelm@18369 ` 426` ``` "setprod uminus E"], auto) ``` wenzelm@18369 ` 427` ``` done ``` wenzelm@18369 ` 428` ``` also have "setprod uminus E = (setprod id E) * (-1)^(card E)" ``` berghofe@22274 ` 429` ``` using finite_E by (induct set: finite) auto ``` wenzelm@18369 ` 430` ``` then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)" ``` haftmann@57512 ` 431` ``` by (simp add: mult.commute) ``` wenzelm@18369 ` 432` ``` with two show ?thesis ``` wenzelm@18369 ` 433` ``` by simp ``` nipkow@15392 ` 434` ```qed ``` paulson@13871 ` 435` wenzelm@21233 ` 436` wenzelm@61382 ` 437` ```subsection \Gauss' Lemma\ ``` paulson@13871 ` 438` haftmann@58410 ` 439` ```lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A" ``` paulson@13871 ` 440` ``` by (auto simp add: finite_E neg_one_special) ``` paulson@13871 ` 441` wenzelm@21233 ` 442` ```theorem pre_gauss_lemma: ``` wenzelm@18369 ` 443` ``` "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)" ``` wenzelm@18369 ` 444` ```proof - ``` wenzelm@18369 ` 445` ``` have "[setprod id A = setprod id F * setprod id D](mod p)" ``` wenzelm@63566 ` 446` ``` by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: setprod.strong_cong) ``` wenzelm@18369 ` 447` ``` then have "[setprod id A = ((-1)^(card E) * setprod id E) * ``` wenzelm@18369 ` 448` ``` setprod id D] (mod p)" ``` wenzelm@63566 ` 449` ``` by (rule zcong_trans) (auto simp add: prod_F_zcong zcong_scalar cong del: setprod.strong_cong) ``` wenzelm@18369 ` 450` ``` then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)" ``` wenzelm@18369 ` 451` ``` apply (rule zcong_trans) ``` wenzelm@18369 ` 452` ``` apply (insert C_prod_eq_D_times_E, erule subst) ``` wenzelm@63566 ` 453` ``` apply (subst mult.assoc) ``` wenzelm@63566 ` 454` ``` apply auto ``` wenzelm@18369 ` 455` ``` done ``` wenzelm@18369 ` 456` ``` then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)" ``` wenzelm@18369 ` 457` ``` apply (rule zcong_trans) ``` wenzelm@63566 ` 458` ``` apply (simp add: C_B_zcong_prod zcong_scalar2 cong del: setprod.strong_cong) ``` wenzelm@18369 ` 459` ``` done ``` wenzelm@18369 ` 460` ``` then have "[setprod id A = ((-1)^(card E) * ``` wenzelm@18369 ` 461` ``` (setprod id ((%x. x * a) ` A)))] (mod p)" ``` wenzelm@18369 ` 462` ``` by (simp add: B_def) ``` wenzelm@18369 ` 463` ``` then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))] ``` wenzelm@18369 ` 464` ``` (mod p)" ``` wenzelm@63566 ` 465` ``` by (simp add:finite_A inj_on_xa_A setprod.reindex cong del: setprod.strong_cong) ``` wenzelm@18369 ` 466` ``` moreover have "setprod (%x. x * a) A = ``` wenzelm@18369 ` 467` ``` setprod (%x. a) A * setprod id A" ``` berghofe@22274 ` 468` ``` using finite_A by (induct set: finite) auto ``` wenzelm@18369 ` 469` ``` ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A * ``` wenzelm@18369 ` 470` ``` setprod id A))] (mod p)" ``` wenzelm@18369 ` 471` ``` by simp ``` wenzelm@18369 ` 472` ``` then have "[setprod id A = ((-1)^(card E) * a^(card A) * ``` wenzelm@18369 ` 473` ``` setprod id A)](mod p)" ``` wenzelm@63566 ` 474` ``` by (rule zcong_trans) (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant mult.assoc) ``` wenzelm@18369 ` 475` ``` then have a: "[setprod id A * (-1)^(card E) = ``` wenzelm@18369 ` 476` ``` ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)" ``` wenzelm@18369 ` 477` ``` by (rule zcong_scalar) ``` wenzelm@18369 ` 478` ``` then have "[setprod id A * (-1)^(card E) = setprod id A * ``` wenzelm@18369 ` 479` ``` (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)" ``` wenzelm@63566 ` 480` ``` by (rule zcong_trans) (simp add: a mult.commute mult.left_commute) ``` wenzelm@18369 ` 481` ``` then have "[setprod id A * (-1)^(card E) = setprod id A * ``` wenzelm@18369 ` 482` ``` a^(card A)](mod p)" ``` wenzelm@63566 ` 483` ``` by (rule zcong_trans) (simp add: aux cong del: setprod.strong_cong) ``` haftmann@58410 ` 484` ``` with this zcong_cancel2 [of p "setprod id A" "(- 1) ^ card E" "a ^ card A"] ``` haftmann@58410 ` 485` ``` p_g_0 A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)" ``` wenzelm@18369 ` 486` ``` by (simp add: order_less_imp_le) ``` wenzelm@18369 ` 487` ``` from this show ?thesis ``` wenzelm@18369 ` 488` ``` by (simp add: A_card_eq zcong_sym) ``` nipkow@15392 ` 489` ```qed ``` paulson@13871 ` 490` wenzelm@21233 ` 491` ```theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)" ``` nipkow@15392 ` 492` ```proof - ``` paulson@13871 ` 493` ``` from Euler_Criterion p_prime p_g_2 have ``` wenzelm@18369 ` 494` ``` "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)" ``` paulson@13871 ` 495` ``` by auto ``` nipkow@15392 ` 496` ``` moreover note pre_gauss_lemma ``` nipkow@15392 ` 497` ``` ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)" ``` paulson@13871 ` 498` ``` by (rule zcong_trans) ``` nipkow@15392 ` 499` ``` moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)" ``` paulson@13871 ` 500` ``` by (auto simp add: Legendre_def) ``` nipkow@15392 ` 501` ``` moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1" ``` paulson@13871 ` 502` ``` by (rule neg_one_power) ``` nipkow@15392 ` 503` ``` ultimately show ?thesis ``` paulson@13871 ` 504` ``` by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym) ``` nipkow@15392 ` 505` ```qed ``` paulson@13871 ` 506` avigad@16775 ` 507` ```end ``` wenzelm@21233 ` 508` wenzelm@21233 ` 509` ```end ```