author  nipkow 
Fri, 26 Jun 2009 10:46:33 +0200  
changeset 31813  4df828bbc411 
parent 31798  fe9a3043d36c 
child 31814  7c122634da81 
permissions  rwrr 
31706  1 
(* Title: GCD.thy 
2 
Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, 

31798  3 
Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow 
31706  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 

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

31706  26 

27 
header {* GCD *} 

21256  28 

29 
theory GCD 

31706  30 
imports NatTransfer 
31 
begin 

32 

33 
declare One_nat_def [simp del] 

34 

35 
subsection {* gcd *} 

36 

37 
class gcd = one + 

38 

39 
fixes 

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

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

42 

21256  43 
begin 
44 

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

47 
where 

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

49 

50 
end 

51 

52 
class prime = one + 

53 

54 
fixes 

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

56 

57 

58 
(* definitions for the natural numbers *) 

59 

60 
instantiation nat :: gcd 

61 

62 
begin 

21256  63 

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

66 
where 

67 
"gcd_nat x y = 

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

69 

70 
definition 

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

72 
where 

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

74 

75 
instance proof qed 

76 

77 
end 

78 

79 

80 
instantiation nat :: prime 

81 

82 
begin 

21256  83 

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

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

89 
instance proof qed 

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

90 

31706  91 
end 
92 

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

93 

31706  94 
(* definitions for the integers *) 
95 

96 
instantiation int :: gcd 

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

97 

31706  98 
begin 
21256  99 

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

102 
where 

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

104 

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

107 
where 

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

109 

31706  110 
instance proof qed 
111 

112 
end 

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

113 

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

114 

31706  115 
instantiation int :: prime 
116 

117 
begin 

118 

119 
definition 

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

121 
where 

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

124 
instance proof qed 

125 

126 
end 

127 

128 

129 
subsection {* Set up Transfer *} 

130 

131 

132 
lemma transfer_nat_int_gcd: 

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

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

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

136 
unfolding gcd_int_def lcm_int_def prime_int_def 

137 
by auto 

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

138 

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

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

142 
by (auto simp add: gcd_int_def lcm_int_def) 

143 

144 
declare TransferMorphism_nat_int[transfer add return: 

145 
transfer_nat_int_gcd transfer_nat_int_gcd_closures] 

146 

147 
lemma transfer_int_nat_gcd: 

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

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

150 
"prime (int x) = prime x" 

151 
by (unfold gcd_int_def lcm_int_def prime_int_def, auto) 

152 

153 
lemma transfer_int_nat_gcd_closures: 

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

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

156 
by (auto simp add: gcd_int_def lcm_int_def) 

157 

158 
declare TransferMorphism_int_nat[transfer add return: 

159 
transfer_int_nat_gcd transfer_int_nat_gcd_closures] 

160 

161 

162 

163 
subsection {* GCD *} 

164 

165 
(* was gcd_induct *) 

166 
lemma nat_gcd_induct: 

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

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

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

169 
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

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

173 
using assms apply simp_all 

174 
done 

175 

176 
(* specific to int *) 

177 

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

179 
by (simp add: gcd_int_def) 

180 

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

182 
by (simp add: gcd_int_def) 

183 

31813  184 
lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y" 
185 
by(simp add: gcd_int_def) 

186 

31706  187 
lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)" 
31813  188 
by (simp add: gcd_int_def) 
189 

190 
lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y" 

191 
by (metis abs_idempotent int_gcd_abs) 

192 

193 
lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y" 

194 
by (metis abs_idempotent int_gcd_abs) 

31706  195 

196 
lemma int_gcd_cases: 

197 
fixes x :: int and y 

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

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

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

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

202 
shows "P (gcd x y)" 

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

21256  204 

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

207 

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

209 
by (simp add: lcm_int_def) 

210 

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

212 
by (simp add: lcm_int_def) 

213 

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

215 
by (simp add: lcm_int_def) 

21256  216 

31706  217 
lemma int_lcm_cases: 
218 
fixes x :: int and y 

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

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

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

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

223 
shows "P (lcm x y)" 

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

225 

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

227 
by (simp add: lcm_int_def) 

228 

229 
(* was gcd_0, etc. *) 

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

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

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

232 

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

235 
by (unfold gcd_int_def, auto) 

236 

237 
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

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

239 

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

242 

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

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

245 

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

247 

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

249 
by simp 

250 

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

21263  252 
by simp 
21256  253 

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

256 

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

258 
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

259 

31798  260 
lemma nat_gcd_idem: "gcd (x::nat) x = x" 
261 
by simp 

31706  262 

