author  Andreas Lochbihler 
Fri, 18 Dec 2015 11:14:28 +0100  
changeset 61856  4b1b85f38944 
parent 61799  4cf66f21b764 
child 61913  58b153bfa737 
permissions  rwrr 
32479  1 
(* Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, 
31798  2 
Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow 
31706  3 

4 

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

31706  7 

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

9 

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

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

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

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

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

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

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

34915  19 
the natural numbers by Chaieb. 
31706  20 

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

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

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

23 

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

31706  27 

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

30 
theory GCD 

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

31 
imports Main 
31706  32 
begin 
33 

60758  34 
subsection \<open>GCD and LCM definitions\<close> 
31706  35 

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

21256  39 
begin 
40 

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

31706  43 

44 
end 

45 

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

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

49 

50 
class semiring_gcd = normalization_semidom + gcd + 

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

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

56 
begin 

57 

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

61 

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

64 
by (rule dvd_trans) (rule gcd_dvd1) 

65 

66 
lemma gcd_dvdI2: 

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

68 
by (rule dvd_trans) (rule gcd_dvd2) 

69 

60686  70 
lemma gcd_0_left [simp]: 
71 
"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

72 
by (rule associated_eqI) simp_all 
60686  73 

74 
lemma gcd_0_right [simp]: 

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

76 
by (rule associated_eqI) simp_all 
60686  77 

78 
lemma gcd_eq_0_iff [simp]: 

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

80 
proof 

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

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

83 
then show ?Q by simp 

84 
next 

85 
assume ?Q then show ?P by simp 

86 
qed 

87 

88 
lemma unit_factor_gcd: 

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

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

91 
case True then show ?thesis by simp 

92 
next 

93 
case False 

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

95 
by (rule unit_factor_mult_normalize) 

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

97 
by simp 

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

99 
by simp 

100 
with False show ?thesis by simp 

101 
qed 

102 

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

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

106 

61605  107 
sublocale gcd: abel_semigroup gcd 
60686  108 
proof 
109 
fix a b c 

110 
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

111 
by (rule associated_eqI) simp_all 
60686  112 
from gcd_dvd1 have "gcd (gcd a b) c dvd a" 
113 
by (rule dvd_trans) simp 

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

115 
by (rule dvd_trans) simp 

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

117 
by (auto intro!: gcd_greatest) 

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

119 
by (rule dvd_trans) simp 

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

121 
by (rule dvd_trans) simp 

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

123 
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

124 
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

125 
by (rule associated_eqI) simp_all 
60686  126 
qed 
127 

128 
lemma gcd_self [simp]: 

129 
"gcd a a = normalize a" 

130 
proof  

131 
have "a dvd gcd a a" 

132 
by (rule gcd_greatest) simp_all 

133 
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

134 
by (auto intro: associated_eqI) 
60686  135 
qed 
136 

137 
lemma coprime_1_left [simp]: 

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

139 
by (rule associated_eqI) simp_all 
60686  140 

141 
lemma coprime_1_right [simp]: 

142 
"coprime a 1" 

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

144 

145 
lemma gcd_mult_left: 

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

147 
proof (cases "c = 0") 

148 
case True then show ?thesis by simp 

149 
next 

150 
case False 

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

152 
by (auto intro: gcd_greatest) 

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

154 
by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute) 

155 
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

156 
by (auto intro: associated_eqI) 
60686  157 
then show ?thesis by (simp add: normalize_mult) 
158 
qed 

159 

160 
lemma gcd_mult_right: 

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

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

163 

164 
lemma mult_gcd_left: 

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

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

167 

168 
lemma mult_gcd_right: 

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

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

171 

60689  172 
lemma dvd_lcm1 [iff]: 
60686  173 
"a dvd lcm a b" 
174 
proof  

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

176 
by (simp add: lcm_gcd normalize_mult div_mult_swap) 

177 
then show ?thesis 

178 
by (simp add: lcm_gcd) 

179 
qed 

180 

60689  181 
lemma dvd_lcm2 [iff]: 
60686  182 
"b dvd lcm a b" 
183 
proof  

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

185 
by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps) 

186 
then show ?thesis 

187 
by (simp add: lcm_gcd) 

188 
qed 

189 

60689  190 
lemma dvd_lcmI1: 
191 
"a dvd b \<Longrightarrow> a dvd lcm b c" 

