author  nipkow 
Mon, 17 Oct 2016 17:33:07 +0200  
changeset 64272  f76b6dda2e56 
parent 64242  93c6f0da5c70 
child 64591  240a39af9ec4 
permissions  rwrr 
63489  1 
(* Title: HOL/GCD.thy 
2 
Author: Christophe Tabacznyj 

3 
Author: Lawrence C. Paulson 

4 
Author: Amine Chaieb 

5 
Author: Thomas M. Rasmussen 

6 
Author: Jeremy Avigad 

7 
Author: Tobias Nipkow 

31706  8 

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

31706  11 

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

13 

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

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

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

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

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

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

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

34915  23 
the natural numbers by Chaieb. 
31706  24 

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

25 
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

26 
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

27 

31798  28 
Tobias Nipkow cleaned up a lot. 
21256  29 
*) 
30 

60758  31 
section \<open>Greatest common divisor and least common multiple\<close> 
21256  32 

33 
theory GCD 

63489  34 
imports Main 
31706  35 
begin 
36 

63489  37 

62345  38 
subsection \<open>Abstract GCD and LCM\<close> 
31706  39 

31992  40 
class gcd = zero + one + dvd + 
41550  41 
fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
42 
and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 

21256  43 
begin 
44 

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

31706  47 

48 
end 

49 

60686  50 
class Gcd = gcd + 
63025  51 
fixes Gcd :: "'a set \<Rightarrow> 'a" 
52 
and Lcm :: "'a set \<Rightarrow> 'a" 

62350  53 
begin 
54 

63025  55 
abbreviation GREATEST_COMMON_DIVISOR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" 
63489  56 
where "GREATEST_COMMON_DIVISOR A f \<equiv> Gcd (f ` A)" 
62350  57 

63025  58 
abbreviation LEAST_COMMON_MULTIPLE :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" 
63489  59 
where "LEAST_COMMON_MULTIPLE A f \<equiv> Lcm (f ` A)" 
62350  60 

61 
end 

62 

63 
syntax 

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

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

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

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

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

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

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

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

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

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

62350  77 

78 
print_translation \<open> 

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

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

83 
class semiring_gcd = normalization_semidom + gcd + 

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

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

63489  89 
begin 
90 

91 
lemma gcd_greatest_iff [simp]: "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c" 

60686  92 
by (blast intro!: gcd_greatest intro: dvd_trans) 
93 

63489  94 
lemma gcd_dvdI1: "a dvd c \<Longrightarrow> gcd a b dvd c" 
60689  95 
by (rule dvd_trans) (rule gcd_dvd1) 
96 

63489  97 
lemma gcd_dvdI2: "b dvd c \<Longrightarrow> gcd a b dvd c" 
60689  98 
by (rule dvd_trans) (rule gcd_dvd2) 
99 

63489  100 
lemma dvd_gcdD1: "a dvd gcd b c \<Longrightarrow> a dvd b" 
62345  101 
using gcd_dvd1 [of b c] by (blast intro: dvd_trans) 
102 

63489  103 
lemma dvd_gcdD2: "a dvd gcd b c \<Longrightarrow> a dvd c" 
62345  104 
using gcd_dvd2 [of b c] by (blast intro: dvd_trans) 
105 

63489  106 
lemma gcd_0_left [simp]: "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

107 
by (rule associated_eqI) simp_all 
60686  108 

63489  109 
lemma gcd_0_right [simp]: "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

110 
by (rule associated_eqI) simp_all 
63489  111 

112 
lemma gcd_eq_0_iff [simp]: "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" 

113 
(is "?P \<longleftrightarrow> ?Q") 

60686  114 
proof 
63489  115 
assume ?P 
116 
then have "0 dvd gcd a b" 

117 
by simp 

118 
then have "0 dvd a" and "0 dvd b" 

119 
by (blast intro: dvd_trans)+ 

120 
then show ?Q 

121 
by simp 

60686  122 
next 
63489  123 
assume ?Q 
124 
then show ?P 

125 
by simp 

60686  126 
qed 
127 

63489  128 
lemma unit_factor_gcd: "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)" 
60686  129 
proof (cases "gcd a b = 0") 
63489  130 
case True 
131 
then show ?thesis by simp 

60686  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 

63489  140 
with False show ?thesis 
141 
by simp 

60686  142 
qed 
143 

63489  144 
lemma is_unit_gcd [simp]: "is_unit (gcd a b) \<longleftrightarrow> coprime a b" 
60690  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 

63489  168 
lemma gcd_self [simp]: "gcd a a = normalize a" 
60686  169 
proof  
170 
have "a dvd gcd a a" 

171 
by (rule gcd_greatest) simp_all 

172 
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

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

63489  176 
lemma gcd_left_idem [simp]: "gcd a (gcd a b) = gcd a b" 
61913  177 
by (auto intro: associated_eqI) 
178 

63489  179 
lemma gcd_right_idem [simp]: "gcd (gcd a b) b = gcd a b" 
61913  180 
unfolding gcd.commute [of a] gcd.commute [of "gcd b a"] by simp 
181 

63489  182 
lemma coprime_1_left [simp]: "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

183 
by (rule associated_eqI) simp_all 
60686  184 

63489  185 
lemma coprime_1_right [simp]: "coprime a 1" 
60686  186 
using coprime_1_left [of a] by (simp add: ac_simps) 
187 

63489  188 
lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b" 
60686  189 
proof (cases "c = 0") 
63489  190 
case True 
191 
then show ?thesis by simp 

60686  192 
next 
193 
case False 

63489  194 
then have *: "c * gcd a b dvd gcd (c * a) (c * b)" 
60686  195 
by (auto intro: gcd_greatest) 
63489  196 
moreover from False * have "gcd (c * a) (c * b) dvd c * gcd a b" 
60686  197 
by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute) 
198 
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

199 
by (auto intro: associated_eqI) 
63489  200 
then show ?thesis 
201 
by (simp add: normalize_mult) 

60686  202 
qed 
203 

63489  204 
lemma gcd_mult_right: "gcd (a * c) (b * c) = gcd b a * normalize c" 
60686  205 
using gcd_mult_left [of c a b] by (simp add: ac_simps) 
206 

63489  207 
lemma mult_gcd_left: "c * gcd a b = unit_factor c * gcd (c * a) (c * b)" 
60686  208 
by (simp add: gcd_mult_left mult.assoc [symmetric]) 
209 

63489  210 
lemma mult_gcd_right: "gcd a b * c = gcd (a * c) (b * c) * unit_factor c" 
60686  211 
using mult_gcd_left [of c a b] by (simp add: ac_simps) 
212 

63489  213 
lemma dvd_lcm1 [iff]: "a dvd lcm a b" 
60686  214 
proof  
215 
have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)" 

216 
by (simp add: lcm_gcd normalize_mult div_mult_swap) 

217 
then show ?thesis 

218 
by (simp add: lcm_gcd) 

219 
qed 

63489  220 

221 
lemma dvd_lcm2 [iff]: "b dvd lcm a b" 

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

224 
by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps) 

225 
then show ?thesis 

226 
by (simp add: lcm_gcd) 

227 
qed 

228 

63489  229 
lemma dvd_lcmI1: "a dvd b \<Longrightarrow> a dvd lcm b c" 
230 
by (rule dvd_trans) (assumption, blast) 

231 

232 
lemma dvd_lcmI2: "a dvd c \<Longrightarrow> a dvd lcm b c" 

60689  233 
by (rule dvd_trans) (assumption, blast) 
234 

63489  235 
lemma lcm_dvdD1: "lcm a b dvd c \<Longrightarrow> a dvd c" 
62345  236 
using dvd_lcm1 [of a b] by (blast intro: dvd_trans) 
237 

63489  238 
lemma lcm_dvdD2: "lcm a b dvd c \<Longrightarrow> b dvd c" 
62345  239 
using dvd_lcm2 [of a b] by (blast intro: dvd_trans) 
240 

60686  241 
lemma lcm_least: 
242 
assumes "a dvd c" and "b dvd c" 

243 
shows "lcm a b dvd c" 

244 
proof (cases "c = 0") 

63489  245 
case True 
246 
then show ?thesis by simp 

60686  247 
next 
63489  248 
case False 
249 
then have *: "is_unit (unit_factor c)" 

250 
by simp 

60686  251 
show ?thesis 
252 
proof (cases "gcd a b = 0") 

63489  253 
case True 
254 
with assms show ?thesis by simp 

60686  255 
next 
63489  256 
case False 
257 
then have "a \<noteq> 0 \<or> b \<noteq> 0" 

258 
by simp 

60686  259 
with \<open>c \<noteq> 0\<close> assms have "a * b dvd a * c" "a * b dvd c * b" 
260 
by (simp_all add: mult_dvd_mono) 

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

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

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

63489  264 
using * by (simp add: dvd_mult_unit_iff) 
60686  265 
then have "normalize (a * b) dvd gcd a b * c" 
266 
by (simp add: mult_gcd_right [of a b c]) 

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

268 
using False by (simp add: div_dvd_iff_mult ac_simps) 

63489  269 
then show ?thesis 
270 
by (simp add: lcm_gcd) 

60686  271 
qed 
272 
qed 

273 

63489  274 
lemma lcm_least_iff [simp]: "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c" 
60686  275 
by (blast intro!: lcm_least intro: dvd_trans) 
276 

63489  277 
lemma normalize_lcm [simp]: "normalize (lcm a b) = lcm a b" 
60686  278 
by (simp add: lcm_gcd dvd_normalize_div) 
279 

63489  280 
lemma lcm_0_left [simp]: "lcm 0 a = 0" 
281 
by (simp add: lcm_gcd) 

282 

283 
lemma lcm_0_right [simp]: "lcm a 0 = 0" 

60686  284 
by (simp add: lcm_gcd) 
63489  285 

286 
lemma lcm_eq_0_iff: "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" 

287 
(is "?P \<longleftrightarrow> ?Q") 

60686  288 
proof 
63489  289 
assume ?P 
290 
then have "0 dvd lcm a b" 

291 
by simp 

60686  292 
then have "0 dvd normalize (a * b) div gcd a b" 
293 
by (simp add: lcm_gcd) 

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

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

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

