equal
deleted
inserted
replaced
6 section\<open>The Divides Relation and Euclid's algorithm for the GCD\<close> |
6 section\<open>The Divides Relation and Euclid's algorithm for the GCD\<close> |
7 |
7 |
8 theory Primes imports ZF begin |
8 theory Primes imports ZF begin |
9 |
9 |
10 definition |
10 definition |
11 divides :: "[i,i]=>o" (infixl "dvd" 50) where |
11 divides :: "[i,i]=>o" (infixl \<open>dvd\<close> 50) where |
12 "m dvd n == m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)" |
12 "m dvd n == m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)" |
13 |
13 |
14 definition |
14 definition |
15 is_gcd :: "[i,i,i]=>o" \<comment> \<open>definition of great common divisor\<close> where |
15 is_gcd :: "[i,i,i]=>o" \<comment> \<open>definition of great common divisor\<close> where |
16 "is_gcd(p,m,n) == ((p dvd m) & (p dvd n)) & |
16 "is_gcd(p,m,n) == ((p dvd m) & (p dvd n)) & |