author  wenzelm 
Wed, 08 Apr 2015 21:48:59 +0200  
changeset 59977  ad2d1cd53877 
parent 59807  22bc39064290 
child 60162  645058aa9d6f 
permissions  rwrr 
32479  1 
(* Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, 
31798  2 
Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow 
31706  3 

4 

32479  5 
This file deals with the functions gcd and lcm. Definitions and 
6 
lemmas are proved uniformly for the natural numbers and integers. 

31706  7 

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

9 

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

58623  11 
and Lawrence C. Paulson, based on @{cite davenport92}. They introduced 
31706  12 
gcd, lcm, and prime for the natural numbers. 
13 

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

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

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

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

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

34915  19 
the natural numbers by Chaieb. 
31706  20 

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

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

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

23 

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

31706  27 

58889  28 
section {* Greatest common divisor and least common multiple *} 
21256  29 

30 
theory GCD 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59545
diff
changeset

31 
imports Main 
31706  32 
begin 
33 

34 
declare One_nat_def [simp del] 

35 

34030
829eb528b226
resorted code equations from "old" number theory version
haftmann
parents:
33946
diff
changeset

36 
subsection {* GCD and LCM definitions *} 
31706  37 

31992  38 
class gcd = zero + one + dvd + 
41550  39 
fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 
40 
and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 

21256  41 
begin 
42 

31706  43 
abbreviation 
44 
coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 

45 
where 

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

47 

48 
end 

49 

59008  50 
class semiring_gcd = comm_semiring_1 + gcd + 
51 
assumes gcd_dvd1 [iff]: "gcd a b dvd a" 

59977  52 
and gcd_dvd2 [iff]: "gcd a b dvd b" 
53 
and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" 

59008  54 

55 
class ring_gcd = comm_ring_1 + semiring_gcd 

56 

31706  57 
instantiation nat :: gcd 
58 
begin 

21256  59 

31706  60 
fun 
61 
gcd_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

62 
where 

63 
"gcd_nat x y = 

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

65 

66 
definition 

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

68 
where 

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

70 

71 
instance proof qed 

72 

73 
end 

74 

75 
instantiation int :: gcd 

76 
begin 

21256  77 

31706  78 
definition 
79 
gcd_int :: "int \<Rightarrow> int \<Rightarrow> int" 

80 
where 

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

82 

31706  83 
definition 
84 
lcm_int :: "int \<Rightarrow> int \<Rightarrow> int" 

85 
where 

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

87 

31706  88 
instance proof qed 
89 

90 
end 

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

91 

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

92 

34030
829eb528b226
resorted code equations from "old" number theory version
haftmann
parents:
33946
diff
changeset

93 
subsection {* Transfer setup *} 
31706  94 

95 
lemma transfer_nat_int_gcd: 

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

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

32479  98 
unfolding gcd_int_def lcm_int_def 
31706  99 
by auto 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

100 

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

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

104 
by (auto simp add: gcd_int_def lcm_int_def) 

105 

35644  106 
declare transfer_morphism_nat_int[transfer add return: 
31706  107 
transfer_nat_int_gcd transfer_nat_int_gcd_closures] 
108 

109 
lemma transfer_int_nat_gcd: 

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

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

32479  112 
by (unfold gcd_int_def lcm_int_def, auto) 
31706  113 

114 
lemma transfer_int_nat_gcd_closures: 

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

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

117 
by (auto simp add: gcd_int_def lcm_int_def) 

118 

35644  119 
declare transfer_morphism_int_nat[transfer add return: 
31706  120 
transfer_int_nat_gcd transfer_int_nat_gcd_closures] 
121 

122 

34030
829eb528b226
resorted code equations from "old" number theory version
haftmann
parents:
33946
diff
changeset

123 
subsection {* GCD properties *} 
31706  124 

125 
(* was gcd_induct *) 

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

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

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

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

129 
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

130 
shows "P m n" 
31706  131 
apply (rule gcd_nat.induct) 
132 
apply (case_tac "y = 0") 

133 
using assms apply simp_all 

134 
done 

135 

136 
(* specific to int *) 

137 

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

138 
lemma gcd_neg1_int [simp]: "gcd (x::int) y = gcd x y" 
31706  139 
by (simp add: gcd_int_def) 
140 

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

141 
lemma gcd_neg2_int [simp]: "gcd (x::int) (y) = gcd x y" 
31706  142 
by (simp add: gcd_int_def) 
143 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

144 
lemma gcd_neg_numeral_1_int [simp]: 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

145 
"gcd ( numeral n :: int) x = gcd (numeral n) x" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

146 
by (fact gcd_neg1_int) 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

147 

03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

148 
lemma gcd_neg_numeral_2_int [simp]: 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

149 
"gcd x ( numeral n :: int) = gcd x (numeral n)" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

150 
by (fact gcd_neg2_int) 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54437
diff
changeset

151 

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

154 

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

155 
lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)" 
31813  156 
by (simp add: gcd_int_def) 
157 

