src/HOL/Library/Primes.thy
 author nipkow Fri Jul 08 11:39:08 2005 +0200 (2005-07-08) changeset 16762 aafd23b47a5d parent 16663 13e9c402308b child 19086 1b3780be6cc2 permissions -rw-r--r--
moved gcd to new GCD.thy
```     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 Main
```
```    11 begin
```
```    12
```
```    13 constdefs
```
```    14   coprime :: "nat => nat => bool"
```
```    15   "coprime m n == gcd (m, n) = 1"
```
```    16
```
```    17   prime :: "nat \<Rightarrow> bool"
```
```    18   "prime p == 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)"
```
```    19
```
```    20
```
```    21 lemma two_is_prime: "prime 2"
```
```    22   apply (auto simp add: prime_def)
```
```    23   apply (case_tac m)
```
```    24    apply (auto dest!: dvd_imp_le)
```
```    25   done
```
```    26
```
```    27 lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd (p, n) = 1"
```
```    28   apply (auto simp add: prime_def)
```
```    29   apply (drule_tac x = "gcd (p, n)" in spec)
```
```    30   apply auto
```
```    31   apply (insert gcd_dvd2 [of p n])
```
```    32   apply simp
```
```    33   done
```
```    34
```
```    35 text {*
```
```    36   This theorem leads immediately to a proof of the uniqueness of
```
```    37   factorization.  If @{term p} divides a product of primes then it is
```
```    38   one of those primes.
```
```    39 *}
```
```    40
```
```    41 lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
```
```    42   by (blast intro: relprime_dvd_mult prime_imp_relprime)
```
```    43
```
```    44 lemma prime_dvd_square: "prime p ==> p dvd m^Suc (Suc 0) ==> p dvd m"
```
```    45   by (auto dest: prime_dvd_mult)
```
```    46
```
```    47 lemma prime_dvd_power_two: "prime p ==> p dvd m\<twosuperior> ==> p dvd m"
```
```    48   by (rule prime_dvd_square) (simp_all add: power2_eq_square)
```
```    49
```
```    50
```
```    51 end
```