equal
deleted
inserted
replaced
13 coprime :: "nat => nat => bool" where |
13 coprime :: "nat => nat => bool" where |
14 "coprime m n \<longleftrightarrow> gcd m n = 1" |
14 "coprime m n \<longleftrightarrow> gcd m n = 1" |
15 |
15 |
16 definition |
16 definition |
17 prime :: "nat \<Rightarrow> bool" where |
17 prime :: "nat \<Rightarrow> bool" where |
18 [code del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))" |
18 "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))" |
19 |
19 |
20 |
20 |
21 lemma two_is_prime: "prime 2" |
21 lemma two_is_prime: "prime 2" |
22 apply (auto simp add: prime_def) |
22 apply (auto simp add: prime_def) |
23 apply (case_tac m) |
23 apply (case_tac m) |