author  nipkow 
Wed, 18 Aug 2004 11:09:40 +0200  
changeset 15140  322485b816ac 
parent 15131  c69542757a4d 
child 15628  9f912f8fd2df 
permissions  rwrr 
11368  1 
(* Title: HOL/Library/Primes.thy 
11363  2 
ID: $Id$ 
3 
Author: Christophe Tabacznyj and Lawrence C Paulson 

4 
Copyright 1996 University of Cambridge 

5 
*) 

6 

14706  7 
header {* The Greatest Common Divisor and Euclid's algorithm *} 
11363  8 

15131  9 
theory Primes 
15140  10 
imports Main 
15131  11 
begin 
11363  12 

13 
text {* 

11368  14 
See \cite{davenport92}. 
11363  15 
\bigskip 
16 
*} 

17 

18 
consts 

11368  19 
gcd :: "nat \<times> nat => nat"  {* Euclid's algorithm *} 
11363  20 

11368  21 
recdef gcd "measure ((\<lambda>(m, n). n) :: nat \<times> nat => nat)" 
11363  22 
"gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))" 
23 

24 
constdefs 

25 
is_gcd :: "nat => nat => nat => bool"  {* @{term gcd} as a relation *} 

26 
"is_gcd p m n == p dvd m \<and> p dvd n \<and> 

27 
(\<forall>d. d dvd m \<and> d dvd n > d dvd p)" 

28 

29 
coprime :: "nat => nat => bool" 

30 
"coprime m n == gcd (m, n) = 1" 

31 

32 
prime :: "nat set" 

33 
"prime == {p. 1 < p \<and> (\<forall>m. m dvd p > m = 1 \<or> m = p)}" 

34 

35 

36 
lemma gcd_induct: 

37 
"(!!m. P m 0) ==> 

38 
(!!m n. 0 < n ==> P n (m mod n) ==> P m n) 

39 
==> P (m::nat) (n::nat)" 

40 
apply (induct m n rule: gcd.induct) 

41 
apply (case_tac "n = 0") 

42 
apply simp_all 

43 
done 

44 

45 

46 
lemma gcd_0 [simp]: "gcd (m, 0) = m" 

47 
apply simp 

48 
done 

49 

50 
lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)" 

51 
apply simp 

52 
done 

53 

54 
declare gcd.simps [simp del] 

55 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset

56 
lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1" 
11363  57 
apply (simp add: gcd_non_0) 
58 
done 

59 

60 
text {* 

61 
\medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}. The 

62 
conjunctions don't seem provable separately. 

63 
*} 

64 

12300  65 
lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m" 
66 
and gcd_dvd2 [iff]: "gcd (m, n) dvd n" 

11363  67 
apply (induct m n rule: gcd_induct) 
68 
apply (simp_all add: gcd_non_0) 

69 
apply (blast dest: dvd_mod_imp_dvd) 

70 
done 

71 

72 
text {* 

73 
\medskip Maximality: for all @{term m}, @{term n}, @{term k} 

74 
naturals, if @{term k} divides @{term m} and @{term k} divides 

75 
@{term n} then @{term k} divides @{term "gcd (m, n)"}. 

76 
*} 

77 

78 
lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)" 

79 
apply (induct m n rule: gcd_induct) 

80 
apply (simp_all add: gcd_non_0 dvd_mod) 

81 
done 

82 

83 
lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)" 

84 
apply (blast intro!: gcd_greatest intro: dvd_trans) 

85 
done 

86 

11374
2badb9b2a8ec
New proof of gcd_zero after a change to Divides.ML made the old one fail
paulson
parents:
11369
diff
changeset

87 
lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)" 
2badb9b2a8ec
New proof of gcd_zero after a change to Divides.ML made the old one fail
paulson
parents:
11369
diff
changeset

88 
by (simp only: dvd_0_left_iff [THEN sym] gcd_greatest_iff) 
2badb9b2a8ec
New proof of gcd_zero after a change to Divides.ML made the old one fail
paulson
parents:
11369
diff
changeset

89 

11363  90 

91 
text {* 

92 
\medskip Function gcd yields the Greatest Common Divisor. 

93 
*} 

94 

95 
lemma is_gcd: "is_gcd (gcd (m, n)) m n" 

96 
apply (simp add: is_gcd_def gcd_greatest) 

97 
done 

98 

99 
text {* 

100 
\medskip Uniqueness of GCDs. 

101 
*} 

102 

103 
lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n" 

104 
apply (simp add: is_gcd_def) 

105 
apply (blast intro: dvd_anti_sym) 

106 
done 

107 

108 
lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m" 

109 
apply (auto simp add: is_gcd_def) 

110 
done 

111 

112 

