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