src/HOL/Library/Primes.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 21256 47195501ecf7
child 22665 cf152ff55d16
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
wenzelm@11368
     1
(*  Title:      HOL/Library/Primes.thy
paulson@11363
     2
    ID:         $Id$
paulson@11363
     3
    Author:     Christophe Tabacznyj and Lawrence C Paulson
paulson@11363
     4
    Copyright   1996  University of Cambridge
paulson@11363
     5
*)
paulson@11363
     6
nipkow@16762
     7
header {* Primality on nat *}
paulson@11363
     8
nipkow@15131
     9
theory Primes
wenzelm@21256
    10
imports GCD
nipkow@15131
    11
begin
paulson@11363
    12
wenzelm@19086
    13
definition
wenzelm@21404
    14
  coprime :: "nat => nat => bool" where
wenzelm@19086
    15
  "coprime m n = (gcd (m, n) = 1)"
paulson@11363
    16
wenzelm@21404
    17
definition
wenzelm@21404
    18
  prime :: "nat \<Rightarrow> bool" where
wenzelm@19086
    19
  "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
paulson@11363
    20
paulson@11363
    21
nipkow@16762
    22
lemma two_is_prime: "prime 2"
nipkow@16762
    23
  apply (auto simp add: prime_def)
nipkow@16762
    24
  apply (case_tac m)
nipkow@16762
    25
   apply (auto dest!: dvd_imp_le)
paulson@11363
    26
  done
paulson@11363
    27
nipkow@16663
    28
lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd (p, n) = 1"
paulson@11363
    29
  apply (auto simp add: prime_def)
paulson@11363
    30
  apply (drule_tac x = "gcd (p, n)" in spec)
paulson@11363
    31
  apply auto
paulson@11363
    32
  apply (insert gcd_dvd2 [of p n])
paulson@11363
    33
  apply simp
paulson@11363
    34
  done
paulson@11363
    35
paulson@11363
    36
text {*
paulson@11363
    37
  This theorem leads immediately to a proof of the uniqueness of
paulson@11363
    38
  factorization.  If @{term p} divides a product of primes then it is
paulson@11363
    39
  one of those primes.
paulson@11363
    40
*}
paulson@11363
    41
nipkow@16663
    42
lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
wenzelm@12739
    43
  by (blast intro: relprime_dvd_mult prime_imp_relprime)
paulson@11363
    44
nipkow@16663
    45
lemma prime_dvd_square: "prime p ==> p dvd m^Suc (Suc 0) ==> p dvd m"
wenzelm@12739
    46
  by (auto dest: prime_dvd_mult)
wenzelm@12739
    47
nipkow@16663
    48
lemma prime_dvd_power_two: "prime p ==> p dvd m\<twosuperior> ==> p dvd m"
paulson@14353
    49
  by (rule prime_dvd_square) (simp_all add: power2_eq_square)
wenzelm@11368
    50
paulson@11363
    51
paulson@11363
    52
end