author | nipkow |
Mon, 21 Feb 2005 18:04:28 +0100 | |
changeset 15541 | 206d779ba96d |
parent 15537 | 5538d3244b4d |
child 16663 | 13e9c402308b |
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) |
|
15537 | 127 |
show "\<forall>x \<in> A. 0 \<le> x * a div p" |
15392 | 128 |
proof |
129 |
fix x |
|
130 |
assume "x \<in> A" |
|
131 |
then have "0 \<le> x" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
132 |
by (auto simp add: A_def) |
15392 | 133 |
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
|
134 |
by (auto simp add: zero_le_mult_iff) |
15392 | 135 |
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
|
136 |
by (auto simp add: pos_imp_zdiv_nonneg_iff) |
15392 | 137 |
qed |
138 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
139 |
ultimately have "(-1::int)^nat((int (card E))) = |
15392 | 140 |
(-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
|
141 |
by (intro neg_one_power_parity, auto) |
15392 | 142 |
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
|
143 |
by auto |
15392 | 144 |
finally show ?thesis . |
145 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
146 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
147 |
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
|
148 |
A = {x. 0 < x & x \<le> (p - 1) div 2} |] ==> |
15392 | 149 |
(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
|
150 |
apply (subst GAUSS.gauss_lemma) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
151 |
apply (auto simp add: GAUSS_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
152 |
apply (subst GAUSS.QRLemma5) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
153 |
by (auto simp add: GAUSS_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
154 |
|
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 |
(* Stuff about S, S1 and S2... *) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
158 |
(* *) |
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 |
locale QRTEMP = |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
162 |
fixes p :: "int" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
163 |
fixes q :: "int" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
164 |
fixes P_set :: "int set" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
165 |
fixes Q_set :: "int set" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
166 |
fixes S :: "(int * int) set" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
167 |
fixes S1 :: "(int * int) set" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
168 |
fixes S2 :: "(int * int) set" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
169 |
fixes f1 :: "int => (int * int) set" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
170 |
fixes f2 :: "int => (int * int) set" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
171 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
172 |
assumes p_prime: "p \<in> zprime" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
173 |
assumes p_g_2: "2 < p" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
174 |
assumes q_prime: "q \<in> zprime" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
175 |
assumes q_g_2: "2 < q" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
176 |
assumes p_neq_q: "p \<noteq> q" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
177 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
178 |
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
|
179 |
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
|
180 |
defines S_def: "S == P_set <*> Q_set" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
181 |
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
|
182 |
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
|
183 |
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
|
184 |
(y \<le> (q * j) div p) }" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
185 |
defines f2_def: "f2 j == { (x, j1). (x, j1):S & j1 = j & |
15392 | 186 |
(x \<le> (p * j) div q) }" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
187 |
|
15392 | 188 |
lemma (in QRTEMP) p_fact: "0 < (p - 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 < p" 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> p - 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> (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
|
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 |
|
15392 | 196 |
lemma (in QRTEMP) q_fact: "0 < (q - 1) div 2" |
197 |
proof - |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
198 |
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
|
199 |
then have "2 \<le> q - 1" by arith |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
200 |
then have "2 div 2 \<le> (q - 1) div 2" by (rule zdiv_mono1, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
201 |
then show ?thesis by auto |
15392 | 202 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
203 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
204 |
lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==> |
15392 | 205 |
(p * b \<noteq> q * a)" |
206 |
proof |
|
207 |
assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
208 |
then have "q dvd (p * b)" by (auto simp add: dvd_def) |
15392 | 209 |
with q_prime p_g_2 have "q dvd p | q dvd b" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
210 |
by (auto simp add: zprime_zdvd_zmult) |
15392 | 211 |
moreover have "~ (q dvd p)" |
212 |
proof |
|
213 |
assume "q dvd p" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
214 |
with p_prime have "q = 1 | q = p" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
215 |
apply (auto simp add: zprime_def QRTEMP_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
216 |
apply (drule_tac x = q and R = False in allE) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
217 |
apply (simp add: QRTEMP_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
218 |
apply (subgoal_tac "0 \<le> q", simp add: QRTEMP_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
219 |
apply (insert prems) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
220 |
by (auto simp add: QRTEMP_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
221 |
with q_g_2 p_neq_q show False by auto |
15392 | 222 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
223 |
ultimately have "q dvd b" by auto |
15392 | 224 |
then have "q \<le> b" |
225 |
proof - |
|
226 |
assume "q dvd b" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
227 |
moreover from prems have "0 < b" by auto |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
228 |
ultimately show ?thesis by (insert zdvd_bounds [of q b], auto) |
15392 | 229 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
230 |
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
|
231 |
then have "2 * q \<le> 2 * ((q - 1) div 2)" by arith |
15392 | 232 |
then have "2 * q \<le> q - 1" |
233 |
proof - |
|
234 |
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
|
235 |
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
|
236 |
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
|
237 |
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
|
238 |
with prems show ?thesis by auto |
15392 | 239 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
240 |
then have p1: "q \<le> -1" by arith |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
241 |
with q_g_2 show False by auto |
15392 | 242 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
243 |
|
15392 | 244 |
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
|
245 |
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
|
246 |
|
15392 | 247 |
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
|
248 |
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
|
249 |
|
15392 | 250 |
lemma (in QRTEMP) S_finite: "finite S" |
15402 | 251 |
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
|
252 |
|
15392 | 253 |
lemma (in QRTEMP) S1_finite: "finite S1" |
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 "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
|
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) S2_finite: "finite S2" |
261 |
proof - |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
262 |
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
|
263 |
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
|
264 |
ultimately show ?thesis by (auto simp add: finite_subset) |
15392 | 265 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
266 |
|
15392 | 267 |
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
|
268 |
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
|
269 |
|
15392 | 270 |
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
|
271 |
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
|
272 |
|
15392 | 273 |
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
|
274 |
apply (insert P_set_card Q_set_card P_set_finite Q_set_finite) |
15541 | 275 |
apply (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
|
276 |
done |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
277 |
|
15392 | 278 |
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
|
279 |
by (auto simp add: S1_def S2_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
280 |
|
15392 | 281 |
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
|
282 |
apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def) |
15392 | 283 |
proof - |
284 |
fix a and b |
|
285 |
assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
286 |
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
|
287 |
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
|
288 |
ultimately show "p * b < q * a" by auto |
15392 | 289 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
290 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
291 |
lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) = |
15392 | 292 |
int(card(S1)) + int(card(S2))" |
293 |
proof- |
|
294 |
have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
295 |
by (auto simp add: S_card) |
15392 | 296 |
also have "... = int( card(S1) + card(S2))" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
297 |
apply (insert S1_finite S2_finite S1_Int_S2_prop S1_Union_S2_prop) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
298 |
apply (drule card_Un_disjoint, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
299 |
done |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
300 |
also have "... = int(card(S1)) + int(card(S2))" by auto |
15392 | 301 |
finally show ?thesis . |
302 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
303 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
304 |
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
|
305 |
0 < b; b \<le> (q - 1) div 2 |] ==> |
15392 | 306 |
(p * b < q * a) = (b \<le> q * a div p)" |
307 |
proof - |
|
308 |
assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2" |
|
309 |
have "p * b < q * a ==> b \<le> q * a div p" |
|
310 |
proof - |
|
311 |
assume "p * b < q * a" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
312 |
then have "p * b \<le> q * a" by auto |
15392 | 313 |
then have "(p * b) div p \<le> (q * a) div p" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
314 |
by (rule zdiv_mono1, insert p_g_2, auto) |
15392 | 315 |
then show "b \<le> (q * a) div p" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
316 |
apply (subgoal_tac "p \<noteq> 0") |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
317 |
apply (frule zdiv_zmult_self2, force) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
318 |
by (insert p_g_2, auto) |
15392 | 319 |
qed |
320 |
moreover have "b \<le> q * a div p ==> p * b < q * a" |
|
321 |
proof - |
|
322 |
assume "b \<le> q * a div p" |
|
323 |
then have "p * b \<le> p * ((q * a) div p)" |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14353
diff
changeset
|
324 |
by (insert p_g_2, auto simp add: mult_le_cancel_left) |
15392 | 325 |
also have "... \<le> q * a" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
326 |
by (rule zdiv_leq_prop, insert p_g_2, auto) |
15392 | 327 |
finally have "p * b \<le> q * a" . |
328 |
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
|
329 |
by (simp only: order_le_imp_less_or_eq) |
15392 | 330 |
moreover have "p * b \<noteq> q * a" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
331 |
by (rule pb_neq_qa, insert prems, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
332 |
ultimately show ?thesis by auto |
15392 | 333 |
qed |
334 |
ultimately show ?thesis .. |
|
335 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
336 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
337 |
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
|
338 |
0 < b; b \<le> (q - 1) div 2 |] ==> |
15392 | 339 |
(q * a < p * b) = (a \<le> p * b div q)" |
340 |
proof - |
|
341 |
assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2" |
|
342 |
have "q * a < p * b ==> a \<le> p * b div q" |
|
343 |
proof - |
|
344 |
assume "q * a < p * b" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
345 |
then have "q * a \<le> p * b" by auto |
15392 | 346 |
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
|
347 |
by (rule zdiv_mono1, insert q_g_2, auto) |
15392 | 348 |
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
|
349 |
apply (subgoal_tac "q \<noteq> 0") |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
350 |
apply (frule zdiv_zmult_self2, force) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
351 |
by (insert q_g_2, auto) |
15392 | 352 |
qed |
353 |
moreover have "a \<le> p * b div q ==> q * a < p * b" |
|
354 |
proof - |
|
355 |
assume "a \<le> p * b div q" |
|
356 |
then have "q * a \<le> q * ((p * b) div q)" |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14353
diff
changeset
|
357 |
by (insert q_g_2, auto simp add: mult_le_cancel_left) |
15392 | 358 |
also have "... \<le> p * b" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
359 |
by (rule zdiv_leq_prop, insert q_g_2, auto) |
15392 | 360 |
finally have "q * a \<le> p * b" . |
361 |
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
|
362 |
by (simp only: order_le_imp_less_or_eq) |
15392 | 363 |
moreover have "p * b \<noteq> q * a" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
364 |
by (rule pb_neq_qa, insert prems, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
365 |
ultimately show ?thesis by auto |
15392 | 366 |
qed |
367 |
ultimately show ?thesis .. |
|
368 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
369 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
370 |
lemma aux2: "[| p \<in> zprime; q \<in> zprime; 2 < p; 2 < q |] ==> |
15392 | 371 |
(q * ((p - 1) div 2)) div p \<le> (q - 1) div 2" |
372 |
proof- |
|
373 |
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
|
374 |
(* Set up what's even and odd *) |
15392 | 375 |
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
|
376 |
by (auto simp add: zprime_zOdd_eq_grt_2) |
15392 | 377 |
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
|
378 |
by (auto simp add: odd_minus_one_even) |
15392 | 379 |
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
|
380 |
by (auto simp add: zEven_def) |
15392 | 381 |
then have even3: "(((q - 1) * p) + (2 * p)):zEven" |
14434 | 382 |
by (auto simp: EvenOdd.even_plus_even) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
383 |
(* using these prove it *) |
15392 | 384 |
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
|
385 |
by (auto simp add: int_distrib) |
15392 | 386 |
then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2" |
387 |
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
|
388 |
by (auto simp add: even3, auto simp add: zmult_ac) |
15392 | 389 |
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
|
390 |
by (auto simp add: even1 even_prod_div_2) |
15392 | 391 |
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
|
392 |
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
|
393 |
finally show ?thesis |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
394 |
apply (rule_tac x = " q * ((p - 1) div 2)" and |
15392 | 395 |
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
|
396 |
by (insert prems, auto) |
15392 | 397 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
398 |
|
15392 | 399 |
lemma (in QRTEMP) aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p" |
400 |
proof |
|
401 |
fix j |
|
402 |
assume j_fact: "j \<in> P_set" |
|
403 |
have "int (card (f1 j)) = int (card {y. y \<in> Q_set & y \<le> (q * j) div p})" |
|
404 |
proof - |
|
405 |
have "finite (f1 j)" |
|
406 |
proof - |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
407 |
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
|
408 |
with S_finite show ?thesis by (auto simp add: finite_subset) |
15392 | 409 |
qed |
410 |
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
|
411 |
by (auto simp add: f1_def inj_on_def) |
15392 | 412 |
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
|
413 |
by (auto simp add: f1_def card_image) |
15392 | 414 |
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
|
415 |
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
|
416 |
image_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
417 |
ultimately show ?thesis by (auto simp add: f1_def) |
15392 | 418 |
qed |
419 |
also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})" |
|
420 |
proof - |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
421 |
have "{y. y \<in> Q_set & y \<le> (q * j) div p} = |
15392 | 422 |
{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
|
423 |
apply (auto simp add: Q_set_def) |
15392 | 424 |
proof - |
425 |
fix x |
|
426 |
assume "0 < x" and "x \<le> q * j div p" |
|
427 |
with j_fact P_set_def have "j \<le> (p - 1) div 2" by auto |
|
428 |
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
|
429 |
by (auto simp add: mult_le_cancel_left) |
15392 | 430 |
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
|
431 |
by (auto simp add: zdiv_mono1) |
15392 | 432 |
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
|
433 |
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
|
434 |
finally show "x \<le> (q - 1) div 2" by (insert prems, auto) |
15392 | 435 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
436 |
then show ?thesis by auto |
15392 | 437 |
qed |
438 |
also have "... = (q * j) div p" |
|
439 |
proof - |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
440 |
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
|
441 |
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
|
442 |
then have "0 \<le> q * j" by auto |
15392 | 443 |
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
|
444 |
apply (rule_tac a = 0 in zdiv_mono1) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
445 |
by (insert p_g_2, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
446 |
also have "0 div p = 0" by auto |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
447 |
finally show ?thesis by (auto simp add: card_bdd_int_set_l_le) |
15392 | 448 |
qed |
449 |
finally show "int (card (f1 j)) = q * j div p" . |
|
450 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
451 |
|
15392 | 452 |
lemma (in QRTEMP) aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q" |
453 |
proof |
|
454 |
fix j |
|
455 |
assume j_fact: "j \<in> Q_set" |
|
456 |
have "int (card (f2 j)) = int (card {y. y \<in> P_set & y \<le> (p * j) div q})" |
|
457 |
proof - |
|
458 |
have "finite (f2 j)" |
|
459 |
proof - |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
460 |
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
|
461 |
with S_finite show ?thesis by (auto simp add: finite_subset) |
15392 | 462 |
qed |
463 |
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
|
464 |
by (auto simp add: f2_def inj_on_def) |
15392 | 465 |
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
|
466 |
by (auto simp add: f2_def card_image) |
15392 | 467 |
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
|
468 |
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
|
469 |
P_set_def image_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
470 |
ultimately show ?thesis by (auto simp add: f2_def) |
15392 | 471 |
qed |
472 |
also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})" |
|
473 |
proof - |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
474 |
have "{y. y \<in> P_set & y \<le> (p * j) div q} = |
15392 | 475 |
{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
|
476 |
apply (auto simp add: P_set_def) |
15392 | 477 |
proof - |
478 |
fix x |
|
479 |
assume "0 < x" and "x \<le> p * j div q" |
|
480 |
with j_fact Q_set_def have "j \<le> (q - 1) div 2" by auto |
|
481 |
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
|
482 |
by (auto simp add: mult_le_cancel_left) |
15392 | 483 |
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
|
484 |
by (auto simp add: zdiv_mono1) |
15392 | 485 |
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
|
486 |
by (auto simp add: aux2 QRTEMP_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
487 |
finally show "x \<le> (p - 1) div 2" by (insert prems, auto) |
15392 | 488 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
489 |
then show ?thesis by auto |
15392 | 490 |
qed |
491 |
also have "... = (p * j) div q" |
|
492 |
proof - |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
493 |
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
|
494 |
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
|
495 |
then have "0 \<le> p * j" by auto |
15392 | 496 |
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
|
497 |
apply (rule_tac a = 0 in zdiv_mono1) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
498 |
by (insert q_g_2, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
499 |
also have "0 div q = 0" by auto |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
500 |
finally show ?thesis by (auto simp add: card_bdd_int_set_l_le) |
15392 | 501 |
qed |
502 |
finally show "int (card (f2 j)) = p * j div q" . |
|
503 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
504 |
|
15392 | 505 |
lemma (in QRTEMP) S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set" |
506 |
proof - |
|
507 |
have "\<forall>x \<in> P_set. finite (f1 x)" |
|
508 |
proof |
|
509 |
fix x |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
510 |
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
|
511 |
with S_finite show "finite (f1 x)" by (auto simp add: finite_subset) |
15392 | 512 |
qed |
513 |
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
|
514 |
by (auto simp add: f1_def) |
15392 | 515 |
moreover note P_set_finite |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
516 |
ultimately have "int(card (UNION P_set f1)) = |
15392 | 517 |
setsum (%x. int(card (f1 x))) P_set" |
15402 | 518 |
by(simp add:card_UN_disjoint int_setsum o_def) |
15392 | 519 |
moreover have "S1 = UNION P_set f1" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
520 |
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
|
521 |
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
|
522 |
by auto |
15392 | 523 |
also have "... = setsum (%j. q * j div p) P_set" |
524 |
using aux3a by(fastsimp intro: setsum_cong) |
|
525 |
finally show ?thesis . |
|
526 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
527 |
|
15392 | 528 |
lemma (in QRTEMP) S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set" |
529 |
proof - |
|
530 |
have "\<forall>x \<in> Q_set. finite (f2 x)" |
|
531 |
proof |
|
532 |
fix x |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
533 |
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
|
534 |
with S_finite show "finite (f2 x)" by (auto simp add: finite_subset) |
15392 | 535 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
536 |
moreover have "(\<forall>x \<in> Q_set. \<forall>y \<in> Q_set. x \<noteq> y --> |
15392 | 537 |
(f2 x) \<inter> (f2 y) = {})" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
538 |
by (auto simp add: f2_def) |
15392 | 539 |
moreover note Q_set_finite |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
540 |
ultimately have "int(card (UNION Q_set f2)) = |
15392 | 541 |
setsum (%x. int(card (f2 x))) Q_set" |
15402 | 542 |
by(simp add:card_UN_disjoint int_setsum o_def) |
15392 | 543 |
moreover have "S2 = UNION Q_set f2" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
544 |
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
|
545 |
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
|
546 |
by auto |
15392 | 547 |
also have "... = setsum (%j. p * j div q) Q_set" |
548 |
using aux3b by(fastsimp intro: setsum_cong) |
|
549 |
finally show ?thesis . |
|
550 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
551 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
552 |
lemma (in QRTEMP) S1_carda: "int (card(S1)) = |
15392 | 553 |
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
|
554 |
by (auto simp add: S1_card zmult_ac) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
555 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
556 |
lemma (in QRTEMP) S2_carda: "int (card(S2)) = |
15392 | 557 |
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
|
558 |
by (auto simp add: S2_card zmult_ac) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
559 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
560 |
lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) + |
15392 | 561 |
(setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)" |
562 |
proof - |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
563 |
have "(setsum (%j. (j * p) div q) Q_set) + |
15392 | 564 |
(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
|
565 |
by (auto simp add: S1_carda S2_carda) |
15392 | 566 |
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
|
567 |
by auto |
15392 | 568 |
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
|
569 |
by (auto simp add: card_sum_S1_S2) |
15392 | 570 |
finally show ?thesis . |
571 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
572 |
|
15392 | 573 |
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
|
574 |
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
|
575 |
apply (drule_tac x = q in allE) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
576 |
apply (drule_tac x = p in allE) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
577 |
by auto |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
578 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
579 |
lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) = |
15392 | 580 |
(-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))" |
581 |
proof - |
|
582 |
from prems have "~([p = 0] (mod q))" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
583 |
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
|
584 |
with prems have a1: "(Legendre p q) = (-1::int) ^ |
15392 | 585 |
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
|
586 |
apply (rule_tac p = q in MainQRLemma) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
587 |
by (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def) |
15392 | 588 |
from prems have "~([q = 0] (mod p))" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
589 |
apply (rule_tac p = q and q = p in pq_prime_neq) |
15392 | 590 |
apply (simp add: QRTEMP_def)+ |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
591 |
by arith |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
592 |
with prems have a2: "(Legendre q p) = |
15392 | 593 |
(-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
|
594 |
apply (rule_tac p = p in MainQRLemma) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
595 |
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
|
596 |
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
|
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 |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
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) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
603 |
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
|
604 |
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
|
605 |
nat((setsum (%x. ((x * p) div q)) Q_set) + |
15392 | 606 |
(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
|
607 |
apply (rule_tac z1 = "setsum (%x. ((x * p) div q)) Q_set" in |
15392 | 608 |
nat_add_distrib [THEN sym]) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
609 |
by (auto simp add: S1_carda [THEN sym] S2_carda [THEN sym]) |
15392 | 610 |
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
|
611 |
by (auto simp add: pq_sum_prop) |
15392 | 612 |
finally show ?thesis . |
613 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
614 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
615 |
theorem Quadratic_Reciprocity: |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
616 |
"[| 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
|
617 |
p \<noteq> q |] |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
618 |
==> (Legendre p q) * (Legendre q p) = |
15392 | 619 |
(-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
|
620 |
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
|
621 |
QRTEMP_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
622 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
623 |
end |