author  huffman 
Wed, 17 Jun 2009 16:55:01 0700  
changeset 31706  1db0c8f235fb 
parent 30738  0842e906300c 
child 31709  061f01ee9978 
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 

86 
"prime_nat p = (1 < p \<and> (\<forall>m. m dvd p > m = 1 \<or> m = p))" 

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 

121 
"prime_int p = prime (nat p)" 

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 

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

287 
by (rule dvd_imp_le, auto) 

288 

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

290 
by (rule dvd_imp_le, auto) 

291 

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

293 
by (rule zdvd_imp_le, auto) 

21256  294 

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

297 

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

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

300 

301 
lemma int_gcd_greatest: 

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

303 
shows "k dvd gcd m n" 

304 

305 
apply (subst int_gcd_abs) 

306 
apply (subst abs_dvd_iff [symmetric]) 

307 
apply (rule nat_gcd_greatest [transferred]) 

308 
using prems apply auto 

309 
done 

21256  310 

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

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

314 

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

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

21256  317 

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

21256  320 

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

21256  323 

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

21256  326 

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

329 

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

331 
by (rule dvd_anti_sym, auto) 

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

332 

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

335 

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

337 
apply (rule dvd_anti_sym) 

338 
apply (blast intro: dvd_trans)+ 

339 
done 

21256  340 

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

343 

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

345 
apply (rule nat_gcd_commute [THEN trans]) 

346 
apply (rule nat_gcd_assoc [THEN trans]) 

347 
apply (rule nat_gcd_commute [THEN arg_cong]) 

348 
done 

349 

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

351 
apply (rule int_gcd_commute [THEN trans]) 

352 
apply (rule int_gcd_assoc [THEN trans]) 

353 
apply (rule int_gcd_commute [THEN arg_cong]) 

354 
done 

355 

356 
lemmas nat_gcd_ac = nat_gcd_assoc nat_gcd_commute nat_gcd_left_commute 

357 
 {* gcd is an ACoperator *} 

21256  358 

31706  359 
lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute 
360 

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

362 
by (subst nat_gcd_commute, simp) 

363 

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

365 
by (subst nat_gcd_commute, simp add: One_nat_def) 

366 

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

368 
by (subst int_gcd_commute, simp) 

21256  369 

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

372 
apply auto 

373 
apply (rule dvd_anti_sym) 

374 
apply (erule (1) nat_gcd_greatest) 

375 
apply auto 

376 
done 

21256  377 

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

380 
apply (case_tac "d = 0") 

381 
apply force 

382 
apply (rule iffI) 

383 
apply (rule zdvd_anti_sym) 

384 
apply arith 

385 
apply (subst int_gcd_pos) 

386 
apply clarsimp 

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

388 
apply (frule zdvd_imp_le) 

389 
apply (auto intro: int_gcd_greatest) 

390 
done 

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

391 

21256  392 
text {* 
393 
\medskip Multiplication laws 

394 
*} 

395 

31706  396 
lemma nat_gcd_mult_distrib: "(k::nat) * gcd m n = gcd (k * m) (k * n)" 
21256  397 
 {* \cite[page 27]{davenport92} *} 
31706  398 
apply (induct m n rule: nat_gcd_induct) 
399 
apply simp 

21256  400 
apply (case_tac "k = 0") 
31706  401 
apply (simp_all add: mod_geq nat_gcd_non_0 mod_mult_distrib2) 
402 
done 

21256  403 

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

406 
apply (simp add: abs_mult) 

407 
apply (rule nat_gcd_mult_distrib [transferred]) 

408 
apply auto 

409 
done 

21256  410 

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

21256  413 

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

416 

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

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

21256  419 
apply simp 
420 
apply (erule_tac t = m in ssubst) 

421 
apply simp 

422 
done 

423 

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

426 
shows "k dvd m" 

21256  427 

31706  428 
using prems 
429 
apply (subst abs_dvd_iff [symmetric]) 

