author  haftmann 
Wed, 08 Jul 2015 14:01:41 +0200  
changeset 60688  01488b559910 
parent 60687  33dbbcb6a8a3 
child 60689  8a2d7c04d8c0 
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 

31706  77 
declare One_nat_def [simp del] 
78 

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

79 
subsection {* GCD and LCM definitions *} 
31706  80 

31992  81 
class gcd = zero + one + dvd + 
41550  82 
fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
83 
and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 

21256  84 
begin 
85 

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

31706  88 

89 
end 

90 

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

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

94 

95 
class semiring_gcd = normalization_semidom + gcd + 

59008  96 
assumes gcd_dvd1 [iff]: "gcd a b dvd a" 
59977  97 
and gcd_dvd2 [iff]: "gcd a b dvd b" 
98 
and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" 

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

101 
begin 

102 

103 
lemma gcd_greatest_iff [iff]: 

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

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

106 

107 
lemma gcd_0_left [simp]: 

108 
"gcd 0 a = normalize a" 

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

109 
by (rule associated_eqI) simp_all 
60686  110 

111 
lemma gcd_0_right [simp]: 

112 
"gcd a 0 = normalize a" 

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

113 
by (rule associated_eqI) simp_all 
60686  114 

115 
lemma gcd_eq_0_iff [simp]: 

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

117 
proof 

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

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

120 
then show ?Q by simp 

121 
next 

122 
assume ?Q then show ?P by simp 

123 
qed 

124 

125 
lemma unit_factor_gcd: 

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

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

128 
case True then show ?thesis by simp 

129 
next 

130 
case False 

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

132 
by (rule unit_factor_mult_normalize) 

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

134 
by simp 

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

136 
by simp 

137 
with False show ?thesis by simp 

138 
qed 

139 

140 
sublocale gcd!: abel_semigroup gcd 

141 
proof 

142 
fix a b c 

143 
show "gcd a b = gcd b a" 

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

144 
by (rule associated_eqI) simp_all 
60686  145 
from gcd_dvd1 have "gcd (gcd a b) c dvd a" 
146 
by (rule dvd_trans) simp 

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

148 
by (rule dvd_trans) simp 

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

150 
by (auto intro!: gcd_greatest) 

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

152 
by (rule dvd_trans) simp 

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

154 
by (rule dvd_trans) simp 

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

156 
by (auto intro!: gcd_greatest) 

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

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

158 
by (rule associated_eqI) simp_all 
60686  159 
qed 
160 

161 
lemma gcd_self [simp]: 

162 
"gcd a a = normalize a" 

163 
proof  

164 
have "a dvd gcd a a" 

165 
by (rule gcd_greatest) simp_all 

166 
then show ?thesis 

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

167 
by (auto intro: associated_eqI) 
60686  168 
qed 
169 

170 
lemma coprime_1_left [simp]: 

171 
"coprime 1 a" 

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

172 
by (rule associated_eqI) simp_all 
60686  173 

174 
lemma coprime_1_right [simp]: 

175 
"coprime a 1" 

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

177 

178 
lemma gcd_mult_left: 

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

180 
proof (cases "c = 0") 

181 
case True then show ?thesis by simp 

182 
next 

183 
case False 

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

185 
by (auto intro: gcd_greatest) 

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

187 
by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute) 

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

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

189 
by (auto intro: associated_eqI) 
60686  190 
then show ?thesis by (simp add: normalize_mult) 
191 
qed 

192 

193 
lemma gcd_mult_right: 

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

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

196 

197 
lemma mult_gcd_left: 

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

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

200 

201 
lemma mult_gcd_right: 

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

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

204 

205 
lemma lcm_dvd1 [iff]: 

206 
"a dvd lcm a b" 

207 
proof  

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

209 
by (simp add: lcm_gcd normalize_mult div_mult_swap) 

210 
then show ?thesis 

211 
by (simp add: lcm_gcd) 

212 
qed 

213 

214 
lemma lcm_dvd2 [iff]: 

215 
"b dvd lcm a b" 

216 
proof  

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

