author  wenzelm 
Mon, 08 Feb 2010 21:28:27 +0100  
changeset 35054  a5db9779b026 
parent 34947  e1b8f2736404 
child 35416  d8d7d1b785af 
permissions  rwrr 
31719  1 
(* Title: UniqueFactorization.thy 
2 
Author: Jeremy Avigad 

3 

4 

5 
Unique factorization for the natural numbers and the integers. 

6 

7 
Note: there were previous Isabelle formalizations of unique 

8 
factorization due to Thomas Marthedal Rasmussen, and, building on 

9 
that, by Jeremy Avigad and David Gray. 

10 
*) 

11 

12 
header {* UniqueFactorization *} 

13 

14 
theory UniqueFactorization 

15 
imports Cong Multiset 

16 
begin 

17 

18 
(* inherited from Multiset *) 

19 
declare One_nat_def [simp del] 

20 

21 
(* As a simp or intro rule, 

22 

23 
prime p \<Longrightarrow> p > 0 

24 

25 
wreaks havoc here. When the premise includes ALL x :# M. prime x, it 

26 
leads to the backchaining 

27 

28 
x > 0 

29 
prime x 

30 
x :# M which is, unfortunately, 

31 
count M x > 0 

32 
*) 

33 

34 

35 
(* useful facts *) 

36 

37 
lemma setsum_Un2: "finite (A Un B) \<Longrightarrow> 

38 
setsum f (A Un B) = setsum f (A  B) + setsum f (B  A) + 

39 
setsum f (A Int B)" 

40 
apply (subgoal_tac "A Un B = (A  B) Un (B  A) Un (A Int B)") 

41 
apply (erule ssubst) 

42 
apply (subst setsum_Un_disjoint) 

43 
apply auto 

44 
apply (subst setsum_Un_disjoint) 

45 
apply auto 

46 
done 

47 

48 
lemma setprod_Un2: "finite (A Un B) \<Longrightarrow> 

49 
setprod f (A Un B) = setprod f (A  B) * setprod f (B  A) * 

50 
setprod f (A Int B)" 

51 
apply (subgoal_tac "A Un B = (A  B) Un (B  A) Un (A Int B)") 

52 
apply (erule ssubst) 

53 
apply (subst setprod_Un_disjoint) 

54 
apply auto 

55 
apply (subst setprod_Un_disjoint) 

56 
apply auto 

57 
done 

58 

59 
(* Should this go in Multiset.thy? *) 

60 
(* TN: No longer an introrule; needed only once and might get in the way *) 

61 
lemma multiset_eqI: "[ !!x. count M x = count N x ] ==> M = N" 

62 
by (subst multiset_eq_conv_count_eq, blast) 

63 

64 
(* Here is a version of set product for multisets. Is it worth moving 

65 
to multiset.thy? If so, one should similarly define msetsum for abelian 

66 
semirings, using of_nat. Also, is it worth developing bounded quantifiers 

67 
"ALL i :# M. P i"? 

68 
*) 

69 

70 
constdefs 

71 
msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b" 

72 
"msetprod f M == setprod (%x. (f x)^(count M x)) (set_of M)" 

73 

74 
syntax 

75 
"_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" 

76 
("(3PROD _:#_. _)" [0, 51, 10] 10) 

77 

78 
translations 

35054  79 
"PROD i :# A. b" == "CONST msetprod (%i. b) A" 
31719  80 

81 
lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 

82 
apply (simp add: msetprod_def power_add) 

83 
apply (subst setprod_Un2) 

84 
apply auto 

