author  haftmann 
Wed, 17 Feb 2016 21:51:56 +0100  
changeset 62345  e66d7841d5a2 
parent 62344  759d684c0e60 
child 62346  97f2ed240431 
permissions  rwrr 
32479  1 
(* Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, 
31798  2 
Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow 
31706  3 

4 

32479  5 
This file deals with the functions gcd and lcm. Definitions and 
6 
lemmas are proved uniformly for the natural numbers and integers. 

31706  7 

8 
This file combines and revises a number of prior developments. 

9 

10 
The original theories "GCD" and "Primes" were by Christophe Tabacznyj 

58623  11 
and Lawrence C. Paulson, based on @{cite davenport92}. They introduced 
31706  12 
gcd, lcm, and prime for the natural numbers. 
13 

14 
The original theory "IntPrimes" was by Thomas M. Rasmussen, and 

15 
extended gcd, lcm, primes to the integers. Amine Chaieb provided 

16 
another extension of the notions to the integers, and added a number 

17 
of results to "Primes" and "GCD". IntPrimes also defined and developed 

18 
the congruence relations on the integers. The notion was extended to 

34915  19 
the natural numbers by Chaieb. 
31706  20 

32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

21 
Jeremy Avigad combined all of these, made everything uniform for the 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

22 
natural numbers and the integers, and added a number of new theorems. 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

23 

31798  24 
Tobias Nipkow cleaned up a lot. 
21256  25 
*) 
26 

31706  27 

60758  28 
section \<open>Greatest common divisor and least common multiple\<close> 
21256  29 

30 
theory GCD 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59545
diff
changeset

31 
imports Main 
31706  32 
begin 
33 

62345  34 
subsection \<open>Abstract GCD and LCM\<close> 
31706  35 

31992  36 
class gcd = zero + one + dvd + 
41550  37 
fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
38 
and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 

21256  39 
begin 
40 

60686  41 
abbreviation coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
42 
where "coprime x y \<equiv> gcd x y = 1" 

31706  43 

44 
end 

45 

60686  46 
class Gcd = gcd + 
47 
fixes Gcd :: "'a set \<Rightarrow> 'a" 

48 
and Lcm :: "'a set \<Rightarrow> 'a" 

49 

50 
class semiring_gcd = normalization_semidom + gcd + 

59008  51 
assumes gcd_dvd1 [iff]: "gcd a b dvd a" 
59977  52 
and gcd_dvd2 [iff]: "gcd a b dvd b" 
53 
and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" 

60686  54 
and normalize_gcd [simp]: "normalize (gcd a b) = gcd a b" 
55 
and lcm_gcd: "lcm a b = normalize (a * b) div gcd a b" 

56 
begin 

57 

60689  58 
lemma gcd_greatest_iff [simp]: 
60686  59 
"a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c" 
60 
by (blast intro!: gcd_greatest intro: dvd_trans) 

61 

60689  62 
lemma gcd_dvdI1: 
63 
"a dvd c \<Longrightarrow> gcd a b dvd c" 

64 
by (rule dvd_trans) (rule gcd_dvd1) 

65 

66 
lemma gcd_dvdI2: 

67 
"b dvd c \<Longrightarrow> gcd a b dvd c" 

68 
by (rule dvd_trans) (rule gcd_dvd2) 

69 

62345  70 
lemma dvd_gcdD1: 
71 
"a dvd gcd b c \<Longrightarrow> a dvd b" 

72 
using gcd_dvd1 [of b c] by (blast intro: dvd_trans) 

73 

74 
lemma dvd_gcdD2: 

75 
"a dvd gcd b c \<Longrightarrow> a dvd c" 

76 
using gcd_dvd2 [of b c] by (blast intro: dvd_trans) 

77 

60686  78 
lemma gcd_0_left [simp]: 
79 
"gcd 0 a = normalize a" 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

80 
by (rule associated_eqI) simp_all 
60686  81 

82 
lemma gcd_0_right [simp]: 

83 
"gcd a 0 = normalize a" 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

84 
by (rule associated_eqI) simp_all 
60686  85 

86 
lemma gcd_eq_0_iff [simp]: 

87 
"gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" (is "?P \<longleftrightarrow> ?Q") 

88 
proof 

89 
assume ?P then have "0 dvd gcd a b" by simp 

90 
then have "0 dvd a" and "0 dvd b" by (blast intro: dvd_trans)+ 

91 
then show ?Q by simp 

92 
next 

93 
assume ?Q then show ?P by simp 

94 
qed 

95 

96 
lemma unit_factor_gcd: 

97 
"unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)" 

98 
proof (cases "gcd a b = 0") 

99 
case True then show ?thesis by simp 

100 
next 

101 
case False 

102 
have "unit_factor (gcd a b) * normalize (gcd a b) = gcd a b" 

103 
by (rule unit_factor_mult_normalize) 

104 
then have "unit_factor (gcd a b) * gcd a b = gcd a b" 

105 
by simp 

106 
then have "unit_factor (gcd a b) * gcd a b div gcd a b = gcd a b div gcd a b" 

107 
by simp 

108 
with False show ?thesis by simp 

109 
qed 

110 

60690  111 
lemma is_unit_gcd [simp]: 
112 
"is_unit (gcd a b) \<longleftrightarrow> coprime a b" 

113 
by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor) 

114 

61605  115 
sublocale gcd: abel_semigroup gcd 
60686  116 
proof 
117 
fix a b c 

118 
show "gcd a b = gcd b a" 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

119 
by (rule associated_eqI) simp_all 
60686  120 
from gcd_dvd1 have "gcd (gcd a b) c dvd a" 
121 
by (rule dvd_trans) simp 

122 
moreover from gcd_dvd1 have "gcd (gcd a b) c dvd b" 

123 
by (rule dvd_trans) simp 

124 
ultimately have P1: "gcd (gcd a b) c dvd gcd a (gcd b c)" 

125 
by (auto intro!: gcd_greatest) 

126 
from gcd_dvd2 have "gcd a (gcd b c) dvd b" 

127 
by (rule dvd_trans) simp 

128 
moreover from gcd_dvd2 have "gcd a (gcd b c) dvd c" 

129 
by (rule dvd_trans) simp 

130 
ultimately have P2: "gcd a (gcd b c) dvd gcd (gcd a b) c" 

131 
by (auto intro!: gcd_greatest) 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

132 
from P1 P2 show "gcd (gcd a b) c = gcd a (gcd b c)" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

133 
by (rule associated_eqI) simp_all 
60686  134 
qed 
135 

136 
lemma gcd_self [simp]: 

137 
"gcd a a = normalize a" 

138 
proof  

139 
have "a dvd gcd a a" 

140 
by (rule gcd_greatest) simp_all 

141 
then show ?thesis 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

142 
by (auto intro: associated_eqI) 
60686  143 
qed 
61913  144 

145 
lemma gcd_left_idem [simp]: 

146 
"gcd a (gcd a b) = gcd a b" 

147 
by (auto intro: associated_eqI) 

148 

149 
lemma gcd_right_idem [simp]: 

150 
"gcd (gcd a b) b = gcd a b" 

151 
unfolding gcd.commute [of a] gcd.commute [of "gcd b a"] by simp 

152 

