author  haftmann 
Wed, 08 Jul 2015 14:01:40 +0200  
changeset 60687  33dbbcb6a8a3 
parent 60686  ea5bc46c11e6 
child 60688  01488b559910 
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]: 

60687  402 
"Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q") 
60686  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) 

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

60686  412 
qed 
413 
next 

414 
assume ?Q 

415 
have "0 dvd Gcd A" 

416 
proof (rule Gcd_greatest) 

417 
fix a 

418 
assume "a \<in> A" 

60687  419 
with \<open>?Q\<close> have "a = 0" by auto 
60686  420 
then show "0 dvd a" by simp 
421 
qed 

422 
then show ?P by simp 

423 
qed 

424 

425 
lemma unit_factor_Gcd: 

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

427 
proof (cases "Gcd A = 0") 

60687  428 
case True then show ?thesis by auto 
60686  429 
next 
430 
case False 

431 
from unit_factor_mult_normalize 

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

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

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

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

60687  436 
with False show ?thesis by auto 
60686  437 
qed 
438 

439 
lemma Gcd_UNIV [simp]: 

440 
"Gcd UNIV = 1" 

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

442 

443 
lemma Gcd_eq_1_I: 

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

445 
shows "Gcd A = 1" 

446 
proof  

447 
from assms have "is_unit (Gcd A)" 

448 
by (blast intro: Gcd_dvd dvd_unit_imp_unit) 

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

450 
by (rule is_unit_normalize) 

451 
then show ?thesis 

452 
by simp 

453 
qed 

454 

455 
lemma Gcd_insert [simp]: 

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

457 
proof  

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

459 
by (auto intro: Gcd_dvd Gcd_greatest) 

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

461 
proof (rule Gcd_greatest) 

462 
fix b 

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

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

465 
proof 

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

467 
next 

468 
assume "b \<in> A" 

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

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

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

472 
qed 

473 
qed 

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

475 
by (rule associatedI) 

476 
then show ?thesis 

60687  477 
by (rule associated_eqI) (auto simp add: unit_factor_gcd unit_factor_Gcd) 
60686  478 
qed 
479 

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

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

482 
by (blast intro: Gcd_greatest) 

483 

484 
lemma Gcd_set [code_unfold]: 

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

486 
by (induct as) simp_all 

487 

488 
end 

489 

490 
class semiring_Lcm = semiring_Gcd + 

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

492 
begin 

493 

494 
lemma dvd_Lcm: 

495 
assumes "a \<in> A" 

496 
shows "a dvd Lcm A" 

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

498 

499 
lemma Gcd_image_normalize [simp]: 

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

501 
proof  

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

503 
proof  

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

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

506 
by (rule gcd_dvd1) 

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

508 
by simp 

509 
qed 

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

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

512 
then show ?thesis 

60687  513 
by (rule associated_eqI) (simp_all add: unit_factor_Gcd, auto dest!: bspec) 
60686  514 
qed 
515 

516 
lemma Lcm_least: 

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

518 
shows "Lcm A dvd a" 

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

520 

521 
lemma normalize_Lcm [simp]: 

522 
"normalize (Lcm A) = Lcm A" 

523 
by (simp add: Lcm_Gcd) 

524 

525 
lemma unit_factor_Lcm: 

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

527 
proof (cases "Lcm A = 0") 

528 
case True then show ?thesis by simp 

529 
next 

530 
case False 

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

532 
by blast 

533 
with False show ?thesis 

534 
by simp 

535 
qed 

536 

537 
lemma Lcm_empty [simp]: 

538 
"Lcm {} = 1" 

539 
by (simp add: Lcm_Gcd) 

540 

541 
lemma Lcm_1_iff [simp]: 

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

543 
proof 

544 
assume ?P 

545 
show ?Q 

546 
proof 

547 
fix a 

548 
assume "a \<in> A" 

549 
then have "a dvd Lcm A" 

550 
by (rule dvd_Lcm) 

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

552 
by simp 

553 
qed 

554 
next 

555 
assume ?Q 

556 
then have "is_unit (Lcm A)" 

557 
by (blast intro: Lcm_least) 

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

559 
by (rule is_unit_normalize) 

560 
then show ?P 

561 
by simp 

562 
qed 

563 

564 
lemma Lcm_UNIV [simp]: 

565 
"Lcm UNIV = 0" 

566 
proof  

567 
have "0 dvd Lcm UNIV" 

568 
by (rule dvd_Lcm) simp 

569 
then show ?thesis 

570 
by simp 

571 
qed 

572 

573 
lemma Lcm_eq_0_I: 

574 
assumes "0 \<in> A" 

575 
shows "Lcm A = 0" 

576 
proof  

577 
from assms have "0 dvd Lcm A" 

578 
by (rule dvd_Lcm) 

579 
then show ?thesis 

580 
by simp 

581 
qed 

