author  chaieb 
Mon, 21 Jul 2008 13:37:05 +0200  
changeset 27669  4b1642284dd7 
parent 27651  16a26996c30e 
child 27676  55676111ed69 
permissions  rwrr 
21256  1 
(* Title: HOL/GCD.thy 
2 
ID: $Id$ 

3 
Author: Christophe Tabacznyj and Lawrence C Paulson 

4 
Copyright 1996 University of Cambridge 

5 
*) 

6 

7 
header {* The Greatest Common Divisor *} 

8 

9 
theory GCD 

27487  10 
imports Plain "~~/src/HOL/Presburger" 
21256  11 
begin 
12 

13 
text {* 

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

14 
See \cite{davenport92}. \bigskip 
21256  15 
*} 
16 

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

17 
subsection {* Specification of GCD on nats *} 
21256  18 

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

20 
is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where  {* @{term gcd} as a relation *} 
27556  21 
[code func del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and> 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

22 
(\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

23 

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

24 
text {* Uniqueness *} 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

25 

27556  26 
lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

27 
by (simp add: is_gcd_def) (blast intro: dvd_anti_sym) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

28 

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

29 
text {* Connection to divides relation *} 
21256  30 

27556  31 
lemma is_gcd_dvd: "is_gcd a b m \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

32 
by (auto simp add: is_gcd_def) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

33 

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

34 
text {* Commutativity *} 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

35 

27556  36 
lemma is_gcd_commute: "is_gcd m n k = is_gcd n m k" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

37 
by (auto simp add: is_gcd_def) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

38 

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

39 

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

40 
subsection {* GCD on nat by Euclid's algorithm *} 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

41 

27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

42 
fun 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

43 
gcd :: "nat => nat => nat" 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

44 
where 
27556  45 
"gcd m n = (if n = 0 then m else gcd n (m mod n))" 
46 
lemma gcd_induct [case_names "0" rec]: 

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

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

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

49 
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

50 
shows "P m n" 
27556  51 
proof (induct m n rule: gcd.induct) 
52 
case (1 m n) with assms show ?case by (cases "n = 0") simp_all 

53 
qed 

21256  54 

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

55 
lemma gcd_0 [simp, algebra]: "gcd m 0 = m" 
21263  56 
by simp 
21256  57 

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

58 
lemma gcd_0_left [simp,algebra]: "gcd 0 m = m" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

60 

27556  61 
lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

63 

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

64 
lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = 1" 
21263  65 
by simp 
21256  66 

67 
declare gcd.simps [simp del] 

68 

69 
text {* 

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

73 

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

74 
lemma gcd_dvd1 [iff, algebra]: "gcd m n dvd m" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

75 
and gcd_dvd2 [iff, algebra]: "gcd m n dvd n" 
21256  76 
apply (induct m n rule: gcd_induct) 
21263  77 
apply (simp_all add: gcd_non_0) 
21256  78 
apply (blast dest: dvd_mod_imp_dvd) 
79 
done 

80 

81 
text {* 

82 
\medskip Maximality: for all @{term m}, @{term n}, @{term k} 

83 
naturals, if @{term k} divides @{term m} and @{term k} divides 

27556  84 
@{term n} then @{term k} divides @{term "gcd m n"}. 
21256  85 
*} 
86 

27556  87 
lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n" 
21263  88 
by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod) 
21256  89 

90 
text {* 

91 
\medskip Function gcd yields the Greatest Common Divisor. 

92 
*} 

93 

27556  94 
lemma is_gcd: "is_gcd m n (gcd m n) " 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

95 
by (simp add: is_gcd_def gcd_greatest) 
21256  96 

97 

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

98 
subsection {* Derived laws for GCD *} 
21256  99 

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

100 
lemma gcd_greatest_iff [iff, algebra]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

101 
by (blast intro!: gcd_greatest intro: dvd_trans) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

102 

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

103 
lemma gcd_zero[algebra]: "gcd m n = 0 \<longleftrightarrow> m = 0 \<and> n = 0" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

104 
by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff) 
21256  105 

27556  106 
lemma gcd_commute: "gcd m n = gcd n m" 
21256  107 
apply (rule is_gcd_unique) 
108 
apply (rule is_gcd) 

109 
apply (subst is_gcd_commute) 

110 
apply (simp add: is_gcd) 

111 
done 

112 

27556  113 
lemma gcd_assoc: "gcd (gcd k m) n = gcd k (gcd m n)" 
21256  114 
apply (rule is_gcd_unique) 
115 
apply (rule is_gcd) 

116 
apply (simp add: is_gcd_def) 

117 
apply (blast intro: dvd_trans) 

118 
done 

119 

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

120 
lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = 1" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

121 
by (simp add: gcd_commute) 
21256  122 

123 
text {* 

124 
\medskip Multiplication laws 

125 
*} 

126 

27556  127 
lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)" 
21256  128 
 {* \cite[page 27]{davenport92} *} 
129 
apply (induct m n rule: gcd_induct) 

130 
apply simp 

131 
apply (case_tac "k = 0") 

132 
apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) 