60686  153 
lemma coprime_1_left [simp]: 
154 
"coprime 1 a" 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

155 
by (rule associated_eqI) simp_all 
60686  156 

157 
lemma coprime_1_right [simp]: 

158 
"coprime a 1" 

159 
using coprime_1_left [of a] by (simp add: ac_simps) 

160 

161 
lemma gcd_mult_left: 

162 
"gcd (c * a) (c * b) = normalize c * gcd a b" 

163 
proof (cases "c = 0") 

164 
case True then show ?thesis by simp 

165 
next 

166 
case False 

167 
then have "c * gcd a b dvd gcd (c * a) (c * b)" 

168 
by (auto intro: gcd_greatest) 

169 
moreover from calculation False have "gcd (c * a) (c * b) dvd c * gcd a b" 

170 
by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute) 

171 
ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)" 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

172 
by (auto intro: associated_eqI) 
60686  173 
then show ?thesis by (simp add: normalize_mult) 
174 
qed 

175 

176 
lemma gcd_mult_right: 

177 
"gcd (a * c) (b * c) = gcd b a * normalize c" 

178 
using gcd_mult_left [of c a b] by (simp add: ac_simps) 

179 

180 
lemma mult_gcd_left: 

181 
"c * gcd a b = unit_factor c * gcd (c * a) (c * b)" 

182 
by (simp add: gcd_mult_left mult.assoc [symmetric]) 

183 

184 
lemma mult_gcd_right: 

185 
"gcd a b * c = gcd (a * c) (b * c) * unit_factor c" 

186 
using mult_gcd_left [of c a b] by (simp add: ac_simps) 

187 

60689  188 
lemma dvd_lcm1 [iff]: 
60686  189 
"a dvd lcm a b" 
190 
proof  

191 
have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)" 

192 
by (simp add: lcm_gcd normalize_mult div_mult_swap) 

193 
then show ?thesis 

194 
by (simp add: lcm_gcd) 

195 
qed 

196 

60689  197 
lemma dvd_lcm2 [iff]: 
60686  198 
"b dvd lcm a b" 
199 
proof  

200 
have "normalize (a * b) div gcd a b = normalize b * (normalize a div gcd a b)" 

201 
by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps) 

202 
then show ?thesis 

203 
by (simp add: lcm_gcd) 

204 
qed 

205 

60689  206 
lemma dvd_lcmI1: 
207 
"a dvd b \<Longrightarrow> a dvd lcm b c" 

208 
by (rule dvd_trans) (assumption, blast) 

209 

210 
lemma dvd_lcmI2: 

211 
"a dvd c \<Longrightarrow> a dvd lcm b c" 

212 
by (rule dvd_trans) (assumption, blast) 

213 

62345  214 
lemma lcm_dvdD1: 
215 
"lcm a b dvd c \<Longrightarrow> a dvd c" 

216 
using dvd_lcm1 [of a b] by (blast intro: dvd_trans) 

217 

218 
lemma lcm_dvdD2: 

219 
"lcm a b dvd c \<Longrightarrow> b dvd c" 

220 
using dvd_lcm2 [of a b] by (blast intro: dvd_trans) 

221 

60686  222 
lemma lcm_least: 
223 
assumes "a dvd c" and "b dvd c" 

224 
shows "lcm a b dvd c" 

225 
proof (cases "c = 0") 

226 
case True then show ?thesis by simp 

227 
next 

228 
case False then have U: "is_unit (unit_factor c)" by simp 

229 
show ?thesis 

230 
proof (cases "gcd a b = 0") 

231 
case True with assms show ?thesis by simp 

232 
next 

233 
case False then have "a \<noteq> 0 \<or> b \<noteq> 0" by simp 

234 
with \<open>c \<noteq> 0\<close> assms have "a * b dvd a * c" "a * b dvd c * b" 

235 
by (simp_all add: mult_dvd_mono) 

236 
then have "normalize (a * b) dvd gcd (a * c) (b * c)" 

237 
by (auto intro: gcd_greatest simp add: ac_simps) 

238 
then have "normalize (a * b) dvd gcd (a * c) (b * c) * unit_factor c" 

239 
using U by (simp add: dvd_mult_unit_iff) 

240 
then have "normalize (a * b) dvd gcd a b * c" 

241 
by (simp add: mult_gcd_right [of a b c]) 

242 
then have "normalize (a * b) div gcd a b dvd c" 

243 
using False by (simp add: div_dvd_iff_mult ac_simps) 

244 
then show ?thesis by (simp add: lcm_gcd) 

245 
qed 

246 
qed 

247 

60689  248 
lemma lcm_least_iff [simp]: 
60686  249 
"lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c" 
250 
by (blast intro!: lcm_least intro: dvd_trans) 

251 

252 
lemma normalize_lcm [simp]: 

253 
"normalize (lcm a b) = lcm a b" 

254 
by (simp add: lcm_gcd dvd_normalize_div) 

255 

256 
lemma lcm_0_left [simp]: 

257 
"lcm 0 a = 0" 

258 
by (simp add: lcm_gcd) 

259 

260 
lemma lcm_0_right [simp]: 

261 
"lcm a 0 = 0" 

262 
by (simp add: lcm_gcd) 

263 

264 
lemma lcm_eq_0_iff: 

265 
"lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" (is "?P \<longleftrightarrow> ?Q") 

266 
proof 

267 
assume ?P then have "0 dvd lcm a b" by simp 

268 
then have "0 dvd normalize (a * b) div gcd a b" 

269 
by (simp add: lcm_gcd) 

270 
then have "0 * gcd a b dvd normalize (a * b)" 

271 
using dvd_div_iff_mult [of "gcd a b" _ 0] by (cases "gcd a b = 0") simp_all 

272 
then have "normalize (a * b) = 0" 

273 
by simp 

274 
then show ?Q by simp 

275 
next 

276 
assume ?Q then show ?P by auto 

277 
qed 

278 

61913  279 
lemma lcm_eq_1_iff [simp]: 
280 
"lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b" 

281 
by (auto intro: associated_eqI) 

282 

60686  283 
lemma unit_factor_lcm : 
284 
"unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)" 

285 
by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd) 

286 

61605  287 
sublocale lcm: abel_semigroup lcm 
60686  288 
proof 
289 
fix a b c 

290 
show "lcm a b = lcm b a" 

291 
by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div) 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

292 
have "lcm (lcm a b) c dvd lcm a (lcm b c)" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

293 
and "lcm a (lcm b c) dvd lcm (lcm a b) c" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

294 
by (auto intro: lcm_least 
60686  295 
dvd_trans [of b "lcm b c" "lcm a (lcm b c)"] 
296 
dvd_trans [of c "lcm b c" "lcm a (lcm b c)"] 

297 
dvd_trans [of a "lcm a b" "lcm (lcm a b) c"] 

298 
dvd_trans [of b "lcm a b" "lcm (lcm a b) c"]) 

299 
then show "lcm (lcm a b) c = lcm a (lcm b c)" 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

300 
by (rule associated_eqI) simp_all 
60686  301 
qed 
302 

303 
lemma lcm_self [simp]: 

304 
"lcm a a = normalize a" 

305 
proof  

306 
have "lcm a a dvd a" 

307 
by (rule lcm_least) simp_all 

