1 (* Title: HOL/Quadratic_Reciprocity/Euler.thy |
|
2 ID: $Id$ |
|
3 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
|
4 *) |
|
5 |
|
6 header {* Euler's criterion *} |
|
7 |
|
8 theory Euler imports Residues EvenOdd begin |
|
9 |
|
10 definition |
|
11 MultInvPair :: "int => int => int => int set" where |
|
12 "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}" |
|
13 |
|
14 definition |
|
15 SetS :: "int => int => int set set" where |
|
16 "SetS a p = (MultInvPair a p ` SRStar p)" |
|
17 |
|
18 |
|
19 subsection {* Property for MultInvPair *} |
|
20 |
|
21 lemma MultInvPair_prop1a: |
|
22 "[| zprime p; 2 < p; ~([a = 0](mod p)); |
|
23 X \<in> (SetS a p); Y \<in> (SetS a p); |
|
24 ~((X \<inter> Y) = {}) |] ==> X = Y" |
|
25 apply (auto simp add: SetS_def) |
|
26 apply (drule StandardRes_SRStar_prop1a)+ defer 1 |
|
27 apply (drule StandardRes_SRStar_prop1a)+ |
|
28 apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym) |
|
29 apply (drule notE, rule MultInv_zcong_prop1, auto)[] |
|
30 apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym)[] |
|
31 apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[] |
|
32 apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[] |
|
33 apply (drule MultInv_zcong_prop1, auto)[] |
|
34 apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[] |
|
35 apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[] |
|
36 apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[] |
|
37 done |
|
38 |
|
39 lemma MultInvPair_prop1b: |
|
40 "[| zprime p; 2 < p; ~([a = 0](mod p)); |
|
41 X \<in> (SetS a p); Y \<in> (SetS a p); |
|
42 X \<noteq> Y |] ==> X \<inter> Y = {}" |
|
43 apply (rule notnotD) |
|
44 apply (rule notI) |
|
45 apply (drule MultInvPair_prop1a, auto) |
|
46 done |
|
47 |
|
48 lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> |
|
49 \<forall>X \<in> SetS a p. \<forall>Y \<in> SetS a p. X \<noteq> Y --> X\<inter>Y = {}" |
|
50 by (auto simp add: MultInvPair_prop1b) |
|
51 |
|
52 lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> |
|
53 Union ( SetS a p) = SRStar p" |
|
54 apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4 |
|
55 SRStar_mult_prop2) |
|
56 apply (frule StandardRes_SRStar_prop3) |
|
57 apply (rule bexI, auto) |
|
58 done |
|
59 |
|
60 lemma MultInvPair_distinct: "[| zprime p; 2 < p; ~([a = 0] (mod p)); |
|
61 ~([j = 0] (mod p)); |
|
62 ~(QuadRes p a) |] ==> |
|
63 ~([j = a * MultInv p j] (mod p))" |
|
64 proof |
|
65 assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and |
|
66 "~([j = 0] (mod p))" and "~(QuadRes p a)" |
|
67 assume "[j = a * MultInv p j] (mod p)" |
|
68 then have "[j * j = (a * MultInv p j) * j] (mod p)" |
|
69 by (auto simp add: zcong_scalar) |
|
70 then have a:"[j * j = a * (MultInv p j * j)] (mod p)" |
|
71 by (auto simp add: zmult_ac) |
|
72 have "[j * j = a] (mod p)" |
|
73 proof - |
|
74 from prems have b: "[MultInv p j * j = 1] (mod p)" |
|
75 by (simp add: MultInv_prop2a) |
|
76 from b a show ?thesis |
|
77 by (auto simp add: zcong_zmult_prop2) |
|
78 qed |
|
79 then have "[j^2 = a] (mod p)" |
|
80 by (metis number_of_is_id power2_eq_square succ_bin_simps) |
|
81 with prems show False |
|
82 by (simp add: QuadRes_def) |
|
83 qed |
|
84 |
|
85 lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p)); |
|
86 ~(QuadRes p a); ~([j = 0] (mod p)) |] ==> |
|
87 card (MultInvPair a p j) = 2" |
|
88 apply (auto simp add: MultInvPair_def) |
|
89 apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))") |
|
90 apply auto |
|
91 apply (metis MultInvPair_distinct Pls_def StandardRes_def aux number_of_is_id one_is_num_one) |
|
92 done |
|
93 |
|
94 |
|
95 subsection {* Properties of SetS *} |
|
96 |
|
97 lemma SetS_finite: "2 < p ==> finite (SetS a p)" |
|
98 by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI) |
|
99 |
|
100 lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X" |
|
101 by (auto simp add: SetS_def MultInvPair_def) |
|
102 |
|
103 lemma SetS_elems_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); |
|
104 ~(QuadRes p a) |] ==> |
|
105 \<forall>X \<in> SetS a p. card X = 2" |
|
106 apply (auto simp add: SetS_def) |
|
107 apply (frule StandardRes_SRStar_prop1a) |
|
108 apply (rule MultInvPair_card_two, auto) |
|
109 done |
|
110 |
|
111 lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))" |
|
112 by (auto simp add: SetS_finite SetS_elems_finite finite_Union) |
|
113 |
|
114 lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); |
|
115 \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S" |
|
116 by (induct set: finite) auto |
|
117 |
|
118 lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> |
|
119 int(card(SetS a p)) = (p - 1) div 2" |
|
120 proof - |
|
121 assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)" |
|
122 then have "(p - 1) = 2 * int(card(SetS a p))" |
|
123 proof - |
|
124 have "p - 1 = int(card(Union (SetS a p)))" |
|
125 by (auto simp add: prems MultInvPair_prop2 SRStar_card) |
|
126 also have "... = int (setsum card (SetS a p))" |
|
127 by (auto simp add: prems SetS_finite SetS_elems_finite |
|
128 MultInvPair_prop1c [of p a] card_Union_disjoint) |
|
129 also have "... = int(setsum (%x.2) (SetS a p))" |
|
130 using prems |
|
131 by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite |
|
132 card_setsum_aux simp del: setsum_constant) |
|
133 also have "... = 2 * int(card( SetS a p))" |
|
134 by (auto simp add: prems SetS_finite setsum_const2) |
|
135 finally show ?thesis . |
|
136 qed |
|
137 from this show ?thesis |
|
138 by auto |
|
139 qed |
|
140 |
|
141 lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); |
|
142 ~(QuadRes p a); x \<in> (SetS a p) |] ==> |
|
143 [\<Prod>x = a] (mod p)" |
|
144 apply (auto simp add: SetS_def MultInvPair_def) |
|
145 apply (frule StandardRes_SRStar_prop1a) |
|
146 apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)") |
|
147 apply (auto simp add: StandardRes_prop2 MultInvPair_distinct) |
|
148 apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in |
|
149 StandardRes_prop4) |
|
150 apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)") |
|
151 apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and |
|
152 b = "x * (a * MultInv p x)" and |
|
153 c = "a * (x * MultInv p x)" in zcong_trans, force) |
|
154 apply (frule_tac p = p and x = x in MultInv_prop2, auto) |
|
155 apply (metis StandardRes_SRStar_prop3 mult_1_right mult_commute zcong_sym zcong_zmult_prop1) |
|
156 apply (auto simp add: zmult_ac) |
|
157 done |
|
158 |
|
159 lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1" |
|
160 by arith |
|
161 |
|
162 lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)" |
|
163 by auto |
|
164 |
|
165 lemma SRStar_d22set_prop: "2 < p \<Longrightarrow> (SRStar p) = {1} \<union> (d22set (p - 1))" |
|
166 apply (induct p rule: d22set.induct) |
|
167 apply auto |
|
168 apply (simp add: SRStar_def d22set.simps) |
|
169 apply (simp add: SRStar_def d22set.simps, clarify) |
|
170 apply (frule aux1) |
|
171 apply (frule aux2, auto) |
|
172 apply (simp_all add: SRStar_def) |
|
173 apply (simp add: d22set.simps) |
|
174 apply (frule d22set_le) |
|
175 apply (frule d22set_g_1, auto) |
|
176 done |
|
177 |
|
178 lemma Union_SetS_setprod_prop1: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> |
|
179 [\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)" |
|
180 proof - |
|
181 assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)" |
|
182 then have "[\<Prod>(Union (SetS a p)) = |
|
183 setprod (setprod (%x. x)) (SetS a p)] (mod p)" |
|
184 by (auto simp add: SetS_finite SetS_elems_finite |
|
185 MultInvPair_prop1c setprod_Union_disjoint) |
|
186 also have "[setprod (setprod (%x. x)) (SetS a p) = |
|
187 setprod (%x. a) (SetS a p)] (mod p)" |
|
188 by (rule setprod_same_function_zcong) |
|
189 (auto simp add: prems SetS_setprod_prop SetS_finite) |
|
190 also (zcong_trans) have "[setprod (%x. a) (SetS a p) = |
|
191 a^(card (SetS a p))] (mod p)" |
|
192 by (auto simp add: prems SetS_finite setprod_constant) |
|
193 finally (zcong_trans) show ?thesis |
|
194 apply (rule zcong_trans) |
|
195 apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto) |
|
196 apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force) |
|
197 apply (auto simp add: prems SetS_card) |
|
198 done |
|
199 qed |
|
200 |
|
201 lemma Union_SetS_setprod_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> |
|
202 \<Prod>(Union (SetS a p)) = zfact (p - 1)" |
|
203 proof - |
|
204 assume "zprime p" and "2 < p" and "~([a = 0](mod p))" |
|
205 then have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)" |
|
206 by (auto simp add: MultInvPair_prop2) |
|
207 also have "... = \<Prod>({1} \<union> (d22set (p - 1)))" |
|
208 by (auto simp add: prems SRStar_d22set_prop) |
|
209 also have "... = zfact(p - 1)" |
|
210 proof - |
|
211 have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))" |
|
212 by (metis d22set_fin d22set_g_1 linorder_neq_iff) |
|
213 then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))" |
|
214 by auto |
|
215 then show ?thesis |
|
216 by (auto simp add: d22set_prod_zfact) |
|
217 qed |
|
218 finally show ?thesis . |
|
219 qed |
|
220 |
|
221 lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> |
|
222 [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)" |
|
223 apply (frule Union_SetS_setprod_prop1) |
|
224 apply (auto simp add: Union_SetS_setprod_prop2) |
|
225 done |
|
226 |
|
227 text {* \medskip Prove the first part of Euler's Criterion: *} |
|
228 |
|
229 lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); |
|
230 ~(QuadRes p x) |] ==> |
|
231 [x^(nat (((p) - 1) div 2)) = -1](mod p)" |
|
232 by (metis Wilson_Russ number_of_is_id zcong_sym zcong_trans zfact_prop) |
|
233 |
|
234 text {* \medskip Prove another part of Euler Criterion: *} |
|
235 |
|
236 lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)" |
|
237 proof - |
|
238 assume "0 < p" |
|
239 then have "a ^ (nat p) = a ^ (1 + (nat p - 1))" |
|
240 by (auto simp add: diff_add_assoc) |
|
241 also have "... = (a ^ 1) * a ^ (nat(p) - 1)" |
|
242 by (simp only: zpower_zadd_distrib) |
|
243 also have "... = a * a ^ (nat(p) - 1)" |
|
244 by auto |
|
245 finally show ?thesis . |
|
246 qed |
|
247 |
|
248 lemma aux_2: "[| (2::int) < p; p \<in> zOdd |] ==> 0 < ((p - 1) div 2)" |
|
249 proof - |
|
250 assume "2 < p" and "p \<in> zOdd" |
|
251 then have "(p - 1):zEven" |
|
252 by (auto simp add: zEven_def zOdd_def) |
|
253 then have aux_1: "2 * ((p - 1) div 2) = (p - 1)" |
|
254 by (auto simp add: even_div_2_prop2) |
|
255 with `2 < p` have "1 < (p - 1)" |
|
256 by auto |
|
257 then have " 1 < (2 * ((p - 1) div 2))" |
|
258 by (auto simp add: aux_1) |
|
259 then have "0 < (2 * ((p - 1) div 2)) div 2" |
|
260 by auto |
|
261 then show ?thesis by auto |
|
262 qed |
|
263 |
|
264 lemma Euler_part2: |
|
265 "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)" |
|
266 apply (frule zprime_zOdd_eq_grt_2) |
|
267 apply (frule aux_2, auto) |
|
268 apply (frule_tac a = a in aux_1, auto) |
|
269 apply (frule zcong_zmult_prop1, auto) |
|
270 done |
|
271 |
|
272 text {* \medskip Prove the final part of Euler's Criterion: *} |
|
273 |
|
274 lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)" |
|
275 by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans) |
|
276 |
|
277 lemma aux__2: "2 * nat((p - 1) div 2) = nat (2 * ((p - 1) div 2))" |
|
278 by (auto simp add: nat_mult_distrib) |
|
279 |
|
280 lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==> |
|
281 [x^(nat (((p) - 1) div 2)) = 1](mod p)" |
|
282 apply (subgoal_tac "p \<in> zOdd") |
|
283 apply (auto simp add: QuadRes_def) |
|
284 prefer 2 |
|
285 apply (metis number_of_is_id numeral_1_eq_1 zprime_zOdd_eq_grt_2) |
|
286 apply (frule aux__1, auto) |
|
287 apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower) |
|
288 apply (auto simp add: zpower_zpower) |
|
289 apply (rule zcong_trans) |
|
290 apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"]) |
|
291 apply (metis Little_Fermat even_div_2_prop2 mult_Bit0 number_of_is_id odd_minus_one_even one_is_num_one zmult_1 aux__2) |
|
292 done |
|
293 |
|
294 |
|
295 text {* \medskip Finally show Euler's Criterion: *} |
|
296 |
|
297 theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) = |
|
298 a^(nat (((p) - 1) div 2))] (mod p)" |
|
299 apply (auto simp add: Legendre_def Euler_part2) |
|
300 apply (frule Euler_part3, auto simp add: zcong_sym)[] |
|
301 apply (frule Euler_part1, auto simp add: zcong_sym)[] |
|
302 done |
|
303 |
|
304 end |
|