192 
by (rule dvd_trans) (assumption, blast) 

193 

194 
lemma dvd_lcmI2: 

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

196 
by (rule dvd_trans) (assumption, blast) 

197 

60686  198 
lemma lcm_least: 
199 
assumes "a dvd c" and "b dvd c" 

200 
shows "lcm a b dvd c" 

201 
proof (cases "c = 0") 

202 
case True then show ?thesis by simp 

203 
next 

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

205 
show ?thesis 

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

207 
case True with assms show ?thesis by simp 

208 
next 

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

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

211 
by (simp_all add: mult_dvd_mono) 

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

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

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

215 
using U by (simp add: dvd_mult_unit_iff) 

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

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

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

219 
using False by (simp add: div_dvd_iff_mult ac_simps) 

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

221 
qed 

222 
qed 

223 

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

227 

228 
lemma normalize_lcm [simp]: 

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

230 
by (simp add: lcm_gcd dvd_normalize_div) 

231 

232 
lemma lcm_0_left [simp]: 

233 
"lcm 0 a = 0" 

234 
by (simp add: lcm_gcd) 

235 

236 
lemma lcm_0_right [simp]: 

237 
"lcm a 0 = 0" 

238 
by (simp add: lcm_gcd) 

239 

240 
lemma lcm_eq_0_iff: 

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

242 
proof 

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

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

245 
by (simp add: lcm_gcd) 

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

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

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

249 
by simp 

250 
then show ?Q by simp 

251 
next 

252 
assume ?Q then show ?P by auto 

253 
qed 

254 

255 
lemma unit_factor_lcm : 

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

257 
by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd) 

258 

61605  259 
sublocale lcm: abel_semigroup lcm 
60686  260 
proof 
261 
fix a b c 

262 
show "lcm a b = lcm b a" 

263 
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

264 
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

265 
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

