author  nipkow 
Tue, 23 Jun 2009 12:58:53 +0200  
changeset 31766  f767c5b1702e 
parent 31734  a4a79836d07b 
child 31798  fe9a3043d36c 
permissions  rwrr 
31706  1 
(* Title: GCD.thy 
2 
Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, 

3 
Thomas M. Rasmussen, Jeremy Avigad 

4 

5 

6 
This file deals with the functions gcd and lcm, and properties of 

7 
primes. Definitions and lemmas are proved uniformly for the natural 

8 
numbers and integers. 

9 

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

11 

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

13 
and Lawrence C. Paulson, based on \cite{davenport92}. They introduced 

14 
gcd, lcm, and prime for the natural numbers. 

15 

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

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

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

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

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

21 
the natural numbers by Chiaeb. 

22 

21256  23 
*) 
24 

31706  25 

26 
header {* GCD *} 

21256  27 

28 
theory GCD 

31706  29 
imports NatTransfer 
30 
begin 

31 

32 
declare One_nat_def [simp del] 

33 

34 
subsection {* gcd *} 

35 

36 
class gcd = one + 

37 

38 
fixes 

39 
gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and 

40 
lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 

41 

21256  42 
begin 
43 

31706  44 
abbreviation 
45 
coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 

46 
where 

47 
"coprime x y == (gcd x y = 1)" 

48 

49 
end 

50 

51 
class prime = one + 

52 

53 
fixes 

54 
prime :: "'a \<Rightarrow> bool" 

55 

56 

57 
(* definitions for the natural numbers *) 

58 

59 
instantiation nat :: gcd 

60 

61 
begin 

21256  62 

31706  63 
fun 
64 
gcd_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

65 
where 

66 
"gcd_nat x y = 

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

68 

69 
definition 

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

71 
where 

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

73 

74 
instance proof qed 

75 

76 
end 

77 

78 

79 
instantiation nat :: prime 

80 

81 
begin 

21256  82 

21263  83 
definition 
31706  84 
prime_nat :: "nat \<Rightarrow> bool" 
85 
where 

31709  86 
[code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p > m = 1 \<or> m = p))" 
31706  87 

88 
instance proof qed 

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

89 

31706  90 
end 
91 

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

92 

31706  93 
(* definitions for the integers *) 
94 

95 
instantiation int :: gcd 

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

96 

31706  97 
begin 
21256  98 

31706  99 
definition 
100 
gcd_int :: "int \<Rightarrow> int \<Rightarrow> int" 

101 
where 

102 
"gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))" 

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

103 

31706  104 
definition 
105 
lcm_int :: "int \<Rightarrow> int \<Rightarrow> int" 

106 
where 

107 
"lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))" 

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

108 

31706  109 
instance proof qed 
110 

111 
end 

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

112 

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

113 

31706  114 
instantiation int :: prime 
115 

116 
begin 

117 

118 
definition 

119 
prime_int :: "int \<Rightarrow> bool" 

120 
where 

31709  121 
[code del]: "prime_int p = prime (nat p)" 
31706  122 

123 
instance proof qed 

124 

125 
end 

126 

127 

128 
subsection {* Set up Transfer *} 

129 

130 

131 
lemma transfer_nat_int_gcd: 

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

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

134 
"(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x" 

135 
unfolding gcd_int_def lcm_int_def prime_int_def 

136 
by auto 

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

137 

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

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

141 
by (auto simp add: gcd_int_def lcm_int_def) 

142 

143 
declare TransferMorphism_nat_int[transfer add return: 

144 
transfer_nat_int_gcd transfer_nat_int_gcd_closures] 

145 

146 
lemma transfer_int_nat_gcd: 

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

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

149 
"prime (int x) = prime x" 

150 
by (unfold gcd_int_def lcm_int_def prime_int_def, auto) 

151 

152 
lemma transfer_int_nat_gcd_closures: 

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

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

155 
by (auto simp add: gcd_int_def lcm_int_def) 

156 

157 
declare TransferMorphism_int_nat[transfer add return: 

158 
transfer_int_nat_gcd transfer_int_nat_gcd_closures] 

159 

160 

161 

162 
subsection {* GCD *} 

163 

164 
(* was gcd_induct *) 

165 
lemma nat_gcd_induct: 

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

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

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

168 
and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

169 
shows "P m n" 
31706  170 
apply (rule gcd_nat.induct) 
171 
apply (case_tac "y = 0") 

172 
using assms apply simp_all 

173 
done 

174 

175 
(* specific to int *) 

176 

177 
lemma int_gcd_neg1 [simp]: "gcd (x::int) y = gcd x y" 

178 
by (simp add: gcd_int_def) 

179 

180 
lemma int_gcd_neg2 [simp]: "gcd (x::int) (y) = gcd x y" 

181 
by (simp add: gcd_int_def) 

182 

183 
lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)" 

184 
by (simp add: gcd_int_def) 

185 

186 
lemma int_gcd_cases: 

187 
fixes x :: int and y 

188 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)" 

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

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

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

192 
shows "P (gcd x y)" 

193 
by (insert prems, auto simp add: int_gcd_neg1 int_gcd_neg2, arith) 

21256  194 

31706  195 
lemma int_gcd_ge_0 [simp]: "gcd (x::int) y >= 0" 
196 
by (simp add: gcd_int_def) 

197 

198 
lemma int_lcm_neg1: "lcm (x::int) y = lcm x y" 

199 
by (simp add: lcm_int_def) 

200 

201 
lemma int_lcm_neg2: "lcm (x::int) (y) = lcm x y" 

202 
by (simp add: lcm_int_def) 

203 

204 
lemma int_lcm_abs: "lcm (x::int) y = lcm (abs x) (abs y)" 

205 
by (simp add: lcm_int_def) 

21256  206 

31706  207 
lemma int_lcm_cases: 
208 
fixes x :: int and y 

209 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)" 

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

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

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

213 
shows "P (lcm x y)" 

214 
by (insert prems, auto simp add: int_lcm_neg1 int_lcm_neg2, arith) 

215 

216 
lemma int_lcm_ge_0 [simp]: "lcm (x::int) y >= 0" 

217 
by (simp add: lcm_int_def) 

218 

219 
(* was gcd_0, etc. *) 

220 
lemma nat_gcd_0 [simp]: "gcd (x::nat) 0 = x" 

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

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

222 

31706  223 
(* was igcd_0, etc. *) 
224 
lemma int_gcd_0 [simp]: "gcd (x::int) 0 = abs x" 

225 
by (unfold gcd_int_def, auto) 

226 

227 
lemma nat_gcd_0_left [simp]: "gcd 0 (x::nat) = x" 

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

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

229 

31706  230 
lemma int_gcd_0_left [simp]: "gcd 0 (x::int) = abs x" 
231 
by (unfold gcd_int_def, auto) 

232 

233 
lemma nat_gcd_red: "gcd (x::nat) y = gcd y (x mod y)" 

234 
by (case_tac "y = 0", auto) 

235 

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

237 

238 
lemma nat_gcd_non_0: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)" 

239 
by simp 

240 

241 
lemma nat_gcd_1 [simp]: "gcd (m::nat) 1 = 1" 

21263  242 
by simp 
21256  243 

31706  244 
lemma nat_gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" 
245 
by (simp add: One_nat_def) 

246 

247 
lemma int_gcd_1 [simp]: "gcd (m::int) 1 = 1" 

248 
by (simp add: gcd_int_def) 

30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
30042
diff
changeset

249 

31706  250 
lemma nat_gcd_self [simp]: "gcd (x::nat) x = x" 
251 
by simp 

252 

253 
lemma int_gcd_def [simp]: "gcd (x::int) x = abs x" 

254 
by (subst int_gcd_abs, auto simp add: gcd_int_def) 

255 

256 
declare gcd_nat.simps [simp del] 

21256  257 

258 
text {* 

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

262 

31706  263 
lemma nat_gcd_dvd1 [iff]: "(gcd (m::nat)) n dvd m" 
264 
and nat_gcd_dvd2 [iff]: "(gcd m n) dvd n" 

265 
apply (induct m n rule: nat_gcd_induct) 

266 
apply (simp_all add: nat_gcd_non_0) 

21256  267 
apply (blast dest: dvd_mod_imp_dvd) 
31706  268 
done 
269 

270 
thm nat_gcd_dvd1 [transferred] 

271 

272 
lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x" 

273 
apply (subst int_gcd_abs) 

274 
apply (rule dvd_trans) 

275 
apply (rule nat_gcd_dvd1 [transferred]) 

276 
apply auto 

277 
done 

21256  278 

31706  279 
lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y" 
280 
apply (subst int_gcd_abs) 

281 
apply (rule dvd_trans) 

282 
apply (rule nat_gcd_dvd2 [transferred]) 

283 
apply auto 

284 
done 

285 

31730  286 
lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m" 
287 
by(metis nat_gcd_dvd1 dvd_trans) 

288 

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

290 
by(metis nat_gcd_dvd2 dvd_trans) 

291 

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

293 
by(metis int_gcd_dvd1 dvd_trans) 

294 

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

296 
by(metis int_gcd_dvd2 dvd_trans) 

297 

31706  298 
lemma nat_gcd_le1 [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a" 
299 
by (rule dvd_imp_le, auto) 

300 

301 
lemma nat_gcd_le2 [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b" 

302 
by (rule dvd_imp_le, auto) 

303 

304 
lemma int_gcd_le1 [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a" 

305 
by (rule zdvd_imp_le, auto) 

21256  306 

31706  307 
lemma int_gcd_le2 [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b" 
308 
by (rule zdvd_imp_le, auto) 

309 

310 
lemma nat_gcd_greatest: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n" 

311 
by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod) 

312 

313 
lemma int_gcd_greatest: 

314 
assumes "(k::int) dvd m" and "k dvd n" 

315 
shows "k dvd gcd m n" 

316 

317 
apply (subst int_gcd_abs) 

318 
apply (subst abs_dvd_iff [symmetric]) 

319 
apply (rule nat_gcd_greatest [transferred]) 

320 
using prems apply auto 

321 
done 

21256  322 

31706  323 
lemma nat_gcd_greatest_iff [iff]: "(k dvd gcd (m::nat) n) = 
324 
(k dvd m & k dvd n)" 

325 
by (blast intro!: nat_gcd_greatest intro: dvd_trans) 

326 

327 
lemma int_gcd_greatest_iff: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)" 

328 
by (blast intro!: int_gcd_greatest intro: dvd_trans) 

21256  329 

31706  330 
lemma nat_gcd_zero [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)" 
331 
by (simp only: dvd_0_left_iff [symmetric] nat_gcd_greatest_iff) 

21256  332 

31706  333 
lemma int_gcd_zero [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)" 
334 
by (auto simp add: gcd_int_def) 

21256  335 

31706  336 
lemma nat_gcd_pos [simp]: "(gcd (m::nat) n > 0) = (m ~= 0  n ~= 0)" 
337 
by (insert nat_gcd_zero [of m n], arith) 

21256  338 

31706  339 
lemma int_gcd_pos [simp]: "(gcd (m::int) n > 0) = (m ~= 0  n ~= 0)" 
340 
by (insert int_gcd_zero [of m n], insert int_gcd_ge_0 [of m n], arith) 

341 

342 
lemma nat_gcd_commute: "gcd (m::nat) n = gcd n m" 

343 
by (rule dvd_anti_sym, auto) 

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

344 

31706  345 
lemma int_gcd_commute: "gcd (m::int) n = gcd n m" 
346 
by (auto simp add: gcd_int_def nat_gcd_commute) 

347 

348 
lemma nat_gcd_assoc: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)" 

349 
apply (rule dvd_anti_sym) 

350 
apply (blast intro: dvd_trans)+ 

351 
done 

21256  352 

31706  353 
lemma int_gcd_assoc: "gcd (gcd (k::int) m) n = gcd k (gcd m n)" 
354 
by (auto simp add: gcd_int_def nat_gcd_assoc) 

355 

31766  356 
lemmas nat_gcd_left_commute = 
357 
mk_left_commute[of gcd, OF nat_gcd_assoc nat_gcd_commute] 

31706  358 

31766  359 
lemmas int_gcd_left_commute = 
360 
mk_left_commute[of gcd, OF int_gcd_assoc int_gcd_commute] 

31706  361 

362 
lemmas nat_gcd_ac = nat_gcd_assoc nat_gcd_commute nat_gcd_left_commute 

363 
 {* gcd is an ACoperator *} 

21256  364 

31706  365 
lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute 
366 

367 
lemma nat_gcd_1_left [simp]: "gcd (1::nat) m = 1" 

368 
by (subst nat_gcd_commute, simp) 

369 

370 
lemma nat_gcd_Suc_0_left [simp]: "gcd (Suc 0) m = Suc 0" 

371 
by (subst nat_gcd_commute, simp add: One_nat_def) 

372 

373 
lemma int_gcd_1_left [simp]: "gcd (1::int) m = 1" 

374 
by (subst int_gcd_commute, simp) 

21256  375 

31706  376 
lemma nat_gcd_unique: "(d::nat) dvd a \<and> d dvd b \<and> 
377 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 

378 
apply auto 

379 
apply (rule dvd_anti_sym) 

380 
apply (erule (1) nat_gcd_greatest) 

381 
apply auto 

382 
done 

21256  383 

31706  384 
lemma int_gcd_unique: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and> 
385 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 

386 
apply (case_tac "d = 0") 

387 
apply force 

388 
apply (rule iffI) 

389 
apply (rule zdvd_anti_sym) 

390 
apply arith 

391 
apply (subst int_gcd_pos) 

392 
apply clarsimp 

393 
apply (drule_tac x = "d + 1" in spec) 

394 
apply (frule zdvd_imp_le) 

395 
apply (auto intro: int_gcd_greatest) 

396 
done 

30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
30042
diff
changeset

397 

21256  398 
text {* 
399 
\medskip Multiplication laws 

400 
*} 

401 

31706  402 
lemma nat_gcd_mult_distrib: "(k::nat) * gcd m n = gcd (k * m) (k * n)" 
21256  403 
 {* \cite[page 27]{davenport92} *} 
31706  404 
apply (induct m n rule: nat_gcd_induct) 
405 
apply simp 

21256  406 
apply (case_tac "k = 0") 
31706  407 
apply (simp_all add: mod_geq nat_gcd_non_0 mod_mult_distrib2) 
408 
done 

21256  409 

31706  410 
lemma int_gcd_mult_distrib: "abs (k::int) * gcd m n = gcd (k * m) (k * n)" 
411 
apply (subst (1 2) int_gcd_abs) 

412 
apply (simp add: abs_mult) 

413 
apply (rule nat_gcd_mult_distrib [transferred]) 

414 
apply auto 

415 
done 

21256  416 

31706  417 
lemma nat_gcd_mult [simp]: "gcd (k::nat) (k * n) = k" 
418 
by (rule nat_gcd_mult_distrib [of k 1 n, simplified, symmetric]) 

21256  419 

31706  420 
lemma int_gcd_mult [simp]: "gcd (k::int) (k * n) = abs k" 
421 
by (rule int_gcd_mult_distrib [of k 1 n, simplified, symmetric]) 

422 

423 
lemma nat_coprime_dvd_mult: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m" 

424 
apply (insert nat_gcd_mult_distrib [of m k n]) 

21256  425 
apply simp 
426 
apply (erule_tac t = m in ssubst) 

427 
apply simp 

428 
done 

429 

31706  430 
lemma int_coprime_dvd_mult: 
431 
assumes "coprime (k::int) n" and "k dvd m * n" 

432 
shows "k dvd m" 

21256  433 

31706  434 
using prems 
435 
apply (subst abs_dvd_iff [symmetric]) 

436 
apply (subst dvd_abs_iff [symmetric]) 

437 
apply (subst (asm) int_gcd_abs) 

438 
apply (rule nat_coprime_dvd_mult [transferred]) 

439 
apply auto 

440 
apply (subst abs_mult [symmetric], auto) 

441 
done 

442 

443 
lemma nat_coprime_dvd_mult_iff: "coprime (k::nat) n \<Longrightarrow> 

444 
(k dvd m * n) = (k dvd m)" 

445 
by (auto intro: nat_coprime_dvd_mult) 

446 

447 
lemma int_coprime_dvd_mult_iff: "coprime (k::int) n \<Longrightarrow> 

448 
(k dvd m * n) = (k dvd m)" 

449 
by (auto intro: int_coprime_dvd_mult) 

450 

451 
lemma nat_gcd_mult_cancel: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n" 

21256  452 
apply (rule dvd_anti_sym) 
31706  453 
apply (rule nat_gcd_greatest) 
454 
apply (rule_tac n = k in nat_coprime_dvd_mult) 

455 
apply (simp add: nat_gcd_assoc) 

456 
apply (simp add: nat_gcd_commute) 

457 
apply (simp_all add: mult_commute) 

458 
done 

21256  459 

31706  460 
lemma int_gcd_mult_cancel: 
461 
assumes "coprime (k::int) n" 

462 
shows "gcd (k * m) n = gcd m n" 

463 

464 
using prems 

465 
apply (subst (1 2) int_gcd_abs) 

466 
apply (subst abs_mult) 

467 
apply (rule nat_gcd_mult_cancel [transferred]) 

468 
apply (auto simp add: int_gcd_abs [symmetric]) 

469 
done 

21256  470 

471 
text {* \medskip Addition laws *} 

472 

31706  473 
lemma nat_gcd_add1 [simp]: "gcd ((m::nat) + n) n = gcd m n" 
474 
apply (case_tac "n = 0") 

475 
apply (simp_all add: nat_gcd_non_0) 

476 
done 

477 

478 
lemma nat_gcd_add2 [simp]: "gcd (m::nat) (m + n) = gcd m n" 

479 
apply (subst (1 2) nat_gcd_commute) 

480 
apply (subst add_commute) 

481 
apply simp 

482 
done 

483 

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

485 

486 
lemma nat_gcd_diff1: "(m::nat) >= n \<Longrightarrow> gcd (m  n) n = gcd m n" 

487 
by (subst nat_gcd_add1 [symmetric], auto) 

488 

489 
lemma nat_gcd_diff2: "(n::nat) >= m \<Longrightarrow> gcd (n  m) n = gcd m n" 

490 
apply (subst nat_gcd_commute) 

491 
apply (subst nat_gcd_diff1 [symmetric]) 

492 
apply auto 

493 
apply (subst nat_gcd_commute) 

494 
apply (subst nat_gcd_diff1) 

495 
apply assumption 

496 
apply (rule nat_gcd_commute) 

497 
done 

498 

499 
lemma int_gcd_non_0: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)" 

500 
apply (frule_tac b = y and a = x in pos_mod_sign) 

501 
apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib) 

502 
apply (auto simp add: nat_gcd_non_0 nat_mod_distrib [symmetric] 

503 
zmod_zminus1_eq_if) 

504 
apply (frule_tac a = x in pos_mod_bound) 

505 
apply (subst (1 2) nat_gcd_commute) 

506 
apply (simp del: pos_mod_bound add: nat_diff_distrib nat_gcd_diff2 

507 
nat_le_eq_zle) 

508 
done 

21256  509 

31706  510 
lemma int_gcd_red: "gcd (x::int) y = gcd y (x mod y)" 
511 
apply (case_tac "y = 0") 

512 
apply force 

513 
apply (case_tac "y > 0") 

514 
apply (subst int_gcd_non_0, auto) 

515 
apply (insert int_gcd_non_0 [of "y" "x"]) 

516 
apply (auto simp add: int_gcd_neg1 int_gcd_neg2) 

517 
done 

518 

519 
lemma int_gcd_add1 [simp]: "gcd ((m::int) + n) n = gcd m n" 

520 
apply (case_tac "n = 0", force) 

521 
apply (subst (1 2) int_gcd_red) 

522 
apply auto 

523 
done 

524 

525 
lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n" 

526 
apply (subst int_gcd_commute) 

527 
apply (subst add_commute) 

528 
apply (subst int_gcd_add1) 

529 
apply (subst int_gcd_commute) 

530 
apply (rule refl) 

531 
done 

21256  532 

31706  533 
lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n" 
534 
by (induct k, simp_all add: ring_simps) 

21256  535 

31706  536 
lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n" 
537 
apply (subgoal_tac "ALL s. ALL m. ALL n. 

538 
gcd m (int (s::nat) * m + n) = gcd m n") 

539 
apply (case_tac "k >= 0") 

540 
apply (drule_tac x = "nat k" in spec, force) 

541 
apply (subst (1 2) int_gcd_neg2 [symmetric]) 

542 
apply (drule_tac x = "nat ( k)" in spec) 

543 
apply (drule_tac x = "m" in spec) 

544 
apply (drule_tac x = "n" in spec) 

545 
apply auto 

546 
apply (rule nat_induct) 

547 
apply auto 

548 
apply (auto simp add: left_distrib) 

549 
apply (subst add_assoc) 

550 
apply simp 

551 
done 

21256  552 

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

555 

556 
lemma nat_gcd_dvd_prod [iff]: "gcd (m::nat) n dvd k * n" 

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

557 
using mult_dvd_mono [of 1] by auto 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

558 

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

31734  561 
lemma finite_divisors_nat: 
562 
assumes "(m::nat)~= 0" shows "finite{d. d dvd m}" 

563 
proof 

564 
have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite) 

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

566 
by(bestsimp intro!:dvd_imp_le) 

567 
qed 

568 

569 
lemma finite_divisors_int: 

570 
assumes "(i::int) ~= 0" shows "finite{d. d dvd i}" 

571 
proof 

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

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

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

575 
by(bestsimp intro!:dvd_imp_le_int) 

576 
qed 

577 

578 
lemma gcd_is_Max_divisors_nat: 

579 
"m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})" 

580 
apply(rule Max_eqI[THEN sym]) 

581 
apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat) 

582 
apply simp 

583 
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le nat_gcd_greatest_iff nat_gcd_pos) 

584 
apply simp 

585 
done 

586 

587 
lemma gcd_is_Max_divisors_int: 

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

589 
apply(rule Max_eqI[THEN sym]) 

590 
apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int) 

591 
apply simp 

592 
apply (metis int_gcd_greatest_iff int_gcd_pos zdvd_imp_le) 

593 
apply simp 

594 
done 

595 

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

596 

31706  597 
subsection {* Coprimality *} 
598 

599 
lemma nat_div_gcd_coprime [intro]: 

600 
assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0" 

601 
shows "coprime (a div gcd a b) (b div gcd a b)" 

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

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

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

607 
have dvdg: "?g dvd a" "?g dvd b" by simp_all 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

608 
have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all 
22367  609 
from dvdg dvdg' obtain ka kb ka' kb' where 
610 
kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'" 

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

611 
unfolding dvd_def by blast 
31706  612 
then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" 
613 
by simp_all 

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

616 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

31706  617 
have "?g \<noteq> 0" using nz by (simp add: nat_gcd_zero) 
618 
then have gp: "?g > 0" by arith 

619 
from nat_gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . 

22367  620 
with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

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

622 

31706  623 
lemma int_div_gcd_coprime [intro]: 
624 
assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0" 

625 
shows "coprime (a div gcd a b) (b div gcd a b)" 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

626 

31706  627 
apply (subst (1 2 3) int_gcd_abs) 
628 
apply (subst (1 2) abs_div) 

629 
apply auto 

630 
prefer 3 

631 
apply (rule nat_div_gcd_coprime [transferred]) 

632 
using nz apply (auto simp add: int_gcd_abs [symmetric]) 

633 
done 

634 

635 
lemma nat_coprime: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)" 

636 
using nat_gcd_unique[of 1 a b, simplified] by auto 

637 

638 
lemma nat_coprime_Suc_0: 

639 
"coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)" 

640 
using nat_coprime by (simp add: One_nat_def) 

641 

642 
lemma int_coprime: "coprime (a::int) b \<longleftrightarrow> 

643 
(\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)" 

644 
using int_gcd_unique [of 1 a b] 

645 
apply clarsimp 

646 
apply (erule subst) 

647 
apply (rule iffI) 

648 
apply force 

649 
apply (drule_tac x = "abs e" in exI) 

650 
apply (case_tac "e >= 0") 

651 
apply force 

652 
apply force 

653 
done 

654 

655 
lemma nat_gcd_coprime: 

656 
assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and 

657 
b: "b = b' * gcd a b" 

658 
shows "coprime a' b'" 

659 

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

661 
apply (erule ssubst) 

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

663 
apply (erule ssubst) 

664 
apply (rule nat_div_gcd_coprime) 

665 
using prems 

666 
apply force 

667 
apply (subst (1) b) 

668 
using z apply force 

669 
apply (subst (1) a) 

670 
using z apply force 

671 
done 

672 

673 
lemma int_gcd_coprime: 

674 
assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and 

675 
b: "b = b' * gcd a b" 

676 
shows "coprime a' b'" 

677 

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

679 
apply (erule ssubst) 

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

681 
apply (erule ssubst) 

682 
apply (rule int_div_gcd_coprime) 

683 
using prems 

684 
apply force 

685 
apply (subst (1) b) 

686 
using z apply force 

687 
apply (subst (1) a) 

688 
using z apply force 

689 
done 

690 

691 
lemma nat_coprime_mult: assumes da: "coprime (d::nat) a" and db: "coprime d b" 

692 
shows "coprime d (a * b)" 

693 
apply (subst nat_gcd_commute) 

694 
using da apply (subst nat_gcd_mult_cancel) 

695 
apply (subst nat_gcd_commute, assumption) 

696 
apply (subst nat_gcd_commute, rule db) 

697 
done 

698 

699 
lemma int_coprime_mult: assumes da: "coprime (d::int) a" and db: "coprime d b" 

700 
shows "coprime d (a * b)" 

701 
apply (subst int_gcd_commute) 

702 
using da apply (subst int_gcd_mult_cancel) 

703 
apply (subst int_gcd_commute, assumption) 

704 
apply (subst int_gcd_commute, rule db) 

705 
done 

706 

707 
lemma nat_coprime_lmult: 

708 
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" 

709 
proof  

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

711 
by (rule nat_gcd_greatest, auto) 

712 
with dab show ?thesis 

713 
by auto 

714 
qed 

715 

716 
lemma int_coprime_lmult: 

717 
assumes dab: "coprime (d::int) (a * b)" shows "coprime d a" 

718 
proof  

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

720 
by (rule int_gcd_greatest, auto) 

721 
with dab show ?thesis 

722 
by auto 

723 
qed 

724 

725 
lemma nat_coprime_rmult: 

726 
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d b" 

727 
proof  

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

729 
by (rule nat_gcd_greatest, auto intro: dvd_mult) 

730 
with dab show ?thesis 

731 
by auto 

732 
qed 

733 

734 
lemma int_coprime_rmult: 

735 
assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" 

736 
proof  

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

738 
by (rule int_gcd_greatest, auto intro: dvd_mult) 

739 
with dab show ?thesis 

740 
by auto 

741 
qed 

742 

743 
lemma nat_coprime_mul_eq: "coprime (d::nat) (a * b) \<longleftrightarrow> 

744 
coprime d a \<and> coprime d b" 

745 
using nat_coprime_rmult[of d a b] nat_coprime_lmult[of d a b] 

746 
nat_coprime_mult[of d a b] 

