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