266 
by (auto intro: lcm_least 
60686  267 
dvd_trans [of b "lcm b c" "lcm a (lcm b c)"] 
268 
dvd_trans [of c "lcm b c" "lcm a (lcm b c)"] 

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

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

271 
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

272 
by (rule associated_eqI) simp_all 
60686  273 
qed 
274 

275 
lemma lcm_self [simp]: 

276 
"lcm a a = normalize a" 

277 
proof  

278 
have "lcm a a dvd a" 

279 
by (rule lcm_least) simp_all 

280 
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

281 
by (auto intro: associated_eqI) 
60686  282 
qed 
283 

284 
lemma gcd_mult_lcm [simp]: 

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

286 
by (simp add: lcm_gcd normalize_mult) 

287 

288 
lemma lcm_mult_gcd [simp]: 

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

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

291 

292 
lemma gcd_lcm: 

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

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

295 
proof  

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

297 
by (simp add: lcm_eq_0_iff) 

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

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

300 
by (simp_all add: normalize_mult) 

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

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

303 
qed 

304 

305 
lemma lcm_1_left [simp]: 

306 
"lcm 1 a = normalize a" 

307 
by (simp add: lcm_gcd) 

308 

309 
lemma lcm_1_right [simp]: 

310 
"lcm a 1 = normalize a" 

311 
by (simp add: lcm_gcd) 

312 

313 
lemma lcm_mult_left: 

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

315 
by (cases "c = 0") 

316 
(simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps, 

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

318 

319 
lemma lcm_mult_right: 

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

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

322 

323 
lemma mult_lcm_left: 

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

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

326 

327 
lemma mult_lcm_right: 

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

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

330 

331 
end 

332 

333 
class semiring_Gcd = semiring_gcd + Gcd + 

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

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

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

337 
begin 

338 

339 
lemma Gcd_empty [simp]: 

340 
"Gcd {} = 0" 

341 
by (rule dvd_0_left, rule Gcd_greatest) simp 

342 

343 
lemma Gcd_0_iff [simp]: 

60687  344 
"Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q") 
60686  345 
proof 
346 
assume ?P 

347 
show ?Q 

348 
proof 

349 
fix a 

350 
assume "a \<in> A" 

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

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

60686  354 
qed 
355 
next 

356 
assume ?Q 

357 
have "0 dvd Gcd A" 

358 
proof (rule Gcd_greatest) 

359 
fix a 

360 
assume "a \<in> A" 

60687  361 
with \<open>?Q\<close> have "a = 0" by auto 
60686  362 
then show "0 dvd a" by simp 
363 
qed 

364 
then show ?P by simp 

365 
qed 

366 

367 
lemma unit_factor_Gcd: 

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

369 
proof (cases "Gcd A = 0") 

60687  370 
case True then show ?thesis by auto 
60686  371 
next 
372 
case False 

373 
from unit_factor_mult_normalize 

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

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

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

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

60687  378 
with False show ?thesis by auto 
60686  379 
qed 
380 

381 
lemma Gcd_UNIV [simp]: 

382 
"Gcd UNIV = 1" 

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

384 

385 
lemma Gcd_eq_1_I: 

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

387 
shows "Gcd A = 1" 

388 
proof  

389 
from assms have "is_unit (Gcd A)" 

390 
by (blast intro: Gcd_dvd dvd_unit_imp_unit) 

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

392 
by (rule is_unit_normalize) 

393 
then show ?thesis 

394 
by simp 

395 
qed 

396 

397 
lemma Gcd_insert [simp]: 

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

399 
proof  

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

401 
by (auto intro: Gcd_dvd Gcd_greatest) 

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

403 
proof (rule Gcd_greatest) 

404 
fix b 

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

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

407 
proof 

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

409 
next 

410 
assume "b \<in> A" 

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

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

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

414 
qed 

415 
qed 

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

416 
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

417 
by (auto intro: associated_eqI) 
60686  418 
qed 
419 

61799  420 
lemma dvd_Gcd: \<comment> \<open>FIXME remove\<close> 
60686  421 
"\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A" 
422 
by (blast intro: Gcd_greatest) 

423 

424 
lemma Gcd_set [code_unfold]: 

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

426 
by (induct as) simp_all 

427 

428 
end 

429 

430 
class semiring_Lcm = semiring_Gcd + 

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

432 
begin 

433 

434 
lemma dvd_Lcm: 

435 
assumes "a \<in> A" 

436 
shows "a dvd Lcm A" 

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

438 

439 
lemma Gcd_image_normalize [simp]: 

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

441 
proof  

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

443 
proof  

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

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

446 
by (rule gcd_dvd1) 

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

448 
by simp 

449 
qed 

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

450 
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

451 
by (auto intro!: Gcd_greatest intro: Gcd_dvd) 
60686  452 
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

453 
by (auto intro: associated_eqI) 
60686  454 
qed 
455 

456 
lemma Lcm_least: 

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

458 
shows "Lcm A dvd a" 

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

460 

461 
lemma normalize_Lcm [simp]: 

462 
"normalize (Lcm A) = Lcm A" 

463 
by (simp add: Lcm_Gcd) 

464 

465 
lemma unit_factor_Lcm: 

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

467 
proof (cases "Lcm A = 0") 

468 
case True then show ?thesis by simp 

469 
next 

470 
case False 

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

472 
by blast 

473 
with False show ?thesis 

474 
by simp 

475 
qed 

476 

477 
lemma Lcm_empty [simp]: 

478 
"Lcm {} = 1" 

479 
by (simp add: Lcm_Gcd) 

480 

481 
lemma Lcm_1_iff [simp]: 

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

483 
proof 

484 
assume ?P 

485 
show ?Q 

486 
proof 

487 
fix a 

488 
assume "a \<in> A" 

489 
then have "a dvd Lcm A" 

490 
by (rule dvd_Lcm) 

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

492 
by simp 

493 
qed 

494 
next 

495 
assume ?Q 

496 
then have "is_unit (Lcm A)" 

497 
by (blast intro: Lcm_least) 

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

499 
by (rule is_unit_normalize) 

500 
then show ?P 

501 
by simp 

502 
qed 

503 

504 
lemma Lcm_UNIV [simp]: 

505 
"Lcm UNIV = 0" 

506 
proof  

507 
have "0 dvd Lcm UNIV" 

508 
by (rule dvd_Lcm) simp 

509 
then show ?thesis 

510 
by simp 

511 
qed 

512 

513 
lemma Lcm_eq_0_I: 

514 
assumes "0 \<in> A" 

515 
shows "Lcm A = 0" 

516 
proof  

517 
from assms have "0 dvd Lcm A" 

518 
by (rule dvd_Lcm) 

519 
then show ?thesis 

520 
by simp 

521 
qed 

522 

523 
lemma Gcd_Lcm: 

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

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

526 
simp add: unit_factor_Gcd unit_factor_Lcm) 

