author  haftmann 
Sun, 09 Nov 2014 10:03:18 +0100  
changeset 58954  18750e86d5b8 
parent 58889  5b7a9633cfa8 
child 59010  ec2b4270a502 
permissions  rwrr 
41959  1 
(* Title: HOL/Number_Theory/UniqueFactorization.thy 
31719  2 
Author: Jeremy Avigad 
3 

41541  4 
Unique factorization for the natural numbers and the integers. 
31719  5 

41541  6 
Note: there were previous Isabelle formalizations of unique 
7 
factorization due to Thomas Marthedal Rasmussen, and, building on 

8 
that, by Jeremy Avigad and David Gray. 

31719  9 
*) 
10 

58889  11 
section {* UniqueFactorization *} 
31719  12 

13 
theory UniqueFactorization 

41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
40461
diff
changeset

14 
imports Cong "~~/src/HOL/Library/Multiset" 
31719  15 
begin 
16 

17 
(* As a simp or intro rule, 

18 

19 
prime p \<Longrightarrow> p > 0 

20 

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

22 
leads to the backchaining 

23 

24 
x > 0 

25 
prime x 

26 
x :# M which is, unfortunately, 

27 
count M x > 0 

28 
*) 

29 

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

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

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

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

34 
*) 

35 

36 

37 
subsection {* unique factorization: multiset version *} 

38 

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

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

41 
proof (rule nat_less_induct, clarify) 

42 
fix n :: nat 

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

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

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

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

47 
by arith 

44872  48 
moreover { 
31719  49 
assume "n = 1" 
51489  50 
then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)" by auto 
44872  51 
} moreover { 
31719  52 
assume "n > 1" and "prime n" 
53 
then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)" 

49824  54 
by auto 
44872  55 
} moreover { 
31719  56 
assume "n > 1" and "~ prime n" 
44872  57 
with not_prime_eq_prod_nat 
58 
obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n" 

59 
by blast 

31719  60 
with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)" 
61 
and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)" 

62 
by blast 

44872  63 
then have "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)" 
41541  64 
by (auto simp add: n msetprod_Un) 
31719  65 
then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)".. 
66 
} 

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

68 
by blast 

69 
qed 

70 

71 
lemma multiset_prime_factorization_unique_aux: 

72 
fixes a :: nat 

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

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

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

76 
shows 

77 
"count M a <= count N a" 

78 
proof cases 

41541  79 
assume M: "a : set_of M" 
80 
with assms have a: "prime a" by auto 

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

49824  82 
by (auto simp add: msetprod_multiplicity intro: dvd_setprod) 
41541  83 
also have "... dvd (PROD i :# N. i)" by (rule assms) 
31719  84 
also have "... = (PROD i : (set_of N). i ^ (count N i))" 
49824  85 
by (simp add: msetprod_multiplicity) 
44872  86 
also have "... = a^(count N a) * (PROD i : (set_of N  {a}). i ^ (count N i))" 
87 
proof (cases) 

88 
assume "a : set_of N" 

89 
then have b: "set_of N = {a} Un (set_of N  {a})" 

90 
by auto 

91 
then show ?thesis 

57418  92 
by (subst (1) b, subst setprod.union_disjoint, auto) 
44872  93 
next 
94 
assume "a ~: set_of N" 

95 
then show ?thesis by auto 

96 
qed 

31719  97 
finally have "a ^ count M a dvd 
98 
a^(count N a) * (PROD i : (set_of N  {a}). i ^ (count N i))". 

44872  99 
moreover 
100 
have "coprime (a ^ count M a) (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

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

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

103 
apply (rule primes_imp_powers_coprime_nat) 
41541  104 
using assms M 
105 
apply auto 

31719  106 
done 
107 
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

108 
by (elim coprime_dvd_mult_nat) 
31719  109 
with a show ?thesis 
44872  110 
apply (intro power_dvd_imp_le) 
111 
apply auto 

112 
done 

31719  113 
next 
114 
assume "a ~: set_of M" 