158 
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

159 
by (metis abs_idempotent gcd_abs_int) 
31813  160 

161 
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

162 
by (metis abs_idempotent gcd_abs_int) 
31706  163 

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

164 
lemma gcd_cases_int: 
31706  165 
fixes x :: int and y 
166 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)" 

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

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

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

170 
shows "P (gcd x y)" 

35216  171 
by (insert assms, auto, arith) 
21256  172 

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

173 
lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0" 
31706  174 
by (simp add: gcd_int_def) 
175 

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

176 
lemma lcm_neg1_int: "lcm (x::int) y = lcm x y" 
31706  177 
by (simp add: lcm_int_def) 
178 

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

179 
lemma lcm_neg2_int: "lcm (x::int) (y) = lcm x y" 
31706  180 
by (simp add: lcm_int_def) 
181 

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

182 
lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)" 
31706  183 
by (simp add: lcm_int_def) 
21256  184 

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

187 

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

189 
by (metis abs_idempotent lcm_int_def) 

190 

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

192 
by (metis abs_idempotent lcm_int_def) 

193 

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

194 
lemma lcm_cases_int: 
31706  195 
fixes x :: int and y 
196 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)" 

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

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

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

200 
shows "P (lcm x y)" 

41550  201 
using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith 
31706  202 

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

203 
lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0" 
31706  204 
by (simp add: lcm_int_def) 
205 

206 
(* was gcd_0, etc. *) 

54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

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

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

209 

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

211 
lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x" 
31706  212 
by (unfold gcd_int_def, auto) 
213 

54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

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

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

216 

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

217 
lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x" 
31706  218 
by (unfold gcd_int_def, auto) 
219 

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

220 
lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)" 
31706  221 
by (case_tac "y = 0", auto) 
222 

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

224 

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

225 
lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)" 
31706  226 
by simp 
227 

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

228 
lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1" 
21263  229 
by simp 
21256  230 

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

231 
lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" 
31706  232 
by (simp add: One_nat_def) 
233 

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

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

236 

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

237 
lemma gcd_idem_nat: "gcd (x::nat) x = x" 
31798  238 
by simp 
31706  239 

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

240 
lemma gcd_idem_int: "gcd (x::int) x = abs x" 
31813  241 
by (auto simp add: gcd_int_def) 
31706  242 

243 
declare gcd_nat.simps [simp del] 

21256  244 

245 
text {* 

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

249 

59008  250 
instance nat :: semiring_gcd 
251 
proof 

252 
fix m n :: nat 

253 
show "gcd m n dvd m" and "gcd m n dvd n" 

254 
proof (induct m n rule: gcd_nat_induct) 

255 
fix m n :: nat 

256 
assume "gcd n (m mod n) dvd m mod n" and "gcd n (m mod n) dvd n" 

257 
then have "gcd n (m mod n) dvd m" 

258 
by (rule dvd_mod_imp_dvd) 

259 
moreover assume "0 < n" 

260 
ultimately show "gcd m n dvd m" 

261 
by (simp add: gcd_non_0_nat) 

262 
qed (simp_all add: gcd_0_nat gcd_non_0_nat) 

263 
next 

264 
fix m n k :: nat 

265 
assume "k dvd m" and "k dvd n" 

266 
then show "k dvd gcd m n" 

267 
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat) 

268 
qed 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59545
diff
changeset

269 

59008  270 
instance int :: ring_gcd 
271 
by intro_classes (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def gcd_greatest) 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59545
diff
changeset

272 

31730  273 
lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m" 
59008  274 
by (metis gcd_dvd1 dvd_trans) 
31730  275 

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

59008  277 
by (metis gcd_dvd2 dvd_trans) 
31730  278 

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

59008  280 
by (metis gcd_dvd1 dvd_trans) 
31730  281 

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

59008  283 
by (metis gcd_dvd2 dvd_trans) 
31730  284 

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

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

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

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

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

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

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

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

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

297 
lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) = 
31706  298 
(k dvd m & k dvd n)" 
59008  299 
by (blast intro!: gcd_greatest intro: dvd_trans) 
31706  300 

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

301 
lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)" 
59008  302 
by (blast intro!: gcd_greatest intro: dvd_trans) 
21256  303 

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

304 
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

305 
by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat) 
21256  306 

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

307 
lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)" 
31706  308 
by (auto simp add: gcd_int_def) 
21256  309 

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

310 
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

311 
by (insert gcd_zero_nat [of m n], arith) 
21256  312 

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

313 
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

314 
by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith) 
31706  315 

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

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

