author  nipkow 
Sat, 20 Jun 2009 13:34:54 +0200  
changeset 31730  d74830dc3e4a 
parent 31729  b9299916d618 
child 31734  a4a79836d07b 
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 

356 
lemma nat_gcd_left_commute: "gcd (k::nat) (gcd m n) = gcd m (gcd k n)" 

357 
apply (rule nat_gcd_commute [THEN trans]) 

358 
apply (rule nat_gcd_assoc [THEN trans]) 

359 
apply (rule nat_gcd_commute [THEN arg_cong]) 

360 
done 

361 

362 
lemma int_gcd_left_commute: "gcd (k::int) (gcd m n) = gcd m (gcd k n)" 

363 
apply (rule int_gcd_commute [THEN trans]) 

364 
apply (rule int_gcd_assoc [THEN trans]) 

365 
apply (rule int_gcd_commute [THEN arg_cong]) 

366 
done 

367 

368 
lemmas nat_gcd_ac = nat_gcd_assoc nat_gcd_commute nat_gcd_left_commute 

369 
 {* gcd is an ACoperator *} 

21256  370 

31706  371 
lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute 
372 

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

374 
by (subst nat_gcd_commute, simp) 

375 

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

377 
by (subst nat_gcd_commute, simp add: One_nat_def) 

378 

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

380 
by (subst int_gcd_commute, simp) 

21256  381 

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

384 
apply auto 

385 
apply (rule dvd_anti_sym) 

386 
apply (erule (1) nat_gcd_greatest) 

387 
apply auto 

388 
done 

21256  389 

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

392 
apply (case_tac "d = 0") 

393 
apply force 

394 
apply (rule iffI) 

395 
apply (rule zdvd_anti_sym) 

396 
apply arith 

397 
apply (subst int_gcd_pos) 

398 
apply clarsimp 

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

400 
apply (frule zdvd_imp_le) 

401 
apply (auto intro: int_gcd_greatest) 

402 
done 

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

403 

21256  404 
text {* 
405 
\medskip Multiplication laws 

406 
*} 

407 

31706  408 
lemma nat_gcd_mult_distrib: "(k::nat) * gcd m n = gcd (k * m) (k * n)" 
21256  409 
 {* \cite[page 27]{davenport92} *} 
31706  410 
apply (induct m n rule: nat_gcd_induct) 
411 
apply simp 

21256  412 
apply (case_tac "k = 0") 
31706  413 
apply (simp_all add: mod_geq nat_gcd_non_0 mod_mult_distrib2) 
414 
done 

21256  415 

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

418 
apply (simp add: abs_mult) 

419 
apply (rule nat_gcd_mult_distrib [transferred]) 

420 
apply auto 

421 
done 

21256  422 

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

21256  425 

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

428 

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

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

21256  431 
apply simp 
432 
apply (erule_tac t = m in ssubst) 

433 
apply simp 

434 
done 

435 

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

438 
shows "k dvd m" 

21256  439 

31706  440 
using prems 
441 
apply (subst abs_dvd_iff [symmetric]) 

442 
apply (subst dvd_abs_iff [symmetric]) 

443 
apply (subst (asm) int_gcd_abs) 

444 
apply (rule nat_coprime_dvd_mult [transferred]) 

445 
apply auto 

446 
apply (subst abs_mult [symmetric], auto) 

447 
done 

448 

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

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

451 
by (auto intro: nat_coprime_dvd_mult) 

452 

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

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

455 
by (auto intro: int_coprime_dvd_mult) 

456 

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

21256  458 
apply (rule dvd_anti_sym) 
31706  459 
apply (rule nat_gcd_greatest) 
460 
apply (rule_tac n = k in nat_coprime_dvd_mult) 

461 
apply (simp add: nat_gcd_assoc) 

462 
apply (simp add: nat_gcd_commute) 

463 
apply (simp_all add: mult_commute) 

464 
done 

21256  465 

31706  466 
lemma int_gcd_mult_cancel: 
467 
assumes "coprime (k::int) n" 

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

469 

470 
using prems 

471 
apply (subst (1 2) int_gcd_abs) 

472 
apply (subst abs_mult) 

473 
apply (rule nat_gcd_mult_cancel [transferred]) 

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

475 
done 

21256  476 

477 
text {* \medskip Addition laws *} 

478 

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

481 
apply (simp_all add: nat_gcd_non_0) 

482 
done 

483 

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

485 
apply (subst (1 2) nat_gcd_commute) 

486 
apply (subst add_commute) 

487 
apply simp 

488 
done 

489 

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

491 

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

493 
by (subst nat_gcd_add1 [symmetric], auto) 

494 

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

496 
apply (subst nat_gcd_commute) 

497 
apply (subst nat_gcd_diff1 [symmetric]) 

498 
apply auto 

499 
apply (subst nat_gcd_commute) 

500 
apply (subst nat_gcd_diff1) 

501 
apply assumption 

502 
apply (rule nat_gcd_commute) 

503 
done 

504 

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

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

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

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

509 
zmod_zminus1_eq_if) 

510 
apply (frule_tac a = x in pos_mod_bound) 

511 
apply (subst (1 2) nat_gcd_commute) 

512 
apply (simp del: pos_mod_bound add: nat_diff_distrib nat_gcd_diff2 

513 
nat_le_eq_zle) 

514 
done 

21256  515 

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

518 
apply force 

519 
apply (case_tac "y > 0") 

520 
apply (subst int_gcd_non_0, auto) 

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

522 
apply (auto simp add: int_gcd_neg1 int_gcd_neg2) 

523 
done 

524 

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

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

527 
apply (subst (1 2) int_gcd_red) 

528 
apply auto 

529 
done 

530 

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

532 
apply (subst int_gcd_commute) 

533 
apply (subst add_commute) 

534 
apply (subst int_gcd_add1) 

535 
apply (subst int_gcd_commute) 

536 
apply (rule refl) 

537 
done 

21256  538 

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

21256  541 

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

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

545 
apply (case_tac "k >= 0") 

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

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

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

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

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

551 
apply auto 

552 
apply (rule nat_induct) 

553 
apply auto 

554 
apply (auto simp add: left_distrib) 

555 
apply (subst add_assoc) 

556 
apply simp 

557 
done 

21256  558 

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

561 

562 
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

563 
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

564 

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

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

567 

31706  568 
subsection {* Coprimality *} 
569 

570 
lemma nat_div_gcd_coprime [intro]: 

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

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

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

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

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

578 
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

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

582 
unfolding dvd_def by blast 
31706  583 
then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" 
584 
by simp_all 

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

587 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

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

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

22367  591 
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

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

593 

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

596 
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

597 

31706  598 
apply (subst (1 2 3) int_gcd_abs) 
599 
apply (subst (1 2) abs_div) 

600 
apply auto 

601 
prefer 3 

602 
apply (rule nat_div_gcd_coprime [transferred]) 

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

604 
done 

605 

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

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

608 

609 
lemma nat_coprime_Suc_0: 

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

611 
using nat_coprime by (simp add: One_nat_def) 

612 

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

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

615 
using int_gcd_unique [of 1 a b] 

616 
apply clarsimp 

617 
apply (erule subst) 

618 
apply (rule iffI) 

619 
apply force 

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

621 
apply (case_tac "e >= 0") 

622 
apply force 

623 
apply force 

624 
done 

625 

626 
lemma nat_gcd_coprime: 

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

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

629 
shows "coprime a' b'" 

630 

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

632 
apply (erule ssubst) 

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

634 
apply (erule ssubst) 

635 
apply (rule nat_div_gcd_coprime) 

636 
using prems 

637 
apply force 

638 
apply (subst (1) b) 

639 
using z apply force 

640 
apply (subst (1) a) 

641 
using z apply force 

642 
done 

643 

644 
lemma int_gcd_coprime: 

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

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

647 
shows "coprime a' b'" 

648 

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

650 
apply (erule ssubst) 

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

652 
apply (erule ssubst) 

653 
apply (rule int_div_gcd_coprime) 

654 
using prems 

655 
apply force 

656 
apply (subst (1) b) 

657 
using z apply force 

658 
apply (subst (1) a) 

659 
using z apply force 

660 
done 

661 

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

663 
shows "coprime d (a * b)" 

664 
apply (subst nat_gcd_commute) 

665 
using da apply (subst nat_gcd_mult_cancel) 

666 
apply (subst nat_gcd_commute, assumption) 

667 
apply (subst nat_gcd_commute, rule db) 

668 
done 

669 

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

671 
shows "coprime d (a * b)" 

672 
apply (subst int_gcd_commute) 

673 
using da apply (subst int_gcd_mult_cancel) 

674 
apply (subst int_gcd_commute, assumption) 

675 
apply (subst int_gcd_commute, rule db) 

676 
done 

677 

678 
lemma nat_coprime_lmult: 

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

680 
proof  

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

682 
by (rule nat_gcd_greatest, auto) 

683 
with dab show ?thesis 

684 
by auto 

685 
qed 

686 

687 
lemma int_coprime_lmult: 

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

689 
proof  

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

691 
by (rule int_gcd_greatest, auto) 

692 
with dab show ?thesis 

693 
by auto 

694 
qed 

695 

696 
lemma nat_coprime_rmult: 

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

698 
proof  

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

700 
by (rule nat_gcd_greatest, auto intro: dvd_mult) 

701 
with dab show ?thesis 

702 
by auto 

703 
qed 

704 

705 
lemma int_coprime_rmult: 

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

707 
proof  

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

709 
by (rule int_gcd_greatest, auto intro: dvd_mult) 

710 
with dab show ?thesis 

711 
by auto 

712 
qed 

713 

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

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

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

717 
nat_coprime_mult[of d a b] 

718 
by blast 

719 

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

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

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

723 
int_coprime_mult[of d a b] 

724 
by blast 

725 

726 
lemma nat_gcd_coprime_exists: 

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

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

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

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

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

732 
done 

733 

734 
lemma int_gcd_coprime_exists: 

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

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

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

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

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

740 
done 

741 

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

743 
by (induct n, simp_all add: nat_coprime_mult) 

744 

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

746 
by (induct n, simp_all add: int_coprime_mult) 

747 

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

749 
apply (rule nat_coprime_exp) 

750 
apply (subst nat_gcd_commute) 

751 
apply (rule nat_coprime_exp) 

752 
apply (subst nat_gcd_commute, assumption) 

753 
done 

754 

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

756 
apply (rule int_coprime_exp) 

757 
apply (subst int_gcd_commute) 

758 
apply (rule int_coprime_exp) 

759 
apply (subst int_gcd_commute, assumption) 

760 
done 

761 

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

763 
proof (cases) 

764 
assume "a = 0 & b = 0" 

765 
thus ?thesis by simp 

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

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

768 
by auto 

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

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

771 
apply (subst (1 2) mult_commute) 

772 
apply (subst nat_gcd_mult_distrib [symmetric]) 

773 
apply simp 

774 
done 

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

776 
apply (subst div_power) 

777 
apply auto 

778 
apply (rule dvd_div_mult_self) 

779 
apply (rule dvd_power_same) 

780 
apply auto 

781 
done 

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

783 
apply (subst div_power) 

784 
apply auto 

785 
apply (rule dvd_div_mult_self) 

786 
apply (rule dvd_power_same) 

787 
apply auto 

788 
done 

789 
finally show ?thesis . 

790 
qed 

791 

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

793 
apply (subst (1 2) int_gcd_abs) 

794 
apply (subst (1 2) power_abs) 

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

796 
apply auto 

797 
done 

798 

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

800 
using nat_coprime_dvd_mult_iff[of d a b] 

801 
by (auto simp add: mult_commute) 

802 

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

804 
using int_coprime_dvd_mult_iff[of d a b] 

805 
by (auto simp add: mult_commute) 

806 

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

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

809 
proof 

810 
let ?g = "gcd a b" 

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

812 
moreover 

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

814 
from nat_gcd_coprime_exists[OF z] 

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

816 
by blast 

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

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

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

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

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

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

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

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

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

826 
with thb thc have ?thesis by blast } 

827 
ultimately show ?thesis by blast 

828 
qed 

829 

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

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

832 
proof 

833 
let ?g = "gcd a b" 

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

835 
moreover 

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

837 
from int_gcd_coprime_exists[OF z] 

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

839 
by blast 

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

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

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

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

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

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

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

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

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

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

850 
with thb thc have ?thesis by blast } 

851 
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

852 
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

853 

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

856 
shows "a dvd b" 

857 
proof 

858 
let ?g = "gcd a b" 

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

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

861 
moreover 

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

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

864 
from nat_gcd_coprime_exists[OF z] 

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

866 
by blast 

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

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

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

870 
by (simp only: power_mult_distrib mult_commute) 

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

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

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

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

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

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

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

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

879 
ultimately show ?thesis by blast 

880 
qed 

881 

882 
lemma int_pow_divides_pow: 

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

884 
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

885 
proof 
31706  886 
let ?g = "gcd a b" 
887 
from n obtain m where m: "n = Suc m" by (cases n, simp_all) 

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

889 
moreover 

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

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

892 
from int_gcd_coprime_exists[OF z] 

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

894 
by blast 

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

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

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

898 
by (simp only: power_mult_distrib mult_commute) 

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

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

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

902 
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 int_coprime_dvd_mult[OF int_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 nat_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)" 

912 
by (auto intro: nat_pow_divides_pow dvd_power_same) 

913 

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

915 
by (auto intro: int_pow_divides_pow dvd_power_same) 

916 

917 
lemma nat_divides_mult: 

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

919 
shows "m * n dvd r" 

920 
proof 

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

922 
unfolding dvd_def by blast 

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

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

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

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

927 
qed 

928 

929 
lemma int_divides_mult: 

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

931 
shows "m * n dvd r" 

932 
proof 

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

934 
unfolding dvd_def by blast 

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

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

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

938 
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

939 
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

940 

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

943 
apply force 

944 
apply (rule nat_dvd_diff) 

945 
apply auto 

946 
done 

947 

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

949 
using nat_coprime_plus_one by (simp add: One_nat_def) 

950 

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

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

953 
apply force 

954 
apply (rule dvd_diff) 

955 
apply auto 

956 
done 

957 

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

959 
using nat_coprime_plus_one [of "n  1"] 

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

961 

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

963 
using int_coprime_plus_one [of "n  1"] 

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

965 

966 
lemma nat_setprod_coprime [rule_format]: 

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

968 
apply (case_tac "finite A") 

969 
apply (induct set: finite) 

970 
apply (auto simp add: nat_gcd_mult_cancel) 

971 
done 

972 

973 
lemma int_setprod_coprime [rule_format]: 

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

975 
apply (case_tac "finite A") 

976 
apply (induct set: finite) 

977 
apply (auto simp add: int_gcd_mult_cancel) 

978 
done 

979 

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

981 
unfolding prime_nat_def 

982 
apply (subst even_mult_two_ex) 

983 
apply clarify 

984 
apply (drule_tac x = 2 in spec) 

985 
apply auto 

986 
done 

987 

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

989 
unfolding prime_int_def 

990 
apply (frule nat_prime_odd) 

991 
apply (auto simp add: even_nat_def) 

992 
done 

993 

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

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

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

997 
apply simp 

998 
apply (erule (1) nat_gcd_greatest) 

999 
done 

1000 

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

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

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

1004 
apply simp 

1005 
apply (erule (1) int_gcd_greatest) 

1006 
done 

1007 

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

1009 
coprime d e" 

1010 
apply (auto simp add: dvd_def) 

1011 
apply (frule int_coprime_lmult) 

1012 
apply (subst int_gcd_commute) 

1013 
apply (subst (asm) (2) int_gcd_commute) 

1014 
apply (erule int_coprime_lmult) 

1015 
done 

1016 

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

1018 
apply (metis nat_coprime_lmult nat_gcd_1 nat_gcd_commute nat_gcd_red) 

1019 
done 

1020 

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

1022 
apply (metis int_coprime_lmult int_gcd_1 int_gcd_commute int_gcd_red) 

1023 
done 

1024 

1025 

1026 
subsection {* Bezout's theorem *} 

1027 

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

1029 
see the theorems that follow the definition. *) 

1030 
fun 

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

1032 
where 

1033 
"bezw x y = 

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

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

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

1037 

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

1039 

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

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

1042 
by simp 

1043 

1044 
declare bezw.simps [simp del] 

1045 

1046 
lemma bezw_aux [rule_format]: 

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

1048 
proof (induct x y rule: nat_gcd_induct) 

1049 
fix m :: nat 

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

1051 
by auto 

1052 
next fix m :: nat and n 

1053 
assume ngt0: "n > 0" and 

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

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

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

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

1058 
apply (simp add: bezw_non_0 nat_gcd_non_0) 

1059 
apply (erule subst) 

1060 
apply (simp add: ring_simps) 

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

1062 
(* applying simp here undoes the last substitution! 

1063 
what is procedure cancel_div_mod? *) 

1064 
apply (simp only: ring_simps zadd_int [symmetric] 

1065 
zmult_int [symmetric]) 

1066 
done 

1067 
qed 

1068 

1069 
lemma int_bezout: 

1070 
fixes x y 

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

1072 
proof  

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

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

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

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

1077 
apply (unfold gcd_int_def) 

1078 
apply simp 

1079 
apply (subst bezw_aux [symmetric]) 

1080 
apply auto 

1081 
done 

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

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

1084 
by auto 

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

1086 
by (erule (1) bezout_aux) 

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

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

1089 
apply auto 

1090 
apply (rule_tac x = u in exI) 

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

1092 
apply (subst int_gcd_neg2 [symmetric]) 

1093 
apply auto 

1094 
done 

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

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

1097 
apply auto 

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

1099 
apply (rule_tac x = v in exI) 

1100 
apply (subst int_gcd_neg1 [symmetric]) 

1101 
apply auto 

1102 
done 

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

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

1105 
apply auto 

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

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

1108 
apply (subst int_gcd_neg1 [symmetric]) 

1109 
apply (subst int_gcd_neg2 [symmetric]) 

1110 
apply auto 

1111 
done 

1112 
ultimately show ?thesis by blast 

1113 
qed 

1114 

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

1116 

1117 
lemma ind_euclid: 

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

1119 
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

1120 
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

1121 
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

1122 
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

1123 
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

1124 
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