44872  115 
then show ?thesis by auto 
31719  116 
qed 
117 

118 
lemma multiset_prime_factorization_unique: 

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

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

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

122 
shows 

123 
"M = N" 

124 
proof  

125 
{ 

126 
fix a 

41541  127 
from assms have "count M a <= count N a" 
31719  128 
by (intro multiset_prime_factorization_unique_aux, auto) 
41541  129 
moreover from assms have "count N a <= count M a" 
31719  130 
by (intro multiset_prime_factorization_unique_aux, auto) 
131 
ultimately have "count M a = count N a" 

132 
by auto 

133 
} 

44872  134 
then show ?thesis by (simp add:multiset_eq_iff) 
31719  135 
qed 
136 

44872  137 
definition multiset_prime_factorization :: "nat => nat multiset" 
138 
where 

31719  139 
"multiset_prime_factorization n == 
140 
if n > 0 then (THE M. ((ALL p : set_of M. prime p) & 

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

142 
else {#}" 

143 

144 
lemma multiset_prime_factorization: "n > 0 ==> 

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

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

147 
apply (unfold multiset_prime_factorization_def) 

148 
apply clarsimp 

149 
apply (frule multiset_prime_factorization_exists) 

150 
apply clarify 

151 
apply (rule theI) 

49719  152 
apply (insert multiset_prime_factorization_unique) 
153 
apply auto 

31719  154 
done 
155 

156 

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

158 

159 
class unique_factorization = 

44872  160 
fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" 
161 
and prime_factors :: "'a \<Rightarrow> 'a set" 

31719  162 

163 
(* definitions for the natural numbers *) 

164 

165 
instantiation nat :: unique_factorization 

166 
begin 

167 

44872  168 
definition multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
169 
where "multiplicity_nat p n = count (multiset_prime_factorization n) p" 

31719  170 

44872  171 
definition prime_factors_nat :: "nat \<Rightarrow> nat set" 
172 
where "prime_factors_nat n = set_of (multiset_prime_factorization n)" 

31719  173 

44872  174 
instance .. 
31719  175 

176 
end 

177 

178 
(* definitions for the integers *) 

179 

180 
instantiation int :: unique_factorization 

181 
begin 

182 

44872  183 
definition multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat" 
184 
where "multiplicity_int p n = multiplicity (nat p) (nat n)" 

31719  185 

44872  186 
definition prime_factors_int :: "int \<Rightarrow> int set" 
187 
where "prime_factors_int n = int ` (prime_factors (nat n))" 

31719  188 

44872  189 
instance .. 
31719  190 

191 
end 

192 

193 

194 
subsection {* Set up transfer *} 

195 

44872  196 
lemma transfer_nat_int_prime_factors: "prime_factors (nat n) = nat ` prime_factors n" 
197 
unfolding prime_factors_int_def 

198 
apply auto 

199 
apply (subst transfer_int_nat_set_return_embed) 

200 
apply assumption 

201 
done 

31719  202 

44872  203 
lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow> nat_set (prime_factors n)" 
31719  204 
by (auto simp add: nat_set_def prime_factors_int_def) 
205 

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

44872  207 
multiplicity (nat p) (nat n) = multiplicity p n" 
31719  208 
by (auto simp add: multiplicity_int_def) 
209 

35644  210 
declare transfer_morphism_nat_int[transfer add return: 
31719  211 
transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure 
212 
transfer_nat_int_multiplicity] 

213 

214 

44872  215 
lemma transfer_int_nat_prime_factors: "prime_factors (int n) = int ` prime_factors n" 
31719  216 
unfolding prime_factors_int_def by auto 
217 

218 
lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> 

219 
nat_set (prime_factors n)" 

220 
by (simp only: transfer_nat_int_prime_factors_closure is_nat_def) 

221 

222 
lemma transfer_int_nat_multiplicity: 

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

224 
by (auto simp add: multiplicity_int_def) 

225 

35644  226 
declare transfer_morphism_int_nat[transfer add return: 
31719  227 
transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure 
228 
transfer_int_nat_multiplicity] 

229 

230 

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

232 

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

233 
lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0" 
44872  234 
unfolding prime_factors_int_def by auto 
31719  235 

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

236 
lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p" 
44872  237 
apply (cases "n = 0") 
31719  238 
apply (simp add: prime_factors_nat_def multiset_prime_factorization_def) 
239 
apply (auto simp add: prime_factors_nat_def multiset_prime_factorization) 

41541  240 
done 
31719  241 

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

242 
lemma prime_factors_prime_int [intro]: 
31719  243 
assumes "n >= 0" and "p : prime_factors (n::int)" 
244 
shows "prime p" 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

245 
apply (rule prime_factors_prime_nat [transferred, of n p, simplified]) 
41541  246 
using assms apply auto 
247 
done 

31719  248 

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

249 
lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)" 
44872  250 
apply (frule prime_factors_prime_nat) 
251 
apply auto 

252 
done 

31719  253 

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

254 
lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow> 
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

255 
int p > (0::int)" 
44872  256 
apply auto 
257 
done 

31719  258 

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

259 
lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))" 
44872  260 
unfolding prime_factors_nat_def by auto 
31719  261 

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