308 
then show ?thesis 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

309 
by (auto intro: associated_eqI) 
60686  310 
qed 
311 

61913  312 
lemma lcm_left_idem [simp]: 
313 
"lcm a (lcm a b) = lcm a b" 

314 
by (auto intro: associated_eqI) 

315 

316 
lemma lcm_right_idem [simp]: 

317 
"lcm (lcm a b) b = lcm a b" 

318 
unfolding lcm.commute [of a] lcm.commute [of "lcm b a"] by simp 

319 

60686  320 
lemma gcd_mult_lcm [simp]: 
321 
"gcd a b * lcm a b = normalize a * normalize b" 

322 
by (simp add: lcm_gcd normalize_mult) 

323 

324 
lemma lcm_mult_gcd [simp]: 

325 
"lcm a b * gcd a b = normalize a * normalize b" 

326 
using gcd_mult_lcm [of a b] by (simp add: ac_simps) 

327 

328 
lemma gcd_lcm: 

329 
assumes "a \<noteq> 0" and "b \<noteq> 0" 

330 
shows "gcd a b = normalize (a * b) div lcm a b" 

331 
proof  

332 
from assms have "lcm a b \<noteq> 0" 

333 
by (simp add: lcm_eq_0_iff) 

334 
have "gcd a b * lcm a b = normalize a * normalize b" by simp 

335 
then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b" 

336 
by (simp_all add: normalize_mult) 

337 
with \<open>lcm a b \<noteq> 0\<close> show ?thesis 

338 
using nonzero_mult_divide_cancel_right [of "lcm a b" "gcd a b"] by simp 

339 
qed 

340 

341 
lemma lcm_1_left [simp]: 

342 
"lcm 1 a = normalize a" 

343 
by (simp add: lcm_gcd) 

344 

345 
lemma lcm_1_right [simp]: 

346 
"lcm a 1 = normalize a" 

347 
by (simp add: lcm_gcd) 

348 

349 
lemma lcm_mult_left: 

350 
"lcm (c * a) (c * b) = normalize c * lcm a b" 

351 
by (cases "c = 0") 

352 
(simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps, 

353 
simp add: dvd_div_mult2_eq mult.left_commute [of "normalize c", symmetric]) 

354 

355 
lemma lcm_mult_right: 

356 
"lcm (a * c) (b * c) = lcm b a * normalize c" 

357 
using lcm_mult_left [of c a b] by (simp add: ac_simps) 

358 

359 
lemma mult_lcm_left: 

360 
"c * lcm a b = unit_factor c * lcm (c * a) (c * b)" 

361 
by (simp add: lcm_mult_left mult.assoc [symmetric]) 

362 

363 
lemma mult_lcm_right: 

364 
"lcm a b * c = lcm (a * c) (b * c) * unit_factor c" 

365 
using mult_lcm_left [of c a b] by (simp add: ac_simps) 

366 

367 
end 

368 

62345  369 
class ring_gcd = comm_ring_1 + semiring_gcd 
370 

60686  371 
class semiring_Gcd = semiring_gcd + Gcd + 
372 
assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a" 

373 
and Gcd_greatest: "(\<And>b. b \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> a dvd Gcd A" 

374 
and normalize_Gcd [simp]: "normalize (Gcd A) = Gcd A" 

62345  375 
assumes dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A" 
376 
and Lcm_least: "(\<And>b. b \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> Lcm A dvd a" 

377 
and normalize_Lcm [simp]: "normalize (Lcm A) = Lcm A" 

60686  378 
begin 
379 

62345  380 
lemma Lcm_Gcd: 
381 
"Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}" 

382 
by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least) 

383 

384 
lemma Gcd_Lcm: 

385 
"Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}" 

386 
by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least) 

387 

60686  388 
lemma Gcd_empty [simp]: 
389 
"Gcd {} = 0" 

390 
by (rule dvd_0_left, rule Gcd_greatest) simp 

391 

62345  392 
lemma Lcm_empty [simp]: 
393 
"Lcm {} = 1" 

394 
by (auto intro: associated_eqI Lcm_least) 

395 

396 
lemma Gcd_insert [simp]: 

397 
"Gcd (insert a A) = gcd a (Gcd A)" 

398 
proof  

399 
have "Gcd (insert a A) dvd gcd a (Gcd A)" 

400 
by (auto intro: Gcd_dvd Gcd_greatest) 

401 
moreover have "gcd a (Gcd A) dvd Gcd (insert a A)" 

402 
proof (rule Gcd_greatest) 

403 
fix b 

404 
assume "b \<in> insert a A" 

405 
then show "gcd a (Gcd A) dvd b" 

406 
proof 

407 
assume "b = a" then show ?thesis by simp 

408 
next 

409 
assume "b \<in> A" 

410 
then have "Gcd A dvd b" by (rule Gcd_dvd) 

411 
moreover have "gcd a (Gcd A) dvd Gcd A" by simp 

412 
ultimately show ?thesis by (blast intro: dvd_trans) 

413 
qed 

414 
qed 

415 
ultimately show ?thesis 

416 
by (auto intro: associated_eqI) 

417 
qed 

418 

419 
lemma Lcm_insert [simp]: 

420 
"Lcm (insert a A) = lcm a (Lcm A)" 

421 
proof (rule sym) 

422 
have "lcm a (Lcm A) dvd Lcm (insert a A)" 

423 
by (auto intro: dvd_Lcm Lcm_least) 

424 
moreover have "Lcm (insert a A) dvd lcm a (Lcm A)" 

425 
proof (rule Lcm_least) 

426 
fix b 

427 
assume "b \<in> insert a A" 

428 
then show "b dvd lcm a (Lcm A)" 

429 
proof 

430 
assume "b = a" then show ?thesis by simp 

431 
next 

432 
assume "b \<in> A" 

433 
then have "b dvd Lcm A" by (rule dvd_Lcm) 

434 
moreover have "Lcm A dvd lcm a (Lcm A)" by simp 

435 
ultimately show ?thesis by (blast intro: dvd_trans) 

436 
qed 

437 
qed 

438 
ultimately show "lcm a (Lcm A) = Lcm (insert a A)" 

439 
by (rule associated_eqI) (simp_all add: lcm_eq_0_iff) 

440 
qed 

441 

60686  442 
lemma Gcd_0_iff [simp]: 
60687  443 
"Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q") 
60686  444 
proof 
445 
assume ?P 

446 
show ?Q 

447 
proof 

448 
fix a 

449 
assume "a \<in> A" 

450 
then have "Gcd A dvd a" by (rule Gcd_dvd) 

60687  451 
with \<open>?P\<close> have "a = 0" by simp 
452 
then show "a \<in> {0}" by simp 

60686  453 
qed 
454 
next 

455 
assume ?Q 

456 
have "0 dvd Gcd A" 

457 
proof (rule Gcd_greatest) 

458 
fix a 

459 
assume "a \<in> A" 

60687  460 
with \<open>?Q\<close> have "a = 0" by auto 
60686  461 
then show "0 dvd a" by simp 
462 
qed 

463 
then show ?P by simp 

464 
qed 

465 

466 
lemma Lcm_1_iff [simp]: 

467 
"Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)" (is "?P \<longleftrightarrow> ?Q") 

