author  wenzelm 
Wed, 25 May 2016 11:49:40 +0200  
changeset 63145  703edebd1d92 
parent 63025  92680537201f 
child 63359  99b51ba8da1c 
permissions  rwrr 
32479  1 
(* Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, 
31798  2 
Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow 
31706  3 

4 

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

31706  7 

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

9 

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

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

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

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

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

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

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

34915  19 
the natural numbers by Chaieb. 
31706  20 

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

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

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

23 

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

31706  27 

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

30 
theory GCD 

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

31 
imports Main 
31706  32 
begin 
33 

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

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

21256  39 
begin 
40 

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

31706  43 

44 
end 

45 

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

62350  49 
begin 
50 

63025  51 
abbreviation GREATEST_COMMON_DIVISOR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" 
62350  52 
where 
63025  53 
"GREATEST_COMMON_DIVISOR A f \<equiv> Gcd (f ` A)" 
62350  54 

63025  55 
abbreviation LEAST_COMMON_MULTIPLE :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" 
62350  56 
where 
63025  57 
"LEAST_COMMON_MULTIPLE A f \<equiv> Lcm (f ` A)" 
62350  58 

59 
end 

60 

61 
syntax 

63025  62 
"_GCD1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3GCD _./ _)" [0, 10] 10) 
63 
"_GCD" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3GCD _\<in>_./ _)" [0, 0, 10] 10) 

64 
"_LCM1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3LCM _./ _)" [0, 10] 10) 

65 
"_LCM" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3LCM _\<in>_./ _)" [0, 0, 10] 10) 

62350  66 

67 
translations 

63025  68 
"GCD x y. B" \<rightleftharpoons> "GCD x. GCD y. B" 
69 
"GCD x. B" \<rightleftharpoons> "CONST GREATEST_COMMON_DIVISOR CONST UNIV (\<lambda>x. B)" 

70 
"GCD x. B" \<rightleftharpoons> "GCD x \<in> CONST UNIV. B" 

71 
"GCD x\<in>A. B" \<rightleftharpoons> "CONST GREATEST_COMMON_DIVISOR A (\<lambda>x. B)" 

72 
"LCM x y. B" \<rightleftharpoons> "LCM x. LCM y. B" 

73 
"LCM x. B" \<rightleftharpoons> "CONST LEAST_COMMON_MULTIPLE CONST UNIV (\<lambda>x. B)" 

74 
"LCM x. B" \<rightleftharpoons> "LCM x \<in> CONST UNIV. B" 

75 
"LCM x\<in>A. B" \<rightleftharpoons> "CONST LEAST_COMMON_MULTIPLE A (\<lambda>x. B)" 

62350  76 

77 
print_translation \<open> 

63025  78 
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax GREATEST_COMMON_DIVISOR} @{syntax_const "_GCD"}, 
79 
Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax LEAST_COMMON_MULTIPLE} @{syntax_const "_LCM"}] 

62350  80 
\<close> \<comment> \<open>to avoid etacontraction of body\<close> 
60686  81 

82 
class semiring_gcd = normalization_semidom + gcd + 

59008  83 
assumes gcd_dvd1 [iff]: "gcd a b dvd a" 
59977  84 
and gcd_dvd2 [iff]: "gcd a b dvd b" 
85 
and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" 

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

88 
begin 

89 

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

93 

60689  94 
lemma gcd_dvdI1: 
95 
"a dvd c \<Longrightarrow> gcd a b dvd c" 

96 
by (rule dvd_trans) (rule gcd_dvd1) 

97 

98 
lemma gcd_dvdI2: 

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

100 
by (rule dvd_trans) (rule gcd_dvd2) 

101 

62345  102 
lemma dvd_gcdD1: 
103 
"a dvd gcd b c \<Longrightarrow> a dvd b" 

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

105 

106 
lemma dvd_gcdD2: 

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

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

109 

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

112 
by (rule associated_eqI) simp_all 
60686  113 

114 
lemma gcd_0_right [simp]: 

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

116 
by (rule associated_eqI) simp_all 
60686  117 

118 
lemma gcd_eq_0_iff [simp]: 

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

120 
proof 

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

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

123 
then show ?Q by simp 

124 
next 

125 
assume ?Q then show ?P by simp 

126 
qed 

127 

128 
lemma unit_factor_gcd: 

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

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

131 
case True then show ?thesis by simp 

132 
next 

133 
case False 

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

135 
by (rule unit_factor_mult_normalize) 

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

137 
by simp 

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

139 
by simp 

140 
with False show ?thesis by simp 

141 
qed 

142 

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

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

146 

61605  147 
sublocale gcd: abel_semigroup gcd 
60686  148 
proof 
149 
fix a b c 

150 
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

151 
by (rule associated_eqI) simp_all 
60686  152 
from gcd_dvd1 have "gcd (gcd a b) c dvd a" 
153 
by (rule dvd_trans) simp 

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

155 
by (rule dvd_trans) simp 

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

157 
by (auto intro!: gcd_greatest) 

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

159 
by (rule dvd_trans) simp 

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

161 
by (rule dvd_trans) simp 

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

163 
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

164 
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

165 
by (rule associated_eqI) simp_all 
60686  166 
qed 
167 

168 
lemma gcd_self [simp]: 

169 
"gcd a a = normalize a" 

170 
proof  

171 
have "a dvd gcd a a" 

172 
by (rule gcd_greatest) simp_all 

173 
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

174 
by (auto intro: associated_eqI) 
60686  175 
qed 
61913  176 

177 
lemma gcd_left_idem [simp]: 

178 
"gcd a (gcd a b) = gcd a b" 

