22 from finite_A have "a * setsum id A = setsum (%x. a * x) A" |
22 from finite_A have "a * setsum id A = setsum (%x. a * x) A" |
23 by (auto simp add: setsum_const_mult id_def) |
23 by (auto simp add: setsum_const_mult id_def) |
24 also have "setsum (%x. a * x) = setsum (%x. x * a)" |
24 also have "setsum (%x. a * x) = setsum (%x. x * a)" |
25 by (auto simp add: zmult_commute) |
25 by (auto simp add: zmult_commute) |
26 also have "setsum (%x. x * a) A = setsum id B" |
26 also have "setsum (%x. x * a) A = setsum id B" |
27 by (auto simp add: B_def setsum_reindex_id finite_A inj_on_xa_A) |
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" |
28 also have "... = setsum (%x. p * (x div p) + StandardRes p x) B" |
29 apply (rule setsum_cong) |
29 by (auto simp add: StandardRes_def zmod_zdiv_equality) |
30 by (auto simp add: finite_B StandardRes_def zmod_zdiv_equality) |
|
31 also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B" |
30 also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B" |
32 by (rule setsum_addf) |
31 by (rule setsum_addf) |
33 also have "setsum (StandardRes p) B = setsum id C" |
32 also have "setsum (StandardRes p) B = setsum id C" |
34 by (auto simp add: C_def setsum_reindex_id [THEN sym] finite_B |
33 by (auto simp add: C_def setsum_reindex_id[OF SR_B_inj]) |
35 SR_B_inj) |
|
36 also from C_eq have "... = setsum id (D \<union> E)" |
34 also from C_eq have "... = setsum id (D \<union> E)" |
37 by auto |
35 by auto |
38 also from finite_D finite_E have "... = setsum id D + setsum id E" |
36 also from finite_D finite_E have "... = setsum id D + setsum id E" |
39 apply (rule setsum_Un_disjoint) |
37 apply (rule setsum_Un_disjoint) |
40 by (auto simp add: D_def E_def) |
38 by (auto simp add: D_def E_def) |
41 also have "setsum (%x. p * (x div p)) B = |
39 also have "setsum (%x. p * (x div p)) B = |
42 setsum ((%x. p * (x div p)) o (%x. (x * a))) A" |
40 setsum ((%x. p * (x div p)) o (%x. (x * a))) A" |
43 by (auto simp add: B_def setsum_reindex finite_A inj_on_xa_A) |
41 by (auto simp add: B_def setsum_reindex inj_on_xa_A) |
44 also have "... = setsum (%x. p * ((x * a) div p)) A" |
42 also have "... = setsum (%x. p * ((x * a) div p)) A" |
45 by (auto simp add: o_def) |
43 by (auto simp add: o_def) |
46 also from finite_A have "setsum (%x. p * ((x * a) div p)) A = |
44 also from finite_A have "setsum (%x. p * ((x * a) div p)) A = |
47 p * setsum (%x. ((x * a) div p)) A" |
45 p * setsum (%x. ((x * a) div p)) A" |
48 by (auto simp add: setsum_const_mult) |
46 by (auto simp add: setsum_const_mult) |
586 apply (rule_tac p = q in MainQRLemma) |
584 apply (rule_tac p = q in MainQRLemma) |
587 by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def) |
585 by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def) |
588 from prems have "~([q = 0] (mod p))" |
586 from prems have "~([q = 0] (mod p))" |
589 apply (rule_tac p = q and q = p in pq_prime_neq) |
587 apply (rule_tac p = q and q = p in pq_prime_neq) |
590 apply (simp add: QRTEMP_def)+ |
588 apply (simp add: QRTEMP_def)+ |
591 by arith |
589 done |
592 with prems have a2: "(Legendre q p) = |
590 with prems have a2: "(Legendre q p) = |
593 (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)" |
591 (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)" |
594 apply (rule_tac p = p in MainQRLemma) |
592 apply (rule_tac p = p in MainQRLemma) |
595 by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def) |
593 by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def) |
596 from a1 a2 have "(Legendre p q) * (Legendre q p) = |
594 from a1 a2 have "(Legendre p q) * (Legendre q p) = |