33657  319 
apply (rule dvd_antisym) 
59008  320 
apply (erule (1) gcd_greatest) 
31706  321 
apply auto 
322 
done 

21256  323 

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

324 
lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and> 
31706  325 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 
33657  326 
apply (case_tac "d = 0") 
327 
apply simp 

328 
apply (rule iffI) 

329 
apply (rule zdvd_antisym_nonneg) 

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

332 

54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

333 
interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

334 
+ gcd_nat: semilattice_neutr_order "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 0 "op dvd" "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)" 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

335 
apply default 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

336 
apply (auto intro: dvd_antisym dvd_trans)[4] 
59545
12a6088ed195
explicit equivalence for strict order on lattices
haftmann
parents:
59497
diff
changeset

337 
apply (metis dvd.dual_order.refl gcd_unique_nat)+ 
54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

338 
done 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

339 

c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

340 
interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int" 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

341 
proof 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

342 
qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute) 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

343 

c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

344 
lemmas gcd_assoc_nat = gcd_nat.assoc 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

345 
lemmas gcd_commute_nat = gcd_nat.commute 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

346 
lemmas gcd_left_commute_nat = gcd_nat.left_commute 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

347 
lemmas gcd_assoc_int = gcd_int.assoc 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

348 
lemmas gcd_commute_int = gcd_int.commute 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

349 
lemmas gcd_left_commute_int = gcd_int.left_commute 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

350 

c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

351 
lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

352 

c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

353 
lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

354 

31798  355 
lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x" 
54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

356 
by (fact gcd_nat.absorb1) 
31798  357 

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

54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

359 
by (fact gcd_nat.absorb2) 
31798  360 

54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

361 
lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x" 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

362 
by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int) 
31798  363 

54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

364 
lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y" 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

365 
by (metis gcd_proj1_if_dvd_int gcd_commute_int) 
31798  366 

21256  367 
text {* 
368 
\medskip Multiplication laws 

369 
*} 

370 

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

371 
lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)" 
58623  372 
 {* @{cite \<open>page 27\<close> davenport92} *} 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

373 
apply (induct m n rule: gcd_nat_induct) 
31706  374 
apply simp 
21256  375 
apply (case_tac "k = 0") 
45270
d5b5c9259afd
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
huffman
parents:
45264
diff
changeset

376 
apply (simp_all add: gcd_non_0_nat) 
31706  377 
done 
21256  378 

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

379 
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

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

382 
apply (rule gcd_mult_distrib_nat [transferred]) 
31706  383 
apply auto 
384 
done 

21256  385 

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

386 
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

387 
apply (insert gcd_mult_distrib_nat [of m k n]) 
21256  388 
apply simp 
389 
apply (erule_tac t = m in ssubst) 

390 
apply simp 

391 
done 

392 

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

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

396 
apply (subst dvd_abs_iff [symmetric]) 

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

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

398 
apply (rule coprime_dvd_mult_nat [transferred]) 
31813  399 
prefer 4 apply assumption 
400 
apply auto 

401 
apply (subst abs_mult [symmetric], auto) 

31706  402 
done 
403 

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

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

406 
by (auto intro: coprime_dvd_mult_nat) 
31706  407 

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

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

410 
by (auto intro: coprime_dvd_mult_int) 
31706  411 

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

412 
lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n" 
33657  413 
apply (rule dvd_antisym) 
59008  414 
apply (rule gcd_greatest) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

415 
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

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

417 
apply (simp add: gcd_commute_nat) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

418 
apply (simp_all add: mult.commute) 
31706  419 
done 
21256  420 

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

421 
lemma gcd_mult_cancel_int: 
31813  422 
"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

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

425 
apply (rule gcd_mult_cancel_nat [transferred], auto) 
31706  426 
done 
21256  427 

35368  428 
lemma coprime_crossproduct_nat: 
429 
fixes a b c d :: nat 

430 
assumes "coprime a d" and "coprime b c" 

431 
shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d" (is "?lhs \<longleftrightarrow> ?rhs") 

432 
proof 

433 
assume ?rhs then show ?lhs by simp 

434 
next 

435 
assume ?lhs 

436 
from `?lhs` have "a dvd b * d" by (auto intro: dvdI dest: sym) 

437 
with `coprime a d` have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat) 

438 
from `?lhs` have "b dvd a * c" by (auto intro: dvdI dest: sym) 

439 
with `coprime b c` have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

440 
from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult.commute) 
35368  441 
with `coprime b c` have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

442 
from `?lhs` have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult.commute) 
35368  443 
with `coprime a d` have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat) 
444 
from `a dvd b` `b dvd a` have "a = b" by (rule Nat.dvd.antisym) 

445 
moreover from `c dvd d` `d dvd c` have "c = d" by (rule Nat.dvd.antisym) 

446 
ultimately show ?rhs .. 

