equal
deleted
inserted
replaced
9 theory Primes |
9 theory Primes |
10 imports GCD |
10 imports GCD |
11 begin |
11 begin |
12 |
12 |
13 definition |
13 definition |
14 coprime :: "nat => nat => bool" |
14 coprime :: "nat => nat => bool" where |
15 "coprime m n = (gcd (m, n) = 1)" |
15 "coprime m n = (gcd (m, n) = 1)" |
16 |
16 |
17 prime :: "nat \<Rightarrow> bool" |
17 definition |
|
18 prime :: "nat \<Rightarrow> bool" where |
18 "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))" |
19 "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))" |
19 |
20 |
20 |
21 |
21 lemma two_is_prime: "prime 2" |
22 lemma two_is_prime: "prime 2" |
22 apply (auto simp add: prime_def) |
23 apply (auto simp add: prime_def) |