1 (* Title: HOL/NumberTheory/IntPrimes.thy |
|
2 ID: $Id$ |
|
3 Author: Thomas M. Rasmussen |
|
4 Copyright 2000 University of Cambridge |
|
5 *) |
|
6 |
|
7 header {* Divisibility and prime numbers (on integers) *} |
|
8 |
|
9 theory IntPrimes |
|
10 imports Main Primes |
|
11 begin |
|
12 |
|
13 text {* |
|
14 The @{text dvd} relation, GCD, Euclid's extended algorithm, primes, |
|
15 congruences (all on the Integers). Comparable to theory @{text |
|
16 Primes}, but @{text dvd} is included here as it is not present in |
|
17 main HOL. Also includes extended GCD and congruences not present in |
|
18 @{text Primes}. |
|
19 *} |
|
20 |
|
21 |
|
22 subsection {* Definitions *} |
|
23 |
|
24 consts |
|
25 xzgcda :: "int * int * int * int * int * int * int * int => int * int * int" |
|
26 |
|
27 recdef xzgcda |
|
28 "measure ((\<lambda>(m, n, r', r, s', s, t', t). nat r) |
|
29 :: int * int * int * int *int * int * int * int => nat)" |
|
30 "xzgcda (m, n, r', r, s', s, t', t) = |
|
31 (if r \<le> 0 then (r', s', t') |
|
32 else xzgcda (m, n, r, r' mod r, |
|
33 s, s' - (r' div r) * s, |
|
34 t, t' - (r' div r) * t))" |
|
35 |
|
36 definition |
|
37 zprime :: "int \<Rightarrow> bool" where |
|
38 "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))" |
|
39 |
|
40 definition |
|
41 xzgcd :: "int => int => int * int * int" where |
|
42 "xzgcd m n = xzgcda (m, n, m, n, 1, 0, 0, 1)" |
|
43 |
|
44 definition |
|
45 zcong :: "int => int => int => bool" ("(1[_ = _] '(mod _'))") where |
|
46 "[a = b] (mod m) = (m dvd (a - b))" |
|
47 |
|
48 subsection {* Euclid's Algorithm and GCD *} |
|
49 |
|
50 |
|
51 lemma zrelprime_zdvd_zmult_aux: |
|
52 "zgcd n k = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m" |
|
53 by (metis abs_of_nonneg dvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right) |
|
54 |
|
55 lemma zrelprime_zdvd_zmult: "zgcd n k = 1 ==> k dvd m * n ==> k dvd m" |
|
56 apply (case_tac "0 \<le> m") |
|
57 apply (blast intro: zrelprime_zdvd_zmult_aux) |
|
58 apply (subgoal_tac "k dvd -m") |
|
59 apply (rule_tac [2] zrelprime_zdvd_zmult_aux, auto) |
|
60 done |
|
61 |
|
62 lemma zgcd_geq_zero: "0 <= zgcd x y" |
|
63 by (auto simp add: zgcd_def) |
|
64 |
|
65 text{*This is merely a sanity check on zprime, since the previous version |
|
66 denoted the empty set.*} |
|
67 lemma "zprime 2" |
|
68 apply (auto simp add: zprime_def) |
|
69 apply (frule zdvd_imp_le, simp) |
|
70 apply (auto simp add: order_le_less dvd_def) |
|
71 done |
|
72 |
|
73 lemma zprime_imp_zrelprime: |
|
74 "zprime p ==> \<not> p dvd n ==> zgcd n p = 1" |
|
75 apply (auto simp add: zprime_def) |
|
76 apply (metis zgcd_geq_zero zgcd_zdvd1 zgcd_zdvd2) |
|
77 done |
|
78 |
|
79 lemma zless_zprime_imp_zrelprime: |
|
80 "zprime p ==> 0 < n ==> n < p ==> zgcd n p = 1" |
|
81 apply (erule zprime_imp_zrelprime) |
|
82 apply (erule zdvd_not_zless, assumption) |
|
83 done |
|
84 |
|
85 lemma zprime_zdvd_zmult: |
|
86 "0 \<le> (m::int) ==> zprime p ==> p dvd m * n ==> p dvd m \<or> p dvd n" |
|
87 by (metis zgcd_zdvd1 zgcd_zdvd2 zgcd_pos zprime_def zrelprime_dvd_mult) |
|
88 |
|
89 lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n" |
|
90 apply (rule zgcd_eq [THEN trans]) |
|
91 apply (simp add: mod_add_eq) |
|
92 apply (rule zgcd_eq [symmetric]) |
|
93 done |
|
94 |
|
95 lemma zgcd_zdvd_zgcd_zmult: "zgcd m n dvd zgcd (k * m) n" |
|
96 by (simp add: zgcd_greatest_iff) |
|
97 |
|
98 lemma zgcd_zmult_zdvd_zgcd: |
|
99 "zgcd k n = 1 ==> zgcd (k * m) n dvd zgcd m n" |
|
100 apply (simp add: zgcd_greatest_iff) |
|
101 apply (rule_tac n = k in zrelprime_zdvd_zmult) |
|
102 prefer 2 |
|
103 apply (simp add: zmult_commute) |
|
104 apply (metis zgcd_1 zgcd_commute zgcd_left_commute) |
|
105 done |
|
106 |
|
107 lemma zgcd_zmult_cancel: "zgcd k n = 1 ==> zgcd (k * m) n = zgcd m n" |
|
108 by (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel) |
|
109 |
|
110 lemma zgcd_zgcd_zmult: |
|
111 "zgcd k m = 1 ==> zgcd n m = 1 ==> zgcd (k * n) m = 1" |
|
112 by (simp add: zgcd_zmult_cancel) |
|
113 |
|
114 lemma zdvd_iff_zgcd: "0 < m ==> m dvd n \<longleftrightarrow> zgcd n m = m" |
|
115 by (metis abs_of_pos zdvd_mult_div_cancel zgcd_0 zgcd_commute zgcd_geq_zero zgcd_zdvd2 zgcd_zmult_eq_self) |
|
116 |
|
117 |
|
118 |
|
119 subsection {* Congruences *} |
|
120 |
|
121 lemma zcong_1 [simp]: "[a = b] (mod 1)" |
|
122 by (unfold zcong_def, auto) |
|
123 |
|
124 lemma zcong_refl [simp]: "[k = k] (mod m)" |
|
125 by (unfold zcong_def, auto) |
|
126 |
|
127 lemma zcong_sym: "[a = b] (mod m) = [b = a] (mod m)" |
|
128 unfolding zcong_def minus_diff_eq [of a, symmetric] dvd_minus_iff .. |
|
129 |
|
130 lemma zcong_zadd: |
|
131 "[a = b] (mod m) ==> [c = d] (mod m) ==> [a + c = b + d] (mod m)" |
|
132 apply (unfold zcong_def) |
|
133 apply (rule_tac s = "(a - b) + (c - d)" in subst) |
|
134 apply (rule_tac [2] dvd_add, auto) |
|
135 done |
|
136 |
|
137 lemma zcong_zdiff: |
|
138 "[a = b] (mod m) ==> [c = d] (mod m) ==> [a - c = b - d] (mod m)" |
|
139 apply (unfold zcong_def) |
|
140 apply (rule_tac s = "(a - b) - (c - d)" in subst) |
|
141 apply (rule_tac [2] dvd_diff, auto) |
|
142 done |
|
143 |
|
144 lemma zcong_trans: |
|
145 "[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)" |
|
146 unfolding zcong_def by (auto elim!: dvdE simp add: algebra_simps) |
|
147 |
|
148 lemma zcong_zmult: |
|
149 "[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)" |
|
150 apply (rule_tac b = "b * c" in zcong_trans) |
|
151 apply (unfold zcong_def) |
|
152 apply (metis zdiff_zmult_distrib2 dvd_mult zmult_commute) |
|
153 apply (metis zdiff_zmult_distrib2 dvd_mult) |
|
154 done |
|
155 |
|
156 lemma zcong_scalar: "[a = b] (mod m) ==> [a * k = b * k] (mod m)" |
|
157 by (rule zcong_zmult, simp_all) |
|
158 |
|
159 lemma zcong_scalar2: "[a = b] (mod m) ==> [k * a = k * b] (mod m)" |
|
160 by (rule zcong_zmult, simp_all) |
|
161 |
|
162 lemma zcong_zmult_self: "[a * m = b * m] (mod m)" |
|
163 apply (unfold zcong_def) |
|
164 apply (rule dvd_diff, simp_all) |
|
165 done |
|
166 |
|
167 lemma zcong_square: |
|
168 "[| zprime p; 0 < a; [a * a = 1] (mod p)|] |
|
169 ==> [a = 1] (mod p) \<or> [a = p - 1] (mod p)" |
|
170 apply (unfold zcong_def) |
|
171 apply (rule zprime_zdvd_zmult) |
|
172 apply (rule_tac [3] s = "a * a - 1 + p * (1 - a)" in subst) |
|
173 prefer 4 |
|
174 apply (simp add: zdvd_reduce) |
|
175 apply (simp_all add: zdiff_zmult_distrib zmult_commute zdiff_zmult_distrib2) |
|
176 done |
|
177 |
|
178 lemma zcong_cancel: |
|
179 "0 \<le> m ==> |
|
180 zgcd k m = 1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)" |
|
181 apply safe |
|
182 prefer 2 |
|
183 apply (blast intro: zcong_scalar) |
|
184 apply (case_tac "b < a") |
|
185 prefer 2 |
|
186 apply (subst zcong_sym) |
|
187 apply (unfold zcong_def) |
|
188 apply (rule_tac [!] zrelprime_zdvd_zmult) |
|
189 apply (simp_all add: zdiff_zmult_distrib) |
|
190 apply (subgoal_tac "m dvd (-(a * k - b * k))") |
|
191 apply simp |
|
192 apply (subst dvd_minus_iff, assumption) |
|
193 done |
|
194 |
|
195 lemma zcong_cancel2: |
|
196 "0 \<le> m ==> |
|
197 zgcd k m = 1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)" |
|
198 by (simp add: zmult_commute zcong_cancel) |
|
199 |
|
200 lemma zcong_zgcd_zmult_zmod: |
|
201 "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd m n = 1 |
|
202 ==> [a = b] (mod m * n)" |
|
203 apply (auto simp add: zcong_def dvd_def) |
|
204 apply (subgoal_tac "m dvd n * ka") |
|
205 apply (subgoal_tac "m dvd ka") |
|
206 apply (case_tac [2] "0 \<le> ka") |
|
207 apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left zmult_commute zrelprime_zdvd_zmult) |
|
208 apply (metis abs_dvd_iff abs_of_nonneg zadd_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs zmult_1_right zmult_commute) |
|
209 apply (metis mult_le_0_iff zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff zle_anti_sym zle_linear zle_refl zmult_commute zrelprime_zdvd_zmult) |
|
210 apply (metis dvd_triv_left) |
|
211 done |
|
212 |
|
213 lemma zcong_zless_imp_eq: |
|
214 "0 \<le> a ==> |
|
215 a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b" |
|
216 apply (unfold zcong_def dvd_def, auto) |
|
217 apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong) |
|
218 apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff mod_add_right_eq) |
|
219 done |
|
220 |
|
221 lemma zcong_square_zless: |
|
222 "zprime p ==> 0 < a ==> a < p ==> |
|
223 [a * a = 1] (mod p) ==> a = 1 \<or> a = p - 1" |
|
224 apply (cut_tac p = p and a = a in zcong_square) |
|
225 apply (simp add: zprime_def) |
|
226 apply (auto intro: zcong_zless_imp_eq) |
|
227 done |
|
228 |
|
229 lemma zcong_not: |
|
230 "0 < a ==> a < m ==> 0 < b ==> b < a ==> \<not> [a = b] (mod m)" |
|
231 apply (unfold zcong_def) |
|
232 apply (rule zdvd_not_zless, auto) |
|
233 done |
|
234 |
|
235 lemma zcong_zless_0: |
|
236 "0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0" |
|
237 apply (unfold zcong_def dvd_def, auto) |
|
238 apply (metis div_pos_pos_trivial linorder_not_less div_mult_self1_is_id) |
|
239 done |
|
240 |
|
241 lemma zcong_zless_unique: |
|
242 "0 < m ==> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
|
243 apply auto |
|
244 prefer 2 apply (metis zcong_sym zcong_trans zcong_zless_imp_eq) |
|
245 apply (unfold zcong_def dvd_def) |
|
246 apply (rule_tac x = "a mod m" in exI, auto) |
|
247 apply (metis zmult_div_cancel) |
|
248 done |
|
249 |
|
250 lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)" |
|
251 unfolding zcong_def |
|
252 apply (auto elim!: dvdE simp add: algebra_simps) |
|
253 apply (rule_tac x = "-k" in exI) apply simp |
|
254 done |
|
255 |
|
256 lemma zgcd_zcong_zgcd: |
|
257 "0 < m ==> |
|
258 zgcd a m = 1 ==> [a = b] (mod m) ==> zgcd b m = 1" |
|
259 by (auto simp add: zcong_iff_lin) |
|
260 |
|
261 lemma zcong_zmod_aux: |
|
262 "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)" |
|
263 by(simp add: zdiff_zmult_distrib2 add_diff_eq eq_diff_eq add_ac) |
|
264 |
|
265 lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)" |
|
266 apply (unfold zcong_def) |
|
267 apply (rule_tac t = "a - b" in ssubst) |
|
268 apply (rule_tac m = m in zcong_zmod_aux) |
|
269 apply (rule trans) |
|
270 apply (rule_tac [2] k = m and m = "a div m - b div m" in zdvd_reduce) |
|
271 apply (simp add: zadd_commute) |
|
272 done |
|
273 |
|
274 lemma zcong_zmod_eq: "0 < m ==> [a = b] (mod m) = (a mod m = b mod m)" |
|
275 apply auto |
|
276 apply (metis pos_mod_conj zcong_zless_imp_eq zcong_zmod) |
|
277 apply (metis zcong_refl zcong_zmod) |
|
278 done |
|
279 |
|
280 lemma zcong_zminus [iff]: "[a = b] (mod -m) = [a = b] (mod m)" |
|
281 by (auto simp add: zcong_def) |
|
282 |
|
283 lemma zcong_zero [iff]: "[a = b] (mod 0) = (a = b)" |
|
284 by (auto simp add: zcong_def) |
|
285 |
|
286 lemma "[a = b] (mod m) = (a mod m = b mod m)" |
|
287 apply (case_tac "m = 0", simp add: DIVISION_BY_ZERO) |
|
288 apply (simp add: linorder_neq_iff) |
|
289 apply (erule disjE) |
|
290 prefer 2 apply (simp add: zcong_zmod_eq) |
|
291 txt{*Remainding case: @{term "m<0"}*} |
|
292 apply (rule_tac t = m in zminus_zminus [THEN subst]) |
|
293 apply (subst zcong_zminus) |
|
294 apply (subst zcong_zmod_eq, arith) |
|
295 apply (frule neg_mod_bound [of _ a], frule neg_mod_bound [of _ b]) |
|
296 apply (simp add: zmod_zminus2_eq_if del: neg_mod_bound) |
|
297 done |
|
298 |
|
299 subsection {* Modulo *} |
|
300 |
|
301 lemma zmod_zdvd_zmod: |
|
302 "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)" |
|
303 by (rule mod_mod_cancel) |
|
304 |
|
305 |
|
306 subsection {* Extended GCD *} |
|
307 |
|
308 declare xzgcda.simps [simp del] |
|
309 |
|
310 lemma xzgcd_correct_aux1: |
|
311 "zgcd r' r = k --> 0 < r --> |
|
312 (\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))" |
|
313 apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and |
|
314 z = s and aa = t' and ab = t in xzgcda.induct) |
|
315 apply (subst zgcd_eq) |
|
316 apply (subst xzgcda.simps, auto) |
|
317 apply (case_tac "r' mod r = 0") |
|
318 prefer 2 |
|
319 apply (frule_tac a = "r'" in pos_mod_sign, auto) |
|
320 apply (rule exI) |
|
321 apply (rule exI) |
|
322 apply (subst xzgcda.simps, auto) |
|
323 done |
|
324 |
|
325 lemma xzgcd_correct_aux2: |
|
326 "(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> 0 < r --> |
|
327 zgcd r' r = k" |
|
328 apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and |
|
329 z = s and aa = t' and ab = t in xzgcda.induct) |
|
330 apply (subst zgcd_eq) |
|
331 apply (subst xzgcda.simps) |
|
332 apply (auto simp add: linorder_not_le) |
|
333 apply (case_tac "r' mod r = 0") |
|
334 prefer 2 |
|
335 apply (frule_tac a = "r'" in pos_mod_sign, auto) |
|
336 apply (metis Pair_eq simps zle_refl) |
|
337 done |
|
338 |
|
339 lemma xzgcd_correct: |
|
340 "0 < n ==> (zgcd m n = k) = (\<exists>s t. xzgcd m n = (k, s, t))" |
|
341 apply (unfold xzgcd_def) |
|
342 apply (rule iffI) |
|
343 apply (rule_tac [2] xzgcd_correct_aux2 [THEN mp, THEN mp]) |
|
344 apply (rule xzgcd_correct_aux1 [THEN mp, THEN mp], auto) |
|
345 done |
|
346 |
|
347 |
|
348 text {* \medskip @{term xzgcd} linear *} |
|
349 |
|
350 lemma xzgcda_linear_aux1: |
|
351 "(a - r * b) * m + (c - r * d) * (n::int) = |
|
352 (a * m + c * n) - r * (b * m + d * n)" |
|
353 by (simp add: zdiff_zmult_distrib zadd_zmult_distrib2 zmult_assoc) |
|
354 |
|
355 lemma xzgcda_linear_aux2: |
|
356 "r' = s' * m + t' * n ==> r = s * m + t * n |
|
357 ==> (r' mod r) = (s' - (r' div r) * s) * m + (t' - (r' div r) * t) * (n::int)" |
|
358 apply (rule trans) |
|
359 apply (rule_tac [2] xzgcda_linear_aux1 [symmetric]) |
|
360 apply (simp add: eq_diff_eq mult_commute) |
|
361 done |
|
362 |
|
363 lemma order_le_neq_implies_less: "(x::'a::order) \<le> y ==> x \<noteq> y ==> x < y" |
|
364 by (rule iffD2 [OF order_less_le conjI]) |
|
365 |
|
366 lemma xzgcda_linear [rule_format]: |
|
367 "0 < r --> xzgcda (m, n, r', r, s', s, t', t) = (rn, sn, tn) --> |
|
368 r' = s' * m + t' * n --> r = s * m + t * n --> rn = sn * m + tn * n" |
|
369 apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and |
|
370 z = s and aa = t' and ab = t in xzgcda.induct) |
|
371 apply (subst xzgcda.simps) |
|
372 apply (simp (no_asm)) |
|
373 apply (rule impI)+ |
|
374 apply (case_tac "r' mod r = 0") |
|
375 apply (simp add: xzgcda.simps, clarify) |
|
376 apply (subgoal_tac "0 < r' mod r") |
|
377 apply (rule_tac [2] order_le_neq_implies_less) |
|
378 apply (rule_tac [2] pos_mod_sign) |
|
379 apply (cut_tac m = m and n = n and r' = r' and r = r and s' = s' and |
|
380 s = s and t' = t' and t = t in xzgcda_linear_aux2, auto) |
|
381 done |
|
382 |
|
383 lemma xzgcd_linear: |
|
384 "0 < n ==> xzgcd m n = (r, s, t) ==> r = s * m + t * n" |
|
385 apply (unfold xzgcd_def) |
|
386 apply (erule xzgcda_linear, assumption, auto) |
|
387 done |
|
388 |
|
389 lemma zgcd_ex_linear: |
|
390 "0 < n ==> zgcd m n = k ==> (\<exists>s t. k = s * m + t * n)" |
|
391 apply (simp add: xzgcd_correct, safe) |
|
392 apply (rule exI)+ |
|
393 apply (erule xzgcd_linear, auto) |
|
394 done |
|
395 |
|
396 lemma zcong_lineq_ex: |
|
397 "0 < n ==> zgcd a n = 1 ==> \<exists>x. [a * x = 1] (mod n)" |
|
398 apply (cut_tac m = a and n = n and k = 1 in zgcd_ex_linear, safe) |
|
399 apply (rule_tac x = s in exI) |
|
400 apply (rule_tac b = "s * a + t * n" in zcong_trans) |
|
401 prefer 2 |
|
402 apply simp |
|
403 apply (unfold zcong_def) |
|
404 apply (simp (no_asm) add: zmult_commute) |
|
405 done |
|
406 |
|
407 lemma zcong_lineq_unique: |
|
408 "0 < n ==> |
|
409 zgcd a n = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)" |
|
410 apply auto |
|
411 apply (rule_tac [2] zcong_zless_imp_eq) |
|
412 apply (tactic {* stac (thm "zcong_cancel2" RS sym) 6 *}) |
|
413 apply (rule_tac [8] zcong_trans) |
|
414 apply (simp_all (no_asm_simp)) |
|
415 prefer 2 |
|
416 apply (simp add: zcong_sym) |
|
417 apply (cut_tac a = a and n = n in zcong_lineq_ex, auto) |
|
418 apply (rule_tac x = "x * b mod n" in exI, safe) |
|
419 apply (simp_all (no_asm_simp)) |
|
420 apply (metis zcong_scalar zcong_zmod zmod_zmult1_eq zmult_1 zmult_assoc) |
|
421 done |
|
422 |
|
423 end |
|