tuned Primes theory;

--- a/src/HOL/Library/Library.thy	Sat Jun 09 08:44:04 2001 +0200
+++ b/src/HOL/Library/Library.thy	Sat Jun 09 14:18:19 2001 +0200
@@ -10,6 +10,7 @@
   Continuity +
   Multiset +
   Permutation +
+  Primes +
   While_Combinator:
 end
 (*>*)

--- a/src/HOL/Library/Primes.thy	Sat Jun 09 08:44:04 2001 +0200
+++ b/src/HOL/Library/Primes.thy	Sat Jun 09 14:18:19 2001 +0200
@@ -1,23 +1,24 @@
-(*  Title:      HOL/NumberTheory/Primes.thy
+(*  Title:      HOL/Library/Primes.thy
     ID:         $Id$
     Author:     Christophe Tabacznyj and Lawrence C Paulson
     Copyright   1996  University of Cambridge
 *)
 
-header {* The Greatest Common Divisor and Euclid's algorithm *}
+header {*
+  \title{The Greatest Common Divisor and Euclid's algorithm}
+  \author{Christophe Tabacznyj and Lawrence C Paulson} *}
 
 theory Primes = Main:
 
 text {*
-  (See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992))
-
+  See \cite{davenport92}.
   \bigskip
 *}
 
 consts
-  gcd  :: "nat * nat => nat"  -- {* Euclid's algorithm *}
+  gcd  :: "nat \<times> nat => nat"  -- {* Euclid's algorithm *}
 
-recdef gcd  "measure ((\<lambda>(m, n). n) :: nat * nat => nat)"
+recdef gcd  "measure ((\<lambda>(m, n). n) :: nat \<times> nat => nat)"
   "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
 
 constdefs
@@ -70,6 +71,17 @@
 lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1, standard]
 lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard]
 
+lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
+proof
+  have "gcd (m, n) dvd m \<and> gcd (m, n) dvd n" by simp
+  also assume "gcd (m, n) = 0"
+  finally have "0 dvd m \<and> 0 dvd n" .
+  thus "m = 0 \<and> n = 0" by (simp add: dvd_0_left)
+next
+  assume "m = 0 \<and> n = 0"
+  thus "gcd (m, n) = 0" by simp
+qed
+
 
 text {*
   \medskip Maximality: for all @{term m}, @{term n}, @{term k}
@@ -145,7 +157,7 @@
 *}
 
 lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
-    -- {* Davenport, page 27 *}
+    -- {* \cite[page 27]{davenport92} *}
   apply (induct m n rule: gcd_induct)
    apply simp
   apply (case_tac "k = 0")
@@ -189,6 +201,10 @@
   apply (blast intro: relprime_dvd_mult prime_imp_relprime)
   done
 
+lemma prime_dvd_square: "p \<in> prime ==> p dvd m^2 ==> p dvd m"
+  apply (auto dest: prime_dvd_mult)
+  done
+
 
 text {* \medskip Addition laws *}
 

--- a/src/HOL/Library/document/root.bib	Sat Jun 09 08:44:04 2001 +0200
+++ b/src/HOL/Library/document/root.bib	Sat Jun 09 14:18:19 2001 +0200
@@ -1,3 +1,11 @@
+
+@Book{davenport92,
+  author =	 {H. Davenport},
+  title = 	 {The Higher Arithmetic},
+  publisher = 	 {Cambridge University Press},
+  year = 	 1992
+}
+
 @InProceedings{paulin-tlca,
   author	= {Christine Paulin-Mohring},
   title		= {Inductive Definitions in the System {Coq}: Rules and

--- a/src/HOL/Library/document/root.tex	Sat Jun 09 08:44:04 2001 +0200
+++ b/src/HOL/Library/document/root.tex	Sat Jun 09 14:18:19 2001 +0200
@@ -18,6 +18,7 @@
   David von Oheimb\\
   Lawrence C Paulson \\
   Thomas M Rasmussen \\
+  Christophe Tabacznyj \\
   Markus Wenzel}
 \maketitle
 

--- a/src/HOL/NumberTheory/ROOT.ML	Sat Jun 09 08:44:04 2001 +0200
+++ b/src/HOL/NumberTheory/ROOT.ML	Sat Jun 09 14:18:19 2001 +0200
@@ -1,7 +1,7 @@
 
 no_document use_thy "Permutation";
+no_document use_thy "Primes";
 
-use_thy "Primes";
 use_thy "Fib";
 use_thy "Factorization";
 use_thy "Chinese";