author  haftmann 
Wed, 08 Jul 2015 14:01:39 +0200  
changeset 60686  ea5bc46c11e6 
parent 60597  2da9b632069b 
child 60687  33dbbcb6a8a3 
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 

58889  28 
section {* Greatest common divisor and least common multiple *} 
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 

60686  34 
context semidom_divide 
35 
begin 

36 

37 
lemma divide_1 [simp]: 

38 
"a div 1 = a" 

39 
using nonzero_mult_divide_cancel_left [of 1 a] by simp 

40 

41 
lemma dvd_mult_cancel_left [simp]: 

42 
assumes "a \<noteq> 0" 

43 
shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q") 

44 
proof 

45 
assume ?P then obtain d where "a * c = a * b * d" .. 

46 
with assms have "c = b * d" by (simp add: ac_simps) 

47 
then show ?Q .. 

48 
next 

49 
assume ?Q then obtain d where "c = b * d" .. 

50 
then have "a * c = a * b * d" by (simp add: ac_simps) 

51 
then show ?P .. 

52 
qed 

53 

54 
lemma dvd_mult_cancel_right [simp]: 

55 
assumes "a \<noteq> 0" 

56 
shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q") 

57 
using dvd_mult_cancel_left [of a b c] assms by (simp add: ac_simps) 

58 

59 
lemma div_dvd_iff_mult: 

60 
assumes "b \<noteq> 0" and "b dvd a" 

61 
shows "a div b dvd c \<longleftrightarrow> a dvd c * b" 

62 
proof  

63 
from \<open>b dvd a\<close> obtain d where "a = b * d" .. 

64 
with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps) 

65 
qed 

66 

67 
lemma dvd_div_iff_mult: 

68 
assumes "c \<noteq> 0" and "c dvd b" 

69 
shows "a dvd b div c \<longleftrightarrow> a * c dvd b" 

70 
proof  

71 
from \<open>c dvd b\<close> obtain d where "b = c * d" .. 

72 
with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a]) 

73 
qed 

74 

75 
end 

76 

77 
context algebraic_semidom 

78 
begin 

79 

80 
lemma associated_1 [simp]: 

81 
"associated 1 a \<longleftrightarrow> is_unit a" 

82 
"associated a 1 \<longleftrightarrow> is_unit a" 

83 
by (auto simp add: associated_def) 

84 

85 
end 

86 

31706  87 
declare One_nat_def [simp del] 
88 

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

89 
subsection {* GCD and LCM definitions *} 
31706  90 

31992  91 
class gcd = zero + one + dvd + 
41550  92 
fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
93 
and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 

21256  94 
begin 
95 

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

31706  98 

99 
end 

100 

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

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

104 

105 
class semiring_gcd = normalization_semidom + gcd + 

59008  106 
assumes gcd_dvd1 [iff]: "gcd a b dvd a" 
59977  107 
and gcd_dvd2 [iff]: "gcd a b dvd b" 
108 
and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" 

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

111 
begin 

112 

113 
lemma gcd_greatest_iff [iff]: 

114 
"a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c" 

115 
by (blast intro!: gcd_greatest intro: dvd_trans) 

116 

117 
lemma gcd_0_left [simp]: 

118 
"gcd 0 a = normalize a" 

119 
proof (rule associated_eqI) 

120 
show "associated (gcd 0 a) (normalize a)" 

121 
by (auto intro!: associatedI gcd_greatest) 

122 
show "unit_factor (gcd 0 a) = 1" if "gcd 0 a \<noteq> 0" 

123 
proof  

124 
from that have "unit_factor (normalize (gcd 0 a)) = 1" 

125 
by (rule unit_factor_normalize) 

126 
then show ?thesis by simp 

127 
qed 

128 
qed simp 

129 

130 
lemma gcd_0_right [simp]: 

131 
"gcd a 0 = normalize a" 

132 
proof (rule associated_eqI) 

133 
show "associated (gcd a 0) (normalize a)" 

134 
by (auto intro!: associatedI gcd_greatest) 

135 
show "unit_factor (gcd a 0) = 1" if "gcd a 0 \<noteq> 0" 

136 
proof  

137 
from that have "unit_factor (normalize (gcd a 0)) = 1" 

138 
by (rule unit_factor_normalize) 

139 
then show ?thesis by simp 

140 
qed 

141 
qed simp 

142 

143 
lemma gcd_eq_0_iff [simp]: 

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

145 
proof 

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

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

148 
then show ?Q by simp 

149 
next 

150 
assume ?Q then show ?P by simp 

151 
qed 

152 

153 
lemma unit_factor_gcd: 

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

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

156 
case True then show ?thesis by simp 

157 
next 

158 
case False 

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

160 
by (rule unit_factor_mult_normalize) 

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

162 
by simp 

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

164 
by simp 

165 
with False show ?thesis by simp 

166 
qed 

167 

168 
sublocale gcd!: abel_semigroup gcd 

169 
proof 

170 
fix a b c 

171 
show "gcd a b = gcd b a" 

172 
by (rule associated_eqI) (auto intro: associatedI gcd_greatest simp add: unit_factor_gcd) 

173 
from gcd_dvd1 have "gcd (gcd a b) c dvd a" 

174 
by (rule dvd_trans) simp 

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

176 
by (rule dvd_trans) simp 

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

