1 (* Title: HOL/Quadratic_Reciprocity/Gauss.thy |
|
2 ID: $Id$ |
|
3 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
|
4 *) |
|
5 |
|
6 header {*Integers: Divisibility and Congruences*} |
|
7 |
|
8 theory Int2 |
|
9 imports Finite2 WilsonRuss |
|
10 begin |
|
11 |
|
12 definition |
|
13 MultInv :: "int => int => int" where |
|
14 "MultInv p x = x ^ nat (p - 2)" |
|
15 |
|
16 |
|
17 subsection {* Useful lemmas about dvd and powers *} |
|
18 |
|
19 lemma zpower_zdvd_prop1: |
|
20 "0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)" |
|
21 by (induct n) (auto simp add: dvd_mult2 [of p y]) |
|
22 |
|
23 lemma zdvd_bounds: "n dvd m ==> m \<le> (0::int) | n \<le> m" |
|
24 proof - |
|
25 assume "n dvd m" |
|
26 then have "~(0 < m & m < n)" |
|
27 using zdvd_not_zless [of m n] by auto |
|
28 then show ?thesis by auto |
|
29 qed |
|
30 |
|
31 lemma zprime_zdvd_zmult_better: "[| zprime p; p dvd (m * n) |] ==> |
|
32 (p dvd m) | (p dvd n)" |
|
33 apply (cases "0 \<le> m") |
|
34 apply (simp add: zprime_zdvd_zmult) |
|
35 apply (insert zprime_zdvd_zmult [of "-m" p n]) |
|
36 apply auto |
|
37 done |
|
38 |
|
39 lemma zpower_zdvd_prop2: |
|
40 "zprime p \<Longrightarrow> p dvd ((y::int) ^ n) \<Longrightarrow> 0 < n \<Longrightarrow> p dvd y" |
|
41 apply (induct n) |
|
42 apply simp |
|
43 apply (frule zprime_zdvd_zmult_better) |
|
44 apply simp |
|
45 apply (force simp del:dvd_mult) |
|
46 done |
|
47 |
|
48 lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y" |
|
49 proof - |
|
50 assume "0 < z" then have modth: "x mod z \<ge> 0" by simp |
|
51 have "(x div z) * z \<le> (x div z) * z" by simp |
|
52 then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith |
|
53 also have "\<dots> = x" |
|
54 by (auto simp add: zmod_zdiv_equality [symmetric] zmult_ac) |
|
55 also assume "x < y * z" |
|
56 finally show ?thesis |
|
57 by (auto simp add: prems mult_less_cancel_right, insert prems, arith) |
|
58 qed |
|
59 |
|
60 lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y" |
|
61 proof - |
|
62 assume "0 < z" and "x < (y * z) + z" |
|
63 then have "x < (y + 1) * z" by (auto simp add: int_distrib) |
|
64 then have "x div z < y + 1" |
|
65 apply - |
|
66 apply (rule_tac y = "y + 1" in div_prop1) |
|
67 apply (auto simp add: prems) |
|
68 done |
|
69 then show ?thesis by auto |
|
70 qed |
|
71 |
|
72 lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)" |
|
73 proof- |
|
74 assume "0 < y" |
|
75 from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto |
|
76 moreover have "0 \<le> x mod y" |
|
77 by (auto simp add: prems pos_mod_sign) |
|
78 ultimately show ?thesis |
|
79 by arith |
|
80 qed |
|
81 |
|
82 |
|
83 subsection {* Useful properties of congruences *} |
|
84 |
|
85 lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)" |
|
86 by (auto simp add: zcong_def) |
|
87 |
|
88 lemma zcong_id: "[m = 0] (mod m)" |
|
89 by (auto simp add: zcong_def) |
|
90 |
|
91 lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)" |
|
92 by (auto simp add: zcong_refl zcong_zadd) |
|
93 |
|
94 lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)" |
|
95 by (induct z) (auto simp add: zcong_zmult) |
|
96 |
|
97 lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==> |
|
98 [a = d](mod m)" |
|
99 apply (erule zcong_trans) |
|
100 apply simp |
|
101 done |
|
102 |
|
103 lemma aux1: "a - b = (c::int) ==> a = c + b" |
|
104 by auto |
|
105 |
|
106 lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) = |
|
107 [c = b * d] (mod m))" |
|
108 apply (auto simp add: zcong_def dvd_def) |
|
109 apply (rule_tac x = "ka + k * d" in exI) |
|
110 apply (drule aux1)+ |
|
111 apply (auto simp add: int_distrib) |
|
112 apply (rule_tac x = "ka - k * d" in exI) |
|
113 apply (drule aux1)+ |
|
114 apply (auto simp add: int_distrib) |
|
115 done |
|
116 |
|
117 lemma zcong_zmult_prop2: "[a = b](mod m) ==> |
|
118 ([c = d * a](mod m) = [c = d * b] (mod m))" |
|
119 by (auto simp add: zmult_ac zcong_zmult_prop1) |
|
120 |
|
121 lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p); |
|
122 ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)" |
|
123 apply (auto simp add: zcong_def) |
|
124 apply (drule zprime_zdvd_zmult_better, auto) |
|
125 done |
|
126 |
|
127 lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m); |
|
128 x < m; y < m |] ==> x = y" |
|
129 by (metis zcong_not zcong_sym zless_linear) |
|
130 |
|
131 lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==> |
|
132 ~([x = 1] (mod p))" |
|
133 proof |
|
134 assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)" |
|
135 then have "[1 = -1] (mod p)" |
|
136 apply (auto simp add: zcong_sym) |
|
137 apply (drule zcong_trans, auto) |
|
138 done |
|
139 then have "[1 + 1 = -1 + 1] (mod p)" |
|
140 by (simp only: zcong_shift) |
|
141 then have "[2 = 0] (mod p)" |
|
142 by auto |
|
143 then have "p dvd 2" |
|
144 by (auto simp add: dvd_def zcong_def) |
|
145 with prems show False |
|
146 by (auto simp add: zdvd_not_zless) |
|
147 qed |
|
148 |
|
149 lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)" |
|
150 by (auto simp add: zcong_def) |
|
151 |
|
152 lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==> |
|
153 [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)" |
|
154 by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult) |
|
155 |
|
156 lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==> |
|
157 ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)" |
|
158 apply auto |
|
159 apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero) |
|
160 apply auto |
|
161 done |
|
162 |
|
163 lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)" |
|
164 by (auto simp add: zcong_zero_equiv_div zdvd_not_zless) |
|
165 |
|
166 lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0" |
|
167 apply (drule order_le_imp_less_or_eq, auto) |
|
168 apply (frule_tac m = m in zcong_not_zero) |
|
169 apply auto |
|
170 done |
|
171 |
|
172 lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. zgcd x y = 1 |] |
|
173 ==> zgcd (setprod id A) y = 1" |
|
174 by (induct set: finite) (auto simp add: zgcd_zgcd_zmult) |
|
175 |
|
176 |
|
177 subsection {* Some properties of MultInv *} |
|
178 |
|
179 lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> |
|
180 [(MultInv p x) = (MultInv p y)] (mod p)" |
|
181 by (auto simp add: MultInv_def zcong_zpower) |
|
182 |
|
183 lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
|
184 [(x * (MultInv p x)) = 1] (mod p)" |
|
185 proof (simp add: MultInv_def zcong_eq_zdvd_prop) |
|
186 assume "2 < p" and "zprime p" and "~ p dvd x" |
|
187 have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)" |
|
188 by auto |
|
189 also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)" |
|
190 by (simp only: nat_add_distrib) |
|
191 also have "p - 2 + 1 = p - 1" by arith |
|
192 finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)" |
|
193 by (rule ssubst, auto) |
|
194 also from prems have "[x ^ nat (p - 1) = 1] (mod p)" |
|
195 by (auto simp add: Little_Fermat) |
|
196 finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" . |
|
197 qed |
|
198 |
|
199 lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
|
200 [(MultInv p x) * x = 1] (mod p)" |
|
201 by (auto simp add: MultInv_prop2 zmult_ac) |
|
202 |
|
203 lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))" |
|
204 by (simp add: nat_diff_distrib) |
|
205 |
|
206 lemma aux_2: "2 < p ==> 0 < nat (p - 2)" |
|
207 by auto |
|
208 |
|
209 lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
|
210 ~([MultInv p x = 0](mod p))" |
|
211 apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1) |
|
212 apply (drule aux_2) |
|
213 apply (drule zpower_zdvd_prop2, auto) |
|
214 done |
|
215 |
|
216 lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> |
|
217 [(MultInv p (MultInv p x)) = (x * (MultInv p x) * |
|
218 (MultInv p (MultInv p x)))] (mod p)" |
|
219 apply (drule MultInv_prop2, auto) |
|
220 apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto) |
|
221 apply (auto simp add: zcong_sym) |
|
222 done |
|
223 |
|
224 lemma aux__2: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> |
|
225 [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)" |
|
226 apply (frule MultInv_prop3, auto) |
|
227 apply (insert MultInv_prop2 [of p "MultInv p x"], auto) |
|
228 apply (drule MultInv_prop2, auto) |
|
229 apply (drule_tac k = x in zcong_scalar2, auto) |
|
230 apply (auto simp add: zmult_ac) |
|
231 done |
|
232 |
|
233 lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
|
234 [(MultInv p (MultInv p x)) = x] (mod p)" |
|
235 apply (frule aux__1, auto) |
|
236 apply (drule aux__2, auto) |
|
237 apply (drule zcong_trans, auto) |
|
238 done |
|
239 |
|
240 lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p)); |
|
241 ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> |
|
242 [x = y] (mod p)" |
|
243 apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and |
|
244 m = p and k = x in zcong_scalar) |
|
245 apply (insert MultInv_prop2 [of p x], simp) |
|
246 apply (auto simp only: zcong_sym [of "MultInv p x * x"]) |
|
247 apply (auto simp add: zmult_ac) |
|
248 apply (drule zcong_trans, auto) |
|
249 apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto) |
|
250 apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac) |
|
251 apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x]) |
|
252 apply (auto simp add: zcong_sym) |
|
253 done |
|
254 |
|
255 lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> |
|
256 [a * MultInv p j = a * MultInv p k] (mod p)" |
|
257 by (drule MultInv_prop1, auto simp add: zcong_scalar2) |
|
258 |
|
259 lemma aux___1: "[j = a * MultInv p k] (mod p) ==> |
|
260 [j * k = a * MultInv p k * k] (mod p)" |
|
261 by (auto simp add: zcong_scalar) |
|
262 |
|
263 lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p)); |
|
264 [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)" |
|
265 apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 |
|
266 [of "MultInv p k * k" 1 p "j * k" a]) |
|
267 apply (auto simp add: zmult_ac) |
|
268 done |
|
269 |
|
270 lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = |
|
271 (MultInv p j) * a] (mod p)" |
|
272 by (auto simp add: zmult_assoc zcong_scalar2) |
|
273 |
|
274 lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p)); |
|
275 [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |] |
|
276 ==> [k = a * (MultInv p j)] (mod p)" |
|
277 apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 |
|
278 [of "MultInv p j * j" 1 p "MultInv p j * a" k]) |
|
279 apply (auto simp add: zmult_ac zcong_sym) |
|
280 done |
|
281 |
|
282 lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p)); |
|
283 ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> |
|
284 [k = a * MultInv p j] (mod p)" |
|
285 apply (drule aux___1) |
|
286 apply (frule aux___2, auto) |
|
287 by (drule aux___3, drule aux___4, auto) |
|
288 |
|
289 lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p)); |
|
290 ~([k = 0](mod p)); ~([j = 0](mod p)); |
|
291 [a * MultInv p j = a * MultInv p k] (mod p) |] ==> |
|
292 [j = k] (mod p)" |
|
293 apply (auto simp add: zcong_eq_zdvd_prop [of a p]) |
|
294 apply (frule zprime_imp_zrelprime, auto) |
|
295 apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto) |
|
296 apply (drule MultInv_prop5, auto) |
|
297 done |
|
298 |
|
299 end |
|