527 

528 
lemma Lcm_insert [simp]: 

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

530 
proof (rule sym) 

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

532 
by (auto intro: dvd_Lcm Lcm_least) 

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

534 
proof (rule Lcm_least) 

535 
fix b 

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

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

538 
proof 

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

540 
next 

541 
assume "b \<in> A" 

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

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

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

545 
qed 

546 
qed 

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

547 
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

548 
by (rule associated_eqI) (simp_all add: lcm_eq_0_iff) 
60686  549 
qed 
550 

551 
lemma Lcm_set [code_unfold]: 

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

553 
by (induct as) simp_all 

554 

555 
end 

59008  556 

557 
class ring_gcd = comm_ring_1 + semiring_gcd 

558 

31706  559 
instantiation nat :: gcd 
560 
begin 

21256  561 

31706  562 
fun 
563 
gcd_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

564 
where 

565 
"gcd_nat x y = 

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

567 

568 
definition 

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

570 
where 

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

572 

573 
instance proof qed 

574 

575 
end 

576 

577 
instantiation int :: gcd 

578 
begin 

21256  579 

31706  580 
definition 
581 
gcd_int :: "int \<Rightarrow> int \<Rightarrow> int" 

582 
where 

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

584 

31706  585 
definition 
586 
lcm_int :: "int \<Rightarrow> int \<Rightarrow> int" 

587 
where 

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

589 

31706  590 
instance proof qed 
591 

592 
end 

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

593 

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

594 

60758  595 
subsection \<open>Transfer setup\<close> 
31706  596 

597 
lemma transfer_nat_int_gcd: 

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

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

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

602 

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

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

606 
by (auto simp add: gcd_int_def lcm_int_def) 

607 

35644  608 
declare transfer_morphism_nat_int[transfer add return: 
31706  609 
transfer_nat_int_gcd transfer_nat_int_gcd_closures] 
610 

611 
lemma transfer_int_nat_gcd: 

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

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

32479  614 
by (unfold gcd_int_def lcm_int_def, auto) 
31706  615 

616 
lemma transfer_int_nat_gcd_closures: 

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

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

619 
by (auto simp add: gcd_int_def lcm_int_def) 

620 

35644  621 
declare transfer_morphism_int_nat[transfer add return: 
31706  622 
transfer_int_nat_gcd transfer_int_nat_gcd_closures] 
623 

624 

60758  625 
subsection \<open>GCD properties\<close> 
31706  626 

627 
(* was gcd_induct *) 

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

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

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

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

631 
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

632 
shows "P m n" 
31706  633 
apply (rule gcd_nat.induct) 
634 
apply (case_tac "y = 0") 

635 
using assms apply simp_all 

636 
done 

637 

638 
(* specific to int *) 

639 

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

640 
lemma gcd_neg1_int [simp]: "gcd (x::int) y = gcd x y" 
31706  641 
by (simp add: gcd_int_def) 
642 

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

643 
lemma gcd_neg2_int [simp]: "gcd (x::int) (y) = gcd x y" 
31706  644 
by (simp add: gcd_int_def) 
645 

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

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

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

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

649 

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

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

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

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

653 

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

656 

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

657 
lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)" 
31813  658 
by (simp add: gcd_int_def) 
659 

660 
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

661 
by (metis abs_idempotent gcd_abs_int) 
31813  662 

663 
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

664 
by (metis abs_idempotent gcd_abs_int) 
31706  665 

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

666 
lemma gcd_cases_int: 
31706  667 
fixes x :: int and y 
668 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)" 

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

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

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

672 
shows "P (gcd x y)" 

35216  673 
by (insert assms, auto, arith) 
21256  674 

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

675 
lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0" 
31706  676 
by (simp add: gcd_int_def) 
677 

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

678 
lemma lcm_neg1_int: "lcm (x::int) y = lcm x y" 
31706  679 
by (simp add: lcm_int_def) 
680 

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

681 
lemma lcm_neg2_int: "lcm (x::int) (y) = lcm x y" 
31706  682 
by (simp add: lcm_int_def) 
683 

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

