Up to index of Isabelle/HOL/HOL-Complex/NumberTheory

```(*  Title:      QuadraticReciprocity.thy
*)

(***************************************************************)
(*                                                             *)
(*  Lemmas leading up to the proof of theorem 3.3 in           *)
(*  Niven and Zuckerman's presentation                         *)
(*                                                             *)
(***************************************************************)

lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
c * setsum f A";
apply (induct set: Finites, auto)

lemma (in GAUSS) QRLemma1: "a * setsum id A =
p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E";
proof -;
from finite_A have "a * setsum id A = setsum (%x. a * x) A";
also have "setsum (%x. a * x) = setsum (%x. x * a)";
also; have "setsum (%x. x * a) A = setsum id B";
by (auto simp add: B_def setsum_reindex_id finite_A inj_on_xa_A)
also have "... = setsum (%x. p * (x div p) + StandardRes p x) B";
apply (rule setsum_cong);
by (auto simp add: finite_B StandardRes_def zmod_zdiv_equality)
also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B";
also; have "setsum (StandardRes p) B = setsum id C";
by (auto simp add: C_def setsum_reindex_id [THEN sym] finite_B
SR_B_inj)
also; from C_eq have "... = setsum id (D ∪ E)";
by auto
also; from finite_D finite_E have "... = setsum id D + setsum id E";
apply (rule setsum_Un_disjoint)
by (auto simp add: D_def E_def)
also have "setsum (%x. p * (x div p)) B =
setsum ((%x. p * (x div p)) o (%x. (x * a))) A";
by (auto simp add: B_def setsum_reindex finite_A inj_on_xa_A)
also have "... = setsum (%x. p * ((x * a) div p)) A";
also from finite_A have "setsum (%x. p * ((x * a) div p)) A =
p * setsum (%x. ((x * a) div p)) A";
finally show ?thesis by arith
qed;

lemma (in GAUSS) QRLemma2: "setsum id A = p * int (card E) - setsum id E +
setsum id D";
proof -;
from F_Un_D_eq_A have "setsum id A = setsum id (D ∪ F)";
also from F_D_disj finite_D finite_F have
"... = setsum id D + setsum id F";
by (intro setsum_Un_disjoint)
also from F_def have "F = (%x. (p - x)) ` E";
by auto
also from finite_E inj_on_pminusx_E have "setsum id ((%x. (p - x)) ` E) =
setsum (%x. (p - x)) E";
also from finite_E have "setsum (op - p) E = setsum (%x. p) E - setsum id E";
by (auto simp add: setsum_subtractf id_def)
also from finite_E have "setsum (%x. p) E = p * int(card E)";
apply (subst setsum_constant);
apply (assumption);
done;
finally show ?thesis;
by arith
qed;

lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A =
p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E";
proof -;
have "(a - 1) * setsum id A = a * setsum id A - setsum id A";
also note QRLemma1;
also; from QRLemma2 have "p * (∑x ∈ A. x * a div p) + setsum id D +
setsum id E - setsum id A =
p * (∑x ∈ A. x * a div p) + setsum id D +
setsum id E - (p * int (card E) - setsum id E + setsum id D)";
by auto
also; have "... = p * (∑x ∈ A. x * a div p) -
p * int (card E) + 2 * setsum id E";
by arith
finally show ?thesis;
by (auto simp only: zdiff_zmult_distrib2)
qed;

lemma (in GAUSS) QRLemma4: "a ∈ zOdd ==>
(setsum (%x. ((x * a) div p)) A ∈ zEven) = (int(card E): zEven)";
proof -;
assume a_odd: "a ∈ zOdd";
from QRLemma3 have a: "p * (setsum (%x. ((x * a) div p)) A - int(card E)) =
(a - 1) * setsum id A - 2 * setsum id E";
by arith
from a_odd have "a - 1 ∈ zEven"
by (rule odd_minus_one_even)
hence "(a - 1) * setsum id A ∈ zEven";
by (rule even_times_either)
moreover have "2 * setsum id E ∈ zEven";
ultimately have "(a - 1) * setsum id A - 2 * setsum id E ∈ zEven"
by (rule even_minus_even)
with a have "p * (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
by simp
hence "p ∈ zEven | (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
by (rule EvenOdd2.even_product)
with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
thus ?thesis;
by (auto simp only: even_diff [THEN sym])
qed;