179 
by (auto intro: associated_eqI) 

180 

181 
lemma gcd_right_idem [simp]: 

182 
"gcd (gcd a b) b = gcd a b" 

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

184 

60686  185 
lemma coprime_1_left [simp]: 
186 
"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

187 
by (rule associated_eqI) simp_all 
60686  188 

189 
lemma coprime_1_right [simp]: 

190 
"coprime a 1" 

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

192 

193 
lemma gcd_mult_left: 

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

195 
proof (cases "c = 0") 

196 
case True then show ?thesis by simp 

197 
next 

198 
case False 

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

200 
by (auto intro: gcd_greatest) 

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

202 
by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute) 

203 
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

204 
by (auto intro: associated_eqI) 
60686  205 
then show ?thesis by (simp add: normalize_mult) 
206 
qed 

207 

208 
lemma gcd_mult_right: 

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

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

211 

212 
lemma mult_gcd_left: 

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

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

215 

216 
lemma mult_gcd_right: 

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

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

219 

60689  220 
lemma dvd_lcm1 [iff]: 
60686  221 
"a dvd lcm a b" 
222 
proof  

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

224 
by (simp add: lcm_gcd normalize_mult div_mult_swap) 

225 
then show ?thesis 

226 
by (simp add: lcm_gcd) 

227 
qed 

228 

60689  229 
lemma dvd_lcm2 [iff]: 
60686  230 
"b dvd lcm a b" 
231 
proof  

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

233 
by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps) 

234 
then show ?thesis 

235 
by (simp add: lcm_gcd) 

236 
qed 

237 

60689  238 
lemma dvd_lcmI1: 
239 
"a dvd b \<Longrightarrow> a dvd lcm b c" 

240 
by (rule dvd_trans) (assumption, blast) 

241 

242 
lemma dvd_lcmI2: 

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

244 
by (rule dvd_trans) (assumption, blast) 

245 

62345  246 
lemma lcm_dvdD1: 
247 
"lcm a b dvd c \<Longrightarrow> a dvd c" 

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

249 

250 
lemma lcm_dvdD2: 

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

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

253 

60686  254 
lemma lcm_least: 
255 
assumes "a dvd c" and "b dvd c" 

256 
shows "lcm a b dvd c" 

257 
proof (cases "c = 0") 

258 
case True then show ?thesis by simp 

259 
next 

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

261 
show ?thesis 

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

263 
case True with assms show ?thesis by simp 

264 
next 

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

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

267 
by (simp_all add: mult_dvd_mono) 

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

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

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

271 
using U by (simp add: dvd_mult_unit_iff) 

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

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

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

275 
using False by (simp add: div_dvd_iff_mult ac_simps) 

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

277 
qed 

278 
qed 

279 

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

283 

284 
lemma normalize_lcm [simp]: 

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

286 
by (simp add: lcm_gcd dvd_normalize_div) 

287 

288 
lemma lcm_0_left [simp]: 

289 
"lcm 0 a = 0" 

290 
by (simp add: lcm_gcd) 

291 

292 
lemma lcm_0_right [simp]: 

293 
"lcm a 0 = 0" 

294 
by (simp add: lcm_gcd) 

295 

296 
lemma lcm_eq_0_iff: 

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

298 
proof 

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

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

301 
by (simp add: lcm_gcd) 

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

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

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

305 
by simp 

306 
then show ?Q by simp 

307 
next 

308 
assume ?Q then show ?P by auto 

309 
qed 

310 

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

313 
by (auto intro: associated_eqI) 

314 

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

317 
by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd) 

318 

61605  319 
sublocale lcm: abel_semigroup lcm 
60686  320 
proof 
321 
fix a b c 

322 
show "lcm a b = lcm b a" 

323 
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

324 
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

325 
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

