|
1 (* Authors: Jeremy Avigad, David Gray, and Adam Kramer |
|
2 |
|
3 Ported by lcp but unfinished |
|
4 *) |
|
5 |
|
6 header {* Gauss' Lemma *} |
|
7 |
|
8 theory Gauss |
|
9 imports Residues |
|
10 begin |
|
11 |
|
12 lemma cong_prime_prod_zero_nat: |
|
13 fixes a::nat |
|
14 shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)" |
|
15 by (auto simp add: cong_altdef_nat) |
|
16 |
|
17 lemma cong_prime_prod_zero_int: |
|
18 fixes a::int |
|
19 shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)" |
|
20 by (auto simp add: cong_altdef_int) |
|
21 |
|
22 |
|
23 locale GAUSS = |
|
24 fixes p :: "nat" |
|
25 fixes a :: "int" |
|
26 |
|
27 assumes p_prime: "prime p" |
|
28 assumes p_ge_2: "2 < p" |
|
29 assumes p_a_relprime: "[a \<noteq> 0](mod p)" |
|
30 assumes a_nonzero: "0 < a" |
|
31 begin |
|
32 |
|
33 definition "A = {0::int <.. ((int p - 1) div 2)}" |
|
34 definition "B = (\<lambda>x. x * a) ` A" |
|
35 definition "C = (\<lambda>x. x mod p) ` B" |
|
36 definition "D = C \<inter> {.. (int p - 1) div 2}" |
|
37 definition "E = C \<inter> {(int p - 1) div 2 <..}" |
|
38 definition "F = (\<lambda>x. (int p - x)) ` E" |
|
39 |
|
40 |
|
41 subsection {* Basic properties of p *} |
|
42 |
|
43 lemma odd_p: "odd p" |
|
44 by (metis p_prime p_ge_2 prime_odd_nat) |
|
45 |
|
46 lemma p_minus_one_l: "(int p - 1) div 2 < p" |
|
47 proof - |
|
48 have "(p - 1) div 2 \<le> (p - 1) div 1" |
|
49 by (metis div_by_1 div_le_dividend) |
|
50 also have "\<dots> = p - 1" by simp |
|
51 finally show ?thesis using p_ge_2 by arith |
|
52 qed |
|
53 |
|
54 lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1" |
|
55 using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"] |
|
56 by auto presburger |
|
57 |
|
58 lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z" |
|
59 using odd_p p_ge_2 |
|
60 by (auto simp add: even_def) (metis p_eq2) |
|
61 |
|
62 |
|
63 subsection {* Basic Properties of the Gauss Sets *} |
|
64 |
|
65 lemma finite_A: "finite (A)" |
|
66 by (auto simp add: A_def) |
|
67 |
|
68 lemma finite_B: "finite (B)" |
|
69 by (auto simp add: B_def finite_A) |
|
70 |
|
71 lemma finite_C: "finite (C)" |
|
72 by (auto simp add: C_def finite_B) |
|
73 |
|
74 lemma finite_D: "finite (D)" |
|
75 by (auto simp add: D_def finite_C) |
|
76 |
|
77 lemma finite_E: "finite (E)" |
|
78 by (auto simp add: E_def finite_C) |
|
79 |
|
80 lemma finite_F: "finite (F)" |
|
81 by (auto simp add: F_def finite_E) |
|
82 |
|
83 lemma C_eq: "C = D \<union> E" |
|
84 by (auto simp add: C_def D_def E_def) |
|
85 |
|
86 lemma A_card_eq: "card A = nat ((int p - 1) div 2)" |
|
87 by (auto simp add: A_def) |
|
88 |
|
89 lemma inj_on_xa_A: "inj_on (\<lambda>x. x * a) A" |
|
90 using a_nonzero by (simp add: A_def inj_on_def) |
|
91 |
|
92 definition ResSet :: "int => int set => bool" |
|
93 where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))" |
|
94 |
|
95 lemma ResSet_image: |
|
96 "\<lbrakk> 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) \<rbrakk> \<Longrightarrow> |
|
97 ResSet m (f ` A)" |
|
98 by (auto simp add: ResSet_def) |
|
99 |
|
100 lemma A_res: "ResSet p A" |
|
101 using p_ge_2 |
|
102 by (auto simp add: A_def ResSet_def intro!: cong_less_imp_eq_int) |
|
103 |
|
104 lemma B_res: "ResSet p B" |
|
105 proof - |
|
106 {fix x fix y |
|
107 assume a: "[x * a = y * a] (mod p)" |
|
108 assume b: "0 < x" |
|
109 assume c: "x \<le> (int p - 1) div 2" |
|
110 assume d: "0 < y" |
|
111 assume e: "y \<le> (int p - 1) div 2" |
|
112 from a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y] |
|
113 have "[x = y](mod p)" |
|
114 by (metis comm_monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int |
|
115 cong_mult_self_int gcd_int.commute prime_imp_coprime_int) |
|
116 with cong_less_imp_eq_int [of x y p] p_minus_one_l |
|
117 order_le_less_trans [of x "(int p - 1) div 2" p] |
|
118 order_le_less_trans [of y "(int p - 1) div 2" p] |
|
119 have "x = y" |
|
120 by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int) |
|
121 } note xy = this |
|
122 show ?thesis |
|
123 apply (insert p_ge_2 p_a_relprime p_minus_one_l) |
|
124 apply (auto simp add: B_def) |
|
125 apply (rule ResSet_image) |
|
126 apply (auto simp add: A_res) |
|
127 apply (auto simp add: A_def xy) |
|
128 done |
|
129 qed |
|
130 |
|
131 lemma SR_B_inj: "inj_on (\<lambda>x. x mod p) B" |
|
132 proof - |
|
133 { fix x fix y |
|
134 assume a: "x * a mod p = y * a mod p" |
|
135 assume b: "0 < x" |
|
136 assume c: "x \<le> (int p - 1) div 2" |
|
137 assume d: "0 < y" |
|
138 assume e: "y \<le> (int p - 1) div 2" |
|
139 assume f: "x \<noteq> y" |
|
140 from a have "[x * a = y * a](mod p)" |
|
141 by (metis cong_int_def) |
|
142 with p_a_relprime p_prime cong_mult_rcancel_int [of a p x y] |
|
143 have "[x = y](mod p)" |
|
144 by (metis cong_mult_self_int dvd_div_mult_self gcd_commute_int prime_imp_coprime_int) |
|
145 with cong_less_imp_eq_int [of x y p] p_minus_one_l |
|
146 order_le_less_trans [of x "(int p - 1) div 2" p] |
|
147 order_le_less_trans [of y "(int p - 1) div 2" p] |
|
148 have "x = y" |
|
149 by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int) |
|
150 then have False |
|
151 by (simp add: f)} |
|
152 then show ?thesis |
|
153 by (auto simp add: B_def inj_on_def A_def) metis |
|
154 qed |
|
155 |
|
156 lemma inj_on_pminusx_E: "inj_on (\<lambda>x. p - x) E" |
|
157 apply (auto simp add: E_def C_def B_def A_def) |
|
158 apply (rule_tac g = "(op - (int p))" in inj_on_inverseI) |
|
159 apply auto |
|
160 done |
|
161 |
|
162 lemma nonzero_mod_p: |
|
163 fixes x::int shows "\<lbrakk>0 < x; x < int p\<rbrakk> \<Longrightarrow> [x \<noteq> 0](mod p)" |
|
164 by (metis Nat_Transfer.transfer_nat_int_function_closures(9) cong_less_imp_eq_int |
|
165 inf.semilattice_strict_iff_order int_less_0_conv le_numeral_extra(3) zero_less_imp_eq_int) |
|
166 |
|
167 lemma A_ncong_p: "x \<in> A \<Longrightarrow> [x \<noteq> 0](mod p)" |
|
168 by (rule nonzero_mod_p) (auto simp add: A_def) |
|
169 |
|
170 lemma A_greater_zero: "x \<in> A \<Longrightarrow> 0 < x" |
|
171 by (auto simp add: A_def) |
|
172 |
|
173 lemma B_ncong_p: "x \<in> B \<Longrightarrow> [x \<noteq> 0](mod p)" |
|
174 by (auto simp add: B_def) (metis cong_prime_prod_zero_int A_ncong_p p_a_relprime p_prime) |
|
175 |
|
176 lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x" |
|
177 using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero) |
|
178 |
|
179 lemma C_greater_zero: "y \<in> C \<Longrightarrow> 0 < y" |
|
180 proof (auto simp add: C_def) |
|
181 fix x :: int |
|
182 assume a1: "x \<in> B" |
|
183 have f2: "\<And>x\<^sub>1. int x\<^sub>1 = 0 \<or> 0 < int x\<^sub>1" by linarith |
|
184 have "x mod int p \<noteq> 0" using a1 B_ncong_p cong_int_def by simp |
|
185 thus "0 < x mod int p" using a1 f2 |
|
186 by (metis (no_types) B_greater_zero Divides.transfer_int_nat_functions(2) zero_less_imp_eq_int) |
|
187 qed |
|
188 |
|
189 lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((int p - 1) div 2)}" |
|
190 apply (auto simp add: F_def E_def C_def) |
|
191 apply (metis p_ge_2 Divides.pos_mod_bound less_diff_eq nat_int plus_int_code(2) zless_nat_conj) |
|
192 apply (auto intro: p_odd_int) |
|
193 done |
|
194 |
|
195 lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}" |
|
196 by (auto simp add: D_def C_greater_zero) |
|
197 |
|
198 lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - ((y*a) mod p) & (int p - 1) div 2 < (y*a) mod p)}" |
|
199 by (auto simp add: F_def E_def D_def C_def B_def A_def) |
|
200 |
|
201 lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = (y*a) mod p & (y*a) mod p \<le> (int p - 1) div 2)}" |
|
202 by (auto simp add: D_def C_def B_def A_def) |
|
203 |
|
204 lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1" |
|
205 using p_prime A_ncong_p [OF assms] |
|
206 by (simp add: cong_altdef_int) (metis gcd_int.commute prime_imp_coprime_int) |
|
207 |
|
208 lemma A_prod_relprime: "gcd (setprod id A) p = 1" |
|
209 by (metis DEADID.map_id all_A_relprime setprod_coprime_int) |
|
210 |
|
211 |
|
212 subsection {* Relationships Between Gauss Sets *} |
|
213 |
|
214 lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> (inj_on (\<lambda>b. b mod m) X)" |
|
215 by (auto simp add: ResSet_def inj_on_def cong_int_def) |
|
216 |
|
217 lemma B_card_eq_A: "card B = card A" |
|
218 using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image) |
|
219 |
|
220 lemma B_card_eq: "card B = nat ((int p - 1) div 2)" |
|
221 by (simp add: B_card_eq_A A_card_eq) |
|
222 |
|
223 lemma F_card_eq_E: "card F = card E" |
|
224 using finite_E |
|
225 by (simp add: F_def inj_on_pminusx_E card_image) |
|
226 |
|
227 lemma C_card_eq_B: "card C = card B" |
|
228 proof - |
|
229 have "inj_on (\<lambda>x. x mod p) B" |
|
230 by (metis SR_B_inj) |
|
231 then show ?thesis |
|
232 by (metis C_def card_image) |
|
233 qed |
|
234 |
|
235 lemma D_E_disj: "D \<inter> E = {}" |
|
236 by (auto simp add: D_def E_def) |
|
237 |
|
238 lemma C_card_eq_D_plus_E: "card C = card D + card E" |
|
239 by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E) |
|
240 |
|
241 lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C" |
|
242 by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod_Un_disjoint sup_commute) |
|
243 |
|
244 lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)" |
|
245 apply (auto simp add: C_def) |
|
246 apply (insert finite_B SR_B_inj) |
|
247 apply (frule_tac f = "\<lambda>x. x mod int p" in setprod_reindex_id [symmetric], auto) |
|
248 apply (rule cong_setprod_int) |
|
249 apply (auto simp add: cong_int_def) |
|
250 done |
|
251 |
|
252 lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A" |
|
253 apply (intro Un_least subset_trans [OF F_subset] subset_trans [OF D_subset]) |
|
254 apply (auto simp add: A_def) |
|
255 done |
|
256 |
|
257 lemma F_D_disj: "(F \<inter> D) = {}" |
|
258 proof (auto simp add: F_eq D_eq) |
|
259 fix y::int and z::int |
|
260 assume "p - (y*a) mod p = (z*a) mod p" |
|
261 then have "[(y*a) mod p + (z*a) mod p = 0] (mod p)" |
|
262 by (metis add_commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0) |
|
263 moreover have "[y * a = (y*a) mod p] (mod p)" |
|
264 by (metis cong_int_def mod_mod_trivial) |
|
265 ultimately have "[a * (y + z) = 0] (mod p)" |
|
266 by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult_commute ring_class.ring_distribs(1)) |
|
267 with p_prime a_nonzero p_a_relprime |
|
268 have a: "[y + z = 0] (mod p)" |
|
269 by (metis cong_prime_prod_zero_int) |
|
270 assume b: "y \<in> A" and c: "z \<in> A" |
|
271 with A_def have "0 < y + z" |
|
272 by auto |
|
273 moreover from b c p_eq2 A_def have "y + z < p" |
|
274 by auto |
|
275 ultimately show False |
|
276 by (metis a nonzero_mod_p) |
|
277 qed |
|
278 |
|
279 lemma F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)" |
|
280 proof - |
|
281 have "card (F \<union> D) = card E + card D" |
|
282 by (auto simp add: finite_F finite_D F_D_disj card_Un_disjoint F_card_eq_E) |
|
283 then have "card (F \<union> D) = card C" |
|
284 by (simp add: C_card_eq_D_plus_E) |
|
285 then show "card (F \<union> D) = nat ((p - 1) div 2)" |
|
286 by (simp add: C_card_eq_B B_card_eq) |
|
287 qed |
|
288 |
|
289 lemma F_Un_D_eq_A: "F \<union> D = A" |
|
290 using finite_A F_Un_D_subset A_card_eq F_Un_D_card |
|
291 by (auto simp add: card_seteq) |
|
292 |
|
293 lemma prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A" |
|
294 by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod_Un_disjoint) |
|
295 |
|
296 lemma prod_F_zcong: "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)" |
|
297 proof - |
|
298 have FE: "setprod id F = setprod (op - p) E" |
|
299 apply (auto simp add: F_def) |
|
300 apply (insert finite_E inj_on_pminusx_E) |
|
301 apply (frule setprod_reindex_id, auto) |
|
302 done |
|
303 then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)" |
|
304 by (metis cong_int_def minus_mod_self1 mod_mod_trivial) |
|
305 then have "[setprod ((\<lambda>x. x mod p) o (op - p)) E = setprod (uminus) E](mod p)" |
|
306 using finite_E p_ge_2 |
|
307 cong_setprod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p] |
|
308 by auto |
|
309 then have two: "[setprod id F = setprod (uminus) E](mod p)" |
|
310 by (metis FE cong_cong_mod_int cong_refl_int cong_setprod_int minus_mod_self1) |
|
311 have "setprod uminus E = (-1) ^ (card E) * (setprod id E)" |
|
312 using finite_E by (induct set: finite) auto |
|
313 with two show ?thesis |
|
314 by simp |
|
315 qed |
|
316 |
|
317 |
|
318 subsection {* Gauss' Lemma *} |
|
319 |
|
320 lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A" |
|
321 by (metis (no_types) minus_minus mult_commute mult_left_commute power_minus power_one) |
|
322 |
|
323 theorem pre_gauss_lemma: |
|
324 "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)" |
|
325 proof - |
|
326 have "[setprod id A = setprod id F * setprod id D](mod p)" |
|
327 by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod_cong) |
|
328 then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)" |
|
329 apply (rule cong_trans_int) |
|
330 apply (metis cong_scalar_int prod_F_zcong) |
|
331 done |
|
332 then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)" |
|
333 by (metis C_prod_eq_D_times_E mult_commute mult_left_commute) |
|
334 then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)" |
|
335 by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int) |
|
336 then have "[setprod id A = ((-1)^(card E) * |
|
337 (setprod id ((\<lambda>x. x * a) ` A)))] (mod p)" |
|
338 by (simp add: B_def) |
|
339 then have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. x * a) A))] |
|
340 (mod p)" |
|
341 by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong) |
|
342 moreover have "setprod (\<lambda>x. x * a) A = |
|
343 setprod (\<lambda>x. a) A * setprod id A" |
|
344 using finite_A by (induct set: finite) auto |
|
345 ultimately have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. a) A * |
|
346 setprod id A))] (mod p)" |
|
347 by simp |
|
348 then have "[setprod id A = ((-1)^(card E) * a^(card A) * |
|
349 setprod id A)](mod p)" |
|
350 apply (rule cong_trans_int) |
|
351 apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult_assoc) |
|
352 done |
|
353 then have a: "[setprod id A * (-1)^(card E) = |
|
354 ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)" |
|
355 by (rule cong_scalar_int) |
|
356 then have "[setprod id A * (-1)^(card E) = setprod id A * |
|
357 (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)" |
|
358 apply (rule cong_trans_int) |
|
359 apply (simp add: a mult_commute mult_left_commute) |
|
360 done |
|
361 then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)" |
|
362 apply (rule cong_trans_int) |
|
363 apply (simp add: aux cong del:setprod_cong) |
|
364 done |
|
365 with A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)" |
|
366 by (metis cong_mult_lcancel_int) |
|
367 then show ?thesis |
|
368 by (simp add: A_card_eq cong_sym_int) |
|
369 qed |
|
370 |
|
371 (*NOT WORKING. Old_Number_Theory/Euler.thy needs to be translated, but it's |
|
372 quite a mess and should better be completely redone. |
|
373 |
|
374 theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)" |
|
375 proof - |
|
376 from Euler_Criterion p_prime p_ge_2 have |
|
377 "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)" |
|
378 by auto |
|
379 moreover note pre_gauss_lemma |
|
380 ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)" |
|
381 by (rule cong_trans_int) |
|
382 moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)" |
|
383 by (auto simp add: Legendre_def) |
|
384 moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1" |
|
385 by (rule neg_one_power) |
|
386 ultimately show ?thesis |
|
387 by (auto simp add: p_ge_2 one_not_neg_one_mod_m zcong_sym) |
|
388 qed |
|
389 *) |
|
390 |
|
391 end |
|
392 |
|
393 end |