29 (if r \<le> 0 then (r', s', t') |
29 (if r \<le> 0 then (r', s', t') |
30 else xzgcda (m, n, r, r' mod r, |
30 else xzgcda (m, n, r, r' mod r, |
31 s, s' - (r' div r) * s, |
31 s, s' - (r' div r) * s, |
32 t, t' - (r' div r) * t))" |
32 t, t' - (r' div r) * t))" |
33 |
33 |
34 constdefs |
34 definition |
35 zgcd :: "int * int => int" |
35 zgcd :: "int * int => int" |
36 "zgcd == \<lambda>(x,y). int (gcd (nat (abs x), nat (abs y)))" |
36 "zgcd = (\<lambda>(x,y). int (gcd (nat (abs x), nat (abs y))))" |
37 |
37 |
38 zprime :: "int \<Rightarrow> bool" |
38 zprime :: "int \<Rightarrow> bool" |
39 "zprime p == 1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p)" |
39 "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))" |
40 |
40 |
41 xzgcd :: "int => int => int * int * int" |
41 xzgcd :: "int => int => int * int * int" |
42 "xzgcd m n == xzgcda (m, n, m, n, 1, 0, 0, 1)" |
42 "xzgcd m n = xzgcda (m, n, m, n, 1, 0, 0, 1)" |
43 |
43 |
44 zcong :: "int => int => int => bool" ("(1[_ = _] '(mod _'))") |
44 zcong :: "int => int => int => bool" ("(1[_ = _] '(mod _'))") |
45 "[a = b] (mod m) == m dvd (a - b)" |
45 "[a = b] (mod m) = (m dvd (a - b))" |
46 |
46 |
47 |
47 |
48 |
48 |
49 text {* \medskip @{term gcd} lemmas *} |
49 text {* \medskip @{term gcd} lemmas *} |
50 |
50 |