lemma (in GAUSS) QRLemma5: "a ∈ zOdd ==>
(-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))";
proof -;
assume "a ∈ zOdd";
from QRLemma4 have
"(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A ∈ zEven)";..;
moreover have "0 ≤ int(card E)";
by auto
moreover have "0 ≤ setsum (%x. ((x * a) div p)) A";
proof (intro setsum_nonneg);
from finite_A show "finite A";.;
next show "∀x ∈ A. 0 ≤ x * a div p";
proof;
fix x;
assume "x ∈ A";
then have "0 ≤ x";
with a_nonzero have "0 ≤ x * a";
with p_g_2 show "0 ≤ x * a div p";
qed;
qed;
ultimately have "(-1::int)^nat((int (card E))) =
(-1)^nat(((∑x ∈ A. x * a div p)))";
by (intro neg_one_power_parity, auto)
also have "nat (int(card E)) = card E";
by auto
finally show ?thesis;.;
qed;

lemma MainQRLemma: "[| a ∈ zOdd; 0 < a; ~([a = 0] (mod p));p ∈ zprime; 2 < p;
A = {x. 0 < x & x ≤ (p - 1) div 2} |] ==>
(Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))";
apply (subst GAUSS.gauss_lemma)
apply (subst GAUSS.QRLemma5)

(******************************************************************)
(*                                                                *)
(* Stuff about S, S1 and S2...                                    *)
(*                                                                *)
(******************************************************************)

locale QRTEMP =
fixes p     :: "int"
fixes q     :: "int"
fixes P_set :: "int set"
fixes Q_set :: "int set"
fixes S     :: "(int * int) set"
fixes S1    :: "(int * int) set"
fixes S2    :: "(int * int) set"
fixes f1    :: "int => (int * int) set"
fixes f2    :: "int => (int * int) set"

assumes p_prime: "p ∈ zprime"
assumes p_g_2: "2 < p"
assumes q_prime: "q ∈ zprime"
assumes q_g_2: "2 < q"
assumes p_neq_q:      "p ≠ q"

defines P_set_def: "P_set == {x. 0 < x & x ≤ ((p - 1) div 2) }"
defines Q_set_def: "Q_set == {x. 0 < x & x ≤ ((q - 1) div 2) }"
defines S_def:     "S     == P_set <*> Q_set"
defines S1_def:    "S1    == { (x, y). (x, y):S & ((p * y) < (q * x)) }"
defines S2_def:    "S2    == { (x, y). (x, y):S & ((q * x) < (p * y)) }"
defines f1_def:    "f1 j  == { (j1, y). (j1, y):S & j1 = j &
(y ≤ (q * j) div p) }"
defines f2_def:    "f2 j  == { (x, j1). (x, j1):S & j1 = j &
(x ≤ (p * j) div q) }";

lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2";
proof -;
from prems have "2 < p" by (simp add: QRTEMP_def)
then have "2 ≤ p - 1" by arith
then have "2 div 2 ≤ (p - 1) div 2" by (rule zdiv_mono1, auto)
then show ?thesis by auto
qed;

lemma (in QRTEMP) q_fact: "0 < (q - 1) div 2";
proof -;
from prems have "2 < q" by (simp add: QRTEMP_def)
then have "2 ≤ q - 1" by arith
then have "2 div 2 ≤ (q - 1) div 2" by (rule zdiv_mono1, auto)
then show ?thesis by auto
qed;

