112 and d: "0 < y" |
112 and d: "0 < y" |
113 and e: "y \<le> (int p - 1) div 2" |
113 and e: "y \<le> (int p - 1) div 2" |
114 for x y |
114 for x y |
115 proof - |
115 proof - |
116 from p_a_relprime have "\<not> p dvd a" |
116 from p_a_relprime have "\<not> p dvd a" |
117 by (simp add: cong_altdef_int) |
117 by (simp add: cong_0_iff) |
118 with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"] |
118 with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"] |
119 have "coprime a (int p)" |
119 have "coprime a (int p)" |
120 by (simp_all add: ac_simps) |
120 by (simp_all add: ac_simps) |
121 with a cong_mult_rcancel_int [of a "int p" x y] have "[x = y] (mod p)" |
121 with a cong_mult_rcancel [of a "int p" x y] have "[x = y] (mod p)" |
122 by simp |
122 by simp |
123 with cong_less_imp_eq_int [of x y p] p_minus_one_l |
123 with cong_less_imp_eq_int [of x y p] p_minus_one_l |
124 order_le_less_trans [of x "(int p - 1) div 2" p] |
124 order_le_less_trans [of x "(int p - 1) div 2" p] |
125 order_le_less_trans [of y "(int p - 1) div 2" p] |
125 order_le_less_trans [of y "(int p - 1) div 2" p] |
126 show ?thesis |
126 show ?thesis |
127 by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff) |
127 by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff) |
128 qed |
128 qed |
129 show ?thesis |
129 show ?thesis |
130 apply (insert p_ge_2 p_a_relprime p_minus_one_l) |
130 using p_ge_2 p_a_relprime p_minus_one_l |
131 apply (auto simp add: B_def) |
131 by (metis "*" A_def A_res B_def GAUSS.ResSet_image GAUSS_axioms greaterThanAtMost_iff odd_p odd_pos of_nat_0_less_iff) |
132 apply (rule ResSet_image) |
|
133 apply (auto simp add: A_res) |
|
134 apply (auto simp add: A_def *) |
|
135 done |
|
136 qed |
132 qed |
137 |
133 |
138 lemma SR_B_inj: "inj_on (\<lambda>x. x mod p) B" |
134 lemma SR_B_inj: "inj_on (\<lambda>x. x mod p) B" |
139 proof - |
135 proof - |
140 have False |
136 have False |
147 for x y |
143 for x y |
148 proof - |
144 proof - |
149 from a have a': "[x * a = y * a](mod p)" |
145 from a have a': "[x * a = y * a](mod p)" |
150 using cong_def by blast |
146 using cong_def by blast |
151 from p_a_relprime have "\<not>p dvd a" |
147 from p_a_relprime have "\<not>p dvd a" |
152 by (simp add: cong_altdef_int) |
148 by (simp add: cong_0_iff) |
153 with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"] |
149 with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"] |
154 have "coprime a (int p)" |
150 have "coprime a (int p)" |
155 by (simp_all add: ac_simps) |
151 by (simp_all add: ac_simps) |
156 with a' cong_mult_rcancel_int [of a "int p" x y] |
152 with a' cong_mult_rcancel [of a "int p" x y] |
157 have "[x = y] (mod p)" by simp |
153 have "[x = y] (mod p)" by simp |
158 with cong_less_imp_eq_int [of x y p] p_minus_one_l |
154 with cong_less_imp_eq_int [of x y p] p_minus_one_l |
159 order_le_less_trans [of x "(int p - 1) div 2" p] |
155 order_le_less_trans [of x "(int p - 1) div 2" p] |
160 order_le_less_trans [of y "(int p - 1) div 2" p] |
156 order_le_less_trans [of y "(int p - 1) div 2" p] |
161 have "x = y" |
157 have "x = y" |
222 |
218 |
223 lemma all_A_relprime: |
219 lemma all_A_relprime: |
224 "coprime x p" if "x \<in> A" |
220 "coprime x p" if "x \<in> A" |
225 proof - |
221 proof - |
226 from A_ncong_p [OF that] have "\<not> int p dvd x" |
222 from A_ncong_p [OF that] have "\<not> int p dvd x" |
227 by (simp add: cong_altdef_int) |
223 by (simp add: cong_0_iff) |
228 with p_prime show ?thesis |
224 with p_prime show ?thesis |
229 by (metis (no_types) coprime_commute prime_imp_coprime prime_nat_int_transfer) |
225 by (metis (no_types) coprime_commute prime_imp_coprime prime_nat_int_transfer) |
230 qed |
226 qed |
231 |
227 |
232 lemma A_prod_relprime: "coprime (prod id A) p" |
228 lemma A_prod_relprime: "coprime (prod id A) p" |
368 (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)" |
364 (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)" |
369 by (rule cong_trans) (simp add: a ac_simps) |
365 by (rule cong_trans) (simp add: a ac_simps) |
370 then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)" |
366 then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)" |
371 by (rule cong_trans) (simp add: aux cong del: prod.strong_cong) |
367 by (rule cong_trans) (simp add: aux cong del: prod.strong_cong) |
372 with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)" |
368 with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)" |
373 by (metis cong_mult_lcancel_int) |
369 by (metis cong_mult_lcancel) |
374 then show ?thesis |
370 then show ?thesis |
375 by (simp add: A_card_eq cong_sym) |
371 by (simp add: A_card_eq cong_sym) |
376 qed |
372 qed |
377 |
373 |
378 theorem gauss_lemma: "Legendre a p = (-1) ^ (card E)" |
374 theorem gauss_lemma: "Legendre a p = (-1) ^ (card E)" |
388 moreover from p_a_relprime have "Legendre a p = 1 \<or> Legendre a p = -1" |
384 moreover from p_a_relprime have "Legendre a p = 1 \<or> Legendre a p = -1" |
389 by (auto simp add: Legendre_def) |
385 by (auto simp add: Legendre_def) |
390 moreover have "(-1::int) ^ (card E) = 1 \<or> (-1::int) ^ (card E) = -1" |
386 moreover have "(-1::int) ^ (card E) = 1 \<or> (-1::int) ^ (card E) = -1" |
391 using neg_one_even_power neg_one_odd_power by blast |
387 using neg_one_even_power neg_one_odd_power by blast |
392 moreover have "[1 \<noteq> - 1] (mod int p)" |
388 moreover have "[1 \<noteq> - 1] (mod int p)" |
393 using cong_altdef_int nonzero_mod_p[of 2] p_odd_int by fastforce |
389 using cong_iff_dvd_diff [where 'a=int] nonzero_mod_p[of 2] p_odd_int |
|
390 by fastforce |
394 ultimately show ?thesis |
391 ultimately show ?thesis |
395 by (auto simp add: cong_sym) |
392 by (auto simp add: cong_sym) |
396 qed |
393 qed |
397 |
394 |
398 end |
395 end |