297 
by simp 

63489  298 
then show ?Q 
299 
by simp 

60686  300 
next 
63489  301 
assume ?Q 
302 
then show ?P 

303 
by auto 

60686  304 
qed 
305 

63489  306 
lemma lcm_eq_1_iff [simp]: "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b" 
61913  307 
by (auto intro: associated_eqI) 
308 

63489  309 
lemma unit_factor_lcm: "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)" 
60686  310 
by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd) 
311 

61605  312 
sublocale lcm: abel_semigroup lcm 
60686  313 
proof 
314 
fix a b c 

315 
show "lcm a b = lcm b a" 

316 
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

317 
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

318 
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

319 
by (auto intro: lcm_least 
60686  320 
dvd_trans [of b "lcm b c" "lcm a (lcm b c)"] 
321 
dvd_trans [of c "lcm b c" "lcm a (lcm b c)"] 

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

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

324 
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

325 
by (rule associated_eqI) simp_all 
60686  326 
qed 
327 

63489  328 
lemma lcm_self [simp]: "lcm a a = normalize a" 
60686  329 
proof  
330 
have "lcm a a dvd a" 

331 
by (rule lcm_least) simp_all 

332 
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

333 
by (auto intro: associated_eqI) 
60686  334 
qed 
335 

63489  336 
lemma lcm_left_idem [simp]: "lcm a (lcm a b) = lcm a b" 
61913  337 
by (auto intro: associated_eqI) 
338 

63489  339 
lemma lcm_right_idem [simp]: "lcm (lcm a b) b = lcm a b" 
61913  340 
unfolding lcm.commute [of a] lcm.commute [of "lcm b a"] by simp 
341 

63489  342 
lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b" 
60686  343 
by (simp add: lcm_gcd normalize_mult) 
344 

63489  345 
lemma lcm_mult_gcd [simp]: "lcm a b * gcd a b = normalize a * normalize b" 
346 
using gcd_mult_lcm [of a b] by (simp add: ac_simps) 

60686  347 

348 
lemma gcd_lcm: 

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

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

351 
proof  

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

353 
by (simp add: lcm_eq_0_iff) 

63489  354 
have "gcd a b * lcm a b = normalize a * normalize b" 
355 
by simp 

60686  356 
then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b" 
357 
by (simp_all add: normalize_mult) 

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

64240  359 
using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp 
60686  360 
qed 
361 

63489  362 
lemma lcm_1_left [simp]: "lcm 1 a = normalize a" 
60686  363 
by (simp add: lcm_gcd) 
364 

63489  365 
lemma lcm_1_right [simp]: "lcm a 1 = normalize a" 
60686  366 
by (simp add: lcm_gcd) 
63489  367 

368 
lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize c * lcm a b" 

60686  369 
by (cases "c = 0") 
370 
(simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps, 

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

372 

63489  373 
lemma lcm_mult_right: "lcm (a * c) (b * c) = lcm b a * normalize c" 
60686  374 
using lcm_mult_left [of c a b] by (simp add: ac_simps) 
375 

63489  376 
lemma mult_lcm_left: "c * lcm a b = unit_factor c * lcm (c * a) (c * b)" 
60686  377 
by (simp add: lcm_mult_left mult.assoc [symmetric]) 
378 

63489  379 
lemma mult_lcm_right: "lcm a b * c = lcm (a * c) (b * c) * unit_factor c" 
60686  380 
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

381 

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

382 
lemma gcdI: 
63489  383 
assumes "c dvd a" and "c dvd b" 
384 
and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c" 

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

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

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

387 
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

388 

63489  389 
lemma gcd_unique: 
390 
"d dvd a \<and> d dvd b \<and> normalize d = d \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 

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

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

392 

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

393 
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

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

395 

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

396 
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

397 
by (rule gcdI [symmetric]) simp_all 
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 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

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

401 

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

402 
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

403 
proof 
63489  404 
assume *: "gcd m n = normalize m" 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

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

406 
proof (cases "m = 0") 
63489  407 
case True 
408 
with * show ?thesis by simp 

409 
next 

410 
case [simp]: False 

411 
from * have **: "m = gcd m n * unit_factor m" 

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

412 
by (simp add: unit_eq_div2) 
63489  413 
show ?thesis 
414 
by (subst **) (simp add: mult_unit_dvd_iff) 

415 
qed 

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

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

417 
assume "m dvd n" 
63489  418 
then show "gcd m n = normalize m" 
419 
by (rule gcd_proj1_if_dvd) 

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

420 
qed 
63489  421 

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

422 
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

423 
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

424 

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

425 
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

426 
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

427 

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

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

430 
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

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

432 
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

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

434 
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

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

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

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

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

439 

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

441 
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

442 

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

444 
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

445 

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

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

447 
"is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c" 
63489  448 
by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1) 
449 

450 
lemma lcm_div_unit2: "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c" 

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

451 
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

452 

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

454 
proof (cases "a = 0") 
63489  455 
case True 
456 
then show ?thesis 

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

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

458 
next 
63489  459 
case False 
460 
then have "is_unit (unit_factor a)" 

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

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

462 
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

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

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

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

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

467 

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

469 
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

470 

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

471 
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

472 
apply (rule gcdI) 
63489  473 
apply simp_all 
474 
apply (rule dvd_trans) 

475 
apply (rule gcd_dvd1) 

476 
apply (simp add: unit_simps) 

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

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

478 

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

479 
lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c" 
63489  480 
apply (subst gcd.commute) 
481 
apply (subst gcd_mult_unit1) 

482 
apply assumption 

483 
apply (rule gcd.commute) 

484 
done 

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

485 

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

486 
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

487 
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

488 

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

489 
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

490 
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

491 

63489  492 
lemma normalize_gcd_left [simp]: "gcd (normalize a) b = gcd a b" 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

493 
proof (cases "a = 0") 
63489  494 
case True 
495 
then show ?thesis 

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

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

497 
next 
63489  498 
case False 
499 
then have "is_unit (unit_factor a)" 

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

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

501 
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

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

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

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

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

506 

63489  507 
lemma normalize_gcd_right [simp]: "gcd a (normalize b) = gcd a b" 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

508 
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

509 

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

510 
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

511 
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

512 

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

513 
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

514 
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

515 

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

517 
proof (rule gcdI) 
63489  518 
assume *: "gcd a b dvd gcd c d" 
519 
and **: "gcd c d dvd gcd a b" 

520 
have "gcd c d dvd c" 

521 
by simp 

522 
with * show "gcd a b dvd c" 

523 
by (rule dvd_trans) 

524 
have "gcd c d dvd d" 

525 
by simp 

526 
with * show "gcd a b dvd d" 

527 
by (rule dvd_trans) 

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

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

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

530 
fix l assume "l dvd c" and "l dvd d" 
63489  531 
then have "l dvd gcd c d" 
532 
by (rule gcd_greatest) 

533 
from this and ** show "l dvd gcd a b" 

534 
by (rule dvd_trans) 

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

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

536 

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

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

538 
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

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

540 
proof (cases "c = 0") 
63489  541 
case True 
542 
then show ?thesis by simp 

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

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

544 
case False 
63489  545 
then have unit: "is_unit (unit_factor c)" 
546 
by simp 

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

547 
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

548 
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

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

550 
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

551 
by (simp add: dvd_mult_unit_iff unit) 
63489  552 
ultimately show ?thesis 
553 
by simp 

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

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

555 

63489  556 
lemma coprime_dvd_mult_iff: "coprime a c \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd b" 
557 
by (auto intro: coprime_dvd_mult) 

558 

559 
lemma gcd_mult_cancel: "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b" 

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

560 
apply (rule associated_eqI) 
63489  561 
apply (rule gcd_greatest) 
562 
apply (rule_tac b = c in coprime_dvd_mult) 

563 
apply (simp add: gcd.assoc) 

564 
apply (simp_all add: ac_simps) 

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

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

566 

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

567 
lemma coprime_crossproduct: 
63489  568 
fixes a b c d :: 'a 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

569 
assumes "coprime a d" and "coprime b c" 
63489  570 
shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow> 
571 
normalize a = normalize b \<and> normalize c = normalize d" 

572 
(is "?lhs \<longleftrightarrow> ?rhs") 

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

573 
proof 
63489  574 
assume ?rhs 
575 
then show ?lhs by simp 

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

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

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

578 
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

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

580 
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

581 
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

582 
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

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

584 
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

585 
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

586 
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

587 
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

588 
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

589 
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

590 
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

591 
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

592 
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

593 
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

594 
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

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

596 
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

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

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

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

600 

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

601 
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

602 
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

603 

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

604 
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

605 
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

606 

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

607 
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

608 
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

609 

63489  610 
lemma coprimeI: "(\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1" 
611 
by (rule sym, rule gcdI) simp_all 

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

612 

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

613 
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

614 
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

615 

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

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

617 
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

618 
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

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

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

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

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

623 
let ?g' = "gcd ?a' ?b'" 
63489  624 
have dvdg: "?g dvd a" "?g dvd b" 
625 
by simp_all 

626 
have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" 

627 
by simp_all 

62429
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 
63489  629 
kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'" 
62429
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" 
63489  634 
by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 
635 
have "?g \<noteq> 0" 

636 
using nz by simp 

62429
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" . 
63489  638 
ultimately show ?thesis 
639 
using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp 

62429
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" 
63489  646 
proof  
62429
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: 
63489  659 
assumes dab: "gcd d (a * b) = 1" 
62429
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) 
63489  662 
fix l 
663 
assume "l dvd d" and "l dvd a" 

