author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45992  15d14fa805b2 
child 48562  f6d6d58fa318 
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 

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

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 

34915  28 
header {* Greatest common divisor and least common multiple *} 
21256  29 

30 
theory GCD 

33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33197
diff
changeset

31 
imports Fact Parity 
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 

50 
instantiation nat :: gcd 

51 
begin 

21256  52 

31706  53 
fun 
54 
gcd_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

55 
where 

56 
"gcd_nat x y = 

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

58 

59 
definition 

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

61 
where 

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

63 

64 
instance proof qed 

65 

66 
end 

67 

68 
instantiation int :: gcd 

69 
begin 

21256  70 

31706  71 
definition 
72 
gcd_int :: "int \<Rightarrow> int \<Rightarrow> int" 

73 
where 

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

75 

31706  76 
definition 
77 
lcm_int :: "int \<Rightarrow> int \<Rightarrow> int" 

78 
where 

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

80 

31706  81 
instance proof qed 
82 

83 
end 

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

84 

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

85 

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

86 
subsection {* Transfer setup *} 
31706  87 

88 
lemma transfer_nat_int_gcd: 

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

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

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

93 

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

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

97 
by (auto simp add: gcd_int_def lcm_int_def) 

98 

35644  99 
declare transfer_morphism_nat_int[transfer add return: 
31706  100 
transfer_nat_int_gcd transfer_nat_int_gcd_closures] 
101 

102 
lemma transfer_int_nat_gcd: 

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

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

32479  105 
by (unfold gcd_int_def lcm_int_def, auto) 
31706  106 

107 
lemma transfer_int_nat_gcd_closures: 

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

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

110 
by (auto simp add: gcd_int_def lcm_int_def) 

111 

35644  112 
declare transfer_morphism_int_nat[transfer add return: 
31706  113 
transfer_int_nat_gcd transfer_int_nat_gcd_closures] 
114 

115 

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

116 
subsection {* GCD properties *} 
31706  117 

118 
(* was gcd_induct *) 

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

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

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

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

122 
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

123 
shows "P m n" 
31706  124 
apply (rule gcd_nat.induct) 
125 
apply (case_tac "y = 0") 

126 
using assms apply simp_all 

127 
done 

128 

129 
(* specific to int *) 

130 

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

131 
lemma gcd_neg1_int [simp]: "gcd (x::int) y = gcd x y" 
31706  132 
by (simp add: gcd_int_def) 
133 

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

134 
lemma gcd_neg2_int [simp]: "gcd (x::int) (y) = gcd x y" 
31706  135 
by (simp add: gcd_int_def) 
136 

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

139 

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

140 
lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)" 
31813  141 
by (simp add: gcd_int_def) 
142 

143 
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

144 
by (metis abs_idempotent gcd_abs_int) 
31813  145 

146 
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

147 
by (metis abs_idempotent gcd_abs_int) 
31706  148 

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

149 
lemma gcd_cases_int: 
31706  150 
fixes x :: int and y 
151 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)" 

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

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

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

155 
shows "P (gcd x y)" 

35216  156 
by (insert assms, auto, arith) 
21256  157 

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

158 
lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0" 
31706  159 
by (simp add: gcd_int_def) 
160 

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

161 
lemma lcm_neg1_int: "lcm (x::int) y = lcm x y" 
31706  162 
by (simp add: lcm_int_def) 
163 

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

164 
lemma lcm_neg2_int: "lcm (x::int) (y) = lcm x y" 
31706  165 
by (simp add: lcm_int_def) 
166 

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

167 
lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)" 
31706  168 
by (simp add: lcm_int_def) 
21256  169 

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

172 

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

174 
by (metis abs_idempotent lcm_int_def) 

175 

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

177 
by (metis abs_idempotent lcm_int_def) 

178 

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

179 
lemma lcm_cases_int: 
31706  180 
fixes x :: int and y 
181 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)" 

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

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

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

185 
shows "P (lcm x y)" 

41550  186 
using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith 
31706  187 

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

188 
lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0" 
31706  189 
by (simp add: lcm_int_def) 
190 

191 
(* was gcd_0, etc. *) 

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

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

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

194 

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

196 
lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x" 
31706  197 
by (unfold gcd_int_def, auto) 
198 

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

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

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

201 

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

202 
lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x" 
31706  203 
by (unfold gcd_int_def, auto) 
204 

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

205 
lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)" 
31706  206 
by (case_tac "y = 0", auto) 
207 

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

209 

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

210 
lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)" 
31706  211 
by simp 
212 

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

213 
lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1" 
21263  214 
by simp 
21256  215 

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

216 
lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" 
31706  217 
by (simp add: One_nat_def) 
218 

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

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

221 

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

222 
lemma gcd_idem_nat: "gcd (x::nat) x = x" 
31798  223 
by simp 
31706  224 

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

225 
lemma gcd_idem_int: "gcd (x::int) x = abs x" 
31813  226 
by (auto simp add: gcd_int_def) 
31706  227 

228 
declare gcd_nat.simps [simp del] 

21256  229 

230 
text {* 

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

234 

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

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

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

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

238 
apply (simp_all add: gcd_non_0_nat) 
21256  239 
apply (blast dest: dvd_mod_imp_dvd) 
31706  240 
done 
241 

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

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

243 
by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat) 
21256  244 

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

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

246 
by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat) 
31706  247 

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

249 
by(metis gcd_dvd1_nat dvd_trans) 
31730  250 

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

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

252 
by(metis gcd_dvd2_nat dvd_trans) 
31730  253 

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

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

255 
by(metis gcd_dvd1_int dvd_trans) 
31730  256 

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

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

258 
by(metis gcd_dvd2_int dvd_trans) 
31730  259 

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

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

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

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

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

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

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

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

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

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

273 
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod) 
31706  274 

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

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

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

279 
apply (rule gcd_greatest_nat [transferred]) 
31813  280 
apply auto 
31706  281 
done 
21256  282 

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

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

285 
by (blast intro!: gcd_greatest_nat intro: dvd_trans) 
31706  286 

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

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

288 
by (blast intro!: gcd_greatest_int intro: dvd_trans) 
21256  289 

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

290 
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

291 
by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat) 
21256  292 

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

293 
lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)" 
31706  294 
by (auto simp add: gcd_int_def) 
21256  295 

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

296 
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

297 
by (insert gcd_zero_nat [of m n], arith) 
21256  298 

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

299 
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

300 
by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith) 
31706  301 

37770
cddb3106adb8
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
haftmann
parents:
36350
diff
changeset

302 
interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34915
diff
changeset

303 
proof 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34915
diff
changeset

304 
qed (auto intro: dvd_antisym dvd_trans) 
31706  305 

37770
cddb3106adb8
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
haftmann
parents:
36350
diff
changeset

306 
interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int" 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34915
diff
changeset

307 
proof 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34915
diff
changeset

308 
qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute) 
21256  309 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34915
diff
changeset

310 
lemmas gcd_assoc_nat = gcd_nat.assoc 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34915
diff
changeset

311 
lemmas gcd_commute_nat = gcd_nat.commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34915
diff
changeset

312 
lemmas gcd_left_commute_nat = gcd_nat.left_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34915
diff
changeset

313 
lemmas gcd_assoc_int = gcd_int.assoc 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34915
diff
changeset

314 
lemmas gcd_commute_int = gcd_int.commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34915
diff
changeset

315 
lemmas gcd_left_commute_int = gcd_int.left_commute 
31706  316 

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

317 
lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat 
21256  318 

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

319 
lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int 
31706  320 

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

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

33657  324 
apply (rule dvd_antisym) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

325 
apply (erule (1) gcd_greatest_nat) 
31706  326 
apply auto 
327 
done 

21256  328 

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

329 
lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and> 
31706  330 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 
33657  331 
apply (case_tac "d = 0") 
332 
apply simp 

333 
apply (rule iffI) 

334 
apply (rule zdvd_antisym_nonneg) 

335 
apply (auto intro: gcd_greatest_int) 

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

337 

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

339 
by (metis dvd.eq_iff gcd_unique_nat) 
31798  340 

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

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

342 
by (metis dvd.eq_iff gcd_unique_nat) 
31798  343 

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

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

345 
by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int) 
31798  346 

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

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

348 
by (metis gcd_proj1_if_dvd_int gcd_commute_int) 
31798  349 

350 

21256  351 
text {* 
352 
\medskip Multiplication laws 

353 
*} 

354 

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

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

357 
apply (induct m n rule: gcd_nat_induct) 
31706  358 
apply simp 
21256  359 
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

360 
apply (simp_all add: gcd_non_0_nat) 
31706  361 
done 
21256  362 

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

363 
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

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

366 
apply (rule gcd_mult_distrib_nat [transferred]) 
31706  367 
apply auto 
368 
done 

21256  369 

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

370 
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

371 
apply (insert gcd_mult_distrib_nat [of m k n]) 
21256  372 
apply simp 
373 
apply (erule_tac t = m in ssubst) 

374 
apply simp 

375 
done 

376 

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

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

380 
apply (subst dvd_abs_iff [symmetric]) 

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

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

382 
apply (rule coprime_dvd_mult_nat [transferred]) 
31813  383 
prefer 4 apply assumption 
384 
apply auto 

385 
apply (subst abs_mult [symmetric], auto) 

31706  386 
done 
387 

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

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

390 
by (auto intro: coprime_dvd_mult_nat) 
31706  391 

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

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

394 
by (auto intro: coprime_dvd_mult_int) 
31706  395 

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

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

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

399 
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

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

401 
apply (simp add: gcd_commute_nat) 
31706  402 
apply (simp_all add: mult_commute) 
403 
done 

21256  404 

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

405 
lemma gcd_mult_cancel_int: 
31813  406 
"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

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

409 
apply (rule gcd_mult_cancel_nat [transferred], auto) 
31706  410 
done 
21256  411 

35368  412 
lemma coprime_crossproduct_nat: 
413 
fixes a b c d :: nat 

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

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

416 
proof 

417 
assume ?rhs then show ?lhs by simp 

418 
next 

419 
assume ?lhs 

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

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

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

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

424 
from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult_commute) 

425 
with `coprime b c` have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat) 

426 
from `?lhs` have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult_commute) 

427 
with `coprime a d` have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat) 

428 
from `a dvd b` `b dvd a` have "a = b" by (rule Nat.dvd.antisym) 

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

430 
ultimately show ?rhs .. 

431 
qed 

432 

433 
lemma coprime_crossproduct_int: 

434 
fixes a b c d :: int 

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

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

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

438 

21256  439 
text {* \medskip Addition laws *} 
440 

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

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

443 
apply (simp_all add: gcd_non_0_nat) 
31706  444 
done 
445 

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

446 
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

447 
apply (subst (1 2) gcd_commute_nat) 
31706  448 
apply (subst add_commute) 
449 
apply simp 

450 
done 

451 

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

453 

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

454 
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

455 
by (subst gcd_add1_nat [symmetric], auto) 
31706  456 

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

457 
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

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

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

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

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

464 
apply (rule gcd_commute_nat) 
31706  465 
done 
466 

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

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

470 
apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] 
31706  471 
zmod_zminus1_eq_if) 
472 
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

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

474 
apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat 
31706  475 
nat_le_eq_zle) 
476 
done 

21256  477 

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

478 
lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)" 
31706  479 
apply (case_tac "y = 0") 
480 
apply force 

481 
apply (case_tac "y > 0") 

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

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

483 
apply (insert gcd_non_0_int [of "y" "x"]) 
35216  484 
apply auto 
31706  485 
done 
486 

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

487 
lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n" 
44821  488 
by (metis gcd_red_int mod_add_self1 add_commute) 
31706  489 

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

490 
lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n" 
44821  491 
by (metis gcd_add1_int gcd_commute_int add_commute) 
21256  492 

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

493 
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

494 
by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat) 
21256  495 

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

496 
lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n" 
44821  497 
by (metis gcd_commute_int gcd_red_int mod_mult_self1 add_commute) 
31798  498 

21256  499 

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

502 

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

504 
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

505 
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

506 

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

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

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

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

514 
by(bestsimp intro!:dvd_imp_le) 

515 
qed 

516 

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

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

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

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

523 
by(bestsimp intro!:dvd_imp_le_int) 

524 
qed 

525 

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

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

528 
apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le) 
31995  529 
apply simp 
530 
done 

531 

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

533 
apply(rule antisym) 

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

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

535 
apply (auto intro: abs_le_D1 dvd_imp_le_int) 
31995  536 
done 
537 

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

540 
apply(rule Max_eqI[THEN sym]) 

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

543 
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat) 
31734  544 
apply simp 
545 
done 

546 

547 
lemma gcd_is_Max_divisors_int: 

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

549 
apply(rule Max_eqI[THEN sym]) 

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

552 
apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le) 
31734  553 
apply simp 
554 
done 

555 

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

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

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

558 
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

559 

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

560 

31706  561 
subsection {* Coprimality *} 
562 

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

563 
lemma div_gcd_coprime_nat: 
31706  564 
assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0" 
565 
shows "coprime (a div gcd a b) (b div gcd a b)" 

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

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

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

571 
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

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

575 
unfolding dvd_def by blast 
31706  576 
then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" 
577 
by simp_all 

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

580 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

35216  581 
have "?g \<noteq> 0" using nz by simp 
31706  582 
then have gp: "?g > 0" by arith 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

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

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

586 

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

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

590 
apply (subst (1 2 3) gcd_abs_int) 
31813  591 
apply (subst (1 2) abs_div) 
592 
apply simp 

593 
apply simp 

594 
apply(subst (1 2) abs_gcd_int) 

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

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

596 
using nz apply (auto simp add: gcd_abs_int [symmetric]) 
31706  597 
done 
598 

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

599 
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

600 
using gcd_unique_nat[of 1 a b, simplified] by auto 
31706  601 

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

602 
lemma coprime_Suc_0_nat: 
31706  603 
"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

604 
using coprime_nat by (simp add: One_nat_def) 
31706  605 

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

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

608 
using gcd_unique_int [of 1 a b] 
31706  609 
apply clarsimp 
610 
apply (erule subst) 

611 
apply (rule iffI) 

612 
apply force 

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

614 
apply (case_tac "e >= 0") 

615 
apply force 

616 
apply force 

617 
done 

618 

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

619 
lemma gcd_coprime_nat: 
31706  620 
assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and 
621 
b: "b = b' * gcd a b" 

622 
shows "coprime a' b'" 

623 

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

625 
apply (erule ssubst) 

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

627 
apply (erule ssubst) 

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

628 
apply (rule div_gcd_coprime_nat) 
41550  629 
using z apply force 
31706  630 
apply (subst (1) b) 
631 
using z apply force 

632 
apply (subst (1) a) 

633 
using z apply force 

41550  634 
done 
31706  635 

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

636 
lemma gcd_coprime_int: 
31706  637 
assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and 
638 
b: "b = b' * gcd a b" 

639 
shows "coprime a' b'" 

640 

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

642 
apply (erule ssubst) 

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

644 
apply (erule ssubst) 

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

645 
apply (rule div_gcd_coprime_int) 
41550  646 
using z apply force 
31706  647 
apply (subst (1) b) 
648 
using z apply force 

649 
apply (subst (1) a) 

650 
using z apply force 

41550  651 
done 
31706  652 

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

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

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

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

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

658 
apply (subst gcd_commute_nat, rule db) 
31706  659 
done 
660 

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

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

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

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

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

666 
apply (subst gcd_commute_int, rule db) 
31706  667 
done 
668 

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

669 
lemma coprime_lmult_nat: 
31706  670 
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" 
671 
proof  

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

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

673 
by (rule gcd_greatest_nat, auto) 
31706  674 
with dab show ?thesis 
675 
by auto 

676 
qed 

677 

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

678 
lemma coprime_lmult_int: 
31798  679 
assumes "coprime (d::int) (a * b)" shows "coprime d a" 
31706  680 
proof  
681 
have "gcd d a dvd gcd d (a * b)" 

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

682 
by (rule gcd_greatest_int, auto) 
31798  683 
with assms show ?thesis 
31706  684 
by auto 
685 
qed 

686 

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

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

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

691 
by (rule gcd_greatest_nat, auto intro: dvd_mult) 
31798  692 
with assms show ?thesis 
31706  693 
by auto 
694 
qed 

695 

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

696 
lemma coprime_rmult_int: 
31706  697 
assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" 
698 
proof  

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

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

700 
by (rule gcd_greatest_int, auto intro: dvd_mult) 
31706  701 
with dab show ?thesis 
702 
by auto 

703 
qed 

704 

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

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

707 
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

708 
coprime_mult_nat[of d a b] 
31706  709 
by blast 
710 

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

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

713 
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

714 
coprime_mult_int[of d a b] 
31706  715 
by blast 
716 

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

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

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

721 
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

722 
using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult) 
31706  723 
done 
724 

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

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

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

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

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

730 
using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self) 
31706  731 
done 
732 

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

733 
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

734 
by (induct n, simp_all add: coprime_mult_nat) 
31706  735 

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

736 
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

737 
by (induct n, simp_all add: coprime_mult_int) 
31706  738 

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

739 
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

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

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

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

743 
apply (subst gcd_commute_nat, assumption) 
31706  744 
done 
745 

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

746 
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

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

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

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

750 
apply (subst gcd_commute_int, assumption) 
31706  751 
done 
752 

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

753 
lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n" 
31706  754 
proof (cases) 
755 
assume "a = 0 & b = 0" 

756 
thus ?thesis by simp 

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

758 
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

759 
by (auto simp:div_gcd_coprime_nat) 
31706  760 
hence "gcd ((a div gcd a b)^n * (gcd a b)^n) 
761 
((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" 

762 
apply (subst (1 2) mult_commute) 

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

763 
apply (subst gcd_mult_distrib_nat [symmetric]) 
31706  764 
apply simp 
765 
done 

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

767 
apply (subst div_power) 

768 
apply auto 

769 
apply (rule dvd_div_mult_self) 

770 
apply (rule dvd_power_same) 

771 
apply auto 

772 
done 

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

774 
apply (subst div_power) 

775 
apply auto 

776 
apply (rule dvd_div_mult_self) 

777 
apply (rule dvd_power_same) 

778 
apply auto 

779 
done 

780 
finally show ?thesis . 

781 
qed 

782 

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

783 
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

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

786 
apply (rule gcd_exp_nat [where n = n, transferred]) 
31706  787 
apply auto 
788 
done 

789 

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

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

793 
let ?g = "gcd a b" 

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

795 
moreover 

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

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

797 
from gcd_coprime_exists_nat[OF z] 
31706  798 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
799 
by blast 

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

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

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

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

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

805 
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

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

809 
with thb thc have ?thesis by blast } 

810 
ultimately show ?thesis by blast 

811 
qed 

812 

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

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

816 
let ?g = "gcd a b" 

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

818 
moreover 

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

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

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

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

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

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

826 
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 

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

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_int[OF ab'(3)] th_1 
31706  831 
have thc: "a' dvd c" by (subst (asm) mult_commute, blast) 
832 
from ab' have "a = ?g*a'" by algebra 

833 
with thb thc have ?thesis by blast } 

834 
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

835 
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

836 

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

837 
lemma pow_divides_pow_nat: 
31706  838 
assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0" 
839 
shows "a dvd b" 

840 
proof 

841 
let ?g = "gcd a b" 

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

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

844 
moreover 

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

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

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

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

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

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

853 
by (simp only: power_mult_distrib mult_commute) 

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

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

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

857 
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

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

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

862 
ultimately show ?thesis by blast 

863 
qed 

864 

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

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

868 
proof 
31706  869 
let ?g = "gcd a b" 
870 
from n obtain m where m: "n = Suc m" by (cases n, simp_all) 

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

872 
moreover 

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

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

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

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

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

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

881 
by (simp only: power_mult_distrib mult_commute) 

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

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

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

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

886 
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

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

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

891 
ultimately show ?thesis by blast 

892 
qed 

893 

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

894 
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

895 
by (auto intro: pow_divides_pow_nat dvd_power_same) 
31706  896 

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

897 
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

898 
by (auto intro: pow_divides_pow_int dvd_power_same) 
31706  899 

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

900 
lemma divides_mult_nat: 
31706  901 
assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n" 
902 
shows "m * n dvd r" 

903 
proof 

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

905 
unfolding dvd_def by blast 

906 
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

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

910 
qed 

911 

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

912 
lemma divides_mult_int: 
31706  913 
assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n" 
914 
shows "m * n dvd r" 

915 
proof 

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

917 
unfolding dvd_def by blast 

918 
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

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

922 
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

923 

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

924 
lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n" 
31706  925 
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1  n)") 
926 
apply force 

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

927 
apply (rule dvd_diff_nat) 
31706  928 
apply auto 
929 
done 

930 

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

931 
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

932 
using coprime_plus_one_nat by (simp add: One_nat_def) 
31706  933 

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

934 
lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n" 
31706  935 
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1  n)") 
936 
apply force 

937 
apply (rule dvd_diff) 

938 
apply auto 

939 
done 

940 

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

941 
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

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

943 
gcd_commute_nat [of "n  1" n] by auto 
31706  944 

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

945 
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

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

947 
gcd_commute_int [of "n  1" n] by auto 
31706  948 

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

949 
lemma setprod_coprime_nat [rule_format]: 
31706  950 
"(ALL i: A. coprime (f i) (x::nat)) > coprime (PROD i:A. f i) x" 
951 
apply (case_tac "finite A") 

952 
apply (induct set: finite) 

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

953 
apply (auto simp add: gcd_mult_cancel_nat) 
31706  954 
done 
955 

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

956 
lemma setprod_coprime_int [rule_format]: 
31706  957 
"(ALL i: A. coprime (f i) (x::int)) > coprime (PROD i:A. f i) x" 
958 
apply (case_tac "finite A") 

959 
apply (induct set: finite) 

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

960 
apply (auto simp add: gcd_mult_cancel_int) 
31706  961 
done 
962 

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

963 
lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> 
31706  964 
x dvd b \<Longrightarrow> x = 1" 
965 
apply (subgoal_tac "x dvd gcd a b") 

966 
apply simp 

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

967 
apply (erule (1) gcd_greatest_nat) 
31706  968 
done 
969 

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

970 
lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> 
31706  971 
x dvd b \<Longrightarrow> abs x = 1" 
972 
apply (subgoal_tac "x dvd gcd a b") 

973 
apply simp 

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

974 
apply (erule (1) gcd_greatest_int) 
31706  975 
done 
976 

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

977 
lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> 
31706  978 
coprime d e" 
979 
apply (auto simp add: dvd_def) 

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

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

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

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

983 
apply (erule coprime_lmult_int) 
31706  984 
done 
985 

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

986 
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

987 
apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat) 
31706  988 
done 
989 

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

990 
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

991 
apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int) 
31706  992 
done 
993 

994 

995 
subsection {* Bezout's theorem *} 

996 

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

998 
see the theorems that follow the definition. *) 

999 
fun 

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

1001 
where 

1002 
"bezw x y = 

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

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

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

1006 

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

1008 

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

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

1011 
by simp 

1012 

1013 
declare bezw.simps [simp del] 

1014 

1015 
lemma bezw_aux [rule_format]: 

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

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

1020 
by auto 

1021 
next fix m :: nat and n 

1022 
assume ngt0: "n > 0" and 

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

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

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

1026 
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

1027 
apply (simp add: bezw_non_0 gcd_non_0_nat) 
31706  1028 
apply (erule subst) 
36350  1029 
apply (simp add: field_simps) 
31706  1030 
apply (subst mod_div_equality [of m n, symmetric]) 
1031 
(* applying simp here undoes the last substitution! 

1032 
what is procedure cancel_div_mod? *) 

44821  1033 
apply (simp only: field_simps of_nat_add of_nat_mult) 
31706  1034 
done 
1035 
qed 

1036 

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

1037 
lemma bezout_int: 
31706  1038 
fixes x y 
1039 
shows "EX u v. u * (x::int) + v * y = gcd x y" 

1040 
proof  

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

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

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

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

1045 
apply (unfold gcd_int_def) 

1046 
apply simp 

1047 
apply (subst bezw_aux [symmetric]) 

1048 
apply auto 

1049 
done 

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

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

1052 
by auto 

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

1054 
by (erule (1) bezout_aux) 

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

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

1057 
apply auto 

1058 
apply (rule_tac x = u in exI) 

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

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

1060 
apply (subst gcd_neg2_int [symmetric]) 
31706  1061 
apply auto 
1062 
done 

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

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

1065 
apply auto 

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

1067 
apply (rule_tac x = v in exI) 

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

1068 
apply (subst gcd_neg1_int [symmetric]) 
31706  1069 
apply auto 
1070 
done 

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

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

1073 
apply auto 

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

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

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

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

1077 
apply (subst gcd_neg2_int [symmetric]) 
31706  1078 
apply auto 
1079 
done 

1080 
ultimately show ?thesis by blast 

1081 
qed 

1082 

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

1084 

1085 
lemma ind_euclid: 

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

1087 
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

1088 
shows "P a b" 
34915  1089 
proof(induct "a + b" arbitrary: a b rule: less_induct) 
1090 
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

1091 
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

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

1095 
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

1096 
{assume lt: "a < b" 
34915  1097 
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

1098 
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

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

1100 
moreover 
34915  1101 
{assume "a + b  a < a + b" 
1102 
also have th0: "a + b  a = a + (b  a)" using lt by arith 

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

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

1105 
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

1106 
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

1107 
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

1108 
{assume lt: "a > b" 
34915  1109 
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

1110 
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

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

1112 
moreover 
34915  1113 
{assume "b + a  b < a + b" 
1114 
also have th0: "b + a  b = b + (a  b)" using lt by arith 

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

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

1117 
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

1118 
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

1119 
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

1120 
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

1121 
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

1122 

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

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

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

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

1128 
using ex 

1129 
apply clarsimp 

35216  1130 
apply (rule_tac x="d" in exI, simp) 
31706  1131 
apply (case_tac "a * x = b * y + d" , simp_all) 
1132 
apply (rule_tac x="x + y" in exI) 

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

1134 
apply algebra 

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

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

1137 
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

1138 
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

1139 

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

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

1143 
apply blast 

1144 
apply clarify 

35216  1145 
apply (rule_tac x="a" in exI, simp) 
31706  1146 
apply clarsimp 
1147 
apply (rule_tac x="d" in exI) 

35216  1148 
apply (case_tac "a * x = b * y + d", simp_all) 
31706  1149 
apply (rule_tac x="x+y" in exI) 
1150 
apply (rule_tac x="y" in exI) 

1151 
apply algebra 

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

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

1154 
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

1155 
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

1156 

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

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

1159 
using bezout_add_nat[of a b] 
31706  1160 
apply clarsimp 
1161 
apply (rule_tac x="d" in exI, simp) 

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

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

1164 
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

1165 
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

1166 

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

1167 
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

1168 
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

1169 
proof 
31706  1170 
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

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

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

1177 
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

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

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

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

1184 
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

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

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

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

1189 
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

1190 
moreover 
31706  1191 
{assume db: "d < b" 
41550  1192 
{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

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

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

1195 
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

1196 
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

1197 
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

1198 
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

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

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

1202 
by (simp only: mult_assoc right_distrib) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

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

1205 
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

1206 
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

1207 
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

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

1209 
by (simp only: diff_mult_distrib2 add_commute mult_ac) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

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

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

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

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

1214 
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

1215 
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

1216 
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

1217 
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

1218 
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

1219 
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

1220 

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

1221 
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

1222 
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

1223 
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

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

1225 
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

1226 
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

1227 
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

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

1230 
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

1231 
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

1232 
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

1233 

31706  1234 

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

1235 
subsection {* LCM properties *} 
31706  1236 

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

1237 
lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b" 
31706  1238 
by (simp add: lcm_int_def lcm_nat_def zdiv_int 
44821  1239 
of_nat_mult gcd_int_def) 
31706  1240 

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

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

1243 
by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat]) 
31706  1244 

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

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

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

1248 
apply (subst prod_gcd_lcm_nat [symmetric]) 
31706  1249 
apply (subst nat_abs_mult_distrib [symmetric]) 
1250 
apply (simp, simp add: abs_mult) 

1251 
done 

1252 

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

1253 
lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0" 
31706  1254 
unfolding lcm_nat_def by simp 
1255 

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

1256 
lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0" 
31706  1257 
unfolding lcm_int_def by simp 
1258 

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

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

1261 

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

1262 
lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0" 
31706  1263 
unfolding lcm_int_def by simp 
1264 

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

1265 
lemma lcm_pos_nat: 
31798  1266 
"(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

1267 
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

1268 

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

1269 
lemma lcm_pos_int: 
31798  1270 
"(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

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

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

1275 

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

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

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

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

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

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

1281 

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

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

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

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

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

1288 
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

1289 
from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1290 
with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

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

1294 
from pos_k k_n have pos_q: "q > 0" by auto 
27556  1295 
have "k * k * gcd q p = k * gcd (k * q) (k * p)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1296 
by (simp add: mult_ac gcd_mult_distrib_nat) 
27556  1297 
also have "\<dots> = k * gcd (m * p * q) (n * q * p)" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

1298 
by (simp add: k_m [symmetric] k_n [symmetric]) 
27556  1299 
also have "\<dots> = k * p * q * gcd m n" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

1300 
by (simp add: mult_ac gcd_mult_distrib_nat) 
27556  1301 
finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

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

1307 
with prod_gcd_lcm_nat [of m n] 
27556  1308 
have "lcm m n * gcd q p * gcd m n = k * gcd m n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

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

1313 

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

1314 
lemma lcm_least_int: 
31798  1315 
"(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k" 