author  avigad 
Fri, 10 Jul 2009 10:45:30 0400  
changeset 32036  8a9228872fbd 
parent 31952  40501bb2d57c 
child 32040  830141c9e528 
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 

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

23 
Jeremy Avigad combined all of these, made everything uniform for the 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

24 
natural numbers and the integers, and added a number of new theorems. 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

25 

31798  26 
Tobias Nipkow cleaned up a lot. 
21256  27 
*) 
28 

31706  29 

30 
header {* GCD *} 

21256  31 

32 
theory GCD 

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

33 
imports Fact 
31706  34 
begin 
35 

36 
declare One_nat_def [simp del] 

37 

38 
subsection {* gcd *} 

39 

40 
class gcd = one + 

41 

42 
fixes 

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

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

45 

21256  46 
begin 
47 

31706  48 
abbreviation 
49 
coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 

50 
where 

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

52 

53 
end 

54 

55 
class prime = one + 

56 

57 
fixes 

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

59 

60 

61 
(* definitions for the natural numbers *) 

62 

63 
instantiation nat :: gcd 

64 

65 
begin 

21256  66 

31706  67 
fun 
68 
gcd_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

69 
where 

70 
"gcd_nat x y = 

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

72 

73 
definition 

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

75 
where 

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

77 

78 
instance proof qed 

79 

80 
end 

81 

82 

83 
instantiation nat :: prime 

84 

85 
begin 

21256  86 

21263  87 
definition 
31706  88 
prime_nat :: "nat \<Rightarrow> bool" 
89 
where 

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

92 
instance proof qed 

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

93 

31706  94 
end 
95 

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

96 

31706  97 
(* definitions for the integers *) 
98 

99 
instantiation int :: gcd 

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

100 

31706  101 
begin 
21256  102 

31706  103 
definition 
104 
gcd_int :: "int \<Rightarrow> int \<Rightarrow> int" 

105 
where 

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

107 

31706  108 
definition 
109 
lcm_int :: "int \<Rightarrow> int \<Rightarrow> int" 

110 
where 

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

112 

31706  113 
instance proof qed 
114 

115 
end 

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

116 

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

117 

31706  118 
instantiation int :: prime 
119 

120 
begin 

121 

122 
definition 

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

124 
where 

31709  125 
[code del]: "prime_int p = prime (nat p)" 
31706  126 

127 
instance proof qed 

128 

129 
end 

130 

131 

132 
subsection {* Set up Transfer *} 

133 

134 

135 
lemma transfer_nat_int_gcd: 

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

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

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

139 
unfolding gcd_int_def lcm_int_def prime_int_def 

140 
by auto 

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

141 

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

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

145 
by (auto simp add: gcd_int_def lcm_int_def) 

146 

147 
declare TransferMorphism_nat_int[transfer add return: 

148 
transfer_nat_int_gcd transfer_nat_int_gcd_closures] 

149 

150 
lemma transfer_int_nat_gcd: 

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

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

153 
"prime (int x) = prime x" 

154 
by (unfold gcd_int_def lcm_int_def prime_int_def, auto) 

155 

156 
lemma transfer_int_nat_gcd_closures: 

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

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

159 
by (auto simp add: gcd_int_def lcm_int_def) 

160 

161 
declare TransferMorphism_int_nat[transfer add return: 

162 
transfer_int_nat_gcd transfer_int_nat_gcd_closures] 

163 

164 

165 

166 
subsection {* GCD *} 

167 

168 
(* was gcd_induct *) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

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

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

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

172 
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

173 
shows "P m n" 
31706  174 
apply (rule gcd_nat.induct) 
175 
apply (case_tac "y = 0") 

176 
using assms apply simp_all 

177 
done 

178 

179 
(* specific to int *) 

180 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

181 
lemma gcd_neg1_int [simp]: "gcd (x::int) y = gcd x y" 
31706  182 
by (simp add: gcd_int_def) 
183 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

184 
lemma gcd_neg2_int [simp]: "gcd (x::int) (y) = gcd x y" 
31706  185 
by (simp add: gcd_int_def) 
186 

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

189 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

190 
lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)" 
31813  191 
by (simp add: gcd_int_def) 
192 

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

194 
by (metis abs_idempotent gcd_abs_int) 
31813  195 

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

197 
by (metis abs_idempotent gcd_abs_int) 
31706  198 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

199 
lemma gcd_cases_int: 
31706  200 
fixes x :: int and y 
201 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)" 

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

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

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

205 
shows "P (gcd x y)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

206 
by (insert prems, auto simp add: gcd_neg1_int gcd_neg2_int, arith) 
21256  207 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

208 
lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0" 
31706  209 
by (simp add: gcd_int_def) 
210 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

211 
lemma lcm_neg1_int: "lcm (x::int) y = lcm x y" 
31706  212 
by (simp add: lcm_int_def) 
213 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

214 
lemma lcm_neg2_int: "lcm (x::int) (y) = lcm x y" 
31706  215 
by (simp add: lcm_int_def) 
216 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

217 
lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)" 
31706  218 
by (simp add: lcm_int_def) 
21256  219 

31814  220 
lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j" 
221 
by(simp add:lcm_int_def) 

222 

223 
lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y" 

224 
by (metis abs_idempotent lcm_int_def) 

225 

226 
lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y" 

227 
by (metis abs_idempotent lcm_int_def) 

228 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

229 
lemma lcm_cases_int: 
31706  230 
fixes x :: int and y 
231 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)" 

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

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

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

235 
shows "P (lcm x y)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

236 
by (insert prems, auto simp add: lcm_neg1_int lcm_neg2_int, arith) 
31706  237 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

238 
lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0" 
31706  239 
by (simp add: lcm_int_def) 
240 

241 
(* was gcd_0, etc. *) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

242 
lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

244 

31706  245 
(* was igcd_0, etc. *) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

246 
lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x" 
31706  247 
by (unfold gcd_int_def, auto) 
248 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

249 
lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

251 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

252 
lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x" 
31706  253 
by (unfold gcd_int_def, auto) 
254 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

255 
lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)" 
31706  256 
by (case_tac "y = 0", auto) 
257 

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

259 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

260 
lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)" 
31706  261 
by simp 
262 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

263 
lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1" 
21263  264 
by simp 
21256  265 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

266 
lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" 
31706  267 
by (simp add: One_nat_def) 
268 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

269 
lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1" 
31706  270 
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

271 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

272 
lemma gcd_idem_nat: "gcd (x::nat) x = x" 
31798  273 
by simp 
31706  274 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

275 
lemma gcd_idem_int: "gcd (x::int) x = abs x" 
31813  276 
by (auto simp add: gcd_int_def) 
31706  277 

278 
declare gcd_nat.simps [simp del] 

21256  279 

280 
text {* 

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

284 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

285 
lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

286 
and gcd_dvd2_nat [iff]: "(gcd m n) dvd n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

287 
apply (induct m n rule: gcd_nat_induct) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

288 
apply (simp_all add: gcd_non_0_nat) 
21256  289 
apply (blast dest: dvd_mod_imp_dvd) 
31706  290 
done 
291 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

292 
lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

293 
by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat) 
21256  294 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

295 
lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

296 
by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat) 
31706  297 

31730  298 
lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

299 
by(metis gcd_dvd1_nat dvd_trans) 
31730  300 

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

302 
by(metis gcd_dvd2_nat dvd_trans) 
31730  303 

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

305 
by(metis gcd_dvd1_int dvd_trans) 
31730  306 

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

308 
by(metis gcd_dvd2_int dvd_trans) 
31730  309 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

310 
lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a" 
31706  311 
by (rule dvd_imp_le, auto) 
312 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

313 
lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b" 
31706  314 
by (rule dvd_imp_le, auto) 
315 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

316 
lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a" 
31706  317 
by (rule zdvd_imp_le, auto) 
21256  318 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

319 
lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b" 
31706  320 
by (rule zdvd_imp_le, auto) 
321 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

322 
lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

323 
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod) 
31706  324 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

325 
lemma gcd_greatest_int: 
31813  326 
"(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

327 
apply (subst gcd_abs_int) 
31706  328 
apply (subst abs_dvd_iff [symmetric]) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

329 
apply (rule gcd_greatest_nat [transferred]) 
31813  330 
apply auto 
31706  331 
done 
21256  332 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

333 
lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) = 
31706  334 
(k dvd m & k dvd n)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

335 
by (blast intro!: gcd_greatest_nat intro: dvd_trans) 
31706  336 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

337 
lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

338 
by (blast intro!: gcd_greatest_int intro: dvd_trans) 
21256  339 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

340 
lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

341 
by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat) 
21256  342 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

343 
lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)" 
31706  344 
by (auto simp add: gcd_int_def) 
21256  345 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

346 
lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0  n ~= 0)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

347 
by (insert gcd_zero_nat [of m n], arith) 
21256  348 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

349 
lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0  n ~= 0)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

350 
by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith) 
31706  351 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

352 
lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m" 
31706  353 
by (rule dvd_anti_sym, auto) 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

354 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

355 
lemma gcd_commute_int: "gcd (m::int) n = gcd n m" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

356 
by (auto simp add: gcd_int_def gcd_commute_nat) 
31706  357 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

358 
lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)" 
31706  359 
apply (rule dvd_anti_sym) 
360 
apply (blast intro: dvd_trans)+ 