684 
lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)" 
31706  685 
by (simp add: lcm_int_def) 
21256  686 

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

689 

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

691 
by (metis abs_idempotent lcm_int_def) 

692 

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

694 
by (metis abs_idempotent lcm_int_def) 

695 

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

696 
lemma lcm_cases_int: 
31706  697 
fixes x :: int and y 
698 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)" 

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

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

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

702 
shows "P (lcm x y)" 

41550  703 
using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith 
31706  704 

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

705 
lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0" 
31706  706 
by (simp add: lcm_int_def) 
707 

708 
(* was gcd_0, etc. *) 

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

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

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

711 

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

713 
lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x" 
31706  714 
by (unfold gcd_int_def, auto) 
715 

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

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

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

718 

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

719 
lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x" 
31706  720 
by (unfold gcd_int_def, auto) 
721 

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

722 
lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)" 
31706  723 
by (case_tac "y = 0", auto) 
724 

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

726 

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

727 
lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)" 
31706  728 
by simp 
729 

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

730 
lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1" 
21263  731 
by simp 
21256  732 

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

733 
lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" 
60690  734 
by simp 
31706  735 

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

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

738 

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

739 
lemma gcd_idem_nat: "gcd (x::nat) x = x" 
31798  740 
by simp 
31706  741 

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

742 
lemma gcd_idem_int: "gcd (x::int) x = abs x" 
31813  743 
by (auto simp add: gcd_int_def) 
31706  744 

745 
declare gcd_nat.simps [simp del] 

21256  746 

60758  747 
text \<open> 
61799  748 
\medskip @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>. The 
21256  749 
conjunctions don't seem provable separately. 
60758  750 
\<close> 
21256  751 

59008  752 
instance nat :: semiring_gcd 
753 
proof 

754 
fix m n :: nat 

755 
show "gcd m n dvd m" and "gcd m n dvd n" 

756 
proof (induct m n rule: gcd_nat_induct) 

757 
fix m n :: nat 

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

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

760 
by (rule dvd_mod_imp_dvd) 

761 
moreover assume "0 < n" 

762 
ultimately show "gcd m n dvd m" 

763 
by (simp add: gcd_non_0_nat) 

764 
qed (simp_all add: gcd_0_nat gcd_non_0_nat) 

765 
next 

766 
fix m n k :: nat 

767 
assume "k dvd m" and "k dvd n" 

768 
then show "k dvd gcd m n" 

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

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

771 

59008  772 
instance int :: ring_gcd 
60686  773 
by standard 
774 
(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

775 

31730  776 
lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m" 
59008  777 
by (metis gcd_dvd1 dvd_trans) 
31730  778 

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

59008  780 
by (metis gcd_dvd2 dvd_trans) 
31730  781 

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

59008  783 
by (metis gcd_dvd1 dvd_trans) 
31730  784 

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

59008  786 
by (metis gcd_dvd2 dvd_trans) 
31730  787 

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

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

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

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

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

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

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

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

60689  800 
lemma gcd_greatest_iff_nat: 
801 
"(k dvd gcd (m::nat) n) = (k dvd m & k dvd n)" 

802 
by (fact gcd_greatest_iff) 

803 

804 
lemma gcd_greatest_iff_int: 

805 
"((k::int) dvd gcd m n) = (k dvd m & k dvd n)" 

806 
by (fact gcd_greatest_iff) 

31706  807 

60689  808 
lemma gcd_zero_nat: 
809 
"(gcd (m::nat) n = 0) = (m = 0 & n = 0)" 

810 
by (fact gcd_eq_0_iff) 

21256  811 

60689  812 
lemma gcd_zero_int [simp]: 
813 
"(gcd (m::int) n = 0) = (m = 0 & n = 0)" 

814 
by (fact gcd_eq_0_iff) 

21256  815 

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

816 
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

817 
by (insert gcd_zero_nat [of m n], arith) 
21256  818 

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

819 
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

820 
by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith) 
31706  821 

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

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

33657  825 
apply (rule dvd_antisym) 
59008  826 
apply (erule (1) gcd_greatest) 
31706  827 
apply auto 
828 
done 

21256  829 

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

830 
lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and> 
31706  831 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 
33657  832 
apply (case_tac "d = 0") 
833 
apply simp 

