author | wenzelm |
Fri, 10 Nov 2006 10:42:28 +0100 | |
changeset 21288 | 2c7d3d120418 |
parent 21233 | 5a5c8ea5f66a |
child 21404 | eb85850d3eb7 |
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/Gauss.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 {* Gauss' Lemma *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
7 |
|
18369 | 8 |
theory Gauss imports Euler begin |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
9 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
10 |
locale GAUSS = |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
11 |
fixes p :: "int" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
12 |
fixes a :: "int" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
13 |
|
16663 | 14 |
assumes p_prime: "zprime p" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
15 |
assumes p_g_2: "2 < p" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
16 |
assumes p_a_relprime: "~[a = 0](mod p)" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
17 |
assumes a_nonzero: "0 < a" |
21233 | 18 |
begin |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
19 |
|
21233 | 20 |
definition |
21 |
A :: "int set" |
|
22 |
"A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}" |
|
23 |
||
24 |
B :: "int set" |
|
25 |
"B = (%x. x * a) ` A" |
|
26 |
||
27 |
C :: "int set" |
|
28 |
"C = StandardRes p ` B" |
|
29 |
||
30 |
D :: "int set" |
|
31 |
"D = C \<inter> {x. x \<le> ((p - 1) div 2)}" |
|
32 |
||
33 |
E :: "int set" |
|
34 |
"E = C \<inter> {x. ((p - 1) div 2) < x}" |
|
35 |
||
36 |
F :: "int set" |
|
37 |
"F = (%x. (p - x)) ` E" |
|
38 |
||
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
39 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
40 |
subsection {* Basic properties of p *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
41 |
|
21233 | 42 |
lemma p_odd: "p \<in> zOdd" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
43 |
by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
44 |
|
21233 | 45 |
lemma p_g_0: "0 < p" |
18369 | 46 |
using p_g_2 by auto |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
47 |
|
21233 | 48 |
lemma int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2" |
18369 | 49 |
using insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
50 |
|
21233 | 51 |
lemma p_minus_one_l: "(p - 1) div 2 < p" |
18369 | 52 |
proof - |
53 |
have "(p - 1) div 2 \<le> (p - 1) div 1" |
|
54 |
by (rule zdiv_mono2) (auto simp add: p_g_0) |
|
55 |
also have "\<dots> = p - 1" by simp |
|
56 |
finally show ?thesis by simp |
|
57 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
58 |
|
21233 | 59 |
lemma p_eq: "p = (2 * (p - 1) div 2) + 1" |
18369 | 60 |
using zdiv_zmult_self2 [of 2 "p - 1"] by auto |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
61 |
|
21233 | 62 |
|
21288 | 63 |
lemma (in -) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
64 |
apply (frule odd_minus_one_even) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
65 |
apply (simp add: zEven_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
66 |
apply (subgoal_tac "2 \<noteq> 0") |
18369 | 67 |
apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2) |
68 |
apply (auto simp add: even_div_2_prop2) |
|
69 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
70 |
|
21233 | 71 |
|
72 |
lemma p_eq2: "p = (2 * ((p - 1) div 2)) + 1" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
73 |
apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto) |
18369 | 74 |
apply (frule zodd_imp_zdiv_eq, auto) |
75 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
76 |
|
21233 | 77 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
78 |
subsection {* Basic Properties of the Gauss Sets *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
79 |
|
21233 | 80 |
lemma finite_A: "finite (A)" |
18369 | 81 |
apply (auto simp add: A_def) |
82 |
apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}") |
|
83 |
apply (auto simp add: bdd_int_set_l_finite finite_subset) |
|
84 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
85 |
|
21233 | 86 |
lemma finite_B: "finite (B)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
87 |
by (auto simp add: B_def finite_A finite_imageI) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
88 |
|
21233 | 89 |
lemma finite_C: "finite (C)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
90 |
by (auto simp add: C_def finite_B finite_imageI) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
91 |
|
21233 | 92 |
lemma finite_D: "finite (D)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
93 |
by (auto simp add: D_def finite_Int finite_C) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
94 |
|
21233 | 95 |
lemma finite_E: "finite (E)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
96 |
by (auto simp add: E_def finite_Int finite_C) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
97 |
|
21233 | 98 |
lemma finite_F: "finite (F)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
99 |
by (auto simp add: F_def finite_E finite_imageI) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
100 |
|
21233 | 101 |
lemma C_eq: "C = D \<union> E" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
102 |
by (auto simp add: C_def D_def E_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
103 |
|
21233 | 104 |
lemma A_card_eq: "card A = nat ((p - 1) div 2)" |
18369 | 105 |
apply (auto simp add: A_def) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
106 |
apply (insert int_nat) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
107 |
apply (erule subst) |
18369 | 108 |
apply (auto simp add: card_bdd_int_set_l_le) |
109 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
110 |
|
21233 | 111 |
lemma inj_on_xa_A: "inj_on (%x. x * a) A" |
18369 | 112 |
using a_nonzero by (simp add: A_def inj_on_def) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
113 |
|
21233 | 114 |
lemma A_res: "ResSet p A" |
18369 | 115 |
apply (auto simp add: A_def ResSet_def) |
116 |
apply (rule_tac m = p in zcong_less_eq) |
|
117 |
apply (insert p_g_2, auto) |
|
118 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
119 |
|
21233 | 120 |
lemma B_res: "ResSet p B" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
121 |
apply (insert p_g_2 p_a_relprime p_minus_one_l) |
18369 | 122 |
apply (auto simp add: B_def) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
123 |
apply (rule ResSet_image) |
18369 | 124 |
apply (auto simp add: A_res) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
125 |
apply (auto simp add: A_def) |
18369 | 126 |
proof - |
127 |
fix x fix y |
|
128 |
assume a: "[x * a = y * a] (mod p)" |
|
129 |
assume b: "0 < x" |
|
130 |
assume c: "x \<le> (p - 1) div 2" |
|
131 |
assume d: "0 < y" |
|
132 |
assume e: "y \<le> (p - 1) div 2" |
|
133 |
from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] |
|
134 |
have "[x = y](mod p)" |
|
135 |
by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) |
|
136 |
with zcong_less_eq [of x y p] p_minus_one_l |
|
137 |
order_le_less_trans [of x "(p - 1) div 2" p] |
|
138 |
order_le_less_trans [of y "(p - 1) div 2" p] show "x = y" |
|
139 |
by (simp add: prems p_minus_one_l p_g_0) |
|
140 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
141 |
|
21233 | 142 |
lemma SR_B_inj: "inj_on (StandardRes p) B" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
143 |
apply (auto simp add: B_def StandardRes_def inj_on_def A_def prems) |
18369 | 144 |
proof - |
145 |
fix x fix y |
|
146 |
assume a: "x * a mod p = y * a mod p" |
|
147 |
assume b: "0 < x" |
|
148 |
assume c: "x \<le> (p - 1) div 2" |
|
149 |
assume d: "0 < y" |
|
150 |
assume e: "y \<le> (p - 1) div 2" |
|
151 |
assume f: "x \<noteq> y" |
|
152 |
from a have "[x * a = y * a](mod p)" |
|
153 |
by (simp add: zcong_zmod_eq p_g_0) |
|
154 |
with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] |
|
155 |
have "[x = y](mod p)" |
|
156 |
by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) |
|
157 |
with zcong_less_eq [of x y p] p_minus_one_l |
|
158 |
order_le_less_trans [of x "(p - 1) div 2" p] |
|
159 |
order_le_less_trans [of y "(p - 1) div 2" p] have "x = y" |
|
160 |
by (simp add: prems p_minus_one_l p_g_0) |
|
161 |
then have False |
|
162 |
by (simp add: f) |
|
163 |
then show "a = 0" |
|
164 |
by simp |
|
165 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
166 |
|
21233 | 167 |
lemma inj_on_pminusx_E: "inj_on (%x. p - x) E" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
168 |
apply (auto simp add: E_def C_def B_def A_def) |
18369 | 169 |
apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI) |
170 |
apply auto |
|
171 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
172 |
|
21233 | 173 |
lemma A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
174 |
apply (auto simp add: A_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
175 |
apply (frule_tac m = p in zcong_not_zero) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
176 |
apply (insert p_minus_one_l) |
18369 | 177 |
apply auto |
178 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
179 |
|
21233 | 180 |
lemma A_greater_zero: "x \<in> A ==> 0 < x" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
181 |
by (auto simp add: A_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
182 |
|
21233 | 183 |
lemma B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
184 |
apply (auto simp add: B_def) |
18369 | 185 |
apply (frule A_ncong_p) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
186 |
apply (insert p_a_relprime p_prime a_nonzero) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
187 |
apply (frule_tac a = x and b = a in zcong_zprime_prod_zero_contra) |
18369 | 188 |
apply (auto simp add: A_greater_zero) |
189 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
190 |
|
21233 | 191 |
lemma B_greater_zero: "x \<in> B ==> 0 < x" |
18369 | 192 |
using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
193 |
|
21233 | 194 |
lemma C_ncong_p: "x \<in> C ==> ~[x = 0](mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
195 |
apply (auto simp add: C_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
196 |
apply (frule B_ncong_p) |
18369 | 197 |
apply (subgoal_tac "[x = StandardRes p x](mod p)") |
198 |
defer apply (simp add: StandardRes_prop1) |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
199 |
apply (frule_tac a = x and b = "StandardRes p x" and c = 0 in zcong_trans) |
18369 | 200 |
apply auto |
201 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
202 |
|
21233 | 203 |
lemma C_greater_zero: "y \<in> C ==> 0 < y" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
204 |
apply (auto simp add: C_def) |
18369 | 205 |
proof - |
206 |
fix x |
|
207 |
assume a: "x \<in> B" |
|
208 |
from p_g_0 have "0 \<le> StandardRes p x" |
|
209 |
by (simp add: StandardRes_lbound) |
|
210 |
moreover have "~[x = 0] (mod p)" |
|
211 |
by (simp add: a B_ncong_p) |
|
212 |
then have "StandardRes p x \<noteq> 0" |
|
213 |
by (simp add: StandardRes_prop3) |
|
214 |
ultimately show "0 < StandardRes p x" |
|
215 |
by (simp add: order_le_less) |
|
216 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
217 |
|
21233 | 218 |
lemma D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
219 |
by (auto simp add: D_def C_ncong_p) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
220 |
|
21233 | 221 |
lemma E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
222 |
by (auto simp add: E_def C_ncong_p) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
223 |
|
21233 | 224 |
lemma F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)" |
18369 | 225 |
apply (auto simp add: F_def) |
226 |
proof - |
|
227 |
fix x assume a: "x \<in> E" assume b: "[p - x = 0] (mod p)" |
|
228 |
from E_ncong_p have "~[x = 0] (mod p)" |
|
229 |
by (simp add: a) |
|
230 |
moreover from a have "0 < x" |
|
231 |
by (simp add: a E_def C_greater_zero) |
|
232 |
moreover from a have "x < p" |
|
233 |
by (auto simp add: E_def C_def p_g_0 StandardRes_ubound) |
|
234 |
ultimately have "~[p - x = 0] (mod p)" |
|
235 |
by (simp add: zcong_not_zero) |
|
236 |
from this show False by (simp add: b) |
|
237 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
238 |
|
21233 | 239 |
lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}" |
18369 | 240 |
apply (auto simp add: F_def E_def) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
241 |
apply (insert p_g_0) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
242 |
apply (frule_tac x = xa in StandardRes_ubound) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
243 |
apply (frule_tac x = x in StandardRes_ubound) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
244 |
apply (subgoal_tac "xa = StandardRes p xa") |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
245 |
apply (auto simp add: C_def StandardRes_prop2 StandardRes_prop1) |
18369 | 246 |
proof - |
247 |
from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have |
|
248 |
"2 * (p - 1) div 2 = 2 * ((p - 1) div 2)" |
|
249 |
by simp |
|
250 |
with p_eq2 show " !!x. [| (p - 1) div 2 < StandardRes p x; x \<in> B |] |
|
251 |
==> p - StandardRes p x \<le> (p - 1) div 2" |
|
252 |
by simp |
|
253 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
254 |
|
21233 | 255 |
lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
256 |
by (auto simp add: D_def C_greater_zero) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
257 |
|
21233 | 258 |
lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
259 |
by (auto simp add: F_def E_def D_def C_def B_def A_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
260 |
|
21233 | 261 |
lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p - 1) div 2)}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
262 |
by (auto simp add: D_def C_def B_def A_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
263 |
|
21233 | 264 |
lemma D_leq: "x \<in> D ==> x \<le> (p - 1) div 2" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
265 |
by (auto simp add: D_eq) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
266 |
|
21233 | 267 |
lemma F_ge: "x \<in> F ==> x \<le> (p - 1) div 2" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
268 |
apply (auto simp add: F_eq A_def) |
18369 | 269 |
proof - |
270 |
fix y |
|
271 |
assume "(p - 1) div 2 < StandardRes p (y * a)" |
|
272 |
then have "p - StandardRes p (y * a) < p - ((p - 1) div 2)" |
|
273 |
by arith |
|
274 |
also from p_eq2 have "... = 2 * ((p - 1) div 2) + 1 - ((p - 1) div 2)" |
|
275 |
by auto |
|
276 |
also have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1" |
|
277 |
by arith |
|
278 |
finally show "p - StandardRes p (y * a) \<le> (p - 1) div 2" |
|
279 |
using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto |
|
280 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
281 |
|
21233 | 282 |
lemma all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1" |
18369 | 283 |
using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
284 |
|
21233 | 285 |
lemma A_prod_relprime: "zgcd((setprod id A),p) = 1" |
18369 | 286 |
using all_A_relprime finite_A by (simp add: all_relprime_prod_relprime) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
287 |
|
21233 | 288 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
289 |
subsection {* Relationships Between Gauss Sets *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
290 |
|
21233 | 291 |
lemma B_card_eq_A: "card B = card A" |
18369 | 292 |
using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
293 |
|
21233 | 294 |
lemma B_card_eq: "card B = nat ((p - 1) div 2)" |
18369 | 295 |
by (simp add: B_card_eq_A A_card_eq) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
296 |
|
21233 | 297 |
lemma F_card_eq_E: "card F = card E" |
18369 | 298 |
using finite_E by (simp add: F_def inj_on_pminusx_E card_image) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
299 |
|
21233 | 300 |
lemma C_card_eq_B: "card C = card B" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
301 |
apply (insert finite_B) |
18369 | 302 |
apply (subgoal_tac "inj_on (StandardRes p) B") |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
303 |
apply (simp add: B_def C_def card_image) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
304 |
apply (rule StandardRes_inj_on_ResSet) |
18369 | 305 |
apply (simp add: B_res) |
306 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
307 |
|
21233 | 308 |
lemma D_E_disj: "D \<inter> E = {}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
309 |
by (auto simp add: D_def E_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
310 |
|
21233 | 311 |
lemma C_card_eq_D_plus_E: "card C = card D + card E" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
312 |
by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
313 |
|
21233 | 314 |
lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
315 |
apply (insert D_E_disj finite_D finite_E C_eq) |
15392 | 316 |
apply (frule setprod_Un_disjoint [of D E id]) |
18369 | 317 |
apply auto |
318 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
319 |
|
21233 | 320 |
lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
321 |
apply (auto simp add: C_def) |
18369 | 322 |
apply (insert finite_B SR_B_inj) |
20898 | 323 |
apply (frule_tac f = "StandardRes p" in setprod_reindex_id [symmetric], auto) |
15392 | 324 |
apply (rule setprod_same_function_zcong) |
18369 | 325 |
apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0) |
326 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
327 |
|
21233 | 328 |
lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
329 |
apply (rule Un_least) |
18369 | 330 |
apply (auto simp add: A_def F_subset D_subset) |
331 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
332 |
|
21233 | 333 |
lemma F_D_disj: "(F \<inter> D) = {}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
334 |
apply (simp add: F_eq D_eq) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
335 |
apply (auto simp add: F_eq D_eq) |
18369 | 336 |
proof - |
337 |
fix y fix ya |
|
338 |
assume "p - StandardRes p (y * a) = StandardRes p (ya * a)" |
|
339 |
then have "p = StandardRes p (y * a) + StandardRes p (ya * a)" |
|
340 |
by arith |
|
341 |
moreover have "p dvd p" |
|
342 |
by auto |
|
343 |
ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))" |
|
344 |
by auto |
|
345 |
then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)" |
|
346 |
by (auto simp add: zcong_def) |
|
347 |
have "[y * a = StandardRes p (y * a)] (mod p)" |
|
348 |
by (simp only: zcong_sym StandardRes_prop1) |
|
349 |
moreover have "[ya * a = StandardRes p (ya * a)] (mod p)" |
|
350 |
by (simp only: zcong_sym StandardRes_prop1) |
|
351 |
ultimately have "[y * a + ya * a = |
|
352 |
StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)" |
|
353 |
by (rule zcong_zadd) |
|
354 |
with a have "[y * a + ya * a = 0] (mod p)" |
|
355 |
apply (elim zcong_trans) |
|
356 |
by (simp only: zcong_refl) |
|
357 |
also have "y * a + ya * a = a * (y + ya)" |
|
358 |
by (simp add: zadd_zmult_distrib2 zmult_commute) |
|
359 |
finally have "[a * (y + ya) = 0] (mod p)" . |
|
360 |
with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"] |
|
361 |
p_a_relprime |
|
362 |
have a: "[y + ya = 0] (mod p)" |
|
363 |
by auto |
|
364 |
assume b: "y \<in> A" and c: "ya: A" |
|
365 |
with A_def have "0 < y + ya" |
|
366 |
by auto |
|
367 |
moreover from b c A_def have "y + ya \<le> (p - 1) div 2 + (p - 1) div 2" |
|
368 |
by auto |
|
369 |
moreover from b c p_eq2 A_def have "y + ya < p" |
|
370 |
by auto |
|
371 |
ultimately show False |
|
372 |
apply simp |
|
373 |
apply (frule_tac m = p in zcong_not_zero) |
|
374 |
apply (auto simp add: a) |
|
375 |
done |
|
376 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
377 |
|
21233 | 378 |
lemma F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)" |
18369 | 379 |
proof - |
380 |
have "card (F \<union> D) = card E + card D" |
|
381 |
by (auto simp add: finite_F finite_D F_D_disj |
|
382 |
card_Un_disjoint F_card_eq_E) |
|
383 |
then have "card (F \<union> D) = card C" |
|
384 |
by (simp add: C_card_eq_D_plus_E) |
|
385 |
from this show "card (F \<union> D) = nat ((p - 1) div 2)" |
|
386 |
by (simp add: C_card_eq_B B_card_eq) |
|
387 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
388 |
|
21233 | 389 |
lemma F_Un_D_eq_A: "F \<union> D = A" |
18369 | 390 |
using finite_A F_Un_D_subset A_card_eq F_Un_D_card by (auto simp add: card_seteq) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
391 |
|
21233 | 392 |
lemma prod_D_F_eq_prod_A: |
18369 | 393 |
"(setprod id D) * (setprod id F) = setprod id A" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
394 |
apply (insert F_D_disj finite_D finite_F) |
15392 | 395 |
apply (frule setprod_Un_disjoint [of F D id]) |
18369 | 396 |
apply (auto simp add: F_Un_D_eq_A) |
397 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
398 |
|
21233 | 399 |
lemma prod_F_zcong: |
18369 | 400 |
"[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)" |
401 |
proof - |
|
402 |
have "setprod id F = setprod id (op - p ` E)" |
|
403 |
by (auto simp add: F_def) |
|
404 |
then have "setprod id F = setprod (op - p) E" |
|
405 |
apply simp |
|
406 |
apply (insert finite_E inj_on_pminusx_E) |
|
407 |
apply (frule_tac f = "op - p" in setprod_reindex_id, auto) |
|
408 |
done |
|
409 |
then have one: |
|
410 |
"[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)" |
|
411 |
apply simp |
|
412 |
apply (insert p_g_0 finite_E) |
|
413 |
by (auto simp add: StandardRes_prod) |
|
414 |
moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)" |
|
415 |
apply clarify |
|
416 |
apply (insert zcong_id [of p]) |
|
417 |
apply (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto) |
|
418 |
done |
|
419 |
moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)" |
|
420 |
apply clarify |
|
421 |
apply (simp add: StandardRes_prop1 zcong_sym) |
|
422 |
done |
|
423 |
moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)" |
|
424 |
apply clarify |
|
425 |
apply (insert a b) |
|
426 |
apply (rule_tac b = "p - x" in zcong_trans, auto) |
|
427 |
done |
|
428 |
ultimately have c: |
|
429 |
"[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)" |
|
430 |
apply simp |
|
431 |
apply (insert finite_E p_g_0) |
|
432 |
apply (rule setprod_same_function_zcong |
|
433 |
[of E "StandardRes p o (op - p)" uminus p], auto) |
|
434 |
done |
|
435 |
then have two: "[setprod id F = setprod (uminus) E](mod p)" |
|
436 |
apply (insert one c) |
|
437 |
apply (rule zcong_trans [of "setprod id F" |
|
15392 | 438 |
"setprod (StandardRes p o op - p) E" p |
18369 | 439 |
"setprod uminus E"], auto) |
440 |
done |
|
441 |
also have "setprod uminus E = (setprod id E) * (-1)^(card E)" |
|
442 |
using finite_E by (induct set: Finites) auto |
|
443 |
then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)" |
|
444 |
by (simp add: zmult_commute) |
|
445 |
with two show ?thesis |
|
446 |
by simp |
|
15392 | 447 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
448 |
|
21233 | 449 |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
450 |
subsection {* Gauss' Lemma *} |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
451 |
|
21233 | 452 |
lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
453 |
by (auto simp add: finite_E neg_one_special) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
454 |
|
21233 | 455 |
theorem pre_gauss_lemma: |
18369 | 456 |
"[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)" |
457 |
proof - |
|
458 |
have "[setprod id A = setprod id F * setprod id D](mod p)" |
|
459 |
by (auto simp add: prod_D_F_eq_prod_A zmult_commute) |
|
460 |
then have "[setprod id A = ((-1)^(card E) * setprod id E) * |
|
461 |
setprod id D] (mod p)" |
|
462 |
apply (rule zcong_trans) |
|
463 |
apply (auto simp add: prod_F_zcong zcong_scalar) |
|
464 |
done |
|
465 |
then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)" |
|
466 |
apply (rule zcong_trans) |
|
467 |
apply (insert C_prod_eq_D_times_E, erule subst) |
|
468 |
apply (subst zmult_assoc, auto) |
|
469 |
done |
|
470 |
then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)" |
|
471 |
apply (rule zcong_trans) |
|
472 |
apply (simp add: C_B_zcong_prod zcong_scalar2) |
|
473 |
done |
|
474 |
then have "[setprod id A = ((-1)^(card E) * |
|
475 |
(setprod id ((%x. x * a) ` A)))] (mod p)" |
|
476 |
by (simp add: B_def) |
|
477 |
then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))] |
|
478 |
(mod p)" |
|
479 |
by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric]) |
|
480 |
moreover have "setprod (%x. x * a) A = |
|
481 |
setprod (%x. a) A * setprod id A" |
|
482 |
using finite_A by (induct set: Finites) auto |
|
483 |
ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A * |
|
484 |
setprod id A))] (mod p)" |
|
485 |
by simp |
|
486 |
then have "[setprod id A = ((-1)^(card E) * a^(card A) * |
|
487 |
setprod id A)](mod p)" |
|
488 |
apply (rule zcong_trans) |
|
489 |
apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant zmult_assoc) |
|
490 |
done |
|
491 |
then have a: "[setprod id A * (-1)^(card E) = |
|
492 |
((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)" |
|
493 |
by (rule zcong_scalar) |
|
494 |
then have "[setprod id A * (-1)^(card E) = setprod id A * |
|
495 |
(-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)" |
|
496 |
apply (rule zcong_trans) |
|
497 |
apply (simp add: a mult_commute mult_left_commute) |
|
498 |
done |
|
499 |
then have "[setprod id A * (-1)^(card E) = setprod id A * |
|
500 |
a^(card A)](mod p)" |
|
501 |
apply (rule zcong_trans) |
|
502 |
apply (simp add: aux) |
|
503 |
done |
|
504 |
with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"] |
|
505 |
p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)" |
|
506 |
by (simp add: order_less_imp_le) |
|
507 |
from this show ?thesis |
|
508 |
by (simp add: A_card_eq zcong_sym) |
|
15392 | 509 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
510 |
|
21233 | 511 |
theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)" |
15392 | 512 |
proof - |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
513 |
from Euler_Criterion p_prime p_g_2 have |
18369 | 514 |
"[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
515 |
by auto |
15392 | 516 |
moreover note pre_gauss_lemma |
517 |
ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
518 |
by (rule zcong_trans) |
15392 | 519 |
moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
520 |
by (auto simp add: Legendre_def) |
15392 | 521 |
moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
522 |
by (rule neg_one_power) |
15392 | 523 |
ultimately show ?thesis |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
524 |
by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym) |
15392 | 525 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
526 |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16733
diff
changeset
|
527 |
end |
21233 | 528 |
|
529 |
end |