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