361 
done 

21256  362 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

363 
lemma gcd_assoc_int: "gcd (gcd (k::int) m) n = gcd k (gcd m n)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

364 
by (auto simp add: gcd_int_def gcd_assoc_nat) 
31706  365 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

366 
lemmas gcd_left_commute_nat = 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

367 
mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat] 
31706  368 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

369 
lemmas gcd_left_commute_int = 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

370 
mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int] 
31706  371 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

372 
lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat 
31706  373 
 {* gcd is an ACoperator *} 
21256  374 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

375 
lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int 
31706  376 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

377 
lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and> 
31706  378 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 
379 
apply auto 

380 
apply (rule dvd_anti_sym) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

381 
apply (erule (1) gcd_greatest_nat) 
31706  382 
apply auto 
383 
done 

21256  384 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

385 
lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and> 
31706  386 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 
387 
apply (case_tac "d = 0") 

388 
apply force 

389 
apply (rule iffI) 

390 
apply (rule zdvd_anti_sym) 

391 
apply arith 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

392 
apply (subst gcd_pos_int) 
31706  393 
apply clarsimp 
394 
apply (drule_tac x = "d + 1" in spec) 

395 
apply (frule zdvd_imp_le) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

396 
apply (auto intro: gcd_greatest_int) 
31706  397 
done 
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
30042
diff
changeset

398 

31798  399 
lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

400 
by (metis dvd.eq_iff gcd_unique_nat) 
31798  401 

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

403 
by (metis dvd.eq_iff gcd_unique_nat) 
31798  404 

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

406 
by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int) 
31798  407 

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

409 
by (metis gcd_proj1_if_dvd_int gcd_commute_int) 
31798  410 

411 

21256  412 
text {* 
413 
\medskip Multiplication laws 

414 
*} 

415 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

416 
lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)" 
21256  417 
 {* \cite[page 27]{davenport92} *} 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

418 
apply (induct m n rule: gcd_nat_induct) 
31706  419 
apply simp 
21256  420 
apply (case_tac "k = 0") 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

421 
apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2) 
31706  422 
done 
21256  423 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

424 
lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

425 
apply (subst (1 2) gcd_abs_int) 
31813  426 
apply (subst (1 2) abs_mult) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

427 
apply (rule gcd_mult_distrib_nat [transferred]) 
31706  428 
apply auto 
429 
done 

21256  430 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

431 
lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

432 
apply (insert gcd_mult_distrib_nat [of m k n]) 
21256  433 
apply simp 
434 
apply (erule_tac t = m in ssubst) 

435 
apply simp 

436 
done 

437 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

438 
lemma coprime_dvd_mult_int: 
31813  439 
"coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m" 
440 
apply (subst abs_dvd_iff [symmetric]) 

441 
apply (subst dvd_abs_iff [symmetric]) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

442 
apply (subst (asm) gcd_abs_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

443 
apply (rule coprime_dvd_mult_nat [transferred]) 
31813  444 
prefer 4 apply assumption 
445 
apply auto 

446 
apply (subst abs_mult [symmetric], auto) 

31706  447 
done 
448 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

449 
lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow> 
31706  450 
(k dvd m * n) = (k dvd m)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

451 
by (auto intro: coprime_dvd_mult_nat) 
31706  452 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

453 
lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow> 
31706  454 
(k dvd m * n) = (k dvd m)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

455 
by (auto intro: coprime_dvd_mult_int) 
31706  456 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

457 
lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n" 
21256  458 
apply (rule dvd_anti_sym) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

459 
apply (rule gcd_greatest_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

460 
apply (rule_tac n = k in coprime_dvd_mult_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

461 
apply (simp add: gcd_assoc_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

462 
apply (simp add: gcd_commute_nat) 
31706  463 
apply (simp_all add: mult_commute) 
464 
done 

21256  465 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

466 
lemma gcd_mult_cancel_int: 
31813  467 
"coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

468 
apply (subst (1 2) gcd_abs_int) 
31813  469 
apply (subst abs_mult) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

470 
apply (rule gcd_mult_cancel_nat [transferred], auto) 
31706  471 
done 
21256  472 

473 
text {* \medskip Addition laws *} 

474 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

475 
lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n" 
31706  476 
apply (case_tac "n = 0") 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

477 
apply (simp_all add: gcd_non_0_nat) 
31706  478 
done 
479 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

480 
lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

481 
apply (subst (1 2) gcd_commute_nat) 
31706  482 
apply (subst add_commute) 
483 
apply simp 

484 
done 

485 

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

487 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

488 
lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m  n) n = gcd m n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

489 
by (subst gcd_add1_nat [symmetric], auto) 
31706  490 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

491 
lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n  m) n = gcd m n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

492 
apply (subst gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

493 
apply (subst gcd_diff1_nat [symmetric]) 
31706  494 
apply auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

495 
apply (subst gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

496 
apply (subst gcd_diff1_nat) 
31706  497 
apply assumption 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

498 
apply (rule gcd_commute_nat) 
31706  499 
done 
500 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

501 
lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)" 
31706  502 
apply (frule_tac b = y and a = x in pos_mod_sign) 
503 
apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

504 
apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] 
31706  505 
zmod_zminus1_eq_if) 
506 
apply (frule_tac a = x in pos_mod_bound) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

507 
apply (subst (1 2) gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

508 
apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat 
31706  509 
nat_le_eq_zle) 
510 
done 

21256  511 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

512 
lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)" 
31706  513 
apply (case_tac "y = 0") 
514 
apply force 

