eberlm@64282 ` 1` ```(* Author: Jaime Mendizabal Roche *) ``` eberlm@64282 ` 2` eberlm@64318 ` 3` ```theory Quadratic_Reciprocity ``` eberlm@64282 ` 4` ```imports Gauss ``` eberlm@64282 ` 5` ```begin ``` eberlm@64282 ` 6` wenzelm@64911 ` 7` ```text \The proof is based on Gauss's fifth proof, which can be found at http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf\ ``` eberlm@64282 ` 8` eberlm@64282 ` 9` ```locale QR = ``` eberlm@64282 ` 10` ``` fixes p :: "nat" ``` eberlm@64282 ` 11` ``` fixes q :: "nat" ``` eberlm@64282 ` 12` eberlm@64282 ` 13` ``` assumes p_prime: "prime p" ``` eberlm@64282 ` 14` ``` assumes p_ge_2: "2 < p" ``` eberlm@64282 ` 15` ``` assumes q_prime: "prime q" ``` eberlm@64282 ` 16` ``` assumes q_ge_2: "2 < q" ``` eberlm@64282 ` 17` ``` assumes pq_neq: "p \ q" ``` eberlm@64282 ` 18` ```begin ``` eberlm@64282 ` 19` eberlm@64282 ` 20` ```lemma odd_p: "odd p" using p_ge_2 p_prime prime_odd_nat by blast ``` eberlm@64282 ` 21` eberlm@64282 ` 22` ```lemma p_ge_0: "0 < int p" ``` eberlm@64282 ` 23` ``` using p_prime not_prime_0[where 'a = nat] by fastforce+ ``` eberlm@64282 ` 24` eberlm@64282 ` 25` ```lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1" using odd_p by simp ``` eberlm@64282 ` 26` eberlm@64282 ` 27` ```lemma odd_q: "odd q" using q_ge_2 q_prime prime_odd_nat by blast ``` eberlm@64282 ` 28` eberlm@64282 ` 29` ```lemma q_ge_0: "0 < int q" using q_prime not_prime_0[where 'a = nat] by fastforce+ ``` eberlm@64282 ` 30` eberlm@64282 ` 31` ```lemma q_eq2: "int q = (2 * ((int q - 1) div 2)) + 1" using odd_q by simp ``` eberlm@64282 ` 32` eberlm@64282 ` 33` ```lemma pq_eq2: "int p * int q = (2 * ((int p * int q - 1) div 2)) + 1" using odd_p odd_q by simp ``` eberlm@64282 ` 34` eberlm@64282 ` 35` ```lemma pq_coprime: "coprime p q" ``` eberlm@64282 ` 36` ``` using pq_neq p_prime primes_coprime_nat q_prime by blast ``` eberlm@64282 ` 37` eberlm@64282 ` 38` ```lemma pq_coprime_int: "coprime (int p) (int q)" ``` eberlm@64282 ` 39` ``` using pq_coprime transfer_int_nat_gcd(1) by presburger ``` eberlm@64282 ` 40` eberlm@64282 ` 41` ```lemma qp_ineq: "(int p * k \ (int p * int q - 1) div 2) = (k \ (int q - 1) div 2)" ``` eberlm@64282 ` 42` ```proof - ``` eberlm@64282 ` 43` ``` have "(2 * int p * k \ int p * int q - 1) = (2 * k \ int q - 1)" using p_ge_0 by auto ``` eberlm@64282 ` 44` ``` thus ?thesis by auto ``` eberlm@64282 ` 45` ```qed ``` eberlm@64282 ` 46` eberlm@64282 ` 47` ```lemma QRqp: "QR q p" using QR_def QR_axioms by simp ``` eberlm@64282 ` 48` eberlm@64282 ` 49` ```lemma pq_commute: "int p * int q = int q * int p" by simp ``` eberlm@64282 ` 50` eberlm@64282 ` 51` ```lemma pq_ge_0: "int p * int q > 0" using p_ge_0 q_ge_0 mult_pos_pos by blast ``` eberlm@64282 ` 52` eberlm@64282 ` 53` ```definition "r = ((p - 1) div 2)*((q - 1) div 2)" ``` eberlm@64282 ` 54` ```definition "m = card (GAUSS.E p q)" ``` eberlm@64282 ` 55` ```definition "n = card (GAUSS.E q p)" ``` eberlm@64282 ` 56` eberlm@64282 ` 57` ```abbreviation "Res (k::int) \ {0 .. k - 1}" ``` eberlm@64282 ` 58` ```abbreviation "Res_ge_0 (k::int) \ {0 <.. k - 1}" ``` eberlm@64282 ` 59` ```abbreviation "Res_0 (k::int) \ {0::int}" ``` eberlm@64282 ` 60` ```abbreviation "Res_l (k::int) \ {0 <.. (k - 1) div 2}" ``` eberlm@64282 ` 61` ```abbreviation "Res_h (k::int) \ {(k - 1) div 2 <.. k - 1}" ``` eberlm@64282 ` 62` eberlm@64282 ` 63` ```abbreviation "Sets_pq r0 r1 r2 \ ``` eberlm@64282 ` 64` ``` {(x::int). x \ r0 (int p * int q) \ x mod p \ r1 (int p) \ x mod q \ r2 (int q)}" ``` eberlm@64282 ` 65` eberlm@64282 ` 66` ```definition "A = Sets_pq Res_l Res_l Res_h" ``` eberlm@64282 ` 67` ```definition "B = Sets_pq Res_l Res_h Res_l" ``` eberlm@64282 ` 68` ```definition "C = Sets_pq Res_h Res_h Res_l" ``` eberlm@64282 ` 69` ```definition "D = Sets_pq Res_l Res_h Res_h" ``` eberlm@64282 ` 70` ```definition "E = Sets_pq Res_l Res_0 Res_h" ``` eberlm@64282 ` 71` ```definition "F = Sets_pq Res_l Res_h Res_0" ``` eberlm@64282 ` 72` eberlm@64282 ` 73` ```definition "a = card A" ``` eberlm@64282 ` 74` ```definition "b = card B" ``` eberlm@64282 ` 75` ```definition "c = card C" ``` eberlm@64282 ` 76` ```definition "d = card D" ``` eberlm@64282 ` 77` ```definition "e = card E" ``` eberlm@64282 ` 78` ```definition "f = card F" ``` eberlm@64282 ` 79` eberlm@64282 ` 80` ```lemma Gpq: "GAUSS p q" unfolding GAUSS_def ``` eberlm@64282 ` 81` ``` using p_prime pq_neq p_ge_2 q_prime ``` eberlm@64282 ` 82` ``` by (auto simp: cong_altdef_int zdvd_int [symmetric] dest: primes_dvd_imp_eq) ``` eberlm@64282 ` 83` eberlm@64282 ` 84` ```lemma Gqp: "GAUSS q p" using QRqp QR.Gpq by simp ``` eberlm@64282 ` 85` eberlm@64282 ` 86` ```lemma QR_lemma_01: "(\x. x mod q) ` E = GAUSS.E q p" ``` eberlm@64282 ` 87` ```proof ``` eberlm@64282 ` 88` ``` { ``` eberlm@64282 ` 89` ``` fix x ``` eberlm@64282 ` 90` ``` assume a1: "x \ E" ``` eberlm@64282 ` 91` ``` then obtain k where k: "x = int p * k" unfolding E_def by blast ``` eberlm@64282 ` 92` ``` have "x \ Res_l (int p * int q)" using a1 E_def by blast ``` eberlm@64282 ` 93` ``` hence "k \ GAUSS.A q" using Gqp GAUSS.A_def k qp_ineq by (simp add: zero_less_mult_iff) ``` eberlm@64282 ` 94` ``` hence "x mod q \ GAUSS.E q p" ``` eberlm@64282 ` 95` ``` using GAUSS.C_def[of q p] Gqp k GAUSS.B_def[of q p] a1 GAUSS.E_def[of q p] ``` eberlm@64282 ` 96` ``` unfolding E_def by force ``` eberlm@64282 ` 97` ``` hence "x \ E \ x mod int q \ GAUSS.E q p" by auto ``` eberlm@64282 ` 98` ``` } ``` eberlm@64282 ` 99` ``` thus "(\x. x mod int q) ` E \ GAUSS.E q p" by auto ``` eberlm@64282 ` 100` ```next ``` eberlm@64282 ` 101` ``` show "GAUSS.E q p \ (\x. x mod q) ` E" ``` eberlm@64282 ` 102` ``` proof ``` eberlm@64282 ` 103` ``` fix x ``` eberlm@64282 ` 104` ``` assume a1: "x \ GAUSS.E q p" ``` eberlm@64282 ` 105` ``` then obtain ka where ka: "ka \ GAUSS.A q" "x = (ka * p) mod q" ``` eberlm@64282 ` 106` ``` using Gqp GAUSS.B_def GAUSS.C_def GAUSS.E_def by auto ``` eberlm@64282 ` 107` ``` hence "ka * p \ Res_l (int p * int q)" ``` eberlm@64282 ` 108` ``` using GAUSS.A_def Gqp p_ge_0 qp_ineq by (simp add: Groups.mult_ac(2)) ``` eberlm@64282 ` 109` ``` thus "x \ (\x. x mod q) ` E" unfolding E_def using ka a1 Gqp GAUSS.E_def q_ge_0 by force ``` eberlm@64282 ` 110` ``` qed ``` eberlm@64282 ` 111` ```qed ``` eberlm@64282 ` 112` eberlm@64282 ` 113` ```lemma QR_lemma_02: "e= n" ``` eberlm@64282 ` 114` ```proof - ``` eberlm@64282 ` 115` ``` { ``` eberlm@64282 ` 116` ``` fix x y ``` eberlm@64282 ` 117` ``` assume a: "x \ E" "y \ E" "x mod q = y mod q" ``` eberlm@64282 ` 118` ``` obtain p_inv where p_inv: "[int p * p_inv = 1] (mod int q)" ``` eberlm@64282 ` 119` ``` using pq_coprime_int cong_solve_coprime_int by blast ``` eberlm@64282 ` 120` ``` obtain kx ky where k: "x = int p * kx" "y = int p * ky" using a E_def dvd_def[of p x] by blast ``` eberlm@64282 ` 121` ``` hence "0 < x" "int p * kx \ (int p * int q - 1) div 2" ``` eberlm@64282 ` 122` ``` "0 < y" "int p * ky \ (int p * int q - 1) div 2" ``` eberlm@64282 ` 123` ``` using E_def a greaterThanAtMost_iff mem_Collect_eq by blast+ ``` eberlm@64282 ` 124` ``` hence "0 \ kx" "kx < q" "0 \ ky" "ky < q" using qp_ineq k by (simp add: zero_less_mult_iff)+ ``` eberlm@64282 ` 125` ``` moreover have "(p_inv * (p * kx)) mod q = (p_inv * (p * ky)) mod q" ``` eberlm@64282 ` 126` ``` using a(3) mod_mult_cong k by blast ``` eberlm@64282 ` 127` ``` hence "(p * p_inv * kx) mod q = (p * p_inv * ky) mod q" by (simp add:algebra_simps) ``` eberlm@64282 ` 128` ``` hence "kx mod q = ky mod q" ``` eberlm@64282 ` 129` ``` using p_inv mod_mult_cong[of "p * p_inv" "q" "1"] cong_int_def by auto ``` eberlm@64282 ` 130` ``` hence "[kx = ky] (mod q)" using cong_int_def by blast ``` eberlm@64282 ` 131` ``` ultimately have "x = y" using cong_less_imp_eq_int k by blast ``` eberlm@64282 ` 132` ``` } ``` eberlm@64282 ` 133` ``` hence "inj_on (\x. x mod q) E" unfolding inj_on_def by auto ``` eberlm@64282 ` 134` ``` thus ?thesis using QR_lemma_01 card_image e_def n_def by fastforce ``` eberlm@64282 ` 135` ```qed ``` eberlm@64282 ` 136` eberlm@64282 ` 137` ```lemma QR_lemma_03: "f = m" ``` eberlm@64282 ` 138` ```proof - ``` eberlm@64282 ` 139` ``` have "F = QR.E q p" unfolding F_def pq_commute using QRqp QR.E_def[of q p] by fastforce ``` eberlm@64282 ` 140` ``` hence "f = QR.e q p" unfolding f_def using QRqp QR.e_def[of q p] by presburger ``` eberlm@64282 ` 141` ``` thus ?thesis using QRqp QR.QR_lemma_02 m_def QRqp QR.n_def by presburger ``` eberlm@64282 ` 142` ```qed ``` eberlm@64282 ` 143` eberlm@64282 ` 144` ```definition f_1 :: "int \ int \ int" where ``` eberlm@64282 ` 145` ``` "f_1 x = ((x mod p), (x mod q))" ``` eberlm@64282 ` 146` eberlm@64282 ` 147` ```definition P_1 :: "int \ int \ int \ bool" where ``` eberlm@64282 ` 148` ``` "P_1 res x \ x mod p = fst res & x mod q = snd res & x \ Res (int p * int q)" ``` eberlm@64282 ` 149` eberlm@64282 ` 150` ```definition g_1 :: "int \ int \ int" where ``` eberlm@64282 ` 151` ``` "g_1 res = (THE x. P_1 res x)" ``` eberlm@64282 ` 152` eberlm@64282 ` 153` ```lemma P_1_lemma: assumes "0 \ fst res" "fst res < p" "0 \ snd res" "snd res < q" ``` eberlm@64282 ` 154` ``` shows "\! x. P_1 res x" ``` eberlm@64282 ` 155` ```proof - ``` eberlm@64282 ` 156` ``` obtain y k1 k2 where yk: "y = nat (fst res) + k1 * p" "y = nat (snd res) + k2 * q" ``` eberlm@64282 ` 157` ``` using chinese_remainder[of p q] pq_coprime p_ge_0 q_ge_0 by fastforce ``` eberlm@64282 ` 158` ``` have h1: "[y = fst res] (mod p)" "[y = snd res] (mod q)" ``` eberlm@64282 ` 159` ``` using yk(1) assms(1) cong_iff_lin_int[of "fst res"] cong_sym_int apply simp ``` eberlm@64282 ` 160` ``` using yk(2) assms(3) cong_iff_lin_int[of "snd res"] cong_sym_int by simp ``` eberlm@64282 ` 161` ``` have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res" ``` eberlm@64282 ` 162` ``` using h1(1) mod_mod_cancel[of "int p"] assms(1) assms(2) cong_int_def apply simp ``` eberlm@64282 ` 163` ``` using h1(2) mod_mod_cancel[of "int q"] assms(3) assms(4) cong_int_def by simp ``` eberlm@64282 ` 164` ``` then obtain x where "P_1 res x" unfolding P_1_def ``` eberlm@64282 ` 165` ``` using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 by fastforce ``` eberlm@64282 ` 166` ``` moreover { ``` eberlm@64282 ` 167` ``` fix a b ``` eberlm@64282 ` 168` ``` assume a: "P_1 res a" "P_1 res b" ``` eberlm@64282 ` 169` ``` hence "int p * int q dvd a - b" ``` haftmann@64593 ` 170` ``` using divides_mult[of "int p" "a - b" "int q"] pq_coprime_int mod_eq_dvd_iff [of a _ b] ``` eberlm@64282 ` 171` ``` unfolding P_1_def by force ``` eberlm@64282 ` 172` ``` hence "a = b" using dvd_imp_le_int[of "a - b"] a unfolding P_1_def by fastforce ``` eberlm@64282 ` 173` ``` } ``` eberlm@64282 ` 174` ``` ultimately show ?thesis by auto ``` eberlm@64282 ` 175` ```qed ``` eberlm@64282 ` 176` eberlm@64282 ` 177` ```lemma g_1_lemma: assumes "0 \ fst res" "fst res < p" "0 \ snd res" "snd res < q" ``` eberlm@64282 ` 178` ``` shows "P_1 res (g_1 res)" using assms P_1_lemma theI'[of "P_1 res"] g_1_def by presburger ``` eberlm@64282 ` 179` eberlm@64282 ` 180` ```definition "BuC = Sets_pq Res_ge_0 Res_h Res_l" ``` eberlm@64282 ` 181` eberlm@64282 ` 182` ```lemma QR_lemma_04: "card BuC = card ((Res_h p) \ (Res_l q))" ``` eberlm@64282 ` 183` ``` using card_bij_eq[of f_1 "BuC" "(Res_h p) \ (Res_l q)" g_1] ``` eberlm@64282 ` 184` ```proof ``` eberlm@64282 ` 185` ``` { ``` eberlm@64282 ` 186` ``` fix x y ``` eberlm@64282 ` 187` ``` assume a: "x \ BuC" "y \ BuC" "f_1 x = f_1 y" ``` eberlm@64282 ` 188` ``` hence "int p * int q dvd x - y" ``` eberlm@64282 ` 189` ``` using f_1_def pq_coprime_int divides_mult[of "int p" "x - y" "int q"] ``` haftmann@64593 ` 190` ``` mod_eq_dvd_iff[of x _ y] by auto ``` eberlm@64282 ` 191` ``` hence "x = y" ``` eberlm@64282 ` 192` ``` using dvd_imp_le_int[of "x - y" "int p * int q"] a unfolding BuC_def by force ``` eberlm@64282 ` 193` ``` } ``` eberlm@64282 ` 194` ``` thus "inj_on f_1 BuC" unfolding inj_on_def by auto ``` eberlm@64282 ` 195` ```next ``` eberlm@64282 ` 196` ``` { ``` eberlm@64282 ` 197` ``` fix x y ``` eberlm@64282 ` 198` ``` assume a: "x \ (Res_h p) \ (Res_l q)" "y \ (Res_h p) \ (Res_l q)" "g_1 x = g_1 y" ``` eberlm@64282 ` 199` ``` hence "0 \ fst x" "fst x < p" "0 \ snd x" "snd x < q" ``` eberlm@64282 ` 200` ``` "0 \ fst y" "fst y < p" "0 \ snd y" "snd y < q" ``` eberlm@64282 ` 201` ``` using mem_Sigma_iff prod.collapse by fastforce+ ``` eberlm@64282 ` 202` ``` hence "x = y" using g_1_lemma[of x] g_1_lemma[of y] a P_1_def by fastforce ``` eberlm@64282 ` 203` ``` } ``` eberlm@64282 ` 204` ``` thus "inj_on g_1 ((Res_h p) \ (Res_l q))" unfolding inj_on_def by auto ``` eberlm@64282 ` 205` ```next ``` eberlm@64282 ` 206` ``` show "g_1 ` ((Res_h p) \ (Res_l q)) \ BuC" ``` eberlm@64282 ` 207` ``` proof ``` eberlm@64282 ` 208` ``` fix y ``` eberlm@64282 ` 209` ``` assume "y \ g_1 ` ((Res_h p) \ (Res_l q))" ``` eberlm@64282 ` 210` ``` then obtain x where x: "y = g_1 x" "x \ ((Res_h p) \ (Res_l q))" by blast ``` eberlm@64282 ` 211` ``` hence "P_1 x y" using g_1_lemma by fastforce ``` eberlm@64282 ` 212` ``` thus "y \ BuC" unfolding P_1_def BuC_def mem_Collect_eq using x SigmaE prod.sel by fastforce ``` eberlm@64282 ` 213` ``` qed ``` eberlm@64282 ` 214` ```qed (auto simp: BuC_def finite_subset f_1_def) ``` eberlm@64282 ` 215` eberlm@64282 ` 216` ```lemma QR_lemma_05: "card ((Res_h p) \ (Res_l q)) = r" ``` eberlm@64282 ` 217` ```proof - ``` eberlm@64282 ` 218` ``` have "card (Res_l q) = (q - 1) div 2" "card (Res_h p) = (p - 1) div 2" using p_eq2 by force+ ``` eberlm@64282 ` 219` ``` thus ?thesis unfolding r_def using card_cartesian_product[of "Res_h p" "Res_l q"] by presburger ``` eberlm@64282 ` 220` ```qed ``` eberlm@64282 ` 221` eberlm@64282 ` 222` ```lemma QR_lemma_06: "b + c = r" ``` eberlm@64282 ` 223` ```proof - ``` eberlm@64282 ` 224` ``` have "B \ C = {}" "finite B" "finite C" "B \ C = BuC" unfolding B_def C_def BuC_def by fastforce+ ``` eberlm@64282 ` 225` ``` thus ?thesis ``` eberlm@64282 ` 226` ``` unfolding b_def c_def using card_empty card_Un_Int QR_lemma_04 QR_lemma_05 by fastforce ``` eberlm@64282 ` 227` ```qed ``` eberlm@64282 ` 228` eberlm@64282 ` 229` ```definition f_2:: "int \ int" where ``` eberlm@64282 ` 230` ``` "f_2 x = (int p * int q) - x" ``` eberlm@64282 ` 231` eberlm@64282 ` 232` ```lemma f_2_lemma_1: "\x. f_2 (f_2 x) = x" unfolding f_2_def by simp ``` eberlm@64282 ` 233` eberlm@64282 ` 234` ```lemma f_2_lemma_2: "[f_2 x = int p - x] (mod p)" unfolding f_2_def using cong_altdef_int by simp ``` eberlm@64282 ` 235` eberlm@64282 ` 236` ```lemma f_2_lemma_3: "f_2 x \ S \ x \ f_2 ` S" ``` eberlm@64282 ` 237` ``` using f_2_lemma_1[of x] image_eqI[of x f_2 "f_2 x" S] by presburger ``` eberlm@64282 ` 238` eberlm@64282 ` 239` ```lemma QR_lemma_07: "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)" ``` eberlm@64282 ` 240` ``` "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)" ``` eberlm@64282 ` 241` ```proof - ``` eberlm@64282 ` 242` ``` have h1: "f_2 ` Res_l (int p * int q) \ Res_h (int p * int q)" using f_2_def by force ``` eberlm@64282 ` 243` ``` have h2: "f_2 ` Res_h (int p * int q) \ Res_l (int p * int q)" using f_2_def pq_eq2 by fastforce ``` eberlm@64282 ` 244` ``` have h3: "Res_h (int p * int q) \ f_2 ` Res_l (int p * int q)" using h2 f_2_lemma_3 by blast ``` eberlm@64282 ` 245` ``` have h4: "Res_l (int p * int q) \ f_2 ` Res_h (int p * int q)" using h1 f_2_lemma_3 by blast ``` eberlm@64282 ` 246` ``` show "f_2 ` Res_l (int p * int q) = Res_h (int p * int q)" using h1 h3 by blast ``` eberlm@64282 ` 247` ``` show "f_2 ` Res_h (int p * int q) = Res_l (int p * int q)" using h2 h4 by blast ``` eberlm@64282 ` 248` ```qed ``` eberlm@64282 ` 249` eberlm@64282 ` 250` ```lemma QR_lemma_08: "(f_2 x mod p \ Res_l p) = (x mod p \ Res_h p)" ``` eberlm@64282 ` 251` ``` "(f_2 x mod p \ Res_h p) = (x mod p \ Res_l p)" ``` eberlm@64282 ` 252` ``` using f_2_lemma_2[of x] cong_int_def[of "f_2 x" "p - x" p] minus_mod_self2[of x p] ``` eberlm@64282 ` 253` ``` zmod_zminus1_eq_if[of x p] p_eq2 by auto ``` eberlm@64282 ` 254` eberlm@64282 ` 255` ```lemma QR_lemma_09: "(f_2 x mod q \ Res_l q) = (x mod q \ Res_h q)" ``` eberlm@64282 ` 256` ``` "(f_2 x mod q \ Res_h q) = (x mod q \ Res_l q)" ``` eberlm@64282 ` 257` ``` using QRqp QR.QR_lemma_08 f_2_def QR.f_2_def pq_commute by auto+ ``` eberlm@64282 ` 258` eberlm@64282 ` 259` ```lemma QR_lemma_10: "a = c" unfolding a_def c_def apply (rule card_bij_eq[of f_2 A C f_2]) ``` eberlm@64282 ` 260` ``` unfolding A_def C_def ``` eberlm@64282 ` 261` ``` using QR_lemma_07 QR_lemma_08 QR_lemma_09 apply ((simp add: inj_on_def f_2_def),blast)+ ``` eberlm@64282 ` 262` ``` by fastforce+ ``` eberlm@64282 ` 263` eberlm@64282 ` 264` ```definition "BuD = Sets_pq Res_l Res_h Res_ge_0" ``` eberlm@64282 ` 265` ```definition "BuDuF = Sets_pq Res_l Res_h Res" ``` eberlm@64282 ` 266` eberlm@64282 ` 267` ```definition f_3 :: "int \ int \ int" where ``` eberlm@64282 ` 268` ``` "f_3 x = (x mod p, x div p + 1)" ``` eberlm@64282 ` 269` eberlm@64282 ` 270` ```definition g_3 :: "int \ int \ int" where ``` eberlm@64282 ` 271` ``` "g_3 x = fst x + (snd x - 1) * p" ``` eberlm@64282 ` 272` eberlm@64282 ` 273` ```lemma QR_lemma_11: "card BuDuF = card ((Res_h p) \ (Res_l q))" ``` eberlm@64282 ` 274` ``` using card_bij_eq[of f_3 BuDuF "(Res_h p) \ (Res_l q)" g_3] ``` eberlm@64282 ` 275` ```proof ``` eberlm@64282 ` 276` ``` show "f_3 ` BuDuF \ (Res_h p) \ (Res_l q)" ``` eberlm@64282 ` 277` ``` proof ``` eberlm@64282 ` 278` ``` fix y ``` eberlm@64282 ` 279` ``` assume "y \ f_3 ` BuDuF" ``` eberlm@64282 ` 280` ``` then obtain x where x: "y = f_3 x" "x \ BuDuF" by blast ``` eberlm@64282 ` 281` ``` hence "x \ int p * (int q - 1) div 2 + (int p - 1) div 2" ``` eberlm@64282 ` 282` ``` unfolding BuDuF_def using p_eq2 int_distrib(4) by auto ``` eberlm@64282 ` 283` ``` moreover have "(int p - 1) div 2 \ - 1 + x mod p" using x BuDuF_def by auto ``` eberlm@64282 ` 284` ``` moreover have "int p * (int q - 1) div 2 = int p * ((int q - 1) div 2)" ``` eberlm@64282 ` 285` ``` using zdiv_zmult1_eq odd_q by auto ``` eberlm@64282 ` 286` ``` hence "p * (int q - 1) div 2 = p * ((int q + 1) div 2 - 1)" by fastforce ``` eberlm@64282 ` 287` ``` ultimately have "x \ p * ((int q + 1) div 2 - 1) - 1 + x mod p" by linarith ``` eberlm@64282 ` 288` ``` hence "x div p < (int q + 1) div 2 - 1" ``` eberlm@64282 ` 289` ``` using mult.commute[of "int p" "x div p"] p_ge_0 div_mult_mod_eq[of x p] ``` eberlm@64282 ` 290` ``` mult_less_cancel_left_pos[of p "x div p" "(int q + 1) div 2 - 1"] by linarith ``` eberlm@64282 ` 291` ``` moreover have "0 < x div p + 1" ``` eberlm@64282 ` 292` ``` using pos_imp_zdiv_neg_iff[of p x] p_ge_0 x mem_Collect_eq BuDuF_def by auto ``` eberlm@64282 ` 293` ``` ultimately show "y \ (Res_h p) \ (Res_l q)" using x BuDuF_def f_3_def by auto ``` eberlm@64282 ` 294` ``` qed ``` eberlm@64282 ` 295` ```next ``` eberlm@64282 ` 296` ``` have h1: "\x. x \ ((Res_h p) \ (Res_l q)) \ f_3 (g_3 x) = x" ``` eberlm@64282 ` 297` ``` proof - ``` eberlm@64282 ` 298` ``` fix x ``` eberlm@64282 ` 299` ``` assume a: "x \ ((Res_h p) \ (Res_l q))" ``` eberlm@64282 ` 300` ``` moreover have h: "(fst x + (snd x - 1) * int p) mod int p = fst x" using a by force ``` eberlm@64282 ` 301` ``` ultimately have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x" ``` eberlm@64282 ` 302` ``` by (auto simp: semiring_numeral_div_class.div_less) ``` eberlm@64282 ` 303` ``` with h show "f_3 (g_3 x) = x" unfolding f_3_def g_3_def by simp ``` eberlm@64282 ` 304` ``` qed ``` eberlm@64282 ` 305` ``` show "inj_on g_3 ((Res_h p) \ (Res_l q))" apply (rule inj_onI[of "(Res_h p) \ (Res_l q)" g_3]) ``` eberlm@64282 ` 306` ``` proof - ``` eberlm@64282 ` 307` ``` fix x y ``` eberlm@64282 ` 308` ``` assume "x \ ((Res_h p) \ (Res_l q))" "y \ ((Res_h p) \ (Res_l q))" "g_3 x = g_3 y" ``` eberlm@64282 ` 309` ``` thus "x = y" using h1[of x] h1[of y] by presburger ``` eberlm@64282 ` 310` ``` qed ``` eberlm@64282 ` 311` ```next ``` eberlm@64282 ` 312` ``` show "g_3 ` ((Res_h p) \ (Res_l q)) \ BuDuF" ``` eberlm@64282 ` 313` ``` proof ``` eberlm@64282 ` 314` ``` fix y ``` eberlm@64282 ` 315` ``` assume "y \ g_3 ` ((Res_h p) \ (Res_l q))" ``` eberlm@64282 ` 316` ``` then obtain x where x: "y = g_3 x" "x \ (Res_h p) \ (Res_l q)" by blast ``` eberlm@64282 ` 317` ``` hence "snd x \ (int q - 1) div 2" by force ``` eberlm@64282 ` 318` ``` moreover have "int p * ((int q - 1) div 2) = (int p * int q - int p) div 2" ``` eberlm@64282 ` 319` ``` using int_distrib(4) zdiv_zmult1_eq[of "int p" "int q - 1" 2] odd_q by fastforce ``` eberlm@64282 ` 320` ``` ultimately have "(snd x) * int p \ (int q * int p - int p) div 2" ``` eberlm@64282 ` 321` ``` using mult_right_mono[of "snd x" "(int q - 1) div 2" p] mult.commute[of "(int q - 1) div 2" p] ``` eberlm@64282 ` 322` ``` pq_commute by presburger ``` eberlm@64282 ` 323` ``` hence "(snd x - 1) * int p \ (int q * int p - 1) div 2 - int p" ``` eberlm@64282 ` 324` ``` using p_ge_0 int_distrib(3) by auto ``` eberlm@64282 ` 325` ``` moreover have "fst x \ int p - 1" using x by force ``` eberlm@64282 ` 326` ``` ultimately have "fst x + (snd x - 1) * int p \ (int p * int q - 1) div 2" ``` eberlm@64282 ` 327` ``` using pq_commute by linarith ``` eberlm@64282 ` 328` ``` moreover have "0 < fst x" "0 \ (snd x - 1) * p" using x(2) by fastforce+ ``` eberlm@64282 ` 329` ``` ultimately show "y \ BuDuF" unfolding BuDuF_def using q_ge_0 x g_3_def x(1) by auto ``` eberlm@64282 ` 330` ``` qed ``` eberlm@64282 ` 331` ```next ``` eberlm@64282 ` 332` ``` show "finite BuDuF" unfolding BuDuF_def by fastforce ``` eberlm@64282 ` 333` ```qed (simp add: inj_on_inverseI[of BuDuF g_3] f_3_def g_3_def QR_lemma_05)+ ``` eberlm@64282 ` 334` eberlm@64282 ` 335` ```lemma QR_lemma_12: "b + d + m = r" ``` eberlm@64282 ` 336` ```proof - ``` eberlm@64282 ` 337` ``` have "B \ D = {}" "finite B" "finite D" "B \ D = BuD" unfolding B_def D_def BuD_def by fastforce+ ``` eberlm@64282 ` 338` ``` hence "b + d = card BuD" unfolding b_def d_def using card_Un_Int by fastforce ``` eberlm@64282 ` 339` ``` moreover have "BuD \ F = {}" "finite BuD" "finite F" unfolding BuD_def F_def by fastforce+ ``` eberlm@64282 ` 340` ``` moreover have "BuD \ F = BuDuF" unfolding BuD_def F_def BuDuF_def ``` eberlm@64282 ` 341` ``` using q_ge_0 ivl_disj_un_singleton(5)[of 0 "int q - 1"] by auto ``` eberlm@64282 ` 342` ``` ultimately show ?thesis using QR_lemma_03 QR_lemma_05 QR_lemma_11 card_Un_disjoint[of BuD F] ``` eberlm@64282 ` 343` ``` unfolding b_def d_def f_def by presburger ``` eberlm@64282 ` 344` ```qed ``` eberlm@64282 ` 345` eberlm@64282 ` 346` ```lemma QR_lemma_13: "a + d + n = r" ``` eberlm@64282 ` 347` ```proof - ``` eberlm@64282 ` 348` ``` have "A = QR.B q p" unfolding A_def pq_commute using QRqp QR.B_def[of q p] by blast ``` eberlm@64282 ` 349` ``` hence "a = QR.b q p" using a_def QRqp QR.b_def[of q p] by presburger ``` eberlm@64282 ` 350` ``` moreover have "D = QR.D q p" unfolding D_def pq_commute using QRqp QR.D_def[of q p] by blast ``` eberlm@64282 ` 351` ``` hence "d = QR.d q p" using d_def QRqp QR.d_def[of q p] by presburger ``` eberlm@64282 ` 352` ``` moreover have "n = QR.m q p" using n_def QRqp QR.m_def[of q p] by presburger ``` eberlm@64282 ` 353` ``` moreover have "r = QR.r q p" unfolding r_def using QRqp QR.r_def[of q p] by auto ``` eberlm@64282 ` 354` ``` ultimately show ?thesis using QRqp QR.QR_lemma_12 by presburger ``` eberlm@64282 ` 355` ```qed ``` eberlm@64282 ` 356` eberlm@64282 ` 357` ```lemma QR_lemma_14: "(-1::int) ^ (m + n) = (-1) ^ r" ``` eberlm@64282 ` 358` ```proof - ``` eberlm@64282 ` 359` ``` have "m + n + 2 * d = r" using QR_lemma_06 QR_lemma_10 QR_lemma_12 QR_lemma_13 by auto ``` eberlm@64282 ` 360` ``` thus ?thesis using power_add[of "-1::int" "m + n" "2 * d"] by fastforce ``` eberlm@64282 ` 361` ```qed ``` eberlm@64282 ` 362` eberlm@64282 ` 363` ```lemma Quadratic_Reciprocity: ``` eberlm@64282 ` 364` ``` "(Legendre p q) * (Legendre q p) = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))" ``` eberlm@64282 ` 365` ``` using Gpq Gqp GAUSS.gauss_lemma power_add[of "-1::int" m n] QR_lemma_14 ``` eberlm@64282 ` 366` ``` unfolding r_def m_def n_def by auto ``` eberlm@64282 ` 367` eberlm@64282 ` 368` ```end ``` eberlm@64282 ` 369` eberlm@64282 ` 370` ```theorem Quadratic_Reciprocity: assumes "prime p" "2 < p" "prime q" "2 < q" "p \ q" ``` eberlm@64282 ` 371` ``` shows "(Legendre p q) * (Legendre q p) = (-1::int) ^ ((p - 1) div 2 * ((q - 1) div 2))" ``` eberlm@64282 ` 372` ``` using QR.Quadratic_Reciprocity QR_def assms by blast ``` eberlm@64282 ` 373` eberlm@64282 ` 374` ```theorem Quadratic_Reciprocity_int: assumes "prime (nat p)" "2 < p" "prime (nat q)" "2 < q" "p \ q" ``` eberlm@64282 ` 375` ``` shows "(Legendre p q) * (Legendre q p) = (-1::int) ^ (nat ((p - 1) div 2 * ((q - 1) div 2)))" ``` eberlm@64282 ` 376` ```proof - ``` eberlm@64282 ` 377` ``` have "0 \ (p - 1) div 2" using assms by simp ``` eberlm@64282 ` 378` ``` moreover have "(nat p - 1) div 2 = nat ((p - 1) div 2)" "(nat q - 1) div 2 = nat ((q - 1) div 2)" ``` eberlm@64282 ` 379` ``` by fastforce+ ``` eberlm@64282 ` 380` ``` ultimately have "(nat p - 1) div 2 * ((nat q - 1) div 2) = nat ((p - 1) div 2 * ((q - 1) div 2))" ``` eberlm@64282 ` 381` ``` using nat_mult_distrib by presburger ``` eberlm@64282 ` 382` ``` moreover have "2 < nat p" "2 < nat q" "nat p \ nat q" "int (nat p) = p" "int (nat q) = q" ``` eberlm@64282 ` 383` ``` using assms by linarith+ ``` eberlm@64282 ` 384` ``` ultimately show ?thesis using Quadratic_Reciprocity[of "nat p" "nat q"] assms by presburger ``` eberlm@64282 ` 385` ```qed ``` eberlm@64282 ` 386` eberlm@64318 ` 387` ```end ```