6 The "divides" relation, the greatest common divisor and Euclid's algorithm |
6 The "divides" relation, the greatest common divisor and Euclid's algorithm |
7 *) |
7 *) |
8 |
8 |
9 Primes = Arith + |
9 Primes = Arith + |
10 consts |
10 consts |
11 dvd :: [i,i]=>o (infixl 70) |
11 dvd :: [i,i]=>o (infixl 70) |
12 gcd :: [i,i,i]=>o (* great common divisor *) |
12 gcd :: [i,i,i]=>o (* great common divisor *) |
13 egcd :: [i,i]=>i (* gcd by Euclid's algorithm *) |
13 egcd :: [i,i]=>i (* gcd by Euclid's algorithm *) |
14 coprime :: [i,i]=>o (* coprime definition *) |
14 coprime :: [i,i]=>o (* coprime definition *) |
15 prime :: [i]=>o (* prime definition *) |
15 prime :: i=>o (* prime definition *) |
16 |
16 |
17 defs |
17 defs |
18 dvd_def "m dvd n == m:nat & n:nat & (EX k:nat. n = m#*k)" |
18 dvd_def "m dvd n == m:nat & n:nat & (EX k:nat. n = m#*k)" |
19 |
19 |
20 gcd_def "gcd(p,m,n) == ((p dvd m) & (p dvd n)) \ |
20 gcd_def "gcd(p,m,n) == ((p dvd m) & (p dvd n)) & |
21 \ & (ALL d. (d dvd m) & (d dvd n) --> d dvd p)" |
21 (ALL d. (d dvd m) & (d dvd n) --> d dvd p)" |
22 |
22 |
23 egcd_def "egcd(m,n) == \ |
23 egcd_def "egcd(m,n) == |
24 \ transrec(n, %n f. lam m:nat. if(n=0, m, f`(m mod n)`n)) ` m" |
24 transrec(n, %n f. lam m:nat. if(n=0, m, f`(m mod n)`n)) ` m" |
25 |
25 |
26 coprime_def "coprime(m,n) == egcd(m,n) = 1" |
26 coprime_def "coprime(m,n) == egcd(m,n) = 1" |
27 |
27 |
28 prime_def "prime(n) == (1<n) & (ALL m:nat. 1<m & m<n --> ~(m dvd n))" |
28 prime_def "prime(n) == (1<n) & (ALL m:nat. 1<m & m<n --> ~(m dvd n))" |
29 |
29 |