src/HOL/Library/Primes.thy
changeset 11368 9c1995c73383
parent 11363 a548865b1b6a
child 11369 2c4bb701546a
     1.1 --- a/src/HOL/Library/Primes.thy	Sat Jun 09 08:44:04 2001 +0200
     1.2 +++ b/src/HOL/Library/Primes.thy	Sat Jun 09 14:18:19 2001 +0200
     1.3 @@ -1,23 +1,24 @@
     1.4 -(*  Title:      HOL/NumberTheory/Primes.thy
     1.5 +(*  Title:      HOL/Library/Primes.thy
     1.6      ID:         $Id$
     1.7      Author:     Christophe Tabacznyj and Lawrence C Paulson
     1.8      Copyright   1996  University of Cambridge
     1.9  *)
    1.10  
    1.11 -header {* The Greatest Common Divisor and Euclid's algorithm *}
    1.12 +header {*
    1.13 +  \title{The Greatest Common Divisor and Euclid's algorithm}
    1.14 +  \author{Christophe Tabacznyj and Lawrence C Paulson} *}
    1.15  
    1.16  theory Primes = Main:
    1.17  
    1.18  text {*
    1.19 -  (See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992))
    1.20 -
    1.21 +  See \cite{davenport92}.
    1.22    \bigskip
    1.23  *}
    1.24  
    1.25  consts
    1.26 -  gcd  :: "nat * nat => nat"  -- {* Euclid's algorithm *}
    1.27 +  gcd  :: "nat \<times> nat => nat"  -- {* Euclid's algorithm *}
    1.28  
    1.29 -recdef gcd  "measure ((\<lambda>(m, n). n) :: nat * nat => nat)"
    1.30 +recdef gcd  "measure ((\<lambda>(m, n). n) :: nat \<times> nat => nat)"
    1.31    "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
    1.32  
    1.33  constdefs
    1.34 @@ -70,6 +71,17 @@
    1.35  lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1, standard]
    1.36  lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard]
    1.37  
    1.38 +lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
    1.39 +proof
    1.40 +  have "gcd (m, n) dvd m \<and> gcd (m, n) dvd n" by simp
    1.41 +  also assume "gcd (m, n) = 0"
    1.42 +  finally have "0 dvd m \<and> 0 dvd n" .
    1.43 +  thus "m = 0 \<and> n = 0" by (simp add: dvd_0_left)
    1.44 +next
    1.45 +  assume "m = 0 \<and> n = 0"
    1.46 +  thus "gcd (m, n) = 0" by simp
    1.47 +qed
    1.48 +
    1.49  
    1.50  text {*
    1.51    \medskip Maximality: for all @{term m}, @{term n}, @{term k}
    1.52 @@ -145,7 +157,7 @@
    1.53  *}
    1.54  
    1.55  lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
    1.56 -    -- {* Davenport, page 27 *}
    1.57 +    -- {* \cite[page 27]{davenport92} *}
    1.58    apply (induct m n rule: gcd_induct)
    1.59     apply simp
    1.60    apply (case_tac "k = 0")
    1.61 @@ -189,6 +201,10 @@
    1.62    apply (blast intro: relprime_dvd_mult prime_imp_relprime)
    1.63    done
    1.64  
    1.65 +lemma prime_dvd_square: "p \<in> prime ==> p dvd m^2 ==> p dvd m"
    1.66 +  apply (auto dest: prime_dvd_mult)
    1.67 +  done
    1.68 +
    1.69  
    1.70  text {* \medskip Addition laws *}
    1.71