834 
apply (rule iffI) 

835 
apply (rule zdvd_antisym_nonneg) 

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

838 

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

839 
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

840 
+ 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  841 
apply standard 
842 
apply (auto intro: dvd_antisym dvd_trans)[2] 

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

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

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

845 

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

847 

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

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

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

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

853 
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

854 

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

855 
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

856 

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

857 
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

858 

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

860 
by (fact gcd_nat.absorb1) 
31798  861 

862 
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

863 
by (fact gcd_nat.absorb2) 
31798  864 

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

865 
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

866 
by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int) 
31798  867 

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

868 
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

869 
by (metis gcd_proj1_if_dvd_int gcd_commute_int) 
31798  870 

60758  871 
text \<open> 
21256  872 
\medskip Multiplication laws 
60758  873 
\<close> 
21256  874 

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

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

877 
apply (induct m n rule: gcd_nat_induct) 
31706  878 
apply simp 
21256  879 
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

880 
apply (simp_all add: gcd_non_0_nat) 
31706  881 
done 
21256  882 

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

883 
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

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

886 
apply (rule gcd_mult_distrib_nat [transferred]) 
31706  887 
apply auto 
888 
done 

21256  889 

60690  890 
context semiring_gcd 
891 
begin 

21256  892 

60690  893 
lemma coprime_dvd_mult: 
894 
assumes "coprime a b" and "a dvd c * b" 

895 
shows "a dvd c" 

896 
proof (cases "c = 0") 

897 
case True then show ?thesis by simp 

898 
next 

899 
case False 

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

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

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

903 
by (simp add: ac_simps) 

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

905 
by (simp add: dvd_mult_unit_iff unit) 

906 
ultimately show ?thesis by simp 

907 
qed 

908 

909 
end 

910 

911 
lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat] 

912 
lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int] 

31706  913 

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

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

916 
by (auto intro: coprime_dvd_mult_nat) 
31706  917 

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

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

920 
by (auto intro: coprime_dvd_mult_int) 
31706  921 

60690  922 
context semiring_gcd 
923 
begin 

924 

925 
lemma gcd_mult_cancel: 

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

927 
apply (rule associated_eqI) 

59008  928 
apply (rule gcd_greatest) 
60690  929 
apply (rule_tac b = c in coprime_dvd_mult) 
930 
apply (simp add: gcd.assoc) 

931 
apply (simp_all add: ac_simps) 

932 
done 

21256  933 

60690  934 
end 
935 

936 
lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat] 

937 
lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int] 

21256  938 

35368  939 
lemma coprime_crossproduct_nat: 
940 
fixes a b c d :: nat 

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

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

943 
proof 

944 
assume ?rhs then show ?lhs by simp 

945 
next 

946 
assume ?lhs 

60758  947 
from \<open>?lhs\<close> have "a dvd b * d" by (auto intro: dvdI dest: sym) 
948 
with \<open>coprime a d\<close> have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat) 

949 
from \<open>?lhs\<close> have "b dvd a * c" by (auto intro: dvdI dest: sym) 

950 
with \<open>coprime b c\<close> have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat) 

951 
from \<open>?lhs\<close> have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult.commute) 

952 
with \<open>coprime b c\<close> have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat) 

953 
from \<open>?lhs\<close> have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult.commute) 

954 
with \<open>coprime a d\<close> have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat) 

955 
from \<open>a dvd b\<close> \<open>b dvd a\<close> have "a = b" by (rule Nat.dvd.antisym) 

956 
moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "c = d" by (rule Nat.dvd.antisym) 

35368  957 
ultimately show ?rhs .. 
958 
qed 

959 

960 
lemma coprime_crossproduct_int: 

961 
fixes a b c d :: int 

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

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

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

965 

60758  966 
text \<open>\medskip Addition laws\<close> 
21256  967 

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

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

970 
apply (simp_all add: gcd_non_0_nat) 
31706  971 
done 
972 

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

973 
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

974 
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

975 
apply (subst add.commute) 
31706  976 
apply simp 
977 
done 

978 

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

980 

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

981 
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

982 
by (subst gcd_add1_nat [symmetric], auto) 
31706  983 

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

984 
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

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

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

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

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

991 
apply (rule gcd_commute_nat) 
31706  992 
done 
993 

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

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

997 
apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] 
31706  998 
zmod_zminus1_eq_if) 
999 
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

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

1001 
apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat 
31706  1002 
nat_le_eq_zle) 
1003 
done 

21256  1004 

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

1005 
lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)" 
31706  1006 
apply (case_tac "y = 0") 
1007 
apply force 

1008 
apply (case_tac "y > 0") 

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

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

1010 
apply (insert gcd_non_0_int [of "y" "x"]) 
35216  1011 
apply auto 
31706  1012 
done 
1013 

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

1014 
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

1015 
by (metis gcd_red_int mod_add_self1 add.commute) 
31706  1016 

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

1017 
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

1018 
by (metis gcd_add1_int gcd_commute_int add.commute) 
21256  1019 

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

1020 
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

1021 
by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat) 
21256  1022 

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

1023 
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

1024 
by (metis gcd_commute_int gcd_red_int mod_mult_self1 add.commute) 
31798  1025 

21256  1026 

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

1029 

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

1031 
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

1032 

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

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

31734  1037 
proof 
60512  1038 
have "finite{d. d <= m}" 
1039 
by (blast intro: bounded_nat_set_is_finite) 

31734  1040 
from finite_subset[OF _ this] show ?thesis using assms 
60512  1041 
by (metis Collect_mono dvd_imp_le neq0_conv) 
31734  1042 
qed 
1043 

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

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

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

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

60512  1050 
by (simp add: dvd_imp_le_int subset_iff) 
31734  1051 
qed 
1052 

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

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

1055 
apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le) 
31995  1056 
apply simp 
1057 
done 

1058 

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

1060 
apply(rule antisym) 

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

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

1062 
apply (auto intro: abs_le_D1 dvd_imp_le_int) 
31995  1063 
done 
1064 

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

1067 
apply(rule Max_eqI[THEN sym]) 

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

1070 
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat) 
31734  1071 
apply simp 
1072 
done 

1073 

1074 
lemma gcd_is_Max_divisors_int: 

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

1076 
apply(rule Max_eqI[THEN sym]) 

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

1079 
apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le) 
31734  1080 
apply simp 
1081 
done 

1082 

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

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

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

1085 
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

1086 

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

1087 

60758  1088 
subsection \<open>Coprimality\<close> 
31706  1089 

60690  1090 
context semiring_gcd 
1091 
begin 

1092 

1093 
lemma div_gcd_coprime: 

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

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

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

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

1101 
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

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

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

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

1110 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

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

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

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

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

1116 

60690  1117 
end 
1118 

1119 
lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat] 

1120 
lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int] 

31706  1121 

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

1122 
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

1123 
using gcd_unique_nat[of 1 a b, simplified] by auto 
31706  1124 

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

1125 
lemma coprime_Suc_0_nat: 
31706  1126 
"coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)" 
60690  1127 
using coprime_nat by simp 
31706  1128 

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

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

1131 
using gcd_unique_int [of 1 a b] 
31706  1132 
apply clarsimp 
1133 
apply (erule subst) 

1134 
apply (rule iffI) 

1135 
apply force 

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

1136 
using abs_dvd_iff abs_ge_zero apply blast 
59807  1137 
done 
31706  1138 

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

1139 
lemma gcd_coprime_nat: 
31706  1140 
assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and 
1141 
b: "b = b' * gcd a b" 

1142 
shows "coprime a' b'" 

1143 

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

1145 
apply (erule ssubst) 

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

1147 
apply (erule ssubst) 

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

1148 
apply (rule div_gcd_coprime_nat) 
41550  1149 
using z apply force 
31706  1150 
apply (subst (1) b) 
1151 
using z apply force 

1152 
apply (subst (1) a) 

1153 
using z apply force 

41550  1154 
done 
31706  1155 

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

1156 
lemma gcd_coprime_int: 
31706  1157 
assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and 
1158 
b: "b = b' * gcd a b" 

1159 
shows "coprime a' b'" 

1160 

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

1162 
apply (erule ssubst) 

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

1164 
apply (erule ssubst) 

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

1165 
apply (rule div_gcd_coprime_int) 
41550  1166 
using z apply force 
31706  1167 
apply (subst (1) b) 
1168 
using z apply force 

1169 
apply (subst (1) a) 

1170 
using z apply force 

41550  1171 
done 
31706  1172 

60690  1173 
context semiring_gcd 
1174 
begin 

31706  1175 

60690  1176 
lemma coprime_mult: 
1177 
assumes da: "coprime d a" and db: "coprime d b" 

1178 
shows "coprime d (a * b)" 

1179 
apply (subst gcd.commute) 

1180 
using da apply (subst gcd_mult_cancel) 

1181 
apply (subst gcd.commute, assumption) 

1182 
apply (subst gcd.commute, rule db) 

1183 
done 

31706  1184 

60690  1185 
end 
1186 

1187 
lemmas coprime_mult_nat = coprime_mult [where ?'a = nat] 

1188 
lemmas coprime_mult_int = coprime_mult [where ?'a = int] 

1189 

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

1190 
lemma coprime_lmult_nat: 
31706  1191 
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" 
1192 
proof  

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

59008  1194 
by (rule gcd_greatest, auto) 
31706  1195 
with dab show ?thesis 
1196 
by auto 

1197 
qed 

1198 

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

1199 
lemma coprime_lmult_int: 
31798  1200 
assumes "coprime (d::int) (a * b)" shows "coprime d a" 
31706  1201 
proof  
1202 
have "gcd d a dvd gcd d (a * b)" 

59008  1203 
by (rule gcd_greatest, auto) 
31798  1204 
with assms show ?thesis 
31706  1205 
by auto 
1206 
qed 

1207 

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

1208 
lemma coprime_rmult_nat: 
31798  1209 
assumes "coprime (d::nat) (a * b)" shows "coprime d b" 
31706  1210 
proof  
1211 
have "gcd d b dvd gcd d (a * b)" 

59008  1212 
by (rule gcd_greatest, auto intro: dvd_mult) 
31798  1213 
with assms show ?thesis 
31706  1214 
by auto 
1215 
qed 

1216 

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

1217 
lemma coprime_rmult_int: 
31706  1218 
assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" 
1219 
proof  

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

59008  1221 
by (rule gcd_greatest, auto intro: dvd_mult) 
31706  1222 
with dab show ?thesis 
1223 
by auto 

1224 
qed 

1225 

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

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

1228 
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

1229 
coprime_mult_nat[of d a b] 
31706  1230 
by blast 
1231 

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

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

1234 
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

1235 
coprime_mult_int[of d a b] 
31706  1236 
by blast 
1237 

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

1240 
using assms 

1241 
proof (induct n) 

1242 
case (Suc n) then show ?case 

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

1244 
qed simp 

1245 

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

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

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

1250 
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

1251 
using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult) 
31706  1252 
done 
1253 

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

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

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

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

59008  1259 
using nz apply (auto simp add: div_gcd_coprime_int) 
31706  1260 
done 
1261 

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

1262 
lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)" 
60596  1263 
by (induct n) (simp_all add: coprime_mult_nat) 
31706  1264 

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

1265 
lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)" 
60596  1266 
by (induct n) (simp_all add: coprime_mult_int) 
31706  1267 

60690  1268 
context semiring_gcd 
1269 
begin 

1270 

1271 
lemma coprime_exp_left: 

1272 
assumes "coprime a b" 

1273 
shows "coprime (a ^ n) b" 

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

1275 

1276 
lemma coprime_exp2: 

1277 
assumes "coprime a b" 

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

1279 
proof (rule coprime_exp_left) 

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

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

1282 
qed 

1283 

1284 
end 

1285 

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

1286 
lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)" 
60690  1287 
by (fact coprime_exp2) 
31706  1288 

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

1289 
lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)" 
60690  1290 
by (fact coprime_exp2) 
31706  1291 

60690  1292 
lemma gcd_exp_nat: 
1293 
"gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n" 

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

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

1296 
next 

1297 
case False 

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

1299 
by (auto simp: div_gcd_coprime) 

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

1301 
by (simp add: coprime_exp2) 

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

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

1311 

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

1312 
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

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

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

1318 

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

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

1322 
let ?g = "gcd a b" 

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

1324 
moreover 

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

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

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

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

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

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

1332 
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

1333 
hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc) 
31706  1334 
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

1335 
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

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

1339 
ultimately show ?thesis by blast 

1340 
qed 

1341 

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

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

1345 
let ?g = "gcd a b" 

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