author  nipkow 
Wed, 15 Jul 2009 20:34:58 +0200  
changeset 32007  a2a3685f61c3 
parent 31996  1d93369079c4 
child 32045  efc5f4806cd5 
permissions  rwrr 
31706  1 
(* Title: GCD.thy 
2 
Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, 

31798  3 
Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow 
31706  4 

5 

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

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

8 
numbers and integers. 

9 

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

11 

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

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

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

15 

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

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

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

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

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

21 
the natural numbers by Chiaeb. 

22 

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

31706  26 

27 
header {* GCD *} 

21256  28 

29 
theory GCD 

31706  30 
imports NatTransfer 
31 
begin 

32 

33 
declare One_nat_def [simp del] 

34 

35 
subsection {* gcd *} 

36 

31992  37 
class gcd = zero + one + dvd + 
31706  38 

39 
fixes 

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

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

42 

21256  43 
begin 
44 

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

47 
where 

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

49 

50 
end 

51 

52 
class prime = one + 

53 

54 
fixes 

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

56 

57 

58 
(* definitions for the natural numbers *) 

59 

60 
instantiation nat :: gcd 

61 

62 
begin 

21256  63 

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

66 
where 

67 
"gcd_nat x y = 

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

69 

70 
definition 

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

72 
where 

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

74 

75 
instance proof qed 

76 

77 
end 

78 

79 

80 
instantiation nat :: prime 

81 

82 
begin 

21256  83 

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

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

89 
instance proof qed 

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

90 

31706  91 
end 
92 

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

93 

31706  94 
(* definitions for the integers *) 
95 

96 
instantiation int :: gcd 

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

97 

31706  98 
begin 
21256  99 

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

102 
where 

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

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

104 

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

107 
where 

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

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

109 

31706  110 
instance proof qed 
111 

112 
end 

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

113 

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

114 

31706  115 
instantiation int :: prime 
116 

117 
begin 

118 

119 
definition 

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

121 
where 

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

124 
instance proof qed 

125 

126 
end 

127 

128 

129 
subsection {* Set up Transfer *} 

130 

131 

132 
lemma transfer_nat_int_gcd: 

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

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

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

136 
unfolding gcd_int_def lcm_int_def prime_int_def 

137 
by auto 

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

138 

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

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

142 
by (auto simp add: gcd_int_def lcm_int_def) 

143 

144 
declare TransferMorphism_nat_int[transfer add return: 

145 
transfer_nat_int_gcd transfer_nat_int_gcd_closures] 

146 

147 
lemma transfer_int_nat_gcd: 

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

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

150 
"prime (int x) = prime x" 

151 
by (unfold gcd_int_def lcm_int_def prime_int_def, auto) 

152 

153 
lemma transfer_int_nat_gcd_closures: 

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

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

156 
by (auto simp add: gcd_int_def lcm_int_def) 

157 

158 
declare TransferMorphism_int_nat[transfer add return: 

159 
transfer_int_nat_gcd transfer_int_nat_gcd_closures] 

160 

161 

162 
subsection {* GCD *} 

163 

164 
(* was gcd_induct *) 

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

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

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

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

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

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

172 
using assms apply simp_all 

173 
done 

174 

175 
(* specific to int *) 

176 

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

177 
lemma gcd_neg1_int [simp]: "gcd (x::int) y = gcd x y" 
31706  178 
by (simp add: gcd_int_def) 
179 

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

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

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

185 

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

186 
lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)" 
31813  187 
by (simp add: gcd_int_def) 
188 

189 
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

190 
by (metis abs_idempotent gcd_abs_int) 
31813  191 

192 
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

193 
by (metis abs_idempotent gcd_abs_int) 
31706  194 

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

195 
lemma gcd_cases_int: 
31706  196 
fixes x :: int and y 
197 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)" 

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

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

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

201 
shows "P (gcd x y)" 

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

202 
by (insert prems, auto simp add: gcd_neg1_int gcd_neg2_int, arith) 
21256  203 

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

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

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

207 
lemma lcm_neg1_int: "lcm (x::int) y = lcm x y" 
31706  208 
by (simp add: lcm_int_def) 
209 

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

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

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

213 
lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)" 
31706  214 
by (simp add: lcm_int_def) 
21256  215 

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

218 

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

220 
by (metis abs_idempotent lcm_int_def) 

221 

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

223 
by (metis abs_idempotent lcm_int_def) 

224 

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

225 
lemma lcm_cases_int: 
31706  226 
fixes x :: int and y 
227 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)" 

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

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

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

231 
shows "P (lcm x y)" 

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

232 
by (insert prems, auto simp add: lcm_neg1_int lcm_neg2_int, arith) 
31706  233 

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

234 
lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0" 
31706  235 
by (simp add: lcm_int_def) 
236 

237 
(* was gcd_0, etc. *) 

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

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

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

240 

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

242 
lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x" 
31706  243 
by (unfold gcd_int_def, auto) 
244 

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

245 
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

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

247 

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

248 
lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x" 
31706  249 
by (unfold gcd_int_def, auto) 
250 

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

251 
lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)" 
31706  252 
by (case_tac "y = 0", auto) 
253 

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

255 

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

256 
lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)" 
31706  257 
by simp 
258 

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

259 
lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1" 
21263  260 
by simp 
21256  261 

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

262 
lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" 
31706  263 
by (simp add: One_nat_def) 
264 

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

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

267 

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

268 
lemma gcd_idem_nat: "gcd (x::nat) x = x" 
31798  269 
by simp 
31706  270 

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

271 
lemma gcd_idem_int: "gcd (x::int) x = abs x" 
31813  272 
by (auto simp add: gcd_int_def) 
31706  273 

274 
declare gcd_nat.simps [simp del] 

21256  275 

276 
text {* 

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

280 

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

281 
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

282 
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

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

284 
apply (simp_all add: gcd_non_0_nat) 
21256  285 
apply (blast dest: dvd_mod_imp_dvd) 
31706  286 
done 
287 

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

288 
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

289 
by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat) 
21256  290 

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

291 
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

292 
by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat) 
31706  293 

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

295 
by(metis gcd_dvd1_nat dvd_trans) 
31730  296 

297 
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

298 
by(metis gcd_dvd2_nat dvd_trans) 
31730  299 

300 
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

301 
by(metis gcd_dvd1_int dvd_trans) 
31730  302 

303 
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

304 
by(metis gcd_dvd2_int dvd_trans) 
31730  305 

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

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

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

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

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

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

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

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

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

318 
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

319 
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod) 
31706  320 

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

321 
lemma gcd_greatest_int: 
31813  322 
"(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

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

325 
apply (rule gcd_greatest_nat [transferred]) 
31813  326 
apply auto 
31706  327 
done 
21256  328 

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

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

331 
by (blast intro!: gcd_greatest_nat intro: dvd_trans) 
31706  332 

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

333 
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

334 
by (blast intro!: gcd_greatest_int intro: dvd_trans) 
21256  335 

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

336 
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

337 
by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat) 
21256  338 

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

339 
lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)" 
31706  340 
by (auto simp add: gcd_int_def) 
21256  341 

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

342 
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

343 
by (insert gcd_zero_nat [of m n], arith) 
21256  344 

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

345 
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

346 
by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith) 
31706  347 

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

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

350 

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

351 
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

352 
by (auto simp add: gcd_int_def gcd_commute_nat) 
31706  353 

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

354 
lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)" 
31706  355 
apply (rule dvd_anti_sym) 
356 
apply (blast intro: dvd_trans)+ 

357 
done 

21256  358 

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

359 
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

360 
by (auto simp add: gcd_int_def gcd_assoc_nat) 
31706  361 

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

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

363 
mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat] 
31706  364 

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

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

366 
mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int] 
31706  367 

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

368 
lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat 
31706  369 
 {* gcd is an ACoperator *} 
21256  370 

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

371 
lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int 
31706  372 

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

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

376 
apply (rule dvd_anti_sym) 

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

377 
apply (erule (1) gcd_greatest_nat) 
31706  378 
apply auto 
379 
done 

21256  380 

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

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

384 
apply force 

385 
apply (rule iffI) 

386 
apply (rule zdvd_anti_sym) 

387 
apply arith 

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

388 
apply (subst gcd_pos_int) 
31706  389 
apply clarsimp 
390 
apply (drule_tac x = "d + 1" in spec) 

391 
apply (frule zdvd_imp_le) 

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

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

394 

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

396 
by (metis dvd.eq_iff gcd_unique_nat) 
31798  397 