lemma (in QRTEMP) pb_neq_qa: "[|1 ≤ b; b ≤ (q - 1) div 2 |] ==>
(p * b ≠ q * a)";
proof;
assume "p * b = q * a" and "1 ≤ b" and "b ≤ (q - 1) div 2";
then have "q dvd (p * b)" by (auto simp add: dvd_def)
with q_prime p_g_2 have "q dvd p | q dvd b";
moreover have "~ (q dvd p)";
proof;
assume "q dvd p";
with p_prime have "q = 1 | q = p"
apply (auto simp add: zprime_def QRTEMP_def)
apply (drule_tac x = q and R = False in allE)
apply (subgoal_tac "0 ≤ q", simp add: QRTEMP_def)
apply (insert prems)
with q_g_2 p_neq_q show False by auto
qed;
ultimately have "q dvd b" by auto
then have "q ≤ b";
proof -;
assume "q dvd b";
moreover from prems have "0 < b" by auto
ultimately show ?thesis by (insert zdvd_bounds [of q b], auto)
qed;
with prems have "q ≤ (q - 1) div 2" by auto
then have "2 * q ≤ 2 * ((q - 1) div 2)" by arith
then have "2 * q ≤ q - 1";
proof -;
assume "2 * q ≤ 2 * ((q - 1) div 2)";
with prems have "q ∈ zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
with odd_minus_one_even have "(q - 1):zEven" by auto
with even_div_2_prop2 have "(q - 1) = 2 * ((q - 1) div 2)" by auto
with prems show ?thesis by auto
qed;
then have p1: "q ≤ -1" by arith
with q_g_2 show False by auto
qed;

lemma (in QRTEMP) P_set_finite: "finite (P_set)";
by (insert p_fact, auto simp add: P_set_def bdd_int_set_l_le_finite)

lemma (in QRTEMP) Q_set_finite: "finite (Q_set)";
by (insert q_fact, auto simp add: Q_set_def bdd_int_set_l_le_finite)

lemma (in QRTEMP) S_finite: "finite S";
by (auto simp add: S_def  P_set_finite Q_set_finite);

lemma (in QRTEMP) S1_finite: "finite S1";
proof -;
have "finite S" by (auto simp add: S_finite)
moreover have "S1 ⊆ S" by (auto simp add: S1_def S_def)
ultimately show ?thesis by (auto simp add: finite_subset)
qed;

lemma (in QRTEMP) S2_finite: "finite S2";
proof -;
have "finite S" by (auto simp add: S_finite)
moreover have "S2 ⊆ S" by (auto simp add: S2_def S_def)
ultimately show ?thesis by (auto simp add: finite_subset)
qed;

lemma (in QRTEMP) P_set_card: "(p - 1) div 2 = int (card (P_set))";
by (insert p_fact, auto simp add: P_set_def card_bdd_int_set_l_le)

lemma (in QRTEMP) Q_set_card: "(q - 1) div 2 = int (card (Q_set))";
by (insert q_fact, auto simp add: Q_set_def card_bdd_int_set_l_le)

lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
apply (insert P_set_card Q_set_card P_set_finite Q_set_finite)
apply (auto simp add: S_def zmult_int setsum_constant);
done

lemma (in QRTEMP) S1_Int_S2_prop: "S1 ∩ S2 = {}";
by (auto simp add: S1_def S2_def)

lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 ∪ S2";
apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def)
proof -;
fix a and b;
assume "~ q * a < p * b" and b1: "0 < b" and b2: "b ≤ (q - 1) div 2";
with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
moreover from pb_neq_qa b1 b2 have "(p * b ≠ q * a)" by auto
ultimately show "p * b < q * a" by auto
qed;

lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) =
int(card(S1)) + int(card(S2))";
proof-;
have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
also have "... = int( card(S1) + card(S2))";
apply (insert S1_finite S2_finite S1_Int_S2_prop S1_Union_S2_prop)
apply (drule card_Un_disjoint, auto)
done
also have "... = int(card(S1)) + int(card(S2))" by auto
finally show ?thesis .;
qed;

lemma (in QRTEMP) aux1a: "[| 0 < a; a ≤ (p - 1) div 2;
0 < b; b ≤ (q - 1) div 2 |] ==>
(p * b < q * a) = (b ≤ q * a div p)";
proof -;
assume "0 < a" and "a ≤ (p - 1) div 2" and "0 < b" and "b ≤ (q - 1) div 2";
have "p * b < q * a ==> b ≤ q * a div p";
proof -;
assume "p * b < q * a";
then have "p * b ≤ q * a" by auto
then have "(p * b) div p ≤ (q * a) div p";
by (rule zdiv_mono1, insert p_g_2, auto)
then show "b ≤ (q * a) div p";
apply (subgoal_tac "p ≠ 0")
apply (frule zdiv_zmult_self2, force)
by (insert p_g_2, auto)
qed;
moreover have "b ≤ q * a div p ==> p * b < q * a";
proof -;
assume "b ≤ q * a div p";
then have "p * b ≤ p * ((q * a) div p)";
by (insert p_g_2, auto simp add: mult_le_cancel_left);
also have "... ≤ q * a";
by (rule zdiv_leq_prop, insert p_g_2, auto)
finally have "p * b ≤ q * a" .;
then have "p * b < q * a | p * b = q * a";
by (simp only: order_le_imp_less_or_eq)
moreover have "p * b ≠ q * a";
by (rule  pb_neq_qa, insert prems, auto)
ultimately show ?thesis by auto
qed;
ultimately show ?thesis ..;
qed;