468 
proof 

469 
assume ?P 

470 
show ?Q 

471 
proof 

472 
fix a 

473 
assume "a \<in> A" 

474 
then have "a dvd Lcm A" 

475 
by (rule dvd_Lcm) 

476 
with \<open>?P\<close> show "is_unit a" 

477 
by simp 

478 
qed 

479 
next 

480 
assume ?Q 

481 
then have "is_unit (Lcm A)" 

482 
by (blast intro: Lcm_least) 

483 
then have "normalize (Lcm A) = 1" 

484 
by (rule is_unit_normalize) 

485 
then show ?P 

486 
by simp 

487 
qed 

488 

62345  489 
lemma unit_factor_Gcd: 
490 
"unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)" 

491 
proof (cases "Gcd A = 0") 

492 
case True then show ?thesis by auto 

493 
next 

494 
case False 

495 
from unit_factor_mult_normalize 

496 
have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A" . 

497 
then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp 

498 
then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp 

499 
with False have "unit_factor (Gcd A) = 1" by simp 

500 
with False show ?thesis by auto 

501 
qed 

502 

503 
lemma unit_factor_Lcm: 

504 
"unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" 

505 
proof (cases "Lcm A = 0") 

506 
case True then show ?thesis by simp 

507 
next 

508 
case False 

509 
with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1" 

510 
by blast 

511 
with False show ?thesis 

512 
by simp 

513 
qed 

514 

515 
lemma Gcd_eq_1_I: 

516 
assumes "is_unit a" and "a \<in> A" 

517 
shows "Gcd A = 1" 

518 
proof  

519 
from assms have "is_unit (Gcd A)" 

520 
by (blast intro: Gcd_dvd dvd_unit_imp_unit) 

521 
then have "normalize (Gcd A) = 1" 

522 
by (rule is_unit_normalize) 

523 
then show ?thesis 

524 
by simp 

525 
qed 

526 

60686  527 
lemma Lcm_eq_0_I: 
528 
assumes "0 \<in> A" 

529 
shows "Lcm A = 0" 

530 
proof  

531 
from assms have "0 dvd Lcm A" 

532 
by (rule dvd_Lcm) 

533 
then show ?thesis 

534 
by simp 

535 
qed 

536 

62345  537 
lemma Gcd_UNIV [simp]: 
538 
"Gcd UNIV = 1" 

539 
using dvd_refl by (rule Gcd_eq_1_I) simp 

540 

61929  541 
lemma Lcm_UNIV [simp]: 
542 
"Lcm UNIV = 0" 

543 
by (rule Lcm_eq_0_I) simp 

60686  544 

61929  545 
lemma Lcm_0_iff: 
546 
assumes "finite A" 

547 
shows "Lcm A = 0 \<longleftrightarrow> 0 \<in> A" 

548 
proof (cases "A = {}") 

549 
case True then show ?thesis by simp 

550 
next 

551 
case False with assms show ?thesis 

552 
by (induct A rule: finite_ne_induct) 

553 
(auto simp add: lcm_eq_0_iff) 

60686  554 
qed 
61929  555 

62345  556 
lemma dvd_Gcd: \<comment> \<open>FIXME remove\<close> 
557 
"\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A" 

558 
by (blast intro: Gcd_greatest) 

559 

560 
lemma Gcd_set [code_unfold]: 

561 
"Gcd (set as) = foldr gcd as 0" 

562 
by (induct as) simp_all 

563 

60686  564 
lemma Lcm_set [code_unfold]: 
565 
"Lcm (set as) = foldr lcm as 1" 

566 
by (induct as) simp_all 

59008  567 

62345  568 
lemma Gcd_image_normalize [simp]: 
569 
"Gcd (normalize ` A) = Gcd A" 

570 
proof  

571 
have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a 

572 
proof  

573 
from that obtain B where "A = insert a B" by blast 

574 
moreover have " gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a" 

575 
by (rule gcd_dvd1) 

576 
ultimately show "Gcd (normalize ` A) dvd a" 

577 
by simp 

578 
qed 

579 
then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)" 

580 
by (auto intro!: Gcd_greatest intro: Gcd_dvd) 

581 
then show ?thesis 

582 
by (auto intro: associated_eqI) 

583 
qed 

584 

585 
end 

586 

587 

588 
subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close> 

59008  589 

31706  590 
instantiation nat :: gcd 
591 
begin 

21256  592 

62345  593 
fun gcd_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
594 
where "gcd_nat x y = 

595 
(if y = 0 then x else gcd y (x mod y))" 

31706  596 

62345  597 
definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
31706  598 
where 
599 
"lcm_nat x y = x * y div (gcd x y)" 

600 

601 
instance proof qed 

602 

603 
end 

604 

605 
instantiation int :: gcd 

606 
begin 

21256  607 

62345  608 
definition gcd_int :: "int \<Rightarrow> int \<Rightarrow> int" 
609 
where "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))" 

23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

610 

62345  611 
definition lcm_int :: "int \<Rightarrow> int \<Rightarrow> int" 
612 
where "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))" 

23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

613 

61944  614 
instance .. 
31706  615 

616 
end 

23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

617 

62345  618 
text \<open>Transfer setup\<close> 
31706  619 

620 
lemma transfer_nat_int_gcd: 

621 
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)" 

622 
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)" 

32479  623 
unfolding gcd_int_def lcm_int_def 
31706  624 
by auto 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

625 

31706  626 
lemma transfer_nat_int_gcd_closures: 
627 
"x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0" 

628 
"x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0" 

629 
by (auto simp add: gcd_int_def lcm_int_def) 

630 

35644  631 
declare transfer_morphism_nat_int[transfer add return: 
31706  632 
transfer_nat_int_gcd transfer_nat_int_gcd_closures] 
633 

634 
lemma transfer_int_nat_gcd: 

635 
"gcd (int x) (int y) = int (gcd x y)" 

636 
"lcm (int x) (int y) = int (lcm x y)" 

32479  637 
by (unfold gcd_int_def lcm_int_def, auto) 
31706  638 

639 
lemma transfer_int_nat_gcd_closures: 

640 
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0" 

641 
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0" 

642 
by (auto simp add: gcd_int_def lcm_int_def) 

643 

35644  644 
declare transfer_morphism_int_nat[transfer add return: 
31706  645 
transfer_int_nat_gcd transfer_int_nat_gcd_closures] 
646 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

647 
lemma gcd_nat_induct: 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

648 
fixes m n :: nat 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

649 
assumes "\<And>m. P m 0" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

650 
and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

651 
shows "P m n" 
31706  652 
apply (rule gcd_nat.induct) 
653 
apply (case_tac "y = 0") 

654 
using assms apply simp_all 

655 
done 

656 

657 
(* specific to int *) 

658 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

659 
lemma gcd_neg1_int [simp]: "gcd (x::int) y = gcd x y" 
31706  660 
by (simp add: gcd_int_def) 
661 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

662 
lemma gcd_neg2_int [simp]: "gcd (x::int) (y) = gcd x y" 
31706  663 
by (simp add: gcd_int_def) 
664 