262 
lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))" 
44872  263 
unfolding prime_factors_int_def by auto 
31719  264 

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

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

268 

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

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

272 
apply (subst prime_factors_altdef_nat) 
31719  273 
apply (auto simp add: image_def) 
41541  274 
done 
31719  275 

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

276 
lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow> 
31719  277 
n = (PROD p : prime_factors n. p^(multiplicity p n))" 
44872  278 
apply (frule multiset_prime_factorization) 
49824  279 
apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_multiplicity) 
44872  280 
done 
31719  281 

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

282 
lemma prime_factorization_int: 
31719  283 
assumes "(n::int) > 0" 
284 
shows "n = (PROD p : prime_factors n. p^(multiplicity p n))" 

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

285 
apply (rule prime_factorization_nat [transferred, of n]) 
41541  286 
using assms apply auto 
287 
done 

31719  288 

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

289 
lemma prime_factorization_unique_nat: 
49718  290 
fixes f :: "nat \<Rightarrow> _" 
291 
assumes S_eq: "S = {p. 0 < f p}" and "finite S" 

292 
and "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)" 

293 
shows "S = prime_factors n \<and> (\<forall>p. f p = multiplicity p n)" 

294 
proof  

295 
from assms have "f \<in> multiset" 

296 
by (auto simp add: multiset_def) 

297 
moreover from assms have "n > 0" by force 

298 
ultimately have "multiset_prime_factorization n = Abs_multiset f" 

299 
apply (unfold multiset_prime_factorization_def) 

300 
apply (subst if_P, assumption) 

301 
apply (rule the1_equality) 

302 
apply (rule ex_ex1I) 

303 
apply (rule multiset_prime_factorization_exists, assumption) 

304 
apply (rule multiset_prime_factorization_unique) 

305 
apply force 

306 
apply force 

307 
apply force 

308 
using assms 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

309 
apply (simp add: set_of_def msetprod_multiplicity) 
49718  310 
done 
311 
with `f \<in> multiset` have "count (multiset_prime_factorization n) = f" 

312 
by (simp add: Abs_multiset_inverse) 

313 
with S_eq show ?thesis 

314 
by (simp add: set_of_def multiset_def prime_factors_nat_def multiplicity_nat_def) 

315 
qed 

31719  316 

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

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

44872  320 
apply (rule prime_factorization_unique_nat [THEN conjunct1, symmetric]) 
321 
apply assumption+ 

322 
done 

31719  323 

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

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

327 
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

328 
apply (rule prime_factors_characterization_nat) 
31719  329 
apply auto 
44872  330 
done 
31719  331 

332 
(* A minor glitch:*) 

333 

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

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

337 

338 
(* 

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

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

341 
*) 