326 
by (auto intro: lcm_least 
60686  327 
dvd_trans [of b "lcm b c" "lcm a (lcm b c)"] 
328 
dvd_trans [of c "lcm b c" "lcm a (lcm b c)"] 

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

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

331 
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

332 
by (rule associated_eqI) simp_all 
60686  333 
qed 
334 

335 
lemma lcm_self [simp]: 

336 
"lcm a a = normalize a" 

337 
proof  

338 
have "lcm a a dvd a" 

339 
by (rule lcm_least) simp_all 

340 
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

341 
by (auto intro: associated_eqI) 
60686  342 
qed 
343 

61913  344 
lemma lcm_left_idem [simp]: 
345 
"lcm a (lcm a b) = lcm a b" 

346 
by (auto intro: associated_eqI) 

347 

348 
lemma lcm_right_idem [simp]: 

349 
"lcm (lcm a b) b = lcm a b" 

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

351 

60686  352 
lemma gcd_mult_lcm [simp]: 
353 
"gcd a b * lcm a b = normalize a * normalize b" 

354 
by (simp add: lcm_gcd normalize_mult) 

355 

356 
lemma lcm_mult_gcd [simp]: 

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

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

359 

360 
lemma gcd_lcm: 

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

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

363 
proof  

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

365 
by (simp add: lcm_eq_0_iff) 

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

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

368 
by (simp_all add: normalize_mult) 

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

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

371 
qed 

372 

373 
lemma lcm_1_left [simp]: 

374 
"lcm 1 a = normalize a" 

375 
by (simp add: lcm_gcd) 

376 

377 
lemma lcm_1_right [simp]: 

378 
"lcm a 1 = normalize a" 

379 
by (simp add: lcm_gcd) 

380 

381 
lemma lcm_mult_left: 

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

383 
by (cases "c = 0") 

384 
(simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps, 

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

386 

387 
lemma lcm_mult_right: 

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

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

390 

391 
lemma mult_lcm_left: 

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

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

394 

395 
lemma mult_lcm_right: 

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

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

62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

398 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

399 
lemma gcdI: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

400 
assumes "c dvd a" and "c dvd b" and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

401 
and "normalize c = c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

402 
shows "c = gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

403 
by (rule associated_eqI) (auto simp: assms intro: gcd_greatest) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

404 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

405 
lemma gcd_unique: "d dvd a \<and> d dvd b \<and> 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

406 
normalize d = d \<and> 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

407 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

408 
by rule (auto intro: gcdI simp: gcd_greatest) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

409 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

410 
lemma gcd_dvd_prod: "gcd a b dvd k * b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

411 
using mult_dvd_mono [of 1] by auto 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

412 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

413 
lemma gcd_proj2_if_dvd: "b dvd a \<Longrightarrow> gcd a b = normalize b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

414 
by (rule gcdI [symmetric]) simp_all 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

415 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

416 
lemma gcd_proj1_if_dvd: "a dvd b \<Longrightarrow> gcd a b = normalize a" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

417 
by (rule gcdI [symmetric]) simp_all 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

418 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

419 
lemma gcd_proj1_iff: "gcd m n = normalize m \<longleftrightarrow> m dvd n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

420 
proof 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

421 
assume A: "gcd m n = normalize m" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

422 
show "m dvd n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

423 
proof (cases "m = 0") 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

424 
assume [simp]: "m \<noteq> 0" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

425 
from A have B: "m = gcd m n * unit_factor m" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

426 
by (simp add: unit_eq_div2) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

427 
show ?thesis by (subst B, simp add: mult_unit_dvd_iff) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

428 
qed (insert A, simp) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

429 
next 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

430 
assume "m dvd n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

431 
then show "gcd m n = normalize m" by (rule gcd_proj1_if_dvd) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

432 
qed 
60686  433 

62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

434 
lemma gcd_proj2_iff: "gcd m n = normalize n \<longleftrightarrow> n dvd m" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

435 
using gcd_proj1_iff [of n m] by (simp add: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

436 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

437 
lemma gcd_mult_distrib': "normalize c * gcd a b = gcd (c * a) (c * b)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

438 
by (rule gcdI) (auto simp: normalize_mult gcd_greatest mult_dvd_mono gcd_mult_left[symmetric]) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

439 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

440 
lemma gcd_mult_distrib: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

441 
"k * gcd a b = gcd (k * a) (k * b) * unit_factor k" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

442 
proof 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

443 
have "normalize k * gcd a b = gcd (k * a) (k * b)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

444 
by (simp add: gcd_mult_distrib') 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

445 
then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

446 
by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

447 
then have "normalize k * unit_factor k * gcd a b = gcd (k * a) (k * b) * unit_factor k" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

448 
by (simp only: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

449 
then show ?thesis 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

450 
by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

451 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

452 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

453 
lemma lcm_mult_unit1: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

454 
"is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

455 
by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

456 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

457 
lemma lcm_mult_unit2: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

458 
"is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

459 
using lcm_mult_unit1 [of a c b] by (simp add: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

460 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

461 
lemma lcm_div_unit1: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

462 
"is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

463 
by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

464 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

465 
lemma lcm_div_unit2: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

466 
"is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

467 
by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

468 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

469 
lemma normalize_lcm_left [simp]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

470 
"lcm (normalize a) b = lcm a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

471 
proof (cases "a = 0") 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

472 
case True then show ?thesis 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

473 
by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

474 
next 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

475 
case False then have "is_unit (unit_factor a)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

476 
by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

477 
moreover have "normalize a = a div unit_factor a" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

478 
by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

479 
ultimately show ?thesis 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

480 
by (simp only: lcm_div_unit1) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

481 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

482 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

483 
lemma normalize_lcm_right [simp]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

484 
"lcm a (normalize b) = lcm a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

485 
using normalize_lcm_left [of b a] by (simp add: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

486 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

487 
lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

488 
apply (rule gcdI) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

489 
apply simp_all 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

490 
apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

491 
done 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

492 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

493 
lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

494 
by (subst gcd.commute, subst gcd_mult_unit1, assumption, rule gcd.commute) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

495 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

496 
lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

497 
by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

498 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

499 
lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

500 
by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

501 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

502 
lemma normalize_gcd_left [simp]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

503 
"gcd (normalize a) b = gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

504 
proof (cases "a = 0") 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

505 
case True then show ?thesis 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

506 
by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

507 
next 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

508 
case False then have "is_unit (unit_factor a)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

509 
by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

510 
moreover have "normalize a = a div unit_factor a" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

511 
by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

512 
ultimately show ?thesis 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

513 
by (simp only: gcd_div_unit1) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

514 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

515 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

516 
lemma normalize_gcd_right [simp]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

517 
"gcd a (normalize b) = gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

518 
using normalize_gcd_left [of b a] by (simp add: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

519 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

520 
lemma comp_fun_idem_gcd: "comp_fun_idem gcd" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

521 
by standard (simp_all add: fun_eq_iff ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

522 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

523 
lemma comp_fun_idem_lcm: "comp_fun_idem lcm" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

524 
by standard (simp_all add: fun_eq_iff ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

525 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

526 
lemma gcd_dvd_antisym: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

527 
"gcd a b dvd gcd c d \<Longrightarrow> gcd c d dvd gcd a b \<Longrightarrow> gcd a b = gcd c d" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

528 
proof (rule gcdI) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

529 
assume A: "gcd a b dvd gcd c d" and B: "gcd c d dvd gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

530 
have "gcd c d dvd c" by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

531 
with A show "gcd a b dvd c" by (rule dvd_trans) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

532 
have "gcd c d dvd d" by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

533 
with A show "gcd a b dvd d" by (rule dvd_trans) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

534 
show "normalize (gcd a b) = gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

535 
by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

536 
fix l assume "l dvd c" and "l dvd d" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

537 
hence "l dvd gcd c d" by (rule gcd_greatest) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

538 
from this and B show "l dvd gcd a b" by (rule dvd_trans) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

539 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

540 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

541 
lemma coprime_dvd_mult: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

542 
assumes "coprime a b" and "a dvd c * b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

543 
shows "a dvd c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

544 
proof (cases "c = 0") 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

545 
case True then show ?thesis by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

546 
next 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

547 
case False 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

548 
then have unit: "is_unit (unit_factor c)" by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

549 
from \<open>coprime a b\<close> mult_gcd_left [of c a b] 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

550 
have "gcd (c * a) (c * b) * unit_factor c = c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

551 
by (simp add: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

552 
moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

553 
by (simp add: dvd_mult_unit_iff unit) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

554 
ultimately show ?thesis by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

555 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

556 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

557 
lemma coprime_dvd_mult_iff: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

558 
assumes "coprime a c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

559 
shows "a dvd b * c \<longleftrightarrow> a dvd b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

560 
using assms by (auto intro: coprime_dvd_mult) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

561 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

562 
lemma gcd_mult_cancel: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

563 
"coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

564 
apply (rule associated_eqI) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

565 
apply (rule gcd_greatest) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

566 
apply (rule_tac b = c in coprime_dvd_mult) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

567 
apply (simp add: gcd.assoc) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

568 
apply (simp_all add: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

569 
done 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

570 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

571 
lemma coprime_crossproduct: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

572 
fixes a b c d 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

573 
assumes "coprime a d" and "coprime b c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

574 
shows "normalize a * normalize c = normalize b * normalize d 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

575 
\<longleftrightarrow> normalize a = normalize b \<and> normalize c = normalize d" (is "?lhs \<longleftrightarrow> ?rhs") 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

576 
proof 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

577 
assume ?rhs then show ?lhs by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

578 
next 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

579 
assume ?lhs 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

580 
from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

581 
by (auto intro: dvdI dest: sym) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

582 
with \<open>coprime a d\<close> have "a dvd b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

583 
by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric]) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

584 
from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

585 
by (auto intro: dvdI dest: sym) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

586 
with \<open>coprime b c\<close> have "b dvd a" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

587 
by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric]) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

588 
from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

589 
by (auto intro: dvdI dest: sym simp add: mult.commute) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

590 
with \<open>coprime b c\<close> have "c dvd d" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

591 
by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric]) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

592 
from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

593 
by (auto intro: dvdI dest: sym simp add: mult.commute) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

594 
with \<open>coprime a d\<close> have "d dvd c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

595 
by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric]) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

596 
from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

597 
by (rule associatedI) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

598 
moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

599 
by (rule associatedI) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

600 
ultimately show ?rhs .. 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

601 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

602 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

603 
lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

604 
by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

605 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

606 
lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

607 
using gcd_add1 [of n m] by (simp add: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

608 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

609 
lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

610 
by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

611 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

612 
lemma coprimeI: "(\<And>l. \<lbrakk>l dvd a; l dvd b\<rbrakk> \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

613 
by (rule sym, rule gcdI, simp_all) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

614 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

615 
lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

616 
by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

617 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

618 
lemma div_gcd_coprime: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

619 
assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

620 
shows "coprime (a div gcd a b) (b div gcd a b)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

621 
proof  
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

622 
let ?g = "gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

623 
let ?a' = "a div ?g" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

624 
let ?b' = "b div ?g" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

625 
let ?g' = "gcd ?a' ?b'" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

626 
have dvdg: "?g dvd a" "?g dvd b" by simp_all 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

627 
have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

628 
from dvdg dvdg' obtain ka kb ka' kb' where 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

629 
kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

630 
unfolding dvd_def by blast 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

631 
from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

632 
by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"]) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

633 
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

634 
by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

635 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

636 
have "?g \<noteq> 0" using nz by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

637 
moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

638 
thm dvd_mult_cancel_left 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

639 
ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

640 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

641 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

642 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

643 
lemma divides_mult: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

644 
assumes "a dvd c" and nr: "b dvd c" and "coprime a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

645 
shows "a * b dvd c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

646 
proof 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

647 
from \<open>b dvd c\<close> obtain b' where"c = b * b'" .. 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

648 
with \<open>a dvd c\<close> have "a dvd b' * b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

649 
by (simp add: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

650 
with \<open>coprime a b\<close> have "a dvd b'" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

651 
by (simp add: coprime_dvd_mult_iff) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

652 
then obtain a' where "b' = a * a'" .. 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

653 
with \<open>c = b * b'\<close> have "c = (a * b) * a'" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

654 
by (simp add: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

655 
then show ?thesis .. 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

656 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

657 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

658 
lemma coprime_lmult: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

659 
assumes dab: "gcd d (a * b) = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

660 
shows "gcd d a = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

661 
proof (rule coprimeI) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

662 
fix l assume "l dvd d" and "l dvd a" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

663 
hence "l dvd a * b" by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

664 
with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

665 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

666 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

667 
lemma coprime_rmult: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

668 
assumes dab: "gcd d (a * b) = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

669 
shows "gcd d b = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

670 
proof (rule coprimeI) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

671 
fix l assume "l dvd d" and "l dvd b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

672 
hence "l dvd a * b" by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

673 
with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

674 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

675 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

676 
lemma coprime_mult: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

677 
assumes da: "coprime d a" and db: "coprime d b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

678 
shows "coprime d (a * b)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

679 
apply (subst gcd.commute) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

680 
using da apply (subst gcd_mult_cancel) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

681 
apply (subst gcd.commute, assumption) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

682 
apply (subst gcd.commute, rule db) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

683 
done 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

684 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

685 
lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

686 
using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b] by blast 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

687 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

688 
lemma gcd_coprime: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

689 
assumes c: "gcd a b \<noteq> 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

690 
shows "gcd a' b' = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

691 
proof  
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

692 
from c have "a \<noteq> 0 \<or> b \<noteq> 0" by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

693 
with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" . 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

694 
also from assms have "a div gcd a b = a'" using dvd_div_eq_mult local.gcd_dvd1 by blast 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

695 
also from assms have "b div gcd a b = b'" using dvd_div_eq_mult local.gcd_dvd1 by blast 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

696 
finally show ?thesis . 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

697 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

698 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

699 
lemma coprime_power: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

700 
assumes "0 < n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

701 
shows "gcd a (b ^ n) = 1 \<longleftrightarrow> gcd a b = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

702 
using assms proof (induct n) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

703 
case (Suc n) then show ?case 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

704 
by (cases n) (simp_all add: coprime_mul_eq) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

705 
qed simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

706 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

707 
lemma gcd_coprime_exists: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

708 
assumes nz: "gcd a b \<noteq> 0" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

709 
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

710 
apply (rule_tac x = "a div gcd a b" in exI) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

711 
apply (rule_tac x = "b div gcd a b" in exI) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

712 
apply (insert nz, auto intro: div_gcd_coprime) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

713 
done 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

714 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

715 
lemma coprime_exp: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

716 
"gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

717 
by (induct n, simp_all add: coprime_mult) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

718 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

719 
lemma coprime_exp_left: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

720 
assumes "coprime a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

721 
shows "coprime (a ^ n) b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

722 
using assms by (induct n) (simp_all add: gcd_mult_cancel) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

723 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

724 
lemma coprime_exp2: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

725 
assumes "coprime a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

726 
shows "coprime (a ^ n) (b ^ m)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

727 
proof (rule coprime_exp_left) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

728 
from assms show "coprime a (b ^ m)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

729 
by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a]) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

730 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

731 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

732 
lemma gcd_exp: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

733 
"gcd (a ^ n) (b ^ n) = gcd a b ^ n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

734 
proof (cases "a = 0 \<and> b = 0") 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

735 
case True 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

736 
then show ?thesis by (cases n) simp_all 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

737 
next 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

738 
case False 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

739 
then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

740 
using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

741 
then have "gcd a b ^ n = gcd a b ^ n * ..." by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

742 
also note gcd_mult_distrib 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

743 
also have "unit_factor (gcd a b ^ n) = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

744 
using False by (auto simp add: unit_factor_power unit_factor_gcd) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

745 
also have "(gcd a b)^n * (a div gcd a b)^n = a^n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

746 
by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

747 
also have "(gcd a b)^n * (b div gcd a b)^n = b^n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

748 
by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

749 
finally show ?thesis by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

750 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

751 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

752 
lemma coprime_common_divisor: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

753 
"gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

754 
apply (subgoal_tac "a dvd gcd a b") 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

755 
apply simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

756 
apply (erule (1) gcd_greatest) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

757 
done 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

758 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

759 
lemma division_decomp: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

760 
assumes dc: "a dvd b * c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

761 
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

762 
proof (cases "gcd a b = 0") 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

763 
assume "gcd a b = 0" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

764 
hence "a = 0 \<and> b = 0" by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

765 
hence "a = 0 * c \<and> 0 dvd b \<and> c dvd c" by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

766 
then show ?thesis by blast 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

767 
next 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

768 
let ?d = "gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

769 
assume "?d \<noteq> 0" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

770 
from gcd_coprime_exists[OF this] 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

771 
obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

772 
by blast 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

773 
from ab'(1) have "a' dvd a" unfolding dvd_def by blast 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

774 
with dc have "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

775 
from dc ab'(1,2) have "a'*?d dvd (b'*?d) * c" by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

776 
hence "?d * a' dvd ?d * (b' * c)" by (simp add: mult_ac) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

777 
with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c" by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

778 
with coprime_dvd_mult[OF ab'(3)] 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

779 
have "a' dvd c" by (subst (asm) ac_simps, blast) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

780 
with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c" by (simp add: mult_ac) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

781 
then show ?thesis by blast 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

782 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

783 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

784 
lemma pow_divs_pow: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

785 
assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

786 
shows "a dvd b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

787 
proof (cases "gcd a b = 0") 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

788 
assume "gcd a b = 0" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

789 
then show ?thesis by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

790 
next 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

791 
let ?d = "gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

792 
assume "?d \<noteq> 0" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

793 
from n obtain m where m: "n = Suc m" by (cases n, simp_all) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

794 
from \<open>?d \<noteq> 0\<close> have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

795 
from gcd_coprime_exists[OF \<open>?d \<noteq> 0\<close>] 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

796 
obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

797 
by blast 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

798 
from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

799 
by (simp add: ab'(1,2)[symmetric]) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

800 
hence "?d^n * a'^n dvd ?d^n * b'^n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

801 
by (simp only: power_mult_distrib ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

802 
with zn have "a'^n dvd b'^n" by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

803 
hence "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

804 
hence "a' dvd b'^m * b'" by (simp add: m ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

805 
with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]] 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

806 
have "a' dvd b'" by (subst (asm) ac_simps, blast) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

807 
hence "a'*?d dvd b'*?d" by (rule mult_dvd_mono, simp) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

808 
with ab'(1,2) show ?thesis by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

809 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

810 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

811 
lemma pow_divs_eq [simp]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

812 
"n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

813 
by (auto intro: pow_divs_pow dvd_power_same) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

814 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

815 
lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

816 
by (subst add_commute, simp) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

817 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

818 
lemma setprod_coprime [rule_format]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

819 
"(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

820 
apply (cases "finite A") 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

821 
apply (induct set: finite) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

822 
apply (auto simp add: gcd_mult_cancel) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

823 
done 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

824 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

825 
lemma listprod_coprime: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

826 
"(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (listprod xs) y" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

827 
by (induction xs) (simp_all add: gcd_mult_cancel) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

828 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

829 
lemma coprime_divisors: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

830 
assumes "d dvd a" "e dvd b" "gcd a b = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

831 
shows "gcd d e = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

832 
proof  
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

833 
from assms obtain k l where "a = d * k" "b = e * l" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

834 
unfolding dvd_def by blast 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

835 
with assms have "gcd (d * k) (e * l) = 1" by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

836 
hence "gcd (d * k) e = 1" by (rule coprime_lmult) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

837 
also have "gcd (d * k) e = gcd e (d * k)" by (simp add: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

838 
finally have "gcd e d = 1" by (rule coprime_lmult) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

839 
then show ?thesis by (simp add: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

840 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

841 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

842 
lemma lcm_gcd_prod: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

843 
"lcm a b * gcd a b = normalize (a * b)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

844 
by (simp add: lcm_gcd) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

845 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

846 
declare unit_factor_lcm [simp] 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

847 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

848 
lemma lcmI: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

849 
assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

850 
and "normalize c = c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

851 
shows "c = lcm a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

852 
by (rule associated_eqI) (auto simp: assms intro: lcm_least) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

853 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

854 
lemma gcd_dvd_lcm [simp]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

855 
"gcd a b dvd lcm a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

856 
using gcd_dvd2 by (rule dvd_lcmI2) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

857 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

858 
lemmas lcm_0 = lcm_0_right 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

859 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

860 
lemma lcm_unique: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

861 
"a dvd d \<and> b dvd d \<and> 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

862 
normalize d = d \<and> 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

863 
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

864 
by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

865 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

866 
lemma lcm_coprime: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

867 
"gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

868 
by (subst lcm_gcd) simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

869 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

870 
lemma lcm_proj1_if_dvd: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

871 
"b dvd a \<Longrightarrow> lcm a b = normalize a" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

872 
by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

873 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

874 
lemma lcm_proj2_if_dvd: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

875 
"a dvd b \<Longrightarrow> lcm a b = normalize b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

876 
using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

877 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

878 
lemma lcm_proj1_iff: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

879 
"lcm m n = normalize m \<longleftrightarrow> n dvd m" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

880 
proof 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

881 
assume A: "lcm m n = normalize m" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

882 
show "n dvd m" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

883 
proof (cases "m = 0") 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

884 
assume [simp]: "m \<noteq> 0" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

885 
from A have B: "m = lcm m n * unit_factor m" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

886 
by (simp add: unit_eq_div2) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

887 
show ?thesis by (subst B, simp) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

888 
qed simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

889 
next 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

890 
assume "n dvd m" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

891 
then show "lcm m n = normalize m" by (rule lcm_proj1_if_dvd) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

892 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

893 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

894 
lemma lcm_proj2_iff: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

895 
"lcm m n = normalize n \<longleftrightarrow> m dvd n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

896 
using lcm_proj1_iff [of n m] by (simp add: ac_simps) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

897 

60686  898 
end 
899 

62345  900 
class ring_gcd = comm_ring_1 + semiring_gcd 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

901 
begin 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

902 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

903 
lemma coprime_minus_one: "coprime (n  1) n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

904 
using coprime_plus_one[of "n  1"] by (simp add: gcd.commute) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

905 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

906 
lemma gcd_neg1 [simp]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

907 
"gcd (a) b = gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

908 
by (rule sym, rule gcdI, simp_all add: gcd_greatest) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

909 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

910 
lemma gcd_neg2 [simp]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

911 
"gcd a (b) = gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

912 
by (rule sym, rule gcdI, simp_all add: gcd_greatest) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

913 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

914 
lemma gcd_neg_numeral_1 [simp]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

915 
"gcd ( numeral n) a = gcd (numeral n) a" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

916 
by (fact gcd_neg1) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

917 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

918 
lemma gcd_neg_numeral_2 [simp]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

919 
"gcd a ( numeral n) = gcd a (numeral n)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

920 
by (fact gcd_neg2) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

921 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

922 
lemma gcd_diff1: "gcd (m  n) n = gcd m n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

923 
by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric], subst gcd_add1, simp) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

924 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

925 
lemma gcd_diff2: "gcd (n  m) n = gcd m n" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

926 
by (subst gcd_neg1[symmetric], simp only: minus_diff_eq gcd_diff1) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

927 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

928 
lemma lcm_neg1 [simp]: "lcm (a) b = lcm a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

929 
by (rule sym, rule lcmI, simp_all add: lcm_least lcm_eq_0_iff) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

930 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

931 
lemma lcm_neg2 [simp]: "lcm a (b) = lcm a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

932 
by (rule sym, rule lcmI, simp_all add: lcm_least lcm_eq_0_iff) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

933 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

934 
lemma lcm_neg_numeral_1 [simp]: "lcm ( numeral n) a = lcm (numeral n) a" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

935 
by (fact lcm_neg1) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

936 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

937 
lemma lcm_neg_numeral_2 [simp]: "lcm a ( numeral n) = lcm a (numeral n)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

938 
by (fact lcm_neg2) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

939 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

940 
end 
62345  941 

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

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

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

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

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

60686  949 
begin 
950 

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

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

954 

955 
lemma Gcd_Lcm: 

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

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

958 

60686  959 
lemma Gcd_empty [simp]: 
960 
"Gcd {} = 0" 

961 
by (rule dvd_0_left, rule Gcd_greatest) simp 

962 

62345  963 
lemma Lcm_empty [simp]: 
964 
"Lcm {} = 1" 

965 
by (auto intro: associated_eqI Lcm_least) 

966 

967 
lemma Gcd_insert [simp]: 

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

969 
proof  

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

971 
by (auto intro: Gcd_dvd Gcd_greatest) 

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

973 
proof (rule Gcd_greatest) 

974 
fix b 

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

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

977 
proof 

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

979 
next 

980 
assume "b \<in> A" 

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

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

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

984 
qed 

985 
qed 

986 
ultimately show ?thesis 

987 
by (auto intro: associated_eqI) 

988 
qed 

989 

990 
lemma Lcm_insert [simp]: 

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

992 
proof (rule sym) 

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

994 
by (auto intro: dvd_Lcm Lcm_least) 

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

996 
proof (rule Lcm_least) 

997 
fix b 

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

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

1000 
proof 

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

1002 
next 

1003 
assume "b \<in> A" 

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

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

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

1007 
qed 

1008 
qed 

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

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

1011 
qed 

1012 

62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1013 
lemma LcmI: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1014 
assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1015 
and "normalize b = b" shows "b = Lcm A" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1016 
by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1017 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1018 
lemma Lcm_subset: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1019 
"A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1020 
by (blast intro: Lcm_least dvd_Lcm) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1021 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1022 
lemma Lcm_Un: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1023 
"Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1024 
apply (rule lcmI) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1025 
apply (blast intro: Lcm_subset) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1026 
apply (blast intro: Lcm_subset) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1027 
apply (intro Lcm_least ballI, elim UnE) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1028 
apply (rule dvd_trans, erule dvd_Lcm, assumption) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1029 
apply (rule dvd_trans, erule dvd_Lcm, assumption) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1030 
apply simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1031 
done 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1032 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1033 

60686  1034 
lemma Gcd_0_iff [simp]: 
60687  1035 
"Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q") 
60686  1036 
proof 
1037 
assume ?P 

1038 
show ?Q 

1039 
proof 

1040 
fix a 

1041 
assume "a \<in> A" 

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

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

60686  1045 
qed 
1046 
next 

1047 
assume ?Q 

1048 
have "0 dvd Gcd A" 

1049 
proof (rule Gcd_greatest) 

1050 
fix a 

1051 
assume "a \<in> A" 

60687  1052 
with \<open>?Q\<close> have "a = 0" by auto 
60686  1053 
then show "0 dvd a" by simp 
1054 
qed 

1055 
then show ?P by simp 

1056 
qed 

1057 

1058 
lemma Lcm_1_iff [simp]: 

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

1060 
proof 

1061 
assume ?P 

1062 
show ?Q 

1063 
proof 

1064 
fix a 

1065 
assume "a \<in> A" 

1066 
then have "a dvd Lcm A" 

1067 
by (rule dvd_Lcm) 

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

1069 
by simp 

1070 
qed 

1071 
next 

1072 
assume ?Q 

1073 
then have "is_unit (Lcm A)" 

1074 
by (blast intro: Lcm_least) 

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

1076 
by (rule is_unit_normalize) 

1077 
then show ?P 

1078 
by simp 

1079 
qed 

1080 

62345  1081 
lemma unit_factor_Lcm: 
1082 
"unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" 

1083 
proof (cases "Lcm A = 0") 

1084 
case True then show ?thesis by simp 

1085 
next 

1086 
case False 

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

1088 
by blast 

1089 
with False show ?thesis 

1090 
by simp 

1091 
qed 

1092 

62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1093 
lemma unit_factor_Gcd: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1094 
proof  
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1095 
show "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1096 
by (simp add: Gcd_Lcm unit_factor_Lcm) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1097 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1098 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1099 
lemma GcdI: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1100 
assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1101 
and "normalize b = b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1102 
shows "b = Gcd A" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1103 
by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1104 

62345  1105 
lemma Gcd_eq_1_I: 
1106 
assumes "is_unit a" and "a \<in> A" 

1107 
shows "Gcd A = 1" 

1108 
proof  

1109 
from assms have "is_unit (Gcd A)" 

1110 
by (blast intro: Gcd_dvd dvd_unit_imp_unit) 

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

1112 
by (rule is_unit_normalize) 

1113 
then show ?thesis 

1114 
by simp 

1115 
qed 

1116 

60686  1117 
lemma Lcm_eq_0_I: 
1118 
assumes "0 \<in> A" 

1119 
shows "Lcm A = 0" 

1120 
proof  

1121 
from assms have "0 dvd Lcm A" 

1122 
by (rule dvd_Lcm) 

1123 
then show ?thesis 

1124 
by simp 

1125 
qed 

1126 

62345  1127 
lemma Gcd_UNIV [simp]: 
1128 
"Gcd UNIV = 1" 

1129 
using dvd_refl by (rule Gcd_eq_1_I) simp 

1130 

61929  1131 
lemma Lcm_UNIV [simp]: 
1132 
"Lcm UNIV = 0" 

1133 
by (rule Lcm_eq_0_I) simp 

60686  1134 

61929  1135 
lemma Lcm_0_iff: 
1136 
assumes "finite A" 

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

1138 
proof (cases "A = {}") 

1139 
case True then show ?thesis by simp 

1140 
next 

1141 
case False with assms show ?thesis 

1142 
by (induct A rule: finite_ne_induct) 

1143 
(auto simp add: lcm_eq_0_iff) 

60686  1144 
qed 
61929  1145 

62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1146 
lemma Gcd_finite: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1147 
assumes "finite A" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1148 
shows "Gcd A = Finite_Set.fold gcd 0 A" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1149 
by (induct rule: finite.induct[OF \<open>finite A\<close>]) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1150 
(simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd]) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1151 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1152 
lemma Gcd_set [code_unfold]: "Gcd (set as) = foldl gcd 0 as" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1153 
by (simp add: Gcd_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1154 
foldl_conv_fold gcd.commute) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1155 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1156 
lemma Lcm_finite: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1157 
assumes "finite A" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1158 
shows "Lcm A = Finite_Set.fold lcm 1 A" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1159 
by (induct rule: finite.induct[OF \<open>finite A\<close>]) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1160 
(simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm]) 
62345  1161 

60686  1162 
lemma Lcm_set [code_unfold]: 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1163 
"Lcm (set as) = foldl lcm 1 as" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1164 
by (simp add: Lcm_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1165 
foldl_conv_fold lcm.commute) 
59008  1166 

62345  1167 
lemma Gcd_image_normalize [simp]: 
1168 
"Gcd (normalize ` A) = Gcd A" 

1169 
proof  

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

1171 
proof  

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

62350  1173 
moreover have "gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a" 
62345  1174 
by (rule gcd_dvd1) 
1175 
ultimately show "Gcd (normalize ` A) dvd a" 

1176 
by simp 

1177 
qed 

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

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

1180 
then show ?thesis 

1181 
by (auto intro: associated_eqI) 

1182 
qed 

1183 

62346  1184 
lemma Gcd_eqI: 
1185 
assumes "normalize a = a" 

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

1187 
and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> c dvd b) \<Longrightarrow> c dvd a" 

1188 
shows "Gcd A = a" 

1189 
using assms by (blast intro: associated_eqI Gcd_greatest Gcd_dvd normalize_Gcd) 

1190 

1191 
lemma Lcm_eqI: 

1192 
assumes "normalize a = a" 

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

1194 
and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> b dvd c) \<Longrightarrow> a dvd c" 

1195 
shows "Lcm A = a" 

1196 
using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm) 

1197 

62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1198 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1199 
lemma Lcm_no_units: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1200 
"Lcm A = Lcm (A  {a. is_unit a})" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1201 
proof  
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1202 
have "(A  {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A" by blast 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1203 
hence "Lcm A = lcm (Lcm (A  {a. is_unit a})) (Lcm {a\<in>A. is_unit a})" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1204 
by (simp add: Lcm_Un [symmetric]) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1205 
also have "Lcm {a\<in>A. is_unit a} = 1" by (simp add: Lcm_1_iff) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1206 
finally show ?thesis by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1207 
qed 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1208 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1209 
lemma Lcm_0_iff': "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1210 
by (metis Lcm_least dvd_0_left dvd_Lcm) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1211 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1212 
lemma Lcm_no_multiple: "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)) \<Longrightarrow> Lcm A = 0" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1213 
by (auto simp: Lcm_0_iff') 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1214 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1215 
lemma Lcm_singleton [simp]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1216 
"Lcm {a} = normalize a" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1217 
by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1218 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1219 
lemma Lcm_2 [simp]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1220 
"Lcm {a,b} = lcm a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1221 
by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1222 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1223 
lemma Lcm_coprime: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1224 
assumes "finite A" and "A \<noteq> {}" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1225 
assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1226 
shows "Lcm A = normalize (\<Prod>A)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1227 
using assms proof (induct rule: finite_ne_induct) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1228 
case (insert a A) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1229 
have "Lcm (insert a A) = lcm a (Lcm A)" by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1230 
also from insert have "Lcm A = normalize (\<Prod>A)" by blast 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1231 
also have "lcm a \<dots> = lcm a (\<Prod>A)" by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1232 
also from insert have "gcd a (\<Prod>A) = 1" by (subst gcd.commute, intro setprod_coprime) auto 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1233 
with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1234 
by (simp add: lcm_coprime) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1235 
finally show ?case . 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1236 
qed simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1237 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1238 
lemma Lcm_coprime': 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1239 
"card A \<noteq> 0 \<Longrightarrow> (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1240 
\<Longrightarrow> Lcm A = normalize (\<Prod>A)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1241 
by (rule Lcm_coprime) (simp_all add: card_eq_0_iff) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1242 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1243 
lemma Gcd_1: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1244 
"1 \<in> A \<Longrightarrow> Gcd A = 1" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1245 
by (auto intro!: Gcd_eq_1_I) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1246 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1247 
lemma Gcd_singleton [simp]: "Gcd {a} = normalize a" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1248 
by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1249 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1250 
lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1251 
by simp 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1252 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1253 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1254 
definition pairwise_coprime where 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1255 
"pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1256 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1257 
lemma pairwise_coprimeI [intro?]: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1258 
"(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1259 
by (simp add: pairwise_coprime_def) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1260 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1261 
lemma pairwise_coprimeD: 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1262 
"pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1263 
by (simp add: pairwise_coprime_def) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1264 

25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1265 
lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B" 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1266 
by (force simp: pairwise_coprime_def) 
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel 