src/HOL/Library/Primes.thy
author wenzelm
Wed Nov 08 23:11:13 2006 +0100 (2006-11-08)
changeset 21256 47195501ecf7
parent 19086 1b3780be6cc2
child 21404 eb85850d3eb7
permissions -rw-r--r--
moved theories Parity, GCD, Binomial to Library;
     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"
    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