747 
by blast 

748 

749 
lemma int_coprime_mul_eq: "coprime (d::int) (a * b) \<longleftrightarrow> 

750 
coprime d a \<and> coprime d b" 

751 
using int_coprime_rmult[of d a b] int_coprime_lmult[of d a b] 

752 
int_coprime_mult[of d a b] 

753 
by blast 

754 

755 
lemma nat_gcd_coprime_exists: 

756 
assumes nz: "gcd (a::nat) b \<noteq> 0" 

757 
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'" 

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

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

760 
using nz apply (auto simp add: nat_div_gcd_coprime dvd_div_mult) 

761 
done 

762 

763 
lemma int_gcd_coprime_exists: 

764 
assumes nz: "gcd (a::int) b \<noteq> 0" 

765 
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'" 

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

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

768 
using nz apply (auto simp add: int_div_gcd_coprime dvd_div_mult_self) 

769 
done 

770 

771 
lemma nat_coprime_exp: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)" 

772 
by (induct n, simp_all add: nat_coprime_mult) 

773 

774 
lemma int_coprime_exp: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)" 

775 
by (induct n, simp_all add: int_coprime_mult) 

776 

777 
lemma nat_coprime_exp2 [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)" 

778 
apply (rule nat_coprime_exp) 

779 
apply (subst nat_gcd_commute) 

780 
apply (rule nat_coprime_exp) 

781 
apply (subst nat_gcd_commute, assumption) 

782 
done 

783 

784 
lemma int_coprime_exp2 [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)" 

785 
apply (rule int_coprime_exp) 

786 
apply (subst int_gcd_commute) 

787 
apply (rule int_coprime_exp) 

788 
apply (subst int_gcd_commute, assumption) 

789 
done 

790 

791 
lemma nat_gcd_exp: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n" 

792 
proof (cases) 

793 
assume "a = 0 & b = 0" 

794 
thus ?thesis by simp 

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

796 
hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)" 

797 
by auto 

798 
hence "gcd ((a div gcd a b)^n * (gcd a b)^n) 

799 
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" 

800 
apply (subst (1 2) mult_commute) 

801 
apply (subst nat_gcd_mult_distrib [symmetric]) 

802 
apply simp 

803 
done 

804 
also have "(a div gcd a b)^n * (gcd a b)^n = a^n" 

805 
apply (subst div_power) 

806 
apply auto 

807 
apply (rule dvd_div_mult_self) 

808 
apply (rule dvd_power_same) 

809 
apply auto 

810 
done 

811 
also have "(b div gcd a b)^n * (gcd a b)^n = b^n" 

812 
apply (subst div_power) 

813 
apply auto 

814 
apply (rule dvd_div_mult_self) 

815 
apply (rule dvd_power_same) 

816 
apply auto 

817 
done 

818 
finally show ?thesis . 

819 
qed 

820 

821 
lemma int_gcd_exp: "gcd ((a::int)^n) (b^n) = (gcd a b)^n" 

822 
apply (subst (1 2) int_gcd_abs) 

823 
apply (subst (1 2) power_abs) 

824 
apply (rule nat_gcd_exp [where n = n, transferred]) 

825 
apply auto 

826 
done 

827 

828 
lemma nat_coprime_divprod: "(d::nat) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b" 

829 
using nat_coprime_dvd_mult_iff[of d a b] 

830 
by (auto simp add: mult_commute) 

831 

832 
lemma int_coprime_divprod: "(d::int) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b" 

833 
using int_coprime_dvd_mult_iff[of d a b] 

834 
by (auto simp add: mult_commute) 

835 

836 
lemma nat_division_decomp: assumes dc: "(a::nat) dvd b * c" 

837 
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c" 

838 
proof 

839 
let ?g = "gcd a b" 

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

841 
moreover 

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

843 
from nat_gcd_coprime_exists[OF z] 

844 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 

845 
by blast 

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

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

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

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

850 
hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc) 

851 
with z have th_1: "a' dvd b' * c" by auto 

852 
from nat_coprime_dvd_mult[OF ab'(3)] th_1 

853 
have thc: "a' dvd c" by (subst (asm) mult_commute, blast) 

854 
from ab' have "a = ?g*a'" by algebra 

855 
with thb thc have ?thesis by blast } 

856 
ultimately show ?thesis by blast 

857 
qed 

858 

859 
lemma int_division_decomp: assumes dc: "(a::int) dvd b * c" 

860 
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c" 

861 
proof 

862 
let ?g = "gcd a b" 

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

864 
moreover 

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

866 
from int_gcd_coprime_exists[OF z] 

867 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 

868 
by blast 

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

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

871 
with dc have th0: "a' dvd b*c" 

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

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

874 
hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc) 

875 
with z have th_1: "a' dvd b' * c" by auto 

876 
from int_coprime_dvd_mult[OF ab'(3)] th_1 

877 
have thc: "a' dvd c" by (subst (asm) mult_commute, blast) 

878 
from ab' have "a = ?g*a'" by algebra 

879 
with thb thc have ?thesis by blast } 

880 
ultimately show ?thesis by blast 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

881 
qed 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

882 

31706  883 
lemma nat_pow_divides_pow: 
884 
assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0" 

885 
shows "a dvd b" 

886 
proof 

887 
let ?g = "gcd a b" 

888 
from n obtain m where m: "n = Suc m" by (cases n, simp_all) 

889 
{assume "?g = 0" with ab n have ?thesis by auto } 

890 
moreover 

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

892 
hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv) 

893 
from nat_gcd_coprime_exists[OF z] 

894 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 

895 
by blast 

896 
from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n" 

897 
by (simp add: ab'(1,2)[symmetric]) 

898 
hence "?g^n*a'^n dvd ?g^n *b'^n" 

899 
by (simp only: power_mult_distrib mult_commute) 

900 
with zn z n have th0:"a'^n dvd b'^n" by auto 

901 
have "a' dvd a'^n" by (simp add: m) 

902 
with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp 

903 
hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute) 

904 
from nat_coprime_dvd_mult[OF nat_coprime_exp [OF ab'(3), of m]] th1 

905 
have "a' dvd b'" by (subst (asm) mult_commute, blast) 

906 
hence "a'*?g dvd b'*?g" by simp 

907 
with ab'(1,2) have ?thesis by simp } 

908 
ultimately show ?thesis by blast 

909 
qed 

910 

911 
lemma int_pow_divides_pow: 

912 
assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0" 

913 
shows "a dvd b" 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

914 
proof 
31706  915 
let ?g = "gcd a b" 
916 
from n obtain m where m: "n = Suc m" by (cases n, simp_all) 

917 
{assume "?g = 0" with ab n have ?thesis by auto } 

918 
moreover 

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

920 
hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv) 

921 
from int_gcd_coprime_exists[OF z] 

922 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 

923 
by blast 

924 
from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n" 

925 
by (simp add: ab'(1,2)[symmetric]) 

926 
hence "?g^n*a'^n dvd ?g^n *b'^n" 

927 
by (simp only: power_mult_distrib mult_commute) 

928 
with zn z n have th0:"a'^n dvd b'^n" by auto 

929 
have "a' dvd a'^n" by (simp add: m) 

930 
with th0 have "a' dvd b'^n" 

931 
using dvd_trans[of a' "a'^n" "b'^n"] by simp 

932 
hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute) 

933 
from int_coprime_dvd_mult[OF int_coprime_exp [OF ab'(3), of m]] th1 

934 
have "a' dvd b'" by (subst (asm) mult_commute, blast) 

935 
hence "a'*?g dvd b'*?g" by simp 

936 
with ab'(1,2) have ?thesis by simp } 

937 
ultimately show ?thesis by blast 

938 
qed 

939 

940 
lemma nat_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)" 

941 
by (auto intro: nat_pow_divides_pow dvd_power_same) 

942 

943 
lemma int_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)" 

944 
by (auto intro: int_pow_divides_pow dvd_power_same) 

945 

946 
lemma nat_divides_mult: 

947 
assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n" 

948 
shows "m * n dvd r" 

949 
proof 

950 
from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'" 

951 
unfolding dvd_def by blast 

952 
from mr n' have "m dvd n'*n" by (simp add: mult_commute) 

953 
hence "m dvd n'" using nat_coprime_dvd_mult_iff[OF mn] by simp 

954 
then obtain k where k: "n' = m*k" unfolding dvd_def by blast 

955 
from n' k show ?thesis unfolding dvd_def by auto 

956 
qed 

957 

958 
lemma int_divides_mult: 

959 
assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n" 

960 
shows "m * n dvd r" 

961 
proof 

962 
from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'" 

963 
unfolding dvd_def by blast 

964 
from mr n' have "m dvd n'*n" by (simp add: mult_commute) 

965 
hence "m dvd n'" using int_coprime_dvd_mult_iff[OF mn] by simp 

966 
then obtain k where k: "n' = m*k" unfolding dvd_def by blast 

967 
from n' k show ?thesis unfolding dvd_def by auto 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

968 
qed 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

969 

31706  970 
lemma nat_coprime_plus_one [simp]: "coprime ((n::nat) + 1) n" 
971 
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1  n)") 

972 
apply force 

973 
apply (rule nat_dvd_diff) 

974 
apply auto 

975 
done 

976 

977 
lemma nat_coprime_Suc [simp]: "coprime (Suc n) n" 

978 
using nat_coprime_plus_one by (simp add: One_nat_def) 

979 

980 
lemma int_coprime_plus_one [simp]: "coprime ((n::int) + 1) n" 

981 
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1  n)") 

982 
apply force 

983 
apply (rule dvd_diff) 

984 
apply auto 

985 
done 

986 

987 
lemma nat_coprime_minus_one: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n  1) n" 

988 
using nat_coprime_plus_one [of "n  1"] 

989 
nat_gcd_commute [of "n  1" n] by auto 

990 

991 
lemma int_coprime_minus_one: "coprime ((n::int)  1) n" 

992 
using int_coprime_plus_one [of "n  1"] 

993 
int_gcd_commute [of "n  1" n] by auto 

994 

995 
lemma nat_setprod_coprime [rule_format]: 

996 
"(ALL i: A. coprime (f i) (x::nat)) > coprime (PROD i:A. f i) x" 

997 
apply (case_tac "finite A") 

998 
apply (induct set: finite) 

999 
apply (auto simp add: nat_gcd_mult_cancel) 

1000 
done 

1001 

1002 
lemma int_setprod_coprime [rule_format]: 

1003 
"(ALL i: A. coprime (f i) (x::int)) > coprime (PROD i:A. f i) x" 

1004 
apply (case_tac "finite A") 

1005 
apply (induct set: finite) 

1006 
apply (auto simp add: int_gcd_mult_cancel) 

1007 
done 

1008 

1009 
lemma nat_prime_odd: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" 

1010 
unfolding prime_nat_def 

1011 
apply (subst even_mult_two_ex) 

1012 
apply clarify 

1013 
apply (drule_tac x = 2 in spec) 

1014 
apply auto 

1015 
done 

1016 

1017 
lemma int_prime_odd: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" 

1018 
unfolding prime_int_def 

1019 
apply (frule nat_prime_odd) 

1020 
apply (auto simp add: even_nat_def) 

1021 
done 

1022 

1023 
lemma nat_coprime_common_divisor: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> 

1024 
x dvd b \<Longrightarrow> x = 1" 

1025 
apply (subgoal_tac "x dvd gcd a b") 

1026 
apply simp 

1027 
apply (erule (1) nat_gcd_greatest) 

1028 
done 

1029 

1030 
lemma int_coprime_common_divisor: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> 

1031 
x dvd b \<Longrightarrow> abs x = 1" 

1032 
apply (subgoal_tac "x dvd gcd a b") 

1033 
apply simp 

1034 
apply (erule (1) int_gcd_greatest) 

1035 
done 

1036 

1037 
lemma nat_coprime_divisors: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> 

1038 
coprime d e" 

1039 
apply (auto simp add: dvd_def) 

1040 
apply (frule int_coprime_lmult) 

1041 
apply (subst int_gcd_commute) 

1042 
apply (subst (asm) (2) int_gcd_commute) 

1043 
apply (erule int_coprime_lmult) 

1044 
done 

1045 

1046 
lemma nat_invertible_coprime: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m" 

1047 
apply (metis nat_coprime_lmult nat_gcd_1 nat_gcd_commute nat_gcd_red) 

1048 
done 

1049 

1050 
lemma int_invertible_coprime: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m" 

1051 
apply (metis int_coprime_lmult int_gcd_1 int_gcd_commute int_gcd_red) 

1052 
done 

1053 

1054 

1055 
subsection {* Bezout's theorem *} 

1056 

1057 
(* Function bezw returns a pair of witnesses to Bezout's theorem  

1058 
see the theorems that follow the definition. *) 

1059 
fun 

1060 
bezw :: "nat \<Rightarrow> nat \<Rightarrow> int * int" 

1061 
where 

1062 
"bezw x y = 

1063 
(if y = 0 then (1, 0) else 

1064 
(snd (bezw y (x mod y)), 

1065 
fst (bezw y (x mod y))  snd (bezw y (x mod y)) * int(x div y)))" 

1066 

1067 
lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp 

1068 

1069 
lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)), 

1070 
fst (bezw y (x mod y))  snd (bezw y (x mod y)) * int(x div y))" 

1071 
by simp 

1072 

1073 
declare bezw.simps [simp del] 

1074 

1075 
lemma bezw_aux [rule_format]: 

1076 
"fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)" 

1077 
proof (induct x y rule: nat_gcd_induct) 

1078 
fix m :: nat 

1079 
show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)" 

1080 
by auto 

1081 
next fix m :: nat and n 

1082 
assume ngt0: "n > 0" and 

1083 
ih: "fst (bezw n (m mod n)) * int n + 

1084 
snd (bezw n (m mod n)) * int (m mod n) = 

1085 
int (gcd n (m mod n))" 

1086 
thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)" 

1087 
apply (simp add: bezw_non_0 nat_gcd_non_0) 

1088 
apply (erule subst) 

1089 
apply (simp add: ring_simps) 

1090 
apply (subst mod_div_equality [of m n, symmetric]) 

1091 
(* applying simp here undoes the last substitution! 

1092 
what is procedure cancel_div_mod? *) 

1093 
apply (simp only: ring_simps zadd_int [symmetric] 

1094 
zmult_int [symmetric]) 

1095 
done 

1096 
qed 

1097 

1098 
lemma int_bezout: 

1099 
fixes x y 

1100 
shows "EX u v. u * (x::int) + v * y = gcd x y" 

1101 
proof  

1102 
have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow> 

1103 
EX u v. u * x + v * y = gcd x y" 

1104 
apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI) 

1105 
apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI) 

1106 
apply (unfold gcd_int_def) 

1107 
apply simp 

1108 
apply (subst bezw_aux [symmetric]) 

1109 
apply auto 

1110 
done 

1111 
have "(x \<ge> 0 \<and> y \<ge> 0)  (x \<ge> 0 \<and> y \<le> 0)  (x \<le> 0 \<and> y \<ge> 0)  

1112 
(x \<le> 0 \<and> y \<le> 0)" 

1113 
by auto 

1114 
moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis" 

1115 
by (erule (1) bezout_aux) 

1116 
moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis" 

1117 
apply (insert bezout_aux [of x "y"]) 

1118 
apply auto 

1119 
apply (rule_tac x = u in exI) 

1120 
apply (rule_tac x = "v" in exI) 

1121 
apply (subst int_gcd_neg2 [symmetric]) 

1122 
apply auto 

1123 
done 

1124 
moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis" 

1125 
apply (insert bezout_aux [of "x" y]) 

1126 
apply auto 

1127 
apply (rule_tac x = "u" in exI) 

1128 
apply (rule_tac x = v in exI) 

1129 
apply (subst int_gcd_neg1 [symmetric]) 

1130 
apply auto 

1131 
done 

1132 
moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis" 

1133 
apply (insert bezout_aux [of "x" "y"]) 

1134 
apply auto 

1135 
apply (rule_tac x = "u" in exI) 

1136 
apply (rule_tac x = "v" in exI) 

1137 
apply (subst int_gcd_neg1 [symmetric]) 

1138 
apply (subst int_gcd_neg2 [symmetric]) 

1139 
apply auto 

1140 
done 

1141 
ultimately show ?thesis by blast 

1142 
qed 

1143 

1144 
text {* versions of Bezout for nat, by Amine Chaieb *} 

1145 

1146 
lemma ind_euclid: 

1147 
assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 

1148 
and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1149 
shows "P a b" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1150 
proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1151 
fix n a b 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1152 
assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1153 
have "a = b \<or> a < b \<or> b < a" by arith 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1154 
moreover {assume eq: "a= b" 
31706  1155 
from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq 
1156 
by simp} 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1157 
moreover 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1158 
{assume lt: "a < b" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1159 
hence "a + b  a < n \<or> a = 0" using H(2) by arith 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1160 
moreover 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1161 
{assume "a =0" with z c have "P a b" by blast } 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1162 
moreover 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1163 
{assume ab: "a + b  a < n" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1164 
have th0: "a + b  a = a + (b  a)" using lt by arith 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1165 
from add[rule_format, OF H(1)[rule_format, OF ab th0]] 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1166 
have "P a b" by (simp add: th0[symmetric])} 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1167 
ultimately have "P a b" by blast} 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1168 
moreover 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1169 
{assume lt: "a > b" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1170 
hence "b + a  b < n \<or> b = 0" using H(2) by arith 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1171 
moreover 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1172 
{assume "b =0" with z c have "P a b" by blast } 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1173 
moreover 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1174 
{assume ab: "b + a  b < n" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1175 
have th0: "b + a  b = b + (a  b)" using lt by arith 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1176 
from add[rule_format, OF H(1)[rule_format, OF ab th0]] 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1177 
have "P b a" by (simp add: th0[symmetric]) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1178 
hence "P a b" using c by blast } 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1179 
ultimately have "P a b" by blast} 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1180 
ultimately show "P a b" by blast 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1181 
qed 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1182 

31706  1183 
lemma nat_bezout_lemma: 
1184 
assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> 

1185 
(a * x = b * y + d \<or> b * x = a * y + d)" 

1186 
shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and> 

1187 
(a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)" 

1188 
using ex 

1189 
apply clarsimp 

1190 
apply (rule_tac x="d" in exI, simp add: dvd_add) 

1191 
apply (case_tac "a * x = b * y + d" , simp_all) 

1192 
apply (rule_tac x="x + y" in exI) 

1193 
apply (rule_tac x="y" in exI) 

1194 
apply algebra 

1195 
apply (rule_tac x="x" in exI) 

1196 
apply (rule_tac x="x + y" in exI) 

1197 
apply algebra 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1198 
done 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1199 

31706  1200 
lemma nat_bezout_add: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> 
1201 
(a * x = b * y + d \<or> b * x = a * y + d)" 

1202 
apply(induct a b rule: ind_euclid) 

1203 
apply blast 

1204 
apply clarify 

1205 
apply (rule_tac x="a" in exI, simp add: dvd_add) 

1206 
apply clarsimp 

1207 
apply (rule_tac x="d" in exI) 

1208 
apply (case_tac "a * x = b * y + d", simp_all add: dvd_add) 

1209 
apply (rule_tac x="x+y" in exI) 

1210 
apply (rule_tac x="y" in exI) 

1211 
apply algebra 

1212 
apply (rule_tac x="x" in exI) 

1213 
apply (rule_tac x="x+y" in exI) 

1214 
apply algebra 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1215 
done 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1216 

31706  1217 
lemma nat_bezout1: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> 
1218 
(a * x  b * y = d \<or> b * x  a * y = d)" 

1219 
using nat_bezout_add[of a b] 

1220 
apply clarsimp 

1221 
apply (rule_tac x="d" in exI, simp) 

1222 
apply (rule_tac x="x" in exI) 

1223 
apply (rule_tac x="y" in exI) 

1224 
apply auto 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1225 
done 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1226 

31706  1227 
lemma nat_bezout_add_strong: assumes nz: "a \<noteq> (0::nat)" 
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1228 
shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1229 
proof 
31706  1230 
from nz have ap: "a > 0" by simp 
1231 
from nat_bezout_add[of a b] 

1232 
have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or> 