342 

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

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

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

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

348 

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

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

352 
apply auto 

44872  353 
done 
31719  354 

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

355 
lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

356 
finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow> 
31719  357 
prime_factors n = S" 
358 
apply simp 

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

360 
apply (simp only:) 

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

361 
apply (subst primes_characterization'_int) 
31719  362 
apply auto 
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

363 
apply (metis nat_int) 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

364 
apply (metis le_cases nat_le_0 zero_not_prime_nat) 
44872  365 
done 
31719  366 

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

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

44872  370 
apply (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, symmetric]) 
371 
apply auto 

372 
done 

31719  373 

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

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

44872  377 
apply (intro impI) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

378 
apply (rule multiplicity_characterization_nat) 
31719  379 
apply auto 
44872  380 
done 
31719  381 

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

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

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

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

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

389 
apply auto 

44872  390 
done 
31719  391 

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

392 
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

393 
finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow> 
31719  394 
p >= 0 \<Longrightarrow> multiplicity p n = f p" 
395 
apply simp 

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

397 
apply (simp only:) 

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

398 
apply (subst multiplicity_characterization'_int) 
31719  399 
apply auto 
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

400 
apply (metis nat_int) 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

401 
apply (metis le_cases nat_le_0 zero_not_prime_nat) 
44872  402 
done 
31719  403 

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

404 
lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0" 
31719  405 
by (simp add: multiplicity_nat_def multiset_prime_factorization_def) 
406 

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

407 
lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0" 
31719  408 
by (simp add: multiplicity_int_def) 
409 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

410 
lemma multiplicity_one_nat': "multiplicity p (1::nat) = 0" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

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

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

413 
lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0" 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

414 
by (metis One_nat_def multiplicity_one_nat') 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

415 

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

416 
lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

417 
by (metis multiplicity_int_def multiplicity_one_nat' transfer_nat_int_numerals(2)) 
31719  418 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

419 
lemma multiplicity_prime_nat [simp]: "prime p \<Longrightarrow> multiplicity p p = 1" 
44872  420 
apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then 1 else 0)"]) 
31719  421 
apply auto 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

422 
by (metis (full_types) less_not_refl) 
31719  423 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

424 
lemma multiplicity_prime_power_nat [simp]: "prime p \<Longrightarrow> multiplicity p (p^n) = n" 
44872  425 
apply (cases "n = 0") 
31719  426 
apply auto 
44872  427 
apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then n else 0)"]) 
31719  428 
apply auto 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

429 
by (metis (full_types) less_not_refl) 
31719  430 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

431 
lemma multiplicity_prime_power_int [simp]: "prime p \<Longrightarrow> multiplicity p ( (int p)^n) = n" 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

432 
by (metis multiplicity_prime_power_nat of_nat_power transfer_int_nat_multiplicity) 
31719  433 

44872  434 
lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> multiplicity p n = 0" 
435 
apply (cases "n = 0") 

31719  436 
apply auto 
437 
apply (frule multiset_prime_factorization) 

438 
apply (auto simp add: set_of_def multiplicity_nat_def) 

44872  439 
done 
31719  440 

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

441 
lemma multiplicity_not_factor_nat [simp]: 
31719  442 
"p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0" 
44872  443 
apply (subst (asm) prime_factors_altdef_nat) 
444 
apply auto 

445 
done 

31719  446 

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

447 
lemma multiplicity_not_factor_int [simp]: 
31719  448 
"p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0" 
44872  449 
apply (subst (asm) prime_factors_altdef_int) 
450 
apply auto 

451 
done 

31719  452 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

453 
(*FIXME: messy*) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

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

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

458 
apply (simp only: prime_factors_altdef_nat) 
31719  459 
apply auto 
460 
apply (subst power_add) 

57418  461 
apply (subst setprod.distrib) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

462 
apply (rule arg_cong2 [where f = "\<lambda>x y. x*y"]) 
31719  463 
apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors k Un 
464 
(prime_factors l  prime_factors k)") 

465 
apply (erule ssubst) 

57418  466 
apply (subst setprod.union_disjoint) 
31719  467 
apply auto 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

468 
apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const) 
31719  469 
apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un 
470 
(prime_factors k  prime_factors l)") 

471 
apply (erule ssubst) 

57418  472 
apply (subst setprod.union_disjoint) 
31719  473 
apply auto 
474 
apply (subgoal_tac "(\<Prod>p\<in>prime_factors k  prime_factors l. p ^ multiplicity p l) = 

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

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

476 
apply auto 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

477 
apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const) 
44872  478 
done 
31719  479 

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

481 
choice of rules. *) 

482 

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

483 
lemma multiplicity_product_aux_int: 
31719  484 
assumes "(k::int) > 0" and "l > 0" 
485 
shows 

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

487 
(ALL p >= 0. 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

488 
apply (rule multiplicity_product_aux_nat [transferred, of l k]) 
41541  489 
using assms apply auto 
490 
done 

31719  491 

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

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

494 
by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric]) 
31719  495 

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

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

498 
by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric]) 
31719  499 

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

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

502 
by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, 
31719  503 
symmetric]) 
504 

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

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

507 
by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, 
31719  508 
symmetric]) 
509 

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

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

513 
apply (induct set: finite) 

514 
apply auto 

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

515 
apply (subst multiplicity_product_nat) 
31719  516 
apply auto 
44872  517 
done 
31719  518 

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

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

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

522 
product. 

523 

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

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

526 
*) 

527 

528 
lemma transfer_nat_int_sum_prod_closure3: 

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

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

531 
apply (rule setsum_nonneg, auto) 

532 
apply (rule setprod_nonneg, auto) 

44872  533 
done 
31719  534 

35644  535 
declare transfer_morphism_nat_int[transfer 
31719  536 
add return: transfer_nat_int_sum_prod_closure3 
537 
del: transfer_nat_int_sum_prod2 (1)] 

538 

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

539 
lemma multiplicity_setprod_int: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow> 
31719  540 
(ALL x : S. f x > 0) \<Longrightarrow> 
541 
multiplicity (p::int) (PROD x : S. f x) = 

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

543 

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

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

547 
apply auto 

57418  548 
apply (subst (asm) setprod.cong) 
31719  549 
apply (rule refl) 
550 
apply (rule if_P) 

551 
apply auto 

57418  552 
apply (rule setsum.cong) 
31719  553 
apply auto 
44872  554 
done 
31719  555 

35644  556 
declare transfer_morphism_nat_int[transfer 
31719  557 
add return: transfer_nat_int_sum_prod2 (1)] 
558 

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

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

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

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

564 
apply (erule ssubst) 

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

565 
apply (subst multiplicity_characterization_nat) 
31719  566 
prefer 5 apply (rule refl) 
567 
apply (rule refl) 

568 
apply auto 

57418  569 
apply (subst setprod.mono_neutral_right) 
31719  570 
apply assumption 
571 
prefer 3 

57418  572 
apply (rule setprod.cong) 
31719  573 
apply (rule refl) 
574 
apply auto 

575 
done 

576 

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

578 

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

579 
lemma multiplicity_prod_prime_powers_int: 
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

580 
"(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow> 
31719  581 
multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)" 
582 
apply (subgoal_tac "int ` nat ` S = S") 

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

583 
apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)" 
31719  584 
and S = "nat ` S", transferred]) 
585 
apply auto 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

586 
apply (metis linear nat_0_iff zero_not_prime_nat) 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

587 
apply (metis (full_types) image_iff int_nat_eq less_le less_linear nat_0_iff zero_not_prime_nat) 
44872  588 
done 
31719  589 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

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

593 
apply (erule ssubst) 

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

594 
apply (subst multiplicity_prod_prime_powers_nat) 
31719  595 
apply auto 
44872  596 
done 
31719  597 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

