src/HOL/Library/Primes.thy
 author chaieb Mon Jun 11 11:06:04 2007 +0200 (2007-06-11) changeset 23315 df3a7e9ebadb parent 22665 cf152ff55d16 child 23839 d9fa0f457d9a permissions -rw-r--r--
tuned Proof
```     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 (drule_tac x = "gcd (p, n)" in spec)
```
```    31   apply auto
```
```    32   apply (insert gcd_dvd2 [of p n])
```
```    33   apply simp
```
```    34   done
```
```    35
```
```    36 text {*
```
```    37   This theorem leads immediately to a proof of the uniqueness of
```
```    38   factorization.  If @{term p} divides a product of primes then it is
```
```    39   one of those primes.
```
```    40 *}
```
```    41
```
```    42 lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
```
```    43   by (blast intro: relprime_dvd_mult prime_imp_relprime)
```
```    44
```
```    45 lemma prime_dvd_square: "prime p ==> p dvd m^Suc (Suc 0) ==> p dvd m"
```
```    46   by (auto dest: prime_dvd_mult)
```
```    47
```
```    48 lemma prime_dvd_power_two: "prime p ==> p dvd m\<twosuperior> ==> p dvd m"
```
```    49   by (rule prime_dvd_square) (simp_all add: power2_eq_square)
```
```    50
```
```    51 end
```