582 

583 
lemma Gcd_Lcm: 

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

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

586 
simp add: unit_factor_Gcd unit_factor_Lcm) 

587 

588 
lemma Lcm_insert [simp]: 

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

590 
proof (rule sym) 

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

592 
by (auto intro: dvd_Lcm Lcm_least) 

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

594 
proof (rule Lcm_least) 

595 
fix b 

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

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

598 
proof 

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

600 
next 

601 
assume "b \<in> A" 

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

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

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

605 
qed 

606 
qed 

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

608 
by (rule associatedI) 

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

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

611 
qed 

612 

613 
lemma Lcm_set [code_unfold]: 

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

615 
by (induct as) simp_all 

616 

617 
end 

59008  618 

619 
class ring_gcd = comm_ring_1 + semiring_gcd 

620 

31706  621 
instantiation nat :: gcd 
622 
begin 

21256  623 

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

626 
where 

627 
"gcd_nat x y = 

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

629 

630 
definition 

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

632 
where 

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

634 

635 
instance proof qed 

636 

637 
end 

638 

639 
instantiation int :: gcd 

640 
begin 

21256  641 

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

644 
where 

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

646 

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

649 
where 

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

651 

31706  652 
instance proof qed 
653 

654 
end 

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

655 

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

656 

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

657 
subsection {* Transfer setup *} 
31706  658 

659 
lemma transfer_nat_int_gcd: 

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

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

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

664 

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

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

668 
by (auto simp add: gcd_int_def lcm_int_def) 

669 

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

673 
lemma transfer_int_nat_gcd: 

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

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

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

678 
lemma transfer_int_nat_gcd_closures: 

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

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

681 
by (auto simp add: gcd_int_def lcm_int_def) 

682 

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

686 

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

687 
subsection {* GCD properties *} 
31706  688 

689 
(* was gcd_induct *) 

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

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

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

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

693 
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

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

697 
using assms apply simp_all 

698 
done 

699 

700 
(* specific to int *) 

701 

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

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

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

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

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

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

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

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

711 

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

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

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

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

715 

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

718 

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

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

722 
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

723 
by (metis abs_idempotent gcd_abs_int) 
31813  724 

725 
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

726 
by (metis abs_idempotent gcd_abs_int) 
31706  727 

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

728 
lemma gcd_cases_int: 
31706  729 
fixes x :: int and y 
730 
assumes "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 
and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (x) (y))" 

734 
shows "P (gcd x y)" 

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

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

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

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

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

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

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

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

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

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

751 

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

753 
by (metis abs_idempotent lcm_int_def) 

754 

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

756 
by (metis abs_idempotent lcm_int_def) 

757 

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

758 
lemma lcm_cases_int: 
31706  759 
fixes x :: int and y 
760 
assumes "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 
and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (x) (y))" 

764 
shows "P (lcm x y)" 

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

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

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

770 
(* was gcd_0, etc. *) 

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

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

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

773 

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

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

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

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

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

780 

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

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

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

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

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

788 

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

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

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

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

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

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

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

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

800 

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

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

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

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

807 
declare gcd_nat.simps [simp del] 

21256  808 

809 
text {* 

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

813 

59008  814 
instance nat :: semiring_gcd 
815 
proof 

816 
fix m n :: nat 

817 
show "gcd m n dvd m" and "gcd m n dvd n" 

818 
proof (induct m n rule: gcd_nat_induct) 

819 
fix m n :: nat 

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

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

822 
by (rule dvd_mod_imp_dvd) 

823 
moreover assume "0 < n" 

824 
ultimately show "gcd m n dvd m" 

825 
by (simp add: gcd_non_0_nat) 

826 
qed (simp_all add: gcd_0_nat gcd_non_0_nat) 

827 
next 

828 
fix m n k :: nat 

829 
assume "k dvd m" and "k dvd n" 

830 
then show "k dvd gcd m n" 

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

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

833 

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

837 

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

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

59008  842 
by (metis gcd_dvd2 dvd_trans) 
31730  843 

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

59008  845 
by (metis gcd_dvd1 dvd_trans) 
31730  846 

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

59008  848 
by (metis gcd_dvd2 dvd_trans) 
31730  849 

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

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

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

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

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

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

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

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

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

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

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

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

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

869 
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

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

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

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

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

875 
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

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

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

878 
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

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

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

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

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

21256  888 

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

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

893 
apply (rule iffI) 

894 
apply (rule zdvd_antisym_nonneg) 

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

897 

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

898 
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

899 
+ 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  900 
apply standard 
901 
apply (auto intro: dvd_antisym dvd_trans)[2] 

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

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

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

904 

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

906 

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

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

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

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

912 
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

913 

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

914 
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

915 

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

916 
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

917 

31798  918 
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

919 
by (fact gcd_nat.absorb1) 
31798  920 

921 
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

922 
by (fact gcd_nat.absorb2) 
31798  923 

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

924 
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

925 
by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int) 
31798  926 

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

