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