lemma (in QRTEMP) aux1b: "[| 0 < a; a ≤ (p - 1) div 2;
0 < b; b ≤ (q - 1) div 2 |] ==>
(q * a < p * b) = (a ≤ p * b div q)";
proof -;
assume "0 < a" and "a ≤ (p - 1) div 2" and "0 < b" and "b ≤ (q - 1) div 2";
have "q * a < p * b ==> a ≤ p * b div q";
proof -;
assume "q * a < p * b";
then have "q * a ≤ p * b" by auto
then have "(q * a) div q ≤ (p * b) div q";
by (rule zdiv_mono1, insert q_g_2, auto)
then show "a ≤ (p * b) div q";
apply (subgoal_tac "q ≠ 0")
apply (frule zdiv_zmult_self2, force)
by (insert q_g_2, auto)
qed;
moreover have "a ≤ p * b div q ==> q * a < p * b";
proof -;
assume "a ≤ p * b div q";
then have "q * a ≤ q * ((p * b) div q)";
by (insert q_g_2, auto simp add: mult_le_cancel_left)
also have "... ≤ p * b";
by (rule zdiv_leq_prop, insert q_g_2, auto)
finally have "q * a ≤ p * b" .;
then have "q * a < p * b | q * a = p * b";
by (simp only: order_le_imp_less_or_eq)
moreover have "p * b ≠ q * a";
by (rule  pb_neq_qa, insert prems, auto)
ultimately show ?thesis by auto
qed;
ultimately show ?thesis ..;
qed;

lemma aux2: "[| p ∈ zprime; q ∈ zprime; 2 < p; 2 < q |] ==>
(q * ((p - 1) div 2)) div p ≤ (q - 1) div 2";
proof-;
assume "p ∈ zprime" and "q ∈ zprime" and "2 < p" and "2 < q";
(* Set up what's even and odd *)
then have "p ∈ zOdd & q ∈ zOdd";
then have even1: "(p - 1):zEven & (q - 1):zEven";
then have even2: "(2 * p):zEven & ((q - 1) * p):zEven";
then have even3: "(((q - 1) * p) + (2 * p)):zEven";
by (auto simp: EvenOdd2.even_plus_even)
(* using these prove it *)
from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)";
then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2";
apply (rule_tac x = "((p - 1) * q)" in even_div_2_l);
also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)";
by (auto simp add: even1 even_prod_div_2)
also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p";
by (auto simp add: even1 even2 even_prod_div_2 even_sum_div_2)
finally show ?thesis
apply (rule_tac x = " q * ((p - 1) div 2)" and
y = "(q - 1) div 2" in div_prop2);
by (insert prems, auto)
qed;

lemma (in QRTEMP) aux3a: "∀j ∈ P_set. int (card (f1 j)) =
(q * j) div p";
proof;
fix j;
assume j_fact: "j ∈ P_set";
have "int (card (f1 j)) = int (card {y. y ∈ Q_set &
y ≤ (q * j) div p})";
proof -;
have "finite (f1 j)";
proof -;
have "(f1 j) ⊆ S" by (auto simp add: f1_def)
with S_finite show ?thesis by (auto simp add: finite_subset)
qed;
moreover have "inj_on (%(x,y). y) (f1 j)";
by (auto simp add: f1_def inj_on_def)
ultimately have "card ((%(x,y). y) ` (f1 j)) = card  (f1 j)";
by (auto simp add: f1_def card_image)
moreover have "((%(x,y). y) ` (f1 j)) = {y. y ∈ Q_set &
y ≤ (q * j) div p}";
by (insert prems, auto simp add: f1_def S_def Q_set_def P_set_def
image_def)
ultimately show ?thesis by (auto simp add: f1_def)
qed;
also have "... = int (card {y. 0 < y & y ≤ (q * j) div p})";
proof -;
have "{y. y ∈ Q_set & y ≤ (q * j) div p} =
{y. 0 < y & y ≤ (q * j) div p}";
proof -;
fix x;
assume "0 < x" and "x ≤ q * j div p";
with j_fact P_set_def  have "j ≤ (p - 1) div 2"; by auto
with q_g_2; have "q * j ≤ q * ((p - 1) div 2)";
with p_g_2 have "q * j div p ≤ q * ((p - 1) div 2) div p";
also from prems have "... ≤ (q - 1) div 2";
apply simp apply (insert aux2) by (simp add: QRTEMP_def)
finally show "x ≤ (q - 1) div 2" by (insert prems, auto)
qed;
then show ?thesis by auto
qed;
also have "... = (q * j) div p";
proof -;
from j_fact P_set_def have "0 ≤ j" by auto
with q_g_2 have "q * 0 ≤ q * j"
by (auto simp only: mult_left_mono);
then have "0 ≤ q * j" by auto
then have "0 div p ≤ (q * j) div p";
apply (rule_tac a = 0 in zdiv_mono1)
by (insert p_g_2, auto)
also have "0 div p = 0" by auto
finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
qed;
finally show "int (card (f1 j)) = q * j div p" .;
qed;

lemma (in QRTEMP) aux3b: "∀j ∈ Q_set. int (card (f2 j)) = (p * j) div q";
proof;
fix j;
assume j_fact: "j ∈ Q_set";
have "int (card (f2 j)) = int (card {y. y ∈ P_set & y ≤ (p * j) div q})";
proof -;
have "finite (f2 j)";
proof -;
have "(f2 j) ⊆ S" by (auto simp add: f2_def)
with S_finite show ?thesis by (auto simp add: finite_subset)
qed;
moreover have "inj_on (%(x,y). x) (f2 j)";
by (auto simp add: f2_def inj_on_def)
ultimately have "card ((%(x,y). x) ` (f2 j)) = card  (f2 j)";
by (auto simp add: f2_def card_image)
moreover have "((%(x,y). x) ` (f2 j)) = {y. y ∈ P_set & y ≤ (p * j) div q}";
by (insert prems, auto simp add: f2_def S_def Q_set_def
P_set_def image_def)
ultimately show ?thesis by (auto simp add: f2_def)
qed;
also have "... = int (card {y. 0 < y & y ≤ (p * j) div q})";
proof -;
have "{y. y ∈ P_set & y ≤ (p * j) div q} =
{y. 0 < y & y ≤ (p * j) div q}";
proof -;
fix x;
assume "0 < x" and "x ≤ p * j div q";
with j_fact Q_set_def  have "j ≤ (q - 1) div 2"; by auto
with p_g_2; have "p * j ≤ p * ((q - 1) div 2)";
with q_g_2 have "p * j div q ≤ p * ((q - 1) div 2) div q";
also from prems have "... ≤ (p - 1) div 2";
by (auto simp add: aux2 QRTEMP_def)
finally show "x ≤ (p - 1) div 2" by (insert prems, auto)
qed;
then show ?thesis by auto
qed;
also have "... = (p * j) div q";
proof -;
from j_fact Q_set_def have "0 ≤ j" by auto
with p_g_2 have "p * 0 ≤ p * j" by (auto simp only: mult_left_mono);
then have "0 ≤ p * j" by auto
then have "0 div q ≤ (p * j) div q";
apply (rule_tac a = 0 in zdiv_mono1)
by (insert q_g_2, auto)
also have "0 div q = 0" by auto
finally show ?thesis by (auto simp add: card_bdd_int_set_l_le)
qed;
finally show "int (card (f2 j)) = p * j div q" .;
qed;

lemma (in QRTEMP) S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set";
proof -;
have "∀x ∈ P_set. finite (f1 x)";
proof;
fix x;
have "f1 x ⊆ S" by (auto simp add: f1_def)
with S_finite show "finite (f1 x)" by (auto simp add: finite_subset)
qed;
moreover have "(∀x ∈ P_set. ∀y ∈ P_set.
x ≠ y --> (f1 x) ∩ (f1 y) = {})";
moreover note P_set_finite;
ultimately have "int(card (UNION P_set f1)) =
setsum (%x. int(card (f1 x))) P_set";
apply (auto simp add: card_UN_disjoint int_setsum o_def);
done;
moreover have "S1 = UNION P_set f1";
by (auto simp add: f1_def S_def S1_def S2_def P_set_def Q_set_def aux1a)
ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set"
by auto
also have "... = setsum (%j. q * j div p) P_set";
proof -;
note aux3a
with  P_set_finite show ?thesis
apply (intro setsum_cong);
apply auto;
done;
qed;
finally show ?thesis .;
qed;

lemma (in QRTEMP) S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set";
proof -;
have "∀x ∈ Q_set. finite (f2 x)";
proof;
fix x;
have "f2 x ⊆ S" by (auto simp add: f2_def)
with S_finite show "finite (f2 x)" by (auto simp add: finite_subset)
qed;
moreover have "(∀x ∈ Q_set. ∀y ∈ Q_set.
x ≠ y --> (f2 x) ∩ (f2 y) = {})";
moreover note Q_set_finite;
ultimately have "int(card (UNION Q_set f2)) =
setsum (%x. int(card (f2 x))) Q_set";
apply (auto simp add: card_UN_disjoint int_setsum o_def);
done;
moreover have "S2 = UNION Q_set f2";
by (auto simp add: f2_def S_def S1_def S2_def P_set_def Q_set_def aux1b)
ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set"
by auto
also have "... = setsum (%j. p * j div q) Q_set";
proof -;
note aux3b;
with Q_set_finite show ?thesis
by (intro setsum_cong, auto);
qed;
finally show ?thesis .;
qed;

lemma (in QRTEMP) S1_carda: "int (card(S1)) =
setsum (%j. (j * q) div p) P_set";
by (auto simp add: S1_card zmult_ac)

lemma (in QRTEMP) S2_carda: "int (card(S2)) =
setsum (%j. (j * p) div q) Q_set";
by (auto simp add: S2_card zmult_ac)

lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
(setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)";
proof -;
have "(setsum (%j. (j * p) div q) Q_set) +
(setsum (%j. (j * q) div p) P_set) = int (card S2) + int (card S1)";
by (auto simp add: S1_carda S2_carda)
also have "... = int (card S1) + int (card S2)";
by auto
also have "... = ((p - 1) div 2) * ((q - 1) div 2)";
finally show ?thesis .;
qed;

lemma pq_prime_neq: "[| p ∈ zprime; q ∈ zprime; p ≠ q |] ==> (~[p = 0] (mod q))";
apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
apply (drule_tac x = q in allE)
apply (drule_tac x = p in allE)
by auto

lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) =
(-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
proof -;
from prems have "~([p = 0] (mod q))";
by (auto simp add: pq_prime_neq QRTEMP_def)
with prems have a1: "(Legendre p q) = (-1::int) ^
nat(setsum (%x. ((x * p) div q)) Q_set)";
apply (rule_tac p = q in  MainQRLemma)
by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
from prems have "~([q = 0] (mod p))";
apply (rule_tac p = q and q = p in pq_prime_neq)
by arith
with prems have a2: "(Legendre q p) =
(-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)";
apply (rule_tac p = p in  MainQRLemma)
by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
from a1 a2 have "(Legendre p q) * (Legendre q p) =
(-1::int) ^ nat(setsum (%x. ((x * p) div q)) Q_set) *
(-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)";
by auto
also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) +
nat(setsum (%x. ((x * q) div p)) P_set))";
also have "nat(setsum (%x. ((x * p) div q)) Q_set) +
nat(setsum (%x. ((x * q) div p)) P_set) =
nat((setsum (%x. ((x * p) div q)) Q_set) +
(setsum (%x. ((x * q) div p)) P_set))";
apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in
by (auto simp add: S1_carda [THEN sym] S2_carda [THEN sym])
also have "... = nat(((p - 1) div 2) * ((q - 1) div 2))";
finally show ?thesis .;
qed;

"[| p ∈ zOdd; p ∈ zprime; q ∈ zOdd; q ∈ zprime;
p ≠ q |]
==> (Legendre p q) * (Legendre q p) =
(-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))";
by (auto simp add: QRTEMP.QR_short zprime_zOdd_eq_grt_2 [THEN sym]
QRTEMP_def)

end
```

lemma setsum_const_mult:

`  finite A ==> (∑x∈A. c * f x) = c * setsum f A`

lemma QRLemma1:

```  GAUSS p a
==> a * setsum id {x. 0 < x ∧ x ≤ (p - 1) div 2} =
p * (∑x | 0 < x ∧ x ≤ (p - 1) div 2. x * a div p) +
setsum id
(StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
{x. x ≤ (p - 1) div 2}) +
setsum id
(StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
{x. (p - 1) div 2 < x})```

lemma QRLemma2:

```  GAUSS p a
==> setsum id {x. 0 < x ∧ x ≤ (p - 1) div 2} =
p * int (card (StandardRes p `
(%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
{x. (p - 1) div 2 < x})) -
setsum id
(StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
{x. (p - 1) div 2 < x}) +
setsum id
(StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
{x. x ≤ (p - 1) div 2})```

lemma QRLemma3:

```  GAUSS p a
==> (a - 1) * setsum id {x. 0 < x ∧ x ≤ (p - 1) div 2} =
p * ((∑x | 0 < x ∧ x ≤ (p - 1) div 2. x * a div p) -
int (card (StandardRes p `
(%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
{x. (p - 1) div 2 < x}))) +
2 * setsum id
(StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
{x. (p - 1) div 2 < x})```

lemma QRLemma4:

```  [| GAUSS p a; a ∈ zOdd |]
==> ((∑x | 0 < x ∧ x ≤ (p - 1) div 2. x * a div p) ∈ zEven) =
(int (card (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
{x. (p - 1) div 2 < x}))
∈ zEven)```

lemma QRLemma5:

```  [| GAUSS p a; a ∈ zOdd |]
==> -1 ^
card (StandardRes p ` (%x. x * a) ` {x. 0 < x ∧ x ≤ (p - 1) div 2} ∩
{x. (p - 1) div 2 < x}) =
-1 ^ nat (∑x | 0 < x ∧ x ≤ (p - 1) div 2. x * a div p)```

lemma MainQRLemma:

```  [| a ∈ zOdd; 0 < a; ¬ [a = 0] (mod p); p ∈ zprime; 2 < p;
A = {x. 0 < x ∧ x ≤ (p - 1) div 2} |]
==> Legendre a p = -1 ^ nat (∑x∈A. x * a div p)```

lemma p_fact:

`  QRTEMP p q ==> 0 < (p - 1) div 2`

lemma q_fact:

`  QRTEMP p q ==> 0 < (q - 1) div 2`

lemma pb_neq_qa:

`  [| QRTEMP p q; 1 ≤ b; b ≤ (q - 1) div 2 |] ==> p * b ≠ q * a`

lemma P_set_finite:

`  QRTEMP p q ==> finite {x. 0 < x ∧ x ≤ (p - 1) div 2}`

lemma Q_set_finite:

`  QRTEMP p q ==> finite {x. 0 < x ∧ x ≤ (q - 1) div 2}`

lemma S_finite:

```  QRTEMP p q
==> finite ({x. 0 < x ∧ x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2})```

lemma S1_finite:

```  QRTEMP p q
==> finite
{(x, y).
(x, y) ∈ {x. 0 < x ∧ x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
p * y < q * x}```

lemma S2_finite:

```  QRTEMP p q
==> finite
{(x, y).
(x, y) ∈ {x. 0 < x ∧ x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
q * x < p * y}```

lemma P_set_card:

`  QRTEMP p q ==> (p - 1) div 2 = int (card {x. 0 < x ∧ x ≤ (p - 1) div 2})`

lemma Q_set_card:

`  QRTEMP p q ==> (q - 1) div 2 = int (card {x. 0 < x ∧ x ≤ (q - 1) div 2})`

lemma S_card:

```  QRTEMP p q
==> (p - 1) div 2 * ((q - 1) div 2) =
int (card ({x. 0 < x ∧ x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2}))```

lemma S1_Int_S2_prop:

```  QRTEMP p q
==> {(x, y).
(x, y) ∈ {x. 0 < x ∧ x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
p * y < q * x} ∩
{(x, y).
(x, y) ∈ {x. 0 < x ∧ x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
q * x < p * y} =
{}```

lemma S1_Union_S2_prop:

```  QRTEMP p q
==> {x. 0 < x ∧ x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} =
{(x, y).
(x, y) ∈ {x. 0 < x ∧ x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
p * y < q * x} ∪
{(x, y).
(x, y) ∈ {x. 0 < x ∧ x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
q * x < p * y}```

lemma card_sum_S1_S2:

```  QRTEMP p q
==> (p - 1) div 2 * ((q - 1) div 2) =
int (card {(x, y).
(x, y)
∈ {x. 0 < x ∧
x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
p * y < q * x}) +
int (card {(x, y).
(x, y)
∈ {x. 0 < x ∧
x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
q * x < p * y})```

lemma aux1a:

```  [| QRTEMP p q; 0 < a; a ≤ (p - 1) div 2; 0 < b; b ≤ (q - 1) div 2 |]
==> (p * b < q * a) = (b ≤ q * a div p)```

lemma aux1b:

```  [| QRTEMP p q; 0 < a; a ≤ (p - 1) div 2; 0 < b; b ≤ (q - 1) div 2 |]
==> (q * a < p * b) = (a ≤ p * b div q)```

lemma aux2:

```  [| p ∈ zprime; q ∈ zprime; 2 < p; 2 < q |]
==> q * ((p - 1) div 2) div p ≤ (q - 1) div 2```

lemma aux3a:

```  QRTEMP p q
==> ∀j∈{x. 0 < x ∧ x ≤ (p - 1) div 2}.
int (card {(j1, y).
(j1, y)
∈ {x. 0 < x ∧
x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
j1 = j ∧ y ≤ q * j div p}) =
q * j div p```

lemma aux3b:

```  QRTEMP p q
==> ∀j∈{x. 0 < x ∧ x ≤ (q - 1) div 2}.
int (card {(x, j1).
(x, j1)
∈ {x. 0 < x ∧
x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
j1 = j ∧ x ≤ p * j div q}) =
p * j div q```

lemma S1_card:

```  QRTEMP p q
==> int (card {(x, y).
(x, y)
∈ {x. 0 < x ∧
x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
p * y < q * x}) =
(∑j∈{x. 0 < x ∧ x ≤ (p - 1) div 2}. q * j div p)```

lemma S2_card:

```  QRTEMP p q
==> int (card {(x, y).
(x, y)
∈ {x. 0 < x ∧
x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
q * x < p * y}) =
(∑j∈{x. 0 < x ∧ x ≤ (q - 1) div 2}. p * j div q)```

lemma S1_carda:

```  QRTEMP p q
==> int (card {(x, y).
(x, y)
∈ {x. 0 < x ∧
x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
p * y < q * x}) =
(∑j∈{x. 0 < x ∧ x ≤ (p - 1) div 2}. j * q div p)```

lemma S2_carda:

```  QRTEMP p q
==> int (card {(x, y).
(x, y)
∈ {x. 0 < x ∧
x ≤ (p - 1) div 2} × {x. 0 < x ∧ x ≤ (q - 1) div 2} ∧
q * x < p * y}) =
(∑j∈{x. 0 < x ∧ x ≤ (q - 1) div 2}. j * p div q)```

lemma pq_sum_prop:

```  QRTEMP p q
==> (∑j∈{x. 0 < x ∧ x ≤ (q - 1) div 2}. j * p div q) +
(∑j∈{x. 0 < x ∧ x ≤ (p - 1) div 2}. j * q div p) =
(p - 1) div 2 * ((q - 1) div 2)```

lemma pq_prime_neq:

`  [| p ∈ zprime; q ∈ zprime; p ≠ q |] ==> ¬ [p = 0] (mod q)`

lemma QR_short:

```  QRTEMP p q
==> Legendre p q * Legendre q p = -1 ^ nat ((p - 1) div 2 * ((q - 1) div 2))```

```  [| p ∈ zOdd; p ∈ zprime; q ∈ zOdd; q ∈ zprime; p ≠ q |]