178 
by (auto intro!: gcd_greatest) 

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

180 
by (rule dvd_trans) simp 

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

182 
by (rule dvd_trans) simp 

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

184 
by (auto intro!: gcd_greatest) 

185 
from P1 P2 have "associated (gcd (gcd a b) c) (gcd a (gcd b c))" 

186 
by (rule associatedI) 

187 
then show "gcd (gcd a b) c = gcd a (gcd b c)" 

188 
by (rule associated_eqI) (simp_all add: unit_factor_gcd) 

189 
qed 

190 

191 
lemma gcd_self [simp]: 

192 
"gcd a a = normalize a" 

193 
proof  

194 
have "a dvd gcd a a" 

195 
by (rule gcd_greatest) simp_all 

196 
then have "associated (gcd a a) (normalize a)" 

197 
by (auto intro: associatedI) 

198 
then show ?thesis 

199 
by (auto intro: associated_eqI simp add: unit_factor_gcd) 

200 
qed 

201 

202 
lemma coprime_1_left [simp]: 

203 
"coprime 1 a" 

204 
by (rule associated_eqI) (simp_all add: unit_factor_gcd) 

205 

206 
lemma coprime_1_right [simp]: 

207 
"coprime a 1" 

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

209 

210 
lemma gcd_mult_left: 

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

212 
proof (cases "c = 0") 

213 
case True then show ?thesis by simp 

214 
next 

215 
case False 

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

217 
by (auto intro: gcd_greatest) 

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

219 
by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute) 

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

221 
by  (rule associated_eqI, auto intro: associated_eqI associatedI simp add: unit_factor_gcd) 

222 
then show ?thesis by (simp add: normalize_mult) 

223 
qed 

224 

225 
lemma gcd_mult_right: 

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

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

228 

229 
lemma mult_gcd_left: 

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

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

232 

233 
lemma mult_gcd_right: 

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

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

236 

237 
lemma lcm_dvd1 [iff]: 

238 
"a dvd lcm a b" 

239 
proof  

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

241 
by (simp add: lcm_gcd normalize_mult div_mult_swap) 

242 
then show ?thesis 

243 
by (simp add: lcm_gcd) 

244 
qed 

245 

246 
lemma lcm_dvd2 [iff]: 

247 
"b dvd lcm a b" 

248 
proof  

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

250 
by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps) 

251 
then show ?thesis 

252 
by (simp add: lcm_gcd) 

253 
qed 

254 

255 
lemma lcm_least: 

256 
assumes "a dvd c" and "b dvd c" 

257 
shows "lcm a b dvd c" 

258 
proof (cases "c = 0") 

259 
case True then show ?thesis by simp 

260 
next 

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

262 
show ?thesis 

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

264 
case True with assms show ?thesis by simp 

265 
next 

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

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

268 
by (simp_all add: mult_dvd_mono) 

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

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

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

272 
using U by (simp add: dvd_mult_unit_iff) 

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

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

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

276 
using False by (simp add: div_dvd_iff_mult ac_simps) 

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

278 
qed 

279 
qed 

280 

281 
lemma lcm_least_iff [iff]: 

282 
"lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c" 

283 
by (blast intro!: lcm_least intro: dvd_trans) 

284 

285 
lemma normalize_lcm [simp]: 

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

287 
by (simp add: lcm_gcd dvd_normalize_div) 

288 

289 
lemma lcm_0_left [simp]: 

290 
"lcm 0 a = 0" 

291 
by (simp add: lcm_gcd) 

292 

293 
lemma lcm_0_right [simp]: 

294 
"lcm a 0 = 0" 

295 
by (simp add: lcm_gcd) 

296 

297 
lemma lcm_eq_0_iff: 

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

299 
proof 

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

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

302 
by (simp add: lcm_gcd) 

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

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

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

306 
by simp 

307 
then show ?Q by simp 

308 
next 

309 
assume ?Q then show ?P by auto 

310 
qed 

311 

312 
lemma unit_factor_lcm : 

313 
"unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)" 

314 
by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd) 

315 

316 
sublocale lcm!: abel_semigroup lcm 

317 
proof 

318 
fix a b c 

319 
show "lcm a b = lcm b a" 

320 
by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div) 

321 
have "associated (lcm (lcm a b) c) (lcm a (lcm b c))" 

