# Theory Primes

Up to index of Isabelle/HOL/HOL-Complex/ex

theory Primes
imports Main
begin

    (*  Title:      HOL/Library/Primes.thy
        ID:         $Id: Primes.thy,v 1.17 2005/07/08 09:39:08 nipkow Exp $
        Author:     Christophe Tabacznyj and Lawrence C Paulson
        Copyright   1996  University of Cambridge
    *)

    header {* Primality on nat *}

    theory Primes
    imports Main
    begin

    constdefs
      coprime :: "nat => nat => bool"
      "coprime m n == gcd (m, n) = 1"

      prime :: "nat => bool"
      "prime p == 1 < p ∧ (∀m. m dvd p --> m = 1 ∨ m = p)"

    lemma two_is_prime: "prime 2"
      apply (auto simp add: prime_def)
      apply (case_tac m)
       apply (auto dest!: dvd_imp_le)
      done

    lemma prime_imp_relprime: "prime p ==> ¬ p dvd n ==> gcd (p, n) = 1"
      apply (auto simp add: prime_def)
      apply (drule_tac x = "gcd (p, n)" in spec)
      apply auto
      apply (insert gcd_dvd2 [of p n])
      apply simp
      done

    text {*
      This theorem leads immediately to a proof of the uniqueness of
      factorization.  If @{term p} divides a product of primes then it is
      one of those primes.
    *}

    lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m ∨ p dvd n"
      by (blast intro: relprime_dvd_mult prime_imp_relprime)

    lemma prime_dvd_square: "prime p ==> p dvd m^Suc (Suc 0) ==> p dvd m"
      by (auto dest: prime_dvd_mult)

    lemma prime_dvd_power_two: "prime p ==> p dvd m² ==> p dvd m"
      by (rule prime_dvd_square) (simp_all add: power2_eq_square)

    end

lemma two_is_prime:

      prime 2

lemma prime_imp_relprime:

      [| prime p; ¬ p dvd n |] ==> gcd (p, n) = 1

lemma prime_dvd_mult:

      [| prime p; p dvd m * n |] ==> p dvd m ∨ p dvd n

lemma prime_dvd_square:

      [| prime p; p dvd m ^ Suc (Suc 0) |] ==> p dvd m

lemma prime_dvd_power_two:

      [| prime p; p dvd m² |] ==> p dvd m