1125 
moreover {assume eq: "a= b" 
31706  1126 
from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq 
1127 
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

1128 
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

1129 
{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

1130 
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

1131 
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

1132 
{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

1133 
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

1134 
{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

1135 
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

1136 
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

1137 
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

1138 
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

1139 
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

1140 
{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

1141 
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

1142 
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

1143 
{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

1144 
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

1145 
{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

1146 
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

1147 
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

1148 
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

1149 
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

1150 
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

1151 
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

1152 
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

1153 

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

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

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

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

1159 
using ex 

1160 
apply clarsimp 

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

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

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

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

1165 
apply algebra 

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

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

1168 
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

1169 
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

1170 

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

1173 
apply(induct a b rule: ind_euclid) 

1174 
apply blast 

1175 
apply clarify 

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

1177 
apply clarsimp 

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

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

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

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

1182 
apply algebra 

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

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

1185 
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

1186 
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

1187 

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

1190 
using nat_bezout_add[of a b] 

1191 
apply clarsimp 

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

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

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

1195 
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

1196 
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

1197 

31706  1198 
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

1199 
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

1200 
proof 
31706  1201 
from nz have ap: "a > 0" by simp 
1202 
from nat_bezout_add[of a b] 

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

1204 
(\<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

1205 
moreover 
31706  1206 
{fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d" 
1207 
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

1208 
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

1209 
{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

1210 
{assume b0: "b = 0" with H have ?thesis by simp} 
31706  1211 
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

1212 
{assume b: "b \<noteq> 0" hence bp: "b > 0" by simp 
31706  1213 
from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b" 
1214 
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

1215 
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

1216 
{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

1217 
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

1218 
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

1219 
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

1220 
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

1221 
moreover 
31706  1222 
{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

1223 
{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

1224 
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

1225 
{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

1226 
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

1227 
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

1228 
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

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

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

1233 
by (simp only: mult_assoc right_distrib) 

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

1235 
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

1236 
hence "a * ((b  1) * y) = d + x*b*(b  1)  d*b" using bp by simp 
31706  1237 
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

1238 
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

1239 
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

1240 
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

1241 
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

1242 
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

1243 
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

1244 
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

1245 
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

1246 
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

1247 
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

1248 
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

1249 
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

1250 
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

1251 

31706  1252 
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

1253 
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

1254 
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

1255 
let ?g = "gcd a b" 
31706  1256 
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

1257 
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

1258 
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

1259 
then obtain k where k: "?g = d*k" unfolding dvd_def by blast 
31706  1260 
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

1261 
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

1262 
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

1263 
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

1264 

31706  1265 

1266 
subsection {* LCM *} 

1267 

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

1269 
by (simp add: lcm_int_def lcm_nat_def zdiv_int 

1270 
zmult_int [symmetric] gcd_int_def) 

1271 

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

1273 
unfolding lcm_nat_def 

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

1275 

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

1277 
unfolding lcm_int_def gcd_int_def 

1278 
apply (subst int_mult [symmetric]) 

1279 
apply (subst nat_prod_gcd_lcm [symmetric]) 

1280 
apply (subst nat_abs_mult_distrib [symmetric]) 

1281 
apply (simp, simp add: abs_mult) 

1282 
done 

1283 

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

1285 
unfolding lcm_nat_def by simp 

1286 

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

1288 
unfolding lcm_int_def by simp 

1289 

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

1291 
unfolding lcm_nat_def by simp 

1292 

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

1294 
unfolding lcm_nat_def by (simp add: One_nat_def) 

1295 

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

1297 
unfolding lcm_int_def by simp 

1298 

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

1300 
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

1301 

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

1304 

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

1306 
unfolding lcm_nat_def by simp 

1307 

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

1309 
unfolding lcm_nat_def by (simp add: One_nat_def) 

1310 

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

1312 
unfolding lcm_int_def by simp 

1313 

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

1315 
unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps) 

1316 

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

1318 
unfolding lcm_int_def by (subst nat_lcm_commute, rule refl) 

1319 

1320 
(* to do: show lcm is associative, and then declare ac simps *) 

1321 

1322 
lemma nat_lcm_pos: 

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

1324 
and npos: "n>0" 

1325 
shows "lcm m n > 0" 

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

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

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

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

1330 
with h 

1331 
have "m*n < gcd m n" 

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

1333 
(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

1334 
moreover 
31706  1335 
have "gcd m n dvd m" by simp 
1336 
with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp 

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

1338 
have "gcd m n \<le> gcd m n*n" using npos by simp 

1339 
with t1 have "gcd m n \<le> m*n" by arith 

1340 
ultimately show "False" 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

1341 
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

1342 

31706  1343 
lemma int_lcm_pos: 
1344 
assumes mneq0: "(m::int) ~= 0" 

1345 
and npos: "n ~= 0" 

1346 
shows "lcm m n > 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

1347 

31706  1348 
apply (subst int_lcm_abs) 
1349 
apply (rule nat_lcm_pos [transferred]) 

1350 
using prems apply auto 

1351 
done 

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

1352 

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

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

1355 
assumes "n > 0" and "m dvd n" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1356 
shows "m > 0" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1357 
using assms by (cases m) auto 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1358 

31706  1359 
lemma nat_lcm_least: 
1360 
assumes "(m::nat) dvd k" and "n dvd k" 

27556  1361 
shows "lcm m n dvd k" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1362 
proof (cases k) 