515 
apply (case_tac "y > 0") 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

516 
apply (subst gcd_non_0_int, auto) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

517 
apply (insert gcd_non_0_int [of "y" "x"]) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

518 
apply (auto simp add: gcd_neg1_int gcd_neg2_int) 
31706  519 
done 
520 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

521 
lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

522 
by (metis gcd_red_int mod_add_self1 zadd_commute) 
31706  523 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

524 
lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

525 
by (metis gcd_add1_int gcd_commute_int zadd_commute) 
21256  526 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

527 
lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

528 
by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat) 
21256  529 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

530 
lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

531 
by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute) 
31798  532 

21256  533 

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

536 

31798  537 
(* FIXME remove iff *) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

538 
lemma gcd_dvd_prod_nat [iff]: "gcd (m::nat) n dvd k * n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

539 
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

540 

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

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

545 
proof 

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

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

548 
by(bestsimp intro!:dvd_imp_le) 

549 
qed 

550 

551 
lemma finite_divisors_int: 

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

553 
proof 

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

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

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

557 
by(bestsimp intro!:dvd_imp_le_int) 

558 
qed 

559 

560 
lemma gcd_is_Max_divisors_nat: 

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

562 
apply(rule Max_eqI[THEN sym]) 

563 
apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat) 

564 
apply simp 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

565 
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat) 
31734  566 
apply simp 
567 
done 

568 

569 
lemma gcd_is_Max_divisors_int: 

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

571 
apply(rule Max_eqI[THEN sym]) 

572 
apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int) 

573 
apply simp 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

574 
apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le) 
31734  575 
apply simp 
576 
done 

577 

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

578 

31706  579 
subsection {* Coprimality *} 
580 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

581 
lemma div_gcd_coprime_nat: 
31706  582 
assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0" 
583 
shows "coprime (a div gcd a b) (b div gcd a b)" 

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

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

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

589 
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

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

593 
unfolding dvd_def by blast 
31706  594 
then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" 
595 
by simp_all 

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

598 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

599 
have "?g \<noteq> 0" using nz by (simp add: gcd_zero_nat) 
31706  600 
then have gp: "?g > 0" by arith 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

601 
from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" . 
22367  602 
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

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

604 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

605 
lemma div_gcd_coprime_int: 
31706  606 
assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0" 
607 
shows "coprime (a div gcd a b) (b div gcd a b)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

608 
apply (subst (1 2 3) gcd_abs_int) 
31813  609 
apply (subst (1 2) abs_div) 
610 
apply simp 

611 
apply simp 

612 
apply(subst (1 2) abs_gcd_int) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

613 
apply (rule div_gcd_coprime_nat [transferred]) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

614 
using nz apply (auto simp add: gcd_abs_int [symmetric]) 
31706  615 
done 
616 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

617 
lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

618 
using gcd_unique_nat[of 1 a b, simplified] by auto 
31706  619 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

620 
lemma coprime_Suc_0_nat: 
31706  621 
"coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

622 
using coprime_nat by (simp add: One_nat_def) 
31706  623 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