218 
by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps) 

219 
then show ?thesis 

220 
by (simp add: lcm_gcd) 

221 
qed 

222 

223 
lemma lcm_least: 

224 
assumes "a dvd c" and "b dvd c" 

225 
shows "lcm a b dvd c" 

226 
proof (cases "c = 0") 

227 
case True then show ?thesis by simp 

228 
next 

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

230 
show ?thesis 

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

232 
case True with assms show ?thesis by simp 

233 
next 

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

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

236 
by (simp_all add: mult_dvd_mono) 

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

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

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

240 
using U by (simp add: dvd_mult_unit_iff) 

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

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

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

244 
using False by (simp add: div_dvd_iff_mult ac_simps) 

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

246 
qed 

247 
qed 

248 

249 
lemma lcm_least_iff [iff]: 

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

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

252 

253 
lemma normalize_lcm [simp]: 

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

255 
by (simp add: lcm_gcd dvd_normalize_div) 

256 

257 
lemma lcm_0_left [simp]: 

258 
"lcm 0 a = 0" 

259 
by (simp add: lcm_gcd) 

260 

261 
lemma lcm_0_right [simp]: 

262 
"lcm a 0 = 0" 

263 
by (simp add: lcm_gcd) 

264 

265 
lemma lcm_eq_0_iff: 

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

267 
proof 

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

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

270 
by (simp add: lcm_gcd) 

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

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

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

274 
by simp 

275 
then show ?Q by simp 

276 
next 

277 
assume ?Q then show ?P by auto 

278 
qed 

279 

280 
lemma unit_factor_lcm : 

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

282 
by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd) 

283 

284 
sublocale lcm!: abel_semigroup lcm 

285 
proof 

286 
fix a b c 

287 
show "lcm a b = lcm b a" 

288 
by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div) 

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

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

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