31798  263 
lemma int_gcd_idem: "gcd (x::int) x = abs x" 
31813  264 
by (auto simp add: gcd_int_def) 
31706  265 

266 
declare gcd_nat.simps [simp del] 

21256  267 

268 
text {* 

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

272 

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

275 
apply (induct m n rule: nat_gcd_induct) 

276 
apply (simp_all add: nat_gcd_non_0) 

21256  277 
apply (blast dest: dvd_mod_imp_dvd) 
31706  278 
done 
279 

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

31813  281 
by (metis gcd_int_def int_dvd_iff nat_gcd_dvd1) 
21256  282 

31706  283 
lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y" 
31813  284 
by (metis gcd_int_def int_dvd_iff nat_gcd_dvd2) 
31706  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" 

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

313 
lemma int_gcd_greatest: 

31813  314 
"(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n" 
31706  315 
apply (subst int_gcd_abs) 
316 
apply (subst abs_dvd_iff [symmetric]) 

317 
apply (rule nat_gcd_greatest [transferred]) 

31813  318 
apply auto 
31706  319 
done 
21256  320 

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

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

324 

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

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

21256  327 

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

21256  330 

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

21256  333 

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

21256  336 

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

339 

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

341 
by (rule dvd_anti_sym, auto) 

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

342 

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

345 

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

347 
apply (rule dvd_anti_sym) 

348 
apply (blast intro: dvd_trans)+ 

349 
done 

21256  350 

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

353 

31766  354 
lemmas nat_gcd_left_commute = 
355 
mk_left_commute[of gcd, OF nat_gcd_assoc nat_gcd_commute] 

31706  356 

31766  357 
lemmas int_gcd_left_commute = 
358 
mk_left_commute[of gcd, OF int_gcd_assoc int_gcd_commute] 

31706  359 

360 
lemmas nat_gcd_ac = nat_gcd_assoc nat_gcd_commute nat_gcd_left_commute 

361 
 {* gcd is an ACoperator *} 

21256  362 

31706  363 
lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute 
364 

365 
lemma nat_gcd_unique: "(d::nat) dvd a \<and> d dvd b \<and> 

366 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 

367 
apply auto 

368 
apply (rule dvd_anti_sym) 

369 
apply (erule (1) nat_gcd_greatest) 

370 
apply auto 

371 
done 

21256  372 

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

375 
apply (case_tac "d = 0") 

376 
apply force 

377 
apply (rule iffI) 

378 
apply (rule zdvd_anti_sym) 

379 
apply arith 

380 
apply (subst int_gcd_pos) 

381 
apply clarsimp 

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

383 
apply (frule zdvd_imp_le) 

384 
apply (auto intro: int_gcd_greatest) 

385 
done 

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

386 

31798  387 
lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x" 
388 
by (metis dvd.eq_iff nat_gcd_unique) 

389 

390 
lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y" 

391 
by (metis dvd.eq_iff nat_gcd_unique) 

392 

393 
lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x" 

394 
by (metis abs_dvd_iff abs_eq_0 int_gcd_0_left int_gcd_abs int_gcd_unique) 

395 

396 
lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y" 

397 
by (metis gcd_proj1_if_dvd_int int_gcd_commute) 

398 

399 

21256  400 
text {* 
401 
\medskip Multiplication laws 

402 
*} 

403 

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

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

21256  411 

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

31813  414 
apply (subst (1 2) abs_mult) 
31706  415 
apply (rule nat_gcd_mult_distrib [transferred]) 
416 
apply auto 

417 
done 

21256  418 

31706  419 
lemma nat_coprime_dvd_mult: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m" 
420 
apply (insert nat_gcd_mult_distrib [of m k n]) 

21256  421 
apply simp 
422 
apply (erule_tac t = m in ssubst) 

423 
apply simp 

424 
done 

425 

31706  426 
lemma int_coprime_dvd_mult: 
31813  427 
"coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m" 
428 
apply (subst abs_dvd_iff [symmetric]) 

429 
apply (subst dvd_abs_iff [symmetric]) 

430 
apply (subst (asm) int_gcd_abs) 

431 
apply (rule nat_coprime_dvd_mult [transferred]) 

432 
prefer 4 apply assumption 

433 
apply auto 

434 
apply (subst abs_mult [symmetric], auto) 

31706  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: 
31813  455 
"coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n" 
456 
apply (subst (1 2) int_gcd_abs) 

457 
apply (subst abs_mult) 

458 
apply (rule nat_gcd_mult_cancel [transferred], auto) 

31706  459 
done 
21256  460 

461 
text {* \medskip Addition laws *} 

462 

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

465 
apply (simp_all add: nat_gcd_non_0) 

466 
done 

467 

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

469 
apply (subst (1 2) nat_gcd_commute) 

470 
apply (subst add_commute) 

471 
apply simp 

472 
done 

473 

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

475 

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

477 
by (subst nat_gcd_add1 [symmetric], auto) 

478 

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

480 
apply (subst nat_gcd_commute) 

481 
apply (subst nat_gcd_diff1 [symmetric]) 

482 
apply auto 

483 
apply (subst nat_gcd_commute) 

484 
apply (subst nat_gcd_diff1) 

485 
apply assumption 

486 
apply (rule nat_gcd_commute) 

487 
done 

488 

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

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

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

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

493 
zmod_zminus1_eq_if) 

494 
apply (frule_tac a = x in pos_mod_bound) 

495 
apply (subst (1 2) nat_gcd_commute) 

496 
apply (simp del: pos_mod_bound add: nat_diff_distrib nat_gcd_diff2 

497 
nat_le_eq_zle) 

498 
done 

21256  499 

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

502 
apply force 

503 
apply (case_tac "y > 0") 

504 
apply (subst int_gcd_non_0, auto) 

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

506 
apply (auto simp add: int_gcd_neg1 int_gcd_neg2) 

507 
done 

508 

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

31798  510 
by (metis int_gcd_red mod_add_self1 zadd_commute) 
31706  511 

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

31798  513 
by (metis int_gcd_add1 int_gcd_commute zadd_commute) 
21256  514 

31706  515 
lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n" 
31798  516 
by (metis mod_mult_self3 nat_gcd_commute nat_gcd_red) 
21256  517 

31706  518 
lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n" 
31798  519 
by (metis int_gcd_commute int_gcd_red mod_mult_self1 zadd_commute) 
520 

21256  521 

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

524 

31798  525 
(* FIXME remove iff *) 
31706  526 
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

527 
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

528 

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

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

533 
proof 

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

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

536 
by(bestsimp intro!:dvd_imp_le) 

537 
qed 

538 

539 
lemma finite_divisors_int: 

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

541 
proof 

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

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

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

545 
by(bestsimp intro!:dvd_imp_le_int) 

546 
qed 

547 

548 
lemma gcd_is_Max_divisors_nat: 

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

550 
apply(rule Max_eqI[THEN sym]) 

551 
apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat) 

552 
apply simp 

553 
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le nat_gcd_greatest_iff nat_gcd_pos) 

554 
apply simp 

555 
done 

556 

557 
lemma gcd_is_Max_divisors_int: 

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

559 
apply(rule Max_eqI[THEN sym]) 

560 
apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int) 

561 
apply simp 

562 
apply (metis int_gcd_greatest_iff int_gcd_pos zdvd_imp_le) 

563 
apply simp 

564 
done 

565 

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

566 

31706  567 
subsection {* Coprimality *} 
568 

31813  569 
lemma nat_div_gcd_coprime: 
31706  570 
assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0" 
571 
shows "coprime (a div gcd a b) (b div gcd a b)" 

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

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

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

577 
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

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

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

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

586 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

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

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

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

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

592 

31813  593 
lemma int_div_gcd_coprime: 
31706  594 
assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0" 
595 
shows "coprime (a div gcd a b) (b div gcd a b)" 

31813  596 
apply (subst (1 2 3) int_gcd_abs) 
597 
apply (subst (1 2) abs_div) 

598 
apply simp 

599 
apply simp 

600 
apply(subst (1 2) abs_gcd_int) 

601 
apply (rule nat_div_gcd_coprime [transferred]) 

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

31706  603 
done 
604 

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

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

607 

608 
lemma nat_coprime_Suc_0: 

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

610 
using nat_coprime by (simp add: One_nat_def) 

611 

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

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

614 
using int_gcd_unique [of 1 a b] 

615 
apply clarsimp 

616 
apply (erule subst) 

617 
apply (rule iffI) 

618 
apply force 

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

620 
apply (case_tac "e >= 0") 

621 
apply force 

622 
apply force 

623 
done 

624 

625 
lemma nat_gcd_coprime: 

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

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

628 
shows "coprime a' b'" 

629 

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

631 
apply (erule ssubst) 

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

633 
apply (erule ssubst) 

634 
apply (rule nat_div_gcd_coprime) 

635 
using prems 

636 
apply force 

637 
apply (subst (1) b) 

638 
using z apply force 

639 
apply (subst (1) a) 

640 
using z apply force 

641 
done 

642 