61944  665 
lemma abs_gcd_int[simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y" 
31813  666 
by(simp add: gcd_int_def) 
667 

61944  668 
lemma gcd_abs_int: "gcd (x::int) y = gcd \<bar>x\<bar> \<bar>y\<bar>" 
31813  669 
by (simp add: gcd_int_def) 
670 

61944  671 
lemma gcd_abs1_int[simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

672 
by (metis abs_idempotent gcd_abs_int) 
31813  673 

61944  674 
lemma gcd_abs2_int[simp]: "gcd x \<bar>y::int\<bar> = gcd x y" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

675 
by (metis abs_idempotent gcd_abs_int) 
31706  676 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

677 
lemma gcd_cases_int: 
31706  678 
fixes x :: int and y 
679 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)" 

680 
and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (y))" 

681 
and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (x) y)" 

682 
and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (x) (y))" 

683 
shows "P (gcd x y)" 

61944  684 
by (insert assms, auto, arith) 
21256  685 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

686 
lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0" 
31706  687 
by (simp add: gcd_int_def) 
688 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

689 
lemma lcm_neg1_int: "lcm (x::int) y = lcm x y" 
31706  690 
by (simp add: lcm_int_def) 
691 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

692 
lemma lcm_neg2_int: "lcm (x::int) (y) = lcm x y" 
31706  693 
by (simp add: lcm_int_def) 
694 

61944  695 
lemma lcm_abs_int: "lcm (x::int) y = lcm \<bar>x\<bar> \<bar>y\<bar>" 
31706  696 
by (simp add: lcm_int_def) 
21256  697 

61944  698 
lemma abs_lcm_int [simp]: "\<bar>lcm i j::int\<bar> = lcm i j" 
699 
by (simp add:lcm_int_def) 

31814  700 

61944  701 
lemma lcm_abs1_int[simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y" 
702 
by (metis abs_idempotent lcm_int_def) 

31814  703 

61944  704 
lemma lcm_abs2_int[simp]: "lcm x \<bar>y::int\<bar> = lcm x y" 
705 
by (metis abs_idempotent lcm_int_def) 

31814  706 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

707 
lemma lcm_cases_int: 
31706  708 
fixes x :: int and y 
709 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)" 

710 
and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (y))" 

711 
and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (x) y)" 

712 
and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (x) (y))" 

713 
shows "P (lcm x y)" 

41550  714 
using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith 
31706  715 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

716 
lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0" 
31706  717 
by (simp add: lcm_int_def) 
718 

54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

719 
lemma gcd_0_nat: "gcd (x::nat) 0 = x" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

720 
by simp 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

721 

61944  722 
lemma gcd_0_int [simp]: "gcd (x::int) 0 = \<bar>x\<bar>" 
31706  723 
by (unfold gcd_int_def, auto) 
724 

54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

725 
lemma gcd_0_left_nat: "gcd 0 (x::nat) = x" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

726 
by simp 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

727 

61944  728 
lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = \<bar>x\<bar>" 
31706  729 
by (unfold gcd_int_def, auto) 
730 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

731 
lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)" 
31706  732 
by (case_tac "y = 0", auto) 
733 

734 
(* weaker, but useful for the simplifier *) 

735 

62345  736 
lemma gcd_non_0_nat: "y \<noteq> (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)" 
31706  737 
by simp 
738 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

739 
lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1" 
21263  740 
by simp 
21256  741 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

742 
lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" 
60690  743 
by simp 
31706  744 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

745 
lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1" 
31706  746 
by (simp add: gcd_int_def) 
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
30042
diff
changeset

747 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

748 
lemma gcd_idem_nat: "gcd (x::nat) x = x" 
31798  749 
by simp 
31706  750 

61944  751 
lemma gcd_idem_int: "gcd (x::int) x = \<bar>x\<bar>" 
31813  752 
by (auto simp add: gcd_int_def) 
31706  753 

754 
declare gcd_nat.simps [simp del] 

21256  755 

60758  756 
text \<open> 
61799  757 
\medskip @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>. The 
21256  758 
conjunctions don't seem provable separately. 
60758  759 
\<close> 
21256  760 

59008  761 
instance nat :: semiring_gcd 
762 
proof 

763 
fix m n :: nat 

764 
show "gcd m n dvd m" and "gcd m n dvd n" 

765 
proof (induct m n rule: gcd_nat_induct) 

766 
fix m n :: nat 

767 
assume "gcd n (m mod n) dvd m mod n" and "gcd n (m mod n) dvd n" 

768 
then have "gcd n (m mod n) dvd m" 

769 
by (rule dvd_mod_imp_dvd) 

770 
moreover assume "0 < n" 

771 
ultimately show "gcd m n dvd m" 

772 
by (simp add: gcd_non_0_nat) 

773 
qed (simp_all add: gcd_0_nat gcd_non_0_nat) 

774 
next 

775 
fix m n k :: nat 

776 
assume "k dvd m" and "k dvd n" 

777 
then show "k dvd gcd m n" 

778 
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat) 

60686  779 
qed (simp_all add: lcm_nat_def) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59545
diff
changeset

780 

59008  781 
instance int :: ring_gcd 
60686  782 
by standard 
783 
(simp_all add: dvd_int_unfold_dvd_nat gcd_int_def lcm_int_def zdiv_int nat_abs_mult_distrib [symmetric] lcm_gcd gcd_greatest) 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59545
diff
changeset

784 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

785 
lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a" 
31706  786 
by (rule dvd_imp_le, auto) 
787 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

788 
lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b" 
31706  789 
by (rule dvd_imp_le, auto) 
790 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

791 
lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a" 
31706  792 
by (rule zdvd_imp_le, auto) 
21256  793 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

794 
lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b" 
31706  795 
by (rule zdvd_imp_le, auto) 
796 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

797 
lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0  n ~= 0)" 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

798 
by (insert gcd_eq_0_iff [of m n], arith) 
21256  799 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

800 
lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0  n ~= 0)" 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

801 
by (insert gcd_eq_0_iff [of m n], insert gcd_ge_0_int [of m n], arith) 
31706  802 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

803 
lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and> 
31706  804 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 
805 
apply auto 

33657  806 
apply (rule dvd_antisym) 
59008  807 
apply (erule (1) gcd_greatest) 
31706  808 
apply auto 
809 
done 

21256  810 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

811 
lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and> 
31706  812 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 
33657  813 
apply (case_tac "d = 0") 
814 
apply simp 

815 
apply (rule iffI) 

816 
apply (rule zdvd_antisym_nonneg) 

59008  817 
apply (auto intro: gcd_greatest) 
31706  818 
done 
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
30042
diff
changeset

819 

61913  820 
interpretation gcd_nat: 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

821 
semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

822 
by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans) 
31798  823 

61944  824 
lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = \<bar>x\<bar>" 
54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

825 
by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int) 
31798  826 

61944  827 
lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = \<bar>y\<bar>" 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

828 
by (metis gcd_proj1_if_dvd_int gcd.commute) 
31798  829 

60758  830 
text \<open> 
21256  831 
\medskip Multiplication laws 
60758  832 
\<close> 
21256  833 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

834 
lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)" 
61799  835 
\<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close> 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

836 
apply (induct m n rule: gcd_nat_induct) 
31706  837 
apply simp 
21256  838 
apply (case_tac "k = 0") 
45270
d5b5c9259afd
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
huffman
parents:
45264
diff
changeset