113 
text {* 

114 
\medskip Commutativity 

115 
*} 

116 

117 
lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m" 

118 
apply (auto simp add: is_gcd_def) 

119 
done 

120 

121 
lemma gcd_commute: "gcd (m, n) = gcd (n, m)" 

122 
apply (rule is_gcd_unique) 

123 
apply (rule is_gcd) 

124 
apply (subst is_gcd_commute) 

125 
apply (simp add: is_gcd) 

126 
done 

127 

128 
lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" 

129 
apply (rule is_gcd_unique) 

130 
apply (rule is_gcd) 

131 
apply (simp add: is_gcd_def) 

132 
apply (blast intro: dvd_trans) 

133 
done 

134 

135 
lemma gcd_0_left [simp]: "gcd (0, m) = m" 

136 
apply (simp add: gcd_commute [of 0]) 

137 
done 

138 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset

139 
lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1" 
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset

140 
apply (simp add: gcd_commute [of "Suc 0"]) 
11363  141 
done 
142 

143 

144 
text {* 

145 
\medskip Multiplication laws 

146 
*} 

147 

148 
lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)" 

11368  149 
 {* \cite[page 27]{davenport92} *} 
11363  150 
apply (induct m n rule: gcd_induct) 
151 
apply simp 

152 
apply (case_tac "k = 0") 

153 
apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) 

154 
done 

155 

156 
lemma gcd_mult [simp]: "gcd (k, k * n) = k" 

157 
apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric]) 

158 
done 

159 

160 
lemma gcd_self [simp]: "gcd (k, k) = k" 

161 
apply (rule gcd_mult [of k 1, simplified]) 

162 
done 

163 

164 
lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m" 

165 
apply (insert gcd_mult_distrib2 [of m k n]) 

166 
apply simp 

167 
apply (erule_tac t = m in ssubst) 

168 
apply simp 

169 
done 

170 

171 
lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)" 

172 
apply (blast intro: relprime_dvd_mult dvd_trans) 

173 
done 

174 

175 
lemma prime_imp_relprime: "p \<in> prime ==> \<not> p dvd n ==> gcd (p, n) = 1" 

176 
apply (auto simp add: prime_def) 

177 
apply (drule_tac x = "gcd (p, n)" in spec) 

178 
apply auto 

179 
apply (insert gcd_dvd2 [of p n]) 

180 
apply simp 

181 
done 

182 

13032  183 
lemma two_is_prime: "2 \<in> prime" 
184 
apply (auto simp add: prime_def) 

185 
apply (case_tac m) 

186 
apply (auto dest!: dvd_imp_le) 

187 
done 

188 

11363  189 
text {* 
190 
This theorem leads immediately to a proof of the uniqueness of 

191 
factorization. If @{term p} divides a product of primes then it is 

192 
one of those primes. 

193 
*} 

194 

195 
lemma prime_dvd_mult: "p \<in> prime ==> p dvd m * n ==> p dvd m \<or> p dvd n" 

12739  196 
by (blast intro: relprime_dvd_mult prime_imp_relprime) 
11363  197 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset

198 
lemma prime_dvd_square: "p \<in> prime ==> p dvd m^Suc (Suc 0) ==> p dvd m" 
12739  199 
by (auto dest: prime_dvd_mult) 
200 

201 
lemma prime_dvd_power_two: "p \<in> prime ==> p dvd m\<twosuperior> ==> p dvd m" 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13187
diff
changeset

202 
by (rule prime_dvd_square) (simp_all add: power2_eq_square) 
11368  203 

11363  204 

205 
text {* \medskip Addition laws *} 

206 

207 
lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)" 

208 
apply (case_tac "n = 0") 

209 
apply (simp_all add: gcd_non_0) 

210 
done 

211 

212 
lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)" 

213 
apply (rule gcd_commute [THEN trans]) 

214 
apply (subst add_commute) 

215 
apply (simp add: gcd_add1) 

216 
apply (rule gcd_commute) 

217 
done 

218 

219 
lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)" 

220 
apply (subst add_commute) 

221 
apply (rule gcd_add2) 

222 
done 

223 

224 
lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)" 

225 
apply (induct k) 

226 
apply (simp_all add: gcd_add2 add_assoc) 

227 
done 

228 

229 

230 
text {* \medskip More multiplication laws *} 

231 

232 
lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)" 

233 
apply (rule dvd_anti_sym) 

234 
apply (rule gcd_greatest) 

235 
apply (rule_tac n = k in relprime_dvd_mult) 

236 
apply (simp add: gcd_assoc) 

237 
apply (simp add: gcd_commute) 

238 
apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2) 

239 
apply (blast intro: gcd_dvd1 dvd_trans) 

240 
done 

241 

242 
end 