322 
by (auto intro!: associatedI lcm_least 

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

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

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

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

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

328 
by (rule associated_eqI) (simp_all add: unit_factor_lcm lcm_eq_0_iff) 

329 
qed 

330 

331 
lemma lcm_self [simp]: 

332 
"lcm a a = normalize a" 

333 
proof  

334 
have "lcm a a dvd a" 

335 
by (rule lcm_least) simp_all 

336 
then have "associated (lcm a a) (normalize a)" 

337 
by (auto intro: associatedI) 

338 
then show ?thesis 

339 
by (rule associated_eqI) (auto simp add: unit_factor_lcm) 

340 
qed 

341 

342 
lemma gcd_mult_lcm [simp]: 

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

344 
by (simp add: lcm_gcd normalize_mult) 

345 

346 
lemma lcm_mult_gcd [simp]: 

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

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

349 

350 
lemma gcd_lcm: 

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

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

353 
proof  

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

355 
by (simp add: lcm_eq_0_iff) 

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

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

358 
by (simp_all add: normalize_mult) 

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

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

361 
qed 

362 

363 
lemma lcm_1_left [simp]: 

364 
"lcm 1 a = normalize a" 

365 
by (simp add: lcm_gcd) 

366 

367 
lemma lcm_1_right [simp]: 

368 
"lcm a 1 = normalize a" 

369 
by (simp add: lcm_gcd) 

370 

371 
lemma lcm_mult_left: 

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

373 
by (cases "c = 0") 

374 
(simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps, 

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

376 

377 
lemma lcm_mult_right: 

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

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

380 

381 
lemma mult_lcm_left: 

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

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

384 

385 
lemma mult_lcm_right: 

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

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

388 

389 
end 

390 

391 
class semiring_Gcd = semiring_gcd + Gcd + 

392 
assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a" 

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

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

395 
begin 

396 

397 
lemma Gcd_empty [simp]: 

398 
"Gcd {} = 0" 

399 
by (rule dvd_0_left, rule Gcd_greatest) simp 

400 

401 
lemma Gcd_0_iff [simp]: 

402 
"Gcd A = 0 \<longleftrightarrow> (\<forall>a\<in>A. a = 0)" (is "?P \<longleftrightarrow> ?Q") 

403 
proof 

404 
assume ?P 

405 
show ?Q 

406 
proof 

407 
fix a 

408 
assume "a \<in> A" 

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

410 
with \<open>?P\<close> show "a = 0" by simp 

411 
qed 

412 
next 

413 
assume ?Q 

414 
have "0 dvd Gcd A" 

415 
proof (rule Gcd_greatest) 

416 
fix a 

417 
assume "a \<in> A" 

418 
with \<open>?Q\<close> have "a = 0" by simp 

419 
then show "0 dvd a" by simp 

420 
qed 

421 
then show ?P by simp 

422 
qed 

423 

424 
lemma unit_factor_Gcd: 

425 
"unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)" 

426 
proof (cases "Gcd A = 0") 

427 
case True then show ?thesis by simp 

428 
next 

429 
case False 

430 
from unit_factor_mult_normalize 

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

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

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

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

435 
with False show ?thesis by simp 

436 
qed 

437 

438 
lemma Gcd_UNIV [simp]: 

439 
"Gcd UNIV = 1" 

440 
by (rule associated_eqI) (auto intro: Gcd_dvd simp add: unit_factor_Gcd) 

441 

442 
lemma Gcd_eq_1_I: 

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

444 
shows "Gcd A = 1" 

445 
proof  

446 
from assms have "is_unit (Gcd A)" 

447 
by (blast intro: Gcd_dvd dvd_unit_imp_unit) 

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

449 
by (rule is_unit_normalize) 

450 
then show ?thesis 

451 
by simp 

452 
qed 

453 

454 
lemma Gcd_insert [simp]: 

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

456 
proof  

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

458 
by (auto intro: Gcd_dvd Gcd_greatest) 

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

460 
proof (rule Gcd_greatest) 

461 
fix b 

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

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

464 
proof 

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

466 
next 

467 
assume "b \<in> A" 

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

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

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

471 
qed 

472 
qed 

473 
ultimately have "associated (Gcd (insert a A)) (gcd a (Gcd A))" 

474 
by (rule associatedI) 

475 
then show ?thesis 

476 
by (rule associated_eqI) (simp_all add: unit_factor_gcd unit_factor_Gcd) 

477 
qed 

478 

479 
lemma dvd_Gcd:  \<open>FIXME remove\<close> 

480 
"\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A" 

481 
by (blast intro: Gcd_greatest) 

482 

483 
lemma Gcd_set [code_unfold]: 

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

485 
by (induct as) simp_all 

486 

487 
end 

488 

489 
class semiring_Lcm = semiring_Gcd + 

490 
assumes Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}" 

491 
begin 

492 

493 
lemma dvd_Lcm: 

494 
assumes "a \<in> A" 

495 
shows "a dvd Lcm A" 

496 
using assms by (auto intro: Gcd_greatest simp add: Lcm_Gcd) 

497 

498 
lemma Gcd_image_normalize [simp]: 

499 
"Gcd (normalize ` A) = Gcd A" 

500 
proof  

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

502 
proof  

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

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

505 
by (rule gcd_dvd1) 

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

507 
by simp 

508 
qed 

509 
then have "associated (Gcd (normalize ` A)) (Gcd A)" 

510 
by (auto intro!: associatedI Gcd_greatest intro: Gcd_dvd) 

511 
then show ?thesis 

512 
by (rule associated_eqI) (simp_all add: unit_factor_Gcd) 

513 
qed 

514 

515 
lemma Lcm_least: 

516 
assumes "\<And>b. b \<in> A \<Longrightarrow> b dvd a" 

517 
shows "Lcm A dvd a" 

518 
using assms by (auto intro: Gcd_dvd simp add: Lcm_Gcd) 

519 

520 
lemma normalize_Lcm [simp]: 

521 
"normalize (Lcm A) = Lcm A" 

522 
by (simp add: Lcm_Gcd) 

523 

524 
lemma unit_factor_Lcm: 

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

526 
proof (cases "Lcm A = 0") 

527 
case True then show ?thesis by simp 

528 
next 

529 
case False 

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

531 
by blast 

532 
with False show ?thesis 

533 
by simp 

534 
qed 

535 

536 
lemma Lcm_empty [simp]: 

537 
"Lcm {} = 1" 

538 
by (simp add: Lcm_Gcd) 

539 

540 
lemma Lcm_1_iff [simp]: 

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

542 
proof 

543 
assume ?P 

544 
show ?Q 

545 
proof 

546 
fix a 

547 
assume "a \<in> A" 

548 
then have "a dvd Lcm A" 

549 
by (rule dvd_Lcm) 

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

551 
by simp 

552 
qed 

553 
next 

554 
assume ?Q 

555 
then have "is_unit (Lcm A)" 

556 
by (blast intro: Lcm_least) 

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

558 
by (rule is_unit_normalize) 

559 
then show ?P 

560 
by simp 

561 
qed 

562 

563 
lemma Lcm_UNIV [simp]: 

564 
"Lcm UNIV = 0" 

565 
proof  

566 
have "0 dvd Lcm UNIV" 

567 
by (rule dvd_Lcm) simp 

568 
then show ?thesis 

569 
by simp 

570 
qed 

571 

572 
lemma Lcm_eq_0_I: 

573 
assumes "0 \<in> A" 

574 
shows "Lcm A = 0" 

575 
proof  

576 
from assms have "0 dvd Lcm A" 

577 
by (rule dvd_Lcm) 

578 
then show ?thesis 

579 
by simp 

580 
qed 

581 

582 
lemma Gcd_Lcm: 

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

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

585 
simp add: unit_factor_Gcd unit_factor_Lcm) 