839 
apply (simp_all add: gcd_non_0_nat) 
31706  840 
done 
21256  841 

61944  842 
lemma gcd_mult_distrib_int: "\<bar>k::int\<bar> * gcd m n = gcd (k * m) (k * n)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

843 
apply (subst (1 2) gcd_abs_int) 
31813  844 
apply (subst (1 2) abs_mult) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

845 
apply (rule gcd_mult_distrib_nat [transferred]) 
31706  846 
apply auto 
847 
done 

21256  848 

60690  849 
context semiring_gcd 
850 
begin 

21256  851 

60690  852 
lemma coprime_dvd_mult: 
853 
assumes "coprime a b" and "a dvd c * b" 

854 
shows "a dvd c" 

855 
proof (cases "c = 0") 

856 
case True then show ?thesis by simp 

857 
next 

858 
case False 

859 
then have unit: "is_unit (unit_factor c)" by simp 

860 
from \<open>coprime a b\<close> mult_gcd_left [of c a b] 

861 
have "gcd (c * a) (c * b) * unit_factor c = c" 

862 
by (simp add: ac_simps) 

863 
moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c" 

864 
by (simp add: dvd_mult_unit_iff unit) 

865 
ultimately show ?thesis by simp 

866 
qed 

867 

62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

868 
lemma coprime_dvd_mult_iff: 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

869 
assumes "coprime a c" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

870 
shows "a dvd b * c \<longleftrightarrow> a dvd b" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

871 
using assms by (auto intro: coprime_dvd_mult) 
60690  872 

873 
lemma gcd_mult_cancel: 

874 
"coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b" 

875 
apply (rule associated_eqI) 

59008  876 
apply (rule gcd_greatest) 
60690  877 
apply (rule_tac b = c in coprime_dvd_mult) 
878 
apply (simp add: gcd.assoc) 

879 
apply (simp_all add: ac_simps) 

880 
done 

21256  881 

62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

882 
lemma coprime_crossproduct: 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

883 
fixes a b c d 
35368  884 
assumes "coprime a d" and "coprime b c" 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

885 
shows "normalize a * normalize c = normalize b * normalize d 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

886 
\<longleftrightarrow> normalize a = normalize b \<and> normalize c = normalize d" (is "?lhs \<longleftrightarrow> ?rhs") 
35368  887 
proof 
888 
assume ?rhs then show ?lhs by simp 

889 
next 

890 
assume ?lhs 

62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

891 
from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

892 
by (auto intro: dvdI dest: sym) 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

893 
with \<open>coprime a d\<close> have "a dvd b" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

894 
by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric]) 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

895 
from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

896 
by (auto intro: dvdI dest: sym) 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

897 
with \<open>coprime b c\<close> have "b dvd a" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

898 
by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric]) 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

899 
from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

900 
by (auto intro: dvdI dest: sym simp add: mult.commute) 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

901 
with \<open>coprime b c\<close> have "c dvd d" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

902 
by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric]) 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

903 
from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

904 
by (auto intro: dvdI dest: sym simp add: mult.commute) 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

905 
with \<open>coprime a d\<close> have "d dvd c" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

906 
by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric]) 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

907 
from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

908 
by (rule associatedI) 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

909 
moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

910 
by (rule associatedI) 
35368  911 
ultimately show ?rhs .. 
912 
qed 

913 

62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

914 
end 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

915 

759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

916 
lemma coprime_crossproduct_nat: 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

917 
fixes a b c d :: nat 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

918 
assumes "coprime a d" and "coprime b c" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

919 
shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d" 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

920 
using assms coprime_crossproduct [of a d b c] by simp 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

921 

35368  922 
lemma coprime_crossproduct_int: 
923 
fixes a b c d :: int 

924 
assumes "coprime a d" and "coprime b c" 

925 
shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>" 

62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

926 
using assms coprime_crossproduct [of a d b c] by simp 
35368  927 

60758  928 
text \<open>\medskip Addition laws\<close> 
21256  929 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

930 
lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n" 
31706  931 
apply (case_tac "n = 0") 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

932 
apply (simp_all add: gcd_non_0_nat) 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

933 
done 
31706  934 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

935 
lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n" 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

936 
apply (subst (1 2) gcd.commute) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

937 
apply (subst add.commute) 
31706  938 
apply simp 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

939 
done 
31706  940 

941 
(* to do: add the other variations? *) 

942 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

943 
lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m  n) n = gcd m n" 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

944 
by (subst gcd_add1_nat [symmetric]) auto 
31706  945 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

946 
lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n  m) n = gcd m n" 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

947 
apply (subst gcd.commute) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

948 
apply (subst gcd_diff1_nat [symmetric]) 
31706  949 
apply auto 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

950 
apply (subst gcd.commute) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

951 
apply (subst gcd_diff1_nat) 
31706  952 
apply assumption 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

953 
apply (rule gcd.commute) 
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

954 
done 
31706  955 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

956 
lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)" 
31706  957 
apply (frule_tac b = y and a = x in pos_mod_sign) 
958 
apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

959 
apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] 
31706  960 
zmod_zminus1_eq_if) 
961 
apply (frule_tac a = x in pos_mod_bound) 

62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

962 
apply (subst (1 2) gcd.commute) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

963 
apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat 
31706  964 
nat_le_eq_zle) 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

965 
done 
21256  966 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

967 
lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)" 
31706  968 
apply (case_tac "y = 0") 
969 
apply force 

970 
apply (case_tac "y > 0") 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

971 
apply (subst gcd_non_0_int, auto) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

972 
apply (insert gcd_non_0_int [of "y" "x"]) 
35216  973 
apply auto 
31706  974 
done 
975 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

976 
lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

977 
by (metis gcd_red_int mod_add_self1 add.commute) 
31706  978 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

979 
lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n" 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

980 
by (metis gcd_add1_int gcd.commute add.commute) 
21256  981 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

982 
lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n" 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

983 
by (metis mod_mult_self3 gcd.commute gcd_red_nat) 
21256  984 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

985 
lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n" 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

986 
by (metis gcd.commute gcd_red_int mod_mult_self1 add.commute) 
31798  987 

21256  988 

31706  989 
(* to do: differences, and all variations of addition rules 
990 
as simplification rules for nat and int *) 

991 

60689  992 
lemma gcd_dvd_prod_nat: "gcd (m::nat) n dvd k * n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

993 
using mult_dvd_mono [of 1] by auto 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

994 

31706  995 
(* to do: add the three variations of these, and for ints? *) 
996 

31992  997 
lemma finite_divisors_nat[simp]: 
998 
assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}" 

31734  999 
proof 
60512  1000 
have "finite{d. d <= m}" 
1001 
by (blast intro: bounded_nat_set_is_finite) 

31734  1002 
from finite_subset[OF _ this] show ?thesis using assms 
60512  1003 
by (metis Collect_mono dvd_imp_le neq0_conv) 
31734  1004 
qed 
1005 

31995  1006 
lemma finite_divisors_int[simp]: 
31734  1007 
assumes "(i::int) ~= 0" shows "finite{d. d dvd i}" 
1008 
proof 