664 
then have "l dvd a * b" 

665 
by simp 

666 
with \<open>l dvd d\<close> and dab show "l dvd 1" 

667 
by (auto intro: gcd_greatest) 

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

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

669 

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

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

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

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

673 
proof (rule coprimeI) 
63489  674 
fix l 
675 
assume "l dvd d" and "l dvd b" 

676 
then have "l dvd a * b" 

677 
by simp 

678 
with \<open>l dvd d\<close> and dab show "l dvd 1" 

679 
by (auto intro: gcd_greatest) 

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

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

681 

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

682 
lemma coprime_mult: 
63489  683 
assumes "coprime d a" 
684 
and "coprime d b" 

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

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

686 
apply (subst gcd.commute) 
63489  687 
using assms(1) apply (subst gcd_mult_cancel) 
688 
apply (subst gcd.commute) 

689 
apply assumption 

690 
apply (subst gcd.commute) 

691 
apply (rule assms(2)) 

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

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

693 

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

694 
lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1" 
63489  695 
using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b] 
696 
by blast 

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

697 

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

698 
lemma gcd_coprime: 
63489  699 
assumes c: "gcd a b \<noteq> 0" 
700 
and a: "a = a' * gcd a b" 

701 
and b: "b = b' * gcd a b" 

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

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