447 
qed 

448 

449 
lemma coprime_crossproduct_int: 

450 
fixes a b c d :: int 

451 
assumes "coprime a d" and "coprime b c" 

452 
shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>" 

453 
using assms by (intro coprime_crossproduct_nat [transferred]) auto 

454 

21256  455 
text {* \medskip Addition laws *} 
456 

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

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

459 
apply (simp_all add: gcd_non_0_nat) 
31706  460 
done 
461 

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

462 
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

463 
apply (subst (1 2) gcd_commute_nat) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

464 
apply (subst add.commute) 
31706  465 
apply simp 
466 
done 

467 

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

469 

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

470 
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

471 
by (subst gcd_add1_nat [symmetric], auto) 
31706  472 

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

473 
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

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

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

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

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

480 
apply (rule gcd_commute_nat) 
31706  481 
done 
482 

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

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

486 
apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] 
31706  487 
zmod_zminus1_eq_if) 
488 
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

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

490 
apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat 
31706  491 
nat_le_eq_zle) 
492 
done 

21256  493 

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

494 
lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)" 
31706  495 
apply (case_tac "y = 0") 
496 
apply force 

497 
apply (case_tac "y > 0") 

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

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

499 
apply (insert gcd_non_0_int [of "y" "x"]) 
35216  500 
apply auto 
31706  501 
done 
502 

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

503 
lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

504 
by (metis gcd_red_int mod_add_self1 add.commute) 
31706  505 

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

506 
lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

507 
by (metis gcd_add1_int gcd_commute_int add.commute) 
21256  508 

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

509 
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

510 
by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat) 
21256  511 

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

512 
lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

513 
by (metis gcd_commute_int gcd_red_int mod_mult_self1 add.commute) 
31798  514 

21256  515 

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

518 

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

520 
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

521 
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

522 

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

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

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

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

530 
by(bestsimp intro!:dvd_imp_le) 

531 
qed 

532 

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

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

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

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

539 
by(bestsimp intro!:dvd_imp_le_int) 

540 
qed 

541 

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

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44845
diff
changeset

544 
apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le) 
31995  545 
apply simp 
546 
done 

547 

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

549 
apply(rule antisym) 

44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
42871
diff
changeset

550 
apply(rule Max_le_iff [THEN iffD2]) 
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
42871
diff
changeset

551 
apply (auto intro: abs_le_D1 dvd_imp_le_int) 
31995  552 
done 
553 

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

556 
apply(rule Max_eqI[THEN sym]) 

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

559 
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat) 
31734  560 
apply simp 
561 
done 

562 

563 
lemma gcd_is_Max_divisors_int: 

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

565 
apply(rule Max_eqI[THEN sym]) 

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

568 
apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le) 
31734  569 
apply simp 
570 
done 

571 

34030
829eb528b226
resorted code equations from "old" number theory version
haftmann
parents:
33946
diff
changeset

572 
lemma gcd_code_int [code]: 
829eb528b226
resorted code equations from "old" number theory version
haftmann
parents:
33946
diff
changeset

573 
"gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>" 
829eb528b226
resorted code equations from "old" number theory version
haftmann
parents:
33946
diff
changeset

574 
by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat) 
829eb528b226
resorted code equations from "old" number theory version
haftmann
parents:
33946
diff
changeset

575 

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

576 

31706  577 
subsection {* Coprimality *} 
578 

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

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

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

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

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

587 
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

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

591 
unfolding dvd_def by blast 
58834  592 
from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" 
593 
by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"]) 

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

596 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

35216  597 
have "?g \<noteq> 0" using nz by simp 
31706  598 
then have gp: "?g > 0" by arith 
59008  599 
from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . 
22367  600 
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

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

602 

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

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

606 
apply (subst (1 2 3) gcd_abs_int) 
31813  607 
apply (subst (1 2) abs_div) 
608 
apply simp 

609 
apply simp 

610 
apply(subst (1 2) abs_gcd_int) 

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

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

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

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

615 
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

616 
using gcd_unique_nat[of 1 a b, simplified] by auto 
31706  617 

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

618 
lemma coprime_Suc_0_nat: 
31706  619 
"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

620 
using coprime_nat by (simp add: One_nat_def) 
31706  621 

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

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

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

627 
apply (rule iffI) 

628 
apply force 

59807  629 
apply (drule_tac x = "abs e" for e in exI) 
630 
apply (case_tac "e >= 0" for e :: int) 

31706  631 
apply force 
632 
apply force 

59807  633 
done 
31706  634 

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

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

638 
shows "coprime a' b'" 

639 

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

641 
apply (erule ssubst) 

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

643 
apply (erule ssubst) 

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

644 
apply (rule div_gcd_coprime_nat) 
41550  645 
using z apply force 
31706  646 
apply (subst (1) b) 
647 
using z apply force 

