author  haftmann 
Tue, 24 Jul 2007 15:20:49 +0200  
changeset 23951  b188cac107ad 
parent 23687  06884f7ffb18 
child 23983  79dc793bec43 
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 

10 
imports Main 

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 *} 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

21 
"is_gcd p m n \<longleftrightarrow> p dvd m \<and> p dvd n \<and> 
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 

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

26 
lemma is_gcd_unique: "is_gcd m a b \<Longrightarrow> is_gcd n a b \<Longrightarrow> m = n" 
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 

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

31 
lemma is_gcd_dvd: "is_gcd m a b \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m" 
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 

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

36 
lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m" 
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 

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

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

43 
gcd :: "nat \<times> nat => nat" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

45 
"gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))" 
21256  46 

47 
lemma gcd_induct: 

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

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

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

50 
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

51 
shows "P m n" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

52 
apply (rule gcd.induct [of "split P" "(m, n)", unfolded Product_Type.split]) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

53 
apply (case_tac "n = 0") 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

55 
using assms apply simp_all 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

56 
done 
21256  57 

58 
lemma gcd_0 [simp]: "gcd (m, 0) = m" 

21263  59 
by simp 
21256  60 

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

61 
lemma gcd_0_left [simp]: "gcd (0, m) = m" 
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 

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

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

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

66 

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

67 
lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1" 
21263  68 
by simp 
21256  69 

70 
declare gcd.simps [simp del] 

71 

72 
text {* 

73 
\medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}. The 

74 
conjunctions don't seem provable separately. 

75 
*} 

76 

77 
lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m" 

78 
and gcd_dvd2 [iff]: "gcd (m, n) dvd n" 

79 
apply (induct m n rule: gcd_induct) 

21263  80 
apply (simp_all add: gcd_non_0) 
21256  81 
apply (blast dest: dvd_mod_imp_dvd) 
82 
done 

83 

84 
text {* 

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

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

87 
@{term n} then @{term k} divides @{term "gcd (m, n)"}. 

88 
*} 

89 

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

90 
lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd (m, n)" 
21263  91 
by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod) 
21256  92 

93 
text {* 

94 
\medskip Function gcd yields the Greatest Common Divisor. 

95 
*} 

96 

97 
lemma is_gcd: "is_gcd (gcd (m, n)) m n" 

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

98 
by (simp add: is_gcd_def gcd_greatest) 
21256  99 

100 

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

101 
subsection {* Derived laws for GCD *} 
21256  102 

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

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

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

105 

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

106 
lemma gcd_zero: "gcd (m, n) = 0 \<longleftrightarrow> m = 0 \<and> n = 0" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

107 
by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff) 
21256  108 

109 
lemma gcd_commute: "gcd (m, n) = gcd (n, m)" 

110 
apply (rule is_gcd_unique) 

111 
apply (rule is_gcd) 

112 
apply (subst is_gcd_commute) 

113 
apply (simp add: is_gcd) 

114 
done 

115 

116 
lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" 

117 
apply (rule is_gcd_unique) 

118 
apply (rule is_gcd) 

119 
apply (simp add: is_gcd_def) 

120 
apply (blast intro: dvd_trans) 

121 
done 

122 

123 
lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1" 

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

124 
by (simp add: gcd_commute) 
21256  125 

126 
text {* 

127 
\medskip Multiplication laws 

128 
*} 

129 

130 
lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)" 

131 
 {* \cite[page 27]{davenport92} *} 

132 
apply (induct m n rule: gcd_induct) 

133 
apply simp 

134 
apply (case_tac "k = 0") 

135 
apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) 

136 
done 

137 

138 
lemma gcd_mult [simp]: "gcd (k, k * n) = k" 

139 
apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric]) 

140 
done 

141 

142 
lemma gcd_self [simp]: "gcd (k, k) = k" 

143 
apply (rule gcd_mult [of k 1, simplified]) 

144 
done 

145 

146 
lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m" 

147 
apply (insert gcd_mult_distrib2 [of m k n]) 

148 
apply simp 

149 
apply (erule_tac t = m in ssubst) 

150 
apply simp 

151 
done 

152 

153 
lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)" 

154 
apply (blast intro: relprime_dvd_mult dvd_trans) 

155 
done 

156 

157 
lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)" 

158 
apply (rule dvd_anti_sym) 

159 
apply (rule gcd_greatest) 

160 
apply (rule_tac n = k in relprime_dvd_mult) 

161 
apply (simp add: gcd_assoc) 

162 
apply (simp add: gcd_commute) 

163 
apply (simp_all add: mult_commute) 

164 
apply (blast intro: dvd_trans) 

165 
done 

166 

167 

168 
text {* \medskip Addition laws *} 

169 

170 
lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)" 

171 
apply (case_tac "n = 0") 

172 
apply (simp_all add: gcd_non_0) 

173 
done 

174 

175 
lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)" 

176 
proof  

22367  177 
have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute) 
21256  178 
also have "... = gcd (n + m, m)" by (simp add: add_commute) 
179 
also have "... = gcd (n, m)" by simp 

22367  180 
also have "... = gcd (m, n)" by (rule gcd_commute) 
21256  181 
finally show ?thesis . 
182 
qed 

183 

184 
lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)" 

185 
apply (subst add_commute) 

186 
apply (rule gcd_add2) 

187 
done 

188 

189 
lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)" 

21263  190 
by (induct k) (simp_all add: add_assoc) 
21256  191 

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

192 
lemma gcd_dvd_prod: "gcd (m, n) dvd m * n" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

193 
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

194 

22367  195 
text {* 
196 
\medskip Division by gcd yields rrelatively primes. 

197 
*} 

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

198 

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

199 
lemma div_gcd_relprime: 
22367  200 
assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0" 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

201 
shows "gcd (a div gcd(a,b), b div gcd(a,b)) = 1" 
22367  202 
proof  
203 
let ?g = "gcd (a, b)" 

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

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

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

206 
let ?g' = "gcd (?a', ?b')" 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

207 
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

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

211 
unfolding dvd_def by blast 
22367  212 
then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all 
213 
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" 

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

215 
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

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

219 
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

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

221 

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

222 
subsection {* LCM defined by GCD *} 
22367  223 

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

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

225 
lcm :: "nat \<times> nat \<Rightarrow> nat" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

227 
"lcm = (\<lambda>(m, n). m * n div gcd (m, n))" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

228 

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

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

230 
"lcm (m, n) = m * n div gcd (m, n)" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

232 

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

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

234 
"m * n = gcd (m, n) * lcm (m, n)" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

235 
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

236 

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

237 
lemma lcm_0 [simp]: "lcm (m, 0) = 0" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

239 

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

240 
lemma lcm_1 [simp]: "lcm (m, 1) = m" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

242 

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

243 
lemma lcm_0_left [simp]: "lcm (0, n) = 0" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

245 

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

246 
lemma lcm_1_left [simp]: "lcm (1, m) = m" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

248 

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

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

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

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

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

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

254 

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

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

257 
shows "lcm (m, n) dvd k" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

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

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

262 
from assms dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

263 
with gcd_zero [of m n] have pos_gcd: "gcd (m, n) > 0" by simp 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

264 
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

265 
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

266 
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

267 
from pos_k k_n have pos_q: "q > 0" by auto 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

268 
have "k * k * gcd (q, p) = k * gcd (k * q, k * p)" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

269 
by (simp add: mult_ac gcd_mult_distrib2) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

270 
also have "\<dots> = k * gcd (m * p * q, n * q * p)" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

271 
by (simp add: k_m [symmetric] k_n [symmetric]) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

272 
also have "\<dots> = k * p * q * gcd (m, n)" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

273 
by (simp add: mult_ac gcd_mult_distrib2) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

