27 |
27 |
28 recdef xzgcda |
28 recdef xzgcda |
29 "measure ((\<lambda>(m, n, r', r, s', s, t', t). nat r) |
29 "measure ((\<lambda>(m, n, r', r, s', s, t', t). nat r) |
30 :: int * int * int * int *int * int * int * int => nat)" |
30 :: int * int * int * int *int * int * int * int => nat)" |
31 "xzgcda (m, n, r', r, s', s, t', t) = |
31 "xzgcda (m, n, r', r, s', s, t', t) = |
32 (if r \<le> Numeral0 then (r', s', t') |
32 (if r \<le> 0 then (r', s', t') |
33 else xzgcda (m, n, r, r' mod r, s, s' - (r' div r) * s, t, t' - (r' div r) * t))" |
33 else xzgcda (m, n, r, r' mod r, s, s' - (r' div r) * s, t, t' - (r' div r) * t))" |
34 (hints simp: pos_mod_bound) |
34 (hints simp: pos_mod_bound) |
35 |
35 |
36 constdefs |
36 constdefs |
37 zgcd :: "int * int => int" |
37 zgcd :: "int * int => int" |
38 "zgcd == \<lambda>(x,y). int (gcd (nat (abs x), nat (abs y)))" |
38 "zgcd == \<lambda>(x,y). int (gcd (nat (abs x), nat (abs y)))" |
39 |
39 |
40 defs |
40 defs |
41 xzgcd_def: "xzgcd m n == xzgcda (m, n, m, n, Numeral1, Numeral0, Numeral0, Numeral1)" |
41 xzgcd_def: "xzgcd m n == xzgcda (m, n, m, n, 1, 0, 0, 1)" |
42 zprime_def: "zprime == {p. Numeral1 < p \<and> (\<forall>m. m dvd p --> m = Numeral1 \<or> m = p)}" |
42 zprime_def: "zprime == {p. 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)}" |
43 zcong_def: "[a = b] (mod m) == m dvd (a - b)" |
43 zcong_def: "[a = b] (mod m) == m dvd (a - b)" |
44 |
44 |
45 |
45 |
46 lemma zabs_eq_iff: |
46 lemma zabs_eq_iff: |
47 "(abs (z::int) = w) = (z = w \<and> Numeral0 <= z \<or> z = -w \<and> z < Numeral0)" |
47 "(abs (z::int) = w) = (z = w \<and> 0 <= z \<or> z = -w \<and> z < 0)" |
48 apply (auto simp add: zabs_def) |
48 apply (auto simp add: zabs_def) |
49 done |
49 done |
50 |
50 |
51 |
51 |
52 text {* \medskip @{term gcd} lemmas *} |
52 text {* \medskip @{term gcd} lemmas *} |
62 done |
62 done |
63 |
63 |
64 |
64 |
65 subsection {* Divides relation *} |
65 subsection {* Divides relation *} |
66 |
66 |
67 lemma zdvd_0_right [iff]: "(m::int) dvd Numeral0" |
67 lemma zdvd_0_right [iff]: "(m::int) dvd 0" |
68 apply (unfold dvd_def) |
68 apply (unfold dvd_def) |
69 apply (blast intro: zmult_0_right [symmetric]) |
69 apply (blast intro: zmult_0_right [symmetric]) |
70 done |
70 done |
71 |
71 |
72 lemma zdvd_0_left [iff]: "(Numeral0 dvd (m::int)) = (m = Numeral0)" |
72 lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)" |
73 apply (unfold dvd_def) |
73 apply (unfold dvd_def) |
74 apply auto |
74 apply auto |
75 done |
75 done |
76 |
76 |
77 lemma zdvd_1_left [iff]: "Numeral1 dvd (m::int)" |
77 lemma zdvd_1_left [iff]: "1 dvd (m::int)" |
78 apply (unfold dvd_def) |
78 apply (unfold dvd_def) |
79 apply simp |
79 apply simp |
80 done |
80 done |
81 |
81 |
82 lemma zdvd_refl [simp]: "m dvd (m::int)" |
82 lemma zdvd_refl [simp]: "m dvd (m::int)" |
184 apply (subgoal_tac "k dvd n * (m div n) + m mod n") |
184 apply (subgoal_tac "k dvd n * (m div n) + m mod n") |
185 apply (simp add: zmod_zdiv_equality [symmetric]) |
185 apply (simp add: zmod_zdiv_equality [symmetric]) |
186 apply (simp add: zdvd_zadd zdvd_zmult2) |
186 apply (simp add: zdvd_zadd zdvd_zmult2) |
187 done |
187 done |
188 |
188 |
189 lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = Numeral0)" |
189 lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = 0)" |
190 apply (unfold dvd_def) |
190 apply (unfold dvd_def) |
191 apply auto |
191 apply auto |
192 done |
192 done |
193 |
193 |
194 lemma zdvd_not_zless: "Numeral0 < m ==> m < n ==> \<not> n dvd (m::int)" |
194 lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)" |
195 apply (unfold dvd_def) |
195 apply (unfold dvd_def) |
196 apply auto |
196 apply auto |
197 apply (subgoal_tac "Numeral0 < n") |
197 apply (subgoal_tac "0 < n") |
198 prefer 2 |
198 prefer 2 |
199 apply (blast intro: zless_trans) |
199 apply (blast intro: zless_trans) |
200 apply (simp add: int_0_less_mult_iff) |
200 apply (simp add: int_0_less_mult_iff) |
201 apply (subgoal_tac "n * k < n * Numeral1") |
201 apply (subgoal_tac "n * k < n * 1") |
202 apply (drule zmult_zless_cancel1 [THEN iffD1]) |
202 apply (drule zmult_zless_cancel1 [THEN iffD1]) |
203 apply auto |
203 apply auto |
204 done |
204 done |
205 |
205 |
206 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" |
206 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" |
219 apply (cut_tac k = m in int_less_0_conv) |
219 apply (cut_tac k = m in int_less_0_conv) |
220 apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff |
220 apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff |
221 nat_mult_distrib [symmetric] nat_eq_iff2) |
221 nat_mult_distrib [symmetric] nat_eq_iff2) |
222 done |
222 done |
223 |
223 |
224 lemma nat_dvd_iff: "(nat z dvd m) = (if Numeral0 \<le> z then (z dvd int m) else m = 0)" |
224 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)" |
225 apply (auto simp add: dvd_def zmult_int [symmetric]) |
225 apply (auto simp add: dvd_def zmult_int [symmetric]) |
226 apply (rule_tac x = "nat k" in exI) |
226 apply (rule_tac x = "nat k" in exI) |
227 apply (cut_tac k = m in int_less_0_conv) |
227 apply (cut_tac k = m in int_less_0_conv) |
228 apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff |
228 apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff |
229 nat_mult_distrib [symmetric] nat_eq_iff2) |
229 nat_mult_distrib [symmetric] nat_eq_iff2) |
259 |
259 |
260 lemma zgcd_zminus2 [simp]: "zgcd (m, -n) = zgcd (m, n)" |
260 lemma zgcd_zminus2 [simp]: "zgcd (m, -n) = zgcd (m, n)" |
261 apply (simp add: zgcd_def) |
261 apply (simp add: zgcd_def) |
262 done |
262 done |
263 |
263 |
264 lemma zgcd_non_0: "Numeral0 < n ==> zgcd (m, n) = zgcd (n, m mod n)" |
264 lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)" |
265 apply (frule_tac b = n and a = m in pos_mod_sign) |
265 apply (frule_tac b = n and a = m in pos_mod_sign) |
266 apply (simp add: zgcd_def zabs_def nat_mod_distrib) |
266 apply (simp add: zgcd_def zabs_def nat_mod_distrib) |
267 apply (cut_tac a = "-m" and b = n in zmod_zminus1_eq_if) |
267 apply (cut_tac a = "-m" and b = n in zmod_zminus1_eq_if) |
268 apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if) |
268 apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if) |
269 apply (frule_tac a = m in pos_mod_bound) |
269 apply (frule_tac a = m in pos_mod_bound) |
271 apply (rule gcd_diff2) |
271 apply (rule gcd_diff2) |
272 apply (simp add: nat_le_eq_zle) |
272 apply (simp add: nat_le_eq_zle) |
273 done |
273 done |
274 |
274 |
275 lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)" |
275 lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)" |
276 apply (tactic {* zdiv_undefined_case_tac "n = Numeral0" 1 *}) |
276 apply (tactic {* zdiv_undefined_case_tac "n = 0" 1 *}) |
277 apply (auto simp add: linorder_neq_iff zgcd_non_0) |
277 apply (auto simp add: linorder_neq_iff zgcd_non_0) |
278 apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0) |
278 apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0) |
279 apply auto |
279 apply auto |
280 done |
280 done |
281 |
281 |
282 lemma zgcd_1 [simp]: "zgcd (m, Numeral1) = Numeral1" |
282 lemma zgcd_1 [simp]: "zgcd (m, 1) = 1" |
283 apply (simp add: zgcd_def zabs_def) |
283 apply (simp add: zgcd_def zabs_def) |
284 done |
284 done |
285 |
285 |
286 lemma zgcd_0_1_iff [simp]: "(zgcd (Numeral0, m) = Numeral1) = (abs m = Numeral1)" |
286 lemma zgcd_0_1_iff [simp]: "(zgcd (0, m) = 1) = (abs m = 1)" |
287 apply (simp add: zgcd_def zabs_def) |
287 apply (simp add: zgcd_def zabs_def) |
288 done |
288 done |
289 |
289 |
290 lemma zgcd_zdvd1 [iff]: "zgcd (m, n) dvd m" |
290 lemma zgcd_zdvd1 [iff]: "zgcd (m, n) dvd m" |
291 apply (simp add: zgcd_def zabs_def int_dvd_iff) |
291 apply (simp add: zgcd_def zabs_def int_dvd_iff) |
301 |
301 |
302 lemma zgcd_commute: "zgcd (m, n) = zgcd (n, m)" |
302 lemma zgcd_commute: "zgcd (m, n) = zgcd (n, m)" |
303 apply (simp add: zgcd_def gcd_commute) |
303 apply (simp add: zgcd_def gcd_commute) |
304 done |
304 done |
305 |
305 |
306 lemma zgcd_1_left [simp]: "zgcd (Numeral1, m) = Numeral1" |
306 lemma zgcd_1_left [simp]: "zgcd (1, m) = 1" |
307 apply (simp add: zgcd_def gcd_1_left) |
307 apply (simp add: zgcd_def gcd_1_left) |
308 done |
308 done |
309 |
309 |
310 lemma zgcd_assoc: "zgcd (zgcd (k, m), n) = zgcd (k, zgcd (m, n))" |
310 lemma zgcd_assoc: "zgcd (zgcd (k, m), n) = zgcd (k, zgcd (m, n))" |
311 apply (simp add: zgcd_def gcd_assoc) |
311 apply (simp add: zgcd_def gcd_assoc) |
318 done |
318 done |
319 |
319 |
320 lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute |
320 lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute |
321 -- {* addition is an AC-operator *} |
321 -- {* addition is an AC-operator *} |
322 |
322 |
323 lemma zgcd_zmult_distrib2: "Numeral0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)" |
323 lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)" |
324 apply (simp del: zmult_zminus_right |
324 apply (simp del: zmult_zminus_right |
325 add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def |
325 add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def |
326 zmult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric]) |
326 zmult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric]) |
327 done |
327 done |
328 |
328 |
329 lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)" |
329 lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)" |
330 apply (simp add: zabs_def zgcd_zmult_distrib2) |
330 apply (simp add: zabs_def zgcd_zmult_distrib2) |
331 done |
331 done |
332 |
332 |
333 lemma zgcd_self [simp]: "Numeral0 \<le> m ==> zgcd (m, m) = m" |
333 lemma zgcd_self [simp]: "0 \<le> m ==> zgcd (m, m) = m" |
334 apply (cut_tac k = m and m = "Numeral1" and n = "Numeral1" in zgcd_zmult_distrib2) |
334 apply (cut_tac k = m and m = "1" and n = "1" in zgcd_zmult_distrib2) |
335 apply simp_all |
335 apply simp_all |
336 done |
336 done |
337 |
337 |
338 lemma zgcd_zmult_eq_self [simp]: "Numeral0 \<le> k ==> zgcd (k, k * n) = k" |
338 lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd (k, k * n) = k" |
339 apply (cut_tac k = k and m = "Numeral1" and n = n in zgcd_zmult_distrib2) |
339 apply (cut_tac k = k and m = "1" and n = n in zgcd_zmult_distrib2) |
340 apply simp_all |
340 apply simp_all |
341 done |
341 done |
342 |
342 |
343 lemma zgcd_zmult_eq_self2 [simp]: "Numeral0 \<le> k ==> zgcd (k * n, k) = k" |
343 lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n, k) = k" |
344 apply (cut_tac k = k and m = n and n = "Numeral1" in zgcd_zmult_distrib2) |
344 apply (cut_tac k = k and m = n and n = "1" in zgcd_zmult_distrib2) |
345 apply simp_all |
345 apply simp_all |
346 done |
346 done |
347 |
347 |
348 lemma aux: "zgcd (n, k) = Numeral1 ==> k dvd m * n ==> Numeral0 \<le> m ==> k dvd m" |
348 lemma aux: "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m" |
349 apply (subgoal_tac "m = zgcd (m * n, m * k)") |
349 apply (subgoal_tac "m = zgcd (m * n, m * k)") |
350 apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2]) |
350 apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2]) |
351 apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff) |
351 apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff) |
352 done |
352 done |
353 |
353 |
354 lemma zrelprime_zdvd_zmult: "zgcd (n, k) = Numeral1 ==> k dvd m * n ==> k dvd m" |
354 lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m" |
355 apply (case_tac "Numeral0 \<le> m") |
355 apply (case_tac "0 \<le> m") |
356 apply (blast intro: aux) |
356 apply (blast intro: aux) |
357 apply (subgoal_tac "k dvd -m") |
357 apply (subgoal_tac "k dvd -m") |
358 apply (rule_tac [2] aux) |
358 apply (rule_tac [2] aux) |
359 apply auto |
359 apply auto |
360 done |
360 done |
361 |
361 |
362 lemma zprime_imp_zrelprime: |
362 lemma zprime_imp_zrelprime: |
363 "p \<in> zprime ==> \<not> p dvd n ==> zgcd (n, p) = Numeral1" |
363 "p \<in> zprime ==> \<not> p dvd n ==> zgcd (n, p) = 1" |
364 apply (unfold zprime_def) |
364 apply (unfold zprime_def) |
365 apply auto |
365 apply auto |
366 done |
366 done |
367 |
367 |
368 lemma zless_zprime_imp_zrelprime: |
368 lemma zless_zprime_imp_zrelprime: |
369 "p \<in> zprime ==> Numeral0 < n ==> n < p ==> zgcd (n, p) = Numeral1" |
369 "p \<in> zprime ==> 0 < n ==> n < p ==> zgcd (n, p) = 1" |
370 apply (erule zprime_imp_zrelprime) |
370 apply (erule zprime_imp_zrelprime) |
371 apply (erule zdvd_not_zless) |
371 apply (erule zdvd_not_zless) |
372 apply assumption |
372 apply assumption |
373 done |
373 done |
374 |
374 |
375 lemma zprime_zdvd_zmult: |
375 lemma zprime_zdvd_zmult: |
376 "Numeral0 \<le> (m::int) ==> p \<in> zprime ==> p dvd m * n ==> p dvd m \<or> p dvd n" |
376 "0 \<le> (m::int) ==> p \<in> zprime ==> p dvd m * n ==> p dvd m \<or> p dvd n" |
377 apply safe |
377 apply safe |
378 apply (rule zrelprime_zdvd_zmult) |
378 apply (rule zrelprime_zdvd_zmult) |
379 apply (rule zprime_imp_zrelprime) |
379 apply (rule zprime_imp_zrelprime) |
380 apply auto |
380 apply auto |
381 done |
381 done |
390 apply (simp add: zgcd_greatest_iff) |
390 apply (simp add: zgcd_greatest_iff) |
391 apply (blast intro: zdvd_trans) |
391 apply (blast intro: zdvd_trans) |
392 done |
392 done |
393 |
393 |
394 lemma zgcd_zmult_zdvd_zgcd: |
394 lemma zgcd_zmult_zdvd_zgcd: |
395 "zgcd (k, n) = Numeral1 ==> zgcd (k * m, n) dvd zgcd (m, n)" |
395 "zgcd (k, n) = 1 ==> zgcd (k * m, n) dvd zgcd (m, n)" |
396 apply (simp add: zgcd_greatest_iff) |
396 apply (simp add: zgcd_greatest_iff) |
397 apply (rule_tac n = k in zrelprime_zdvd_zmult) |
397 apply (rule_tac n = k in zrelprime_zdvd_zmult) |
398 prefer 2 |
398 prefer 2 |
399 apply (simp add: zmult_commute) |
399 apply (simp add: zmult_commute) |
400 apply (subgoal_tac "zgcd (k, zgcd (k * m, n)) = zgcd (k * m, zgcd (k, n))") |
400 apply (subgoal_tac "zgcd (k, zgcd (k * m, n)) = zgcd (k * m, zgcd (k, n))") |
401 apply simp |
401 apply simp |
402 apply (simp (no_asm) add: zgcd_ac) |
402 apply (simp (no_asm) add: zgcd_ac) |
403 done |
403 done |
404 |
404 |
405 lemma zgcd_zmult_cancel: "zgcd (k, n) = Numeral1 ==> zgcd (k * m, n) = zgcd (m, n)" |
405 lemma zgcd_zmult_cancel: "zgcd (k, n) = 1 ==> zgcd (k * m, n) = zgcd (m, n)" |
406 apply (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel) |
406 apply (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel) |
407 done |
407 done |
408 |
408 |
409 lemma zgcd_zgcd_zmult: |
409 lemma zgcd_zgcd_zmult: |
410 "zgcd (k, m) = Numeral1 ==> zgcd (n, m) = Numeral1 ==> zgcd (k * n, m) = Numeral1" |
410 "zgcd (k, m) = 1 ==> zgcd (n, m) = 1 ==> zgcd (k * n, m) = 1" |
411 apply (simp (no_asm_simp) add: zgcd_zmult_cancel) |
411 apply (simp (no_asm_simp) add: zgcd_zmult_cancel) |
412 done |
412 done |
413 |
413 |
414 lemma zdvd_iff_zgcd: "Numeral0 < m ==> (m dvd n) = (zgcd (n, m) = m)" |
414 lemma zdvd_iff_zgcd: "0 < m ==> (m dvd n) = (zgcd (n, m) = m)" |
415 apply safe |
415 apply safe |
416 apply (rule_tac [2] n = "zgcd (n, m)" in zdvd_trans) |
416 apply (rule_tac [2] n = "zgcd (n, m)" in zdvd_trans) |
417 apply (rule_tac [3] zgcd_zdvd1) |
417 apply (rule_tac [3] zgcd_zdvd1) |
418 apply simp_all |
418 apply simp_all |
419 apply (unfold dvd_def) |
419 apply (unfold dvd_def) |
492 apply (rule zdvd_zdiff) |
492 apply (rule zdvd_zdiff) |
493 apply simp_all |
493 apply simp_all |
494 done |
494 done |
495 |
495 |
496 lemma zcong_square: |
496 lemma zcong_square: |
497 "p \<in> zprime ==> Numeral0 < a ==> [a * a = Numeral1] (mod p) |
497 "p \<in> zprime ==> 0 < a ==> [a * a = 1] (mod p) |
498 ==> [a = Numeral1] (mod p) \<or> [a = p - Numeral1] (mod p)" |
498 ==> [a = 1] (mod p) \<or> [a = p - 1] (mod p)" |
499 apply (unfold zcong_def) |
499 apply (unfold zcong_def) |
500 apply (rule zprime_zdvd_zmult) |
500 apply (rule zprime_zdvd_zmult) |
501 apply (rule_tac [3] s = "a * a - Numeral1 + p * (Numeral1 - a)" in subst) |
501 apply (rule_tac [3] s = "a * a - 1 + p * (1 - a)" in subst) |
502 prefer 4 |
502 prefer 4 |
503 apply (simp add: zdvd_reduce) |
503 apply (simp add: zdvd_reduce) |
504 apply (simp_all add: zdiff_zmult_distrib zmult_commute zdiff_zmult_distrib2) |
504 apply (simp_all add: zdiff_zmult_distrib zmult_commute zdiff_zmult_distrib2) |
505 done |
505 done |
506 |
506 |
507 lemma zcong_cancel: |
507 lemma zcong_cancel: |
508 "Numeral0 \<le> m ==> |
508 "0 \<le> m ==> |
509 zgcd (k, m) = Numeral1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)" |
509 zgcd (k, m) = 1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)" |
510 apply safe |
510 apply safe |
511 prefer 2 |
511 prefer 2 |
512 apply (blast intro: zcong_scalar) |
512 apply (blast intro: zcong_scalar) |
513 apply (case_tac "b < a") |
513 apply (case_tac "b < a") |
514 prefer 2 |
514 prefer 2 |
521 apply (subst zdvd_zminus_iff) |
521 apply (subst zdvd_zminus_iff) |
522 apply assumption |
522 apply assumption |
523 done |
523 done |
524 |
524 |
525 lemma zcong_cancel2: |
525 lemma zcong_cancel2: |
526 "Numeral0 \<le> m ==> |
526 "0 \<le> m ==> |
527 zgcd (k, m) = Numeral1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)" |
527 zgcd (k, m) = 1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)" |
528 apply (simp add: zmult_commute zcong_cancel) |
528 apply (simp add: zmult_commute zcong_cancel) |
529 done |
529 done |
530 |
530 |
531 lemma zcong_zgcd_zmult_zmod: |
531 lemma zcong_zgcd_zmult_zmod: |
532 "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd (m, n) = Numeral1 |
532 "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd (m, n) = 1 |
533 ==> [a = b] (mod m * n)" |
533 ==> [a = b] (mod m * n)" |
534 apply (unfold zcong_def dvd_def) |
534 apply (unfold zcong_def dvd_def) |
535 apply auto |
535 apply auto |
536 apply (subgoal_tac "m dvd n * ka") |
536 apply (subgoal_tac "m dvd n * ka") |
537 apply (subgoal_tac "m dvd ka") |
537 apply (subgoal_tac "m dvd ka") |
538 apply (case_tac [2] "Numeral0 \<le> ka") |
538 apply (case_tac [2] "0 \<le> ka") |
539 prefer 3 |
539 prefer 3 |
540 apply (subst zdvd_zminus_iff [symmetric]) |
540 apply (subst zdvd_zminus_iff [symmetric]) |
541 apply (rule_tac n = n in zrelprime_zdvd_zmult) |
541 apply (rule_tac n = n in zrelprime_zdvd_zmult) |
542 apply (simp add: zgcd_commute) |
542 apply (simp add: zgcd_commute) |
543 apply (simp add: zmult_commute zdvd_zminus_iff) |
543 apply (simp add: zmult_commute zdvd_zminus_iff) |
564 apply (rule_tac [2] mod_pos_pos_trivial) |
564 apply (rule_tac [2] mod_pos_pos_trivial) |
565 apply auto |
565 apply auto |
566 done |
566 done |
567 |
567 |
568 lemma zcong_square_zless: |
568 lemma zcong_square_zless: |
569 "p \<in> zprime ==> Numeral0 < a ==> a < p ==> |
569 "p \<in> zprime ==> 0 < a ==> a < p ==> |
570 [a * a = Numeral1] (mod p) ==> a = Numeral1 \<or> a = p - Numeral1" |
570 [a * a = 1] (mod p) ==> a = 1 \<or> a = p - 1" |
571 apply (cut_tac p = p and a = a in zcong_square) |
571 apply (cut_tac p = p and a = a in zcong_square) |
572 apply (simp add: zprime_def) |
572 apply (simp add: zprime_def) |
573 apply (auto intro: zcong_zless_imp_eq) |
573 apply (auto intro: zcong_zless_imp_eq) |
574 done |
574 done |
575 |
575 |
576 lemma zcong_not: |
576 lemma zcong_not: |
577 "Numeral0 < a ==> a < m ==> Numeral0 < b ==> b < a ==> \<not> [a = b] (mod m)" |
577 "0 < a ==> a < m ==> 0 < b ==> b < a ==> \<not> [a = b] (mod m)" |
578 apply (unfold zcong_def) |
578 apply (unfold zcong_def) |
579 apply (rule zdvd_not_zless) |
579 apply (rule zdvd_not_zless) |
580 apply auto |
580 apply auto |
581 done |
581 done |
582 |
582 |
583 lemma zcong_zless_0: |
583 lemma zcong_zless_0: |
584 "Numeral0 \<le> a ==> a < m ==> [a = Numeral0] (mod m) ==> a = Numeral0" |
584 "0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0" |
585 apply (unfold zcong_def dvd_def) |
585 apply (unfold zcong_def dvd_def) |
586 apply auto |
586 apply auto |
587 apply (subgoal_tac "Numeral0 < m") |
587 apply (subgoal_tac "0 < m") |
588 apply (rotate_tac -1) |
588 apply (rotate_tac -1) |
589 apply (simp add: int_0_le_mult_iff) |
589 apply (simp add: int_0_le_mult_iff) |
590 apply (subgoal_tac "m * k < m * Numeral1") |
590 apply (subgoal_tac "m * k < m * 1") |
591 apply (drule zmult_zless_cancel1 [THEN iffD1]) |
591 apply (drule zmult_zless_cancel1 [THEN iffD1]) |
592 apply (auto simp add: linorder_neq_iff) |
592 apply (auto simp add: linorder_neq_iff) |
593 done |
593 done |
594 |
594 |
595 lemma zcong_zless_unique: |
595 lemma zcong_zless_unique: |
596 "Numeral0 < m ==> (\<exists>!b. Numeral0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
596 "0 < m ==> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
597 apply auto |
597 apply auto |
598 apply (subgoal_tac [2] "[b = y] (mod m)") |
598 apply (subgoal_tac [2] "[b = y] (mod m)") |
599 apply (case_tac [2] "b = Numeral0") |
599 apply (case_tac [2] "b = 0") |
600 apply (case_tac [3] "y = Numeral0") |
600 apply (case_tac [3] "y = 0") |
601 apply (auto intro: zcong_trans zcong_zless_0 zcong_zless_imp_eq order_less_le |
601 apply (auto intro: zcong_trans zcong_zless_0 zcong_zless_imp_eq order_less_le |
602 simp add: zcong_sym) |
602 simp add: zcong_sym) |
603 apply (unfold zcong_def dvd_def) |
603 apply (unfold zcong_def dvd_def) |
604 apply (rule_tac x = "a mod m" in exI) |
604 apply (rule_tac x = "a mod m" in exI) |
605 apply (auto simp add: pos_mod_sign pos_mod_bound) |
605 apply (auto simp add: pos_mod_sign pos_mod_bound) |
657 |
657 |
658 lemma zcong_zminus [iff]: "[a = b] (mod -m) = [a = b] (mod m)" |
658 lemma zcong_zminus [iff]: "[a = b] (mod -m) = [a = b] (mod m)" |
659 apply (auto simp add: zcong_def) |
659 apply (auto simp add: zcong_def) |
660 done |
660 done |
661 |
661 |
662 lemma zcong_zero [iff]: "[a = b] (mod Numeral0) = (a = b)" |
662 lemma zcong_zero [iff]: "[a = b] (mod 0) = (a = b)" |
663 apply (auto simp add: zcong_def) |
663 apply (auto simp add: zcong_def) |
664 done |
664 done |
665 |
665 |
666 lemma "[a = b] (mod m) = (a mod m = b mod m)" |
666 lemma "[a = b] (mod m) = (a mod m = b mod m)" |
667 apply (tactic {* zdiv_undefined_case_tac "m = Numeral0" 1 *}) |
667 apply (tactic {* zdiv_undefined_case_tac "m = 0" 1 *}) |
668 apply (case_tac "Numeral0 < m") |
668 apply (case_tac "0 < m") |
669 apply (simp add: zcong_zmod_eq) |
669 apply (simp add: zcong_zmod_eq) |
670 apply (rule_tac t = m in zminus_zminus [THEN subst]) |
670 apply (rule_tac t = m in zminus_zminus [THEN subst]) |
671 apply (subst zcong_zminus) |
671 apply (subst zcong_zminus) |
672 apply (subst zcong_zmod_eq) |
672 apply (subst zcong_zmod_eq) |
673 apply arith |
673 apply arith |
694 subsection {* Extended GCD *} |
694 subsection {* Extended GCD *} |
695 |
695 |
696 declare xzgcda.simps [simp del] |
696 declare xzgcda.simps [simp del] |
697 |
697 |
698 lemma aux1: |
698 lemma aux1: |
699 "zgcd (r', r) = k --> Numeral0 < r --> |
699 "zgcd (r', r) = k --> 0 < r --> |
700 (\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))" |
700 (\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))" |
701 apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and |
701 apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and |
702 z = s and aa = t' and ab = t in xzgcda.induct) |
702 z = s and aa = t' and ab = t in xzgcda.induct) |
703 apply (subst zgcd_eq) |
703 apply (subst zgcd_eq) |
704 apply (subst xzgcda.simps) |
704 apply (subst xzgcda.simps) |
705 apply auto |
705 apply auto |
706 apply (case_tac "r' mod r = Numeral0") |
706 apply (case_tac "r' mod r = 0") |
707 prefer 2 |
707 prefer 2 |
708 apply (frule_tac a = "r'" in pos_mod_sign) |
708 apply (frule_tac a = "r'" in pos_mod_sign) |
709 apply auto |
709 apply auto |
710 apply arith |
710 apply arith |
711 apply (rule exI) |
711 apply (rule exI) |
714 apply auto |
714 apply auto |
715 apply (simp add: zabs_def) |
715 apply (simp add: zabs_def) |
716 done |
716 done |
717 |
717 |
718 lemma aux2: |
718 lemma aux2: |
719 "(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> Numeral0 < r --> |
719 "(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> 0 < r --> |
720 zgcd (r', r) = k" |
720 zgcd (r', r) = k" |
721 apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and |
721 apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and |
722 z = s and aa = t' and ab = t in xzgcda.induct) |
722 z = s and aa = t' and ab = t in xzgcda.induct) |
723 apply (subst zgcd_eq) |
723 apply (subst zgcd_eq) |
724 apply (subst xzgcda.simps) |
724 apply (subst xzgcda.simps) |
725 apply (auto simp add: linorder_not_le) |
725 apply (auto simp add: linorder_not_le) |
726 apply (case_tac "r' mod r = Numeral0") |
726 apply (case_tac "r' mod r = 0") |
727 prefer 2 |
727 prefer 2 |
728 apply (frule_tac a = "r'" in pos_mod_sign) |
728 apply (frule_tac a = "r'" in pos_mod_sign) |
729 apply auto |
729 apply auto |
730 apply arith |
730 apply arith |
731 apply (erule_tac P = "xzgcda ?u = ?v" in rev_mp) |
731 apply (erule_tac P = "xzgcda ?u = ?v" in rev_mp) |
766 |
766 |
767 lemma order_le_neq_implies_less: "(x::'a::order) \<le> y ==> x \<noteq> y ==> x < y" |
767 lemma order_le_neq_implies_less: "(x::'a::order) \<le> y ==> x \<noteq> y ==> x < y" |
768 by (rule iffD2 [OF order_less_le conjI]) |
768 by (rule iffD2 [OF order_less_le conjI]) |
769 |
769 |
770 lemma xzgcda_linear [rule_format]: |
770 lemma xzgcda_linear [rule_format]: |
771 "Numeral0 < r --> xzgcda (m, n, r', r, s', s, t', t) = (rn, sn, tn) --> |
771 "0 < r --> xzgcda (m, n, r', r, s', s, t', t) = (rn, sn, tn) --> |
772 r' = s' * m + t' * n --> r = s * m + t * n --> rn = sn * m + tn * n" |
772 r' = s' * m + t' * n --> r = s * m + t * n --> rn = sn * m + tn * n" |
773 apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and |
773 apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and |
774 z = s and aa = t' and ab = t in xzgcda.induct) |
774 z = s and aa = t' and ab = t in xzgcda.induct) |
775 apply (subst xzgcda.simps) |
775 apply (subst xzgcda.simps) |
776 apply (simp (no_asm)) |
776 apply (simp (no_asm)) |
777 apply (rule impI)+ |
777 apply (rule impI)+ |
778 apply (case_tac "r' mod r = Numeral0") |
778 apply (case_tac "r' mod r = 0") |
779 apply (simp add: xzgcda.simps) |
779 apply (simp add: xzgcda.simps) |
780 apply clarify |
780 apply clarify |
781 apply (subgoal_tac "Numeral0 < r' mod r") |
781 apply (subgoal_tac "0 < r' mod r") |
782 apply (rule_tac [2] order_le_neq_implies_less) |
782 apply (rule_tac [2] order_le_neq_implies_less) |
783 apply (rule_tac [2] pos_mod_sign) |
783 apply (rule_tac [2] pos_mod_sign) |
784 apply (cut_tac m = m and n = n and r' = r' and r = r and s' = s' and |
784 apply (cut_tac m = m and n = n and r' = r' and r = r and s' = s' and |
785 s = s and t' = t' and t = t in aux) |
785 s = s and t' = t' and t = t in aux) |
786 apply auto |
786 apply auto |
787 done |
787 done |
788 |
788 |
789 lemma xzgcd_linear: |
789 lemma xzgcd_linear: |
790 "Numeral0 < n ==> xzgcd m n = (r, s, t) ==> r = s * m + t * n" |
790 "0 < n ==> xzgcd m n = (r, s, t) ==> r = s * m + t * n" |
791 apply (unfold xzgcd_def) |
791 apply (unfold xzgcd_def) |
792 apply (erule xzgcda_linear) |
792 apply (erule xzgcda_linear) |
793 apply assumption |
793 apply assumption |
794 apply auto |
794 apply auto |
795 done |
795 done |
796 |
796 |
797 lemma zgcd_ex_linear: |
797 lemma zgcd_ex_linear: |
798 "Numeral0 < n ==> zgcd (m, n) = k ==> (\<exists>s t. k = s * m + t * n)" |
798 "0 < n ==> zgcd (m, n) = k ==> (\<exists>s t. k = s * m + t * n)" |
799 apply (simp add: xzgcd_correct) |
799 apply (simp add: xzgcd_correct) |
800 apply safe |
800 apply safe |
801 apply (rule exI)+ |
801 apply (rule exI)+ |
802 apply (erule xzgcd_linear) |
802 apply (erule xzgcd_linear) |
803 apply auto |
803 apply auto |
804 done |
804 done |
805 |
805 |
806 lemma zcong_lineq_ex: |
806 lemma zcong_lineq_ex: |
807 "Numeral0 < n ==> zgcd (a, n) = Numeral1 ==> \<exists>x. [a * x = Numeral1] (mod n)" |
807 "0 < n ==> zgcd (a, n) = 1 ==> \<exists>x. [a * x = 1] (mod n)" |
808 apply (cut_tac m = a and n = n and k = "Numeral1" in zgcd_ex_linear) |
808 apply (cut_tac m = a and n = n and k = "1" in zgcd_ex_linear) |
809 apply safe |
809 apply safe |
810 apply (rule_tac x = s in exI) |
810 apply (rule_tac x = s in exI) |
811 apply (rule_tac b = "s * a + t * n" in zcong_trans) |
811 apply (rule_tac b = "s * a + t * n" in zcong_trans) |
812 prefer 2 |
812 prefer 2 |
813 apply simp |
813 apply simp |
814 apply (unfold zcong_def) |
814 apply (unfold zcong_def) |
815 apply (simp (no_asm) add: zmult_commute zdvd_zminus_iff) |
815 apply (simp (no_asm) add: zmult_commute zdvd_zminus_iff) |
816 done |
816 done |
817 |
817 |
818 lemma zcong_lineq_unique: |
818 lemma zcong_lineq_unique: |
819 "Numeral0 < n ==> |
819 "0 < n ==> |
820 zgcd (a, n) = Numeral1 ==> \<exists>!x. Numeral0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)" |
820 zgcd (a, n) = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)" |
821 apply auto |
821 apply auto |
822 apply (rule_tac [2] zcong_zless_imp_eq) |
822 apply (rule_tac [2] zcong_zless_imp_eq) |
823 apply (tactic {* stac (thm "zcong_cancel2" RS sym) 6 *}) |
823 apply (tactic {* stac (thm "zcong_cancel2" RS sym) 6 *}) |
824 apply (rule_tac [8] zcong_trans) |
824 apply (rule_tac [8] zcong_trans) |
825 apply (simp_all (no_asm_simp)) |
825 apply (simp_all (no_asm_simp)) |