648 
apply (subst (1) a) 

649 
using z apply force 

41550  650 
done 
31706  651 

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

652 
lemma gcd_coprime_int: 
31706  653 
assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and 
654 
b: "b = b' * gcd a b" 

655 
shows "coprime a' b'" 

656 

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

658 
apply (erule ssubst) 

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

660 
apply (erule ssubst) 

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

661 
apply (rule div_gcd_coprime_int) 
41550  662 
using z apply force 
31706  663 
apply (subst (1) b) 
664 
using z apply force 

665 
apply (subst (1) a) 

666 
using z apply force 

41550  667 
done 
31706  668 

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

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

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

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

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

674 
apply (subst gcd_commute_nat, rule db) 
31706  675 
done 
676 

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

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

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

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

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

682 
apply (subst gcd_commute_int, rule db) 
31706  683 
done 
684 

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

685 
lemma coprime_lmult_nat: 
31706  686 
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" 
687 
proof  

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

59008  689 
by (rule gcd_greatest, auto) 
31706  690 
with dab show ?thesis 
691 
by auto 

692 
qed 

693 

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

694 
lemma coprime_lmult_int: 
31798  695 
assumes "coprime (d::int) (a * b)" shows "coprime d a" 
31706  696 
proof  
697 
have "gcd d a dvd gcd d (a * b)" 

59008  698 
by (rule gcd_greatest, auto) 
31798  699 
with assms show ?thesis 
31706  700 
by auto 
701 
qed 

702 

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

703 
lemma coprime_rmult_nat: 
31798  704 
assumes "coprime (d::nat) (a * b)" shows "coprime d b" 
31706  705 
proof  
706 
have "gcd d b dvd gcd d (a * b)" 

59008  707 
by (rule gcd_greatest, auto intro: dvd_mult) 
31798  708 
with assms show ?thesis 
31706  709 
by auto 
710 
qed 

711 

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

712 
lemma coprime_rmult_int: 
31706  713 
assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" 
714 
proof  

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

59008  716 
by (rule gcd_greatest, auto intro: dvd_mult) 
31706  717 
with dab show ?thesis 
718 
by auto 

719 
qed 

720 

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

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

723 
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

724 
coprime_mult_nat[of d a b] 
31706  725 
by blast 
726 

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

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

729 
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

730 
coprime_mult_int[of d a b] 
31706  731 
by blast 
732 

52397  733 
lemma coprime_power_int: 
734 
assumes "0 < n" shows "coprime (a :: int) (b ^ n) \<longleftrightarrow> coprime a b" 

735 
using assms 

736 
proof (induct n) 

737 
case (Suc n) then show ?case 

738 
by (cases n) (simp_all add: coprime_mul_eq_int) 

739 
qed simp 

740 

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

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

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

745 
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

746 
using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult) 
31706  747 
done 
748 

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

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

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

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

59008  754 
using nz apply (auto simp add: div_gcd_coprime_int) 
31706  755 
done 
756 

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

757 
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

758 
by (induct n, simp_all add: coprime_mult_nat) 
31706  759 

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

760 
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

761 
by (induct n, simp_all add: coprime_mult_int) 
31706  762 

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

763 
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

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

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

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

767 
apply (subst gcd_commute_nat, assumption) 
31706  768 
done 
769 

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

770 
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

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

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

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

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

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

777 
lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n" 
31706  778 
proof (cases) 
779 
assume "a = 0 & b = 0" 

780 
thus ?thesis by simp 

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

782 
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

783 
by (auto simp:div_gcd_coprime_nat) 
31706  784 
hence "gcd ((a div gcd a b)^n * (gcd a b)^n) 
785 
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

786 
apply (subst (1 2) mult.commute) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

787 
apply (subst gcd_mult_distrib_nat [symmetric]) 
31706  788 
apply simp 
789 
done 

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

791 
apply (subst div_power) 

792 
apply auto 

793 
apply (rule dvd_div_mult_self) 

794 
apply (rule dvd_power_same) 

795 
apply auto 

796 
done 

797 
also have "(b div gcd a b)^n * (gcd a b)^n = b^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 
finally show ?thesis . 

805 
qed 

806 

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

807 
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

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

810 
apply (rule gcd_exp_nat [where n = n, transferred]) 
31706  811 
apply auto 
812 
done 

813 

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

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

817 
let ?g = "gcd a b" 

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

819 
moreover 

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

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

821 
from gcd_coprime_exists_nat[OF z] 
31706  822 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
823 
by blast 

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

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

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

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

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

828 
hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc) 
31706  829 
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

830 
from coprime_dvd_mult_nat[OF ab'(3)] th_1 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

831 
have thc: "a' dvd c" by (subst (asm) mult.commute, blast) 
31706  832 
from ab' have "a = ?g*a'" by algebra 
833 
with thb thc have ?thesis by blast } 

834 
ultimately show ?thesis by blast 

835 
qed 

836 

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

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

840 
let ?g = "gcd a b" 

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

842 
moreover 

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

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

844 
from gcd_coprime_exists_int[OF z] 
31706  845 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
846 
by blast 

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

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

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

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

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

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

852 
hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc) 
31706  853 
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

854 
from coprime_dvd_mult_int[OF ab'(3)] th_1 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

855 
have thc: "a' dvd c" by (subst (asm) mult.commute, blast) 
31706  856 
from ab' have "a = ?g*a'" by algebra 
857 
with thb thc have ?thesis by blast } 

858 
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

859 
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

860 

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

861 
lemma pow_divides_pow_nat: 
31706  862 
assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0" 
863 
shows "a dvd b" 

864 
proof 

865 
let ?g = "gcd a b" 

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

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

868 
moreover 

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

35216  870 
hence zn: "?g ^ n \<noteq> 0" using n by simp 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

871 
from gcd_coprime_exists_nat[OF z] 
31706  872 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
873 
by blast 

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

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

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

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

877 
by (simp only: power_mult_distrib mult.commute) 
58787  878 
then have th0: "a'^n dvd b'^n" 
879 
using zn by auto 

31706  880 
have "a' dvd a'^n" by (simp add: m) 
881 
with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

882 
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

883 
from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

884 
have "a' dvd b'" by (subst (asm) mult.commute, blast) 
31706  885 
hence "a'*?g dvd b'*?g" by simp 
886 
with ab'(1,2) have ?thesis by simp } 

887 
ultimately show ?thesis by blast 

888 
qed 

889 

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

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

893 
proof 
31706  894 
let ?g = "gcd a b" 
895 
from n obtain m where m: "n = Suc m" by (cases n, simp_all) 

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

897 
moreover 

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

35216  899 
hence zn: "?g ^ n \<noteq> 0" using n by simp 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

900 
from gcd_coprime_exists_int[OF z] 
31706  901 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
902 
by blast 

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

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

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

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

906 
by (simp only: power_mult_distrib mult.commute) 
31706  907 
with zn z n have th0:"a'^n dvd b'^n" by auto 
908 
have "a' dvd a'^n" by (simp add: m) 

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

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

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

911 
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

912 
from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

913 
have "a' dvd b'" by (subst (asm) mult.commute, blast) 
31706  914 
hence "a'*?g dvd b'*?g" by simp 
915 
with ab'(1,2) have ?thesis by simp } 

916 
ultimately show ?thesis by blast 

917 
qed 

918 

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

919 
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

920 
by (auto intro: pow_divides_pow_nat dvd_power_same) 
31706  921 

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

922 
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

923 
by (auto intro: pow_divides_pow_int dvd_power_same) 
31706  924 

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

925 
lemma divides_mult_nat: 
31706  926 
assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n" 
927 
shows "m * n dvd r" 

928 
proof 

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

930 
unfolding dvd_def by blast 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

931 
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

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

935 
qed 

936 

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

937 
lemma divides_mult_int: 
31706  938 
assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n" 
939 
shows "m * n dvd r" 

940 
proof 

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

942 
unfolding dvd_def by blast 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

943 
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

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

947 
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

948 

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

949 
lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n" 
31706  950 
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1  n)") 
951 
apply force 

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

952 
apply (rule dvd_diff_nat) 
31706  953 
apply auto 
954 
done 

955 

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

956 
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

957 
using coprime_plus_one_nat by (simp add: One_nat_def) 
31706  958 

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

959 
lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n" 
31706  960 
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1  n)") 
961 
apply force 

962 
apply (rule dvd_diff) 

963 
apply auto 

964 
done 

965 

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

966 
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

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

968 
gcd_commute_nat [of "n  1" n] by auto 
31706  969 

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

970 
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

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

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

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

974 
lemma setprod_coprime_nat [rule_format]: 
31706  975 
"(ALL i: A. coprime (f i) (x::nat)) > coprime (PROD i:A. f i) x" 
976 
apply (case_tac "finite A") 

977 
apply (induct set: finite) 

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

978 
apply (auto simp add: gcd_mult_cancel_nat) 
31706  979 
done 
980 

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

981 
lemma setprod_coprime_int [rule_format]: 
31706  982 
"(ALL i: A. coprime (f i) (x::int)) > coprime (PROD i:A. f i) x" 
983 
apply (case_tac "finite A") 

984 
apply (induct set: finite) 

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

985 
apply (auto simp add: gcd_mult_cancel_int) 
31706  986 
done 
987 

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

988 
lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> 
31706  989 
x dvd b \<Longrightarrow> x = 1" 
990 
apply (subgoal_tac "x dvd gcd a b") 

991 
apply simp 

59008  992 
apply (erule (1) gcd_greatest) 
31706  993 
done 
994 

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

995 
lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> 
31706  996 
x dvd b \<Longrightarrow> abs x = 1" 
997 
apply (subgoal_tac "x dvd gcd a b") 

998 
apply simp 

59008  999 
apply (erule (1) gcd_greatest) 
31706  1000 
done 
1001 

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

1002 
lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> 
31706  1003 
coprime d e" 
1004 
apply (auto simp add: dvd_def) 

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

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

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

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

1008 
apply (erule coprime_lmult_int) 
31706  1009 
done 
1010 

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

1011 
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

1012 
apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat) 
31706  1013 
done 
1014 

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

1015 
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

1016 
apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int) 
31706  1017 
done 
1018 

1019 

1020 
subsection {* Bezout's theorem *} 

1021 

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

1023 
see the theorems that follow the definition. *) 

1024 
fun 

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

1026 
where 

1027 
"bezw x y = 

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

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

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

1031 

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

1033 

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

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

1036 
by simp 

1037 

1038 
declare bezw.simps [simp del] 

1039 

1040 
lemma bezw_aux [rule_format]: 

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

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

1045 
by auto 

1046 
next fix m :: nat and n 

1047 
assume ngt0: "n > 0" and 

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

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

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

1051 
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

1052 
apply (simp add: bezw_non_0 gcd_non_0_nat) 
31706  1053 
apply (erule subst) 
36350  1054 
apply (simp add: field_simps) 
31706  1055 
apply (subst mod_div_equality [of m n, symmetric]) 
1056 
(* applying simp here undoes the last substitution! 

1057 
what is procedure cancel_div_mod? *) 

58776
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58770
diff
changeset

1058 
apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult) 
31706  1059 
done 
1060 
qed 

1061 

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

1062 
lemma bezout_int: 
31706  1063 
fixes x y 
1064 
shows "EX u v. u * (x::int) + v * y = gcd x y" 

1065 
proof  

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

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

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

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

1070 
apply (unfold gcd_int_def) 

1071 
apply simp 

1072 
apply (subst bezw_aux [symmetric]) 

1073 
apply auto 

1074 
done 

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

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

1077 
by auto 

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

1079 
by (erule (1) bezout_aux) 

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

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

1082 
apply auto 

1083 
apply (rule_tac x = u in exI) 

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

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

1085 
apply (subst gcd_neg2_int [symmetric]) 
31706  1086 
apply auto 
1087 
done 

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

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

1090 
apply auto 

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

1092 
apply (rule_tac x = v in exI) 

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

1093 
apply (subst gcd_neg1_int [symmetric]) 
31706  1094 
apply auto 
1095 
done 

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

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

1098 
apply auto 

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

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

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

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

1102 
apply (subst gcd_neg2_int [symmetric]) 
31706  1103 
apply auto 
1104 
done 

1105 
ultimately show ?thesis by blast 

1106 
qed 

1107 

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

1109 

1110 
lemma ind_euclid: 

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

1112 
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

1113 
shows "P a b" 
34915  1114 
proof(induct "a + b" arbitrary: a b rule: less_induct) 
1115 
case less 

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

1116 
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

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

1120 
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