61944  1009 
have "{d. \<bar>d\<bar> <= \<bar>i\<bar>} = { \<bar>i\<bar> .. \<bar>i\<bar>}" by(auto simp:abs_if) 
1010 
hence "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}" by simp 

31734  1011 
from finite_subset[OF _ this] show ?thesis using assms 
60512  1012 
by (simp add: dvd_imp_le_int subset_iff) 
31734  1013 
qed 
1014 

31995  1015 
lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n" 
1016 
apply(rule antisym) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44845
diff
changeset

1017 
apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le) 
31995  1018 
apply simp 
1019 
done 

1020 

61944  1021 
lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>" 
31995  1022 
apply(rule antisym) 
44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
42871
diff
changeset

1023 
apply(rule Max_le_iff [THEN iffD2]) 
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
42871
diff
changeset

1024 
apply (auto intro: abs_le_D1 dvd_imp_le_int) 
31995  1025 
done 
1026 

31734  1027 
lemma gcd_is_Max_divisors_nat: 
1028 
"m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})" 

1029 
apply(rule Max_eqI[THEN sym]) 

31995  1030 
apply (metis finite_Collect_conjI finite_divisors_nat) 
31734  1031 
apply simp 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

1032 
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat) 
31734  1033 
apply simp 
1034 
done 

1035 

1036 
lemma gcd_is_Max_divisors_int: 

1037 
"m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})" 

1038 
apply(rule Max_eqI[THEN sym]) 

31995  1039 
apply (metis finite_Collect_conjI finite_divisors_int) 
31734  1040 
apply simp 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

1041 
apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le) 
31734  1042 
apply simp 
1043 
done 

1044 

34030
829eb528b226
resorted code equations from "old" number theory version
haftmann
parents:
33946
diff
changeset

1045 
lemma gcd_code_int [code]: 
829eb528b226
resorted code equations from "old" number theory version
haftmann
parents:
33946
diff
changeset

1046 
"gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>" 
829eb528b226
resorted code equations from "old" number theory version
haftmann
parents:
33946
diff
changeset

1047 
by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat) 
829eb528b226
resorted code equations from "old" number theory version
haftmann
parents:
33946
diff
changeset

1048 

22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

1049 

60758  1050 
subsection \<open>Coprimality\<close> 
31706  1051 

60690  1052 
context semiring_gcd 
1053 
begin 

1054 

1055 
lemma div_gcd_coprime: 

1056 
assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0" 

31706  1057 
shows "coprime (a div gcd a b) (b div gcd a b)" 
22367  1058 
proof  
27556  1059 
let ?g = "gcd a b" 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

1060 
let ?a' = "a div ?g" 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

1061 
let ?b' = "b div ?g" 
27556  1062 
let ?g' = "gcd ?a' ?b'" 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

1063 
have dvdg: "?g dvd a" "?g dvd b" by simp_all 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

1064 
have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all 
22367  1065 
from dvdg dvdg' obtain ka kb ka' kb' where 
1066 
kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'" 

22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

1067 
unfolding dvd_def by blast 
58834  1068 
from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" 
1069 
by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"]) 

22367  1070 
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" 
1071 
by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] 

1072 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

35216  1073 
have "?g \<noteq> 0" using nz by simp 
60690  1074 
moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . 
1075 
thm dvd_mult_cancel_left 

1076 
ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp 

22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

1077 
qed 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

1078 

62345  1079 
lemma coprime: 
1080 
"coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)" (is "?P \<longleftrightarrow> ?Q") 

1081 
proof 

1082 
assume ?P then show ?Q by auto 

1083 
next 

1084 
assume ?Q 

1085 
then have "is_unit (gcd a b) \<longleftrightarrow> gcd a b dvd a \<and> gcd a b dvd b" 

1086 
by blast 

1087 
then have "is_unit (gcd a b)" 

1088 
by simp 

1089 
then show ?P 

1090 
by simp 

1091 
qed 

1092 

60690  1093 
end 
1094 

62345  1095 
lemma coprime_nat: 
1096 
"coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)" 

1097 
using coprime [of a b] by simp 

31706  1098 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1099 
lemma coprime_Suc_0_nat: 
62345  1100 
"coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)" 
60690  1101 
using coprime_nat by simp 
31706  1102 

62345  1103 
lemma coprime_int: 
1104 
"coprime (a::int) b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1105 
using gcd_unique_int [of 1 a b] 
31706  1106 
apply clarsimp 
1107 
apply (erule subst) 

1108 
apply (rule iffI) 

1109 
apply force 

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61605
diff
changeset

1110 
using abs_dvd_iff abs_ge_zero apply blast 
59807  1111 
done 
31706  1112 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1113 
lemma gcd_coprime_nat: 
31706  1114 
assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and 
1115 
b: "b = b' * gcd a b" 

1116 
shows "coprime a' b'" 

1117 

1118 
apply (subgoal_tac "a' = a div gcd a b") 

1119 
apply (erule ssubst) 

1120 
apply (subgoal_tac "b' = b div gcd a b") 

1121 
apply (erule ssubst) 

62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

1122 
apply (rule div_gcd_coprime) 
41550  1123 
using z apply force 
31706  1124 
apply (subst (1) b) 
1125 
using z apply force 

1126 
apply (subst (1) a) 

1127 
using z apply force 

41550  1128 
done 
31706  1129 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1130 
lemma gcd_coprime_int: 
31706  1131 
assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and 
1132 
b: "b = b' * gcd a b" 

1133 
shows "coprime a' b'" 

1134 
apply (subgoal_tac "a' = a div gcd a b") 

1135 
apply (erule ssubst) 

1136 
apply (subgoal_tac "b' = b div gcd a b") 

1137 
apply (erule ssubst) 

62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

1138 
apply (rule div_gcd_coprime) 
41550  1139 
using z apply force 
31706  1140 
apply (subst (1) b) 
1141 
using z apply force 

1142 
apply (subst (1) a) 

1143 
using z apply force 

41550  1144 
done 
31706  1145 

60690  1146 
context semiring_gcd 
1147 
begin 

31706  1148 

60690  1149 
lemma coprime_mult: 
1150 
assumes da: "coprime d a" and db: "coprime d b" 

1151 
shows "coprime d (a * b)" 

1152 
apply (subst gcd.commute) 

1153 
using da apply (subst gcd_mult_cancel) 

1154 
apply (subst gcd.commute, assumption) 

1155 
apply (subst gcd.commute, rule db) 

1156 
done 

31706  1157 

60690  1158 
end 
1159 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1160 
lemma coprime_lmult_nat: 
31706  1161 
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" 
1162 
proof  

1163 
have "gcd d a dvd gcd d (a * b)" 

59008  1164 
by (rule gcd_greatest, auto) 
31706  1165 
with dab show ?thesis 
1166 
by auto 

1167 
qed 

1168 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1169 
lemma coprime_lmult_int: 
31798  1170 
assumes "coprime (d::int) (a * b)" shows "coprime d a" 
31706  1171 
proof  
1172 
have "gcd d a dvd gcd d (a * b)" 

59008  1173 
by (rule gcd_greatest, auto) 
31798  1174 
with assms show ?thesis 
31706  1175 
by auto 
1176 
qed 

1177 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1178 
lemma coprime_rmult_nat: 
31798  1179 
assumes "coprime (d::nat) (a * b)" shows "coprime d b" 
31706  1180 
proof  
1181 
have "gcd d b dvd gcd d (a * b)" 

59008  1182 
by (rule gcd_greatest, auto intro: dvd_mult) 
31798  1183 
with assms show ?thesis 
31706  1184 
by auto 
1185 
qed 

1186 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1187 
lemma coprime_rmult_int: 
31706  1188 
assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" 
1189 
proof  

1190 
have "gcd d b dvd gcd d (a * b)" 

59008  1191 
by (rule gcd_greatest, auto intro: dvd_mult) 
31706  1192 
with dab show ?thesis 
1193 
by auto 

1194 
qed 

1195 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1196 
lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow> 
31706  1197 
coprime d a \<and> coprime d b" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1198 
using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b] 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

1199 
coprime_mult [of d a b] 
31706  1200 
by blast 
1201 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1202 
lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow> 
31706  1203 
coprime d a \<and> coprime d b" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1204 
using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b] 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

1205 
coprime_mult [of d a b] 
31706  1206 
by blast 
1207 

52397  1208 
lemma coprime_power_int: 
1209 
assumes "0 < n" shows "coprime (a :: int) (b ^ n) \<longleftrightarrow> coprime a b" 

1210 
using assms 

1211 
proof (induct n) 

1212 
case (Suc n) then show ?case 

1213 
by (cases n) (simp_all add: coprime_mul_eq_int) 

1214 
qed simp 

1215 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1216 
lemma gcd_coprime_exists_nat: 
31706  1217 
assumes nz: "gcd (a::nat) b \<noteq> 0" 
1218 
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'" 

1219 
apply (rule_tac x = "a div gcd a b" in exI) 

1220 
apply (rule_tac x = "b div gcd a b" in exI) 

62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

1221 
using nz apply (auto simp add: div_gcd_coprime dvd_div_mult) 
31706  1222 
done 
1223 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1224 
lemma gcd_coprime_exists_int: 
31706  1225 
assumes nz: "gcd (a::int) b \<noteq> 0" 
1226 
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'" 

1227 
apply (rule_tac x = "a div gcd a b" in exI) 

1228 
apply (rule_tac x = "b div gcd a b" in exI) 

62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

1229 
using nz apply (auto simp add: div_gcd_coprime) 
31706  1230 
done 
1231 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1232 
lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)" 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

1233 
by (induct n) (simp_all add: coprime_mult) 
31706  1234 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1235 
lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)" 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

1236 
by (induct n) (simp_all add: coprime_mult) 
31706  1237 

60690  1238 
context semiring_gcd 
1239 
begin 

1240 

1241 
lemma coprime_exp_left: 

1242 
assumes "coprime a b" 

1243 
shows "coprime (a ^ n) b" 

1244 
using assms by (induct n) (simp_all add: gcd_mult_cancel) 

1245 

1246 
lemma coprime_exp2: 

1247 
assumes "coprime a b" 

1248 
shows "coprime (a ^ n) (b ^ m)" 

1249 
proof (rule coprime_exp_left) 

1250 
from assms show "coprime a (b ^ m)" 

1251 
by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a]) 

1252 
qed 

1253 

1254 
end 

1255 

1256 
lemma gcd_exp_nat: 

1257 
"gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n" 

1258 
proof (cases "a = 0 \<and> b = 0") 

1259 
case True then show ?thesis by (cases "n > 0") (simp_all add: zero_power) 

1260 
next 

1261 
case False 

1262 
then have "coprime (a div gcd a b) (b div gcd a b)" 

1263 
by (auto simp: div_gcd_coprime) 

1264 
then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)" 

1265 
by (simp add: coprime_exp2) 

1266 
then have "gcd ((a div gcd a b)^n * (gcd a b)^n) 

31706  1267 
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" 
60162  1268 
by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral) 
31706  1269 
also have "(a div gcd a b)^n * (gcd a b)^n = a^n" 
60162  1270 
by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib) 
31706  1271 
also have "(b div gcd a b)^n * (gcd a b)^n = b^n" 
60162  1272 
by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib) 
31706  1273 
finally show ?thesis . 
1274 
qed 

1275 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1276 
lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1277 
apply (subst (1 2) gcd_abs_int) 
31706  1278 
apply (subst (1 2) power_abs) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1279 
apply (rule gcd_exp_nat [where n = n, transferred]) 
31706  1280 
apply auto 
1281 
done 

1282 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1283 
lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c" 
31706  1284 
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c" 
1285 
proof 

1286 
let ?g = "gcd a b" 

1287 
{assume "?g = 0" with dc have ?thesis by auto} 

1288 
moreover 

1289 
{assume z: "?g \<noteq> 0" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1290 
from gcd_coprime_exists_nat[OF z] 
31706  1291 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
1292 
by blast 

1293 
have thb: "?g dvd b" by auto 

1294 
from ab'(1) have "a' dvd a" unfolding dvd_def by blast 

1295 
with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp 

1296 
from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

1297 
hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc) 
31706  1298 
with z have th_1: "a' dvd b' * c" by auto 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

1299 
from coprime_dvd_mult [OF ab'(3)] th_1 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

1300 
have thc: "a' dvd c" by (subst (asm) mult.commute, blast) 
31706  1301 
from ab' have "a = ?g*a'" by algebra 
1302 
with thb thc have ?thesis by blast } 

1303 
ultimately show ?thesis by blast 

1304 
qed 

1305 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1306 
lemma division_decomp_int: assumes dc: "(a::int) dvd b * c" 
31706  1307 
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c" 
1308 
proof 

1309 
let ?g = "gcd a b" 

1310 
{assume "?g = 0" with dc have ?thesis by auto} 

1311 
moreover 

1312 
{assume z: "?g \<noteq> 0" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1313 
from gcd_coprime_exists_int[OF z] 
31706  1314 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
1315 
by blast 

1316 
have thb: "?g dvd b" by auto 

1317 
from ab'(1) have "a' dvd a" unfolding dvd_def by blast 

1318 
with dc have th0: "a' dvd b*c" 

1319 
using dvd_trans[of a' a "b*c"] by simp 

1320 
from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto 

60690  1321 
hence "?g*a' dvd ?g * (b' * c)" by (simp add: ac_simps) 
31706  1322 
with z have th_1: "a' dvd b' * c" by auto 
62344
759d684c0e60
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
haftmann
parents:
62343
diff
changeset

1323 
from coprime_dvd_mult [OF ab'(3)] th_1 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

1324 
have thc: "a' dvd c" by (subst (asm) mult.commute, blast) 
31706  1325 
from ab' have "a = ?g*a'" by algebra 
1326 
with thb thc have ?thesis by blast } 

1327 
ultimately show ?thesis by blast 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1328 
qed 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1329 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1330 
lemma pow_divides_pow_nat: 
31706  1331 
assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0" 
1332 
shows "a dvd b" 

1333 
proof 

1334 
let ?g = "gcd a b" 

1335 
from n obtain m where m: "n = Suc m" by (cases n, simp_all) 

1336 
{assume "?g = 0" with ab n have ?thesis by auto } 

1337 
moreover 