85 
apply (subgoal_tac 

86 
"(PROD x:set_of A  set_of B. f x ^ count A x * f x ^ count B x) = 

87 
(PROD x:set_of A  set_of B. f x ^ count A x)") 

88 
apply (erule ssubst) 

89 
apply (subgoal_tac 

90 
"(PROD x:set_of B  set_of A. f x ^ count A x * f x ^ count B x) = 

91 
(PROD x:set_of B  set_of A. f x ^ count B x)") 

92 
apply (erule ssubst) 

93 
apply (subgoal_tac "(PROD x:set_of A. f x ^ count A x) = 

94 
(PROD x:set_of A  set_of B. f x ^ count A x) * 

95 
(PROD x:set_of A Int set_of B. f x ^ count A x)") 

96 
apply (erule ssubst) 

97 
apply (subgoal_tac "(PROD x:set_of B. f x ^ count B x) = 

98 
(PROD x:set_of B  set_of A. f x ^ count B x) * 

99 
(PROD x:set_of A Int set_of B. f x ^ count B x)") 

100 
apply (erule ssubst) 

101 
apply (subst setprod_timesf) 

102 
apply (force simp add: mult_ac) 

103 
apply (subst setprod_Un_disjoint [symmetric]) 

104 
apply (auto intro: setprod_cong) 

105 
apply (subst setprod_Un_disjoint [symmetric]) 

106 
apply (auto intro: setprod_cong) 

107 
done 

108 

109 

110 
subsection {* unique factorization: multiset version *} 

111 

112 
lemma multiset_prime_factorization_exists [rule_format]: "n > 0 > 

113 
(EX M. (ALL (p::nat) : set_of M. prime p) & n = (PROD i :# M. i))" 

114 
proof (rule nat_less_induct, clarify) 

115 
fix n :: nat 

116 
assume ih: "ALL m < n. 0 < m > (EX M. (ALL p : set_of M. prime p) & m = 

117 
(PROD i :# M. i))" 

118 
assume "(n::nat) > 0" 

119 
then have "n = 1  (n > 1 & prime n)  (n > 1 & ~ prime n)" 

120 
by arith 

121 
moreover 

122 
{ 

123 
assume "n = 1" 

124 
then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)" 

125 
by (auto simp add: msetprod_def) 

126 
} 

127 
moreover 

128 
{ 

129 
assume "n > 1" and "prime n" 

130 
then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)" 

131 
by (auto simp add: msetprod_def) 

132 
} 

133 
moreover 

134 
{ 

135 
assume "n > 1" and "~ prime n" 

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

136 
from prems not_prime_eq_prod_nat 
31719  137 
obtain m k where "n = m * k & 1 < m & m < n & 1 < k & k < n" 
138 
by blast 

139 
with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)" 

140 
and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)" 

141 
by blast 

142 
hence "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)" 

143 
by (auto simp add: prems msetprod_Un set_of_union) 

144 
then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)".. 

145 
} 

146 
ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)" 

147 
by blast 

148 
qed 

149 

150 
lemma multiset_prime_factorization_unique_aux: 

151 
fixes a :: nat 

152 
assumes "(ALL p : set_of M. prime p)" and 

153 
"(ALL p : set_of N. prime p)" and 

154 
"(PROD i :# M. i) dvd (PROD i:# N. i)" 

155 
shows 

156 
"count M a <= count N a" 

157 
proof cases 

158 
assume "a : set_of M" 

159 
with prems have a: "prime a" 

160 
by auto 

161 
with prems have "a ^ count M a dvd (PROD i :# M. i)" 

162 
by (auto intro: dvd_setprod simp add: msetprod_def) 

163 
also have "... dvd (PROD i :# N. i)" 

164 
by (rule prems) 

165 
also have "... = (PROD i : (set_of N). i ^ (count N i))" 

166 
by (simp add: msetprod_def) 

167 
also have "... = 

168 
a^(count N a) * (PROD i : (set_of N  {a}). i ^ (count N i))" 

169 
proof (cases) 

170 
assume "a : set_of N" 

171 
hence b: "set_of N = {a} Un (set_of N  {a})" 

172 
by auto 

173 
thus ?thesis 

174 
by (subst (1) b, subst setprod_Un_disjoint, auto) 

175 
next 

176 
assume "a ~: set_of N" 

177 
thus ?thesis 

178 
by auto 

179 
qed 

180 
finally have "a ^ count M a dvd 

181 
a^(count N a) * (PROD i : (set_of N  {a}). i ^ (count N i))". 

182 
moreover have "coprime (a ^ count M a) 

183 
(PROD i : (set_of N  {a}). i ^ (count N i))" 

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

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

185 
apply (rule setprod_coprime_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

186 
apply (rule primes_imp_powers_coprime_nat) 
31719  187 
apply (insert prems, auto) 
188 
done 

189 
ultimately have "a ^ count M a dvd a^(count N a)" 

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

190 
by (elim coprime_dvd_mult_nat) 
31719  191 
with a show ?thesis 
192 
by (intro power_dvd_imp_le, auto) 

193 
next 

194 
assume "a ~: set_of M" 

195 
thus ?thesis by auto 

196 
qed 

197 

198 
lemma multiset_prime_factorization_unique: 

199 
assumes "(ALL (p::nat) : set_of M. prime p)" and 

200 
"(ALL p : set_of N. prime p)" and 

201 
"(PROD i :# M. i) = (PROD i:# N. i)" 

202 
shows 

203 
"M = N" 

204 
proof  

205 
{ 

206 
fix a 

207 
from prems have "count M a <= count N a" 

208 
by (intro multiset_prime_factorization_unique_aux, auto) 

209 
moreover from prems have "count N a <= count M a" 

210 
by (intro multiset_prime_factorization_unique_aux, auto) 

211 
ultimately have "count M a = count N a" 

212 
by auto 

213 
} 

214 
thus ?thesis by (simp add:multiset_eq_conv_count_eq) 

215 
qed 

216 

217 
constdefs 

218 
multiset_prime_factorization :: "nat => nat multiset" 

219 
"multiset_prime_factorization n == 

220 
if n > 0 then (THE M. ((ALL p : set_of M. prime p) & 

221 
n = (PROD i :# M. i))) 

222 
else {#}" 

223 

224 
lemma multiset_prime_factorization: "n > 0 ==> 

225 
(ALL p : set_of (multiset_prime_factorization n). prime p) & 

226 
n = (PROD i :# (multiset_prime_factorization n). i)" 

227 
apply (unfold multiset_prime_factorization_def) 

228 
apply clarsimp 

229 
apply (frule multiset_prime_factorization_exists) 

230 
apply clarify 

231 
apply (rule theI) 

232 
apply (insert multiset_prime_factorization_unique, blast)+ 

233 
done 

234 

235 

236 
subsection {* Prime factors and multiplicity for nats and ints *} 

237 

238 
class unique_factorization = 

239 

240 
fixes 

241 
multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" and 

242 
prime_factors :: "'a \<Rightarrow> 'a set" 

243 

244 
(* definitions for the natural numbers *) 

245 

246 
instantiation nat :: unique_factorization 

247 

248 
begin 

249 

250 
definition 

251 
multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

252 
where 

253 
"multiplicity_nat p n = count (multiset_prime_factorization n) p" 

254 

255 
definition 

256 
prime_factors_nat :: "nat \<Rightarrow> nat set" 

257 
where 

258 
"prime_factors_nat n = set_of (multiset_prime_factorization n)" 

259 

260 
instance proof qed 

261 

262 
end 

263 

264 
(* definitions for the integers *) 

265 

266 
instantiation int :: unique_factorization 

267 

268 
begin 

269 

270 
definition 

271 
multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat" 

272 
where 

273 
"multiplicity_int p n = multiplicity (nat p) (nat n)" 

274 

275 
definition 

276 
prime_factors_int :: "int \<Rightarrow> int set" 

277 
where 

278 
"prime_factors_int n = int ` (prime_factors (nat n))" 

279 

280 
instance proof qed 

281 

282 
end 

283 

284 

285 
subsection {* Set up transfer *} 

286 

287 
lemma transfer_nat_int_prime_factors: 

288 
"prime_factors (nat n) = nat ` prime_factors n" 

289 
unfolding prime_factors_int_def apply auto 

290 
by (subst transfer_int_nat_set_return_embed, assumption) 

291 

292 
lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow> 

293 
nat_set (prime_factors n)" 

294 
by (auto simp add: nat_set_def prime_factors_int_def) 

295 

296 
lemma transfer_nat_int_multiplicity: "p >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow> 

297 
multiplicity (nat p) (nat n) = multiplicity p n" 

298 
by (auto simp add: multiplicity_int_def) 

299 

300 
declare TransferMorphism_nat_int[transfer add return: 

301 
transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure 

302 
transfer_nat_int_multiplicity] 

303 

304 

305 
lemma transfer_int_nat_prime_factors: 

306 
"prime_factors (int n) = int ` prime_factors n" 

307 
unfolding prime_factors_int_def by auto 

308 

309 
lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> 

310 
nat_set (prime_factors n)" 

311 
by (simp only: transfer_nat_int_prime_factors_closure is_nat_def) 

312 

313 
lemma transfer_int_nat_multiplicity: 

314 
"multiplicity (int p) (int n) = multiplicity p n" 

315 
by (auto simp add: multiplicity_int_def) 

316 

317 
declare TransferMorphism_int_nat[transfer add return: 

318 
transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure 

319 
transfer_int_nat_multiplicity] 

320 

321 

322 
subsection {* Properties of prime factors and multiplicity for nats and ints *} 

323 

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

324 
lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0" 
31719  325 
by (unfold prime_factors_int_def, auto) 
326 

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

327 
lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p" 
31719  328 
apply (case_tac "n = 0") 
329 
apply (simp add: prime_factors_nat_def multiset_prime_factorization_def) 

330 
apply (auto simp add: prime_factors_nat_def multiset_prime_factorization) 

331 
done 

332 

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

333 
lemma prime_factors_prime_int [intro]: 
31719  334 
assumes "n >= 0" and "p : prime_factors (n::int)" 
335 
shows "prime p" 

336 

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

337 
apply (rule prime_factors_prime_nat [transferred, of n p]) 
31719  338 
using prems apply auto 
339 
done 

340 

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

341 
lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

342 
by (frule prime_factors_prime_nat, auto) 
31719  343 

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

344 
lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow> 
31719  345 
p > (0::int)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

346 
by (frule (1) prime_factors_prime_int, auto) 
31719  347 

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

348 
lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))" 
31719  349 
by (unfold prime_factors_nat_def, auto) 
350 

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

351 
lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))" 
31719  352 
by (unfold prime_factors_int_def, auto) 
353 

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

354 
lemma prime_factors_altdef_nat: "prime_factors (n::nat) = 
31719  355 
{p. multiplicity p n > 0}" 
356 
by (force simp add: prime_factors_nat_def multiplicity_nat_def) 

357 

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

358 
lemma prime_factors_altdef_int: "prime_factors (n::int) = 
31719  359 
{p. p >= 0 & multiplicity p n > 0}" 
360 
apply (unfold prime_factors_int_def multiplicity_int_def) 

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

361 
apply (subst prime_factors_altdef_nat) 
31719  362 
apply (auto simp add: image_def) 
363 
done 

364 

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

365 
lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow> 
31719  366 
n = (PROD p : prime_factors n. p^(multiplicity p n))" 
367 
by (frule multiset_prime_factorization, 

368 
simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def) 

369 

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

370 
thm prime_factorization_nat [transferred] 
31719  371 

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

372 
lemma prime_factorization_int: 
31719  373 
assumes "(n::int) > 0" 
374 
shows "n = (PROD p : prime_factors n. p^(multiplicity p n))" 

375 

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

376 
apply (rule prime_factorization_nat [transferred, of n]) 
31719  377 
using prems apply auto 
378 
done 

379 

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

380 
lemma neq_zero_eq_gt_zero_nat: "((x::nat) ~= 0) = (x > 0)" 
31719  381 
by auto 
382 

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

383 
lemma prime_factorization_unique_nat: 
31719  384 
"S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow> 
385 
n = (PROD p : S. p^(f p)) \<Longrightarrow> 

386 
S = prime_factors n & (ALL p. f p = multiplicity p n)" 

387 
apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset 

388 
f") 

389 
apply (unfold prime_factors_nat_def multiplicity_nat_def) 

34947  390 
apply (simp add: set_of_def Abs_multiset_inverse multiset_def) 
31719  391 
apply (unfold multiset_prime_factorization_def) 
392 
apply (subgoal_tac "n > 0") 

393 
prefer 2 

394 
apply force 

395 
apply (subst if_P, assumption) 

396 
apply (rule the1_equality) 

397 
apply (rule ex_ex1I) 

398 
apply (rule multiset_prime_factorization_exists, assumption) 

399 
apply (rule multiset_prime_factorization_unique) 

400 
apply force 

401 
apply force 

402 
apply force 

34947  403 
unfolding set_of_def msetprod_def 
31719  404 
apply (subgoal_tac "f : multiset") 
405 
apply (auto simp only: Abs_multiset_inverse) 

406 
unfolding multiset_def apply force 

407 
done 

408 

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

409 
lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
31719  410 
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow> 
411 
prime_factors n = S" 

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

412 
by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric], 
31719  413 
assumption+) 
414 

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

415 
lemma prime_factors_characterization'_nat: 
31719  416 
"finite {p. 0 < f (p::nat)} \<Longrightarrow> 
417 
(ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> 

418 
prime_factors (PROD p  0 < f p . p ^ f p) = {p. 0 < f p}" 

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

419 
apply (rule prime_factors_characterization_nat) 
31719  420 
apply auto 
421 
done 

422 

423 
(* A minor glitch:*) 

424 

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

425 
thm prime_factors_characterization'_nat 
31719  426 
[where f = "%x. f (int (x::nat))", 
427 
transferred direction: nat "op <= (0::int)", rule_format] 

428 

429 
(* 

430 
Transfer isn't smart enough to know that the "0 < f p" should 

431 
remain a comparison between nats. But the transfer still works. 

432 
*) 

433 

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

434 
lemma primes_characterization'_int [rule_format]: 
31719  435 
"finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow> 
436 
(ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> 

437 
prime_factors (PROD p  p >=0 & 0 < f p . p ^ f p) = 

438 
{p. p >= 0 & 0 < f p}" 

439 

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

440 
apply (insert prime_factors_characterization'_nat 
31719  441 
[where f = "%x. f (int (x::nat))", 
442 
transferred direction: nat "op <= (0::int)"]) 

443 
apply auto 

444 
done 

445 

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

446 
lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
31719  447 
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow> 
448 
prime_factors n = S" 

449 
apply simp 

450 
apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}") 

451 
apply (simp only:) 

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

452 
apply (subst primes_characterization'_int) 
31719  453 
apply auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

454 
apply (auto simp add: prime_ge_0_int) 
31719  455 
done 
456 

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

457 
lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
31719  458 
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow> 
459 
multiplicity p n = f p" 

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

460 
by (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, 
31719  461 
symmetric], auto) 
462 

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

463 
lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow> 
31719  464 
(ALL p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> 
465 
multiplicity p (PROD p  0 < f p . p ^ f p) = f p" 

466 
apply (rule impI)+ 

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

467 
apply (rule multiplicity_characterization_nat) 
31719  468 
apply auto 
469 
done 

470 

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

471 
lemma multiplicity_characterization'_int [rule_format]: 
31719  472 
"finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow> 
473 
(ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p >= 0 \<Longrightarrow> 

474 
multiplicity p (PROD p  p >= 0 & 0 < f p . p ^ f p) = f p" 

475 

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

476 
apply (insert multiplicity_characterization'_nat 
31719  477 
[where f = "%x. f (int (x::nat))", 
478 
transferred direction: nat "op <= (0::int)", rule_format]) 

479 
apply auto 

480 
done 

481 

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

482 
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
31719  483 
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow> 
484 
p >= 0 \<Longrightarrow> multiplicity p n = f p" 

485 
apply simp 

486 
apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}") 

487 
apply (simp only:) 

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

488 
apply (subst multiplicity_characterization'_int) 
31719  489 
apply auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

490 
apply (auto simp add: prime_ge_0_int) 
31719  491 
done 
492 

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

493 
lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0" 
31719  494 
by (simp add: multiplicity_nat_def multiset_prime_factorization_def) 
495 

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

496 
lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0" 
31719  497 
by (simp add: multiplicity_int_def) 
498 

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

499 
lemma multiplicity_one_nat [simp]: "multiplicity p (1::nat) = 0" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

500 
by (subst multiplicity_characterization_nat [where f = "%x. 0"], auto) 
31719  501 

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

502 
lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0" 
31719  503 
by (simp add: multiplicity_int_def) 
504 

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

505 
lemma multiplicity_prime_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

506 
apply (subst multiplicity_characterization_nat 
31719  507 
[where f = "(%q. if q = p then 1 else 0)"]) 
508 
apply auto 

509 
apply (case_tac "x = p") 

510 
apply auto 

511 
done 

512 

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

513 
lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1" 
31719  514 
unfolding prime_int_def multiplicity_int_def by auto 
515 

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

516 
lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow> 
31719  517 
multiplicity p (p^n) = n" 
518 
apply (case_tac "n = 0") 

519 
apply auto 

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

520 
apply (subst multiplicity_characterization_nat 
31719  521 
[where f = "(%q. if q = p then n else 0)"]) 
522 
apply auto 

523 
apply (case_tac "x = p") 

524 
apply auto 

525 
done 

526 

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

527 
lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow> 
31719  528 
multiplicity p (p^n) = n" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

529 
apply (frule prime_ge_0_int) 
31719  530 
apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq) 
531 
done 

532 

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

533 
lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> 
31719  534 
multiplicity p n = 0" 
535 
apply (case_tac "n = 0") 

536 
apply auto 

537 
apply (frule multiset_prime_factorization) 

538 
apply (auto simp add: set_of_def multiplicity_nat_def) 

539 
done 

540 

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

541 
lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0" 
31719  542 
by (unfold multiplicity_int_def prime_int_def, auto) 
543 

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

544 
lemma multiplicity_not_factor_nat [simp]: 
31719  545 
"p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

546 
by (subst (asm) prime_factors_altdef_nat, auto) 
31719  547 

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

548 
lemma multiplicity_not_factor_int [simp]: 
31719  549 
"p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

550 
by (subst (asm) prime_factors_altdef_int, auto) 
31719  551 

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

552 
lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> 
31719  553 
(prime_factors k) Un (prime_factors l) = prime_factors (k * l) & 
554 
(ALL p. multiplicity p k + multiplicity p l = multiplicity p (k * l))" 

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

555 
apply (rule prime_factorization_unique_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

556 
apply (simp only: prime_factors_altdef_nat) 
31719  557 
apply auto 
558 
apply (subst power_add) 

559 
apply (subst setprod_timesf) 

560 
apply (rule arg_cong2)back back 

561 
apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors k Un 

562 
(prime_factors l  prime_factors k)") 

563 
apply (erule ssubst) 

564 
apply (subst setprod_Un_disjoint) 

565 
apply auto 

566 
apply (subgoal_tac "(\<Prod>p\<in>prime_factors l  prime_factors k. p ^ multiplicity p k) = 

567 
(\<Prod>p\<in>prime_factors l  prime_factors k. 1)") 

568 
apply (erule ssubst) 

569 
apply (simp add: setprod_1) 

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

570 
apply (erule prime_factorization_nat) 
31719  571 
apply (rule setprod_cong, auto) 
572 
apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un 

573 
(prime_factors k  prime_factors l)") 

574 
apply (erule ssubst) 

575 
apply (subst setprod_Un_disjoint) 

576 
apply auto 

577 
apply (subgoal_tac "(\<Prod>p\<in>prime_factors k  prime_factors l. p ^ multiplicity p l) = 

578 
(\<Prod>p\<in>prime_factors k  prime_factors l. 1)") 

579 
apply (erule ssubst) 

580 
apply (simp add: setprod_1) 

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

581 
apply (erule prime_factorization_nat) 
31719  582 
apply (rule setprod_cong, auto) 
583 
done 

584 

585 
(* transfer doesn't have the same problem here with the right 

586 
choice of rules. *) 

587 

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

588 
lemma multiplicity_product_aux_int: 
31719  589 
assumes "(k::int) > 0" and "l > 0" 
590 
shows 

591 
"(prime_factors k) Un (prime_factors l) = prime_factors (k * l) & 

592 
(ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))" 

593 

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

594 
apply (rule multiplicity_product_aux_nat [transferred, of l k]) 
31719  595 
using prems apply auto 
596 
done 

597 

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

598 
lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
31719  599 
prime_factors k Un prime_factors l" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

600 
by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric]) 
31719  601 

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

602 
lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
31719  603 
prime_factors k Un prime_factors l" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

604 
by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric]) 
31719  605 

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

606 
lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) = 
31719  607 
multiplicity p k + multiplicity p l" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

