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