equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Primes.thy |
1 (* Title: HOL/Library/Primes.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Amine Chaieb Christophe Tabacznyj and Lawrence C Paulson |
3 Author: Amine Chaieb, Christophe Tabacznyj and Lawrence C Paulson |
4 Copyright 1996 University of Cambridge |
4 Copyright 1996 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header {* Primality on nat *} |
7 header {* Primality on nat *} |
8 |
8 |
14 coprime :: "nat => nat => bool" where |
14 coprime :: "nat => nat => bool" where |
15 "coprime m n \<longleftrightarrow> (gcd (m, n) = 1)" |
15 "coprime m n \<longleftrightarrow> (gcd (m, n) = 1)" |
16 |
16 |
17 definition |
17 definition |
18 prime :: "nat \<Rightarrow> bool" where |
18 prime :: "nat \<Rightarrow> bool" where |
19 "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))" |
19 [code func del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))" |
20 |
20 |
21 |
21 |
22 lemma two_is_prime: "prime 2" |
22 lemma two_is_prime: "prime 2" |
23 apply (auto simp add: prime_def) |
23 apply (auto simp add: prime_def) |
24 apply (case_tac m) |
24 apply (case_tac m) |