291 
by (auto intro: lcm_least 
60686  292 
dvd_trans [of b "lcm b c" "lcm a (lcm b c)"] 
293 
dvd_trans [of c "lcm b c" "lcm a (lcm b c)"] 

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

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

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

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

297 
by (rule associated_eqI) simp_all 
60686  298 
qed 
299 

300 
lemma lcm_self [simp]: 

301 
"lcm a a = normalize a" 

302 
proof  

303 
have "lcm a a dvd a" 

304 
by (rule lcm_least) simp_all 

305 
then show ?thesis 

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

306 
by (auto intro: associated_eqI) 
60686  307 
qed 
308 

309 
lemma gcd_mult_lcm [simp]: 

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

311 
by (simp add: lcm_gcd normalize_mult) 

312 

313 
lemma lcm_mult_gcd [simp]: 

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

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

316 

317 
lemma gcd_lcm: 

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

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

320 
proof  

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

322 
by (simp add: lcm_eq_0_iff) 

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

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

325 
by (simp_all add: normalize_mult) 

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

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

328 
qed 

329 

330 
lemma lcm_1_left [simp]: 

331 
"lcm 1 a = normalize a" 

332 
by (simp add: lcm_gcd) 

333 

334 
lemma lcm_1_right [simp]: 

335 
"lcm a 1 = normalize a" 

336 
by (simp add: lcm_gcd) 

337 

338 
lemma lcm_mult_left: 

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

340 
by (cases "c = 0") 

341 
(simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps, 

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

343 

344 
lemma lcm_mult_right: 

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

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

347 

348 
lemma mult_lcm_left: 

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

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

351 

352 
lemma mult_lcm_right: 

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

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

355 

356 
end 

357 

358 
class semiring_Gcd = semiring_gcd + Gcd + 

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

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

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

362 
begin 

363 

364 
lemma Gcd_empty [simp]: 

365 
"Gcd {} = 0" 

366 
by (rule dvd_0_left, rule Gcd_greatest) simp 

367 

368 
lemma Gcd_0_iff [simp]: 

60687  369 
"Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q") 
60686  370 
proof 
371 
assume ?P 

372 
show ?Q 

373 
proof 

374 
fix a 

375 
assume "a \<in> A" 

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

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

60686  379 
qed 
380 
next 

381 
assume ?Q 

382 
have "0 dvd Gcd A" 

383 
proof (rule Gcd_greatest) 

384 
fix a 

385 
assume "a \<in> A" 

60687  386 
with \<open>?Q\<close> have "a = 0" by auto 
60686  387 
then show "0 dvd a" by simp 
388 
qed 

389 
then show ?P by simp 

390 
qed 

391 

392 
lemma unit_factor_Gcd: 

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

394 
proof (cases "Gcd A = 0") 

60687  395 
case True then show ?thesis by auto 
60686  396 
next 
397 
case False 

398 
from unit_factor_mult_normalize 

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

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

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

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

60687  403 
with False show ?thesis by auto 
60686  404 
qed 
405 

406 
lemma Gcd_UNIV [simp]: 

407 
"Gcd UNIV = 1" 

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

409 

410 
lemma Gcd_eq_1_I: 

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

412 
shows "Gcd A = 1" 

413 
proof  

414 
from assms have "is_unit (Gcd A)" 

415 
by (blast intro: Gcd_dvd dvd_unit_imp_unit) 

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

417 
by (rule is_unit_normalize) 

418 
then show ?thesis 

419 
by simp 

420 
qed 

421 

422 
lemma Gcd_insert [simp]: 

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

424 
proof  

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

426 
by (auto intro: Gcd_dvd Gcd_greatest) 

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

428 
proof (rule Gcd_greatest) 

429 
fix b 

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

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

432 
proof 

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

434 
next 

435 
assume "b \<in> A" 

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

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

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

439 
qed 

440 
qed 

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

441 
ultimately show ?thesis 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

442 
by (auto intro: associated_eqI) 
60686  443 
qed 
444 

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

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

447 
by (blast intro: Gcd_greatest) 

448 

449 
lemma Gcd_set [code_unfold]: 

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

451 
by (induct as) simp_all 

452 

453 
end 

454 

455 
class semiring_Lcm = semiring_Gcd + 

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

457 
begin 

458 

459 
lemma dvd_Lcm: 

460 
assumes "a \<in> A" 

461 
shows "a dvd Lcm A" 

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

463 

464 
lemma Gcd_image_normalize [simp]: 

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

466 
proof  

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

468 
proof  

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

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

471 
by (rule gcd_dvd1) 

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

473 
by simp 

474 
qed 

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

475 
then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

476 
by (auto intro!: Gcd_greatest intro: Gcd_dvd) 
60686  477 
then show ?thesis 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

478 
by (auto intro: associated_eqI) 
60686  479 
qed 
480 

481 
lemma Lcm_least: 

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

483 
shows "Lcm A dvd a" 

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

485 

486 
lemma normalize_Lcm [simp]: 

487 
"normalize (Lcm A) = Lcm A" 

488 
by (simp add: Lcm_Gcd) 

489 

490 
lemma unit_factor_Lcm: 

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

492 
proof (cases "Lcm A = 0") 

493 
case True then show ?thesis by simp 

494 
next 

495 
case False 

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

497 
by blast 

498 
with False show ?thesis 

499 
by simp 

500 
qed 

501 

502 
lemma Lcm_empty [simp]: 

503 
"Lcm {} = 1" 

504 
by (simp add: Lcm_Gcd) 

505 

506 
lemma Lcm_1_iff [simp]: 

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

508 
proof 

509 
assume ?P 

510 
show ?Q 

511 
proof 

512 
fix a 

513 
assume "a \<in> A" 

514 
then have "a dvd Lcm A" 

515 
by (rule dvd_Lcm) 

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

517 
by simp 

518 
qed 

519 
next 

520 
assume ?Q 

521 
then have "is_unit (Lcm A)" 

522 
by (blast intro: Lcm_least) 

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

524 
by (rule is_unit_normalize) 

525 
then show ?P 

526 
by simp 

527 
qed 

528 

529 
lemma Lcm_UNIV [simp]: 

530 
"Lcm UNIV = 0" 

531 
proof  

532 
have "0 dvd Lcm UNIV" 

533 
by (rule dvd_Lcm) simp 

534 
then show ?thesis 

535 
by simp 

536 
qed 

537 

538 
lemma Lcm_eq_0_I: 

539 
assumes "0 \<in> A" 

540 
shows "Lcm A = 0" 

541 
proof  

542 
from assms have "0 dvd Lcm A" 

543 
by (rule dvd_Lcm) 

544 
then show ?thesis 

545 
by simp 

546 
qed 

547 

548 
lemma Gcd_Lcm: 

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

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

551 
simp add: unit_factor_Gcd unit_factor_Lcm) 