624 
lemma coprime_int: "coprime (a::int) b \<longleftrightarrow> 
31706  625 
(\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

626 
using gcd_unique_int [of 1 a b] 
31706  627 
apply clarsimp 
628 
apply (erule subst) 

629 
apply (rule iffI) 

630 
apply force 

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

632 
apply (case_tac "e >= 0") 

633 
apply force 

634 
apply force 

635 
done 

636 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

637 
lemma gcd_coprime_nat: 
31706  638 
assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and 
639 
b: "b = b' * gcd a b" 

640 
shows "coprime a' b'" 

641 

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

643 
apply (erule ssubst) 

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

645 
apply (erule ssubst) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

646 
apply (rule div_gcd_coprime_nat) 
31706  647 
using prems 
648 
apply force 

649 
apply (subst (1) b) 

650 
using z apply force 

651 
apply (subst (1) a) 

652 
using z apply force 

653 
done 

654 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

655 
lemma gcd_coprime_int: 
31706  656 
assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and 
657 
b: "b = b' * gcd a b" 

658 
shows "coprime a' b'" 

659 

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

661 
apply (erule ssubst) 

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

663 
apply (erule ssubst) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

664 
apply (rule div_gcd_coprime_int) 
31706  665 
using prems 
666 
apply force 

667 
apply (subst (1) b) 

668 
using z apply force 

669 
apply (subst (1) a) 

670 
using z apply force 

671 
done 

672 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

673 
lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b" 
31706  674 
shows "coprime d (a * b)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

675 
apply (subst gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

676 
using da apply (subst gcd_mult_cancel_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

677 
apply (subst gcd_commute_nat, assumption) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

678 
apply (subst gcd_commute_nat, rule db) 
31706  679 
done 
680 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

681 
lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b" 
31706  682 
shows "coprime d (a * b)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

683 
apply (subst gcd_commute_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

684 
using da apply (subst gcd_mult_cancel_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

685 
apply (subst gcd_commute_int, assumption) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

686 
apply (subst gcd_commute_int, rule db) 
31706  687 
done 
688 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

689 
lemma coprime_lmult_nat: 
31706  690 
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" 
691 
proof  

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

693 
by (rule gcd_greatest_nat, auto) 
31706  694 
with dab show ?thesis 
695 
by auto 

696 
qed 

697 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

698 
lemma coprime_lmult_int: 
31798  699 
assumes "coprime (d::int) (a * b)" shows "coprime d a" 
31706  700 
proof  
701 
have "gcd d a dvd gcd d (a * b)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

702 
by (rule gcd_greatest_int, auto) 
31798  703 
with assms show ?thesis 
31706  704 
by auto 
705 
qed 

706 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

707 
lemma coprime_rmult_nat: 
31798  708 
assumes "coprime (d::nat) (a * b)" shows "coprime d b" 
31706  709 
proof  
710 
have "gcd d b dvd gcd d (a * b)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

711 
by (rule gcd_greatest_nat, auto intro: dvd_mult) 
31798  712 
with assms show ?thesis 
31706  713 
by auto 
714 
qed 

715 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

716 
lemma coprime_rmult_int: 
31706  717 
assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" 
718 
proof  

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

720 
by (rule gcd_greatest_int, auto intro: dvd_mult) 
31706  721 
with dab show ?thesis 
722 
by auto 

723 
qed 

724 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

725 
lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow> 
31706  726 
coprime d a \<and> coprime d b" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

727 
using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b] 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

728 
coprime_mult_nat[of d a b] 
31706  729 
by blast 
730 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

731 
lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow> 
31706  732 
coprime d a \<and> coprime d b" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

733 
using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b] 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

734 
coprime_mult_int[of d a b] 
31706  735 
by blast 
736 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

737 
lemma gcd_coprime_exists_nat: 
31706  738 
assumes nz: "gcd (a::nat) b \<noteq> 0" 
739 
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'" 

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

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

742 
using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult) 
31706  743 
done 
744 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

745 
lemma gcd_coprime_exists_int: 
31706  746 
assumes nz: "gcd (a::int) b \<noteq> 0" 
747 
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'" 

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

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

750 
using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self) 
31706  751 
done 
752 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

753 
lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

754 
by (induct n, simp_all add: coprime_mult_nat) 
31706  755 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

756 
lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

757 
by (induct n, simp_all add: coprime_mult_int) 
31706  758 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

759 
lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

760 
apply (rule coprime_exp_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

761 
apply (subst gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

762 
apply (rule coprime_exp_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

763 
apply (subst gcd_commute_nat, assumption) 
31706  764 
done 
765 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

766 
lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

767 
apply (rule coprime_exp_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

768 
apply (subst gcd_commute_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

769 
apply (rule coprime_exp_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

770 
apply (subst gcd_commute_int, assumption) 
31706  771 
done 
772 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

773 
lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n" 
31706  774 
proof (cases) 
775 
assume "a = 0 & b = 0" 

776 
thus ?thesis by simp 

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

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

779 
by (auto simp:div_gcd_coprime_nat) 
31706  780 
hence "gcd ((a div gcd a b)^n * (gcd a b)^n) 
781 
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" 

782 
apply (subst (1 2) mult_commute) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

783 
apply (subst gcd_mult_distrib_nat [symmetric]) 
31706  784 
apply simp 
785 
done 

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

787 
apply (subst div_power) 

788 
apply auto 

789 
apply (rule dvd_div_mult_self) 

790 
apply (rule dvd_power_same) 

791 
apply auto 

792 
done 

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

794 
apply (subst div_power) 

795 
apply auto 

796 
apply (rule dvd_div_mult_self) 

797 
apply (rule dvd_power_same) 

798 
apply auto 

799 
done 

800 
finally show ?thesis . 

801 
qed 

802 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

803 
lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

804 
apply (subst (1 2) gcd_abs_int) 
31706  805 
apply (subst (1 2) power_abs) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

806 
apply (rule gcd_exp_nat [where n = n, transferred]) 
31706  807 
apply auto 
808 
done 

809 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

810 
lemma coprime_divprod_nat: "(d::nat) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

811 
using coprime_dvd_mult_iff_nat[of d a b] 
31706  812 
by (auto simp add: mult_commute) 
813 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

814 
lemma coprime_divprod_int: "(d::int) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

815 
using coprime_dvd_mult_iff_int[of d a b] 
31706  816 
by (auto simp add: mult_commute) 
817 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

818 
lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c" 
31706  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" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

825 
from gcd_coprime_exists_nat[OF z] 
31706  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" using dvd_trans[of a' a "b*c"] by simp 

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

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

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

834 
from coprime_dvd_mult_nat[OF ab'(3)] th_1 
31706  835 
have thc: "a' dvd c" by (subst (asm) mult_commute, blast) 
836 
from ab' have "a = ?g*a'" by algebra 

837 
with thb thc have ?thesis by blast } 

838 
ultimately show ?thesis by blast 

839 
qed 

840 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

841 
lemma division_decomp_int: assumes dc: "(a::int) dvd b * c" 
31706  842 
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c" 
843 
proof 

844 
let ?g = "gcd a b" 

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

846 
moreover 

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

848 
from gcd_coprime_exists_int[OF z] 
31706  849 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
850 
by blast 

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

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

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

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

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

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

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

858 
from coprime_dvd_mult_int[OF ab'(3)] th_1 
31706  859 
have thc: "a' dvd c" by (subst (asm) mult_commute, blast) 
860 
from ab' have "a = ?g*a'" by algebra 

861 
with thb thc have ?thesis by blast } 

862 
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

863 
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

864 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

865 
lemma pow_divides_pow_nat: 
31706  866 
assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0" 
867 
shows "a dvd b" 

868 
proof 

869 
let ?g = "gcd a b" 

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

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

872 
moreover 

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

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

875 
from gcd_coprime_exists_nat[OF z] 
31706  876 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
877 
by blast 

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

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

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

881 
by (simp only: power_mult_distrib mult_commute) 

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

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

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

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

886 
from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1 
31706  887 
have "a' dvd b'" by (subst (asm) mult_commute, blast) 
888 
hence "a'*?g dvd b'*?g" by simp 

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

890 
ultimately show ?thesis by blast 

891 
qed 

892 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

893 
lemma pow_divides_pow_int: 
31706  894 
assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0" 
895 
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

896 
proof 
31706  897 
let ?g = "gcd a b" 
898 
from n obtain m where m: "n = Suc m" by (cases n, simp_all) 

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

900 
moreover 

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

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

903 
from gcd_coprime_exists_int[OF z] 
31706  904 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
905 
by blast 

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

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

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

909 
by (simp only: power_mult_distrib mult_commute) 

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

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

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

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

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

915 
from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1 
31706  916 
have "a' dvd b'" by (subst (asm) mult_commute, blast) 
917 
hence "a'*?g dvd b'*?g" by simp 

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

919 
ultimately show ?thesis by blast 

920 
qed 

921 

31798  922 
(* FIXME move to Divides(?) *) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

923 
lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

924 
by (auto intro: pow_divides_pow_nat dvd_power_same) 
31706  925 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

926 
lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

927 
by (auto intro: pow_divides_pow_int dvd_power_same) 
31706  928 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

929 
lemma divides_mult_nat: 
31706  930 
assumes mr: "(m::nat) 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) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

936 
hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp 
31706  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 

939 
qed 

940 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

941 
lemma divides_mult_int: 
31706  942 
assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n" 
943 
shows "m * n dvd r" 

944 
proof 

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

946 
unfolding dvd_def by blast 

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

948 
hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp 
31706  949 
then obtain k where k: "n' = m*k" unfolding dvd_def by blast 
950 
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

951 
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

952 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

953 
lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n" 
31706  954 
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1  n)") 
955 
apply force 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

956 
apply (rule dvd_diff_nat) 
31706  957 
apply auto 
958 
done 

959 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

960 
lemma coprime_Suc_nat [simp]: "coprime (Suc n) n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

961 
using coprime_plus_one_nat by (simp add: One_nat_def) 
31706  962 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

963 
lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n" 
31706  964 
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1  n)") 
965 
apply force 

966 
apply (rule dvd_diff) 

967 
apply auto 

968 
done 

969 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

970 
lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n  1) n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

971 
using coprime_plus_one_nat [of "n  1"] 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

972 
gcd_commute_nat [of "n  1" n] by auto 
31706  973 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

974 
lemma coprime_minus_one_int: "coprime ((n::int)  1) n" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

975 
using coprime_plus_one_int [of "n  1"] 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

976 
gcd_commute_int [of "n  1" n] by auto 
31706  977 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

978 
lemma setprod_coprime_nat [rule_format]: 
31706  979 
"(ALL i: A. coprime (f i) (x::nat)) > coprime (PROD i:A. f i) x" 
980 
apply (case_tac "finite A") 

981 
apply (induct set: finite) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

982 
apply (auto simp add: gcd_mult_cancel_nat) 
31706  983 
done 
984 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

985 
lemma setprod_coprime_int [rule_format]: 
31706  986 
"(ALL i: A. coprime (f i) (x::int)) > coprime (PROD i:A. f i) x" 
987 
apply (case_tac "finite A") 

988 
apply (induct set: finite) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

989 
apply (auto simp add: gcd_mult_cancel_int) 
31706  990 
done 
991 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

992 
lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" 
31706  993 
unfolding prime_nat_def 
994 
apply (subst even_mult_two_ex) 

995 
apply clarify 

996 
apply (drule_tac x = 2 in spec) 

997 
apply auto 

998 
done 

999 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1000 
lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" 
31706  1001 
unfolding prime_int_def 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1002 
apply (frule prime_odd_nat) 
31706  1003 
apply (auto simp add: even_nat_def) 
1004 
done 

1005 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1006 
lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> 
31706  1007 
x dvd b \<Longrightarrow> x = 1" 
1008 
apply (subgoal_tac "x dvd gcd a b") 

1009 
apply simp 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1010 
apply (erule (1) gcd_greatest_nat) 
31706  1011 
done 
1012 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1013 
lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> 
31706  1014 
x dvd b \<Longrightarrow> abs x = 1" 
1015 
apply (subgoal_tac "x dvd gcd a b") 

1016 
apply simp 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1017 
apply (erule (1) gcd_greatest_int) 
31706  1018 
done 
1019 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1020 
lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> 
31706  1021 
coprime d e" 
1022 
apply (auto simp add: dvd_def) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1023 
apply (frule coprime_lmult_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1024 
apply (subst gcd_commute_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1025 
apply (subst (asm) (2) gcd_commute_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1026 
apply (erule coprime_lmult_int) 
31706  1027 
done 
1028 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1029 
lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1030 
apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat) 
31706  1031 
done 
1032 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1033 
lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1034 
apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int) 
31706  1035 
done 
1036 

1037 

1038 
subsection {* Bezout's theorem *} 

1039 

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

1041 
see the theorems that follow the definition. *) 

1042 
fun 

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

1044 
where 

1045 
"bezw x y = 

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

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

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

1049 

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

1051 

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

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

1054 
by simp 

1055 

1056 
declare bezw.simps [simp del] 

1057 

1058 
lemma bezw_aux [rule_format]: 

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1060 
proof (induct x y rule: gcd_nat_induct) 
31706  1061 
fix m :: nat 
1062 
show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)" 

1063 
by auto 

1064 
next fix m :: nat and n 

1065 
assume ngt0: "n > 0" and 

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

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

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

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1070 
apply (simp add: bezw_non_0 gcd_non_0_nat) 
31706  1071 
apply (erule subst) 
1072 
apply (simp add: ring_simps) 

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

1074 
(* applying simp here undoes the last substitution! 

1075 
what is procedure cancel_div_mod? *) 

1076 
apply (simp only: ring_simps zadd_int [symmetric] 

1077 
zmult_int [symmetric]) 

1078 
done 

1079 
qed 

1080 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1081 
lemma bezout_int: 
31706  1082 
fixes x y 
1083 
shows "EX u v. u * (x::int) + v * y = gcd x y" 

1084 
proof  

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

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

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

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

1089 
apply (unfold gcd_int_def) 

1090 
apply simp 

1091 
apply (subst bezw_aux [symmetric]) 

1092 
apply auto 

1093 
done 

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

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

1096 
by auto 

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

1098 
by (erule (1) bezout_aux) 

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

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

1101 
apply auto 

1102 
apply (rule_tac x = u in exI) 

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1104 
apply (subst gcd_neg2_int [symmetric]) 
31706  1105 
apply auto 
1106 
done 

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

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

1109 
apply auto 

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

1111 
apply (rule_tac x = v in exI) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1112 
apply (subst gcd_neg1_int [symmetric]) 
31706  1113 
apply auto 
1114 
done 

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

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

1117 
apply auto 

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

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

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1120 
apply (subst gcd_neg1_int [symmetric]) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1121 
apply (subst gcd_neg2_int [symmetric]) 
31706  1122 
apply auto 
1123 
done 

1124 
ultimately show ?thesis by blast 

1125 
qed 

1126 

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

1128 

1129 
lemma ind_euclid: 

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

1131 
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

1132 
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

1133 
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

1134 
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

1135 
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

1136 
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

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

1140 
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

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

1142 
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

1143 
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

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

1145 
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

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

1147 
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

1148 
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

1149 
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

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

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

1153 
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

1154 
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

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

1156 
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

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

1158 
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

1159 
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

1160 
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

1161 
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

1162 
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

1163 
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

1164 
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

1165 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1166 
lemma bezout_lemma_nat: 
31706  1167 
assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> 
1168 
(a * x = b * y + d \<or> b * x = a * y + d)" 

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

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

1171 
using ex 

1172 
apply clarsimp 

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

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

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

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

1177 
apply algebra 

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

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

1180 
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

1181 
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

1182 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1183 
lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> 
31706  1184 
(a * x = b * y + d \<or> b * x = a * y + d)" 
1185 
apply(induct a b rule: ind_euclid) 

1186 
apply blast 

1187 
apply clarify 

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

1189 
apply clarsimp 

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

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

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

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

1194 
apply algebra 

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

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

1197 
apply algebra 

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

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

1199 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1200 
lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> 
31706  1201 
(a * x  b * y = d \<or> b * x  a * y = d)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1202 
using bezout_add_nat[of a b] 
31706  1203 
apply clarsimp 
1204 
apply (rule_tac x="d" in exI, simp) 

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

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

1207 
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

1208 
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

1209 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1210 
lemma bezout_add_strong_nat: 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

1211 
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

1212 
proof 
31706  1213 
from nz have ap: "a > 0" by simp 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1214 
from bezout_add_nat[of a b] 
31706  1215 
have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or> 
1216 
(\<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

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

1220 
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

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

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

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

1227 
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

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

1229 
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

1230 
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

1231 
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

1232 
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

1233 
moreover 
31706  1234 
{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

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

1236 
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

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

1238 
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

1239 
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

1240 
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

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

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

1245 
by (simp only: mult_assoc right_distrib) 

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

1247 
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

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

1250 
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

1251 
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

1252 
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

1253 
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

1254 
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

1255 
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

1256 
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

1257 
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

1258 
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

1259 
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

1260 
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

1261 
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

1262 
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

1263 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1264 
lemma bezout_nat: 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

1265 
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

1266 
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

1267 
let ?g = "gcd a b" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1268 
from bezout_add_strong_nat[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

1269 
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

1270 
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

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

1273 
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

1274 
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

1275 
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

1276 

31706  1277 

1278 
subsection {* LCM *} 

1279 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1280 
lemma lcm_altdef_int: "lcm (a::int) b = (abs a) * (abs b) div gcd a b" 
31706  1281 
by (simp add: lcm_int_def lcm_nat_def zdiv_int 
1282 
zmult_int [symmetric] gcd_int_def) 

1283 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1284 
lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n" 
31706  1285 
unfolding lcm_nat_def 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1286 
by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat]) 
31706  1287 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1288 
lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n" 
31706  1289 
unfolding lcm_int_def gcd_int_def 
1290 
apply (subst int_mult [symmetric]) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1291 
apply (subst prod_gcd_lcm_nat [symmetric]) 
31706  1292 
apply (subst nat_abs_mult_distrib [symmetric]) 
1293 
apply (simp, simp add: abs_mult) 

1294 
done 

1295 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1296 
lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0" 
31706  1297 
unfolding lcm_nat_def by simp 
1298 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1299 
lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0" 
31706  1300 
unfolding lcm_int_def by simp 
1301 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1302 
lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0" 
31706  1303 
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

1304 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1305 
lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0" 
31706  1306 
unfolding lcm_int_def by simp 
1307 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1308 
lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1309 
unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps) 
31706  1310 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1311 
lemma lcm_commute_int: "lcm (m::int) n = lcm n m" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1312 
unfolding lcm_int_def by (subst lcm_commute_nat, rule refl) 
31706  1313 

1314 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1315 
lemma lcm_pos_nat: 
31798  1316 
"(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1317 
by (metis gr0I mult_is_0 prod_gcd_lcm_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

1318 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1319 
lemma lcm_pos_int: 
31798  1320 
"(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1321 
apply (subst lcm_abs_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1322 
apply (rule lcm_pos_nat [transferred]) 
31798  1323 
apply auto 
31706  1324 
done 
23687 