643 
lemma int_gcd_coprime: 

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

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

646 
shows "coprime a' b'" 

647 

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

649 
apply (erule ssubst) 

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

651 
apply (erule ssubst) 

652 
apply (rule int_div_gcd_coprime) 

653 
using prems 

654 
apply force 

655 
apply (subst (1) b) 

656 
using z apply force 

657 
apply (subst (1) a) 

658 
using z apply force 

659 
done 

660 

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

662 
shows "coprime d (a * b)" 

663 
apply (subst nat_gcd_commute) 

664 
using da apply (subst nat_gcd_mult_cancel) 

665 
apply (subst nat_gcd_commute, assumption) 

666 
apply (subst nat_gcd_commute, rule db) 

667 
done 

668 

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

670 
shows "coprime d (a * b)" 

671 
apply (subst int_gcd_commute) 

672 
using da apply (subst int_gcd_mult_cancel) 

673 
apply (subst int_gcd_commute, assumption) 

674 
apply (subst int_gcd_commute, rule db) 

675 
done 

676 

677 
lemma nat_coprime_lmult: 

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

679 
proof  

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

681 
by (rule nat_gcd_greatest, auto) 

682 
with dab show ?thesis 

683 
by auto 

684 
qed 

685 

686 
lemma int_coprime_lmult: 

31798  687 
assumes "coprime (d::int) (a * b)" shows "coprime d a" 
31706  688 
proof  
689 
have "gcd d a dvd gcd d (a * b)" 

690 
by (rule int_gcd_greatest, auto) 

31798  691 
with assms show ?thesis 
31706  692 
by auto 
693 
qed 

694 

695 
lemma nat_coprime_rmult: 

31798  696 
assumes "coprime (d::nat) (a * b)" shows "coprime d b" 
31706  697 
proof  
698 
have "gcd d b dvd gcd d (a * b)" 

699 
by (rule nat_gcd_greatest, auto intro: dvd_mult) 

31798  700 
with assms show ?thesis 
31706  701 
by auto 
702 
qed 

703 

704 
lemma int_coprime_rmult: 

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

706 
proof  

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

708 
by (rule int_gcd_greatest, auto intro: dvd_mult) 

709 
with dab show ?thesis 

710 
by auto 

711 
qed 

712 

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

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

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

716 
nat_coprime_mult[of d a b] 

717 
by blast 

718 

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

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

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

722 
int_coprime_mult[of d a b] 

723 
by blast 

724 

725 
lemma nat_gcd_coprime_exists: 

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

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

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

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

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

731 
done 

732 

733 
lemma int_gcd_coprime_exists: 

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

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

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

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

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

739 
done 

740 

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

742 
by (induct n, simp_all add: nat_coprime_mult) 

743 

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

745 
by (induct n, simp_all add: int_coprime_mult) 

746 

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

748 
apply (rule nat_coprime_exp) 

749 
apply (subst nat_gcd_commute) 

750 
apply (rule nat_coprime_exp) 

751 
apply (subst nat_gcd_commute, assumption) 

752 
done 

753 

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

755 
apply (rule int_coprime_exp) 

756 
apply (subst int_gcd_commute) 

757 
apply (rule int_coprime_exp) 

758 
apply (subst int_gcd_commute, assumption) 

759 
done 

760 

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

762 
proof (cases) 

763 
assume "a = 0 & b = 0" 

764 
thus ?thesis by simp 

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

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

31813  767 
by (auto simp:nat_div_gcd_coprime) 
31706  768 
hence "gcd ((a div gcd a b)^n * (gcd a b)^n) 
769 
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" 

770 
apply (subst (1 2) mult_commute) 

771 
apply (subst nat_gcd_mult_distrib [symmetric]) 

772 
apply simp 

773 
done 

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

775 
apply (subst div_power) 

776 
apply auto 

777 
apply (rule dvd_div_mult_self) 

778 
apply (rule dvd_power_same) 

779 
apply auto 

780 
done 

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

782 
apply (subst div_power) 

783 
apply auto 

784 
apply (rule dvd_div_mult_self) 

785 
apply (rule dvd_power_same) 

786 
apply auto 

787 
done 

788 
finally show ?thesis . 

789 
qed 

790 

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

792 
apply (subst (1 2) int_gcd_abs) 

793 
apply (subst (1 2) power_abs) 

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

795 
apply auto 

796 
done 

797 

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

799 
using nat_coprime_dvd_mult_iff[of d a b] 

800 
by (auto simp add: mult_commute) 

801 

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

803 
using int_coprime_dvd_mult_iff[of d a b] 

804 
by (auto simp add: mult_commute) 

805 

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

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

808 
proof 

809 
let ?g = "gcd a b" 

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

811 
moreover 

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

813 
from nat_gcd_coprime_exists[OF z] 

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

815 
by blast 

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

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

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

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

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

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

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

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

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

825 
with thb thc have ?thesis by blast } 

826 
ultimately show ?thesis by blast 

827 
qed 

828 

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

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

831 
proof 

832 
let ?g = "gcd a b" 

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

834 
moreover 

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

836 
from int_gcd_coprime_exists[OF z] 

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

838 
by blast 

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

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

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

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

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

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

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

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

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

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

849 
with thb thc have ?thesis by blast } 

850 
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

851 
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

852 

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

855 
shows "a dvd b" 

856 
proof 

857 
let ?g = "gcd a b" 

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

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

860 
moreover 

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

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

863 
from nat_gcd_coprime_exists[OF z] 

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

865 
by blast 

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

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

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

869 
by (simp only: power_mult_distrib mult_commute) 

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

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

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

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

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

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

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

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

878 
ultimately show ?thesis by blast 

879 
qed 

880 

881 
lemma int_pow_divides_pow: 

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

883 
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

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

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

888 
moreover 

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

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

891 
from int_gcd_coprime_exists[OF z] 

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

893 
by blast 

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

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

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

897 
by (simp only: power_mult_distrib mult_commute) 

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

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

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

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

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

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

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

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

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

907 
ultimately show ?thesis by blast 

908 
qed 

909 

31798  910 
(* FIXME move to Divides(?) *) 
31706  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_0_left [simp]: "lcm (0::nat) n = 0" 

1291 
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

1292 

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

1295 

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

1297 
unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps) 

1298 

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

1300 
unfolding lcm_int_def by (subst nat_lcm_commute, rule refl) 

1301 

1302 

1303 
lemma nat_lcm_pos: 

31798  1304 
"(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0" 
1305 
by (metis gr0I mult_is_0 nat_prod_gcd_lcm) 

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

1306 

31706  1307 
lemma int_lcm_pos: 
31798  1308 
"(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0" 
31706  1309 
apply (subst int_lcm_abs) 
1310 
apply (rule nat_lcm_pos [transferred]) 

31798  1311 
apply auto 
31706  1312 
done 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1313 

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

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

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

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

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

1319 

31706  1320 
lemma nat_lcm_least: 
1321 
assumes "(m::nat) dvd k" and "n dvd k" 

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

1323 
proof (cases k) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1324 
case 0 then show ?thesis by auto 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

1326 
case (Suc _) then have pos_k: "k > 0" by auto 
31706  1327 
from assms nat_dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto 
1328 
with nat_gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp 

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

1329 
from assms obtain p where k_m: "k = m * p" using dvd_def by blast 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1330 
from assms obtain q where k_n: "k = n * q" using dvd_def by blast 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1331 
from pos_k k_m have pos_p: "p > 0" by auto 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1332 
from pos_k k_n have pos_q: "q > 0" by auto 
27556  1333 
have "k * k * gcd q p = k * gcd (k * q) (k * p)" 
31706  1334 
by (simp add: mult_ac nat_gcd_mult_distrib) 
27556  1335 
also have "\<dots> = k * gcd (m * p * q) (n * q * p)" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1336 
by (simp add: k_m [symmetric] k_n [symmetric]) 
27556  1337 
also have "\<dots> = k * p * q * gcd m n" 
31706  1338 
by (simp add: mult_ac nat_gcd_mult_distrib) 
27556  1339 
finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1340 
by (simp only: k_m [symmetric] k_n [symmetric]) 
27556  1341 
then have "p * q * m * n * gcd q p = p * q * k * gcd m n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1342 
by (simp add: mult_ac) 
27556  1343 
with pos_p pos_q have "m * n * gcd q p = k * gcd m n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1344 
by simp 
31706  1345 
with nat_prod_gcd_lcm [of m n] 
27556  1346 
have "lcm m n * gcd q p * gcd m n = k * gcd m n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1347 
by (simp add: mult_ac) 
31706  1348 
with pos_gcd have "lcm m n * gcd q p = k" by auto 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1349 
then show ?thesis using dvd_def by auto 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

1351 

31706  1352 
lemma int_lcm_least: 
31798  1353 
"(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k" 
1354 
apply (subst int_lcm_abs) 

1355 
apply (rule dvd_trans) 

1356 
apply (rule nat_lcm_least [transferred, of _ "abs k" _]) 

1357 
apply auto 

31706  1358 
done 