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