430 
apply (subst dvd_abs_iff [symmetric]) 

431 
apply (subst (asm) int_gcd_abs) 

432 
apply (rule nat_coprime_dvd_mult [transferred]) 

433 
apply auto 

434 
apply (subst abs_mult [symmetric], auto) 

435 
done 

436 

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

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

439 
by (auto intro: nat_coprime_dvd_mult) 

440 

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

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

443 
by (auto intro: int_coprime_dvd_mult) 

444 

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

21256  446 
apply (rule dvd_anti_sym) 
31706  447 
apply (rule nat_gcd_greatest) 
448 
apply (rule_tac n = k in nat_coprime_dvd_mult) 

449 
apply (simp add: nat_gcd_assoc) 

450 
apply (simp add: nat_gcd_commute) 

451 
apply (simp_all add: mult_commute) 

452 
done 

21256  453 

31706  454 
lemma int_gcd_mult_cancel: 
455 
assumes "coprime (k::int) n" 

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

457 

458 
using prems 

459 
apply (subst (1 2) int_gcd_abs) 

460 
apply (subst abs_mult) 

461 
apply (rule nat_gcd_mult_cancel [transferred]) 

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

463 
done 

21256  464 

465 
text {* \medskip Addition laws *} 

466 

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

469 
apply (simp_all add: nat_gcd_non_0) 

470 
done 

471 

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

473 
apply (subst (1 2) nat_gcd_commute) 

474 
apply (subst add_commute) 

475 
apply simp 

476 
done 

477 

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

479 

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

481 
by (subst nat_gcd_add1 [symmetric], auto) 

482 

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

484 
apply (subst nat_gcd_commute) 

485 
apply (subst nat_gcd_diff1 [symmetric]) 

486 
apply auto 

487 
apply (subst nat_gcd_commute) 

488 
apply (subst nat_gcd_diff1) 

489 
apply assumption 

490 
apply (rule nat_gcd_commute) 

491 
done 

492 

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

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

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

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

497 
zmod_zminus1_eq_if) 

498 
apply (frule_tac a = x in pos_mod_bound) 

499 
apply (subst (1 2) nat_gcd_commute) 

500 
apply (simp del: pos_mod_bound add: nat_diff_distrib nat_gcd_diff2 

501 
nat_le_eq_zle) 

502 
done 

21256  503 

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

506 
apply force 

507 
apply (case_tac "y > 0") 

508 
apply (subst int_gcd_non_0, auto) 

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

510 
apply (auto simp add: int_gcd_neg1 int_gcd_neg2) 

511 
done 

512 

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

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

515 
apply (subst (1 2) int_gcd_red) 

516 
apply auto 

517 
done 

518 

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

520 
apply (subst int_gcd_commute) 

521 
apply (subst add_commute) 

522 
apply (subst int_gcd_add1) 

523 
apply (subst int_gcd_commute) 

524 
apply (rule refl) 

525 
done 

21256  526 

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

21256  529 

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

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

533 
apply (case_tac "k >= 0") 

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

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

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

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

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

539 
apply auto 

540 
apply (rule nat_induct) 

541 
apply auto 

542 
apply (auto simp add: left_distrib) 

543 
apply (subst add_assoc) 

544 
apply simp 

545 
done 

21256  546 

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

549 

550 
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

551 
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

552 

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

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

555 

31706  556 
subsection {* Coprimality *} 
557 

558 
lemma nat_div_gcd_coprime [intro]: 

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

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

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

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

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

566 
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

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

570 
unfolding dvd_def by blast 
31706  571 
then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" 
572 
by simp_all 

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

575 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

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

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

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

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

581 

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

584 
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

585 

31706  586 
apply (subst (1 2 3) int_gcd_abs) 
587 
apply (subst (1 2) abs_div) 

588 
apply auto 

589 
prefer 3 

590 
apply (rule nat_div_gcd_coprime [transferred]) 

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

592 
done 

593 

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

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

596 

