src/HOL/Library/Primes.thy
 author paulson Wed Jul 18 11:43:06 2007 +0200 (2007-07-18) changeset 23839 d9fa0f457d9a parent 22665 cf152ff55d16 child 25593 0b0df6c8646a permissions -rw-r--r--
tidying using metis
```     1 (*  Title:      HOL/Library/Primes.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Christophe Tabacznyj and Lawrence C Paulson
```
```     4     Copyright   1996  University of Cambridge
```
```     5 *)
```
```     6
```
```     7 header {* Primality on nat *}
```
```     8
```
```     9 theory Primes
```
```    10 imports GCD
```
```    11 begin
```
```    12
```
```    13 definition
```
```    14   coprime :: "nat => nat => bool" where
```
```    15   "coprime m n = (gcd (m, n) = 1)"
```
```    16
```
```    17 definition
```
```    18   prime :: "nat \<Rightarrow> bool" where
```
```    19   "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
```
```    20
```
```    21
```
```    22 lemma two_is_prime: "prime 2"
```
```    23   apply (auto simp add: prime_def)
```
```    24   apply (case_tac m)
```
```    25    apply (auto dest!: dvd_imp_le)
```
```    26   done
```
```    27
```
```    28 lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd (p, n) = 1"
```
```    29   apply (auto simp add: prime_def)
```
```    30   apply (metis One_nat_def gcd_dvd1 gcd_dvd2)
```
```    31   done
```
```    32
```
```    33 text {*
```
```    34   This theorem leads immediately to a proof of the uniqueness of
```
```    35   factorization.  If @{term p} divides a product of primes then it is
```
```    36   one of those primes.
```
```    37 *}
```
```    38
```
```    39 lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
```
```    40   by (blast intro: relprime_dvd_mult prime_imp_relprime)
```
```    41
```
```    42 lemma prime_dvd_square: "prime p ==> p dvd m^Suc (Suc 0) ==> p dvd m"
```
```    43   by (auto dest: prime_dvd_mult)
```
```    44
```
```    45 lemma prime_dvd_power_two: "prime p ==> p dvd m\<twosuperior> ==> p dvd m"
```
```    46   by (rule prime_dvd_square) (simp_all add: power2_eq_square)
```
```    47
```
```    48 end
```