586 

587 
lemma Lcm_insert [simp]: 

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

589 
proof (rule sym) 

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

591 
by (auto intro: dvd_Lcm Lcm_least) 

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

593 
proof (rule Lcm_least) 

594 
fix b 

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

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

597 
proof 

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

599 
next 

600 
assume "b \<in> A" 

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

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

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

604 
qed 

605 
qed 

606 
ultimately have "associated (lcm a (Lcm A)) (Lcm (insert a A))" 

607 
by (rule associatedI) 

608 
then show "lcm a (Lcm A) = Lcm (insert a A)" 

609 
by (rule associated_eqI) (simp_all add: unit_factor_lcm unit_factor_Lcm lcm_eq_0_iff) 

610 
qed 

611 

612 
lemma Lcm_set [code_unfold]: 

613 
"Lcm (set as) = foldr lcm as 1" 

614 
by (induct as) simp_all 

615 

616 
end 

59008  617 

618 
class ring_gcd = comm_ring_1 + semiring_gcd 

619 

31706  620 
instantiation nat :: gcd 
621 
begin 

21256  622 

31706  623 
fun 
624 
gcd_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

625 
where 

626 
"gcd_nat x y = 

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

628 

629 
definition 

630 
lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

631 
where 

632 
"lcm_nat x y = x * y div (gcd x y)" 

633 

634 
instance proof qed 

635 

636 
end 

637 

638 
instantiation int :: gcd 

639 
begin 

21256  640 

31706  641 
definition 
642 
gcd_int :: "int \<Rightarrow> int \<Rightarrow> int" 

643 
where 

644 
"gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))" 

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

645 

31706  646 
definition 
647 
lcm_int :: "int \<Rightarrow> int \<Rightarrow> int" 

648 
where 

649 
"lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))" 

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

650 

31706  651 
instance proof qed 
652 

653 
end 

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

654 

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

655 

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

656 
subsection {* Transfer setup *} 
31706  657 

658 
lemma transfer_nat_int_gcd: 

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

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

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

663 

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

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

667 
by (auto simp add: gcd_int_def lcm_int_def) 

668 

35644  669 
declare transfer_morphism_nat_int[transfer add return: 
31706  670 
transfer_nat_int_gcd transfer_nat_int_gcd_closures] 
671 

672 
lemma transfer_int_nat_gcd: 

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

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

32479  675 
by (unfold gcd_int_def lcm_int_def, auto) 
31706  676 

677 
lemma transfer_int_nat_gcd_closures: 

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

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

680 
by (auto simp add: gcd_int_def lcm_int_def) 

681 

35644  682 
declare transfer_morphism_int_nat[transfer add return: 
31706  683 
transfer_int_nat_gcd transfer_int_nat_gcd_closures] 
684 

685 

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

686 
subsection {* GCD properties *} 
31706  687 

688 
(* was gcd_induct *) 

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

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

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

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

692 
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

693 
shows "P m n" 
31706  694 
apply (rule gcd_nat.induct) 
695 
apply (case_tac "y = 0") 

696 
using assms apply simp_all 

697 
done 

698 

699 
(* specific to int *) 

700 

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

701 
lemma gcd_neg1_int [simp]: "gcd (x::int) y = gcd x y" 
31706  702 
by (simp add: gcd_int_def) 
703 

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

704 
lemma gcd_neg2_int [simp]: "gcd (x::int) (y) = gcd x y" 
31706  705 
by (simp add: gcd_int_def) 
706 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

707 
lemma gcd_neg_numeral_1_int [simp]: 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

708 
"gcd ( numeral n :: int) x = gcd (numeral n) x" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

709 
by (fact gcd_neg1_int) 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

710 

03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

711 
lemma gcd_neg_numeral_2_int [simp]: 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

712 
"gcd x ( numeral n :: int) = gcd x (numeral n)" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

