author  haftmann 
Mon, 08 Mar 2010 09:38:58 +0100  
changeset 35644  d20cf282342e 
parent 35416  d8d7d1b785af 
child 36903  489c1fbbb028 
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 

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

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

73 
syntax 

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

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

76 

77 
translations 

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

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

81 
apply (simp add: msetprod_def power_add) 

82 
apply (subst setprod_Un2) 

83 
apply auto 

84 
apply (subgoal_tac 

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

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

87 
apply (erule ssubst) 

88 
apply (subgoal_tac 

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

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

91 
apply (erule ssubst) 

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

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

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

95 
apply (erule ssubst) 

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

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

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

99 
apply (erule ssubst) 

100 
apply (subst setprod_timesf) 

101 
apply (force simp add: mult_ac) 

102 
apply (subst setprod_Un_disjoint [symmetric]) 

103 
apply (auto intro: setprod_cong) 

104 
apply (subst setprod_Un_disjoint [symmetric]) 

105 
apply (auto intro: setprod_cong) 

106 
done 

107 

108 

109 
subsection {* unique factorization: multiset version *} 

110 

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

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

113 
proof (rule nat_less_induct, clarify) 

114 
fix n :: nat 

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

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

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

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

119 
by arith 

120 
moreover 

121 
{ 

122 
assume "n = 1" 

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

124 
by (auto simp add: msetprod_def) 

125 
} 

126 
moreover 

127 
{ 

128 
assume "n > 1" and "prime n" 

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

130 
by (auto simp add: msetprod_def) 

131 
} 

132 
moreover 

133 
{ 

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

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

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

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

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

140 
by blast 

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

142 
by (auto simp add: prems msetprod_Un set_of_union) 

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

144 
} 

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

146 
by blast 

147 
qed 

148 

149 
lemma multiset_prime_factorization_unique_aux: 

150 
fixes a :: nat 

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

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

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

154 
shows 

155 
"count M a <= count N a" 

156 
proof cases 

157 
assume "a : set_of M" 

158 
with prems have a: "prime a" 

159 
by auto 

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

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

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

163 
by (rule prems) 

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

165 
by (simp add: msetprod_def) 

166 
also have "... = 

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

168 
proof (cases) 

169 
assume "a : set_of N" 

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

171 
by auto 

172 
thus ?thesis 

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

174 
next 

175 
assume "a ~: set_of N" 

176 
thus ?thesis 

177 
by auto 

178 
qed 

179 
finally have "a ^ count M a dvd 

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

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

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

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

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

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

188 
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

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

192 
next 

193 
assume "a ~: set_of M" 

194 
thus ?thesis by auto 

195 
qed 

196 

197 
lemma multiset_prime_factorization_unique: 

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

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

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

201 
shows 

202 
"M = N" 

203 
proof  

204 
{ 

205 
fix a 

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

207 
by (intro multiset_prime_factorization_unique_aux, auto) 

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

209 
by (intro multiset_prime_factorization_unique_aux, auto) 

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

211 
by auto 

212 
} 

213 
thus ?thesis by (simp add:multiset_eq_conv_count_eq) 

214 
qed 

215 

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

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

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

220 
else {#}" 

221 

222 
lemma multiset_prime_factorization: "n > 0 ==> 

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

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

225 
apply (unfold multiset_prime_factorization_def) 

226 
apply clarsimp 

227 
apply (frule multiset_prime_factorization_exists) 

228 
apply clarify 

229 
apply (rule theI) 

230 
apply (insert multiset_prime_factorization_unique, blast)+ 

231 
done 

232 

233 

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

235 

236 
class unique_factorization = 

237 

238 
fixes 

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

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

241 

242 
(* definitions for the natural numbers *) 

243 

244 
instantiation nat :: unique_factorization 

245 

246 
begin 

247 

248 
definition 

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

250 
where 

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

252 

253 
definition 

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

255 
where 

256 
"prime_factors_nat n = set_of (multiset_prime_factorization n)" 

257 

258 
instance proof qed 

259 

260 
end 

261 

262 
(* definitions for the integers *) 

263 

264 
instantiation int :: unique_factorization 

265 

266 
begin 

267 

268 
definition 

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

270 
where 

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

272 

273 
definition 

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

275 
where 

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

277 

278 
instance proof qed 

279 

280 
end 

281 

282 

283 
subsection {* Set up transfer *} 

284 

285 
lemma transfer_nat_int_prime_factors: 

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

287 
unfolding prime_factors_int_def apply auto 

288 
by (subst transfer_int_nat_set_return_embed, assumption) 

289 

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

291 
nat_set (prime_factors n)" 

292 
by (auto simp add: nat_set_def prime_factors_int_def) 

293 

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

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

296 
by (auto simp add: multiplicity_int_def) 

297 

35644  298 
declare transfer_morphism_nat_int[transfer add return: 
31719  299 
transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure 
300 
transfer_nat_int_multiplicity] 

301 

302 

303 
lemma transfer_int_nat_prime_factors: 

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

305 
unfolding prime_factors_int_def by auto 

306 

307 
lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> 

308 
nat_set (prime_factors n)" 

309 
by (simp only: transfer_nat_int_prime_factors_closure is_nat_def) 

310 

311 
lemma transfer_int_nat_multiplicity: 

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

313 
by (auto simp add: multiplicity_int_def) 

314 

35644  315 
declare transfer_morphism_int_nat[transfer add return: 
31719  316 
transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure 
317 
transfer_int_nat_multiplicity] 

318 

319 

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

321 

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

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

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

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

328 
apply (auto simp add: prime_factors_nat_def multiset_prime_factorization) 

329 
done 

330 

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

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

334 

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

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

338 

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

339 
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

340 
by (frule prime_factors_prime_nat, auto) 
31719  341 

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

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

344 
by (frule (1) prime_factors_prime_int, auto) 
31719  345 

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

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

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

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

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

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

355 

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

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

359 
apply (subst prime_factors_altdef_nat) 
31719  360 
apply (auto simp add: image_def) 
361 
done 

362 

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

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

366 
simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def) 

367 

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

368 
thm prime_factorization_nat [transferred] 
31719  369 

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

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

373 

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

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

377 

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

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

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

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

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

385 
apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset 

386 
f") 

387 
apply (unfold prime_factors_nat_def multiplicity_nat_def) 

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

391 
prefer 2 

392 
apply force 

393 
apply (subst if_P, assumption) 

394 
apply (rule the1_equality) 

395 
apply (rule ex_ex1I) 

396 
apply (rule multiset_prime_factorization_exists, assumption) 

397 
apply (rule multiset_prime_factorization_unique) 

398 
apply force 

399 
apply force 

400 
apply force 

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

404 
unfolding multiset_def apply force 

405 
done 

406 

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

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

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

410 
by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric], 
31719  411 
assumption+) 
412 

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

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

416 
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

417 
apply (rule prime_factors_characterization_nat) 
31719  418 
apply auto 
419 
done 

420 

421 
(* A minor glitch:*) 

422 

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

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

426 

427 
(* 

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

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

430 
*) 

431 

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

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

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

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

437 

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

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

441 
apply auto 

442 
done 

443 

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

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

447 
apply simp 

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

449 
apply (simp only:) 

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

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

452 
apply (auto simp add: prime_ge_0_int) 
31719  453 
done 
454 

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

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

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

458 
by (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, 
31719  459 
symmetric], auto) 
460 

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

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

464 
apply (rule impI)+ 

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

465 
apply (rule multiplicity_characterization_nat) 
31719  466 
apply auto 
467 
done 

468 

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

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

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

473 

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

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

477 
apply auto 

478 
done 

479 

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

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

483 
apply simp 

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

485 
apply (simp only:) 

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

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

488 
apply (auto simp add: prime_ge_0_int) 
31719  489 
done 
490 

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

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

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

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

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

497 
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

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

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

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

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

503 
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

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

507 
apply (case_tac "x = p") 

508 
apply auto 

509 
done 

510 

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

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

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

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

517 
apply auto 

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

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

521 
apply (case_tac "x = p") 

522 
apply auto 

523 
done 

524 

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

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

527 
apply (frule prime_ge_0_int) 
31719  528 
apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq) 
529 
done 

530 

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

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

534 
apply auto 

535 
apply (frule multiset_prime_factorization) 

536 
apply (auto simp add: set_of_def multiplicity_nat_def) 

537 
done 

538 

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

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

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

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

544 
by (subst (asm) prime_factors_altdef_nat, auto) 
31719  545 

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

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

548 
by (subst (asm) prime_factors_altdef_int, auto) 
31719  549 

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

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

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

554 
apply (simp only: prime_factors_altdef_nat) 
31719  555 
apply auto 
556 
apply (subst power_add) 

557 
apply (subst setprod_timesf) 

558 
apply (rule arg_cong2)back back 

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

560 
(prime_factors l  prime_factors k)") 

561 
apply (erule ssubst) 

562 
apply (subst setprod_Un_disjoint) 

563 
apply auto 

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

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

566 
apply (erule ssubst) 

567 
apply (simp add: setprod_1) 

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

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

571 
(prime_factors k  prime_factors l)") 

572 
apply (erule ssubst) 

573 
apply (subst setprod_Un_disjoint) 

574 
apply auto 

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

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

577 
apply (erule ssubst) 

578 
apply (simp add: setprod_1) 

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

579 
apply (erule prime_factorization_nat) 
31719  580 
apply (rule setprod_cong, auto) 
581 
done 

582 

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

584 
choice of rules. *) 

585 

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

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

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

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

591 

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

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

595 

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

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

598 
by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric]) 
31719  599 

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

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

602 
by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric]) 
31719  603 

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

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

606 
by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, 
31719  607 
symmetric]) 
608 

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

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

611 
by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, 
31719  612 
symmetric]) 
613 

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

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

617 
apply (induct set: finite) 

618 
apply auto 

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

619 
apply (subst multiplicity_product_nat) 
31719  620 
apply auto 
621 
done 

622 

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

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

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

626 
product. 

627 

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

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

630 
*) 

631 

632 
lemma transfer_nat_int_sum_prod_closure3: 

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

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

635 
apply (rule setsum_nonneg, auto) 

636 
apply (rule setprod_nonneg, auto) 

637 
done 

638 

35644  639 
declare transfer_morphism_nat_int[transfer 
31719  640 
add return: transfer_nat_int_sum_prod_closure3 
641 
del: transfer_nat_int_sum_prod2 (1)] 

642 

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

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

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

647 

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

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

651 
apply auto 

652 
apply (subst (asm) setprod_cong) 

653 
apply (rule refl) 

654 
apply (rule if_P) 

655 
apply auto 

656 
apply (rule setsum_cong) 

657 
apply auto 

658 
done 

659 

35644  660 
declare transfer_morphism_nat_int[transfer 
31719  661 
add return: transfer_nat_int_sum_prod2 (1)] 
662 

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

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

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

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

668 
apply (erule ssubst) 

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

669 
apply (subst multiplicity_characterization_nat) 
31719  670 
prefer 5 apply (rule refl) 
671 
apply (rule refl) 

672 
apply auto 

673 
apply (subst setprod_mono_one_right) 

674 
apply assumption 

675 
prefer 3 

676 
apply (rule setprod_cong) 

677 
apply (rule refl) 

678 
apply auto 

679 
done 

680 

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

682 

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

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

686 

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

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

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

691 
apply (subst prime_int_def [symmetric]) 

692 
apply auto 

693 
apply (subgoal_tac "xb >= 0") 

694 
apply force 

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

695 
apply (rule prime_ge_0_int) 
31719  696 
apply force 
697 
apply (subst transfer_nat_int_set_return_embed) 

698 
apply (unfold nat_set_def, auto) 

699 
done 

700 

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

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

704 
apply (erule ssubst) 

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

705 
apply (subst multiplicity_prod_prime_powers_nat) 
31719  706 
apply auto 
707 
done 

708 

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

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

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

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

715 
apply auto 

716 
done 

717 

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

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

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

721 
apply (auto simp add: dvd_def multiplicity_product_nat) 
31719  722 
done 
723 

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

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

727 
apply (case_tac "x = 0") 

728 
apply (auto simp add: dvd_def) 

729 
apply (subgoal_tac "0 < k") 

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

730 
apply (auto simp add: multiplicity_product_int) 
31719  731 
apply (erule zero_less_mult_pos) 
732 
apply arith 

733 
done 

734 

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

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

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

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

742 
apply (erule order_less_le_trans)back 

743 
apply assumption 

744 
done 

745 

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

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

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

750 
apply (rule dvd_multiplicity_int) 
31719  751 
apply auto 
752 
done 

753 

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

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

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

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

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

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

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

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

765 
apply (rule le_imp_power_dvd) 

766 
apply blast 

767 
done 

768 

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

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

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

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

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

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

776 
apply (subst prime_factors_altdef_int)+ 
31719  777 
apply auto 
778 
apply (rule dvd_power_le) 

779 
apply auto 

780 
apply (drule_tac x = xa in spec) 

781 
apply (erule impE) 

782 
apply auto 

783 
done 

784 

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

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

788 
apply auto 

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

789 
apply (rule multiplicity_dvd_nat, auto) 
31719  790 
apply (case_tac "prime p") 
791 
apply auto 

792 
done 

793 

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

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

797 
apply auto 

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

798 
apply (rule multiplicity_dvd_int, auto) 
31719  799 
apply (case_tac "prime p") 
800 
apply auto 

801 
done 

802 

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

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

805 
by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat) 
31719  806 

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

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

809 
by (auto intro: dvd_multiplicity_int multiplicity_dvd_int) 
31719  810 

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

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

814 
apply auto 

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

815 
apply (subst prime_factorization_nat [where n = n], assumption) 
31719  816 
apply (rule dvd_trans) 
817 
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

818 
apply (subst (asm) prime_factors_altdef_nat, force) 
31719  819 
apply (rule dvd_setprod) 
820 
apply auto 

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

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

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

825 
apply auto 

826 
done 

827 

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

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

831 

832 
apply (case_tac "p >= 0") 

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

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

835 
apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int) 
31719  836 
done 
837 

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

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

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

842 
shows "x = y" 

843 

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

845 
apply (auto intro: multiplicity_dvd'_nat) 
31719  846 
done 
847 

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

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

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

852 
shows "x = y" 

853 

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

855 
apply (auto intro: multiplicity_dvd'_int) 
31719  856 
done 
857 

858 

859 
subsection {* An application *} 

860 

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

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

864 
(PROD p: prime_factors x Un prime_factors y. 

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

866 
proof  

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

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

869 
have [arith]: "z > 0" 

870 
unfolding z_def by (rule setprod_pos_nat, auto) 

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

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

873 
unfolding z_def 

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

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

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

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

878 
by (intro multiplicity_dvd'_nat, auto simp add: aux) 
31719  879 
moreover have "z dvd y" 
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 "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z" 
882 
apply auto 

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

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

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

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

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

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

891 
qed 

892 

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

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

896 
(PROD p: prime_factors x Un prime_factors y. 

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

898 
proof  

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

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

901 
have [arith]: "z > 0" 

902 
unfolding z_def by (rule setprod_pos_nat, auto) 

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

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

905 
unfolding z_def 

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

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

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

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

910 
by (intro multiplicity_dvd'_nat, auto simp add: aux) 
31719  911 
moreover have "y 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 "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w" 
914 
apply auto 

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

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

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

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

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

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

923 
qed 

924 

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

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

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

929 

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

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

932 
apply (subst multiplicity_prod_prime_powers_nat) 
31719  933 
apply auto 
934 
done 

935 

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

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

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

940 

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

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

943 
apply (subst multiplicity_prod_prime_powers_nat) 
31719  944 
apply auto 
945 
done 

946 

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

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

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

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

951 
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

952 
lcm_pos_nat) 
31719  953 
done 
954 

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

955 
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

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

957 
apply (subst lcm_abs_int) 
31719  958 
apply (subst (2) abs_of_nonneg) 
959 
apply force 

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

960 
apply (rule gcd_lcm_distrib_nat [transferred]) 
31719  961 
apply auto 
962 
done 

963 

964 
end 