haftmann@32479 ` 1` ```(* Authors: Jeremy Avigad, David Gray, and Adam Kramer ``` paulson@13871 ` 2` ```*) ``` paulson@13871 ` 3` paulson@13871 ` 4` ```header {* The law of Quadratic reciprocity *} ``` paulson@13871 ` 5` nipkow@15392 ` 6` ```theory Quadratic_Reciprocity ``` nipkow@15392 ` 7` ```imports Gauss ``` nipkow@15392 ` 8` ```begin ``` paulson@13871 ` 9` wenzelm@19670 ` 10` ```text {* ``` wenzelm@19670 ` 11` ``` Lemmas leading up to the proof of theorem 3.3 in Niven and ``` wenzelm@19670 ` 12` ``` Zuckerman's presentation. ``` wenzelm@19670 ` 13` ```*} ``` paulson@13871 ` 14` wenzelm@21233 ` 15` ```context GAUSS ``` wenzelm@21233 ` 16` ```begin ``` wenzelm@21233 ` 17` wenzelm@21233 ` 18` ```lemma QRLemma1: "a * setsum id A = ``` nipkow@15392 ` 19` ``` p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E" ``` nipkow@15392 ` 20` ```proof - ``` wenzelm@18369 ` 21` ``` from finite_A have "a * setsum id A = setsum (%x. a * x) A" ``` paulson@13871 ` 22` ``` by (auto simp add: setsum_const_mult id_def) ``` wenzelm@18369 ` 23` ``` also have "setsum (%x. a * x) = setsum (%x. x * a)" ``` paulson@13871 ` 24` ``` by (auto simp add: zmult_commute) ``` nipkow@15392 ` 25` ``` also have "setsum (%x. x * a) A = setsum id B" ``` nipkow@16733 ` 26` ``` by (simp add: B_def setsum_reindex_id[OF inj_on_xa_A]) ``` nipkow@15392 ` 27` ``` also have "... = setsum (%x. p * (x div p) + StandardRes p x) B" ``` nipkow@16733 ` 28` ``` by (auto simp add: StandardRes_def zmod_zdiv_equality) ``` nipkow@15392 ` 29` ``` also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B" ``` paulson@13871 ` 30` ``` by (rule setsum_addf) ``` nipkow@15392 ` 31` ``` also have "setsum (StandardRes p) B = setsum id C" ``` nipkow@16733 ` 32` ``` by (auto simp add: C_def setsum_reindex_id[OF SR_B_inj]) ``` nipkow@15392 ` 33` ``` also from C_eq have "... = setsum id (D \ E)" ``` paulson@13871 ` 34` ``` by auto ``` nipkow@15392 ` 35` ``` also from finite_D finite_E have "... = setsum id D + setsum id E" ``` wenzelm@18369 ` 36` ``` by (rule setsum_Un_disjoint) (auto simp add: D_def E_def) ``` wenzelm@18369 ` 37` ``` also have "setsum (%x. p * (x div p)) B = ``` nipkow@15392 ` 38` ``` setsum ((%x. p * (x div p)) o (%x. (x * a))) A" ``` nipkow@16733 ` 39` ``` by (auto simp add: B_def setsum_reindex inj_on_xa_A) ``` nipkow@15392 ` 40` ``` also have "... = setsum (%x. p * ((x * a) div p)) A" ``` paulson@13871 ` 41` ``` by (auto simp add: o_def) ``` wenzelm@18369 ` 42` ``` also from finite_A have "setsum (%x. p * ((x * a) div p)) A = ``` nipkow@15392 ` 43` ``` p * setsum (%x. ((x * a) div p)) A" ``` paulson@13871 ` 44` ``` by (auto simp add: setsum_const_mult) ``` paulson@13871 ` 45` ``` finally show ?thesis by arith ``` nipkow@15392 ` 46` ```qed ``` paulson@13871 ` 47` wenzelm@21233 ` 48` ```lemma QRLemma2: "setsum id A = p * int (card E) - setsum id E + ``` wenzelm@18369 ` 49` ``` setsum id D" ``` nipkow@15392 ` 50` ```proof - ``` nipkow@15392 ` 51` ``` from F_Un_D_eq_A have "setsum id A = setsum id (D \ F)" ``` paulson@13871 ` 52` ``` by (simp add: Un_commute) ``` wenzelm@18369 ` 53` ``` also from F_D_disj finite_D finite_F ``` wenzelm@18369 ` 54` ``` have "... = setsum id D + setsum id F" ``` wenzelm@18369 ` 55` ``` by (auto simp add: Int_commute intro: setsum_Un_disjoint) ``` nipkow@15392 ` 56` ``` also from F_def have "F = (%x. (p - x)) ` E" ``` paulson@13871 ` 57` ``` by auto ``` paulson@13871 ` 58` ``` also from finite_E inj_on_pminusx_E have "setsum id ((%x. (p - x)) ` E) = ``` nipkow@15392 ` 59` ``` setsum (%x. (p - x)) E" ``` nipkow@15392 ` 60` ``` by (auto simp add: setsum_reindex) ``` nipkow@15392 ` 61` ``` also from finite_E have "setsum (op - p) E = setsum (%x. p) E - setsum id E" ``` nipkow@15392 ` 62` ``` by (auto simp add: setsum_subtractf id_def) ``` nipkow@15392 ` 63` ``` also from finite_E have "setsum (%x. p) E = p * int(card E)" ``` paulson@13871 ` 64` ``` by (intro setsum_const) ``` nipkow@15392 ` 65` ``` finally show ?thesis ``` paulson@13871 ` 66` ``` by arith ``` nipkow@15392 ` 67` ```qed ``` paulson@13871 ` 68` wenzelm@21233 ` 69` ```lemma QRLemma3: "(a - 1) * setsum id A = ``` nipkow@15392 ` 70` ``` p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E" ``` nipkow@15392 ` 71` ```proof - ``` nipkow@15392 ` 72` ``` have "(a - 1) * setsum id A = a * setsum id A - setsum id A" ``` wenzelm@18369 ` 73` ``` by (auto simp add: zdiff_zmult_distrib) ``` nipkow@15392 ` 74` ``` also note QRLemma1 ``` wenzelm@18369 ` 75` ``` also from QRLemma2 have "p * (\x \ A. x * a div p) + setsum id D + ``` wenzelm@18369 ` 76` ``` setsum id E - setsum id A = ``` wenzelm@18369 ` 77` ``` p * (\x \ A. x * a div p) + setsum id D + ``` nipkow@15392 ` 78` ``` setsum id E - (p * int (card E) - setsum id E + setsum id D)" ``` paulson@13871 ` 79` ``` by auto ``` wenzelm@18369 ` 80` ``` also have "... = p * (\x \ A. x * a div p) - ``` wenzelm@18369 ` 81` ``` p * int (card E) + 2 * setsum id E" ``` paulson@13871 ` 82` ``` by arith ``` nipkow@15392 ` 83` ``` finally show ?thesis ``` paulson@13871 ` 84` ``` by (auto simp only: zdiff_zmult_distrib2) ``` nipkow@15392 ` 85` ```qed ``` paulson@13871 ` 86` wenzelm@21233 ` 87` ```lemma QRLemma4: "a \ zOdd ==> ``` nipkow@15392 ` 88` ``` (setsum (%x. ((x * a) div p)) A \ zEven) = (int(card E): zEven)" ``` nipkow@15392 ` 89` ```proof - ``` nipkow@15392 ` 90` ``` assume a_odd: "a \ zOdd" ``` paulson@13871 ` 91` ``` from QRLemma3 have a: "p * (setsum (%x. ((x * a) div p)) A - int(card E)) = ``` wenzelm@18369 ` 92` ``` (a - 1) * setsum id A - 2 * setsum id E" ``` paulson@13871 ` 93` ``` by arith ``` paulson@13871 ` 94` ``` from a_odd have "a - 1 \ zEven" ``` paulson@13871 ` 95` ``` by (rule odd_minus_one_even) ``` nipkow@15392 ` 96` ``` hence "(a - 1) * setsum id A \ zEven" ``` paulson@13871 ` 97` ``` by (rule even_times_either) ``` nipkow@15392 ` 98` ``` moreover have "2 * setsum id E \ zEven" ``` paulson@13871 ` 99` ``` by (auto simp add: zEven_def) ``` paulson@13871 ` 100` ``` ultimately have "(a - 1) * setsum id A - 2 * setsum id E \ zEven" ``` paulson@13871 ` 101` ``` by (rule even_minus_even) ``` nipkow@15392 ` 102` ``` with a have "p * (setsum (%x. ((x * a) div p)) A - int(card E)): zEven" ``` paulson@13871 ` 103` ``` by simp ``` nipkow@15392 ` 104` ``` hence "p \ zEven | (setsum (%x. ((x * a) div p)) A - int(card E)): zEven" ``` paulson@14434 ` 105` ``` by (rule EvenOdd.even_product) ``` nipkow@15392 ` 106` ``` with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven" ``` paulson@13871 ` 107` ``` by (auto simp add: odd_iff_not_even) ``` nipkow@15392 ` 108` ``` thus ?thesis ``` wenzelm@18369 ` 109` ``` by (auto simp only: even_diff [symmetric]) ``` nipkow@15392 ` 110` ```qed ``` paulson@13871 ` 111` wenzelm@21233 ` 112` ```lemma QRLemma5: "a \ zOdd ==> ``` nipkow@15392 ` 113` ``` (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))" ``` nipkow@15392 ` 114` ```proof - ``` nipkow@15392 ` 115` ``` assume "a \ zOdd" ``` wenzelm@23373 ` 116` ``` from QRLemma4 [OF this] have ``` wenzelm@23373 ` 117` ``` "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \ zEven)" .. ``` nipkow@15392 ` 118` ``` moreover have "0 \ int(card E)" ``` paulson@13871 ` 119` ``` by auto ``` nipkow@15392 ` 120` ``` moreover have "0 \ setsum (%x. ((x * a) div p)) A" ``` nipkow@15392 ` 121` ``` proof (intro setsum_nonneg) ``` nipkow@15537 ` 122` ``` show "\x \ A. 0 \ x * a div p" ``` nipkow@15392 ` 123` ``` proof ``` nipkow@15392 ` 124` ``` fix x ``` nipkow@15392 ` 125` ``` assume "x \ A" ``` nipkow@15392 ` 126` ``` then have "0 \ x" ``` paulson@13871 ` 127` ``` by (auto simp add: A_def) ``` nipkow@15392 ` 128` ``` with a_nonzero have "0 \ x * a" ``` paulson@14353 ` 129` ``` by (auto simp add: zero_le_mult_iff) ``` wenzelm@18369 ` 130` ``` with p_g_2 show "0 \ x * a div p" ``` paulson@13871 ` 131` ``` by (auto simp add: pos_imp_zdiv_nonneg_iff) ``` nipkow@15392 ` 132` ``` qed ``` nipkow@15392 ` 133` ``` qed ``` paulson@13871 ` 134` ``` ultimately have "(-1::int)^nat((int (card E))) = ``` nipkow@15392 ` 135` ``` (-1)^nat(((\x \ A. x * a div p)))" ``` paulson@13871 ` 136` ``` by (intro neg_one_power_parity, auto) ``` nipkow@15392 ` 137` ``` also have "nat (int(card E)) = card E" ``` paulson@13871 ` 138` ``` by auto ``` nipkow@15392 ` 139` ``` finally show ?thesis . ``` nipkow@15392 ` 140` ```qed ``` paulson@13871 ` 141` wenzelm@21233 ` 142` ```end ``` wenzelm@21233 ` 143` nipkow@16663 ` 144` ```lemma MainQRLemma: "[| a \ zOdd; 0 < a; ~([a = 0] (mod p)); zprime p; 2 < p; ``` wenzelm@18369 ` 145` ``` A = {x. 0 < x & x \ (p - 1) div 2} |] ==> ``` nipkow@15392 ` 146` ``` (Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))" ``` paulson@13871 ` 147` ``` apply (subst GAUSS.gauss_lemma) ``` paulson@13871 ` 148` ``` apply (auto simp add: GAUSS_def) ``` paulson@13871 ` 149` ``` apply (subst GAUSS.QRLemma5) ``` wenzelm@18369 ` 150` ``` apply (auto simp add: GAUSS_def) ``` wenzelm@21233 ` 151` ``` apply (simp add: GAUSS.A_def [OF GAUSS.intro] GAUSS_def) ``` wenzelm@18369 ` 152` ``` done ``` paulson@13871 ` 153` wenzelm@19670 ` 154` wenzelm@19670 ` 155` ```subsection {* Stuff about S, S1 and S2 *} ``` paulson@13871 ` 156` paulson@13871 ` 157` ```locale QRTEMP = ``` paulson@13871 ` 158` ``` fixes p :: "int" ``` paulson@13871 ` 159` ``` fixes q :: "int" ``` paulson@13871 ` 160` nipkow@16663 ` 161` ``` assumes p_prime: "zprime p" ``` paulson@13871 ` 162` ``` assumes p_g_2: "2 < p" ``` nipkow@16663 ` 163` ``` assumes q_prime: "zprime q" ``` paulson@13871 ` 164` ``` assumes q_g_2: "2 < q" ``` paulson@13871 ` 165` ``` assumes p_neq_q: "p \ q" ``` wenzelm@21233 ` 166` ```begin ``` paulson@13871 ` 167` wenzelm@21233 ` 168` ```definition ``` wenzelm@21404 ` 169` ``` P_set :: "int set" where ``` wenzelm@21233 ` 170` ``` "P_set = {x. 0 < x & x \ ((p - 1) div 2) }" ``` wenzelm@21233 ` 171` wenzelm@21404 ` 172` ```definition ``` wenzelm@21404 ` 173` ``` Q_set :: "int set" where ``` wenzelm@21233 ` 174` ``` "Q_set = {x. 0 < x & x \ ((q - 1) div 2) }" ``` wenzelm@21233 ` 175` ``` ``` wenzelm@21404 ` 176` ```definition ``` wenzelm@21404 ` 177` ``` S :: "(int * int) set" where ``` wenzelm@21233 ` 178` ``` "S = P_set <*> Q_set" ``` wenzelm@21233 ` 179` wenzelm@21404 ` 180` ```definition ``` wenzelm@21404 ` 181` ``` S1 :: "(int * int) set" where ``` wenzelm@21233 ` 182` ``` "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }" ``` paulson@13871 ` 183` wenzelm@21404 ` 184` ```definition ``` wenzelm@21404 ` 185` ``` S2 :: "(int * int) set" where ``` wenzelm@21233 ` 186` ``` "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }" ``` wenzelm@21233 ` 187` wenzelm@21404 ` 188` ```definition ``` wenzelm@21404 ` 189` ``` f1 :: "int => (int * int) set" where ``` wenzelm@21233 ` 190` ``` "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \ (q * j) div p) }" ``` wenzelm@21233 ` 191` wenzelm@21404 ` 192` ```definition ``` wenzelm@21404 ` 193` ``` f2 :: "int => (int * int) set" where ``` wenzelm@21233 ` 194` ``` "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \ (p * j) div q) }" ``` wenzelm@21233 ` 195` wenzelm@21233 ` 196` ```lemma p_fact: "0 < (p - 1) div 2" ``` nipkow@15392 ` 197` ```proof - ``` wenzelm@21233 ` 198` ``` from p_g_2 have "2 \ p - 1" by arith ``` paulson@13871 ` 199` ``` then have "2 div 2 \ (p - 1) div 2" by (rule zdiv_mono1, auto) ``` paulson@13871 ` 200` ``` then show ?thesis by auto ``` nipkow@15392 ` 201` ```qed ``` paulson@13871 ` 202` wenzelm@21233 ` 203` ```lemma q_fact: "0 < (q - 1) div 2" ``` nipkow@15392 ` 204` ```proof - ``` wenzelm@21233 ` 205` ``` from q_g_2 have "2 \ q - 1" by arith ``` paulson@13871 ` 206` ``` then have "2 div 2 \ (q - 1) div 2" by (rule zdiv_mono1, auto) ``` paulson@13871 ` 207` ``` then show ?thesis by auto ``` nipkow@15392 ` 208` ```qed ``` paulson@13871 ` 209` wenzelm@21233 ` 210` ```lemma pb_neq_qa: "[|1 \ b; b \ (q - 1) div 2 |] ==> ``` nipkow@15392 ` 211` ``` (p * b \ q * a)" ``` nipkow@15392 ` 212` ```proof ``` nipkow@15392 ` 213` ``` assume "p * b = q * a" and "1 \ b" and "b \ (q - 1) div 2" ``` paulson@13871 ` 214` ``` then have "q dvd (p * b)" by (auto simp add: dvd_def) ``` nipkow@15392 ` 215` ``` with q_prime p_g_2 have "q dvd p | q dvd b" ``` paulson@13871 ` 216` ``` by (auto simp add: zprime_zdvd_zmult) ``` nipkow@15392 ` 217` ``` moreover have "~ (q dvd p)" ``` nipkow@15392 ` 218` ``` proof ``` nipkow@15392 ` 219` ``` assume "q dvd p" ``` paulson@13871 ` 220` ``` with p_prime have "q = 1 | q = p" ``` paulson@13871 ` 221` ``` apply (auto simp add: zprime_def QRTEMP_def) ``` paulson@13871 ` 222` ``` apply (drule_tac x = q and R = False in allE) ``` wenzelm@18369 ` 223` ``` apply (simp add: QRTEMP_def) ``` paulson@13871 ` 224` ``` apply (subgoal_tac "0 \ q", simp add: QRTEMP_def) ``` paulson@13871 ` 225` ``` apply (insert prems) ``` wenzelm@18369 ` 226` ``` apply (auto simp add: QRTEMP_def) ``` wenzelm@18369 ` 227` ``` done ``` paulson@13871 ` 228` ``` with q_g_2 p_neq_q show False by auto ``` nipkow@15392 ` 229` ``` qed ``` paulson@13871 ` 230` ``` ultimately have "q dvd b" by auto ``` nipkow@15392 ` 231` ``` then have "q \ b" ``` nipkow@15392 ` 232` ``` proof - ``` nipkow@15392 ` 233` ``` assume "q dvd b" ``` paulson@13871 ` 234` ``` moreover from prems have "0 < b" by auto ``` wenzelm@18369 ` 235` ``` ultimately show ?thesis using zdvd_bounds [of q b] by auto ``` nipkow@15392 ` 236` ``` qed ``` paulson@13871 ` 237` ``` with prems have "q \ (q - 1) div 2" by auto ``` paulson@13871 ` 238` ``` then have "2 * q \ 2 * ((q - 1) div 2)" by arith ``` nipkow@15392 ` 239` ``` then have "2 * q \ q - 1" ``` nipkow@15392 ` 240` ``` proof - ``` nipkow@15392 ` 241` ``` assume "2 * q \ 2 * ((q - 1) div 2)" ``` paulson@13871 ` 242` ``` with prems have "q \ zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2) ``` paulson@13871 ` 243` ``` with odd_minus_one_even have "(q - 1):zEven" by auto ``` paulson@13871 ` 244` ``` with even_div_2_prop2 have "(q - 1) = 2 * ((q - 1) div 2)" by auto ``` paulson@13871 ` 245` ``` with prems show ?thesis by auto ``` nipkow@15392 ` 246` ``` qed ``` paulson@13871 ` 247` ``` then have p1: "q \ -1" by arith ``` paulson@13871 ` 248` ``` with q_g_2 show False by auto ``` nipkow@15392 ` 249` ```qed ``` paulson@13871 ` 250` wenzelm@21233 ` 251` ```lemma P_set_finite: "finite (P_set)" ``` wenzelm@18369 ` 252` ``` using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite) ``` paulson@13871 ` 253` wenzelm@21233 ` 254` ```lemma Q_set_finite: "finite (Q_set)" ``` wenzelm@18369 ` 255` ``` using q_fact by (auto simp add: Q_set_def bdd_int_set_l_le_finite) ``` paulson@13871 ` 256` wenzelm@21233 ` 257` ```lemma S_finite: "finite S" ``` nipkow@15402 ` 258` ``` by (auto simp add: S_def P_set_finite Q_set_finite finite_cartesian_product) ``` paulson@13871 ` 259` wenzelm@21233 ` 260` ```lemma S1_finite: "finite S1" ``` nipkow@15392 ` 261` ```proof - ``` paulson@13871 ` 262` ``` have "finite S" by (auto simp add: S_finite) ``` paulson@13871 ` 263` ``` moreover have "S1 \ S" by (auto simp add: S1_def S_def) ``` paulson@13871 ` 264` ``` ultimately show ?thesis by (auto simp add: finite_subset) ``` nipkow@15392 ` 265` ```qed ``` paulson@13871 ` 266` wenzelm@21233 ` 267` ```lemma S2_finite: "finite S2" ``` nipkow@15392 ` 268` ```proof - ``` paulson@13871 ` 269` ``` have "finite S" by (auto simp add: S_finite) ``` paulson@13871 ` 270` ``` moreover have "S2 \ S" by (auto simp add: S2_def S_def) ``` paulson@13871 ` 271` ``` ultimately show ?thesis by (auto simp add: finite_subset) ``` nipkow@15392 ` 272` ```qed ``` paulson@13871 ` 273` wenzelm@21233 ` 274` ```lemma P_set_card: "(p - 1) div 2 = int (card (P_set))" ``` wenzelm@18369 ` 275` ``` using p_fact by (auto simp add: P_set_def card_bdd_int_set_l_le) ``` paulson@13871 ` 276` wenzelm@21233 ` 277` ```lemma Q_set_card: "(q - 1) div 2 = int (card (Q_set))" ``` wenzelm@18369 ` 278` ``` using q_fact by (auto simp add: Q_set_def card_bdd_int_set_l_le) ``` paulson@13871 ` 279` wenzelm@21233 ` 280` ```lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))" ``` wenzelm@18369 ` 281` ``` using P_set_card Q_set_card P_set_finite Q_set_finite ``` huffman@23431 ` 282` ``` by (auto simp add: S_def zmult_int setsum_constant) ``` paulson@13871 ` 283` wenzelm@21233 ` 284` ```lemma S1_Int_S2_prop: "S1 \ S2 = {}" ``` paulson@13871 ` 285` ``` by (auto simp add: S1_def S2_def) ``` paulson@13871 ` 286` wenzelm@21233 ` 287` ```lemma S1_Union_S2_prop: "S = S1 \ S2" ``` paulson@13871 ` 288` ``` apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def) ``` wenzelm@18369 ` 289` ```proof - ``` wenzelm@18369 ` 290` ``` fix a and b ``` wenzelm@18369 ` 291` ``` assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \ (q - 1) div 2" ``` wenzelm@18369 ` 292` ``` with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto ``` wenzelm@18369 ` 293` ``` moreover from pb_neq_qa b1 b2 have "(p * b \ q * a)" by auto ``` wenzelm@18369 ` 294` ``` ultimately show "p * b < q * a" by auto ``` wenzelm@18369 ` 295` ```qed ``` paulson@13871 ` 296` wenzelm@21233 ` 297` ```lemma card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) = ``` nipkow@15392 ` 298` ``` int(card(S1)) + int(card(S2))" ``` wenzelm@18369 ` 299` ```proof - ``` nipkow@15392 ` 300` ``` have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))" ``` paulson@13871 ` 301` ``` by (auto simp add: S_card) ``` nipkow@15392 ` 302` ``` also have "... = int( card(S1) + card(S2))" ``` paulson@13871 ` 303` ``` apply (insert S1_finite S2_finite S1_Int_S2_prop S1_Union_S2_prop) ``` paulson@13871 ` 304` ``` apply (drule card_Un_disjoint, auto) ``` wenzelm@18369 ` 305` ``` done ``` paulson@13871 ` 306` ``` also have "... = int(card(S1)) + int(card(S2))" by auto ``` nipkow@15392 ` 307` ``` finally show ?thesis . ``` nipkow@15392 ` 308` ```qed ``` paulson@13871 ` 309` wenzelm@21233 ` 310` ```lemma aux1a: "[| 0 < a; a \ (p - 1) div 2; ``` paulson@13871 ` 311` ``` 0 < b; b \ (q - 1) div 2 |] ==> ``` nipkow@15392 ` 312` ``` (p * b < q * a) = (b \ q * a div p)" ``` nipkow@15392 ` 313` ```proof - ``` nipkow@15392 ` 314` ``` assume "0 < a" and "a \ (p - 1) div 2" and "0 < b" and "b \ (q - 1) div 2" ``` nipkow@15392 ` 315` ``` have "p * b < q * a ==> b \ q * a div p" ``` nipkow@15392 ` 316` ``` proof - ``` nipkow@15392 ` 317` ``` assume "p * b < q * a" ``` paulson@13871 ` 318` ``` then have "p * b \ q * a" by auto ``` nipkow@15392 ` 319` ``` then have "(p * b) div p \ (q * a) div p" ``` wenzelm@18369 ` 320` ``` by (rule zdiv_mono1) (insert p_g_2, auto) ``` nipkow@15392 ` 321` ``` then show "b \ (q * a) div p" ``` paulson@13871 ` 322` ``` apply (subgoal_tac "p \ 0") ``` nipkow@30034 ` 323` ``` apply (frule div_mult_self1_is_id, force) ``` wenzelm@18369 ` 324` ``` apply (insert p_g_2, auto) ``` wenzelm@18369 ` 325` ``` done ``` nipkow@15392 ` 326` ``` qed ``` nipkow@15392 ` 327` ``` moreover have "b \ q * a div p ==> p * b < q * a" ``` nipkow@15392 ` 328` ``` proof - ``` nipkow@15392 ` 329` ``` assume "b \ q * a div p" ``` nipkow@15392 ` 330` ``` then have "p * b \ p * ((q * a) div p)" ``` wenzelm@18369 ` 331` ``` using p_g_2 by (auto simp add: mult_le_cancel_left) ``` nipkow@15392 ` 332` ``` also have "... \ q * a" ``` wenzelm@18369 ` 333` ``` by (rule zdiv_leq_prop) (insert p_g_2, auto) ``` nipkow@15392 ` 334` ``` finally have "p * b \ q * a" . ``` nipkow@15392 ` 335` ``` then have "p * b < q * a | p * b = q * a" ``` paulson@13871 ` 336` ``` by (simp only: order_le_imp_less_or_eq) ``` nipkow@15392 ` 337` ``` moreover have "p * b \ q * a" ``` wenzelm@18369 ` 338` ``` by (rule pb_neq_qa) (insert prems, auto) ``` paulson@13871 ` 339` ``` ultimately show ?thesis by auto ``` nipkow@15392 ` 340` ``` qed ``` nipkow@15392 ` 341` ``` ultimately show ?thesis .. ``` nipkow@15392 ` 342` ```qed ``` paulson@13871 ` 343` wenzelm@21233 ` 344` ```lemma aux1b: "[| 0 < a; a \ (p - 1) div 2; ``` paulson@13871 ` 345` ``` 0 < b; b \ (q - 1) div 2 |] ==> ``` nipkow@15392 ` 346` ``` (q * a < p * b) = (a \ p * b div q)" ``` nipkow@15392 ` 347` ```proof - ``` nipkow@15392 ` 348` ``` assume "0 < a" and "a \ (p - 1) div 2" and "0 < b" and "b \ (q - 1) div 2" ``` nipkow@15392 ` 349` ``` have "q * a < p * b ==> a \ p * b div q" ``` nipkow@15392 ` 350` ``` proof - ``` nipkow@15392 ` 351` ``` assume "q * a < p * b" ``` paulson@13871 ` 352` ``` then have "q * a \ p * b" by auto ``` nipkow@15392 ` 353` ``` then have "(q * a) div q \ (p * b) div q" ``` wenzelm@18369 ` 354` ``` by (rule zdiv_mono1) (insert q_g_2, auto) ``` nipkow@15392 ` 355` ``` then show "a \ (p * b) div q" ``` paulson@13871 ` 356` ``` apply (subgoal_tac "q \ 0") ``` nipkow@30034 ` 357` ``` apply (frule div_mult_self1_is_id, force) ``` wenzelm@18369 ` 358` ``` apply (insert q_g_2, auto) ``` wenzelm@18369 ` 359` ``` done ``` nipkow@15392 ` 360` ``` qed ``` nipkow@15392 ` 361` ``` moreover have "a \ p * b div q ==> q * a < p * b" ``` nipkow@15392 ` 362` ``` proof - ``` nipkow@15392 ` 363` ``` assume "a \ p * b div q" ``` nipkow@15392 ` 364` ``` then have "q * a \ q * ((p * b) div q)" ``` wenzelm@18369 ` 365` ``` using q_g_2 by (auto simp add: mult_le_cancel_left) ``` nipkow@15392 ` 366` ``` also have "... \ p * b" ``` wenzelm@18369 ` 367` ``` by (rule zdiv_leq_prop) (insert q_g_2, auto) ``` nipkow@15392 ` 368` ``` finally have "q * a \ p * b" . ``` nipkow@15392 ` 369` ``` then have "q * a < p * b | q * a = p * b" ``` paulson@13871 ` 370` ``` by (simp only: order_le_imp_less_or_eq) ``` nipkow@15392 ` 371` ``` moreover have "p * b \ q * a" ``` wenzelm@18369 ` 372` ``` by (rule pb_neq_qa) (insert prems, auto) ``` paulson@13871 ` 373` ``` ultimately show ?thesis by auto ``` nipkow@15392 ` 374` ``` qed ``` nipkow@15392 ` 375` ``` ultimately show ?thesis .. ``` nipkow@15392 ` 376` ```qed ``` paulson@13871 ` 377` wenzelm@21288 ` 378` ```lemma (in -) aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==> ``` nipkow@15392 ` 379` ``` (q * ((p - 1) div 2)) div p \ (q - 1) div 2" ``` nipkow@15392 ` 380` ```proof- ``` nipkow@16663 ` 381` ``` assume "zprime p" and "zprime q" and "2 < p" and "2 < q" ``` paulson@13871 ` 382` ``` (* Set up what's even and odd *) ``` nipkow@15392 ` 383` ``` then have "p \ zOdd & q \ zOdd" ``` paulson@13871 ` 384` ``` by (auto simp add: zprime_zOdd_eq_grt_2) ``` nipkow@15392 ` 385` ``` then have even1: "(p - 1):zEven & (q - 1):zEven" ``` paulson@13871 ` 386` ``` by (auto simp add: odd_minus_one_even) ``` nipkow@15392 ` 387` ``` then have even2: "(2 * p):zEven & ((q - 1) * p):zEven" ``` paulson@13871 ` 388` ``` by (auto simp add: zEven_def) ``` nipkow@15392 ` 389` ``` then have even3: "(((q - 1) * p) + (2 * p)):zEven" ``` paulson@14434 ` 390` ``` by (auto simp: EvenOdd.even_plus_even) ``` paulson@13871 ` 391` ``` (* using these prove it *) ``` nipkow@15392 ` 392` ``` from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)" ``` paulson@13871 ` 393` ``` by (auto simp add: int_distrib) ``` nipkow@15392 ` 394` ``` then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2" ``` nipkow@15392 ` 395` ``` apply (rule_tac x = "((p - 1) * q)" in even_div_2_l) ``` paulson@13871 ` 396` ``` by (auto simp add: even3, auto simp add: zmult_ac) ``` nipkow@15392 ` 397` ``` also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)" ``` paulson@13871 ` 398` ``` by (auto simp add: even1 even_prod_div_2) ``` nipkow@15392 ` 399` ``` also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p" ``` paulson@13871 ` 400` ``` by (auto simp add: even1 even2 even_prod_div_2 even_sum_div_2) ``` wenzelm@18369 ` 401` ``` finally show ?thesis ``` wenzelm@18369 ` 402` ``` apply (rule_tac x = " q * ((p - 1) div 2)" and ``` nipkow@15392 ` 403` ``` y = "(q - 1) div 2" in div_prop2) ``` wenzelm@18369 ` 404` ``` using prems by auto ``` nipkow@15392 ` 405` ```qed ``` paulson@13871 ` 406` wenzelm@21233 ` 407` ```lemma aux3a: "\j \ P_set. int (card (f1 j)) = (q * j) div p" ``` nipkow@15392 ` 408` ```proof ``` nipkow@15392 ` 409` ``` fix j ``` nipkow@15392 ` 410` ``` assume j_fact: "j \ P_set" ``` nipkow@15392 ` 411` ``` have "int (card (f1 j)) = int (card {y. y \ Q_set & y \ (q * j) div p})" ``` nipkow@15392 ` 412` ``` proof - ``` nipkow@15392 ` 413` ``` have "finite (f1 j)" ``` nipkow@15392 ` 414` ``` proof - ``` paulson@13871 ` 415` ``` have "(f1 j) \ S" by (auto simp add: f1_def) ``` paulson@13871 ` 416` ``` with S_finite show ?thesis by (auto simp add: finite_subset) ``` nipkow@15392 ` 417` ``` qed ``` nipkow@15392 ` 418` ``` moreover have "inj_on (%(x,y). y) (f1 j)" ``` paulson@13871 ` 419` ``` by (auto simp add: f1_def inj_on_def) ``` nipkow@15392 ` 420` ``` ultimately have "card ((%(x,y). y) ` (f1 j)) = card (f1 j)" ``` paulson@13871 ` 421` ``` by (auto simp add: f1_def card_image) ``` nipkow@15392 ` 422` ``` moreover have "((%(x,y). y) ` (f1 j)) = {y. y \ Q_set & y \ (q * j) div p}" ``` wenzelm@18369 ` 423` ``` using prems by (auto simp add: f1_def S_def Q_set_def P_set_def image_def) ``` paulson@13871 ` 424` ``` ultimately show ?thesis by (auto simp add: f1_def) ``` nipkow@15392 ` 425` ``` qed ``` nipkow@15392 ` 426` ``` also have "... = int (card {y. 0 < y & y \ (q * j) div p})" ``` nipkow@15392 ` 427` ``` proof - ``` wenzelm@18369 ` 428` ``` have "{y. y \ Q_set & y \ (q * j) div p} = ``` nipkow@15392 ` 429` ``` {y. 0 < y & y \ (q * j) div p}" ``` paulson@13871 ` 430` ``` apply (auto simp add: Q_set_def) ``` wenzelm@18369 ` 431` ``` proof - ``` wenzelm@18369 ` 432` ``` fix x ``` wenzelm@18369 ` 433` ``` assume "0 < x" and "x \ q * j div p" ``` wenzelm@18369 ` 434` ``` with j_fact P_set_def have "j \ (p - 1) div 2" by auto ``` wenzelm@18369 ` 435` ``` with q_g_2 have "q * j \ q * ((p - 1) div 2)" ``` wenzelm@18369 ` 436` ``` by (auto simp add: mult_le_cancel_left) ``` wenzelm@18369 ` 437` ``` with p_g_2 have "q * j div p \ q * ((p - 1) div 2) div p" ``` wenzelm@18369 ` 438` ``` by (auto simp add: zdiv_mono1) ``` wenzelm@21233 ` 439` ``` also from prems P_set_def have "... \ (q - 1) div 2" ``` wenzelm@18369 ` 440` ``` apply simp ``` wenzelm@18369 ` 441` ``` apply (insert aux2) ``` wenzelm@18369 ` 442` ``` apply (simp add: QRTEMP_def) ``` wenzelm@18369 ` 443` ``` done ``` wenzelm@18369 ` 444` ``` finally show "x \ (q - 1) div 2" using prems by auto ``` wenzelm@18369 ` 445` ``` qed ``` paulson@13871 ` 446` ``` then show ?thesis by auto ``` nipkow@15392 ` 447` ``` qed ``` nipkow@15392 ` 448` ``` also have "... = (q * j) div p" ``` nipkow@15392 ` 449` ``` proof - ``` paulson@13871 ` 450` ``` from j_fact P_set_def have "0 \ j" by auto ``` paulson@14387 ` 451` ``` with q_g_2 have "q * 0 \ q * j" by (auto simp only: mult_left_mono) ``` paulson@13871 ` 452` ``` then have "0 \ q * j" by auto ``` nipkow@15392 ` 453` ``` then have "0 div p \ (q * j) div p" ``` paulson@13871 ` 454` ``` apply (rule_tac a = 0 in zdiv_mono1) ``` wenzelm@18369 ` 455` ``` apply (insert p_g_2, auto) ``` wenzelm@18369 ` 456` ``` done ``` paulson@13871 ` 457` ``` also have "0 div p = 0" by auto ``` paulson@13871 ` 458` ``` finally show ?thesis by (auto simp add: card_bdd_int_set_l_le) ``` nipkow@15392 ` 459` ``` qed ``` nipkow@15392 ` 460` ``` finally show "int (card (f1 j)) = q * j div p" . ``` nipkow@15392 ` 461` ```qed ``` paulson@13871 ` 462` wenzelm@21233 ` 463` ```lemma aux3b: "\j \ Q_set. int (card (f2 j)) = (p * j) div q" ``` nipkow@15392 ` 464` ```proof ``` nipkow@15392 ` 465` ``` fix j ``` nipkow@15392 ` 466` ``` assume j_fact: "j \ Q_set" ``` nipkow@15392 ` 467` ``` have "int (card (f2 j)) = int (card {y. y \ P_set & y \ (p * j) div q})" ``` nipkow@15392 ` 468` ``` proof - ``` nipkow@15392 ` 469` ``` have "finite (f2 j)" ``` nipkow@15392 ` 470` ``` proof - ``` paulson@13871 ` 471` ``` have "(f2 j) \ S" by (auto simp add: f2_def) ``` paulson@13871 ` 472` ``` with S_finite show ?thesis by (auto simp add: finite_subset) ``` nipkow@15392 ` 473` ``` qed ``` nipkow@15392 ` 474` ``` moreover have "inj_on (%(x,y). x) (f2 j)" ``` paulson@13871 ` 475` ``` by (auto simp add: f2_def inj_on_def) ``` nipkow@15392 ` 476` ``` ultimately have "card ((%(x,y). x) ` (f2 j)) = card (f2 j)" ``` paulson@13871 ` 477` ``` by (auto simp add: f2_def card_image) ``` nipkow@15392 ` 478` ``` moreover have "((%(x,y). x) ` (f2 j)) = {y. y \ P_set & y \ (p * j) div q}" ``` wenzelm@18369 ` 479` ``` using prems by (auto simp add: f2_def S_def Q_set_def P_set_def image_def) ``` paulson@13871 ` 480` ``` ultimately show ?thesis by (auto simp add: f2_def) ``` nipkow@15392 ` 481` ``` qed ``` nipkow@15392 ` 482` ``` also have "... = int (card {y. 0 < y & y \ (p * j) div q})" ``` nipkow@15392 ` 483` ``` proof - ``` wenzelm@18369 ` 484` ``` have "{y. y \ P_set & y \ (p * j) div q} = ``` nipkow@15392 ` 485` ``` {y. 0 < y & y \ (p * j) div q}" ``` paulson@13871 ` 486` ``` apply (auto simp add: P_set_def) ``` wenzelm@18369 ` 487` ``` proof - ``` wenzelm@18369 ` 488` ``` fix x ``` wenzelm@18369 ` 489` ``` assume "0 < x" and "x \ p * j div q" ``` wenzelm@18369 ` 490` ``` with j_fact Q_set_def have "j \ (q - 1) div 2" by auto ``` wenzelm@18369 ` 491` ``` with p_g_2 have "p * j \ p * ((q - 1) div 2)" ``` wenzelm@18369 ` 492` ``` by (auto simp add: mult_le_cancel_left) ``` wenzelm@18369 ` 493` ``` with q_g_2 have "p * j div q \ p * ((q - 1) div 2) div q" ``` wenzelm@18369 ` 494` ``` by (auto simp add: zdiv_mono1) ``` wenzelm@18369 ` 495` ``` also from prems have "... \ (p - 1) div 2" ``` wenzelm@18369 ` 496` ``` by (auto simp add: aux2 QRTEMP_def) ``` wenzelm@18369 ` 497` ``` finally show "x \ (p - 1) div 2" using prems by auto ``` nipkow@15392 ` 498` ``` qed ``` paulson@13871 ` 499` ``` then show ?thesis by auto ``` nipkow@15392 ` 500` ``` qed ``` nipkow@15392 ` 501` ``` also have "... = (p * j) div q" ``` nipkow@15392 ` 502` ``` proof - ``` paulson@13871 ` 503` ``` from j_fact Q_set_def have "0 \ j" by auto ``` paulson@14387 ` 504` ``` with p_g_2 have "p * 0 \ p * j" by (auto simp only: mult_left_mono) ``` paulson@13871 ` 505` ``` then have "0 \ p * j" by auto ``` nipkow@15392 ` 506` ``` then have "0 div q \ (p * j) div q" ``` paulson@13871 ` 507` ``` apply (rule_tac a = 0 in zdiv_mono1) ``` wenzelm@18369 ` 508` ``` apply (insert q_g_2, auto) ``` wenzelm@18369 ` 509` ``` done ``` paulson@13871 ` 510` ``` also have "0 div q = 0" by auto ``` paulson@13871 ` 511` ``` finally show ?thesis by (auto simp add: card_bdd_int_set_l_le) ``` nipkow@15392 ` 512` ``` qed ``` nipkow@15392 ` 513` ``` finally show "int (card (f2 j)) = p * j div q" . ``` nipkow@15392 ` 514` ```qed ``` paulson@13871 ` 515` wenzelm@21233 ` 516` ```lemma S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set" ``` nipkow@15392 ` 517` ```proof - ``` nipkow@15392 ` 518` ``` have "\x \ P_set. finite (f1 x)" ``` nipkow@15392 ` 519` ``` proof ``` nipkow@15392 ` 520` ``` fix x ``` paulson@13871 ` 521` ``` have "f1 x \ S" by (auto simp add: f1_def) ``` paulson@13871 ` 522` ``` with S_finite show "finite (f1 x)" by (auto simp add: finite_subset) ``` nipkow@15392 ` 523` ``` qed ``` nipkow@15392 ` 524` ``` moreover have "(\x \ P_set. \y \ P_set. x \ y --> (f1 x) \ (f1 y) = {})" ``` paulson@13871 ` 525` ``` by (auto simp add: f1_def) ``` nipkow@15392 ` 526` ``` moreover note P_set_finite ``` wenzelm@18369 ` 527` ``` ultimately have "int(card (UNION P_set f1)) = ``` nipkow@15392 ` 528` ``` setsum (%x. int(card (f1 x))) P_set" ``` nipkow@15402 ` 529` ``` by(simp add:card_UN_disjoint int_setsum o_def) ``` nipkow@15392 ` 530` ``` moreover have "S1 = UNION P_set f1" ``` paulson@13871 ` 531` ``` by (auto simp add: f1_def S_def S1_def S2_def P_set_def Q_set_def aux1a) ``` wenzelm@18369 ` 532` ``` ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set" ``` paulson@13871 ` 533` ``` by auto ``` nipkow@15392 ` 534` ``` also have "... = setsum (%j. q * j div p) P_set" ``` nipkow@15392 ` 535` ``` using aux3a by(fastsimp intro: setsum_cong) ``` nipkow@15392 ` 536` ``` finally show ?thesis . ``` nipkow@15392 ` 537` ```qed ``` paulson@13871 ` 538` wenzelm@21233 ` 539` ```lemma S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set" ``` nipkow@15392 ` 540` ```proof - ``` nipkow@15392 ` 541` ``` have "\x \ Q_set. finite (f2 x)" ``` nipkow@15392 ` 542` ``` proof ``` nipkow@15392 ` 543` ``` fix x ``` paulson@13871 ` 544` ``` have "f2 x \ S" by (auto simp add: f2_def) ``` paulson@13871 ` 545` ``` with S_finite show "finite (f2 x)" by (auto simp add: finite_subset) ``` nipkow@15392 ` 546` ``` qed ``` wenzelm@18369 ` 547` ``` moreover have "(\x \ Q_set. \y \ Q_set. x \ y --> ``` nipkow@15392 ` 548` ``` (f2 x) \ (f2 y) = {})" ``` paulson@13871 ` 549` ``` by (auto simp add: f2_def) ``` nipkow@15392 ` 550` ``` moreover note Q_set_finite ``` wenzelm@18369 ` 551` ``` ultimately have "int(card (UNION Q_set f2)) = ``` nipkow@15392 ` 552` ``` setsum (%x. int(card (f2 x))) Q_set" ``` nipkow@15402 ` 553` ``` by(simp add:card_UN_disjoint int_setsum o_def) ``` nipkow@15392 ` 554` ``` moreover have "S2 = UNION Q_set f2" ``` paulson@13871 ` 555` ``` by (auto simp add: f2_def S_def S1_def S2_def P_set_def Q_set_def aux1b) ``` wenzelm@18369 ` 556` ``` ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set" ``` paulson@13871 ` 557` ``` by auto ``` nipkow@15392 ` 558` ``` also have "... = setsum (%j. p * j div q) Q_set" ``` nipkow@15392 ` 559` ``` using aux3b by(fastsimp intro: setsum_cong) ``` nipkow@15392 ` 560` ``` finally show ?thesis . ``` nipkow@15392 ` 561` ```qed ``` paulson@13871 ` 562` wenzelm@21233 ` 563` ```lemma S1_carda: "int (card(S1)) = ``` nipkow@15392 ` 564` ``` setsum (%j. (j * q) div p) P_set" ``` paulson@13871 ` 565` ``` by (auto simp add: S1_card zmult_ac) ``` paulson@13871 ` 566` wenzelm@21233 ` 567` ```lemma S2_carda: "int (card(S2)) = ``` nipkow@15392 ` 568` ``` setsum (%j. (j * p) div q) Q_set" ``` paulson@13871 ` 569` ``` by (auto simp add: S2_card zmult_ac) ``` paulson@13871 ` 570` wenzelm@21233 ` 571` ```lemma pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) + ``` nipkow@15392 ` 572` ``` (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)" ``` nipkow@15392 ` 573` ```proof - ``` wenzelm@18369 ` 574` ``` have "(setsum (%j. (j * p) div q) Q_set) + ``` nipkow@15392 ` 575` ``` (setsum (%j. (j * q) div p) P_set) = int (card S2) + int (card S1)" ``` paulson@13871 ` 576` ``` by (auto simp add: S1_carda S2_carda) ``` nipkow@15392 ` 577` ``` also have "... = int (card S1) + int (card S2)" ``` paulson@13871 ` 578` ``` by auto ``` nipkow@15392 ` 579` ``` also have "... = ((p - 1) div 2) * ((q - 1) div 2)" ``` paulson@13871 ` 580` ``` by (auto simp add: card_sum_S1_S2) ``` nipkow@15392 ` 581` ``` finally show ?thesis . ``` nipkow@15392 ` 582` ```qed ``` paulson@13871 ` 583` wenzelm@21233 ` 584` wenzelm@21288 ` 585` ```lemma (in -) pq_prime_neq: "[| zprime p; zprime q; p \ q |] ==> (~[p = 0] (mod q))" ``` paulson@13871 ` 586` ``` apply (auto simp add: zcong_eq_zdvd_prop zprime_def) ``` paulson@13871 ` 587` ``` apply (drule_tac x = q in allE) ``` paulson@13871 ` 588` ``` apply (drule_tac x = p in allE) ``` wenzelm@18369 ` 589` ``` apply auto ``` wenzelm@18369 ` 590` ``` done ``` paulson@13871 ` 591` wenzelm@21233 ` 592` wenzelm@21233 ` 593` ```lemma QR_short: "(Legendre p q) * (Legendre q p) = ``` nipkow@15392 ` 594` ``` (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))" ``` nipkow@15392 ` 595` ```proof - ``` nipkow@15392 ` 596` ``` from prems have "~([p = 0] (mod q))" ``` paulson@13871 ` 597` ``` by (auto simp add: pq_prime_neq QRTEMP_def) ``` wenzelm@21233 ` 598` ``` with prems Q_set_def have a1: "(Legendre p q) = (-1::int) ^ ``` nipkow@15392 ` 599` ``` nat(setsum (%x. ((x * p) div q)) Q_set)" ``` paulson@13871 ` 600` ``` apply (rule_tac p = q in MainQRLemma) ``` wenzelm@18369 ` 601` ``` apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def) ``` wenzelm@18369 ` 602` ``` done ``` nipkow@15392 ` 603` ``` from prems have "~([q = 0] (mod p))" ``` paulson@13871 ` 604` ``` apply (rule_tac p = q and q = p in pq_prime_neq) ``` nipkow@15392 ` 605` ``` apply (simp add: QRTEMP_def)+ ``` nipkow@16733 ` 606` ``` done ``` wenzelm@21233 ` 607` ``` with prems P_set_def have a2: "(Legendre q p) = ``` nipkow@15392 ` 608` ``` (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)" ``` paulson@13871 ` 609` ``` apply (rule_tac p = p in MainQRLemma) ``` wenzelm@18369 ` 610` ``` apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def) ``` wenzelm@18369 ` 611` ``` done ``` wenzelm@18369 ` 612` ``` from a1 a2 have "(Legendre p q) * (Legendre q p) = ``` paulson@13871 ` 613` ``` (-1::int) ^ nat(setsum (%x. ((x * p) div q)) Q_set) * ``` nipkow@15392 ` 614` ``` (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)" ``` paulson@13871 ` 615` ``` by auto ``` wenzelm@18369 ` 616` ``` also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) + ``` nipkow@15392 ` 617` ``` nat(setsum (%x. ((x * q) div p)) P_set))" ``` paulson@13871 ` 618` ``` by (auto simp add: zpower_zadd_distrib) ``` wenzelm@18369 ` 619` ``` also have "nat(setsum (%x. ((x * p) div q)) Q_set) + ``` paulson@13871 ` 620` ``` nat(setsum (%x. ((x * q) div p)) P_set) = ``` wenzelm@18369 ` 621` ``` nat((setsum (%x. ((x * p) div q)) Q_set) + ``` nipkow@15392 ` 622` ``` (setsum (%x. ((x * q) div p)) P_set))" ``` wenzelm@20898 ` 623` ``` apply (rule_tac z = "setsum (%x. ((x * p) div q)) Q_set" in ``` wenzelm@18369 ` 624` ``` nat_add_distrib [symmetric]) ``` wenzelm@18369 ` 625` ``` apply (auto simp add: S1_carda [symmetric] S2_carda [symmetric]) ``` wenzelm@18369 ` 626` ``` done ``` nipkow@15392 ` 627` ``` also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))" ``` paulson@13871 ` 628` ``` by (auto simp add: pq_sum_prop) ``` nipkow@15392 ` 629` ``` finally show ?thesis . ``` nipkow@15392 ` 630` ```qed ``` paulson@13871 ` 631` wenzelm@21233 ` 632` ```end ``` wenzelm@21233 ` 633` paulson@13871 ` 634` ```theorem Quadratic_Reciprocity: ``` wenzelm@18369 ` 635` ``` "[| p \ zOdd; zprime p; q \ zOdd; zprime q; ``` wenzelm@18369 ` 636` ``` p \ q |] ``` wenzelm@18369 ` 637` ``` ==> (Legendre p q) * (Legendre q p) = ``` nipkow@15392 ` 638` ``` (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))" ``` wenzelm@18369 ` 639` ``` by (auto simp add: QRTEMP.QR_short zprime_zOdd_eq_grt_2 [symmetric] ``` paulson@13871 ` 640` ``` QRTEMP_def) ``` paulson@13871 ` 641` paulson@13871 ` 642` ```end ```