927 
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

928 
by (metis gcd_proj1_if_dvd_int gcd_commute_int) 
31798  929 

21256  930 
text {* 
931 
\medskip Multiplication laws 

932 
*} 

933 

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

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

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

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

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

942 
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

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

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

21256  948 

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

949 
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

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

953 
apply simp 

954 
done 

955 

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

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

959 
apply (subst dvd_abs_iff [symmetric]) 

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

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

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

964 
apply (subst abs_mult [symmetric], auto) 

31706  965 
done 
966 

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

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

969 
by (auto intro: coprime_dvd_mult_nat) 
31706  970 

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

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

973 
by (auto intro: coprime_dvd_mult_int) 
31706  974 

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

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

978 
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

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

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

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

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

984 
lemma gcd_mult_cancel_int: 
31813  985 
"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

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

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

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

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

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

995 
proof 

996 
assume ?rhs then show ?lhs by simp 

997 
next 

998 
assume ?lhs 

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

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

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

1002 
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

1003 
from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult.commute) 
35368  1004 
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

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

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

1009 
ultimately show ?rhs .. 

1010 
qed 

1011 

1012 
lemma coprime_crossproduct_int: 

1013 
fixes a b c d :: int 

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

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

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

1017 

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

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

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

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

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

1025 
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

1026 
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

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

1030 

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

1032 

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

1033 
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

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

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

1036 
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

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

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

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

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

1043 
apply (rule gcd_commute_nat) 
31706  1044 
done 
1045 

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

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

1049 
apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] 
31706  1050 
zmod_zminus1_eq_if) 
1051 
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

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

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

21256  1056 

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

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

1060 
apply (case_tac "y > 0") 

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

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

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

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

1066 
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

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

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

1069 
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

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

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

1072 
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

1073 
by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat) 
21256  1074 

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

1075 
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

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

21256  1078 

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

1081 

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

1083 
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

1084 
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

1085 

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

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

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

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

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

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

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

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

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

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

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

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

1111 

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

1113 
apply(rule antisym) 

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

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

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

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

1120 
apply(rule Max_eqI[THEN sym]) 

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

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

1126 

1127 
lemma gcd_is_Max_divisors_int: 

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

1129 
apply(rule Max_eqI[THEN sym]) 

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

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

1135 

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

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

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

1138 
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

1139 

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

1140 

31706  1141 
subsection {* Coprimality *} 
1142 

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

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

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

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

1149 
let ?b' = "b div ?g" 
27556  1150 
let ?g' = "gcd ?a' ?b'" 
22027
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 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

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

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

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

1160 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

35216  1161 
have "?g \<noteq> 0" using nz by simp 
31706  1162 
then have gp: "?g > 0" by arith 
59008  1163 
from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . 
22367  1164 
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

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

1166 

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

1167 
lemma div_gcd_coprime_int: 
31706  1168 
assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0" 
1169 
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

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

1173 
apply simp 

1174 
apply(subst (1 2) abs_gcd_int) 

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

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

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

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

1179 
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

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

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

1182 
lemma coprime_Suc_0_nat: 
31706  1183 
"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

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

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

1186 
lemma coprime_int: "coprime (a::int) b \<longleftrightarrow> 
31706  1187 
(\<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

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

1191 
apply (rule iffI) 

1192 
apply force 

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

31706  1195 
apply force 
1196 
apply force 

59807  1197 
done 
31706  1198 

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

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

1202 
shows "coprime a' b'" 

1203 

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

1205 
apply (erule ssubst) 

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

1207 
apply (erule ssubst) 

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

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

1212 
apply (subst (1) a) 

1213 
using z apply force 

41550  1214 
done 
31706  1215 

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

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

1219 
shows "coprime a' b'" 

1220 

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

1222 
apply (erule ssubst) 

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

1224 
apply (erule ssubst) 

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

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

1229 
apply (subst (1) a) 

1230 
using z apply force 

41550  1231 
done 
31706  1232 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1256 
qed 

1257 

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

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

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

1266 

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

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

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

1275 

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

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

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

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

1283 
qed 

1284 

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

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

1287 
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

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

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

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

1293 
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

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

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

1299 
using assms 

1300 
proof (induct n) 

1301 
case (Suc n) then show ?case 

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

1303 
qed simp 

1304 

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

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

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

1309 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1336 
thus ?thesis by simp 

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

1338 
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

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

60162  1342 
by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral) 
31706  1343 
also have "(a div gcd a b)^n * (gcd a b)^n = a^n" 
60162  1344 
by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib) 
31706  1345 
also have "(b div gcd a b)^n * (gcd a b)^n = b^n" 
60162  1346 
by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib) 
31706  1347 
finally show ?thesis . 
1348 
qed 
