author  haftmann 
Mon, 12 Jul 2010 08:58:13 +0200  
changeset 37765  26bdfb7b680b 
parent 37290  3464d7232670 
child 39302  d7728f65b353 
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 
(* Here is a version of set product for multisets. Is it worth moving 

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

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

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

63 
*) 

64 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

65 
definition msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b" where 
31719  66 
"msetprod f M == setprod (%x. (f x)^(count M x)) (set_of M)" 
67 

68 
syntax 

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

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

71 

72 
translations 

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

37290  75 
lemma msetprod_empty: 
76 
"msetprod f {#} = 1" 

77 
by (simp add: msetprod_def) 

78 

79 
lemma msetprod_singleton: 

80 
"msetprod f {#x#} = f x" 

81 
by (simp add: msetprod_def) 

82 

31719  83 
lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 
84 
apply (simp add: msetprod_def power_add) 

85 
apply (subst setprod_Un2) 

86 
apply auto 

87 
apply (subgoal_tac 

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

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

90 
apply (erule ssubst) 

91 
apply (subgoal_tac 

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

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

94 
apply (erule ssubst) 

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

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

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

98 
apply (erule ssubst) 

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

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

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

102 
apply (erule ssubst) 

103 
apply (subst setprod_timesf) 

104 
apply (force simp add: mult_ac) 

105 
apply (subst setprod_Un_disjoint [symmetric]) 

106 
apply (auto intro: setprod_cong) 

107 
apply (subst setprod_Un_disjoint [symmetric]) 

108 
apply (auto intro: setprod_cong) 

109 
done 

110 

111 

112 
subsection {* unique factorization: multiset version *} 

113 

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

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

116 
proof (rule nat_less_induct, clarify) 

117 
fix n :: nat 

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

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

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

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

122 
by arith 

123 
moreover 

124 
{ 

125 
assume "n = 1" 

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

127 
by (auto simp add: msetprod_def) 

128 
} 

129 
moreover 

130 
{ 

131 
assume "n > 1" and "prime n" 

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

133 
by (auto simp add: msetprod_def) 

134 
} 

135 
moreover 

136 
{ 

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

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

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

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

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

143 
by blast 

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

145 
by (auto simp add: prems msetprod_Un set_of_union) 

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

147 
} 

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

149 
by blast 

150 
qed 

151 

152 
lemma multiset_prime_factorization_unique_aux: 

153 
fixes a :: nat 

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

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

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

157 
shows 

158 
"count M a <= count N a" 

159 
proof cases 

160 
assume "a : set_of M" 

161 
with prems have a: "prime a" 

162 
by auto 

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

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

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

166 
by (rule prems) 

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

168 
by (simp add: msetprod_def) 

169 
also have "... = 

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

171 
proof (cases) 

172 
assume "a : set_of N" 

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

174 
by auto 

175 
thus ?thesis 

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

177 
next 

178 
assume "a ~: set_of N" 

179 
thus ?thesis 

180 
by auto 

181 
qed 

182 
finally have "a ^ count M a dvd 

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

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

185 
(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

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

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

188 
apply (rule primes_imp_powers_coprime_nat) 
31719  189 
apply (insert prems, auto) 
190 
done 

191 
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

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

195 
next 

196 
assume "a ~: set_of M" 

197 
thus ?thesis by auto 

198 
qed 

199 

200 
lemma multiset_prime_factorization_unique: 

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

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

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

204 
shows 

205 
"M = N" 

206 
proof  

207 
{ 

208 
fix a 

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

210 
by (intro multiset_prime_factorization_unique_aux, auto) 

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

212 
by (intro multiset_prime_factorization_unique_aux, auto) 

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

214 
by auto 

215 
} 

36903  216 
thus ?thesis by (simp add:multiset_ext_iff) 
31719  217 
qed 
218 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

219 
definition multiset_prime_factorization :: "nat => nat multiset" where 
31719  220 
"multiset_prime_factorization n == 
221 
if n > 0 then (THE M. ((ALL p : set_of M. prime p) & 

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

223 
else {#}" 

224 

225 
lemma multiset_prime_factorization: "n > 0 ==> 

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

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

228 
apply (unfold multiset_prime_factorization_def) 

229 
apply clarsimp 

230 
apply (frule multiset_prime_factorization_exists) 

231 
apply clarify 

232 
apply (rule theI) 

233 
apply (insert multiset_prime_factorization_unique, blast)+ 

234 
done 

235 

236 

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

238 

239 
class unique_factorization = 

240 

241 
fixes 

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

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

244 

245 
(* definitions for the natural numbers *) 

246 

247 
instantiation nat :: unique_factorization 

248 

249 
begin 

250 

251 
definition 

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

253 
where 

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

255 

256 
definition 

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

258 
where 

259 
"prime_factors_nat n = set_of (multiset_prime_factorization n)" 

260 

261 
instance proof qed 

262 

263 
end 

264 

265 
(* definitions for the integers *) 

266 

267 
instantiation int :: unique_factorization 

268 

269 
begin 

270 

271 
definition 

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

273 
where 

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

275 

276 
definition 

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

278 
where 

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

280 

281 
instance proof qed 

282 

283 
end 

284 

285 

286 
subsection {* Set up transfer *} 

287 

288 
lemma transfer_nat_int_prime_factors: 

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

290 
unfolding prime_factors_int_def apply auto 

291 
by (subst transfer_int_nat_set_return_embed, assumption) 

292 

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

294 
nat_set (prime_factors n)" 

295 
by (auto simp add: nat_set_def prime_factors_int_def) 

296 

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

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

299 
by (auto simp add: multiplicity_int_def) 

300 

35644  301 
declare transfer_morphism_nat_int[transfer add return: 
31719  302 
transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure 
303 
transfer_nat_int_multiplicity] 

304 

305 

306 
lemma transfer_int_nat_prime_factors: 

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

308 
unfolding prime_factors_int_def by auto 

309 

310 
lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> 

311 
nat_set (prime_factors n)" 

312 
by (simp only: transfer_nat_int_prime_factors_closure is_nat_def) 

313 

314 
lemma transfer_int_nat_multiplicity: 

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

316 
by (auto simp add: multiplicity_int_def) 

317 

35644  318 
declare transfer_morphism_int_nat[transfer add return: 
31719  319 
transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure 
320 
transfer_int_nat_multiplicity] 

321 

322 

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

324 

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

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

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

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

331 
apply (auto simp add: prime_factors_nat_def multiset_prime_factorization) 

332 
done 

333 

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

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

337 

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

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

341 

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

342 
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

343 
by (frule prime_factors_prime_nat, auto) 
31719  344 

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

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

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

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

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

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

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

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

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

358 

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

359 
lemma prime_factors_altdef_int: "prime_factors (n::int) = 
31719  360 
{p. p >= 0 & multiplicity p n > 0}" 
361 
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

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

365 

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

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

369 
simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def) 

370 

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

371 
thm prime_factorization_nat [transferred] 
31719  372 

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

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

376 

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

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

380 

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

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

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

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

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

388 
apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset 

389 
f") 

390 
apply (unfold prime_factors_nat_def multiplicity_nat_def) 

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

394 
prefer 2 

395 
apply force 

396 
apply (subst if_P, assumption) 

397 
apply (rule the1_equality) 

398 
apply (rule ex_ex1I) 

399 
apply (rule multiset_prime_factorization_exists, assumption) 

400 
apply (rule multiset_prime_factorization_unique) 

401 
apply force 

402 
apply force 

403 
apply force 

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

407 
unfolding multiset_def apply force 

408 
done 

409 

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

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

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

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

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

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

419 
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

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

423 

424 
(* A minor glitch:*) 

425 

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

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

429 

430 
(* 

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

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

433 
*) 

434 

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

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

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

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

440 

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

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

444 
apply auto 

445 
done 

446 

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

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

450 
apply simp 

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

452 
apply (simp only:) 

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

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

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

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

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

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

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

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

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

467 
apply (rule impI)+ 

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

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

471 

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

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

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

476 

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

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

480 
apply auto 

481 
done 

482 

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

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

486 
apply simp 

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

488 
apply (simp only:) 

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

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

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

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

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

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

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

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

500 
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

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

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

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

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

506 
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

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

510 
apply (case_tac "x = p") 

511 
apply auto 

512 
done 

513 

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

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

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

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

520 
apply auto 

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

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

524 
apply (case_tac "x = p") 

525 
apply auto 

526 
done 

527 

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

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

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

533 

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

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

537 
apply auto 

538 
apply (frule multiset_prime_factorization) 

539 
apply (auto simp add: set_of_def multiplicity_nat_def) 

540 
done 

541 

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

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

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

545 
lemma multiplicity_not_factor_nat [simp]: 
31719  546 
"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

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

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

549 
lemma multiplicity_not_factor_int [simp]: 
31719  550 
"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

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

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

553 
lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> 
31719  554 
(prime_factors k) Un (prime_factors l) = prime_factors (k * l) & 
555 
(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

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

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

560 
apply (subst setprod_timesf) 

561 
apply (rule arg_cong2)back back 

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

563 
(prime_factors l  prime_factors k)") 

564 
apply (erule ssubst) 

565 
apply (subst setprod_Un_disjoint) 

566 
apply auto 

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

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

569 
apply (erule ssubst) 

570 
apply (simp add: setprod_1) 

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

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

574 
(prime_factors k  prime_factors l)") 

575 
apply (erule ssubst) 

576 
apply (subst setprod_Un_disjoint) 

577 
apply auto 

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

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

580 
apply (erule ssubst) 

581 
apply (simp add: setprod_1) 

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

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

585 

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

587 
choice of rules. *) 

588 

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

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

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

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

594 

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

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

598 

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

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

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

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

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

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

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

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

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

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

612 
lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow> 
31719  613 
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

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

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

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

620 
apply (induct set: finite) 

621 
apply auto 

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

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

625 

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

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

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

629 
product. 

630 

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

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

633 
*) 

634 

635 
lemma transfer_nat_int_sum_prod_closure3: 

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

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

638 
apply (rule setsum_nonneg, auto) 

639 
apply (rule setprod_nonneg, auto) 

640 
done 

641 

35644  642 
declare transfer_morphism_nat_int[transfer 
31719  643 
add return: transfer_nat_int_sum_prod_closure3 
644 
del: transfer_nat_int_sum_prod2 (1)] 

645 

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

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

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

650 

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

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

654 
apply auto 

655 
apply (subst (asm) setprod_cong) 

656 
apply (rule refl) 

657 
apply (rule if_P) 

658 
apply auto 

659 
apply (rule setsum_cong) 

660 
apply auto 

661 
done 

662 

35644  663 
declare transfer_morphism_nat_int[transfer 
31719  664 
add return: transfer_nat_int_sum_prod2 (1)] 
665 

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

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

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

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

671 
apply (erule ssubst) 

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

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

675 
apply auto 

676 
apply (subst setprod_mono_one_right) 

677 
apply assumption 

678 
prefer 3 

679 
apply (rule setprod_cong) 

680 
apply (rule refl) 

681 
apply auto 

682 
done 

683 

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

685 

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

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

689 

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

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

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

694 
apply (subst prime_int_def [symmetric]) 

695 
apply auto 

696 
apply (subgoal_tac "xb >= 0") 

697 
apply force 

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

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

701 
apply (unfold nat_set_def, auto) 

702 
done 

703 

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

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

707 
apply (erule ssubst) 

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

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

711 

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

712 
lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> 
31719  713 
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

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

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

718 
apply auto 

719 
done 

720 

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

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

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

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

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

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

730 
apply (case_tac "x = 0") 

731 
apply (auto simp add: dvd_def) 

732 
apply (subgoal_tac "0 < k") 

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

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

736 
done 

737 

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

738 
lemma dvd_prime_factors_nat [intro]: 
31719  739 
"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

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

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

745 
apply (erule order_less_le_trans)back 

746 
apply assumption 

747 
done 

748 

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

749 
lemma dvd_prime_factors_int [intro]: 
31719  750 
"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

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

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

756 

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

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

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

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

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

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

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

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

768 
apply (rule le_imp_power_dvd) 

769 
apply blast 

770 
done 

771 

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

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

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

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

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

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

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

782 
apply auto 

783 
apply (drule_tac x = xa in spec) 

784 
apply (erule impE) 

785 
apply auto 

786 
done 

787 

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

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

791 
apply auto 

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

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

795 
done 

796 

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

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

800 
apply auto 

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

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

804 
done 

805 

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

806 
lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
31719  807 
(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

808 
by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat) 
31719  809 

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

810 
lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> 
31719  811 
(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

812 
by (auto intro: dvd_multiplicity_int multiplicity_dvd_int) 
31719  813 

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

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

817 
apply auto 

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

818 
apply (subst prime_factorization_nat [where n = n], assumption) 
31719  819 
apply (rule dvd_trans) 
820 
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

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

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

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

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

828 
apply auto 

829 
done 

830 

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

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

834 

835 
apply (case_tac "p >= 0") 

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

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

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

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

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

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

845 
shows "x = y" 

846 

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

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

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

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

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

855 
shows "x = y" 

856 

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

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

861 

862 
subsection {* An application *} 

863 

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

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

867 
(PROD p: prime_factors x Un prime_factors y. 

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

869 
proof  

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

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

872 
have [arith]: "z > 0" 

873 
unfolding z_def by (rule setprod_pos_nat, auto) 

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

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

876 
unfolding z_def 

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

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

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

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

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

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

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

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

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

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

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

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

894 
qed 

895 

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

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

899 
(PROD p: prime_factors x Un prime_factors y. 

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

901 
proof  

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

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

904 
have [arith]: "z > 0" 

905 
unfolding z_def by (rule setprod_pos_nat, auto) 

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

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

908 
unfolding z_def 

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

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

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

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

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

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

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

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

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

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

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

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

926 
qed 

927 

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

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

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

932 

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

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

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

938 

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

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

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

943 

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

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

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

949 

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

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

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

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

954 
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

955 
lcm_pos_nat) 
31719  956 
done 
957 

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

958 
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

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

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

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

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

966 

967 
end 