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