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