608 
by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, 
31719  609 
symmetric]) 
610 

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

611 
lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow> 
31719  612 
multiplicity p (k * l) = multiplicity p k + multiplicity p l" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

613 
by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, 
31719  614 
symmetric]) 
615 

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

616 
lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> (ALL x : S. f x > 0) \<Longrightarrow> 
31719  617 
multiplicity (p::nat) (PROD x : S. f x) = 
618 
(SUM x : S. multiplicity p (f x))" 

619 
apply (induct set: finite) 

620 
apply auto 

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

621 
apply (subst multiplicity_product_nat) 
31719  622 
apply auto 
623 
done 

624 

625 
(* Transfer is delicate here for two reasons: first, because there is 

626 
an implicit quantifier over functions (f), and, second, because the 

627 
product over the multiplicity should not be translated to an integer 

628 
product. 

629 

630 
The way to handle the first is to use quantifier rules for functions. 

631 
The way to handle the second is to turn off the offending rule. 

632 
*) 

633 

634 
lemma transfer_nat_int_sum_prod_closure3: 

635 
"(SUM x : A. int (f x)) >= 0" 

636 
"(PROD x : A. int (f x)) >= 0" 

637 
apply (rule setsum_nonneg, auto) 

638 
apply (rule setprod_nonneg, auto) 

639 
done 

640 

641 
declare TransferMorphism_nat_int[transfer 

642 
add return: transfer_nat_int_sum_prod_closure3 

643 
del: transfer_nat_int_sum_prod2 (1)] 

644 

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

645 
lemma multiplicity_setprod_int: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow> 
31719  646 
(ALL x : S. f x > 0) \<Longrightarrow> 
647 
multiplicity (p::int) (PROD x : S. f x) = 

648 
(SUM x : S. multiplicity p (f x))" 

649 

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

650 
apply (frule multiplicity_setprod_nat 
31719  651 
[where f = "%x. nat(int(nat(f x)))", 
652 
transferred direction: nat "op <= (0::int)"]) 

653 
apply auto 

654 
apply (subst (asm) setprod_cong) 

655 
apply (rule refl) 

656 
apply (rule if_P) 

657 
apply auto 

658 
apply (rule setsum_cong) 

659 
apply auto 

660 
done 

661 

662 
declare TransferMorphism_nat_int[transfer 

663 
add return: transfer_nat_int_sum_prod2 (1)] 

664 

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

665 
lemma multiplicity_prod_prime_powers_nat: 
31719  666 
"finite S \<Longrightarrow> (ALL p : S. prime (p::nat)) \<Longrightarrow> 
667 
multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)" 