133 
done 

134 

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

135 
lemma gcd_mult [simp, algebra]: "gcd k (k * n) = k" 
21256  136 
apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric]) 
137 
done 

138 

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

139 
lemma gcd_self [simp, algebra]: "gcd k k = k" 
21256  140 
apply (rule gcd_mult [of k 1, simplified]) 
141 
done 

142 

27556  143 
lemma relprime_dvd_mult: "gcd k n = 1 ==> k dvd m * n ==> k dvd m" 
21256  144 
apply (insert gcd_mult_distrib2 [of m k n]) 
145 
apply simp 

146 
apply (erule_tac t = m in ssubst) 

147 
apply simp 

148 
done 

149 

27556  150 
lemma relprime_dvd_mult_iff: "gcd k n = 1 ==> (k dvd m * n) = (k dvd m)" 
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27568
diff
changeset

151 
by (auto intro: relprime_dvd_mult dvd_mult2) 
21256  152 

27556  153 
lemma gcd_mult_cancel: "gcd k n = 1 ==> gcd (k * m) n = gcd m n" 
21256  154 
apply (rule dvd_anti_sym) 
155 
apply (rule gcd_greatest) 

156 
apply (rule_tac n = k in relprime_dvd_mult) 

157 
apply (simp add: gcd_assoc) 

158 
apply (simp add: gcd_commute) 

159 
apply (simp_all add: mult_commute) 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27568
diff
changeset

160 
apply (blast intro: dvd_mult) 
21256  161 
done 
162 

163 

164 
text {* \medskip Addition laws *} 

165 

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

166 
lemma gcd_add1 [simp,algebra]: "gcd (m + n) n = gcd m n" 
21256  167 
apply (case_tac "n = 0") 
168 
apply (simp_all add: gcd_non_0) 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27568
diff
changeset

169 
apply (simp add: mod_add_self2) 
21256  170 
done 
171 

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

172 
lemma gcd_add2 [simp, algebra]: "gcd m (m + n) = gcd m n" 
21256  173 
proof  
27556  174 
have "gcd m (m + n) = gcd (m + n) m" by (rule gcd_commute) 
175 
also have "... = gcd (n + m) m" by (simp add: add_commute) 

176 
also have "... = gcd n m" by simp 

177 
also have "... = gcd m n" by (rule gcd_commute) 

21256  178 
finally show ?thesis . 
179 
qed 

180 

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

181 
lemma gcd_add2' [simp, algebra]: "gcd m (n + m) = gcd m n" 
21256  182 
apply (subst add_commute) 
183 
apply (rule gcd_add2) 

184 
done 

185 

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

186 
lemma gcd_add_mult[algebra]: "gcd m (k * m + n) = gcd m n" 
21263  187 
by (induct k) (simp_all add: add_assoc) 
21256  188 

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

189 
lemma gcd_dvd_prod: "gcd m n dvd m * n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

190 
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

191 

22367  192 
text {* 
193 
\medskip Division by gcd yields rrelatively primes. 

194 
*} 

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

195 

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

196 
lemma div_gcd_relprime: 
22367  197 
assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0" 
27556  198 
shows "gcd (a div gcd a b) (b div gcd a b) = 1" 
22367  199 
proof  
27556  200 
let ?g = "gcd a b" 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

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

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

204 
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

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

208 
unfolding dvd_def by blast 
22367  209 
then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all 
210 
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" 

211 
by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] 

212 
dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

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

213 
have "?g \<noteq> 0" using nz by (simp add: gcd_zero) 
22367  214 
then have gp: "?g > 0" by simp 
215 
from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . 

216 
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

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

218 

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

219 

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

220 
lemma gcd_unique: "d dvd a\<and>d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = 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

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

222 
assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd 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

223 
from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of 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

224 
have th: "gcd a b dvd 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

225 
from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]] show "d = gcd 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

226 
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

227 

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

228 
lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

229 
shows "gcd x y = gcd u v" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

230 
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

231 
from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd u v" 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

232 
with gcd_unique[of "gcd u v" x y] show ?thesis by auto 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

233 
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

234 

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

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

236 
assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

237 
and add: "\<forall>a b. P a b \<longrightarrow> P a (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

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

239 
proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

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

241 
assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

242 
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

243 
moreover {assume eq: "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

244 
from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq 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

245 
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

246 
{assume lt: "a < b" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

247 
hence "a + b  a < n \<or> a = 0" using H(2) by arith 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

248 
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

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

250 
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

251 
{assume ab: "a + b  a < n" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

252 
have th0: "a + b  a = a + (b  a)" using lt by arith 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

253 
from add[rule_format, OF H(1)[rule_format, OF ab th0]] 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

254 
have "P a b" by (simp add: th0[symmetric])} 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

255 
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

256 
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

257 
{assume lt: "a > b" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

258 
hence "b + a  b < n \<or> b = 0" using H(2) by arith 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

259 
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

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

261 
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

262 
{assume ab: "b + a  b < n" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

263 
have th0: "b + a  b = b + (a  b)" using lt by arith 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

264 
from add[rule_format, OF H(1)[rule_format, OF ab th0]] 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

265 
have "P b a" by (simp add: th0[symmetric]) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

266 
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

267 
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

268 
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

269 
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

270 

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

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

272 
assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x = b * y + d \<or> 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

273 
shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and> (a * x = (a + b) * y + d \<or> (a + 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

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

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

276 
apply (rule_tac x="d" in exI, simp add: dvd_add) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

277 
apply (case_tac "a * x = b * y + d" , simp_all) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

278 
apply (rule_tac x="x + y" in exI) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

279 
apply (rule_tac x="y" in exI) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

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

281 
apply (rule_tac x="x" in exI) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

282 
apply (rule_tac x="x + y" in exI) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

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

284 
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

285 

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

286 
lemma bezout_add: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x = b * y + d \<or> 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

287 
apply(induct a b rule: ind_euclid) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

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

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

290 
apply (rule_tac x="a" in exI, simp add: dvd_add) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

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

292 
apply (rule_tac x="d" in exI) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

293 
apply (case_tac "a * x = b * y + d", simp_all add: dvd_add) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

294 
apply (rule_tac x="x+y" in exI) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

295 
apply (rule_tac x="y" in exI) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

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

297 
apply (rule_tac x="x" in exI) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

298 
apply (rule_tac x="x+y" in exI) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

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

300 
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

301 

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

302 
lemma bezout: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x  b * y = d \<or> 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

303 
using bezout_add[of 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

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

305 
apply (rule_tac x="d" in exI, 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

306 
apply (rule_tac x="x" in exI) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

307 
apply (rule_tac x="y" in exI) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

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

309 
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

310 

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

311 

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

312 
text {* We can get a stronger version with a nonzeroness assumption. *} 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

313 
lemma divides_le: "m dvd n ==> m <= n \<or> n = (0::nat)" by (auto simp add: dvd_def) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

314 

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

315 
lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

316 
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

317 
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

318 
from nz have ap: "a > 0" by simp 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

319 
from bezout_add[of 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

320 
have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or> (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * 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

321 
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

322 
{fix d x y assume H: "d dvd a" "d dvd b" "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

323 
from H 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

324 
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

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

326 
{assume b0: "b = 0" with H have ?thesis 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

327 
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

328 
{assume b: "b \<noteq> 0" hence bp: "b > 0" by simp 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

329 
from divides_le[OF H(2)] b have "d < b \<or> d = b" using le_less 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

330 
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

331 
{assume db: "d=b" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

332 
from prems have ?thesis apply simp 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

333 
apply (rule exI[where x = b], simp) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

334 
apply (rule exI[where x = b]) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

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

336 
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

337 
{assume db: "d < b" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

338 
{assume "x=0" hence ?thesis using prems by simp } 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

339 
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

340 
{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

341 

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

342 
from db have "d \<le> b  1" by simp 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

343 
hence "d*b \<le> b*(b  1)" by simp 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

344 
with xp mult_mono[of "1" "x" "d*b" "b*(b  1)"] 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

345 
have dble: "d*b \<le> x*b*(b  1)" using bp 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

346 
from H (3) have "a * ((b  1) * y) + d * (b  1 + 1) = d + x*b*(b  1)" by algebra 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

347 
hence "a * ((b  1) * y) = d + x*b*(b  1)  d*b" using bp 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

348 
hence "a * ((b  1) * y) = d + (x*b*(b  1)  d*b)" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

349 
by (simp only: diff_add_assoc[OF dble, of d, symmetric]) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

350 
hence "a * ((b  1) * y) = b*(x*(b  1)  d) + d" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

351 
by (simp only: diff_mult_distrib2 add_commute mult_ac) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

352 
hence ?thesis using H(1,2) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

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

354 
apply (rule exI[where x=d], simp) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

355 
apply (rule exI[where x="(b  1) * y"]) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

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

357 
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

358 
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

359 
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

360 
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

361 
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

362 

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

363 

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

364 
lemma bezout_gcd: "\<exists>x y. a * x  b * y = gcd a b \<or> b * x  a * 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

365 
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

366 
let ?g = "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

367 
from bezout[of a b] obtain d x y where d: "d dvd a" "d dvd b" "a * x  b * y = d \<or> b * x  a * 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

368 
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

369 
then obtain k where k: "?g = d*k" unfolding dvd_def 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

370 
from d(3) have "(a * x  b * y)*k = d*k \<or> (b * x  a * y)*k = d*k" 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

371 
hence "a * x * k  b * y*k = d*k \<or> b * x * k  a * y*k = d*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

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

373 
hence "a * (x * k)  b * (y*k) = ?g \<or> b * (x * k)  a * (y*k) = ?g" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

374 
by (simp add: k mult_assoc) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

375 
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

376 
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

377 

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

378 
lemma bezout_gcd_strong: assumes a: "a \<noteq> 0" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

379 
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

380 
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

381 
let ?g = "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

382 
from bezout_add_strong[OF a, of 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

383 
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

384 
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

385 
then obtain k where k: "?g = d*k" unfolding dvd_def 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

386 
from d(3) have "a * x * k = (b * y + d) *k " by algebra 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

387 
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

388 
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

389 
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

390 

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

391 
lemma gcd_mult_distrib: "gcd(a * c) (b * c) = c * 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

392 
by(simp add: gcd_mult_distrib2 mult_commute) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

393 

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

394 
lemma gcd_bezout: "(\<exists>x y. a * x  b * y = d \<or> b * x  a * y = d) \<longleftrightarrow> gcd a b dvd 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

395 
(is "?lhs \<longleftrightarrow> ?rhs") 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

396 
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

397 
let ?g = "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

398 
{assume H: ?rhs then obtain k where k: "d = ?g*k" unfolding dvd_def 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

399 
from bezout_gcd[of a b] obtain x y where xy: "a * x  b * y = ?g \<or> b * x  a * y = ?g" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

400 
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

401 
hence "(a * x  b * y)*k = ?g*k \<or> (b * x  a * y)*k = ?g*k" by auto 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

402 
hence "a * x*k  b * y*k = ?g*k \<or> b * x * k  a * y*k = ?g*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

403 
by (simp only: diff_mult_distrib) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

404 
hence "a * (x*k)  b * (y*k) = d \<or> b * (x * k)  a * (y*k) = 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

405 
by (simp add: k[symmetric] mult_assoc) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

406 
hence ?lhs 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

407 
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

408 
{fix x y assume H: "a * x  b * y = d \<or> 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

409 
have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

410 
using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

411 
from dvd_diff[OF dv(1,2)] dvd_diff[OF dv(3,4)] H 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

412 
have ?rhs by auto} 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

413 
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

414 
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

415 

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

416 
lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd a b dvd 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

417 
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

418 
let ?g = "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

419 
have dv: "?g dvd a*x" "?g dvd b * y" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

420 
using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

421 
from dvd_add[OF dv] H 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

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

423 
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

424 

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

425 
lemma gcd_mult': "gcd b (a * b) = 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

426 
by (simp add: gcd_mult mult_commute[of 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

427 

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

428 
lemma gcd_add: "gcd(a + b) b = 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

429 
"gcd(b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = 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

430 
apply (simp_all add: gcd_add1) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

431 
by (simp add: gcd_commute gcd_add1) 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

432 

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

433 
lemma gcd_sub: "b <= a ==> gcd(a  b) b = gcd a b" "a <= b ==> gcd a (b  a) = 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

434 
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

435 
{fix a b assume H: "b \<le> (a::nat)" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

436 
hence th: "a  b + 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

437 
from gcd_add(1)[of "a  b" b] th have "gcd(a  b) b = gcd a b" 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

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

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

440 
assume ab: "b \<le> a" 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

441 
from th[OF ab] show "gcd (a  b) b = gcd 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

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

443 
assume ab: "a \<le> 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

444 
from th[OF ab] show "gcd a (b  a) = 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

445 
by (simp add: gcd_commute)} 
4b1642284dd7
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
chaieb
parents:
27651
diff
changeset

446 
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

447 

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

448 

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

449 
subsection {* LCM defined by GCD *} 
22367  450 

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

451 

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

452 
definition 
27556  453 
lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

454 
where 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

455 
lcm_def: "lcm m n = m * n div gcd m n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

456 

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

457 
lemma prod_gcd_lcm: 
27556  458 
"m * n = gcd m n * lcm m n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

459 
unfolding lcm_def by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod]) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

460 

27556  461 
lemma lcm_0 [simp]: "lcm m 0 = 0" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

463 

27556  464 
lemma lcm_1 [simp]: "lcm m 1 = m" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

466 

27556  467 
lemma lcm_0_left [simp]: "lcm 0 n = 0" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

469 

27556  470 
lemma lcm_1_left [simp]: "lcm 1 m = m" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

472 

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

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

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

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

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

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

478 

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

480 
assumes "m dvd k" and "n dvd k" 
27556  481 
shows "lcm m n dvd k" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

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

485 
case (Suc _) then have pos_k: "k > 0" by auto 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

486 
from assms dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto 
27556  487 
with gcd_zero [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

488 
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

489 
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

490 
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

491 
from pos_k k_n have pos_q: "q > 0" by auto 
27556  492 
have "k * k * gcd q p = k * gcd (k * q) (k * p)" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

495 
by (simp add: k_m [symmetric] k_n [symmetric]) 
27556  496 
also have "\<dots> = k * p * q * gcd m n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

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

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

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

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

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

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

510 

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

511 
lemma lcm_dvd1 [iff]: 
27556  512 
"m dvd lcm m n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

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

516 
case (Suc _) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

517 
then have mpos: "m > 0" by simp 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

518 
show ?thesis 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

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

522 
case (Suc _) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

523 
then have npos: "n > 0" by simp 
27556  524 
have "gcd m n dvd n" by simp 
525 
then obtain k where "n = gcd m n * k" using dvd_def by auto 

526 
then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: mult_ac) 

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

527 
also have "\<dots> = m * k" using mpos npos gcd_zero by simp 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

528 
finally show ?thesis by (simp add: lcm_def) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

531 

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

532 
lemma lcm_dvd2 [iff]: 
27556  533 
"n dvd lcm m n" 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

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

537 
case (Suc _) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

538 
then have npos: "n > 0" by simp 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

539 
show ?thesis 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

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

543 
case (Suc _) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

544 
then have mpos: "m > 0" by simp 
27556  545 
have "gcd m n dvd m" by simp 
546 
then obtain k where "m = gcd m n * k" using dvd_def by auto 

547 
then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: mult_ac) 

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

548 
also have "\<dots> = n * k" using mpos npos gcd_zero by simp 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

549 
finally show ?thesis by (simp add: lcm_def) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

552 

27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

553 
lemma gcd_add1_eq: "gcd (m + k) k = gcd (m + k) m" 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

554 
by (simp add: gcd_commute) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

555 

9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

556 
lemma gcd_diff2: "m \<le> n ==> gcd n (n  m) = gcd n m" 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

557 
apply (subgoal_tac "n = m + (n  m)") 
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

558 
apply (erule ssubst, rule gcd_add1_eq, simp) 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

559 
done 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

560 

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

561 

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

562 
subsection {* GCD and LCM on integers *} 
22367  563 

564 
definition 

27556  565 
zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where 
566 
"zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))" 

22367  567 

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

568 
lemma zgcd_zdvd1 [iff,simp, algebra]: "zgcd i j dvd i" 
27556  569 
by (simp add: zgcd_def int_dvd_iff) 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

570 

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

571 
lemma zgcd_zdvd2 [iff,simp, algebra]: "zgcd i j dvd j" 
27556  572 
by (simp add: zgcd_def int_dvd_iff) 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

573 

27556  574 
lemma zgcd_pos: "zgcd i j \<ge> 0" 
575 
by (simp add: zgcd_def) 

22367  576 

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

577 
lemma zgcd0 [simp,algebra]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)" 
27556  578 
by (simp add: zgcd_def gcd_zero) arith 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

579 

27556  580 
lemma zgcd_commute: "zgcd i j = zgcd j i" 
581 
unfolding zgcd_def by (simp add: gcd_commute) 

22367  582 

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

583 
lemma zgcd_zminus [simp, algebra]: "zgcd ( i) j = zgcd i j" 
27556  584 
unfolding zgcd_def by simp 
22367  585 

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

586 
lemma zgcd_zminus2 [simp, algebra]: "zgcd i ( j) = zgcd i j" 
27556  587 
unfolding zgcd_def by simp 
22367  588 

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

589 
(* should be solved by algebra*) 
27556  590 
lemma zrelprime_dvd_mult: "zgcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k" 
591 
unfolding zgcd_def 

22367  592 
proof  
27556  593 
assume "int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>)) = 1" "i dvd k * j" 
594 
then have g: "gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>) = 1" by simp 

22367  595 
from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

596 
have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>" 
22367  597 
unfolding dvd_def 
598 
by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric]) 

599 
from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'" 

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

600 
unfolding dvd_def by blast 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

601 
from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23365
diff
changeset

602 
then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult) 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

603 
then show ?thesis 
22367  604 
apply (subst zdvd_abs1 [symmetric]) 
605 
apply (subst zdvd_abs2 [symmetric]) 

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

606 
apply (unfold dvd_def) 
22367  607 
apply (rule_tac x = "int h'" in exI, simp) 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

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

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

610 

27556  611 
lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith 
22367  612 

27556  613 
lemma zgcd_greatest: 
22367  614 
assumes "k dvd m" and "k dvd n" 
27556  615 
shows "k dvd zgcd m n" 
22367  616 
proof  
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

617 
let ?k' = "nat \<bar>k\<bar>" 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

618 
let ?m' = "nat \<bar>m\<bar>" 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

619 
let ?n' = "nat \<bar>n\<bar>" 
22367  620 
from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'" 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

621 
unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2) 
27556  622 
from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n" 
623 
unfolding zgcd_def by (simp only: zdvd_int) 

624 
then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs) 

625 
then show "k dvd zgcd m n" by (simp add: zdvd_abs1) 

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

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

627 

27556  628 
lemma div_zgcd_relprime: 
22367  629 
assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0" 
27556  630 
shows "zgcd (a div (zgcd a b)) (b div (zgcd a b)) = 1" 
22367  631 
proof  
25112  632 
from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by arith 
27556  633 
let ?g = "zgcd a b" 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

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

635 
let ?b' = "b div ?g" 
27556  636 
let ?g' = "zgcd ?a' ?b'" 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

637 
have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

638 
have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2) 
22367  639 
from dvdg dvdg' obtain ka kb ka' kb' where 
640 
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

641 
unfolding dvd_def by blast 
22367  642 
then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all 
643 
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" 

644 
by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)] 

645 
zdvd_mult_div_cancel [OF dvdg(2)] dvd_def) 

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

646 
have "?g \<noteq> 0" using nz by simp 
27556  647 
then have gp: "?g \<noteq> 0" using zgcd_pos[where i="a" and j="b"] by arith 
648 
from zgcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . 

22367  649 
with zdvd_mult_cancel1 [OF gp] have "\<bar>?g'\<bar> = 1" by simp 
27556  650 
with zgcd_pos show "?g' = 1" by simp 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

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

652 

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

653 
lemma zgcd_0 [simp, algebra]: "zgcd m 0 = abs m" 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

654 
by (simp add: zgcd_def abs_if) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

655 

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

656 
lemma zgcd_0_left [simp, algebra]: "zgcd 0 m = abs m" 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

657 
by (simp add: zgcd_def abs_if) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

658 

9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

659 
lemma zgcd_non_0: "0 < n ==> zgcd m n = zgcd n (m mod n)" 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

660 
apply (frule_tac b = n and a = m in pos_mod_sign) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

661 
apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

662 
apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

663 
apply (frule_tac a = m in pos_mod_bound) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

664 
apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

665 
done 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

666 

9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

667 
lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)" 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

668 
apply (case_tac "n = 0", simp add: DIVISION_BY_ZERO) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

669 
apply (auto simp add: linorder_neq_iff zgcd_non_0) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

670 
apply (cut_tac m = "m" and n = "n" in zgcd_non_0, auto) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

671 
done 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

672 

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

673 
lemma zgcd_1 [simp, algebra]: "zgcd m 1 = 1" 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

674 
by (simp add: zgcd_def abs_if) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

675 

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

676 
lemma zgcd_0_1_iff [simp, algebra]: "zgcd 0 m = 1 \<longleftrightarrow> \<bar>m\<bar> = 1" 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

677 
by (simp add: zgcd_def abs_if) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

678 

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

679 
lemma zgcd_greatest_iff[algebra]: "k dvd zgcd m n = (k dvd m \<and> k dvd n)" 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

680 
by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

681 

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

682 
lemma zgcd_1_left [simp, algebra]: "zgcd 1 m = 1" 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

683 
by (simp add: zgcd_def gcd_1_left) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

684 

9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

685 
lemma zgcd_assoc: "zgcd (zgcd k m) n = zgcd k (zgcd m n)" 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

686 
by (simp add: zgcd_def gcd_assoc) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

687 

9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

688 
lemma zgcd_left_commute: "zgcd k (zgcd m n) = zgcd m (zgcd k n)" 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

689 
apply (rule zgcd_commute [THEN trans]) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

690 
apply (rule zgcd_assoc [THEN trans]) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

691 
apply (rule zgcd_commute [THEN arg_cong]) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

692 
done 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

693 

9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

694 
lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

695 
 {* addition is an ACoperator *} 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

696 

9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

697 
lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)" 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

698 
by (simp del: minus_mult_right [symmetric] 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

699 
add: minus_mult_right nat_mult_distrib zgcd_def abs_if 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

700 
mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric]) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

701 

9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

702 
lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n" 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

703 
by (simp add: abs_if zgcd_zmult_distrib2) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

704 

9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

705 
lemma zgcd_self [simp]: "0 \<le> m ==> zgcd m m = m" 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

706 
by (cut_tac k = m and m = 1 and n = 1 in zgcd_zmult_distrib2, simp_all) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

707 

9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

708 
lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd k (k * n) = k" 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

709 
by (cut_tac k = k and m = 1 and n = n in zgcd_zmult_distrib2, simp_all) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

710 

9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

711 
lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n) k = k" 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

712 
by (cut_tac k = k and m = n and n = 1 in zgcd_zmult_distrib2, simp_all) 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

713 

9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

714 

9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

715 
definition "zlcm i j = int (lcm(nat(abs i)) (nat(abs j)))" 
23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

716 

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

717 
lemma dvd_zlcm_self1[simp, algebra]: "i dvd zlcm i j" 
27556  718 
by(simp add:zlcm_def dvd_int_iff) 
23983  719 

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

720 
lemma dvd_zlcm_self2[simp, algebra]: "j dvd zlcm i j" 
27556  721 
by(simp add:zlcm_def dvd_int_iff) 
23983  722 

23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

723 

27556  724 
lemma dvd_imp_dvd_zlcm1: 
725 
assumes "k dvd i" shows "k dvd (zlcm i j)" 

23983  726 
proof  
727 
have "nat(abs k) dvd nat(abs i)" using `k dvd i` 

23994  728 
by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1) 
27556  729 
thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans) 
23983  730 
qed 
731 

27556  732 
lemma dvd_imp_dvd_zlcm2: 
733 
assumes "k dvd j" shows "k dvd (zlcm i j)" 

23983  734 
proof  
735 
have "nat(abs k) dvd nat(abs j)" using `k dvd j` 

23994  736 
by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1) 
27556  737 
thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans) 
23983  738 
qed 
739 

23994  740 

23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

741 
lemma zdvd_self_abs1: "(d::int) dvd (abs d)" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

742 
by (case_tac "d <0", simp_all) 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

743 

1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

744 
lemma zdvd_self_abs2: "(abs (d::int)) dvd d" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

745 
by (case_tac "d<0", simp_all) 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

746 

1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

747 
(* lcm a b is positive for positive a and b *) 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

748 

1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

749 
lemma lcm_pos: 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

750 
assumes mpos: "m > 0" 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

751 
and npos: "n>0" 
27556  752 
shows "lcm m n > 0" 
23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

753 
proof(rule ccontr, simp add: lcm_def gcd_zero) 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

754 
assume h:"m*n div gcd m n = 0" 
27556  755 
from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp 
756 
hence gcdp: "gcd m n > 0" by simp 

23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

757 
with h 
27556  758 
have "m*n < gcd m n" 
759 
by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"]) 

23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

760 
moreover 
27556  761 
have "gcd m n dvd m" by simp 
762 
with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp 

27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

763 
with npos have t1:"gcd m n *n \<le> m*n" by simp 
27556  764 
have "gcd m n \<le> gcd m n*n" using npos by simp 
765 
with t1 have "gcd m n \<le> m*n" by arith 

23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

766 
ultimately show "False" by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

767 
qed 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

768 

27556  769 
lemma zlcm_pos: 
23983  770 
assumes anz: "a \<noteq> 0" 
771 
and bnz: "b \<noteq> 0" 

27556  772 
shows "0 < zlcm a b" 
23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

773 
proof 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

774 
let ?na = "nat (abs a)" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

775 
let ?nb = "nat (abs b)" 
23983  776 
have nap: "?na >0" using anz by simp 
777 
have nbp: "?nb >0" using bnz by simp 

27556  778 
have "0 < lcm ?na ?nb" by (rule lcm_pos[OF nap nbp]) 
779 
thus ?thesis by (simp add: zlcm_def) 

23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

780 
qed 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

781 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27568
diff
changeset

782 
lemma zgcd_code [code func]: 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27568
diff
changeset

783 
"zgcd k l = \<bar>if l = 0 then k else zgcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>" 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27568
diff
changeset

784 
by (simp add: zgcd_def gcd.simps [of "nat \<bar>k\<bar>"] nat_mod_distrib) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27568
diff
changeset

785 

21256  786 
end 