src/HOL/Library/Primes.thy

-(*  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 *}
-
-recdef gcd  "measure ((\<lambda>(m, n). n) :: nat * nat => nat)"
+  gcd  :: "nat \<times> nat => nat"  -- {* Euclid's algorithm *}
+
+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
   is_gcd :: "nat => nat => nat => bool"  -- {* @{term gcd} as a relation *}
   "is_gcd p m n == p dvd m \<and> p dvd n \<and>

   done
 
 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}
   naturals, if @{term k} divides @{term m} and @{term k} divides
   @{term n} then @{term k} divides @{term "gcd (m, n)"}.

 text {*
   \medskip Multiplication laws
 *}
 
 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")
    apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
   done

   one of those primes.
 *}
 
 lemma prime_dvd_mult: "p \<in> prime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
   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 *}