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