274 
finally have "(m * p) * (n * q) * gcd (q, p) = k * p * q * gcd (m, n)" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

275 
by (simp only: k_m [symmetric] k_n [symmetric]) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

276 
then have "p * q * m * n * gcd (q, p) = p * q * k * gcd (m, n)" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

278 
with pos_p pos_q have "m * n * gcd (q, p) = k * gcd (m, n)" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

280 
with prod_gcd_lcm [of m n] 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

281 
have "lcm (m, n) * gcd (q, p) * gcd (m, n) = k * gcd (m, n)" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

283 
with pos_gcd have "lcm (m, n) * gcd (q, p) = k" by simp 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

286 

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

287 
lemma lcm_dvd1 [iff]: 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

288 
"m dvd lcm (m, n)" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

300 
have "gcd (m, n) dvd n" by simp 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

301 
then obtain k where "n = gcd (m, n) * k" using dvd_def by auto 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

302 
then have "m * n div gcd (m, n) = m * (gcd (m, n) * k) div gcd (m, n)" by (simp add: mult_ac) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

303 
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

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

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

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

307 

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

308 
lemma lcm_dvd2 [iff]: 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

309 
"n dvd lcm (m, n)" 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

321 
have "gcd (m, n) dvd m" by simp 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

322 
then obtain k where "m = gcd (m, n) * k" using dvd_def by auto 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

323 
then have "m * n div gcd (m, n) = (gcd (m, n) * k) * n div gcd (m, n)" by (simp add: mult_ac) 
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

324 
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

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

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

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

328 

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

329 

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

330 
subsection {* GCD and LCM on integers *} 
22367  331 

332 
definition 

333 
igcd :: "int \<Rightarrow> int \<Rightarrow> int" where 

334 
"igcd i j = int (gcd (nat (abs i), nat (abs j)))" 

335 

336 
lemma igcd_dvd1 [simp]: "igcd i j dvd i" 

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

337 
by (simp add: igcd_def int_dvd_iff) 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

338 

22367  339 
lemma igcd_dvd2 [simp]: "igcd i j dvd j" 
340 
by (simp add: igcd_def int_dvd_iff) 

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

341 

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

342 
lemma igcd_pos: "igcd i j \<ge> 0" 
22367  343 
by (simp add: igcd_def) 
344 

345 
lemma igcd0 [simp]: "(igcd i j = 0) = (i = 0 \<and> j = 0)" 

346 
by (simp add: igcd_def gcd_zero) arith 

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

347 

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

348 
lemma igcd_commute: "igcd i j = igcd j i" 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

349 
unfolding igcd_def by (simp add: gcd_commute) 
22367  350 

351 
lemma igcd_neg1 [simp]: "igcd ( i) j = igcd i j" 

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

352 
unfolding igcd_def by simp 
22367  353 

354 
lemma igcd_neg2 [simp]: "igcd i ( j) = igcd i j" 

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

355 
unfolding igcd_def by simp 
22367  356 

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

357 
lemma zrelprime_dvd_mult: "igcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k" 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

358 
unfolding igcd_def 
22367  359 
proof  
360 
assume "int (gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>)) = 1" "i dvd k * j" 

361 
then have g: "gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>) = 1" by simp 

362 
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

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

366 
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

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

368 
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

369 
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

370 
then show ?thesis 
22367  371 
apply (subst zdvd_abs1 [symmetric]) 
372 
apply (subst zdvd_abs2 [symmetric]) 

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

373 
apply (unfold dvd_def) 
22367  374 
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

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

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

377 

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

378 
lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith 
22367  379 

380 
lemma igcd_greatest: 

381 
assumes "k dvd m" and "k dvd n" 

382 
shows "k dvd igcd m n" 

383 
proof  

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

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

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

386 
let ?n' = "nat \<bar>n\<bar>" 
22367  387 
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

388 
unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2) 
22367  389 
from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd igcd m n" 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