597 
lemma nat_coprime_Suc_0: 

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

599 
using nat_coprime by (simp add: One_nat_def) 

600 

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

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

603 
using int_gcd_unique [of 1 a b] 

604 
apply clarsimp 

605 
apply (erule subst) 

606 
apply (rule iffI) 

607 
apply force 

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

609 
apply (case_tac "e >= 0") 

610 
apply force 

611 
apply force 

612 
done 

613 

614 
lemma nat_gcd_coprime: 

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

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

617 
shows "coprime a' b'" 

618 

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

620 
apply (erule ssubst) 

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

622 
apply (erule ssubst) 

623 
apply (rule nat_div_gcd_coprime) 

624 
using prems 

625 
apply force 

626 
apply (subst (1) b) 

627 
using z apply force 

628 
apply (subst (1) a) 

629 
using z apply force 

630 
done 

631 

632 
lemma int_gcd_coprime: 

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

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

635 
shows "coprime a' b'" 

636 

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

638 
apply (erule ssubst) 

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

640 
apply (erule ssubst) 

641 
apply (rule int_div_gcd_coprime) 

642 
using prems 

643 
apply force 

644 
apply (subst (1) b) 

645 
using z apply force 

646 
apply (subst (1) a) 

647 
using z apply force 

648 
done 

649 

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

651 
shows "coprime d (a * b)" 

652 
apply (subst nat_gcd_commute) 

653 
using da apply (subst nat_gcd_mult_cancel) 

654 
apply (subst nat_gcd_commute, assumption) 

655 
apply (subst nat_gcd_commute, rule db) 

656 
done 

657 

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

659 
shows "coprime d (a * b)" 

660 
apply (subst int_gcd_commute) 

661 
using da apply (subst int_gcd_mult_cancel) 

662 
apply (subst int_gcd_commute, assumption) 

663 
apply (subst int_gcd_commute, rule db) 

664 
done 

665 

666 
lemma nat_coprime_lmult: 

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

668 
proof  

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

670 
by (rule nat_gcd_greatest, auto) 

671 
with dab show ?thesis 

672 
by auto 

673 
qed 

674 

675 
lemma int_coprime_lmult: 

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

677 
proof  

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

679 
by (rule int_gcd_greatest, auto) 

680 
with dab show ?thesis 

681 
by auto 

682 
qed 

683 

684 
lemma nat_coprime_rmult: 

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

686 
proof  

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

688 
by (rule nat_gcd_greatest, auto intro: dvd_mult) 

689 
with dab show ?thesis 

690 
by auto 

691 
qed 

692 

693 
lemma int_coprime_rmult: 

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

695 
proof  

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

697 
by (rule int_gcd_greatest, auto intro: dvd_mult) 

698 
with dab show ?thesis 

699 
by auto 

700 
qed 

701 

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

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

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

705 
nat_coprime_mult[of d a b] 

706 
by blast 

707 

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

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

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

711 
int_coprime_mult[of d a b] 

712 
by blast 

713 

714 
lemma nat_gcd_coprime_exists: 

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

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

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

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

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

720 
done 

721 

722 
lemma int_gcd_coprime_exists: 

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

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

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

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

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

728 
done 

729 

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

731 
by (induct n, simp_all add: nat_coprime_mult) 

732 

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

734 
by (induct n, simp_all add: int_coprime_mult) 

735 

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

737 
apply (rule nat_coprime_exp) 

738 
apply (subst nat_gcd_commute) 

739 
apply (rule nat_coprime_exp) 

740 
apply (subst nat_gcd_commute, assumption) 

741 
done 

742 

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

744 
apply (rule int_coprime_exp) 

745 
apply (subst int_gcd_commute) 

746 
apply (rule int_coprime_exp) 

747 
apply (subst int_gcd_commute, assumption) 

748 
done 

749 

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

751 
proof (cases) 

752 
assume "a = 0 & b = 0" 

753 
thus ?thesis by simp 

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

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

756 
by auto 

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

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

759 
apply (subst (1 2) mult_commute) 

760 
apply (subst nat_gcd_mult_distrib [symmetric]) 

761 
apply simp 

762 
done 

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

764 
apply (subst div_power) 

765 
apply auto 

766 
apply (rule dvd_div_mult_self) 

767 
apply (rule dvd_power_same) 

768 
apply auto 

769 
done 

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

771 
apply (subst div_power) 

772 
apply auto 

773 
apply (rule dvd_div_mult_self) 

774 
apply (rule dvd_power_same) 

775 
apply auto 

776 
done 

777 
finally show ?thesis . 

778 
qed 

779 

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

781 
apply (subst (1 2) int_gcd_abs) 

782 
apply (subst (1 2) power_abs) 

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

784 
apply auto 

785 
done 

786 

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

788 
using nat_coprime_dvd_mult_iff[of d a b] 

789 
by (auto simp add: mult_commute) 

790 

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

792 
using int_coprime_dvd_mult_iff[of d a b] 

793 
by (auto simp add: mult_commute) 

794 

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

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

797 
proof 

798 
let ?g = "gcd a b" 

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

800 
moreover 

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

802 
from nat_gcd_coprime_exists[OF z] 

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

804 
by blast 

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

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

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

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

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

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

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

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

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

814 
with thb thc have ?thesis by blast } 

815 
ultimately show ?thesis by blast 

816 
qed 

817 

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

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

820 
proof 

821 
let ?g = "gcd a b" 

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

823 
moreover 

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

825 
from int_gcd_coprime_exists[OF z] 

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

827 
by blast 

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

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

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

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

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

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

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

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

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

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

838 
with thb thc have ?thesis by blast } 

839 
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

840 
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

841 

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

844 
shows "a dvd b" 

845 
proof 

846 
let ?g = "gcd a b" 

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

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

849 
moreover 

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

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

852 
from nat_gcd_coprime_exists[OF z] 

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

854 
by blast 

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

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

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

858 
by (simp only: power_mult_distrib mult_commute) 

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

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

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

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

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

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

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

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

867 
ultimately show ?thesis by blast 

868 
qed 

869 

870 
lemma int_pow_divides_pow: 

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

872 
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

873 
proof 
31706  874 
let ?g = "gcd a b" 
875 
from n obtain m where m: "n = Suc m" by (cases n, simp_all) 

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

877 
moreover 

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

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

880 
from int_gcd_coprime_exists[OF z] 

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

882 
by blast 

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

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

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

886 
by (simp only: power_mult_distrib mult_commute) 

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

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

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

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

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

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

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

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

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

896 
ultimately show ?thesis by blast 

897 
qed 

898 

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

900 
by (auto intro: nat_pow_divides_pow dvd_power_same) 

901 

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

903 
by (auto intro: int_pow_divides_pow dvd_power_same) 

904 

905 
lemma nat_divides_mult: 

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

907 
shows "m * n dvd r" 

908 
proof 

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

910 
unfolding dvd_def by blast 

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

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

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

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

915 
qed 

916 

917 
lemma int_divides_mult: 

918 
assumes mr: "(m::int) 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 int_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 

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

927 
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

928 

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

931 
apply force 

932 
apply (rule nat_dvd_diff) 

933 
apply auto 

934 
done 

935 

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

937 
using nat_coprime_plus_one by (simp add: One_nat_def) 

938 

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

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

941 
apply force 

942 
apply (rule dvd_diff) 

943 
apply auto 

944 
done 

945 

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

947 
using nat_coprime_plus_one [of "n  1"] 

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

949 

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

951 
using int_coprime_plus_one [of "n  1"] 

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

953 

954 
lemma nat_setprod_coprime [rule_format]: 

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

956 
apply (case_tac "finite A") 

957 
apply (induct set: finite) 

958 
apply (auto simp add: nat_gcd_mult_cancel) 

959 
done 

960 

961 
lemma int_setprod_coprime [rule_format]: 

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

963 
apply (case_tac "finite A") 

964 
apply (induct set: finite) 

965 
apply (auto simp add: int_gcd_mult_cancel) 

966 
done 

967 

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

969 
unfolding prime_nat_def 

970 
apply (subst even_mult_two_ex) 

971 
apply clarify 

972 
apply (drule_tac x = 2 in spec) 

973 
apply auto 

974 
done 

975 

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

977 
unfolding prime_int_def 

978 
apply (frule nat_prime_odd) 

979 
apply (auto simp add: even_nat_def) 

980 
done 

981 

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

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

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

985 
apply simp 

986 
apply (erule (1) nat_gcd_greatest) 

987 
done 

988 

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

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

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

992 
apply simp 

993 
apply (erule (1) int_gcd_greatest) 

994 
done 

995 

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

997 
coprime d e" 

998 
apply (auto simp add: dvd_def) 

999 
apply (frule int_coprime_lmult) 

1000 
apply (subst int_gcd_commute) 

1001 
apply (subst (asm) (2) int_gcd_commute) 

1002 
apply (erule int_coprime_lmult) 

1003 
done 

1004 

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

1006 
apply (metis nat_coprime_lmult nat_gcd_1 nat_gcd_commute nat_gcd_red) 

1007 
done 

1008 

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

1010 
apply (metis int_coprime_lmult int_gcd_1 int_gcd_commute int_gcd_red) 

1011 
done 

1012 

1013 

1014 
subsection {* Bezout's theorem *} 

1015 

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

1017 
see the theorems that follow the definition. *) 

1018 
fun 

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

1020 
where 

1021 
"bezw x y = 

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

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

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

1025 

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

1027 

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

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

1030 
by simp 

1031 

1032 
declare bezw.simps [simp del] 

1033 

1034 
lemma bezw_aux [rule_format]: 

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

1036 
proof (induct x y rule: nat_gcd_induct) 

1037 
fix m :: nat 

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

1039 
by auto 

1040 
next fix m :: nat and n 

1041 
assume ngt0: "n > 0" and 

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

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

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

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

1046 
apply (simp add: bezw_non_0 nat_gcd_non_0) 

1047 
apply (erule subst) 

1048 
apply (simp add: ring_simps) 

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

1050 
(* applying simp here undoes the last substitution! 

1051 
what is procedure cancel_div_mod? *) 

1052 
apply (simp only: ring_simps zadd_int [symmetric] 

1053 
zmult_int [symmetric]) 

1054 
done 

1055 
qed 

1056 

1057 
lemma int_bezout: 

1058 
fixes x y 

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

1060 
proof  

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

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

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

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

1065 
apply (unfold gcd_int_def) 

1066 
apply simp 

1067 
apply (subst bezw_aux [symmetric]) 

1068 
apply auto 

1069 
done 

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

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

1072 
by auto 

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

1074 
by (erule (1) bezout_aux) 

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

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

1077 
apply auto 

1078 
apply (rule_tac x = u in exI) 

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

1080 
apply (subst int_gcd_neg2 [symmetric]) 

1081 
apply auto 

1082 
done 

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

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

1085 
apply auto 

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

1087 
apply (rule_tac x = v in exI) 

1088 
apply (subst int_gcd_neg1 [symmetric]) 

1089 
apply auto 

1090 
done 

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

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

1093 
apply auto 

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

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

1096 
apply (subst int_gcd_neg1 [symmetric]) 

1097 
apply (subst int_gcd_neg2 [symmetric]) 

1098 
apply auto 

1099 
done 

1100 
ultimately show ?thesis by blast 

1101 
qed 

1102 

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

1104 

1105 
lemma ind_euclid: 

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

1107 
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

1108 
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

1109 
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

1110 
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

1111 
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

1112 
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

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

1116 
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

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

1118 
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

1119 
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

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

1121 
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

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

1123 
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

1124 
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

1125 
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

1126 
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

1127 
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

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

1129 
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