668 
apply (subgoal_tac "(PROD p : S. p ^ f p) = 

669 
(PROD p : S. p ^ (%x. if x : S then f x else 0) p)") 

670 
apply (erule ssubst) 

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

671 
apply (subst multiplicity_characterization_nat) 
31719  672 
prefer 5 apply (rule refl) 
673 
apply (rule refl) 

674 
apply auto 

675 
apply (subst setprod_mono_one_right) 

676 
apply assumption 

677 
prefer 3 

678 
apply (rule setprod_cong) 

679 
apply (rule refl) 

680 
apply auto 

681 
done 

682 

683 
(* Here the issue with transfer is the implicit quantifier over S *) 

684 

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

685 
lemma multiplicity_prod_prime_powers_int: 
31719  686 
"(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow> 
687 
multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)" 

688 

689 
apply (subgoal_tac "int ` nat ` S = S") 

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

690 
apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)" 
31719  691 
and S = "nat ` S", transferred]) 
692 
apply auto 

693 
apply (subst prime_int_def [symmetric]) 

694 
apply auto 

695 
apply (subgoal_tac "xb >= 0") 

696 
apply force 

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

697 
apply (rule prime_ge_0_int) 
31719  698 
apply force 
699 
apply (subst transfer_nat_int_set_return_embed) 

700 
apply (unfold nat_set_def, auto) 

701 
done 

702 

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

703 
lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> 
31719  704 
p ~= q \<Longrightarrow> multiplicity p (q^n) = 0" 
705 
apply (subgoal_tac "q^n = setprod (%x. x^n) {q}") 

706 
apply (erule ssubst) 

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

707 
apply (subst multiplicity_prod_prime_powers_nat) 
31719  708 
apply auto 
709 
done 

710 

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

711 
lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> 
31719  712 
p ~= q \<Longrightarrow> multiplicity p (q^n) = 0" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

713 
apply (frule prime_ge_0_int [of q]) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

714 
apply (frule multiplicity_distinct_prime_power_nat [transferred leaving: n]) 
31719  715 
prefer 4 
716 
apply assumption 

717 
apply auto 

718 
done 

719 

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

720 
lemma dvd_multiplicity_nat: 
31719  721 
"(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y" 
722 
apply (case_tac "x = 0") 

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

723 
apply (auto simp add: dvd_def multiplicity_product_nat) 
31719  724 
done 
725 

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

726 
lemma dvd_multiplicity_int: 
31719  727 
"(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow> 
728 
multiplicity p x <= multiplicity p y" 

729 
apply (case_tac "x = 0") 

730 
apply (auto simp add: dvd_def) 

731 
apply (subgoal_tac "0 < k") 

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

732 
apply (auto simp add: multiplicity_product_int) 
31719  733 
apply (erule zero_less_mult_pos) 
734 
apply arith 

735 
done 

736 

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

737 
lemma dvd_prime_factors_nat [intro]: 
31719  738 
"0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

739 
apply (simp only: prime_factors_altdef_nat) 
31719  740 
apply auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

741 
apply (frule dvd_multiplicity_nat) 
31719  742 
apply auto 
743 
(* It is a shame that auto and arith don't get this. *) 

744 
apply (erule order_less_le_trans)back 

745 
apply assumption 

746 
done 

747 

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

748 
lemma dvd_prime_factors_int [intro]: 
31719  749 
"0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

750 
apply (auto simp add: prime_factors_altdef_int) 
31719  751 
apply (erule order_less_le_trans) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

752 
apply (rule dvd_multiplicity_int) 
31719  753 
apply auto 
754 
done 

755 

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

756 
lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
31719  757 
ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow> 
758 
x dvd y" 

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

759 
apply (subst prime_factorization_nat [of x], assumption) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

760 
apply (subst prime_factorization_nat [of y], assumption) 
31719  761 
apply (rule setprod_dvd_setprod_subset2) 
762 
apply force 

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

763 
apply (subst prime_factors_altdef_nat)+ 
31719  764 
apply auto 
765 
(* Again, a shame that auto and arith don't get this. *) 

766 
apply (drule_tac x = xa in spec, auto) 

767 
apply (rule le_imp_power_dvd) 

768 
apply blast 

769 
done 

770 

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

771 
lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> 
31719  772 
ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow> 
773 
x dvd y" 

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

774 
apply (subst prime_factorization_int [of x], assumption) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

775 
apply (subst prime_factorization_int [of y], assumption) 
31719  776 
apply (rule setprod_dvd_setprod_subset2) 
777 
apply force 

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

778 
apply (subst prime_factors_altdef_int)+ 
31719  779 
apply auto 
780 
apply (rule dvd_power_le) 

781 
apply auto 

782 
apply (drule_tac x = xa in spec) 

783 
apply (erule impE) 

784 
apply auto 

785 
done 

786 

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

787 
lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow> 
31719  788 
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y" 
789 
apply (cases "y = 0") 

790 
apply auto 

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

791 
apply (rule multiplicity_dvd_nat, auto) 
31719  792 
apply (case_tac "prime p") 
793 
apply auto 

794 
done 

795 

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

796 
lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow> 
31719  797 
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y" 
798 
apply (cases "y = 0") 

799 
apply auto 

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

800 
apply (rule multiplicity_dvd_int, auto) 
31719  801 
apply (case_tac "prime p") 
802 
apply auto 

803 
done 

804 

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

805 
lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
31719  806 
(x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

807 
by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat) 
31719  808 

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

809 
lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> 
31719  810 
(x dvd y) = (ALL p >= 0. multiplicity p x <= multiplicity p y)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

811 
by (auto intro: dvd_multiplicity_int multiplicity_dvd_int) 
31719  812 

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

813 
lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow> 
31719  814 
(p : prime_factors n) = (prime p & p dvd n)" 
815 
apply (case_tac "prime p") 

816 
apply auto 

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

817 
apply (subst prime_factorization_nat [where n = n], assumption) 
31719  818 
apply (rule dvd_trans) 
819 
apply (rule dvd_power [where x = p and n = "multiplicity p n"]) 

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

820 
apply (subst (asm) prime_factors_altdef_nat, force) 
31719  821 
apply (rule dvd_setprod) 
822 
apply auto 

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

823 
apply (subst prime_factors_altdef_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

824 
apply (subst (asm) dvd_multiplicity_eq_nat) 
31719  825 
apply auto 
826 
apply (drule spec [where x = p]) 

827 
apply auto 

828 
done 

829 

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

830 
lemma prime_factors_altdef2_int: 
31719  831 
assumes "(n::int) > 0" 
832 
shows "(p : prime_factors n) = (prime p & p dvd n)" 

833 

834 
apply (case_tac "p >= 0") 

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

835 
apply (rule prime_factors_altdef2_nat [transferred]) 
31719  836 
using prems apply auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

837 
apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int) 
31719  838 
done 
839 

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

840 
lemma multiplicity_eq_nat: 
31719  841 
fixes x and y::nat 
842 
assumes [arith]: "x > 0" "y > 0" and 

843 
mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y" 

844 
shows "x = y" 

845 

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

847 
apply (auto intro: multiplicity_dvd'_nat) 
31719  848 
done 
849 

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

850 
lemma multiplicity_eq_int: 
31719  851 
fixes x and y::int 
852 
assumes [arith]: "x > 0" "y > 0" and 

853 
mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y" 

854 
shows "x = y" 

855 

33657  856 
apply (rule dvd_antisym [transferred]) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

857 
apply (auto intro: multiplicity_dvd'_int) 
31719  858 
done 
859 

860 

861 
subsection {* An application *} 

862 

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

863 
lemma gcd_eq_nat: 
31719  864 
assumes pos [arith]: "x > 0" "y > 0" 
865 
shows "gcd (x::nat) y = 

866 
(PROD p: prime_factors x Un prime_factors y. 

867 
p ^ (min (multiplicity p x) (multiplicity p y)))" 

868 
proof  

869 
def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 

870 
p ^ (min (multiplicity p x) (multiplicity p y)))" 

871 
have [arith]: "z > 0" 

872 
unfolding z_def by (rule setprod_pos_nat, auto) 

873 
have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 

874 
min (multiplicity p x) (multiplicity p y)" 

875 
unfolding z_def 

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

876 
apply (subst multiplicity_prod_prime_powers_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

877 
apply (auto simp add: multiplicity_not_factor_nat) 
31719  878 
done 
879 
have "z dvd x" 

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

880 
by (intro multiplicity_dvd'_nat, auto simp add: aux) 
31719  881 
moreover have "z dvd y" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

882 
by (intro multiplicity_dvd'_nat, auto simp add: aux) 
31719  883 
moreover have "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z" 
884 
apply auto 

885 
apply (case_tac "w = 0", auto) 

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

886 
apply (erule multiplicity_dvd'_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

887 
apply (auto intro: dvd_multiplicity_nat simp add: aux) 
31719  888 
done 
889 
ultimately have "z = gcd x y" 

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

890 
by (subst gcd_unique_nat [symmetric], blast) 
31719  891 
thus ?thesis 
892 
unfolding z_def by auto 

893 
qed 

894 

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

895 
lemma lcm_eq_nat: 
31719  896 
assumes pos [arith]: "x > 0" "y > 0" 
897 
shows "lcm (x::nat) y = 

898 
(PROD p: prime_factors x Un prime_factors y. 

899 
p ^ (max (multiplicity p x) (multiplicity p y)))" 

900 
proof  

901 
def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 

902 
p ^ (max (multiplicity p x) (multiplicity p y)))" 

903 
have [arith]: "z > 0" 

904 
unfolding z_def by (rule setprod_pos_nat, auto) 

905 
have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 

906 
max (multiplicity p x) (multiplicity p y)" 

907 
unfolding z_def 

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

908 
apply (subst multiplicity_prod_prime_powers_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

909 
apply (auto simp add: multiplicity_not_factor_nat) 
31719  910 
done 
911 
have "x dvd z" 

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

912 
by (intro multiplicity_dvd'_nat, auto simp add: aux) 
31719  913 
moreover have "y dvd z" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

914 
by (intro multiplicity_dvd'_nat, auto simp add: aux) 
31719  915 
moreover have "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w" 
916 
apply auto 

917 
apply (case_tac "w = 0", auto) 

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

918 
apply (rule multiplicity_dvd'_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

919 
apply (auto intro: dvd_multiplicity_nat simp add: aux) 
31719  920 
done 
921 
ultimately have "z = lcm x y" 

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

922 
by (subst lcm_unique_nat [symmetric], blast) 
31719  923 
thus ?thesis 
924 
unfolding z_def by auto 

925 
qed 

926 

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

927 
lemma multiplicity_gcd_nat: 
31719  928 
assumes [arith]: "x > 0" "y > 0" 
929 
shows "multiplicity (p::nat) (gcd x y) = 

930 
min (multiplicity p x) (multiplicity p y)" 

931 

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

932 
apply (subst gcd_eq_nat) 
31719  933 
apply auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

934 
apply (subst multiplicity_prod_prime_powers_nat) 
31719  935 
apply auto 
936 
done 

937 

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

938 
lemma multiplicity_lcm_nat: 
31719  939 
assumes [arith]: "x > 0" "y > 0" 
940 
shows "multiplicity (p::nat) (lcm x y) = 

941 
max (multiplicity p x) (multiplicity p y)" 

942 

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

943 
apply (subst lcm_eq_nat) 
31719  944 
apply auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

945 
apply (subst multiplicity_prod_prime_powers_nat) 
31719  946 
apply auto 
947 
done 

948 

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

949 
lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)" 
31719  950 
apply (case_tac "x = 0  y = 0  z = 0") 
951 
apply auto 

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

952 
apply (rule multiplicity_eq_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

953 
apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

954 
lcm_pos_nat) 
31719  955 
done 
956 

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

957 
lemma gcd_lcm_distrib_int: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)" 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

958 
apply (subst (1 2 3) gcd_abs_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

959 
apply (subst lcm_abs_int) 
31719  960 
apply (subst (2) abs_of_nonneg) 
961 
apply force 

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

962 
apply (rule gcd_lcm_distrib_nat [transferred]) 
31719  963 
apply auto 
964 
done 

965 

966 
end 