390 
unfolding igcd_def by (simp only: zdvd_int) 
22367  391 
then have "\<bar>k\<bar> dvd igcd m n" by (simp only: int_nat_abs) 
392 
then show "k dvd igcd m n" by (simp add: zdvd_abs1) 

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

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

394 

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

395 
lemma div_igcd_relprime: 
22367  396 
assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0" 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

397 
shows "igcd (a div (igcd a b)) (b div (igcd a b)) = 1" 
22367  398 
proof  
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

399 
from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by simp 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

400 
let ?g = "igcd a b" 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

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

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

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

404 
have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2) 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

405 
have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: igcd_dvd1 igcd_dvd2) 
22367  406 
from dvdg dvdg' obtain ka kb ka' kb' where 
407 
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

408 
unfolding dvd_def by blast 
22367  409 
then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all 
410 
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" 

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

412 
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

413 
have "?g \<noteq> 0" using nz by simp 
22367  414 
then have gp: "?g \<noteq> 0" using igcd_pos[where i="a" and j="b"] by arith 
415 
from igcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . 

416 
with zdvd_mult_cancel1 [OF gp] have "\<bar>?g'\<bar> = 1" by simp 

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

417 
with igcd_pos show "?g' = 1" by simp 
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

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

419 

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

420 
definition "ilcm = (\<lambda>i j. int (lcm(nat(abs i),nat(abs j))))" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

421 

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

422 
(* ilcm_dvd12 are needed later *) 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

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

424 
assumes anz: "a \<noteq> 0" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

425 
and bnz: "b \<noteq> 0" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

426 
shows "a dvd (ilcm a b)" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

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

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

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

430 
have nap: "?na >0" using anz by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

431 
have nbp: "?nb >0" using bnz by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

432 
from nap nbp have "?na dvd lcm(?na,?nb)" using lcm_dvd1 by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

433 
thus ?thesis by (simp add: ilcm_def dvd_int_iff) 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

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

435 

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

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

437 
assumes anz: "a \<noteq> 0" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

438 
and bnz: "b \<noteq> 0" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

439 
shows "b dvd (ilcm a b)" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

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

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

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

443 
have nap: "?na >0" using anz by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

444 
have nbp: "?nb >0" using bnz by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

445 
from nap nbp have "?nb dvd lcm(?na,?nb)" using lcm_dvd2 by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

446 
thus ?thesis by (simp add: ilcm_def dvd_int_iff) 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

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

448 

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

449 
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

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

451 

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

452 
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

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

454 

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

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

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

457 

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

458 
(* 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

459 

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

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

461 
assumes mpos: "m > 0" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

462 
and npos: "n>0" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

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

464 
proof(rule ccontr, simp add: lcm_def gcd_zero) 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

465 
assume h:"m*n div gcd(m,n) = 0" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

466 
from mpos npos have "gcd (m,n) \<noteq> 0" using gcd_zero by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

467 
hence gcdp: "gcd(m,n) > 0" by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

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

469 
have "m*n < gcd(m,n)" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

470 
by (cases "m * n < gcd (m, n)") (auto simp add: div_if[OF gcdp, where m="m*n"]) 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

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

472 
have "gcd(m,n) dvd m" by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

473 
with mpos dvd_imp_le have t1:"gcd(m,n) \<le> m" by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

474 
with npos have t1:"gcd(m,n)*n \<le> m*n" by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

475 
have "gcd(m,n) \<le> gcd(m,n)*n" using npos by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

476 
with t1 have "gcd(m,n) \<le> m*n" by arith 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

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

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

479 

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

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

481 
assumes apos: " 0 < a" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

482 
and bpos: "0 < b" 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

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

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

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

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

487 
have nap: "?na >0" using apos by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

488 
have nbp: "?nb >0" using bpos by simp 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

489 
have "0 < lcm (?na,?nb)" by (rule lcm_pos[OF nap nbp]) 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

490 
thus ?thesis by (simp add: ilcm_def) 
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

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

492 

21256  493 
end 