713 
by (fact gcd_neg2_int) 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

714 

31813  715 
lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y" 
716 
by(simp add: gcd_int_def) 

717 

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

718 
lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)" 
31813  719 
by (simp add: gcd_int_def) 
720 

721 
lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y" 

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

722 
by (metis abs_idempotent gcd_abs_int) 
31813  723 

724 
lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y" 

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

725 
by (metis abs_idempotent gcd_abs_int) 
31706  726 

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

727 
lemma gcd_cases_int: 
31706  728 
fixes x :: int and y 
729 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)" 

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

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

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

733 
shows "P (gcd x y)" 

35216  734 
by (insert assms, auto, arith) 
21256  735 

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

736 
lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0" 
31706  737 
by (simp add: gcd_int_def) 
738 

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

739 
lemma lcm_neg1_int: "lcm (x::int) y = lcm x y" 
31706  740 
by (simp add: lcm_int_def) 
741 

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

742 
lemma lcm_neg2_int: "lcm (x::int) (y) = lcm x y" 
31706  743 
by (simp add: lcm_int_def) 
744 

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

745 
lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)" 
31706  746 
by (simp add: lcm_int_def) 
21256  747 

31814  748 
lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j" 
749 
by(simp add:lcm_int_def) 

750 

751 
lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y" 

752 
by (metis abs_idempotent lcm_int_def) 

753 

754 
lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y" 

755 
by (metis abs_idempotent lcm_int_def) 

756 

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

757 
lemma lcm_cases_int: 
31706  758 
fixes x :: int and y 
759 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)" 

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

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

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

763 
shows "P (lcm x y)" 

41550  764 
using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith 
31706  765 

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

766 
lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0" 
31706  767 
by (simp add: lcm_int_def) 
768 

769 
(* was gcd_0, etc. *) 

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

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

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

772 

31706  773 
(* was igcd_0, etc. *) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

774 
lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x" 
31706  775 
by (unfold gcd_int_def, auto) 
776 

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

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

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

779 

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

780 
lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x" 
31706  781 
by (unfold gcd_int_def, auto) 
782 

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

783 
lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)" 
31706  784 
by (case_tac "y = 0", auto) 
785 

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

787 

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

788 
lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)" 
31706  789 
by simp 
790 

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

791 
lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1" 
21263  792 
by simp 
21256  793 

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

794 
lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" 
31706  795 
by (simp add: One_nat_def) 
796 

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

797 
lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1" 
31706  798 
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

799 

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

800 
lemma gcd_idem_nat: "gcd (x::nat) x = x" 
31798  801 
by simp 
31706  802 

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

803 
lemma gcd_idem_int: "gcd (x::int) x = abs x" 
31813  804 
by (auto simp add: gcd_int_def) 
31706  805 

806 
declare gcd_nat.simps [simp del] 

21256  807 

808 
text {* 

27556  809 
\medskip @{term "gcd m n"} divides @{text m} and @{text n}. The 
21256  810 
conjunctions don't seem provable separately. 
811 
*} 

812 

59008  813 
instance nat :: semiring_gcd 
814 
proof 

815 
fix m n :: nat 

816 
show "gcd m n dvd m" and "gcd m n dvd n" 

817 
proof (induct m n rule: gcd_nat_induct) 

818 
fix m n :: nat 

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

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

821 
by (rule dvd_mod_imp_dvd) 

822 
moreover assume "0 < n" 

823 
ultimately show "gcd m n dvd m" 

824 
by (simp add: gcd_non_0_nat) 

825 
qed (simp_all add: gcd_0_nat gcd_non_0_nat) 

826 
next 

827 
fix m n k :: nat 

828 
assume "k dvd m" and "k dvd n" 

829 
then show "k dvd gcd m n" 

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

60686  831 
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

832 

59008  833 
instance int :: ring_gcd 
60686  834 
by standard 
835 
(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

836 

31730  837 
lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m" 
59008  838 
by (metis gcd_dvd1 dvd_trans) 
31730  839 

840 
lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n" 

59008  841 
by (metis gcd_dvd2 dvd_trans) 
31730  842 

843 
lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m" 

59008  844 
by (metis gcd_dvd1 dvd_trans) 
31730  845 

846 
lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n" 

59008  847 
by (metis gcd_dvd2 dvd_trans) 
31730  848 

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

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

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

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

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

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

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

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

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

861 
lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) = 
31706  862 
(k dvd m & k dvd n)" 
59008  863 
by (blast intro!: gcd_greatest intro: dvd_trans) 
31706  864 

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

865 
lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)" 
59008  866 
by (blast intro!: gcd_greatest intro: dvd_trans) 
21256  867 

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

868 
lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

869 
by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat) 
21256  870 

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

871 
lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)" 
31706  872 
by (auto simp add: gcd_int_def) 
21256  873 

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

874 
lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0  n ~= 0)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

875 
by (insert gcd_zero_nat [of m n], arith) 
21256  876 

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

877 
lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0  n ~= 0)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

878 
by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith) 
31706  879 

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

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

33657  883 
apply (rule dvd_antisym) 
59008  884 
apply (erule (1) gcd_greatest) 
31706  885 
apply auto 
886 
done 

21256  887 

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

888 
lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and> 
31706  889 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 
33657  890 
apply (case_tac "d = 0") 
891 
apply simp 