1121 
{assume lt: "a < b" 
34915  1122 
hence "a + b  a < a + b \<or> a = 0" by arith 
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

1123 
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

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

1125 
moreover 
34915  1126 
{assume "a + b  a < a + b" 
1127 
also have th0: "a + b  a = a + (b  a)" using lt by arith 

1128 
finally have "a + (b  a) < a + b" . 

1129 
then have "P a (a + (b  a))" by (rule add[rule_format, OF less]) 

1130 
then have "P a b" by (simp add: th0[symmetric])} 

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

1131 
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

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

1133 
{assume lt: "a > b" 
34915  1134 
hence "b + a  b < a + b \<or> b = 0" by arith 
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

1135 
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

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

1137 
moreover 
34915  1138 
{assume "b + a  b < a + b" 
1139 
also have th0: "b + a  b = b + (a  b)" using lt by arith 

1140 
finally have "b + (a  b) < a + b" . 

1141 
then have "P b (b + (a  b))" by (rule add[rule_format, OF less]) 

1142 
then have "P b a" by (simp add: th0[symmetric]) 

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

1144 
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

1145 
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

1146 
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

1147 

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

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

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

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

1153 
using ex 

1154 
apply clarsimp 

35216  1155 
apply (rule_tac x="d" in exI, simp) 
31706  1156 
apply (case_tac "a * x = b * y + d" , simp_all) 
1157 
apply (rule_tac x="x + y" in exI) 

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

1159 
apply algebra 

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

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

1162 
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

1163 
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

1164 

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

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

1168 
apply blast 

1169 
apply clarify 

35216  1170 
apply (rule_tac x="a" in exI, simp) 
31706  1171 
apply clarsimp 
1172 
apply (rule_tac x="d" in exI) 

35216  1173 
apply (case_tac "a * x = b * y + d", simp_all) 
31706  1174 
apply (rule_tac x="x+y" in exI) 
1175 
apply (rule_tac x="y" in exI) 

1176 
apply algebra 

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

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

1179 
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

1180 
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

1181 

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

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

1184 
using bezout_add_nat[of a b] 
31706  1185 
apply clarsimp 
1186 
apply (rule_tac x="d" in exI, simp) 

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

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

1189 
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

1190 
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

1191 

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

1192 
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

1193 
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

1194 
proof 
31706  1195 
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

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

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

1202 
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

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

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

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

1209 
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

1210 
{assume db: "d=b" 
41550  1211 
with nz H have ?thesis apply simp 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1212 
apply (rule exI[where x = b], simp) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1213 
apply (rule exI[where x = b]) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1214 
by (rule exI[where x = "a  1"], simp add: diff_mult_distrib2)} 
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1215 
moreover 
31706  1216 
{assume db: "d < b" 
41550  1217 
{assume "x=0" hence ?thesis using nz H by simp } 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1218 
moreover 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1219 
{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1220 
from db have "d \<le> b  1" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1221 
hence "d*b \<le> b*(b  1)" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1222 
with xp mult_mono[of "1" "x" "d*b" "b*(b  1)"] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1223 
have dble: "d*b \<le> x*b*(b  1)" using bp by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1224 
from H (3) have "d + (b  1) * (b*x) = d + (b  1) * (a*y + d)" 
31706  1225 
by simp 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1226 
hence "d + (b  1) * a * y + (b  1) * d = d + (b  1) * b * x" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56218
diff
changeset

1227 
by (simp only: mult.assoc distrib_left) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1228 
hence "a * ((b  1) * y) + d * (b  1 + 1) = d + x*b*(b  1)" 
31706  1229 
by algebra 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1230 
hence "a * ((b  1) * y) = d + x*b*(b  1)  d*b" using bp by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1231 
hence "a * ((b  1) * y) = d + (x*b*(b  1)  d*b)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1232 
by (simp only: diff_add_assoc[OF dble, of d, symmetric]) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1233 
hence "a * ((b  1) * y) = b*(x*(b  1)  d) + d" 
59008  1234 
by (simp only: diff_mult_distrib2 ac_simps) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1235 
hence ?thesis using H(1,2) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1236 
apply  
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1237 
apply (rule exI[where x=d], simp) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1238 
apply (rule exI[where x="(b  1) * y"]) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

1239 
by (rule exI[where x="x*(b  1)  d"], simp)} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

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

1241 
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

1242 
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

1243 
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

1244 
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

1245 

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

1246 
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

1247 
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

1248 
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

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

1250 
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

1251 
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

1252 
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

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

1255 
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

1256 
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

1257 
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

1258 

31706  1259 

34030
829eb528b226
resorted code equations from "old" number theory version
haftmann
parents:
33946
diff
changeset

1260 
subsection {* LCM properties *} 
31706  1261 

34030
829eb528b226
resorted code equations from "old" number theory version
haftmann
parents:
33946
diff
changeset

1262 
lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b" 
31706  1263 
by (simp add: lcm_int_def lcm_nat_def zdiv_int 
44821  1264 
of_nat_mult gcd_int_def) 
31706  1265 

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

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

1268 
by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat]) 
31706  1269 

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

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

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

1273 
apply (subst prod_gcd_lcm_nat [symmetric]) 
31706  1274 
apply (subst nat_abs_mult_distrib [symmetric]) 
1275 
apply (simp, simp add: abs_mult) 

1276 
done 

1277 

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

1278 
lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0" 
31706  1279 
unfolding lcm_nat_def by simp 
1280 

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

1281 
lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0" 
31706  1282 
unfolding lcm_int_def by simp 
1283 

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

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

1286 

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

1287 
lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0" 
31706  1288 
unfolding lcm_int_def by simp 
1289 

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

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

1292 
by (metis gr0I mult_is_0 prod_gcd_lcm_nat) 
27669
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1293 

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

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

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

1297 
apply (rule lcm_pos_nat [transferred]) 
31798  1298 
apply auto 
31706  1299 
done 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1300 

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

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

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

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

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

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

1306 

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

1307 
lemma lcm_least_nat: 
31706  1308 
assumes "(m::nat) dvd k" and "n dvd k" 
27556  1309 
shows "lcm m n dvd k" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

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

1313 
case (Suc _) then have pos_k: "k > 0" by auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1314 
from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto 