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
```