892 
apply (rule iffI) 

893 
apply (rule zdvd_antisym_nonneg) 

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

896 

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

897 
interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

898 
+ gcd_nat: semilattice_neutr_order "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 0 "op dvd" "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)" 
60686  899 
apply standard 
900 
apply (auto intro: dvd_antisym dvd_trans)[2] 

59545
12a6088ed195
explicit equivalence for strict order on lattices
haftmann
parents:
59497
diff
changeset

901 
apply (metis dvd.dual_order.refl gcd_unique_nat)+ 
54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

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

903 

60686  904 
interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int" .. 
54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

905 

60686  906 
lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat] 
907 
lemmas gcd_commute_nat = gcd.commute [where ?'a = nat] 

908 
lemmas gcd_left_commute_nat = gcd.left_commute [where ?'a = nat] 

909 
lemmas gcd_assoc_int = gcd.assoc [where ?'a = int] 

910 
lemmas gcd_commute_int = gcd.commute [where ?'a = int] 

911 
lemmas gcd_left_commute_int = gcd.left_commute [where ?'a = int] 

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

912 

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

913 
lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

914 

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

915 
lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

916 

31798  917 
lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x" 
54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

918 
by (fact gcd_nat.absorb1) 
31798  919 

920 
lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y" 

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

921 
by (fact gcd_nat.absorb2) 
31798  922 

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

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

924 
by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int) 
31798  925 

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

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

927 
by (metis gcd_proj1_if_dvd_int gcd_commute_int) 
31798  928 

21256  929 
text {* 
930 
\medskip Multiplication laws 

931 
*} 

932 

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

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

935 
apply (induct m n rule: gcd_nat_induct) 
31706  936 
apply simp 
21256  937 
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

938 
apply (simp_all add: gcd_non_0_nat) 
31706  939 
done 
21256  940 

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

941 
lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

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

944 
apply (rule gcd_mult_distrib_nat [transferred]) 
31706  945 
apply auto 
946 
done 

21256  947 

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

948 
lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

949 
apply (insert gcd_mult_distrib_nat [of m k n]) 
21256  950 
apply simp 
951 
apply (erule_tac t = m in ssubst) 

952 
apply simp 

953 
done 

954 

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

955 
lemma coprime_dvd_mult_int: 
31813  956 
"coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m" 
957 
apply (subst abs_dvd_iff [symmetric]) 

958 
apply (subst dvd_abs_iff [symmetric]) 

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

959 
apply (subst (asm) gcd_abs_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

960 
apply (rule coprime_dvd_mult_nat [transferred]) 
31813  961 
prefer 4 apply assumption 
962 
apply auto 

963 
apply (subst abs_mult [symmetric], auto) 

31706  964 
done 
965 

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

966 
lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow> 
31706  967 
(k dvd m * n) = (k dvd m)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

968 
by (auto intro: coprime_dvd_mult_nat) 
31706  969 

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

970 
lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow> 
31706  971 
(k dvd m * n) = (k dvd m)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

972 
by (auto intro: coprime_dvd_mult_int) 
31706  973 

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

974 
lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n" 
33657  975 
apply (rule dvd_antisym) 
59008  976 
apply (rule gcd_greatest) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

977 
apply (rule_tac n = k in coprime_dvd_mult_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

978 
apply (simp add: gcd_assoc_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

979 
apply (simp add: gcd_commute_nat) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

980 
apply (simp_all add: mult.commute) 
31706  981 
done 
21256  982 

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

983 
lemma gcd_mult_cancel_int: 
31813  984 
"coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

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

987 
apply (rule gcd_mult_cancel_nat [transferred], auto) 
31706  988 
done 
21256  989 

35368  990 
lemma coprime_crossproduct_nat: 
991 
fixes a b c d :: nat 

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

993 
shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d" (is "?lhs \<longleftrightarrow> ?rhs") 

994 
proof 

995 
assume ?rhs then show ?lhs by simp 

996 
next 

997 
assume ?lhs 

998 
from `?lhs` have "a dvd b * d" by (auto intro: dvdI dest: sym) 

999 
with `coprime a d` have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat) 

1000 
from `?lhs` have "b dvd a * c" by (auto intro: dvdI dest: sym) 

1001 
with `coprime b c` have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat) 

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

1002 
from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult.commute) 
35368  1003 
with `coprime b c` have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

1004 
from `?lhs` have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult.commute) 
35368  1005 
with `coprime a d` have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat) 
1006 
from `a dvd b` `b dvd a` have "a = b" by (rule Nat.dvd.antisym) 

1007 
moreover from `c dvd d` `d dvd c` have "c = d" by (rule Nat.dvd.antisym) 

1008 
ultimately show ?rhs .. 

1009 
qed 

1010 

1011 
lemma coprime_crossproduct_int: 

1012 
fixes a b c d :: int 

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

1014 
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>" 

1015 
using assms by (intro coprime_crossproduct_nat [transferred]) auto 

1016 

21256  1017 
text {* \medskip Addition laws *} 
1018 

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

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

1021 
apply (simp_all add: gcd_non_0_nat) 
31706  1022 
done 
1023 

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

1024 
lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

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

1026 
apply (subst add.commute) 
31706  1027 
apply simp 
1028 
done 

1029 

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

1031 

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

1032 
lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m  n) n = gcd m n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1033 
by (subst gcd_add1_nat [symmetric], auto) 
31706  1034 

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

1035 
lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n  m) n = gcd m n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1036 
apply (subst gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1037 
apply (subst gcd_diff1_nat [symmetric]) 
31706  1038 
apply auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1039 
apply (subst gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1040 
apply (subst gcd_diff1_nat) 
31706  1041 
apply assumption 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1042 
apply (rule gcd_commute_nat) 
31706  1043 
done 
1044 

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

1045 
lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)" 
31706  1046 
apply (frule_tac b = y and a = x in pos_mod_sign) 
1047 
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

1048 
apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] 
31706  1049 
zmod_zminus1_eq_if) 
1050 
apply (frule_tac a = x in pos_mod_bound) 

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

