author haftmann Wed Sep 26 20:27:55 2007 +0200 (2007-09-26) changeset 24728 e2b3a1065676 parent 23431 25ca91279a9b child 30034 60f64f112174 permissions -rw-r--r--
moved Finite_Set before Datatype
1 (*  Title:      HOL/NumberTheory/Quadratic_Reciprocity.thy
2     ID:         \$Id\$
3     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
4 *)
6 header {* The law of Quadratic reciprocity *}
9 imports Gauss
10 begin
12 text {*
13   Lemmas leading up to the proof of theorem 3.3 in Niven and
14   Zuckerman's presentation.
15 *}
17 context GAUSS
18 begin
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
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
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
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
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
144 end
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
157 subsection {* Stuff about S, S1 and S2 *}
159 locale QRTEMP =
160   fixes p     :: "int"
161   fixes q     :: "int"
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
170 definition
171   P_set :: "int set" where
172   "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
174 definition
175   Q_set :: "int set" where
176   "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
178 definition
179   S :: "(int * int) set" where
180   "S = P_set <*> Q_set"
182 definition
183   S1 :: "(int * int) set" where
184   "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
186 definition
187   S2 :: "(int * int) set" where
188   "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
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) }"
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) }"
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
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
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
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)
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)
259 lemma S_finite: "finite S"
260   by (auto simp add: S_def  P_set_finite Q_set_finite finite_cartesian_product)
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
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
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)
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)
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)
286 lemma S1_Int_S2_prop: "S1 \<inter> S2 = {}"
287   by (auto simp add: S1_def S2_def)
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
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
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 zdiv_zmult_self2, 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
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 zdiv_zmult_self2, 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
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
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
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
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
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
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)
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)
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
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
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))"
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
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
634 end