258 lemma F_D_disj: "(F \<inter> D) = {}" |
258 lemma F_D_disj: "(F \<inter> D) = {}" |
259 proof (auto simp add: F_eq D_eq) |
259 proof (auto simp add: F_eq D_eq) |
260 fix y::int and z::int |
260 fix y::int and z::int |
261 assume "p - (y*a) mod p = (z*a) mod p" |
261 assume "p - (y*a) mod p = (z*a) mod p" |
262 then have "[(y*a) mod p + (z*a) mod p = 0] (mod p)" |
262 then have "[(y*a) mod p + (z*a) mod p = 0] (mod p)" |
263 by (metis add_commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0) |
263 by (metis add.commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0) |
264 moreover have "[y * a = (y*a) mod p] (mod p)" |
264 moreover have "[y * a = (y*a) mod p] (mod p)" |
265 by (metis cong_int_def mod_mod_trivial) |
265 by (metis cong_int_def mod_mod_trivial) |
266 ultimately have "[a * (y + z) = 0] (mod p)" |
266 ultimately have "[a * (y + z) = 0] (mod p)" |
267 by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult_commute ring_class.ring_distribs(1)) |
267 by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1)) |
268 with p_prime a_nonzero p_a_relprime |
268 with p_prime a_nonzero p_a_relprime |
269 have a: "[y + z = 0] (mod p)" |
269 have a: "[y + z = 0] (mod p)" |
270 by (metis cong_prime_prod_zero_int) |
270 by (metis cong_prime_prod_zero_int) |
271 assume b: "y \<in> A" and c: "z \<in> A" |
271 assume b: "y \<in> A" and c: "z \<in> A" |
272 with A_def have "0 < y + z" |
272 with A_def have "0 < y + z" |
317 |
317 |
318 |
318 |
319 subsection {* Gauss' Lemma *} |
319 subsection {* Gauss' Lemma *} |
320 |
320 |
321 lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A" |
321 lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A" |
322 by (metis (no_types) minus_minus mult_commute mult_left_commute power_minus power_one) |
322 by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one) |
323 |
323 |
324 theorem pre_gauss_lemma: |
324 theorem pre_gauss_lemma: |
325 "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)" |
325 "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)" |
326 proof - |
326 proof - |
327 have "[setprod id A = setprod id F * setprod id D](mod p)" |
327 have "[setprod id A = setprod id F * setprod id D](mod p)" |
328 by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod.cong) |
328 by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del:setprod.cong) |
329 then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)" |
329 then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)" |
330 apply (rule cong_trans_int) |
330 apply (rule cong_trans_int) |
331 apply (metis cong_scalar_int prod_F_zcong) |
331 apply (metis cong_scalar_int prod_F_zcong) |
332 done |
332 done |
333 then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)" |
333 then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)" |
334 by (metis C_prod_eq_D_times_E mult_commute mult_left_commute) |
334 by (metis C_prod_eq_D_times_E mult.commute mult.left_commute) |
335 then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)" |
335 then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)" |
336 by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int) |
336 by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int) |
337 then have "[setprod id A = ((-1)^(card E) * |
337 then have "[setprod id A = ((-1)^(card E) * |
338 (setprod id ((\<lambda>x. x * a) ` A)))] (mod p)" |
338 (setprod id ((\<lambda>x. x * a) ` A)))] (mod p)" |
339 by (simp add: B_def) |
339 by (simp add: B_def) |
347 setprod id A))] (mod p)" |
347 setprod id A))] (mod p)" |
348 by simp |
348 by simp |
349 then have "[setprod id A = ((-1)^(card E) * a^(card A) * |
349 then have "[setprod id A = ((-1)^(card E) * a^(card A) * |
350 setprod id A)](mod p)" |
350 setprod id A)](mod p)" |
351 apply (rule cong_trans_int) |
351 apply (rule cong_trans_int) |
352 apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult_assoc) |
352 apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult.assoc) |
353 done |
353 done |
354 then have a: "[setprod id A * (-1)^(card E) = |
354 then have a: "[setprod id A * (-1)^(card E) = |
355 ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)" |
355 ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)" |
356 by (rule cong_scalar_int) |
356 by (rule cong_scalar_int) |
357 then have "[setprod id A * (-1)^(card E) = setprod id A * |
357 then have "[setprod id A * (-1)^(card E) = setprod id A * |
358 (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)" |
358 (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)" |
359 apply (rule cong_trans_int) |
359 apply (rule cong_trans_int) |
360 apply (simp add: a mult_commute mult_left_commute) |
360 apply (simp add: a mult.commute mult.left_commute) |
361 done |
361 done |
362 then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)" |
362 then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)" |
363 apply (rule cong_trans_int) |
363 apply (rule cong_trans_int) |
364 apply (simp add: aux cong del:setprod.cong) |
364 apply (simp add: aux cong del:setprod.cong) |
365 done |
365 done |