703 
proof  
63489  704 
from c have "a \<noteq> 0 \<or> b \<noteq> 0" 
705 
by simp 

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

706 
with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" . 
63489  707 
also from assms have "a div gcd a b = a'" 
708 
using dvd_div_eq_mult local.gcd_dvd1 by blast 

709 
also from assms have "b div gcd a b = b'" 

710 
using dvd_div_eq_mult local.gcd_dvd1 by blast 

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

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

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

713 

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

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

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

716 
shows "gcd a (b ^ n) = 1 \<longleftrightarrow> gcd a b = 1" 
63489  717 
using assms 
718 
proof (induct n) 

719 
case 0 

720 
then show ?case by simp 

721 
next 

722 
case (Suc n) 

723 
then show ?case 

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

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

726 

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

727 
lemma gcd_coprime_exists: 
63489  728 
assumes "gcd a b \<noteq> 0" 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

729 
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

730 
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

731 
apply (rule_tac x = "b div gcd a b" in exI) 
63489  732 
using assms 
733 
apply (auto intro: div_gcd_coprime) 

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

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

735 

63489  736 
lemma coprime_exp: "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1" 
737 
by (induct n) (simp_all add: coprime_mult) 

738 

739 
lemma coprime_exp_left: "coprime a b \<Longrightarrow> coprime (a ^ n) b" 

740 
by (induct n) (simp_all add: gcd_mult_cancel) 

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

741 

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

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

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

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

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

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

747 
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

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

749 

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

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

752 
case True 
63489  753 
then show ?thesis 
754 
by (cases n) simp_all 

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

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

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

757 
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

758 
using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp 
63489  759 
then have "gcd a b ^ n = gcd a b ^ n * \<dots>" 
760 
by simp 

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

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

762 
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

763 
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

764 
also have "(gcd a b)^n * (a div gcd a b)^n = a^n" 
63489  765 
apply (subst ac_simps) 
766 
apply (subst div_power) 

767 
apply simp 

768 
apply (rule dvd_div_mult_self) 

769 
apply (rule dvd_power_same) 

770 
apply simp 

771 
done 

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

772 
also have "(gcd a b)^n * (b div gcd a b)^n = b^n" 
63489  773 
apply (subst ac_simps) 
774 
apply (subst div_power) 

775 
apply simp 

776 
apply (rule dvd_div_mult_self) 

777 
apply (rule dvd_power_same) 

778 
apply simp 

779 
done 

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

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

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

782 

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

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

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

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

788 

63489  789 
lemma division_decomp: 
790 
assumes "a dvd b * c" 

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

791 
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

792 
proof (cases "gcd a b = 0") 
63489  793 
case True 
794 
then have "a = 0 \<and> b = 0" 

795 
by simp 

796 
then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c" 

797 
by simp 

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

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

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

801 
let ?d = "gcd a b" 
63489  802 
from gcd_coprime_exists [OF False] 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

803 
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

804 
by blast 
63489  805 
from ab'(1) have "a' dvd a" 
806 
unfolding dvd_def by blast 

807 
with assms have "a' dvd b * c" 

808 
using dvd_trans[of a' a "b*c"] by simp 

809 
from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c" 

810 
by simp 

811 
then have "?d * a' dvd ?d * (b' * c)" 

812 
by (simp add: mult_ac) 

813 
with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c" 

814 
by simp 

815 
with coprime_dvd_mult[OF ab'(3)] have "a' dvd c" 

816 
by (subst (asm) ac_simps) blast 

817 
with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c" 

818 
by (simp add: mult_ac) 

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

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

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

821 

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

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

823 
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

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

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

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

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

830 
let ?d = "gcd a b" 
63489  831 
from n obtain m where m: "n = Suc m" 
832 
by (cases n) simp_all 

833 
from False have zn: "?d ^ n \<noteq> 0" 

834 
by (rule power_not_zero) 

835 
from gcd_coprime_exists [OF False] 

836 
obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1" 

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

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

838 
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

839 
by (simp add: ab'(1,2)[symmetric]) 
63489  840 
then have "?d^n * a'^n dvd ?d^n * b'^n" 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

841 
by (simp only: power_mult_distrib ac_simps) 
63489  842 
with zn have "a'^n dvd b'^n" 
843 
by simp 

844 
then have "a' dvd b'^n" 

845 
using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m) 

846 
then have "a' dvd b'^m * b'" 

847 
by (simp add: m ac_simps) 

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

848 
with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]] 
63489  849 
have "a' dvd b'" by (subst (asm) ac_simps) blast 
850 
then have "a' * ?d dvd b' * ?d" 