552 

553 
lemma Lcm_insert [simp]: 

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

555 
proof (rule sym) 

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

557 
by (auto intro: dvd_Lcm Lcm_least) 

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

559 
proof (rule Lcm_least) 

560 
fix b 

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

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

563 
proof 

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

565 
next 

566 
assume "b \<in> A" 

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

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

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

570 
qed 

571 
qed 

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

572 
ultimately show "lcm a (Lcm A) = Lcm (insert a A)" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

573 
by (rule associated_eqI) (simp_all add: lcm_eq_0_iff) 
60686  574 
qed 
575 

576 
lemma Lcm_set [code_unfold]: 

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

578 
by (induct as) simp_all 

579 

580 
end 

59008  581 

582 
class ring_gcd = comm_ring_1 + semiring_gcd 

583 

31706  584 
instantiation nat :: gcd 
585 
begin 

21256  586 

31706  587 
fun 
588 
gcd_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

589 
where 

590 
"gcd_nat x y = 

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

592 

593 
definition 

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

595 
where 

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

597 

598 
instance proof qed 

599 

600 
end 

601 

602 
instantiation int :: gcd 

603 
begin 

21256  604 

31706  605 
definition 
606 
gcd_int :: "int \<Rightarrow> int \<Rightarrow> int" 

607 
where 

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

609 

31706  610 
definition 
611 
lcm_int :: "int \<Rightarrow> int \<Rightarrow> int" 

612 
where 

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

614 

31706  615 
instance proof qed 
616 

617 
end 

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

618 

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

619 

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

620 
subsection {* Transfer setup *} 
31706  621 

622 
lemma transfer_nat_int_gcd: 

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

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

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

627 

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

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

631 
by (auto simp add: gcd_int_def lcm_int_def) 

632 

35644  633 
declare transfer_morphism_nat_int[transfer add return: 
31706  634 
transfer_nat_int_gcd transfer_nat_int_gcd_closures] 
635 

636 
lemma transfer_int_nat_gcd: 

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

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

32479  639 
by (unfold gcd_int_def lcm_int_def, auto) 
31706  640 

641 
lemma transfer_int_nat_gcd_closures: 

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

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

644 
by (auto simp add: gcd_int_def lcm_int_def) 

645 

35644  646 
declare transfer_morphism_int_nat[transfer add return: 
31706  647 
transfer_int_nat_gcd transfer_int_nat_gcd_closures] 
648 

649 

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

650 
subsection {* GCD properties *} 
31706  651 

652 
(* was gcd_induct *) 

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

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

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

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

656 
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

657 
shows "P m n" 
31706  658 
apply (rule gcd_nat.induct) 
659 
apply (case_tac "y = 0") 

660 
using assms apply simp_all 

661 
done 

662 

663 
(* specific to int *) 

664 

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

665 
lemma gcd_neg1_int [simp]: "gcd (x::int) y = gcd x y" 
31706  666 
by (simp add: gcd_int_def) 
667 

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

668 
lemma gcd_neg2_int [simp]: "gcd (x::int) (y) = gcd x y" 
31706  669 
by (simp add: gcd_int_def) 
670 

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

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

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

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

674 

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

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

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

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

678 

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

681 

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

682 
lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)" 
31813  683 
by (simp add: gcd_int_def) 
684 

685 
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

686 
by (metis abs_idempotent gcd_abs_int) 
31813  687 

688 
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