1233 
(\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1234 
moreover 
31706  1235 
{fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d" 
1236 
from H have ?thesis by blast } 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1237 
moreover 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1238 
{fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1239 
{assume b0: "b = 0" with H have ?thesis by simp} 
31706  1240 
moreover 
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1241 
{assume b: "b \<noteq> 0" hence bp: "b > 0" by simp 
31706  1242 
from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b" 
1243 
by auto 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1244 
moreover 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1245 
{assume db: "d=b" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1246 
from prems have ?thesis apply simp 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1247 
apply (rule exI[where x = b], simp) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1248 
apply (rule exI[where x = b]) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1249 
by (rule exI[where x = "a  1"], simp add: diff_mult_distrib2)} 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1250 
moreover 
31706  1251 
{assume db: "d < b" 
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1252 
{assume "x=0" hence ?thesis using prems by simp } 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1253 
moreover 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1254 
{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1255 
from db have "d \<le> b  1" by simp 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1256 
hence "d*b \<le> b*(b  1)" by simp 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1257 
with xp mult_mono[of "1" "x" "d*b" "b*(b  1)"] 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1258 
have dble: "d*b \<le> x*b*(b  1)" using bp by simp 
31706  1259 
from H (3) have "d + (b  1) * (b*x) = d + (b  1) * (a*y + d)" 
1260 
by simp 

1261 
hence "d + (b  1) * a * y + (b  1) * d = d + (b  1) * b * x" 

1262 
by (simp only: mult_assoc right_distrib) 

1263 
hence "a * ((b  1) * y) + d * (b  1 + 1) = d + x*b*(b  1)" 

1264 
by algebra 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1265 
hence "a * ((b  1) * y) = d + x*b*(b  1)  d*b" using bp by simp 
31706  1266 
hence "a * ((b  1) * y) = d + (x*b*(b  1)  d*b)" 
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1267 
by (simp only: diff_add_assoc[OF dble, of d, symmetric]) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1268 
hence "a * ((b  1) * y) = b*(x*(b  1)  d) + d" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1269 
by (simp only: diff_mult_distrib2 add_commute mult_ac) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1270 
hence ?thesis using H(1,2) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1271 
apply  
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1272 
apply (rule exI[where x=d], simp) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1273 
apply (rule exI[where x="(b  1) * y"]) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1274 
by (rule exI[where x="x*(b  1)  d"], simp)} 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1275 
ultimately have ?thesis by blast} 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1276 
ultimately have ?thesis by blast} 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1277 
ultimately have ?thesis by blast} 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1278 
ultimately show ?thesis by blast 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1279 
qed 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1280 

31706  1281 
lemma nat_bezout: assumes a: "(a::nat) \<noteq> 0" 
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1282 
shows "\<exists>x y. a * x = b * y + gcd a b" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1283 
proof 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1284 
let ?g = "gcd a b" 
31706  1285 
from nat_bezout_add_strong[OF a, of b] 
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1286 
obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1287 
from d(1,2) have "d dvd ?g" by simp 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1288 
then obtain k where k: "?g = d*k" unfolding dvd_def by blast 
31706  1289 
from d(3) have "a * x * k = (b * y + d) *k " by auto 
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1290 
hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1291 
thus ?thesis by blast 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1292 
qed 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1293 

31706  1294 

1295 
subsection {* LCM *} 

1296 

1297 
lemma int_lcm_altdef: "lcm (a::int) b = (abs a) * (abs b) div gcd a b" 

1298 
by (simp add: lcm_int_def lcm_nat_def zdiv_int 

1299 
zmult_int [symmetric] gcd_int_def) 

1300 

1301 
lemma nat_prod_gcd_lcm: "(m::nat) * n = gcd m n * lcm m n" 

1302 
unfolding lcm_nat_def 

1303 
by (simp add: dvd_mult_div_cancel [OF nat_gcd_dvd_prod]) 

1304 

1305 
lemma int_prod_gcd_lcm: "abs(m::int) * abs n = gcd m n * lcm m n" 

1306 
unfolding lcm_int_def gcd_int_def 

1307 
apply (subst int_mult [symmetric]) 

1308 
apply (subst nat_prod_gcd_lcm [symmetric]) 

1309 
apply (subst nat_abs_mult_distrib [symmetric]) 

1310 
apply (simp, simp add: abs_mult) 

1311 
done 

1312 

1313 
lemma nat_lcm_0 [simp]: "lcm (m::nat) 0 = 0" 

1314 
unfolding lcm_nat_def by simp 

1315 

1316 
lemma int_lcm_0 [simp]: "lcm (m::int) 0 = 0" 

1317 
unfolding lcm_int_def by simp 

1318 

1319 
lemma nat_lcm_1 [simp]: "lcm (m::nat) 1 = m" 

1320 
unfolding lcm_nat_def by simp 

1321 

1322 
lemma nat_lcm_Suc_0 [simp]: "lcm (m::nat) (Suc 0) = m" 

1323 
unfolding lcm_nat_def by (simp add: One_nat_def) 

1324 

1325 
lemma int_lcm_1 [simp]: "lcm (m::int) 1 = abs m" 

1326 
unfolding lcm_int_def by simp 

1327 

1328 
lemma nat_lcm_0_left [simp]: "lcm (0::nat) n = 0" 

1329 
unfolding lcm_nat_def by simp 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1330 

31706  1331 
lemma int_lcm_0_left [simp]: "lcm (0::int) n = 0" 
1332 
unfolding lcm_int_def by simp 

1333 

1334 
lemma nat_lcm_1_left [simp]: "lcm (1::nat) m = m" 

1335 
unfolding lcm_nat_def by simp 

1336 

1337 
lemma nat_lcm_Suc_0_left [simp]: "lcm (Suc 0) m = m" 

1338 
unfolding lcm_nat_def by (simp add: One_nat_def) 

1339 

1340 
lemma int_lcm_1_left [simp]: "lcm (1::int) m = abs m" 

1341 
unfolding lcm_int_def by simp 

1342 

1343 
lemma nat_lcm_commute: "lcm (m::nat) n = lcm n m" 

1344 
unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps) 

1345 

1346 
lemma int_lcm_commute: "lcm (m::int) n = lcm n m" 

1347 
unfolding lcm_int_def by (subst nat_lcm_commute, rule refl) 

1348 

1349 

1350 
lemma nat_lcm_pos: 

1351 
assumes mpos: "(m::nat) > 0" 

1352 
and npos: "n>0" 

1353 
shows "lcm m n > 0" 

1354 
proof(rule ccontr, simp add: lcm_nat_def nat_gcd_zero) 

1355 
assume h:"m*n div gcd m n = 0" 

1356 
from mpos npos have "gcd m n \<noteq> 0" using nat_gcd_zero by simp 

1357 
hence gcdp: "gcd m n > 0" by simp 

1358 
with h 

1359 
have "m*n < gcd m n" 

1360 
by (cases "m * n < gcd m n") 

1361 
(auto simp add: div_if[OF gcdp, where m="m*n"]) 

27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1362 
moreover 
31706  1363 
have "gcd m n dvd m" by simp 
1364 
with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp 

1365 
with npos have t1:"gcd m n*n \<le> m*n" by simp 