1130 
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

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

1132 
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

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

1134 
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

1135 
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

1136 
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

1137 
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

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

1140 
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

1141 

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

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

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

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

1147 
using ex 

1148 
apply clarsimp 

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

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

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

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

1153 
apply algebra 

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

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

1156 
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

1157 
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

1158 

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

1161 
apply(induct a b rule: ind_euclid) 

1162 
apply blast 

1163 
apply clarify 

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

1165 
apply clarsimp 

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

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

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

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

1170 
apply algebra 

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

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

1173 
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

1174 
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

1175 

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

1178 
using nat_bezout_add[of a b] 

1179 
apply clarsimp 

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

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

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

1183 
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

1184 
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

1185 

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

1187 
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

1188 
proof 
31706  1189 
from nz have ap: "a > 0" by simp 
1190 
from nat_bezout_add[of a b] 

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

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

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

1196 
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

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

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

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

1203 
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

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

1205 
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

1206 
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

1207 
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

1208 
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

1209 
moreover 
31706  1210 
{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

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

1212 
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

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

1214 
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

1215 
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

1216 
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

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

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

1221 
by (simp only: mult_assoc right_distrib) 

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

1223 
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

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

1226 
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

1227 
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

1228 
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

1229 
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

1230 
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

1231 
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

1232 
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

1233 
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

1234 
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

1235 
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

1236 
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

1237 
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

1238 
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

1239 

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

1241 
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

1242 
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

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

1245 
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

1246 
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

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

1249 
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

1250 
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

1251 
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

1252 

31706  1253 

1254 
subsection {* LCM *} 

1255 

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

1257 
by (simp add: lcm_int_def lcm_nat_def zdiv_int 

1258 
zmult_int [symmetric] gcd_int_def) 

1259 

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

1261 
unfolding lcm_nat_def 

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

1263 

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

1265 
unfolding lcm_int_def gcd_int_def 

1266 
apply (subst int_mult [symmetric]) 

1267 
apply (subst nat_prod_gcd_lcm [symmetric]) 

1268 
apply (subst nat_abs_mult_distrib [symmetric]) 

1269 
apply (simp, simp add: abs_mult) 

1270 
done 

1271 

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

1273 
unfolding lcm_nat_def by simp 

1274 

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

1276 
unfolding lcm_int_def by simp 

1277 

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

1279 
unfolding lcm_nat_def by simp 

1280 

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

1282 
unfolding lcm_nat_def by (simp add: One_nat_def) 

1283 

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

1285 
unfolding lcm_int_def by simp 

1286 

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

1288 
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

1289 

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

1292 

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

1294 
unfolding lcm_nat_def by simp 

1295 

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

1297 
unfolding lcm_nat_def by (simp add: One_nat_def) 

1298 

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

1300 
unfolding lcm_int_def by simp 

1301 

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

1303 
unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps) 

1304 

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

1306 
unfolding lcm_int_def by (subst nat_lcm_commute, rule refl) 

1307 

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

1309 

1310 
lemma nat_lcm_pos: 

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

1312 
and npos: "n>0" 

1313 
shows "lcm m n > 0" 

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

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

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

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

1318 
with h 

1319 
have "m*n < gcd m n" 

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

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

1322 
moreover 
31706  1323 
have "gcd m n dvd m" by simp 
1324 
with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp 

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

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

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

1328 
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

1329 
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

1330 

31706  1331 
lemma int_lcm_pos: 
1332 
assumes mneq0: "(m::int) ~= 0" 

1333 
and npos: "n ~= 0" 

1334 
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

1335 

31706  1336 
apply (subst int_lcm_abs) 
1337 
apply (rule nat_lcm_pos [transferred]) 

1338 
using prems apply auto 

1339 
done 

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

1340 

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

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

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

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

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

1346 

31706  1347 
lemma nat_lcm_least: 
1348 
assumes "(m::nat) dvd k" and "n dvd k" 

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

1350 
proof (cases k) 