689 
by (metis abs_idempotent gcd_abs_int) 
31706  690 

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

691 
lemma gcd_cases_int: 
31706  692 
fixes x :: int and y 
693 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)" 

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

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

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

697 
shows "P (gcd x y)" 

35216  698 
by (insert assms, auto, arith) 
21256  699 

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

700 
lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0" 
31706  701 
by (simp add: gcd_int_def) 
702 

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

703 
lemma lcm_neg1_int: "lcm (x::int) y = lcm x y" 
31706  704 
by (simp add: lcm_int_def) 
705 

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

706 
lemma lcm_neg2_int: "lcm (x::int) (y) = lcm x y" 
31706  707 
by (simp add: lcm_int_def) 
708 

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

709 
lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)" 
31706  710 
by (simp add: lcm_int_def) 
21256  711 

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

714 

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

716 
by (metis abs_idempotent lcm_int_def) 

717 

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

719 
by (metis abs_idempotent lcm_int_def) 

720 

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

721 
lemma lcm_cases_int: 
31706  722 
fixes x :: int and y 
723 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)" 

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

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

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

727 
shows "P (lcm x y)" 

41550  728 
using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith 
31706  729 

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

730 
lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0" 
31706  731 
by (simp add: lcm_int_def) 
732 

733 
(* was gcd_0, etc. *) 

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

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

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

736 

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

738 
lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x" 
31706  739 
by (unfold gcd_int_def, auto) 
740 

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

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

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

743 

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

744 
lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x" 
31706  745 
by (unfold gcd_int_def, auto) 
746 

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

747 
lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)" 
31706  748 
by (case_tac "y = 0", auto) 
749 

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

751 

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

752 
lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)" 
31706  753 
by simp 
754 

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

755 
lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1" 
21263  756 
by simp 
21256  757 

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

758 
lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" 
31706  759 
by (simp add: One_nat_def) 
760 

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

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

763 

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

764 
lemma gcd_idem_nat: "gcd (x::nat) x = x" 
31798  765 
by simp 
31706  766 

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

767 
lemma gcd_idem_int: "gcd (x::int) x = abs x" 
31813  768 
by (auto simp add: gcd_int_def) 
31706  769 

770 
declare gcd_nat.simps [simp del] 

21256  771 

772 
text {* 

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

776 

59008  777 
instance nat :: semiring_gcd 
778 
proof 

779 
fix m n :: nat 

780 
show "gcd m n dvd m" and "gcd m n dvd n" 

781 
proof (induct m n rule: gcd_nat_induct) 

782 
fix m n :: nat 

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

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

785 
by (rule dvd_mod_imp_dvd) 

786 
moreover assume "0 < n" 

787 
ultimately show "gcd m n dvd m" 

788 
by (simp add: gcd_non_0_nat) 

789 
qed (simp_all add: gcd_0_nat gcd_non_0_nat) 

790 
next 

791 
fix m n k :: nat 

792 
assume "k dvd m" and "k dvd n" 

793 
then show "k dvd gcd m n" 

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

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

796 

59008  797 
instance int :: ring_gcd 
60686  798 
by standard 
799 
(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

800 

31730  801 
lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m" 
59008  802 
by (metis gcd_dvd1 dvd_trans) 
31730  803 

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

59008  805 
by (metis gcd_dvd2 dvd_trans) 
31730  806 

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

59008  808 
by (metis gcd_dvd1 dvd_trans) 
31730  809 

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

59008  811 
by (metis gcd_dvd2 dvd_trans) 
31730  812 

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

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

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

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

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

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

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

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

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

825 
lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) = 
31706  826 
(k dvd m & k dvd n)" 
59008  827 
by (blast intro!: gcd_greatest intro: dvd_trans) 
31706  828 

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

829 
lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)" 
59008  830 
by (blast intro!: gcd_greatest intro: dvd_trans) 
21256  831 

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

832 
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

833 
by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat) 
21256  834 

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

835 
lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)" 
31706  836 
by (auto simp add: gcd_int_def) 
21256  837 

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

838 
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

839 
by (insert gcd_zero_nat [of m n], arith) 
21256  840 

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

841 
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

842 
by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith) 
31706  843 

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

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

33657  847 
apply (rule dvd_antisym) 
59008  848 
apply (erule (1) gcd_greatest) 
31706  849 
apply auto 
850 
done 

21256  851 

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

852 
lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and> 
31706  853 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 
33657  854 
apply (case_tac "d = 0") 
855 
apply simp 

856 
apply (rule iffI) 

857 
apply (rule zdvd_antisym_nonneg) 

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

860 

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

861 
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

862 
+ 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  863 
apply standard 
864 
apply (auto intro: dvd_antisym dvd_trans)[2] 

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

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

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

867 

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

869 

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

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

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

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

875 
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

876 

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

877 
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

878 

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

879 
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

880 

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

882 
by (fact gcd_nat.absorb1) 
31798  883 

884 
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

885 
by (fact gcd_nat.absorb2) 
31798  886 

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

887 
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

888 
by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int) 
31798  889 

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

890 
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

891 
by (metis gcd_proj1_if_dvd_int gcd_commute_int) 
31798  892 

21256  893 
text {* 
894 
\medskip Multiplication laws 

895 
*} 

896 

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

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

899 
apply (induct m n rule: gcd_nat_induct) 
31706  900 
apply simp 
21256  901 
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

902 
apply (simp_all add: gcd_non_0_nat) 
31706  903 
done 
21256  904 

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

905 
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

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

908 
apply (rule gcd_mult_distrib_nat [transferred]) 
31706  909 
apply auto 
910 
done 

21256  911 

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

912 
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

913 
apply (insert gcd_mult_distrib_nat [of m k n]) 
21256  914 
apply simp 
915 
apply (erule_tac t = m in ssubst) 

916 
apply simp 

917 
done 

918 

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

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

922 
apply (subst dvd_abs_iff [symmetric]) 

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

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

924 
apply (rule coprime_dvd_mult_nat [transferred]) 
31813  925 
prefer 4 apply assumption 
926 
apply auto 

927 
apply (subst abs_mult [symmetric], auto) 

31706  928 
done 
929 

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

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

932 
by (auto intro: coprime_dvd_mult_nat) 
31706  933 

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

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

936 
by (auto intro: coprime_dvd_mult_int) 
31706  937 

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

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

941 
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

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

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

944 
apply (simp_all add: mult.commute) 
31706  945 
done 
21256  946 

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

947 
lemma gcd_mult_cancel_int: 
31813  948 
"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

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

951 
apply (rule gcd_mult_cancel_nat [transferred], auto) 
31706  952 
done 
21256  953 

35368  954 
lemma coprime_crossproduct_nat: 
955 
fixes a b c d :: nat 

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

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

958 
proof 

959 
assume ?rhs then show ?lhs by simp 

960 
next 

961 
assume ?lhs 

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

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

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

965 
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

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

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

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

972 
ultimately show ?rhs .. 

973 
qed 

974 

975 
lemma coprime_crossproduct_int: 

976 
fixes a b c d :: int 

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

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

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

980 

21256  981 
text {* \medskip Addition laws *} 
982 

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

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

985 
apply (simp_all add: gcd_non_0_nat) 
31706  986 
done 
987 

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

988 
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

989 
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

990 
apply (subst add.commute) 
31706  991 
apply simp 
992 
done 

993 

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

995 

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

996 
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

997 
by (subst gcd_add1_nat [symmetric], auto) 
31706  998 

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

999 
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

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

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

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

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

1006 
apply (rule gcd_commute_nat) 
31706  1007 
done 
1008 

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

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

1012 
apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] 
31706  1013 
zmod_zminus1_eq_if) 
1014 
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

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

1016 
apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat 
31706  1017 
nat_le_eq_zle) 
1018 
done 

21256  1019 

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

1020 
lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)" 
31706  1021 
apply (case_tac "y = 0") 
1022 
apply force 

1023 
apply (case_tac "y > 0") 

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

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

1025 
apply (insert gcd_non_0_int [of "y" "x"]) 
35216  1026 
apply auto 
31706  1027 
done 
1028 

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

1029 
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

1030 
by (metis gcd_red_int mod_add_self1 add.commute) 
31706  1031 

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

1032 
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

1033 
by (metis gcd_add1_int gcd_commute_int add.commute) 
21256  1034 

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

1035 
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

1036 
by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat) 
21256  1037 

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

1038 
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

1039 
by (metis gcd_commute_int gcd_red_int mod_mult_self1 add.commute) 
31798  1040 

21256  1041 

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

1044 

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

1046 
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

1047 
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

1048 

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

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

31734  1053 
proof 
60512  1054 
have "finite{d. d <= m}" 
1055 
by (blast intro: bounded_nat_set_is_finite) 

31734  1056 
from finite_subset[OF _ this] show ?thesis using assms 
60512  1057 
by (metis Collect_mono dvd_imp_le neq0_conv) 
31734  1058 
qed 
1059 

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

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

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

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

60512  1066 
by (simp add: dvd_imp_le_int subset_iff) 
31734  1067 
qed 
1068 

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

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

1071 
apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le) 
31995  1072 
apply simp 
1073 
done 

1074 

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

1076 
apply(rule antisym) 

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

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

1078 
apply (auto intro: abs_le_D1 dvd_imp_le_int) 
31995  1079 
done 
1080 

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

1083 
apply(rule Max_eqI[THEN sym]) 

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

1086 
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat) 
31734  1087 
apply simp 
1088 
done 

1089 

1090 
lemma gcd_is_Max_divisors_int: 

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

1092 
apply(rule Max_eqI[THEN sym]) 

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

1095 
apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le) 
31734  1096 
apply simp 
1097 
done 

1098 

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

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

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

1101 
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

1102 

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

1103 

31706  1104 
subsection {* Coprimality *} 
1105 

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

1106 
lemma div_gcd_coprime_nat: 
31706  1107 
assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0" 
1108 
shows "coprime (a div gcd a b) (b div gcd a b)" 

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

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

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

1114 
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

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

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

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

1123 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

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

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

1129 

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

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

1133 
apply (subst (1 2 3) gcd_abs_int) 
31813  1134 
apply (subst (1 2) abs_div) 
1135 
apply simp 

1136 
apply simp 

1137 
apply(subst (1 2) abs_gcd_int) 

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

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

1139 
using nz apply (auto simp add: gcd_abs_int [symmetric]) 
31706  1140 
done 
1141 

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

1142 
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

1143 
using gcd_unique_nat[of 1 a b, simplified] by auto 
31706  1144 

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

1145 
lemma coprime_Suc_0_nat: 
31706  1146 
"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

1147 
using coprime_nat by (simp add: One_nat_def) 
31706  1148 

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

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

1151 
using gcd_unique_int [of 1 a b] 
31706  1152 
apply clarsimp 
1153 
apply (erule subst) 

1154 
apply (rule iffI) 

1155 
apply force 

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

31706  1158 
apply force 
1159 
apply force 

59807  1160 
done 
31706  1161 

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

1162 
lemma gcd_coprime_nat: 
31706  1163 
assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and 
1164 
b: "b = b' * gcd a b" 

1165 
shows "coprime a' b'" 

1166 

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

1168 
apply (erule ssubst) 

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

1170 
apply (erule ssubst) 

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

1171 
apply (rule div_gcd_coprime_nat) 
41550  1172 
using z apply force 
31706  1173 
apply (subst (1) b) 
1174 
using z apply force 

1175 
apply (subst (1) a) 

1176 
using z apply force 

41550  1177 
done 
31706  1178 

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

1179 
lemma gcd_coprime_int: 
31706  1180 
assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and 
1181 
b: "b = b' * gcd a b" 

1182 
shows "coprime a' b'" 

1183 

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

1185 
apply (erule ssubst) 

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

1187 
apply (erule ssubst) 

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

1188 
apply (rule div_gcd_coprime_int) 
41550  1189 
using z apply force 
31706  1190 
apply (subst (1) b) 
1191 
using z apply force 

1192 
apply (subst (1) a) 

1193 
using z apply force 

41550  1194 
done 
31706  1195 

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

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

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

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

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

1201 
apply (subst gcd_commute_nat, rule db) 
31706  1202 
done 
1203 

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

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

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

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

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

1209 
apply (subst gcd_commute_int, rule db) 
31706  1210 
done 
1211 

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

1212 
lemma coprime_lmult_nat: 
31706  1213 
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" 
1214 
proof  

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

59008  1216 
by (rule gcd_greatest, auto) 
31706  1217 
with dab show ?thesis 
1218 
by auto 

1219 
qed 

1220 

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

1221 
lemma coprime_lmult_int: 
31798  1222 
assumes "coprime (d::int) (a * b)" shows "coprime d a" 
31706  1223 
proof  
1224 
have "gcd d a dvd gcd d (a * b)" 

59008  1225 
by (rule gcd_greatest, auto) 
31798  1226 
with assms show ?thesis 
31706  1227 
by auto 
1228 
qed 

1229 

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

1230 
lemma coprime_rmult_nat: 
31798  1231 
assumes "coprime (d::nat) (a * b)" shows "coprime d b" 
31706  1232 
proof  
1233 
have "gcd d b dvd gcd d (a * b)" 

59008  1234 
by (rule gcd_greatest, auto intro: dvd_mult) 
31798  1235 
with assms show ?thesis 
31706  1236 
by auto 
1237 
qed 

1238 

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

1239 
lemma coprime_rmult_int: 
31706  1240 
assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" 
1241 
proof  

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

59008  1243 
by (rule gcd_greatest, auto intro: dvd_mult) 
31706  1244 
with dab show ?thesis 
1245 
by auto 

1246 
qed 

1247 

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

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

1250 
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

1251 
coprime_mult_nat[of d a b] 
31706  1252 
by blast 
1253 

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

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

1256 
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

1257 
coprime_mult_int[of d a b] 
31706  1258 
by blast 
1259 

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

1262 
using assms 

1263 
proof (induct n) 

1264 
case (Suc n) then show ?case 

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

1266 
qed simp 

1267 

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

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

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

1272 
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

1273 
using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult) 
31706  1274 
done 
1275 

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

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

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

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

59008  1281 
using nz apply (auto simp add: div_gcd_coprime_int) 
31706  1282 
done 
1283 

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

1284 
lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)" 
60596  1285 
by (induct n) (simp_all add: coprime_mult_nat) 
31706  1286 

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

1287 
lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)" 
60596  1288 
by (induct n) (simp_all add: coprime_mult_int) 
31706  1289 

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

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

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

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

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

1296 
lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n" 
31706  1297 
proof (cases) 
1298 
assume "a = 0 & b = 0" 

1299 
thus ?thesis by simp 

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

1301 
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

1302 
by (auto simp:div_gcd_coprime_nat) 
31706  1303 
hence "gcd ((a div gcd a b)^n * (gcd a b)^n) 
1304 
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" 

60162  1305 
by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral) 
31706  1306 
also have "(a div gcd a b)^n * (gcd a b)^n = a^n" 
60162  1307 
by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib) 
31706  1308 
also have "(b div gcd a b)^n * (gcd a b)^n = b^n" 
60162  1309 
by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib) 
31706  1310 
finally show ?thesis . 
1311 
qed 

1312 

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

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

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

1316 
apply (rule gcd_exp_nat [where n = n, transferred]) 
31706  1317 
apply auto 
1318 
done 

1319 

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

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

1323 
let ?g = "gcd a b" 

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

1325 
moreover 

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

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

1327 
from gcd_coprime_exists_nat[OF z] 
31706  1328 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
1329 
by blast 

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

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

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

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

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

1334 
hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc) 
31706  1335 
with z have th_1: "a' dvd b' * c" by auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

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

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

1340 
ultimately show ?thesis by blast 

1341 
qed 

1342 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
