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