1051 
apply (subst (1 2) gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1052 
apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat 
31706  1053 
nat_le_eq_zle) 
1054 
done 

21256  1055 

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

1056 
lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)" 
31706  1057 
apply (case_tac "y = 0") 
1058 
apply force 

1059 
apply (case_tac "y > 0") 

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

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

1061 
apply (insert gcd_non_0_int [of "y" "x"]) 
35216  1062 
apply auto 
31706  1063 
done 
1064 

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

1065 
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

1066 
by (metis gcd_red_int mod_add_self1 add.commute) 
31706  1067 

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

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

1069 
by (metis gcd_add1_int gcd_commute_int add.commute) 
21256  1070 

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

1071 
lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1072 
by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat) 
21256  1073 

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

1074 
lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

1075 
by (metis gcd_commute_int gcd_red_int mod_mult_self1 add.commute) 
31798  1076 

21256  1077 

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

1080 

31798  1081 
(* FIXME remove iff *) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

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

1083 
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

1084 

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

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

31734  1089 
proof 
60512  1090 
have "finite{d. d <= m}" 
1091 
by (blast intro: bounded_nat_set_is_finite) 

31734  1092 
from finite_subset[OF _ this] show ?thesis using assms 
60512  1093 
by (metis Collect_mono dvd_imp_le neq0_conv) 
31734  1094 
qed 
1095 

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

1099 
have "{d. abs d <= abs i} = { abs i .. abs i}" by(auto simp:abs_if) 

1100 
hence "finite{d. abs d <= abs i}" by simp 

1101 
from finite_subset[OF _ this] show ?thesis using assms 

60512  1102 
by (simp add: dvd_imp_le_int subset_iff) 
31734  1103 
qed 
1104 

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

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

1107 
apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le) 
31995  1108 
apply simp 
1109 
done 

1110 

1111 
lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n" 

1112 
apply(rule antisym) 

44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
42871
diff
changeset

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

1114 
apply (auto intro: abs_le_D1 dvd_imp_le_int) 
31995  1115 
done 
1116 

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

1119 
apply(rule Max_eqI[THEN sym]) 

31995  1120 
apply (metis finite_Collect_conjI finite_divisors_nat) 
31734  1121 
apply simp 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1122 
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat) 
31734  1123 
apply simp 
1124 
done 

1125 

1126 
lemma gcd_is_Max_divisors_int: 

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

1128 
apply(rule Max_eqI[THEN sym]) 

31995  1129 
apply (metis finite_Collect_conjI finite_divisors_int) 
31734  1130 
apply simp 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1131 
apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le) 
31734  1132 
apply simp 
1133 
done 

1134 

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

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

1136 
"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

1137 
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

1138 

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

1139 

31706  1140 
subsection {* Coprimality *} 
1141 

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

1142 
lemma div_gcd_coprime_nat: 
31706  1143 
assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0" 
1144 
shows "coprime (a div gcd a b) (b div gcd a b)" 

22367  1145 
proof  
27556  1146 
let ?g = "gcd a b" 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

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

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

1150 
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

1151 
have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all 
22367  1152 
from dvdg dvdg' obtain ka kb ka' kb' where 
1153 
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

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

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

1159 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

35216  1160 
have "?g \<noteq> 0" using nz by simp 
31706  1161 
then have gp: "?g > 0" by arith 
59008  1162 
from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . 
22367  1163 
with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

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

1165 

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

1166 
lemma div_gcd_coprime_int: 
31706  1167 
assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0" 
1168 
shows "coprime (a div gcd a b) (b div gcd a b)" 

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

1169 
apply (subst (1 2 3) gcd_abs_int) 
31813  1170 
apply (subst (1 2) abs_div) 
1171 
apply simp 

1172 
apply simp 

1173 
apply(subst (1 2) abs_gcd_int) 

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

1174 
apply (rule div_gcd_coprime_nat [transferred]) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1175 
using nz apply (auto simp add: gcd_abs_int [symmetric]) 
31706  1176 
done 
1177 

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

1178 
lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1179 
using gcd_unique_nat[of 1 a b, simplified] by auto 
31706  1180 

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

1181 
lemma coprime_Suc_0_nat: 
31706  1182 
"coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1183 
using coprime_nat by (simp add: One_nat_def) 
31706  1184 

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