598 
lemma multiplicity_distinct_prime_power_int: "prime p \<Longrightarrow> prime q \<Longrightarrow> 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

599 
p ~= q \<Longrightarrow> multiplicity p (int q ^ n) = 0" 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

600 
by (metis multiplicity_distinct_prime_power_nat of_nat_power transfer_int_nat_multiplicity) 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

601 

31719  602 

44872  603 
lemma dvd_multiplicity_nat: 
31719  604 
"(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y" 
44872  605 
apply (cases "x = 0") 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

606 
apply (auto simp add: dvd_def multiplicity_product_nat) 
44872  607 
done 
31719  608 

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

609 
lemma dvd_multiplicity_int: 
31719  610 
"(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow> 
611 
multiplicity p x <= multiplicity p y" 

44872  612 
apply (cases "x = 0") 
31719  613 
apply (auto simp add: dvd_def) 
614 
apply (subgoal_tac "0 < k") 

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

615 
apply (auto simp add: multiplicity_product_int) 
31719  616 
apply (erule zero_less_mult_pos) 
617 
apply arith 

44872  618 
done 
31719  619 

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

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

622 
apply (simp only: prime_factors_altdef_nat) 
31719  623 
apply auto 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

624 
apply (metis dvd_multiplicity_nat le_0_eq neq0_conv) 
44872  625 
done 
31719  626 

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

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

629 
apply (auto simp add: prime_factors_altdef_int) 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset

630 
apply (metis dvd_multiplicity_int le_0_eq neq0_conv) 
44872  631 
done 
31719  632 

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

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

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

636 
apply (subst prime_factorization_nat [of y], assumption) 
31719  637 
apply (rule setprod_dvd_setprod_subset2) 
638 
apply force 

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

639 
apply (subst prime_factors_altdef_nat)+ 
31719  640 
apply auto 
40461  641 
apply (metis gr0I le_0_eq less_not_refl) 
642 
apply (metis le_imp_power_dvd) 

44872  643 
done 
31719  644 

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

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

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

648 
apply (subst prime_factorization_int [of y], assumption) 
31719  649 
apply (rule setprod_dvd_setprod_subset2) 
650 
apply force 

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

651 
apply (subst prime_factors_altdef_int)+ 
31719  652 
apply auto 
40461  653 
apply (metis le_imp_power_dvd prime_factors_ge_0_int) 
44872  654 
done 
31719  655 

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

656 
lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow> 
31719  657 
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y" 
44872  658 
by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat 
659 
multiplicity_nonprime_nat neq0_conv) 

31719  660 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

661 
lemma multiplicity_dvd'_int: 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

662 
fixes x::int and y::int 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

663 
shows "0 < x \<Longrightarrow> 0 <= y \<Longrightarrow> 
31719  664 
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y" 
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

665 
by (metis GCD.dvd_int_iff abs_int_eq multiplicity_dvd'_nat multiplicity_int_def nat_int 
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

666 
zero_le_imp_eq_int zero_less_imp_eq_int) 
31719  667 

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

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

670 
by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat) 
31719  671 

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

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

674 
by (auto intro: dvd_multiplicity_int multiplicity_dvd_int) 
31719  675 

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

676 
lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow> 
31719  677 
(p : prime_factors n) = (prime p & p dvd n)" 
44872  678 
apply (cases "prime p") 
31719  679 
apply auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

680 
apply (subst prime_factorization_nat [where n = n], assumption) 
31719  681 
apply (rule dvd_trans) 
682 
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

683 
apply (subst (asm) prime_factors_altdef_nat, force) 
31719  684 
apply (rule dvd_setprod) 
685 
apply auto 

40461  686 
apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat) 
44872  687 
done 
31719  688 

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

689 
lemma prime_factors_altdef2_int: 
31719  690 
assumes "(n::int) > 0" 
691 
shows "(p : prime_factors n) = (prime p & p dvd n)" 

55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

692 
using assms by (simp add: prime_factors_altdef2_nat [transferred]) 
31719  693 

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

694 
lemma multiplicity_eq_nat: 
31719  695 
fixes x and y::nat 
696 
assumes [arith]: "x > 0" "y > 0" and 

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

698 
shows "x = y" 

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

700 
apply (auto intro: multiplicity_dvd'_nat) 
44872  701 
done 
31719  702 

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

703 
lemma multiplicity_eq_int: 
31719  704 
fixes x and y::int 
705 
assumes [arith]: "x > 0" "y > 0" and 

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

707 
shows "x = y" 

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

709 
apply (auto intro: multiplicity_dvd'_int) 
44872  710 
done 
31719  711 

712 

713 
subsection {* An application *} 

714 

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

715 
lemma gcd_eq_nat: 
31719  716 
assumes pos [arith]: "x > 0" "y > 0" 
717 
shows "gcd (x::nat) y = 

718 
(PROD p: prime_factors x Un prime_factors y. 

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

720 
proof  

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

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

723 
have [arith]: "z > 0" 

724 
unfolding z_def by (rule setprod_pos_nat, auto) 

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

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

727 
unfolding z_def 

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

728 
apply (subst multiplicity_prod_prime_powers_nat) 
41541  729 
apply auto 
31719  730 
done 
731 
have "z dvd x" 

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

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

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

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

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

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

739 
apply (auto intro: dvd_multiplicity_nat simp add: aux) 
31719  740 
done 
741 
ultimately have "z = gcd x y" 

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

742 
by (subst gcd_unique_nat [symmetric], blast) 
44872  743 
then show ?thesis 
31719  744 
unfolding z_def by auto 
745 
qed 

746 

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

747 
lemma lcm_eq_nat: 
31719  748 
assumes pos [arith]: "x > 0" "y > 0" 
749 
shows "lcm (x::nat) y = 

750 
(PROD p: prime_factors x Un prime_factors y. 

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

752 
proof  

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

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

755 
have [arith]: "z > 0" 

756 
unfolding z_def by (rule setprod_pos_nat, auto) 

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

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

759 
unfolding z_def 

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

760 
apply (subst multiplicity_prod_prime_powers_nat) 
41541  761 
apply auto 
31719  762 
done 
763 
have "x dvd z" 

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

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

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

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

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

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

771 
apply (auto intro: dvd_multiplicity_nat simp add: aux) 
31719  772 
done 
773 
ultimately have "z = lcm x y" 

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

774 
by (subst lcm_unique_nat [symmetric], blast) 
44872  775 
then show ?thesis 
31719  776 
unfolding z_def by auto 
777 
qed 

778 

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

779 
lemma multiplicity_gcd_nat: 
31719  780 
assumes [arith]: "x > 0" "y > 0" 
44872  781 
shows "multiplicity (p::nat) (gcd x y) = min (multiplicity p x) (multiplicity p y)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

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

784 
apply (subst multiplicity_prod_prime_powers_nat) 
31719  785 
apply auto 
44872  786 
done 
31719  787 

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

788 
lemma multiplicity_lcm_nat: 
31719  789 
assumes [arith]: "x > 0" "y > 0" 
44872  790 
shows "multiplicity (p::nat) (lcm x y) = max (multiplicity p x) (multiplicity p y)" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

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

793 
apply (subst multiplicity_prod_prime_powers_nat) 
31719  794 
apply auto 
44872  795 
done 
31719  796 

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

797 
lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)" 
44872  798 
apply (cases "x = 0  y = 0  z = 0") 
31719  799 
apply auto 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

800 
apply (rule multiplicity_eq_nat) 
44872  801 
apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat lcm_pos_nat) 
802 
done 

31719  803 

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

804 
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

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

806 
apply (subst lcm_abs_int) 
31719  807 
apply (subst (2) abs_of_nonneg) 
808 
apply force 

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

809 
apply (rule gcd_lcm_distrib_nat [transferred]) 
31719  810 
apply auto 
44872  811 
done 
31719  812 

813 
end 

49718  814 