851 
by (rule mult_dvd_mono) simp 

852 
with ab'(1,2) show ?thesis 

853 
by simp 

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

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

855 

63489  856 
lemma pow_divs_eq [simp]: "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b" 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

857 
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

858 

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

859 
lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1" 
63489  860 
by (subst add_commute) simp 
861 

64272  862 
lemma prod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1" 
63915  863 
by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel) 
63489  864 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63489
diff
changeset

865 
lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y" 
63489  866 
by (induct xs) (simp_all add: gcd_mult_cancel) 
867 

868 
lemma coprime_divisors: 

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

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

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

872 
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

873 
unfolding dvd_def by blast 
63489  874 
with assms have "gcd (d * k) (e * l) = 1" 
875 
by simp 

876 
then have "gcd (d * k) e = 1" 

877 
by (rule coprime_lmult) 

878 
also have "gcd (d * k) e = gcd e (d * k)" 

879 
by (simp add: ac_simps) 

880 
finally have "gcd e d = 1" 

881 
by (rule coprime_lmult) 

882 
then show ?thesis 

883 
by (simp add: ac_simps) 

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

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

885 

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

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

888 

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

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

890 

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

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

892 
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

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

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

895 
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

896 

63489  897 
lemma gcd_dvd_lcm [simp]: "gcd a b dvd lcm a b" 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

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

899 

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

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

901 

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

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

904 
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

905 

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

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

908 

63489  909 
lemma lcm_proj1_if_dvd: "b dvd a \<Longrightarrow> lcm a b = normalize a" 
910 
apply (cases "a = 0") 

911 
apply simp 

912 
apply (rule sym) 

913 
apply (rule lcmI) 

914 
apply simp_all 

915 
done 

916 

917 
lemma lcm_proj2_if_dvd: "a dvd b \<Longrightarrow> lcm a b = normalize b" 

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

918 
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

919 

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

921 
proof 
63489  922 
assume *: "lcm m n = normalize m" 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

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

924 
proof (cases "m = 0") 
63489  925 
case True 
926 
then show ?thesis by simp 

927 
next 

928 
case [simp]: False 

929 
from * have **: "m = lcm m n * unit_factor m" 

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

930 
by (simp add: unit_eq_div2) 
63489  931 
show ?thesis by (subst **) simp 
932 
qed 

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

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

934 
assume "n dvd m" 
63489  935 
then show "lcm m n = normalize m" 
936 
by (rule lcm_proj1_if_dvd) 

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

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

938 

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

940 
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

941 

63924  942 
lemma dvd_productE: 
943 
assumes "p dvd (a * b)" 

944 
obtains x y where "p = x * y" "x dvd a" "y dvd b" 

945 
proof (cases "a = 0") 

946 
case True 

947 
thus ?thesis by (intro that[of p 1]) simp_all 

948 
next 

949 
case False 

950 
define x y where "x = gcd a p" and "y = p div x" 

951 
have "p = x * y" by (simp add: x_def y_def) 

952 
moreover have "x dvd a" by (simp add: x_def) 

953 
moreover from assms have "p dvd gcd (b * a) (b * p)" 

954 
by (intro gcd_greatest) (simp_all add: mult.commute) 

955 
hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib) 

956 
with False have "y dvd b" 

957 
by (simp add: x_def y_def div_dvd_iff_mult assms) 

958 
ultimately show ?thesis by (rule that) 

959 
qed 

960 

60686  961 
end 
962 

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

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

965 

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

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

967 
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

968 

63489  969 
lemma gcd_neg1 [simp]: "gcd (a) b = gcd a b" 
970 
by (rule sym, rule gcdI) (simp_all add: gcd_greatest) 

971 

972 
lemma gcd_neg2 [simp]: "gcd a (b) = gcd a b" 

973 
by (rule sym, rule gcdI) (simp_all add: gcd_greatest) 

974 

975 
lemma gcd_neg_numeral_1 [simp]: "gcd ( numeral n) a = gcd (numeral n) a" 

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

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

977 

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

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

980 

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

981 
lemma gcd_diff1: "gcd (m  n) n = gcd m n" 
63489  982 
by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric], subst gcd_add1, simp) 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

983 

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

984 
lemma gcd_diff2: "gcd (n  m) n = gcd m n" 
63489  985 
by (subst gcd_neg1[symmetric]) (simp only: minus_diff_eq gcd_diff1) 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

986 

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

987 
lemma lcm_neg1 [simp]: "lcm (a) b = lcm a b" 
63489  988 
by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff) 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

989 

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

990 
lemma lcm_neg2 [simp]: "lcm a (b) = lcm a b" 
63489  991 
by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff) 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

992 

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

993 
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

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

995 

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

996 
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

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

998 

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

999 
end 
62345  1000 

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

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

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

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

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

60686  1008 
begin 
1009 

63489  1010 
lemma Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}" 
62345  1011 
by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least) 
1012 

63489  1013 
lemma Gcd_Lcm: "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}" 
62345  1014 
by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least) 
1015 

63489  1016 
lemma Gcd_empty [simp]: "Gcd {} = 0" 
60686  1017 
by (rule dvd_0_left, rule Gcd_greatest) simp 
1018 

63489  1019 
lemma Lcm_empty [simp]: "Lcm {} = 1" 
62345  1020 
by (auto intro: associated_eqI Lcm_least) 
1021 

63489  1022 
lemma Gcd_insert [simp]: "Gcd (insert a A) = gcd a (Gcd A)" 
62345  1023 
proof  
1024 
have "Gcd (insert a A) dvd gcd a (Gcd A)" 

1025 
by (auto intro: Gcd_dvd Gcd_greatest) 

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

1027 
proof (rule Gcd_greatest) 

1028 
fix b 

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

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

1031 
proof 

63489  1032 
assume "b = a" 
1033 
then show ?thesis 

1034 
by simp 

62345  1035 
next 
1036 
assume "b \<in> A" 

63489  1037 
then have "Gcd A dvd b" 
1038 
by (rule Gcd_dvd) 

1039 
moreover have "gcd a (Gcd A) dvd Gcd A" 

1040 
by simp 

1041 
ultimately show ?thesis 

1042 
by (blast intro: dvd_trans) 

62345  1043 
qed 
1044 
qed 

1045 
ultimately show ?thesis 

1046 
by (auto intro: associated_eqI) 

1047 
qed 

1048 

63489  1049 
lemma Lcm_insert [simp]: "Lcm (insert a A) = lcm a (Lcm A)" 
62345  1050 
proof (rule sym) 
1051 
have "lcm a (Lcm A) dvd Lcm (insert a A)" 

1052 
by (auto intro: dvd_Lcm Lcm_least) 

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

1054 
proof (rule Lcm_least) 

1055 
fix b 

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

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

1058 
proof 

63489  1059 
assume "b = a" 
1060 
then show ?thesis by simp 

62345  1061 
next 
1062 
assume "b \<in> A" 

63489  1063 
then have "b dvd Lcm A" 
1064 
by (rule dvd_Lcm) 

1065 
moreover have "Lcm A dvd lcm a (Lcm A)" 

1066 
by simp 

1067 
ultimately show ?thesis 

1068 
by (blast intro: dvd_trans) 

62345  1069 
qed 
1070 
qed 

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

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

1073 
qed 

1074 

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

1075 
lemma LcmI: 
63489  1076 
assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b" 
1077 
and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c" 

1078 
and "normalize b = b" 

1079 
shows "b = Lcm A" 

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

1080 
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

1081 

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

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

1084 

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

1086 
apply (rule lcmI) 
63489  1087 
apply (blast intro: Lcm_subset) 
1088 
apply (blast intro: Lcm_subset) 

1089 
apply (intro Lcm_least ballI, elim UnE) 

1090 
apply (rule dvd_trans, erule dvd_Lcm, assumption) 

1091 
apply (rule dvd_trans, erule dvd_Lcm, assumption) 

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

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

1093 
done 
63489  1094 

1095 
lemma Gcd_0_iff [simp]: "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" 

1096 
(is "?P \<longleftrightarrow> ?Q") 

60686  1097 
proof 
1098 
assume ?P 

1099 
show ?Q 

1100 
proof 

1101 
fix a 

1102 
assume "a \<in> A" 

63489  1103 
then have "Gcd A dvd a" 
1104 
by (rule Gcd_dvd) 

1105 
with \<open>?P\<close> have "a = 0" 

1106 
by simp 

1107 
then show "a \<in> {0}" 

1108 
by simp 

60686  1109 
qed 
1110 
next 

1111 
assume ?Q 

1112 
have "0 dvd Gcd A" 

1113 
proof (rule Gcd_greatest) 

1114 
fix a 

1115 
assume "a \<in> A" 

63489  1116 
with \<open>?Q\<close> have "a = 0" 
1117 
by auto 

1118 
then show "0 dvd a" 

1119 
by simp 

60686  1120 
qed 
63489  1121 
then show ?P 
1122 
by simp 

60686  1123 
qed 
1124 

63489  1125 
lemma Lcm_1_iff [simp]: "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)" 
1126 
(is "?P \<longleftrightarrow> ?Q") 

60686  1127 
proof 
1128 
assume ?P 

1129 
show ?Q 

1130 
proof 

1131 
fix a 

1132 
assume "a \<in> A" 

1133 
then have "a dvd Lcm A" 

1134 
by (rule dvd_Lcm) 

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

1136 
by simp 

1137 
qed 

1138 
next 

1139 
assume ?Q 

1140 
then have "is_unit (Lcm A)" 

1141 
by (blast intro: Lcm_least) 

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

1143 
by (rule is_unit_normalize) 

1144 
then show ?P 

1145 
by simp 

1146 
qed 

1147 

63489  1148 
lemma unit_factor_Lcm: "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" 
62345  1149 
proof (cases "Lcm A = 0") 
63489  1150 
case True 
1151 
then show ?thesis 

1152 
by simp 

62345  1153 
next 
1154 
case False 

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

1156 
by blast 

1157 
with False show ?thesis 

1158 
by simp 

1159 
qed 

1160 

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

1161 
lemma unit_factor_Gcd: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" 
63489  1162 
by (simp add: Gcd_Lcm unit_factor_Lcm) 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1163 

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

1164 
lemma GcdI: 
63489  1165 
assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a" 
1166 
and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b" 

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

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

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

1169 
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

1170 

62345  1171 
lemma Gcd_eq_1_I: 
1172 
assumes "is_unit a" and "a \<in> A" 

1173 
shows "Gcd A = 1" 

1174 
proof  

1175 
from assms have "is_unit (Gcd A)" 

1176 
by (blast intro: Gcd_dvd dvd_unit_imp_unit) 

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

1178 
by (rule is_unit_normalize) 

1179 
then show ?thesis 

1180 
by simp 

1181 
qed 

1182 

60686  1183 
lemma Lcm_eq_0_I: 
1184 
assumes "0 \<in> A" 

1185 
shows "Lcm A = 0" 

1186 
proof  

1187 
from assms have "0 dvd Lcm A" 

1188 
by (rule dvd_Lcm) 

1189 
then show ?thesis 

1190 
by simp 

1191 
qed 

1192 

63489  1193 
lemma Gcd_UNIV [simp]: "Gcd UNIV = 1" 
62345  1194 
using dvd_refl by (rule Gcd_eq_1_I) simp 
1195 

63489  1196 
lemma Lcm_UNIV [simp]: "Lcm UNIV = 0" 
61929  1197 
by (rule Lcm_eq_0_I) simp 
60686  1198 

61929  1199 
lemma Lcm_0_iff: 
1200 
assumes "finite A" 

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

1202 
proof (cases "A = {}") 

63489  1203 
case True 
1204 
then show ?thesis by simp 

61929  1205 
next 
63489  1206 
case False 
1207 
with assms show ?thesis 

1208 
by (induct A rule: finite_ne_induct) (auto simp add: lcm_eq_0_iff) 

60686  1209 
qed 
61929  1210 

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

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

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

1213 
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

1214 
by (induct rule: finite.induct[OF \<open>finite A\<close>]) 
63489  1215 
(simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd]) 
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62353
diff
changeset

1216 

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

1217 
lemma Gcd_set [code_unfold]: "Gcd (set as) = foldl gcd 0 as" 
63489  1218 
by (simp add: Gcd_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] 
1219 
foldl_conv_fold gcd.commute) 

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

1220 

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

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

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

1223 
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

1224 
by (induct rule: finite.induct[OF \<open>finite A\<close>]) 
63489  1225 
(simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm]) 
1226 

1227 
lemma Lcm_set [code_unfold]: "Lcm (set as) = foldl lcm 1 as" 

1228 
by (simp add: Lcm_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] 

1229 
foldl_conv_fold lcm.commute) 

1230 

1231 
lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A" 

62345  1232 
proof  
1233 
have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a 

1234 
proof  

63489  1235 
from that obtain B where "A = insert a B" 
1236 
by blast 

62350  1237 
moreover have "gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a" 
62345  1238 
by (rule gcd_dvd1) 
1239 
ultimately show "Gcd (normalize ` A) dvd a" 

1240 
by simp 

1241 
qed 

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

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

1244 
then show ?thesis 

1245 
by (auto intro: associated_eqI) 

1246 
qed 

1247 

62346  1248 
lemma Gcd_eqI: 
1249 
assumes "normalize a = a" 

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

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

1252 
shows "Gcd A = a" 

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

1254 

63489  1255 
lemma dvd_GcdD: "x dvd Gcd A \<Longrightarrow> y \<in> A \<Longrightarrow> x dvd y" 
1256 
using Gcd_dvd dvd_trans by blast 

1257 

1258 
lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)" 

63359  1259 
by (blast dest: dvd_GcdD intro: Gcd_greatest) 
1260 

1261 
lemma Gcd_mult: "Gcd (op * c ` A) = normalize c * Gcd A" 

1262 
proof (cases "c = 0") 

63489  1263 
case True 
1264 
then show ?thesis by auto 

1265 
next 

63359  1266 
case [simp]: False 
1267 
have "Gcd (op * c ` A) div c dvd Gcd A" 

1268 
by (intro Gcd_greatest, subst div_dvd_iff_mult) 

1269 
(auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c]) 

63489  1270 
then have "Gcd (op * c ` A) dvd c * Gcd A" 
63359  1271 
by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac) 
1272 
also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c" 

1273 
by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac) 

1274 
also have "Gcd (op * c ` A) dvd \<dots> \<longleftrightarrow> Gcd (op * c ` A) dvd normalize c * Gcd A" 

1275 
by (simp add: dvd_mult_unit_iff) 

1276 
finally have "Gcd (op * c ` A) dvd normalize c * Gcd A" . 

1277 
moreover have "normalize c * Gcd A dvd Gcd (op * c ` A)" 

1278 
by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd) 

1279 
ultimately have "normalize (Gcd (op * c ` A)) = normalize (normalize c * Gcd A)" 

1280 
by (rule associatedI) 

63489  1281 
then show ?thesis 
1282 
by (simp add: normalize_mult) 

1283 
qed 

63359  1284 

62346  1285 
lemma Lcm_eqI: 
1286 
assumes "normalize a = a" 
