author  haftmann 
Thu, 23 Oct 2014 14:04:05 +0200  
changeset 58770  ae5e9b4f8daf 
parent 58623  2db1df2c8467 
child 58776  95e58e04e534 
permissions  rwrr 
32479  1 
(* Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, 
31798  2 
Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow 
31706  3 

4 

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

31706  7 

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

9 

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

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

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

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

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

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

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

34915  19 
the natural numbers by Chaieb. 
31706  20 

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

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

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

23 

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

31706  27 

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

30 
theory GCD 

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

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

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

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

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

140 

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

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

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

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

144 

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

147 

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

148 
lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)" 
31813  149 
by (simp add: gcd_int_def) 
150 

151 
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

152 
by (metis abs_idempotent gcd_abs_int) 
31813  153 

154 
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

155 
by (metis abs_idempotent gcd_abs_int) 
31706  156 

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

157 
lemma gcd_cases_int: 
31706  158 
fixes x :: int and y 
159 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)" 

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

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

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

163 
shows "P (gcd x y)" 

35216  164 
by (insert assms, auto, arith) 
21256  165 

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

166 
lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0" 
31706  167 
by (simp add: gcd_int_def) 
168 

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

169 
lemma lcm_neg1_int: "lcm (x::int) y = lcm x y" 
31706  170 
by (simp add: lcm_int_def) 
171 

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

172 
lemma lcm_neg2_int: "lcm (x::int) (y) = lcm x y" 
31706  173 
by (simp add: lcm_int_def) 
174 

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

175 
lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)" 
31706  176 
by (simp add: lcm_int_def) 
21256  177 

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

180 

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

182 
by (metis abs_idempotent lcm_int_def) 

183 

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

185 
by (metis abs_idempotent lcm_int_def) 

186 

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

187 
lemma lcm_cases_int: 
31706  188 
fixes x :: int and y 
189 
assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)" 

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

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

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

193 
shows "P (lcm x y)" 

41550  194 
using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith 
31706  195 

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

196 
lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0" 
31706  197 
by (simp add: lcm_int_def) 
198 

199 
(* was gcd_0, etc. *) 

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

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

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

202 

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

204 
lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x" 
31706  205 
by (unfold gcd_int_def, auto) 
206 

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

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

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

209 

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

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

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

213 
lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)" 
31706  214 
by (case_tac "y = 0", auto) 
215 

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

217 

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

218 
lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)" 
31706  219 
by simp 
220 

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

221 
lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1" 
21263  222 
by simp 
21256  223 

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

224 
lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" 
31706  225 
by (simp add: One_nat_def) 
226 

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

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

229 

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

230 
lemma gcd_idem_nat: "gcd (x::nat) x = x" 
31798  231 
by simp 
31706  232 

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

233 
lemma gcd_idem_int: "gcd (x::int) x = abs x" 
31813  234 
by (auto simp add: gcd_int_def) 
31706  235 

236 
declare gcd_nat.simps [simp del] 

21256  237 

238 
text {* 

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

242 

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

243 
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

244 
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

245 
apply (induct m n rule: gcd_nat_induct) 
54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

246 
apply (simp_all add: gcd_non_0_nat gcd_0_nat) 
21256  247 
apply (blast dest: dvd_mod_imp_dvd) 
31706  248 
done 
249 

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

250 
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

251 
by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat) 
21256  252 

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

253 
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

254 
by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat) 
31706  255 

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

257 
by(metis gcd_dvd1_nat dvd_trans) 
31730  258 

259 
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

260 
by(metis gcd_dvd2_nat dvd_trans) 
31730  261 

262 
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

263 
by(metis gcd_dvd1_int dvd_trans) 
31730  264 

265 
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

266 
by(metis gcd_dvd2_int dvd_trans) 
31730  267 

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

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

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

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

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

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

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

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

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

280 
lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n" 
54867
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

281 
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat) 
31706  282 

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

283 
lemma gcd_greatest_int: 
31813  284 
"(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

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

287 
apply (rule gcd_greatest_nat [transferred]) 
31813  288 
apply auto 
31706  289 
done 
21256  290 

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

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

293 
by (blast intro!: gcd_greatest_nat intro: dvd_trans) 
31706  294 

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

295 
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

296 
by (blast intro!: gcd_greatest_int intro: dvd_trans) 
21256  297 

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

298 
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

299 
by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat) 
21256  300 

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

301 
lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)" 
31706  302 
by (auto simp add: gcd_int_def) 
21256  303 

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

304 
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

305 
by (insert gcd_zero_nat [of m n], arith) 
21256  306 

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

307 
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

308 
by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith) 
31706  309 

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

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

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

314 
apply (erule (1) gcd_greatest_nat) 
31706  315 
apply auto 
316 
done 

21256  317 

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

318 
lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and> 
31706  319 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 
33657  320 
apply (case_tac "d = 0") 
321 
apply simp 

322 
apply (rule iffI) 

323 
apply (rule zdvd_antisym_nonneg) 

324 
apply (auto intro: gcd_greatest_int) 

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

326 

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

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

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

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

330 
apply (auto intro: dvd_antisym dvd_trans)[4] 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

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

332 
apply (auto intro: dvdI elim: dvdE) 
c21a2465cac1
prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents:
54489
diff
changeset

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

334 

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

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

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

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

338 

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

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

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

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

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

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

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

345 

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

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

347 

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

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

349 

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

351 
by (fact gcd_nat.absorb1) 
31798  352 

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

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

354 
by (fact gcd_nat.absorb2) 
31798  355 

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

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

357 
by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int) 
31798  358 

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

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

360 
by (metis gcd_proj1_if_dvd_int gcd_commute_int) 
31798  361 

21256  362 
text {* 
363 
\medskip Multiplication laws 

364 
*} 

365 

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

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

368 
apply (induct m n rule: gcd_nat_induct) 
31706  369 
apply simp 
21256  370 
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

371 
apply (simp_all add: gcd_non_0_nat) 
31706  372 
done 
21256  373 

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

374 
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

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

377 
apply (rule gcd_mult_distrib_nat [transferred]) 
31706  378 
apply auto 
379 
done 

21256  380 

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

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

382 
apply (insert gcd_mult_distrib_nat [of m k n]) 
21256  383 
apply simp 
384 
apply (erule_tac t = m in ssubst) 

385 
apply simp 

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_int: 
31813  389 
"coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m" 
390 
apply (subst abs_dvd_iff [symmetric]) 

391 
apply (subst dvd_abs_iff [symmetric]) 

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

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

393 
apply (rule coprime_dvd_mult_nat [transferred]) 
31813  394 
prefer 4 apply assumption 
395 
apply auto 

396 
apply (subst abs_mult [symmetric], auto) 

31706  397 
done 
398 

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

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

401 
by (auto intro: coprime_dvd_mult_nat) 
31706  402 

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

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

405 
by (auto intro: coprime_dvd_mult_int) 
31706  406 

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

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

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

410 
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

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

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

413 
apply (simp_all add: mult.commute) 
31706  414 
done 
21256  415 

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

416 
lemma gcd_mult_cancel_int: 
31813  417 
"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

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

420 
apply (rule gcd_mult_cancel_nat [transferred], auto) 
31706  421 
done 
21256  422 

35368  423 
lemma coprime_crossproduct_nat: 
424 
fixes a b c d :: nat 

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

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

427 
proof 

428 
assume ?rhs then show ?lhs by simp 

429 
next 

430 
assume ?lhs 

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

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

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

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

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

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

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

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

441 
ultimately show ?rhs .. 

442 
qed 

443 

444 
lemma coprime_crossproduct_int: 

445 
fixes a b c d :: int 

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

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

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

449 

21256  450 
text {* \medskip Addition laws *} 
451 

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

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

454 
apply (simp_all add: gcd_non_0_nat) 
31706  455 
done 
456 

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

457 
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

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

459 
apply (subst add.commute) 
31706  460 
apply simp 
461 
done 

462 

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

464 

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

465 
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

466 
by (subst gcd_add1_nat [symmetric], auto) 
31706  467 

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

468 
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

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

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

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

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

475 
apply (rule gcd_commute_nat) 
31706  476 
done 
477 

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

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

481 
apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] 
31706  482 
zmod_zminus1_eq_if) 
483 
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

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

485 
apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat 
31706  486 
nat_le_eq_zle) 
487 
done 

21256  488 

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

489 
lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)" 
31706  490 
apply (case_tac "y = 0") 
491 
apply force 

492 
apply (case_tac "y > 0") 

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

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

494 
apply (insert gcd_non_0_int [of "y" "x"]) 
35216  495 
apply auto 
31706  496 
done 
497 

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

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

499 
by (metis gcd_red_int mod_add_self1 add.commute) 
31706  500 

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

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

502 
by (metis gcd_add1_int gcd_commute_int add.commute) 
21256  503 

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

504 
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

505 
by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat) 
21256  506 

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

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

508 
by (metis gcd_commute_int gcd_red_int mod_mult_self1 add.commute) 
31798  509 

21256  510 

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

513 

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

515 
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

516 
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

517 

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

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

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

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

525 
by(bestsimp intro!:dvd_imp_le) 

526 
qed 

527 

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

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

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

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

534 
by(bestsimp intro!:dvd_imp_le_int) 

535 
qed 

536 

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

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

539 
apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le) 
31995  540 
apply simp 
541 
done 

542 

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

544 
apply(rule antisym) 

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

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

546 
apply (auto intro: abs_le_D1 dvd_imp_le_int) 
31995  547 
done 
548 

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

551 
apply(rule Max_eqI[THEN sym]) 

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

554 
apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat) 
31734  555 
apply simp 
556 
done 

557 

558 
lemma gcd_is_Max_divisors_int: 

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

560 
apply(rule Max_eqI[THEN sym]) 

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

563 
apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le) 
31734  564 
apply simp 
565 
done 

566 

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

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

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

569 
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

570 

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

571 

31706  572 
subsection {* Coprimality *} 
573 

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

574 
lemma div_gcd_coprime_nat: 
31706  575 
assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0" 
576 
shows "coprime (a div gcd a b) (b div gcd a b)" 

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

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

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

582 
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

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

586 
unfolding dvd_def by blast 
31706  587 
then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" 
588 
by simp_all 

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

591 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

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

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

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

597 

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

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

601 
apply (subst (1 2 3) gcd_abs_int) 
31813  602 
apply (subst (1 2) abs_div) 
603 
apply simp 

604 
apply simp 

605 
apply(subst (1 2) abs_gcd_int) 

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

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

607 
using nz apply (auto simp add: gcd_abs_int [symmetric]) 
31706  608 
done 
609 

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

610 
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

611 
using gcd_unique_nat[of 1 a b, simplified] by auto 
31706  612 

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

613 
lemma coprime_Suc_0_nat: 
31706  614 
"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

615 
using coprime_nat by (simp add: One_nat_def) 
31706  616 

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

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

619 
using gcd_unique_int [of 1 a b] 
31706  620 
apply clarsimp 
621 
apply (erule subst) 

622 
apply (rule iffI) 

623 
apply force 

48562
f6d6d58fa318
tuned proofs  avoid odd situations of polymorphic Frees in goal state;
wenzelm
parents:
45992
diff
changeset

624 
apply (drule_tac x = "abs ?e" in exI) 
f6d6d58fa318
tuned proofs  avoid odd situations of polymorphic Frees in goal state;
wenzelm
parents:
45992
diff
changeset

625 
apply (case_tac "(?e::int) >= 0") 
31706  626 
apply force 
627 
apply force 

628 
done 

629 

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

630 
lemma gcd_coprime_nat: 
31706  631 
assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and 
632 
b: "b = b' * gcd a b" 

633 
shows "coprime a' b'" 

634 

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

636 
apply (erule ssubst) 

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

638 
apply (erule ssubst) 

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

639 
apply (rule div_gcd_coprime_nat) 
41550  640 
using z apply force 
31706  641 
apply (subst (1) b) 
642 
using z apply force 

643 
apply (subst (1) a) 

644 
using z apply force 

41550  645 
done 
31706  646 

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

647 
lemma gcd_coprime_int: 
31706  648 
assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and 
649 
b: "b = b' * gcd a b" 

650 
shows "coprime a' b'" 

651 

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

653 
apply (erule ssubst) 

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

655 
apply (erule ssubst) 

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

656 
apply (rule div_gcd_coprime_int) 
41550  657 
using z apply force 
31706  658 
apply (subst (1) b) 
659 
using z apply force 

660 
apply (subst (1) a) 

661 
using z apply force 

41550  662 
done 
31706  663 

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

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

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

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

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

669 
apply (subst gcd_commute_nat, rule db) 
31706  670 
done 
671 

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

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

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

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

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

677 
apply (subst gcd_commute_int, rule db) 
31706  678 
done 
679 

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

680 
lemma coprime_lmult_nat: 
31706  681 
assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" 
682 
proof  

683 
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

684 
by (rule gcd_greatest_nat, auto) 
31706  685 
with dab show ?thesis 
686 
by auto 

687 
qed 

688 

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

689 
lemma coprime_lmult_int: 
31798  690 
assumes "coprime (d::int) (a * b)" shows "coprime d a" 
31706  691 
proof  
692 
have "gcd d a dvd gcd d (a * b)" 

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

693 
by (rule gcd_greatest_int, auto) 
31798  694 
with assms show ?thesis 
31706  695 
by auto 
696 
qed 

697 

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

698 
lemma coprime_rmult_nat: 
31798  699 
assumes "coprime (d::nat) (a * b)" shows "coprime d b" 
31706  700 
proof  
701 
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

702 
by (rule gcd_greatest_nat, auto intro: dvd_mult) 
31798  703 
with assms show ?thesis 
31706  704 
by auto 
705 
qed 

706 

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

707 
lemma coprime_rmult_int: 
31706  708 
assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" 
709 
proof  

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

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

711 
by (rule gcd_greatest_int, auto intro: dvd_mult) 
31706  712 
with dab show ?thesis 
713 
by auto 

714 
qed 

715 

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

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

718 
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

719 
coprime_mult_nat[of d a b] 
31706  720 
by blast 
721 

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

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

724 
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

725 
coprime_mult_int[of d a b] 
31706  726 
by blast 
727 

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

730 
using assms 

731 
proof (induct n) 

732 
case (Suc n) then show ?case 

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

734 
qed simp 

735 

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

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

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

740 
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

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

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

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

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

748 
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

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

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

752 
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

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

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

755 
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

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

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

758 
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

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

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

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

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

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

765 
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

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

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

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

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

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

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

775 
thus ?thesis by simp 

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

777 
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

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

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

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

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

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

786 
apply (subst div_power) 

787 
apply auto 

788 
apply (rule dvd_div_mult_self) 

789 
apply (rule dvd_power_same) 

790 
apply auto 

791 
done 

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

793 
apply (subst div_power) 

794 
apply auto 

795 
apply (rule dvd_div_mult_self) 

796 
apply (rule dvd_power_same) 

797 
apply auto 

798 
done 

799 
finally show ?thesis . 

800 
qed 

801 

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

802 
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

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

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

808 

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

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

812 
let ?g = "gcd a b" 

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

814 
moreover 

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

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

816 
from gcd_coprime_exists_nat[OF z] 
31706  817 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
818 
by blast 

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

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

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

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

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

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

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

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

829 
ultimately show ?thesis by blast 

830 
qed 

831 

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

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

835 
let ?g = "gcd a b" 

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

837 
moreover 

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

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

839 
from gcd_coprime_exists_int[OF z] 
31706  840 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
841 
by blast 

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

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

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

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

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

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

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

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

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

853 
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

854 
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

855 

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

856 
lemma pow_divides_pow_nat: 
31706  857 
assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0" 
858 
shows "a dvd b" 

859 
proof 

860 
let ?g = "gcd a b" 

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

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

863 
moreover 

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

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

866 
from gcd_coprime_exists_nat[OF z] 
31706  867 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
868 
by blast 

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

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

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

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

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

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

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

876 
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

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

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

881 
ultimately show ?thesis by blast 

882 
qed 

883 

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

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

887 
proof 
31706  888 
let ?g = "gcd a b" 
889 
from n obtain m where m: "n = Suc m" by (cases n, simp_all) 

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

891 
moreover 

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

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

894 
from gcd_coprime_exists_int[OF z] 
31706  895 
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" 
896 
by blast 

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

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

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

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

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

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

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

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

905 
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

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

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

910 
ultimately show ?thesis by blast 

911 
qed 

912 

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

913 
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

914 
by (auto intro: pow_divides_pow_nat dvd_power_same) 
31706  915 

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

916 
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

917 
by (auto intro: pow_divides_pow_int dvd_power_same) 
31706  918 

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

919 
lemma divides_mult_nat: 
31706  920 
assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n" 
921 
shows "m * n dvd r" 

922 
proof 

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

924 
unfolding dvd_def by blast 

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

925 
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

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

929 
qed 

930 

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

931 
lemma divides_mult_int: 
31706  932 
assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n" 
933 
shows "m * n dvd r" 

934 
proof 

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

936 
unfolding dvd_def by blast 

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

937 
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

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

941 
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

942 

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

943 
lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n" 
31706  944 
apply (subgoal_tac "gcd (n + 1) n dvd (n + 1  n)") 
945 
apply force 

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

946 
apply (rule dvd_diff_nat) 
31706  947 
apply auto 
948 
done 

949 

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

950 
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

951 
using coprime_plus_one_nat by (simp add: One_nat_def) 
31706  952 

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

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

956 
apply (rule dvd_diff) 

957 
apply auto 

958 
done 

959 

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

960 
lemma coprime_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

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

962 
gcd_commute_nat [of "n  1" n] by auto 
31706  963 

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

964 
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

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

966 
gcd_commute_int [of "n  1" n] by auto 
31706  967 

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

968 
lemma setprod_coprime_nat [rule_format]: 
31706  969 
"(ALL i: A. coprime (f i) (x::nat)) > coprime (PROD i:A. f i) x" 
970 
apply (case_tac "finite A") 

971 
apply (induct set: finite) 

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

972 
apply (auto simp add: gcd_mult_cancel_nat) 
31706  973 
done 
974 

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

975 
lemma setprod_coprime_int [rule_format]: 
31706  976 
"(ALL i: A. coprime (f i) (x::int)) > coprime (PROD i:A. f i) x" 
977 
apply (case_tac "finite A") 

978 
apply (induct set: finite) 

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

979 
apply (auto simp add: gcd_mult_cancel_int) 
31706  980 
done 
981 

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

982 
lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> 
31706  983 
x dvd b \<Longrightarrow> x = 1" 
984 
apply (subgoal_tac "x dvd gcd a b") 

985 
apply simp 

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

986 
apply (erule (1) gcd_greatest_nat) 
31706  987 
done 
988 

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

989 
lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> 
31706  990 
x dvd b \<Longrightarrow> abs x = 1" 
991 
apply (subgoal_tac "x dvd gcd a b") 

992 
apply simp 

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

993 
apply (erule (1) gcd_greatest_int) 
31706  994 
done 
995 

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

996 
lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> 
31706  997 
coprime d e" 
998 
apply (auto simp add: dvd_def) 

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

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

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

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

1002 
apply (erule coprime_lmult_int) 
31706  1003 
done 
1004 

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

1005 
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

1006 
apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat) 
31706  1007 
done 
1008 

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

1009 
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

1010 
apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int) 
31706  1011 
done 
1012 

1013 

1014 
subsection {* Bezout's theorem *} 

1015 

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

1017 
see the theorems that follow the definition. *) 

1018 
fun 

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

1020 
where 

1021 
"bezw x y = 

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

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

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

1025 

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

1027 

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

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

1030 
by simp 

1031 

1032 
declare bezw.simps [simp del] 

1033 

1034 
lemma bezw_aux [rule_format]: 

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

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

1039 
by auto 

1040 
next fix m :: nat and n 

1041 
assume ngt0: "n > 0" and 

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

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

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

1045 
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

1046 
apply (simp add: bezw_non_0 gcd_non_0_nat) 
31706  1047 
apply (erule subst) 
36350  1048 
apply (simp add: field_simps) 
31706  1049 
apply (subst mod_div_equality [of m n, symmetric]) 
1050 
(* applying simp here undoes the last substitution! 

1051 
what is procedure cancel_div_mod? *) 

44821  1052 
apply (simp only: field_simps of_nat_add of_nat_mult) 
31706  1053 
done 
1054 
qed 

1055 

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

1056 
lemma bezout_int: 
31706  1057 
fixes x y 
1058 
shows "EX u v. u * (x::int) + v * y = gcd x y" 

1059 
proof  

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

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

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

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

1064 
apply (unfold gcd_int_def) 

1065 
apply simp 

1066 
apply (subst bezw_aux [symmetric]) 

1067 
apply auto 

1068 
done 

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

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

1071 
by auto 

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

1073 
by (erule (1) bezout_aux) 

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

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

1076 
apply auto 

1077 
apply (rule_tac x = u in exI) 

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

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

1079 
apply (subst gcd_neg2_int [symmetric]) 
31706  1080 
apply auto 
1081 
done 

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

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

1084 
apply auto 

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

1086 
apply (rule_tac x = v in exI) 

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

1087 
apply (subst gcd_neg1_int [symmetric]) 
31706  1088 
apply auto 
1089 
done 

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

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

1092 
apply auto 

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

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

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

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

1096 
apply (subst gcd_neg2_int [symmetric]) 
31706  1097 
apply auto 
1098 
done 

1099 
ultimately show ?thesis by blast 

1100 
qed 

1101 

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

1103 

1104 
lemma ind_euclid: 

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

1106 
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

1107 
shows "P a b" 
34915  1108 
proof(induct "a + b" arbitrary: a b rule: less_induct) 
1109 
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

1110 
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

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

1114 
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

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

1117 
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

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

1119 
moreover 
34915  1120 
{assume "a + b  a < a + b" 
1121 
also have th0: "a + b  a = a + (b  a)" using lt by arith 

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

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

1124 
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

1125 
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

1126 
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

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

1129 
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

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

1131 
moreover 
34915  1132 
{assume "b + a  b < a + b" 
1133 
also have th0: "b + a  b = b + (a  b)" using lt by arith 

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

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

1136 
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

1137 
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

1138 
ultimately have "P a b" by blast} 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

1139 
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

1140 
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

1141 

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

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

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

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

1147 
using ex 

1148 
apply clarsimp 

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

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

1153 
apply algebra 

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

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

1156 
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

1157 
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

1158 

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

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

1162 
apply blast 

1163 
apply clarify 

35216  1164 
apply (rule_tac x="a" in exI, simp) 
31706  1165 
apply clarsimp 
1166 
apply (rule_tac x="d" in exI) 

35216  1167 
apply (case_tac "a * x = b * y + d", simp_all) 
31706  1168 
apply (rule_tac x="x+y" in exI) 
1169 
apply (rule_tac x="y" in exI) 

1170 
apply algebra 

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

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

1173 
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

1174 
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

1175 

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

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

1178 
using bezout_add_nat[of a b] 
31706  1179 
apply clarsimp 
1180 
apply (rule_tac x="d" in exI, simp) 

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

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

1183 
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

1184 
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

1185 

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

1186 
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

1187 
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

1188 
proof 
31706  1189 
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

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

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

1196 
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

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

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

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

1203 
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

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

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

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

1208 
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

1209 
moreover 
31706  1210 
{assume db: "d < b" 
41550  1211 
{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

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

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

1214 
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

1215 
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

1216 
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

1217 
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

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

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

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

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

1224 
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

1225 
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

1226 
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

1227 
hence "a * ((b  1) * y) = b*(x*(b  1)  d) + d" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

1228 
by (simp only: diff_mult_distrib2 add.commute ac_simps) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32879
diff
changeset

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

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

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

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

1233 
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

1234 
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

1235 
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

1236 
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

1237 
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

1238 
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

1239 

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

1240 
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

1241 
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

1242 
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

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

1244 
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

1245 
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

1246 
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

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

1249 
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

1250 
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

1251 
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

1252 

31706  1253 

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

1254 
subsection {* LCM properties *} 
31706  1255 

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

1256 
lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b" 
31706  1257 
by (simp add: lcm_int_def lcm_nat_def zdiv_int 
44821  1258 
of_nat_mult gcd_int_def) 
31706  1259 

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

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

1262 
by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat]) 
31706  1263 

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

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

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

1267 
apply (subst prod_gcd_lcm_nat [symmetric]) 
31706  1268 
apply (subst nat_abs_mult_distrib [symmetric]) 
1269 
apply (simp, simp add: abs_mult) 

1270 
done 

1271 

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

1272 
lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0" 
31706  1273 
unfolding lcm_nat_def by simp 
1274 

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

1275 
lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0" 
31706  1276 
unfolding lcm_int_def by simp 
1277 

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

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

1280 

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

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

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

1284 
lemma lcm_pos_nat: 
31798  1285 
"(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

1286 
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

1287 

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

1288 
lemma lcm_pos_int: 
31798  1289 
"(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

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

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

1294 

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

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

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

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

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

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

1300 

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

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

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

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

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

1307 
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

1308 
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

1309 
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

1310 
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

1311 
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

1312 
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

1313 
from pos_k k_n have pos_q: "q > 0" by auto 
27556 