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