1185 
lemma coprime_int: "coprime (a::int) b \<longleftrightarrow> 
31706  1186 
(\<forall>d. d >= 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

1187 
using gcd_unique_int [of 1 a b] 
31706  1188 
apply clarsimp 
1189 
apply (erule subst) 

1190 
apply (rule iffI) 

1191 
apply force 

59807  1192 
apply (drule_tac x = "abs e" for e in exI) 
1193 
apply (case_tac "e >= 0" for e :: int) 

31706  1194 
apply force 
1195 
apply force 

59807  1196 
done 
31706  1197 

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

1198 
lemma gcd_coprime_nat: 
31706  1199 
assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and 
1200 
b: "b = b' * gcd a b" 

1201 
shows "coprime a' b'" 

1202 

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

1204 
apply (erule ssubst) 

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

1206 
apply (erule ssubst) 

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

1207 
apply (rule div_gcd_coprime_nat) 
41550  1208 
using z apply force 
31706  1209 
apply (subst (1) b) 
1210 
using z apply force 

1211 
apply (subst (1) a) 

1212 
using z apply force 

41550  1213 
done 
31706  1214 

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

1215 
lemma gcd_coprime_int: 
31706  1216 
assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and 
1217 
b: "b = b' * gcd a b" 

1218 
shows "coprime a' b'" 

1219 

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

1221 
apply (erule ssubst) 

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

1223 
apply (erule ssubst) 

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

1224 
apply (rule div_gcd_coprime_int) 
41550  1225 
using z apply force 
31706  1226 
apply (subst (1) b) 
1227 
using z apply force 

1228 
apply (subst (1) a) 

1229 
using z apply force 

41550  1230 
done 
31706  1231 

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

1232 
lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b" 
31706  1233 
shows "coprime d (a * b)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1234 
apply (subst gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1235 
using da apply (subst gcd_mult_cancel_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1236 
apply (subst gcd_commute_nat, assumption) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1237 
apply (subst gcd_commute_nat, rule db) 
31706  1238 
done 
1239 

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

1240 
lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b" 
31706  1241 
shows "coprime d (a * b)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1242 
apply (subst gcd_commute_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1243 
using da apply (subst gcd_mult_cancel_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1244 
apply (subst gcd_commute_int, assumption) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1245 
apply (subst gcd_commute_int, rule db) 
31706  1246 
done 
1247 

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

1248 
lemma coprime_lmult_nat: 
31706  1249 
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" 
1250 
proof  

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

59008  1252 
by (rule gcd_greatest, auto) 
31706  1253 
with dab show ?thesis 
1254 
by auto 

1255 
qed 

1256 

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

1257 
lemma coprime_lmult_int: 
31798  1258 
assumes "coprime (d::int) (a * b)" shows "coprime d a" 
31706  1259 
proof  
1260 
have "gcd d a dvd gcd d (a * b)" 

59008  1261 
by (rule gcd_greatest, auto) 
31798  1262 
with assms show ?thesis 
31706  1263 
by auto 
1264 
qed 

1265 

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

1266 
lemma coprime_rmult_nat: 
31798  1267 
assumes "coprime (d::nat) (a * b)" shows "coprime d b" 
31706  1268 
proof  
1269 
have "gcd d b dvd gcd d (a * b)" 

59008  1270 
by (rule gcd_greatest, auto intro: dvd_mult) 
31798  1271 
with assms show ?thesis 
31706  1272 
by auto 
1273 
qed 

1274 

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

1275 
lemma coprime_rmult_int: 
31706  1276 
assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" 
1277 
proof  

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

59008  1279 
by (rule gcd_greatest, auto intro: dvd_mult) 
31706  1280 
with dab show ?thesis 
1281 
by auto 

1282 
qed 

1283 

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

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

1286 
using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b] 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1287 
coprime_mult_nat[of d a b] 
31706  1288 
by blast 
1289 

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

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

1292 
using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b] 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1293 
coprime_mult_int[of d a b] 
31706  1294 
by blast 
1295 

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

1298 
using assms 

1299 
proof (induct n) 

1300 
case (Suc n) then show ?case 

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

1302 
qed simp 

1303 

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

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

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

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

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

1309 
using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult) 
31706  1310 
done 
1311 

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

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

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

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

59008  1317 
using nz apply (auto simp add: div_gcd_coprime_int) 
31706  1318 
done 
1319 

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

1320 
lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)" 
60596  1321 
by (induct n) (simp_all add: coprime_mult_nat) 
31706  1322 

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

1323 
lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)" 
60596  1324 
by (induct n) (simp_all add: coprime_mult_int) 
31706  1325 

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

1326 
lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)" 
60686  1327 
by (simp add: coprime_exp_nat ac_simps) 
31706  1328 

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

1329 
lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)" 
60686  1330 
by (simp add: coprime_exp_int ac_simps) 
31706  1331 

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

1332 
lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n" 
31706  1333 
proof (cases) 
1334 
assume "a = 0 & b = 0" 

1335 
thus ?thesis by simp 

1336 
next assume "~(a = 0 & b = 0)" 

1337 
hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)" 

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

1338 
by (auto simp:div_gcd_coprime_nat) 
31706  1339 
hence "gcd ((a div gcd a b)^n * (gcd a b)^n) 
1340 
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" 

60162  1341 
by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral) 
31706  1342 
also have "(a div gcd a b)^n * (gcd a b)^n = a^n" 
60162  1343 
by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib) 
31706  1344 
also have "(b div gcd a b)^n * (gcd a b)^n = b^n" 
60162