398 
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

399 
by (metis dvd.eq_iff gcd_unique_nat) 
31798  400 

401 
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

402 
by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int) 
31798  403 

404 
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

405 
by (metis gcd_proj1_if_dvd_int gcd_commute_int) 
31798  406 

407 

21256  408 
text {* 
409 
\medskip Multiplication laws 

410 
*} 

411 

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

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

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

417 
apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2) 
31706  418 
done 
21256  419 

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

420 
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

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

423 
apply (rule gcd_mult_distrib_nat [transferred]) 
31706  424 
apply auto 
425 
done 

21256  426 

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

427 
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

428 
apply (insert gcd_mult_distrib_nat [of m k n]) 
21256  429 
apply simp 
430 
apply (erule_tac t = m in ssubst) 

431 
apply simp 

432 
done 

433 

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

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

437 
apply (subst dvd_abs_iff [symmetric]) 

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

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

439 
apply (rule coprime_dvd_mult_nat [transferred]) 
31813  440 
prefer 4 apply assumption 
441 
apply auto 

442 
apply (subst abs_mult [symmetric], auto) 

31706  443 
done 
444 

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

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

447 
by (auto intro: coprime_dvd_mult_nat) 
31706  448 

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

449 
lemma coprime_dvd_mult_iff_int: "coprime (k::int) 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_int) 
31706  452 

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

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

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

456 
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

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

458 
apply (simp add: gcd_commute_nat) 
31706  459 
apply (simp_all add: mult_commute) 
460 
done 

21256  461 

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

462 
lemma gcd_mult_cancel_int: 
31813  463 
"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

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

466 
apply (rule gcd_mult_cancel_nat [transferred], auto) 
31706  467 
done 
21256  468 

469 
text {* \medskip Addition laws *} 

470 

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

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

473 
apply (simp_all add: gcd_non_0_nat) 
31706  474 
done 
475 

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

476 
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

477 
apply (subst (1 2) gcd_commute_nat) 
31706  478 
apply (subst add_commute) 
479 
apply simp 

480 
done 

481 

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

483 

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

484 
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

485 
by (subst gcd_add1_nat [symmetric], auto) 
31706  486 

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

487 
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

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

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

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

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

494 
apply (rule gcd_commute_nat) 
31706  495 
done 
496 

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

497 
lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)" 
31706  498 
apply (frule_tac b = y and a = x in pos_mod_sign) 
499 
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

500 
apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] 
31706  501 
zmod_zminus1_eq_if) 
502 
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

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

504 
apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat 
31706  505 
nat_le_eq_zle) 
506 
done 

21256  507 

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

508 
lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)" 
31706  509 
apply (case_tac "y = 0") 
510 
apply force 

511 
apply (case_tac "y > 0") 

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

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

513 
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

514 
apply (auto simp add: gcd_neg1_int gcd_neg2_int) 
31706  515 
done 
516 

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

517 
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

518 
by (metis gcd_red_int mod_add_self1 zadd_commute) 
31706  519 

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

520 
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

521 
by (metis gcd_add1_int gcd_commute_int zadd_commute) 
21256  522 

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

523 
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

524 
by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat) 
21256  525 

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

526 
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

527 
by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute) 
31798  528 

21256  529 

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

532 

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

534 
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

535 
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

536 

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

31992  539 
lemma finite_divisors_nat[simp]: 
540 
assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}" 

31734  541 
proof 
542 
have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite) 

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

544 
by(bestsimp intro!:dvd_imp_le) 

545 
qed 

546 

31995  547 
lemma finite_divisors_int[simp]: 
31734  548 
assumes "(i::int) ~= 0" shows "finite{d. d dvd i}" 
549 
proof 

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

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

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

553 
by(bestsimp intro!:dvd_imp_le_int) 

554 
qed 

555 

31995  556 
lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n" 
557 
apply(rule antisym) 

558 
apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le) 

559 
apply simp 

560 
done 

561 

562 
lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n" 

563 
apply(rule antisym) 

564 
apply(rule Max_le_iff[THEN iffD2]) 

565 
apply simp 

566 
apply fastsimp 

567 
apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans) 

568 
apply simp 

569 
done 

570 

31734  571 
lemma gcd_is_Max_divisors_nat: 
572 
"m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})" 

573 
apply(rule Max_eqI[THEN sym]) 

31995  574 
apply (metis finite_Collect_conjI finite_divisors_nat) 
31734  575 
apply simp 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

576 
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat) 
31734  577 
apply simp 
578 
done 

579 

580 
lemma gcd_is_Max_divisors_int: 

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

582 
apply(rule Max_eqI[THEN sym]) 

31995  583 
apply (metis finite_Collect_conjI finite_divisors_int) 
31734  584 
apply simp 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

585 
apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le) 
31734  586 
apply simp 
587 
done 

588 

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

589 

31706  590 
subsection {* Coprimality *} 
591 

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

592 
lemma div_gcd_coprime_nat: 
31706  593 
assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0" 
594 
shows "coprime (a div gcd a b) (b div gcd a b)" 

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

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

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

600 
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

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

604 
unfolding dvd_def by blast 
31706  605 
then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" 
606 
by simp_all 

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

609 
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

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

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

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

615 

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

616 
lemma div_gcd_coprime_int: 
31706  617 
assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0" 
618 
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

619 
apply (subst (1 2 3) gcd_abs_int) 
31813  620 
apply (subst (1 2) abs_div) 
621 
apply simp 

622 
apply simp 

623 
apply(subst (1 2) abs_gcd_int) 

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

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

625 
using nz apply (auto simp add: gcd_abs_int [symmetric]) 
31706  626 
done 
627 

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

628 
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

629 
using gcd_unique_nat[of 1 a b, simplified] by auto 
31706  630 

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

631 
lemma coprime_Suc_0_nat: 
31706  632 
"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

633 
using coprime_nat by (simp add: One_nat_def) 
31706  634 

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

635 
lemma coprime_int: "coprime (a::int) b \<longleftrightarrow> 
31706  636 
(\<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

637 
using gcd_unique_int [of 1 a b] 
31706  638 
apply clarsimp 
639 
apply (erule subst) 

640 
apply (rule iffI) 

641 
apply force 

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

643 
apply (case_tac "e >= 0") 

644 
apply force 

645 
apply force 

646 
done 

647 

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

648 
lemma gcd_coprime_nat: 
31706  649 
assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and 
650 
b: "b = b' * gcd a b" 

651 
shows "coprime a' b'" 

652 

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

654 
apply (erule ssubst) 

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

656 
apply (erule ssubst) 

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

657 
apply (rule div_gcd_coprime_nat) 
31706  658 
using prems 
659 
apply force 

660 
apply (subst (1) b) 

661 
using z apply force 

662 
apply (subst (1) a) 

663 
using z apply force 

664 
done 

665 

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

666 
lemma gcd_coprime_int: 
31706  667 
assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and 
668 
b: "b = b' * gcd a b" 

669 
shows "coprime a' b'" 

670 

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

672 
apply (erule ssubst) 

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

674 
apply (erule ssubst) 

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

675 
apply (rule div_gcd_coprime_int) 
31706  676 
using prems 
677 
apply force 

678 
apply (subst (1) b) 

679 
using z apply force 

680 
apply (subst (1) a) 

681 
using z apply force 

682 
done 

683 

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

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

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

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

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

689 
apply (subst gcd_commute_nat, rule db) 
31706  690 
done 
691 

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

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

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

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

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

697 
apply (subst gcd_commute_int, rule db) 
31706  698 
done 
699 

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

700 
lemma coprime_lmult_nat: 
31706  701 
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" 
702 
proof  

703 
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

704 
by (rule gcd_greatest_nat, auto) 
31706  705 
with dab show ?thesis 
706 
by auto 

707 
qed 

708 

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

709 
lemma coprime_lmult_int: 
31798  710 
assumes "coprime (d::int) (a * b)" shows "coprime d a" 
31706  711 
proof  
712 
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

713 
by (rule gcd_greatest_int, auto) 
31798  714 
with assms show ?thesis 
31706  715 
by auto 
716 
qed 

717 

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

718 
lemma coprime_rmult_nat: 
31798  719 
assumes "coprime (d::nat) (a * b)" shows "coprime d b" 
31706  720 
proof  
721 
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

722 
by (rule gcd_greatest_nat, auto intro: dvd_mult) 
31798  723 
with assms show ?thesis 
31706  724 
by auto 
725 
qed 

726 

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

727 
lemma coprime_rmult_int: 
31706  728 
assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" 
729 
proof  

730 
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

731 
by (rule gcd_greatest_int, auto intro: dvd_mult) 
31706  732 
with dab show ?thesis 
733 
by auto 

734 
qed 

735 

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

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

738 
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

739 
coprime_mult_nat[of d a b] 
31706  740 
by blast 
741 

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

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

744 
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

745 
coprime_mult_int[of d a b] 
31706  746 
by blast 
747 

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

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

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

752 
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

753 
using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult) 
31706  754 
done 
755 

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

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

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

760 
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

761 
using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self) 
31706  762 
done 
763 

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

764 
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

765 
by (induct n, simp_all add: coprime_mult_nat) 
31706  766 

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

767 
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

768 
by (induct n, simp_all add: coprime_mult_int) 
31706  769 

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

770 
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

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

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

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

774 
apply (subst gcd_commute_nat, assumption) 
31706  775 
done 
776 

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

777 
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

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

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

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

781 
apply (subst gcd_commute_int, assumption) 
31706  782 
done 
783 

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

784 
lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n" 
31706  785 
proof (cases) 
786 
assume "a = 0 & b = 0" 

787 
thus ?thesis by simp 

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

789 
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

790 
by (auto simp:div_gcd_coprime_nat) 
31706  791 
hence "gcd ((a div gcd a b)^n * (gcd a b)^n) 
792 
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" 

793 
apply (subst (1 2) mult_commute) 

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

794 
apply (subst gcd_mult_distrib_nat [symmetric]) 
31706  795 
apply simp 
796 
done 

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

798 
apply (subst div_power) 

799 
apply auto 

800 
apply (rule dvd_div_mult_self) 

801 
apply (rule dvd_power_same) 

802 
apply auto 

803 
done 

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

805 
apply (subst div_power) 

806 
apply auto 

807 
apply (rule dvd_div_mult_self) 

808 
apply (rule dvd_power_same) 

809 
apply auto 

810 
done 

811 
finally show ?thesis . 

812 
qed 

813 

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

814 
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

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

817 
apply (rule gcd_exp_nat [where n = n, transferred]) 
31706  818 
apply auto 
819 
done 

820 

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

821 
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

822 
using coprime_dvd_mult_iff_nat[of d a b] 
31706  823 
by (auto simp add: mult_commute) 
824 

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

825 
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

826 
using coprime_dvd_mult_iff_int[of d a b] 
31706  827 
by (auto simp add: mult_commute) 
828 

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

829 
lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c" 
31706  830 
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c" 
831 
proof 

832 
let ?g = "gcd a b" 

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

834 
moreover 

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

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

836 
from gcd_coprime_exists_nat[OF z] 
31706  837 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
838 
by blast 

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

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

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

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

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

844 
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

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

848 
with thb thc have ?thesis by blast } 

849 
ultimately show ?thesis by blast 

850 
qed 

851 

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

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

855 
let ?g = "gcd a b" 

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

857 
moreover 

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

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

859 
from gcd_coprime_exists_int[OF z] 
31706  860 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
861 
by blast 

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

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

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

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

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

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

868 
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

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

872 
with thb thc have ?thesis by blast } 

873 
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

874 
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

875 

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

876 
lemma pow_divides_pow_nat: 
31706  877 
assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0" 
878 
shows "a dvd b" 

879 
proof 

880 
let ?g = "gcd a b" 

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

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

883 
moreover 

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

885 
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

886 
from gcd_coprime_exists_nat[OF z] 
31706  887 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
888 
by blast 

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

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

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

892 
by (simp only: power_mult_distrib mult_commute) 

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

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

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

896 
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

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

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

901 
ultimately show ?thesis by blast 

902 
qed 

903 

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

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

907 
proof 
31706  908 
let ?g = "gcd a b" 
909 
from n obtain m where m: "n = Suc m" by (cases n, simp_all) 

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

911 
moreover 

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

913 
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

914 
from gcd_coprime_exists_int[OF z] 
31706  915 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
916 
by blast 

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

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

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

920 
by (simp only: power_mult_distrib mult_commute) 

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

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

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

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

925 
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

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

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

930 
ultimately show ?thesis by blast 

931 
qed 

932 

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

934 
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

935 
by (auto intro: pow_divides_pow_nat dvd_power_same) 
31706  936 

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

937 
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

938 
by (auto intro: pow_divides_pow_int dvd_power_same) 
31706  939 

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

940 
lemma divides_mult_nat: 
31706  941 
assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n" 
942 
shows "m * n dvd r" 

943 
proof 

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

945 
unfolding dvd_def by blast 

946 
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

947 
hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp 
31706  948 
then obtain k where k: "n' = m*k" unfolding dvd_def by blast 
949 
from n' k show ?thesis unfolding dvd_def by auto 

950 
qed 

951 

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

952 
lemma divides_mult_int: 
31706  953 
assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n" 
954 
shows "m * n dvd r" 

955 
proof 

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

957 
unfolding dvd_def by blast 

958 
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

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

962 
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

963 

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

964 
lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n" 
31706  965 
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1  n)") 
966 
apply force 

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

967 
apply (rule dvd_diff_nat) 
31706  968 
apply auto 
969 
done 

970 

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

971 
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

972 
using coprime_plus_one_nat by (simp add: One_nat_def) 
31706  973 

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

974 
lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n" 
31706  975 
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1  n)") 
976 
apply force 

977 
apply (rule dvd_diff) 

978 
apply auto 

979 
done 

980 

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

981 
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

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

983 
gcd_commute_nat [of "n  1" n] by auto 
31706  984 

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

985 
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

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

987 
gcd_commute_int [of "n  1" n] by auto 
31706  988 

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

989 
lemma setprod_coprime_nat [rule_format]: 
31706  990 
"(ALL i: A. coprime (f i) (x::nat)) > coprime (PROD i:A. f i) x" 
991 
apply (case_tac "finite A") 

992 
apply (induct set: finite) 

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

993 
apply (auto simp add: gcd_mult_cancel_nat) 
31706  994 
done 
995 

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

996 
lemma setprod_coprime_int [rule_format]: 
31706  997 
"(ALL i: A. coprime (f i) (x::int)) > coprime (PROD i:A. f i) x" 
998 
apply (case_tac "finite A") 

999 
apply (induct set: finite) 

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

1000 
apply (auto simp add: gcd_mult_cancel_int) 
31706  1001 
done 
1002 

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

1003 
lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" 
31706  1004 
unfolding prime_nat_def 
1005 
apply (subst even_mult_two_ex) 

1006 
apply clarify 

1007 
apply (drule_tac x = 2 in spec) 

1008 
apply auto 

1009 
done 

1010 

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

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

1013 
apply (frule prime_odd_nat) 
31706  1014 
apply (auto simp add: even_nat_def) 
1015 
done 

1016 

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

1017 
lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> 
31706  1018 
x dvd b \<Longrightarrow> x = 1" 
1019 
apply (subgoal_tac "x dvd gcd a b") 

1020 
apply simp 

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

1021 
apply (erule (1) gcd_greatest_nat) 
31706  1022 
done 
1023 

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

1024 
lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> 
31706  1025 
x dvd b \<Longrightarrow> abs x = 1" 
1026 
apply (subgoal_tac "x dvd gcd a b") 

1027 
apply simp 

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

1028 
apply (erule (1) gcd_greatest_int) 
31706  1029 
done 
1030 

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

1031 
lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> 
31706  1032 
coprime d e" 
1033 
apply (auto simp add: dvd_def) 

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

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

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

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

1037 
apply (erule coprime_lmult_int) 
31706  1038 
done 
1039 

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

1040 
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

1041 
apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat) 
31706  1042 
done 
1043 

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

1044 
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

1045 
apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int) 
31706  1046 
done 
1047 

1048 

1049 
subsection {* Bezout's theorem *} 

1050 

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

1052 
see the theorems that follow the definition. *) 

1053 
fun 

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

1055 
where 

1056 
"bezw x y = 

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

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

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

1060 

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

1062 

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

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

1065 
by simp 

1066 

1067 
declare bezw.simps [simp del] 

1068 

1069 
lemma bezw_aux [rule_format]: 

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

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

1074 
by auto 

1075 
next fix m :: nat and n 

1076 
assume ngt0: "n > 0" and 

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

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

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

1080 
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

1081 
apply (simp add: bezw_non_0 gcd_non_0_nat) 
31706  1082 
apply (erule subst) 
1083 
apply (simp add: ring_simps) 

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

1085 
(* applying simp here undoes the last substitution! 

1086 
what is procedure cancel_div_mod? *) 

1087 
apply (simp only: ring_simps zadd_int [symmetric] 

1088 
zmult_int [symmetric]) 

1089 
done 

1090 
qed 

1091 

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

1092 
lemma bezout_int: 
31706  1093 
fixes x y 
1094 
shows "EX u v. u * (x::int) + v * y = gcd x y" 

1095 
proof  

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

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

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

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

1100 
apply (unfold gcd_int_def) 

1101 
apply simp 

1102 
apply (subst bezw_aux [symmetric]) 

1103 
apply auto 

1104 
done 

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

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

1107 
by auto 

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

1109 
by (erule (1) bezout_aux) 

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

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

1112 
apply auto 

1113 
apply (rule_tac x = u in exI) 

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

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

1115 
apply (subst gcd_neg2_int [symmetric]) 
31706  1116 
apply auto 
1117 
done 

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

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

1120 
apply auto 

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

1122 
apply (rule_tac x = v in exI) 

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

1123 
apply (subst gcd_neg1_int [symmetric]) 
31706  1124 
apply auto 
1125 
done 

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

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

1128 
apply auto 

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

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

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

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

1132 
apply (subst gcd_neg2_int [symmetric]) 
31706  1133 
apply auto 
1134 
done 

1135 
ultimately show ?thesis by blast 

1136 
qed 

1137 

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

1139 

1140 
lemma ind_euclid: 

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

1142 
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

1143 
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

1144 
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

1145 
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

1146 
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

1147 
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

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

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

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

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

1158 
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

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

1161 
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

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

1163 
{assume 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

1164 
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

1165 
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

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

1167 
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

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

1169 
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

1170 
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

1171 
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

1172 
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

1173 
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

1174 
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

1175 
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

1176 

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

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

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

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

1182 
using ex 

1183 
apply clarsimp 

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

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

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

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

1188 
apply algebra 

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

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

1191 
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

1192 
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

1193 

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

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

1197 
apply blast 

1198 
apply clarify 

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

1200 
apply clarsimp 

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

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

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

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

1205 
apply algebra 

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

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

1208 
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

1209 
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

1210 

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

1211 
lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> 
31706  1212 
(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

1213 
using bezout_add_nat[of a b] 
31706  1214 
apply clarsimp 
1215 
apply (rule_tac x="d" in exI, simp) 

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

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

1218 
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

1219 
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

1220 

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

1221 
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

1222 
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

1223 
proof 
31706  1224 
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

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

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

1231 
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

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

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

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

1238 
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

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

1240 
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

1241 
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

1242 
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

1243 
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

1244 
moreover 
31706  1245 
{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

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

1247 
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

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

1249 
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

1250 
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

1251 
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

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

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

1256 
by (simp only: mult_assoc right_distrib) 

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

1258 
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

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

1261 
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

1262 
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

1263 
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

1264 
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

1265 
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

1266 
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

1267 
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

1268 
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

1269 
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

1270 
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

1271 
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

1272 
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

1273 
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

1274 

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

1275 
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

1276 
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

1277 
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

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

1279 
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

1280 
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

1281 
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

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

1284 
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

1285 
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

1286 
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

1287 

31706  1288 

1289 
subsection {* LCM *} 

1290 

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

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

1294 

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

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

1297 
by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat]) 
31706  1298 

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

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

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

1302 
apply (subst prod_gcd_lcm_nat [symmetric]) 
31706  1303 
apply (subst nat_abs_mult_distrib [symmetric]) 
1304 
apply (simp, simp add: abs_mult) 

1305 
done 

1306 

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

1307 
lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0" 
31706  1308 
unfolding lcm_nat_def by simp 
1309 

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

1310 
lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0" 
31706  1311 
unfolding lcm_int_def by simp 
1312 

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

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

1315 

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

1316 
lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0" 
31706  1317 
unfolding lcm_int_def by simp 
1318 

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

1319 
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

1320 
unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps) 
31706  1321 

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

1322 
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

1323 
unfolding lcm_int_def by (subst lcm_commute_nat, rule refl) 
31706  1324 

1325 

31952 