author | wenzelm |
Mon, 08 Feb 2010 21:28:27 +0100 | |
changeset 35054 | a5db9779b026 |
parent 34947 | e1b8f2736404 |
child 35416 | d8d7d1b785af |
permissions | -rw-r--r-- |
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 intro-rule; needed only once and might get in the way *) |
|
61 |
lemma multiset_eqI: "[| !!x. count M x = count N x |] ==> M = N" |
|
62 |
by (subst multiset_eq_conv_count_eq, blast) |
|
63 |
||
64 |
(* Here is a version of set product for multisets. Is it worth moving |
|
65 |
to multiset.thy? If so, one should similarly define msetsum for abelian |
|
66 |
semirings, using of_nat. Also, is it worth developing bounded quantifiers |
|
67 |
"ALL i :# M. P i"? |
|
68 |
*) |
|
69 |
||
70 |
constdefs |
|
71 |
msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b" |
|
72 |
"msetprod f M == setprod (%x. (f x)^(count M x)) (set_of M)" |
|
73 |
||
74 |
syntax |
|
75 |
"_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" |
|
76 |
("(3PROD _:#_. _)" [0, 51, 10] 10) |
|
77 |
||
78 |
translations |
|
35054 | 79 |
"PROD i :# A. b" == "CONST msetprod (%i. b) A" |
31719 | 80 |
|
81 |
lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" |
|
82 |
apply (simp add: msetprod_def power_add) |
|
83 |
apply (subst setprod_Un2) |
|
84 |
apply auto |
|
85 |
apply (subgoal_tac |
|
86 |
"(PROD x:set_of A - set_of B. f x ^ count A x * f x ^ count B x) = |
|
87 |
(PROD x:set_of A - set_of B. f x ^ count A x)") |
|
88 |
apply (erule ssubst) |
|
89 |
apply (subgoal_tac |
|
90 |
"(PROD x:set_of B - set_of A. f x ^ count A x * f x ^ count B x) = |
|
91 |
(PROD x:set_of B - set_of A. f x ^ count B x)") |
|
92 |
apply (erule ssubst) |
|
93 |
apply (subgoal_tac "(PROD x:set_of A. f x ^ count A x) = |
|
94 |
(PROD x:set_of A - set_of B. f x ^ count A x) * |
|
95 |
(PROD x:set_of A Int set_of B. f x ^ count A x)") |
|
96 |
apply (erule ssubst) |
|
97 |
apply (subgoal_tac "(PROD x:set_of B. f x ^ count B x) = |
|
98 |
(PROD x:set_of B - set_of A. f x ^ count B x) * |
|
99 |
(PROD x:set_of A Int set_of B. f x ^ count B x)") |
|
100 |
apply (erule ssubst) |
|
101 |
apply (subst setprod_timesf) |
|
102 |
apply (force simp add: mult_ac) |
|
103 |
apply (subst setprod_Un_disjoint [symmetric]) |
|
104 |
apply (auto intro: setprod_cong) |
|
105 |
apply (subst setprod_Un_disjoint [symmetric]) |
|
106 |
apply (auto intro: setprod_cong) |
|
107 |
done |
|
108 |
||
109 |
||
110 |
subsection {* unique factorization: multiset version *} |
|
111 |
||
112 |
lemma multiset_prime_factorization_exists [rule_format]: "n > 0 --> |
|
113 |
(EX M. (ALL (p::nat) : set_of M. prime p) & n = (PROD i :# M. i))" |
|
114 |
proof (rule nat_less_induct, clarify) |
|
115 |
fix n :: nat |
|
116 |
assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_of M. prime p) & m = |
|
117 |
(PROD i :# M. i))" |
|
118 |
assume "(n::nat) > 0" |
|
119 |
then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)" |
|
120 |
by arith |
|
121 |
moreover |
|
122 |
{ |
|
123 |
assume "n = 1" |
|
124 |
then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)" |
|
125 |
by (auto simp add: msetprod_def) |
|
126 |
} |
|
127 |
moreover |
|
128 |
{ |
|
129 |
assume "n > 1" and "prime n" |
|
130 |
then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)" |
|
131 |
by (auto simp add: msetprod_def) |
|
132 |
} |
|
133 |
moreover |
|
134 |
{ |
|
135 |
assume "n > 1" and "~ prime n" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
136 |
from prems not_prime_eq_prod_nat |
31719 | 137 |
obtain m k where "n = m * k & 1 < m & m < n & 1 < k & k < n" |
138 |
by blast |
|
139 |
with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)" |
|
140 |
and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)" |
|
141 |
by blast |
|
142 |
hence "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)" |
|
143 |
by (auto simp add: prems msetprod_Un set_of_union) |
|
144 |
then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)".. |
|
145 |
} |
|
146 |
ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)" |
|
147 |
by blast |
|
148 |
qed |
|
149 |
||
150 |
lemma multiset_prime_factorization_unique_aux: |
|
151 |
fixes a :: nat |
|
152 |
assumes "(ALL p : set_of M. prime p)" and |
|
153 |
"(ALL p : set_of N. prime p)" and |
|
154 |
"(PROD i :# M. i) dvd (PROD i:# N. i)" |
|
155 |
shows |
|
156 |
"count M a <= count N a" |
|
157 |
proof cases |
|
158 |
assume "a : set_of M" |
|
159 |
with prems have a: "prime a" |
|
160 |
by auto |
|
161 |
with prems have "a ^ count M a dvd (PROD i :# M. i)" |
|
162 |
by (auto intro: dvd_setprod simp add: msetprod_def) |
|
163 |
also have "... dvd (PROD i :# N. i)" |
|
164 |
by (rule prems) |
|
165 |
also have "... = (PROD i : (set_of N). i ^ (count N i))" |
|
166 |
by (simp add: msetprod_def) |
|
167 |
also have "... = |
|
168 |
a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))" |
|
169 |
proof (cases) |
|
170 |
assume "a : set_of N" |
|
171 |
hence b: "set_of N = {a} Un (set_of N - {a})" |
|
172 |
by auto |
|
173 |
thus ?thesis |
|
174 |
by (subst (1) b, subst setprod_Un_disjoint, auto) |
|
175 |
next |
|
176 |
assume "a ~: set_of N" |
|
177 |
thus ?thesis |
|
178 |
by auto |
|
179 |
qed |
|
180 |
finally have "a ^ count M a dvd |
|
181 |
a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))". |
|
182 |
moreover have "coprime (a ^ count M a) |
|
183 |
(PROD i : (set_of N - {a}). i ^ (count N i))" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
184 |
apply (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
185 |
apply (rule setprod_coprime_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
186 |
apply (rule primes_imp_powers_coprime_nat) |
31719 | 187 |
apply (insert prems, auto) |
188 |
done |
|
189 |
ultimately have "a ^ count M a dvd a^(count N a)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
190 |
by (elim coprime_dvd_mult_nat) |
31719 | 191 |
with a show ?thesis |
192 |
by (intro power_dvd_imp_le, auto) |
|
193 |
next |
|
194 |
assume "a ~: set_of M" |
|
195 |
thus ?thesis by auto |
|
196 |
qed |
|
197 |
||
198 |
lemma multiset_prime_factorization_unique: |
|
199 |
assumes "(ALL (p::nat) : set_of M. prime p)" and |
|
200 |
"(ALL p : set_of N. prime p)" and |
|
201 |
"(PROD i :# M. i) = (PROD i:# N. i)" |
|
202 |
shows |
|
203 |
"M = N" |
|
204 |
proof - |
|
205 |
{ |
|
206 |
fix a |
|
207 |
from prems have "count M a <= count N a" |
|
208 |
by (intro multiset_prime_factorization_unique_aux, auto) |
|
209 |
moreover from prems have "count N a <= count M a" |
|
210 |
by (intro multiset_prime_factorization_unique_aux, auto) |
|
211 |
ultimately have "count M a = count N a" |
|
212 |
by auto |
|
213 |
} |
|
214 |
thus ?thesis by (simp add:multiset_eq_conv_count_eq) |
|
215 |
qed |
|
216 |
||
217 |
constdefs |
|
218 |
multiset_prime_factorization :: "nat => nat multiset" |
|
219 |
"multiset_prime_factorization n == |
|
220 |
if n > 0 then (THE M. ((ALL p : set_of M. prime p) & |
|
221 |
n = (PROD i :# M. i))) |
|
222 |
else {#}" |
|
223 |
||
224 |
lemma multiset_prime_factorization: "n > 0 ==> |
|
225 |
(ALL p : set_of (multiset_prime_factorization n). prime p) & |
|
226 |
n = (PROD i :# (multiset_prime_factorization n). i)" |
|
227 |
apply (unfold multiset_prime_factorization_def) |
|
228 |
apply clarsimp |
|
229 |
apply (frule multiset_prime_factorization_exists) |
|
230 |
apply clarify |
|
231 |
apply (rule theI) |
|
232 |
apply (insert multiset_prime_factorization_unique, blast)+ |
|
233 |
done |
|
234 |
||
235 |
||
236 |
subsection {* Prime factors and multiplicity for nats and ints *} |
|
237 |
||
238 |
class unique_factorization = |
|
239 |
||
240 |
fixes |
|
241 |
multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" and |
|
242 |
prime_factors :: "'a \<Rightarrow> 'a set" |
|
243 |
||
244 |
(* definitions for the natural numbers *) |
|
245 |
||
246 |
instantiation nat :: unique_factorization |
|
247 |
||
248 |
begin |
|
249 |
||
250 |
definition |
|
251 |
multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
252 |
where |
|
253 |
"multiplicity_nat p n = count (multiset_prime_factorization n) p" |
|
254 |
||
255 |
definition |
|
256 |
prime_factors_nat :: "nat \<Rightarrow> nat set" |
|
257 |
where |
|
258 |
"prime_factors_nat n = set_of (multiset_prime_factorization n)" |
|
259 |
||
260 |
instance proof qed |
|
261 |
||
262 |
end |
|
263 |
||
264 |
(* definitions for the integers *) |
|
265 |
||
266 |
instantiation int :: unique_factorization |
|
267 |
||
268 |
begin |
|
269 |
||
270 |
definition |
|
271 |
multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat" |
|
272 |
where |
|
273 |
"multiplicity_int p n = multiplicity (nat p) (nat n)" |
|
274 |
||
275 |
definition |
|
276 |
prime_factors_int :: "int \<Rightarrow> int set" |
|
277 |
where |
|
278 |
"prime_factors_int n = int ` (prime_factors (nat n))" |
|
279 |
||
280 |
instance proof qed |
|
281 |
||
282 |
end |
|
283 |
||
284 |
||
285 |
subsection {* Set up transfer *} |
|
286 |
||
287 |
lemma transfer_nat_int_prime_factors: |
|
288 |
"prime_factors (nat n) = nat ` prime_factors n" |
|
289 |
unfolding prime_factors_int_def apply auto |
|
290 |
by (subst transfer_int_nat_set_return_embed, assumption) |
|
291 |
||
292 |
lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow> |
|
293 |
nat_set (prime_factors n)" |
|
294 |
by (auto simp add: nat_set_def prime_factors_int_def) |
|
295 |
||
296 |
lemma transfer_nat_int_multiplicity: "p >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow> |
|
297 |
multiplicity (nat p) (nat n) = multiplicity p n" |
|
298 |
by (auto simp add: multiplicity_int_def) |
|
299 |
||
300 |
declare TransferMorphism_nat_int[transfer add return: |
|
301 |
transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure |
|
302 |
transfer_nat_int_multiplicity] |
|
303 |
||
304 |
||
305 |
lemma transfer_int_nat_prime_factors: |
|
306 |
"prime_factors (int n) = int ` prime_factors n" |
|
307 |
unfolding prime_factors_int_def by auto |
|
308 |
||
309 |
lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> |
|
310 |
nat_set (prime_factors n)" |
|
311 |
by (simp only: transfer_nat_int_prime_factors_closure is_nat_def) |
|
312 |
||
313 |
lemma transfer_int_nat_multiplicity: |
|
314 |
"multiplicity (int p) (int n) = multiplicity p n" |
|
315 |
by (auto simp add: multiplicity_int_def) |
|
316 |
||
317 |
declare TransferMorphism_int_nat[transfer add return: |
|
318 |
transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure |
|
319 |
transfer_int_nat_multiplicity] |
|
320 |
||
321 |
||
322 |
subsection {* Properties of prime factors and multiplicity for nats and ints *} |
|
323 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
324 |
lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0" |
31719 | 325 |
by (unfold prime_factors_int_def, auto) |
326 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
327 |
lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p" |
31719 | 328 |
apply (case_tac "n = 0") |
329 |
apply (simp add: prime_factors_nat_def multiset_prime_factorization_def) |
|
330 |
apply (auto simp add: prime_factors_nat_def multiset_prime_factorization) |
|
331 |
done |
|
332 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
333 |
lemma prime_factors_prime_int [intro]: |
31719 | 334 |
assumes "n >= 0" and "p : prime_factors (n::int)" |
335 |
shows "prime p" |
|
336 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
337 |
apply (rule prime_factors_prime_nat [transferred, of n p]) |
31719 | 338 |
using prems apply auto |
339 |
done |
|
340 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
341 |
lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
342 |
by (frule prime_factors_prime_nat, auto) |
31719 | 343 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
344 |
lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow> |
31719 | 345 |
p > (0::int)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
346 |
by (frule (1) prime_factors_prime_int, auto) |
31719 | 347 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
348 |
lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))" |
31719 | 349 |
by (unfold prime_factors_nat_def, auto) |
350 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
351 |
lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))" |
31719 | 352 |
by (unfold prime_factors_int_def, auto) |
353 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
354 |
lemma prime_factors_altdef_nat: "prime_factors (n::nat) = |
31719 | 355 |
{p. multiplicity p n > 0}" |
356 |
by (force simp add: prime_factors_nat_def multiplicity_nat_def) |
|
357 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
358 |
lemma prime_factors_altdef_int: "prime_factors (n::int) = |
31719 | 359 |
{p. p >= 0 & multiplicity p n > 0}" |
360 |
apply (unfold prime_factors_int_def multiplicity_int_def) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
361 |
apply (subst prime_factors_altdef_nat) |
31719 | 362 |
apply (auto simp add: image_def) |
363 |
done |
|
364 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
365 |
lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow> |
31719 | 366 |
n = (PROD p : prime_factors n. p^(multiplicity p n))" |
367 |
by (frule multiset_prime_factorization, |
|
368 |
simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def) |
|
369 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
370 |
thm prime_factorization_nat [transferred] |
31719 | 371 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
372 |
lemma prime_factorization_int: |
31719 | 373 |
assumes "(n::int) > 0" |
374 |
shows "n = (PROD p : prime_factors n. p^(multiplicity p n))" |
|
375 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
376 |
apply (rule prime_factorization_nat [transferred, of n]) |
31719 | 377 |
using prems apply auto |
378 |
done |
|
379 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
380 |
lemma neq_zero_eq_gt_zero_nat: "((x::nat) ~= 0) = (x > 0)" |
31719 | 381 |
by auto |
382 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
383 |
lemma prime_factorization_unique_nat: |
31719 | 384 |
"S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow> |
385 |
n = (PROD p : S. p^(f p)) \<Longrightarrow> |
|
386 |
S = prime_factors n & (ALL p. f p = multiplicity p n)" |
|
387 |
apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset |
|
388 |
f") |
|
389 |
apply (unfold prime_factors_nat_def multiplicity_nat_def) |
|
34947 | 390 |
apply (simp add: set_of_def Abs_multiset_inverse multiset_def) |
31719 | 391 |
apply (unfold multiset_prime_factorization_def) |
392 |
apply (subgoal_tac "n > 0") |
|
393 |
prefer 2 |
|
394 |
apply force |
|
395 |
apply (subst if_P, assumption) |
|
396 |
apply (rule the1_equality) |
|
397 |
apply (rule ex_ex1I) |
|
398 |
apply (rule multiset_prime_factorization_exists, assumption) |
|
399 |
apply (rule multiset_prime_factorization_unique) |
|
400 |
apply force |
|
401 |
apply force |
|
402 |
apply force |
|
34947 | 403 |
unfolding set_of_def msetprod_def |
31719 | 404 |
apply (subgoal_tac "f : multiset") |
405 |
apply (auto simp only: Abs_multiset_inverse) |
|
406 |
unfolding multiset_def apply force |
|
407 |
done |
|
408 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
409 |
lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> |
31719 | 410 |
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow> |
411 |
prime_factors n = S" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
412 |
by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric], |
31719 | 413 |
assumption+) |
414 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
415 |
lemma prime_factors_characterization'_nat: |
31719 | 416 |
"finite {p. 0 < f (p::nat)} \<Longrightarrow> |
417 |
(ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> |
|
418 |
prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
419 |
apply (rule prime_factors_characterization_nat) |
31719 | 420 |
apply auto |
421 |
done |
|
422 |
||
423 |
(* A minor glitch:*) |
|
424 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
425 |
thm prime_factors_characterization'_nat |
31719 | 426 |
[where f = "%x. f (int (x::nat))", |
427 |
transferred direction: nat "op <= (0::int)", rule_format] |
|
428 |
||
429 |
(* |
|
430 |
Transfer isn't smart enough to know that the "0 < f p" should |
|
431 |
remain a comparison between nats. But the transfer still works. |
|
432 |
*) |
|
433 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
434 |
lemma primes_characterization'_int [rule_format]: |
31719 | 435 |
"finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow> |
436 |
(ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> |
|
437 |
prime_factors (PROD p | p >=0 & 0 < f p . p ^ f p) = |
|
438 |
{p. p >= 0 & 0 < f p}" |
|
439 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
440 |
apply (insert prime_factors_characterization'_nat |
31719 | 441 |
[where f = "%x. f (int (x::nat))", |
442 |
transferred direction: nat "op <= (0::int)"]) |
|
443 |
apply auto |
|
444 |
done |
|
445 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
446 |
lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> |
31719 | 447 |
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow> |
448 |
prime_factors n = S" |
|
449 |
apply simp |
|
450 |
apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}") |
|
451 |
apply (simp only:) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
452 |
apply (subst primes_characterization'_int) |
31719 | 453 |
apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
454 |
apply (auto simp add: prime_ge_0_int) |
31719 | 455 |
done |
456 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
457 |
lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> |
31719 | 458 |
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow> |
459 |
multiplicity p n = f p" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
460 |
by (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, |
31719 | 461 |
symmetric], auto) |
462 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
463 |
lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow> |
31719 | 464 |
(ALL p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> |
465 |
multiplicity p (PROD p | 0 < f p . p ^ f p) = f p" |
|
466 |
apply (rule impI)+ |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
467 |
apply (rule multiplicity_characterization_nat) |
31719 | 468 |
apply auto |
469 |
done |
|
470 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
471 |
lemma multiplicity_characterization'_int [rule_format]: |
31719 | 472 |
"finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow> |
473 |
(ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p >= 0 \<Longrightarrow> |
|
474 |
multiplicity p (PROD p | p >= 0 & 0 < f p . p ^ f p) = f p" |
|
475 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
476 |
apply (insert multiplicity_characterization'_nat |
31719 | 477 |
[where f = "%x. f (int (x::nat))", |
478 |
transferred direction: nat "op <= (0::int)", rule_format]) |
|
479 |
apply auto |
|
480 |
done |
|
481 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
482 |
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> |
31719 | 483 |
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow> |
484 |
p >= 0 \<Longrightarrow> multiplicity p n = f p" |
|
485 |
apply simp |
|
486 |
apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}") |
|
487 |
apply (simp only:) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
488 |
apply (subst multiplicity_characterization'_int) |
31719 | 489 |
apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
490 |
apply (auto simp add: prime_ge_0_int) |
31719 | 491 |
done |
492 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
493 |
lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0" |
31719 | 494 |
by (simp add: multiplicity_nat_def multiset_prime_factorization_def) |
495 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
496 |
lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0" |
31719 | 497 |
by (simp add: multiplicity_int_def) |
498 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
499 |
lemma multiplicity_one_nat [simp]: "multiplicity p (1::nat) = 0" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
500 |
by (subst multiplicity_characterization_nat [where f = "%x. 0"], auto) |
31719 | 501 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
502 |
lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0" |
31719 | 503 |
by (simp add: multiplicity_int_def) |
504 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
505 |
lemma multiplicity_prime_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
506 |
apply (subst multiplicity_characterization_nat |
31719 | 507 |
[where f = "(%q. if q = p then 1 else 0)"]) |
508 |
apply auto |
|
509 |
apply (case_tac "x = p") |
|
510 |
apply auto |
|
511 |
done |
|
512 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
513 |
lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1" |
31719 | 514 |
unfolding prime_int_def multiplicity_int_def by auto |
515 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
516 |
lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow> |
31719 | 517 |
multiplicity p (p^n) = n" |
518 |
apply (case_tac "n = 0") |
|
519 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
520 |
apply (subst multiplicity_characterization_nat |
31719 | 521 |
[where f = "(%q. if q = p then n else 0)"]) |
522 |
apply auto |
|
523 |
apply (case_tac "x = p") |
|
524 |
apply auto |
|
525 |
done |
|
526 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
527 |
lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow> |
31719 | 528 |
multiplicity p (p^n) = n" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
529 |
apply (frule prime_ge_0_int) |
31719 | 530 |
apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq) |
531 |
done |
|
532 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
533 |
lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> |
31719 | 534 |
multiplicity p n = 0" |
535 |
apply (case_tac "n = 0") |
|
536 |
apply auto |
|
537 |
apply (frule multiset_prime_factorization) |
|
538 |
apply (auto simp add: set_of_def multiplicity_nat_def) |
|
539 |
done |
|
540 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
541 |
lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0" |
31719 | 542 |
by (unfold multiplicity_int_def prime_int_def, auto) |
543 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
544 |
lemma multiplicity_not_factor_nat [simp]: |
31719 | 545 |
"p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
546 |
by (subst (asm) prime_factors_altdef_nat, auto) |
31719 | 547 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
548 |
lemma multiplicity_not_factor_int [simp]: |
31719 | 549 |
"p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
550 |
by (subst (asm) prime_factors_altdef_int, auto) |
31719 | 551 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
552 |
lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> |
31719 | 553 |
(prime_factors k) Un (prime_factors l) = prime_factors (k * l) & |
554 |
(ALL p. multiplicity p k + multiplicity p l = multiplicity p (k * l))" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
555 |
apply (rule prime_factorization_unique_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
556 |
apply (simp only: prime_factors_altdef_nat) |
31719 | 557 |
apply auto |
558 |
apply (subst power_add) |
|
559 |
apply (subst setprod_timesf) |
|
560 |
apply (rule arg_cong2)back back |
|
561 |
apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors k Un |
|
562 |
(prime_factors l - prime_factors k)") |
|
563 |
apply (erule ssubst) |
|
564 |
apply (subst setprod_Un_disjoint) |
|
565 |
apply auto |
|
566 |
apply (subgoal_tac "(\<Prod>p\<in>prime_factors l - prime_factors k. p ^ multiplicity p k) = |
|
567 |
(\<Prod>p\<in>prime_factors l - prime_factors k. 1)") |
|
568 |
apply (erule ssubst) |
|
569 |
apply (simp add: setprod_1) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
570 |
apply (erule prime_factorization_nat) |
31719 | 571 |
apply (rule setprod_cong, auto) |
572 |
apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un |
|
573 |
(prime_factors k - prime_factors l)") |
|
574 |
apply (erule ssubst) |
|
575 |
apply (subst setprod_Un_disjoint) |
|
576 |
apply auto |
|
577 |
apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) = |
|
578 |
(\<Prod>p\<in>prime_factors k - prime_factors l. 1)") |
|
579 |
apply (erule ssubst) |
|
580 |
apply (simp add: setprod_1) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
581 |
apply (erule prime_factorization_nat) |
31719 | 582 |
apply (rule setprod_cong, auto) |
583 |
done |
|
584 |
||
585 |
(* transfer doesn't have the same problem here with the right |
|
586 |
choice of rules. *) |
|
587 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
588 |
lemma multiplicity_product_aux_int: |
31719 | 589 |
assumes "(k::int) > 0" and "l > 0" |
590 |
shows |
|
591 |
"(prime_factors k) Un (prime_factors l) = prime_factors (k * l) & |
|
592 |
(ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))" |
|
593 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
594 |
apply (rule multiplicity_product_aux_nat [transferred, of l k]) |
31719 | 595 |
using prems apply auto |
596 |
done |
|
597 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
598 |
lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = |
31719 | 599 |
prime_factors k Un prime_factors l" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
600 |
by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric]) |
31719 | 601 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
602 |
lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = |
31719 | 603 |
prime_factors k Un prime_factors l" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
604 |
by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric]) |
31719 | 605 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
606 |
lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) = |
31719 | 607 |
multiplicity p k + multiplicity p l" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
608 |
by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, |
31719 | 609 |
symmetric]) |
610 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
611 |
lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow> |
31719 | 612 |
multiplicity p (k * l) = multiplicity p k + multiplicity p l" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
613 |
by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, |
31719 | 614 |
symmetric]) |
615 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
616 |
lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> (ALL x : S. f x > 0) \<Longrightarrow> |
31719 | 617 |
multiplicity (p::nat) (PROD x : S. f x) = |
618 |
(SUM x : S. multiplicity p (f x))" |
|
619 |
apply (induct set: finite) |
|
620 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
621 |
apply (subst multiplicity_product_nat) |
31719 | 622 |
apply auto |
623 |
done |
|
624 |
||
625 |
(* Transfer is delicate here for two reasons: first, because there is |
|
626 |
an implicit quantifier over functions (f), and, second, because the |
|
627 |
product over the multiplicity should not be translated to an integer |
|
628 |
product. |
|
629 |
||
630 |
The way to handle the first is to use quantifier rules for functions. |
|
631 |
The way to handle the second is to turn off the offending rule. |
|
632 |
*) |
|
633 |
||
634 |
lemma transfer_nat_int_sum_prod_closure3: |
|
635 |
"(SUM x : A. int (f x)) >= 0" |
|
636 |
"(PROD x : A. int (f x)) >= 0" |
|
637 |
apply (rule setsum_nonneg, auto) |
|
638 |
apply (rule setprod_nonneg, auto) |
|
639 |
done |
|
640 |
||
641 |
declare TransferMorphism_nat_int[transfer |
|
642 |
add return: transfer_nat_int_sum_prod_closure3 |
|
643 |
del: transfer_nat_int_sum_prod2 (1)] |
|
644 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
645 |
lemma multiplicity_setprod_int: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow> |
31719 | 646 |
(ALL x : S. f x > 0) \<Longrightarrow> |
647 |
multiplicity (p::int) (PROD x : S. f x) = |
|
648 |
(SUM x : S. multiplicity p (f x))" |
|
649 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
650 |
apply (frule multiplicity_setprod_nat |
31719 | 651 |
[where f = "%x. nat(int(nat(f x)))", |
652 |
transferred direction: nat "op <= (0::int)"]) |
|
653 |
apply auto |
|
654 |
apply (subst (asm) setprod_cong) |
|
655 |
apply (rule refl) |
|
656 |
apply (rule if_P) |
|
657 |
apply auto |
|
658 |
apply (rule setsum_cong) |
|
659 |
apply auto |
|
660 |
done |
|
661 |
||
662 |
declare TransferMorphism_nat_int[transfer |
|
663 |
add return: transfer_nat_int_sum_prod2 (1)] |
|
664 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
665 |
lemma multiplicity_prod_prime_powers_nat: |
31719 | 666 |
"finite S \<Longrightarrow> (ALL p : S. prime (p::nat)) \<Longrightarrow> |
667 |
multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)" |
|
668 |
apply (subgoal_tac "(PROD p : S. p ^ f p) = |
|
669 |
(PROD p : S. p ^ (%x. if x : S then f x else 0) p)") |
|
670 |
apply (erule ssubst) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
671 |
apply (subst multiplicity_characterization_nat) |
31719 | 672 |
prefer 5 apply (rule refl) |
673 |
apply (rule refl) |
|
674 |
apply auto |
|
675 |
apply (subst setprod_mono_one_right) |
|
676 |
apply assumption |
|
677 |
prefer 3 |
|
678 |
apply (rule setprod_cong) |
|
679 |
apply (rule refl) |
|
680 |
apply auto |
|
681 |
done |
|
682 |
||
683 |
(* Here the issue with transfer is the implicit quantifier over S *) |
|
684 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
685 |
lemma multiplicity_prod_prime_powers_int: |
31719 | 686 |
"(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow> |
687 |
multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)" |
|
688 |
||
689 |
apply (subgoal_tac "int ` nat ` S = S") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
690 |
apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)" |
31719 | 691 |
and S = "nat ` S", transferred]) |
692 |
apply auto |
|
693 |
apply (subst prime_int_def [symmetric]) |
|
694 |
apply auto |
|
695 |
apply (subgoal_tac "xb >= 0") |
|
696 |
apply force |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
697 |
apply (rule prime_ge_0_int) |
31719 | 698 |
apply force |
699 |
apply (subst transfer_nat_int_set_return_embed) |
|
700 |
apply (unfold nat_set_def, auto) |
|
701 |
done |
|
702 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
703 |
lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> |
31719 | 704 |
p ~= q \<Longrightarrow> multiplicity p (q^n) = 0" |
705 |
apply (subgoal_tac "q^n = setprod (%x. x^n) {q}") |
|
706 |
apply (erule ssubst) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
707 |
apply (subst multiplicity_prod_prime_powers_nat) |
31719 | 708 |
apply auto |
709 |
done |
|
710 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
711 |
lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> |
31719 | 712 |
p ~= q \<Longrightarrow> multiplicity p (q^n) = 0" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
713 |
apply (frule prime_ge_0_int [of q]) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
714 |
apply (frule multiplicity_distinct_prime_power_nat [transferred leaving: n]) |
31719 | 715 |
prefer 4 |
716 |
apply assumption |
|
717 |
apply auto |
|
718 |
done |
|
719 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
720 |
lemma dvd_multiplicity_nat: |
31719 | 721 |
"(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y" |
722 |
apply (case_tac "x = 0") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
723 |
apply (auto simp add: dvd_def multiplicity_product_nat) |
31719 | 724 |
done |
725 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
726 |
lemma dvd_multiplicity_int: |
31719 | 727 |
"(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow> |
728 |
multiplicity p x <= multiplicity p y" |
|
729 |
apply (case_tac "x = 0") |
|
730 |
apply (auto simp add: dvd_def) |
|
731 |
apply (subgoal_tac "0 < k") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
732 |
apply (auto simp add: multiplicity_product_int) |
31719 | 733 |
apply (erule zero_less_mult_pos) |
734 |
apply arith |
|
735 |
done |
|
736 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
737 |
lemma dvd_prime_factors_nat [intro]: |
31719 | 738 |
"0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
739 |
apply (simp only: prime_factors_altdef_nat) |
31719 | 740 |
apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
741 |
apply (frule dvd_multiplicity_nat) |
31719 | 742 |
apply auto |
743 |
(* It is a shame that auto and arith don't get this. *) |
|
744 |
apply (erule order_less_le_trans)back |
|
745 |
apply assumption |
|
746 |
done |
|
747 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
748 |
lemma dvd_prime_factors_int [intro]: |
31719 | 749 |
"0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
750 |
apply (auto simp add: prime_factors_altdef_int) |
31719 | 751 |
apply (erule order_less_le_trans) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
752 |
apply (rule dvd_multiplicity_int) |
31719 | 753 |
apply auto |
754 |
done |
|
755 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
756 |
lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> |
31719 | 757 |
ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow> |
758 |
x dvd y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
759 |
apply (subst prime_factorization_nat [of x], assumption) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
760 |
apply (subst prime_factorization_nat [of y], assumption) |
31719 | 761 |
apply (rule setprod_dvd_setprod_subset2) |
762 |
apply force |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
763 |
apply (subst prime_factors_altdef_nat)+ |
31719 | 764 |
apply auto |
765 |
(* Again, a shame that auto and arith don't get this. *) |
|
766 |
apply (drule_tac x = xa in spec, auto) |
|
767 |
apply (rule le_imp_power_dvd) |
|
768 |
apply blast |
|
769 |
done |
|
770 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
771 |
lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> |
31719 | 772 |
ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow> |
773 |
x dvd y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
774 |
apply (subst prime_factorization_int [of x], assumption) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
775 |
apply (subst prime_factorization_int [of y], assumption) |
31719 | 776 |
apply (rule setprod_dvd_setprod_subset2) |
777 |
apply force |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
778 |
apply (subst prime_factors_altdef_int)+ |
31719 | 779 |
apply auto |
780 |
apply (rule dvd_power_le) |
|
781 |
apply auto |
|
782 |
apply (drule_tac x = xa in spec) |
|
783 |
apply (erule impE) |
|
784 |
apply auto |
|
785 |
done |
|
786 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
787 |
lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow> |
31719 | 788 |
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y" |
789 |
apply (cases "y = 0") |
|
790 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
791 |
apply (rule multiplicity_dvd_nat, auto) |
31719 | 792 |
apply (case_tac "prime p") |
793 |
apply auto |
|
794 |
done |
|
795 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
796 |
lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow> |
31719 | 797 |
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y" |
798 |
apply (cases "y = 0") |
|
799 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
800 |
apply (rule multiplicity_dvd_int, auto) |
31719 | 801 |
apply (case_tac "prime p") |
802 |
apply auto |
|
803 |
done |
|
804 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
805 |
lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> |
31719 | 806 |
(x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
807 |
by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat) |
31719 | 808 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
809 |
lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> |
31719 | 810 |
(x dvd y) = (ALL p >= 0. multiplicity p x <= multiplicity p y)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
811 |
by (auto intro: dvd_multiplicity_int multiplicity_dvd_int) |
31719 | 812 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
813 |
lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow> |
31719 | 814 |
(p : prime_factors n) = (prime p & p dvd n)" |
815 |
apply (case_tac "prime p") |
|
816 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
817 |
apply (subst prime_factorization_nat [where n = n], assumption) |
31719 | 818 |
apply (rule dvd_trans) |
819 |
apply (rule dvd_power [where x = p and n = "multiplicity p n"]) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
820 |
apply (subst (asm) prime_factors_altdef_nat, force) |
31719 | 821 |
apply (rule dvd_setprod) |
822 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
823 |
apply (subst prime_factors_altdef_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
824 |
apply (subst (asm) dvd_multiplicity_eq_nat) |
31719 | 825 |
apply auto |
826 |
apply (drule spec [where x = p]) |
|
827 |
apply auto |
|
828 |
done |
|
829 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
830 |
lemma prime_factors_altdef2_int: |
31719 | 831 |
assumes "(n::int) > 0" |
832 |
shows "(p : prime_factors n) = (prime p & p dvd n)" |
|
833 |
||
834 |
apply (case_tac "p >= 0") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
835 |
apply (rule prime_factors_altdef2_nat [transferred]) |
31719 | 836 |
using prems apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
837 |
apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int) |
31719 | 838 |
done |
839 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
840 |
lemma multiplicity_eq_nat: |
31719 | 841 |
fixes x and y::nat |
842 |
assumes [arith]: "x > 0" "y > 0" and |
|
843 |
mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y" |
|
844 |
shows "x = y" |
|
845 |
||
33657 | 846 |
apply (rule dvd_antisym) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
847 |
apply (auto intro: multiplicity_dvd'_nat) |
31719 | 848 |
done |
849 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
850 |
lemma multiplicity_eq_int: |
31719 | 851 |
fixes x and y::int |
852 |
assumes [arith]: "x > 0" "y > 0" and |
|
853 |
mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y" |
|
854 |
shows "x = y" |
|
855 |
||
33657 | 856 |
apply (rule dvd_antisym [transferred]) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
857 |
apply (auto intro: multiplicity_dvd'_int) |
31719 | 858 |
done |
859 |
||
860 |
||
861 |
subsection {* An application *} |
|
862 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
863 |
lemma gcd_eq_nat: |
31719 | 864 |
assumes pos [arith]: "x > 0" "y > 0" |
865 |
shows "gcd (x::nat) y = |
|
866 |
(PROD p: prime_factors x Un prime_factors y. |
|
867 |
p ^ (min (multiplicity p x) (multiplicity p y)))" |
|
868 |
proof - |
|
869 |
def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. |
|
870 |
p ^ (min (multiplicity p x) (multiplicity p y)))" |
|
871 |
have [arith]: "z > 0" |
|
872 |
unfolding z_def by (rule setprod_pos_nat, auto) |
|
873 |
have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = |
|
874 |
min (multiplicity p x) (multiplicity p y)" |
|
875 |
unfolding z_def |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
876 |
apply (subst multiplicity_prod_prime_powers_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
877 |
apply (auto simp add: multiplicity_not_factor_nat) |
31719 | 878 |
done |
879 |
have "z dvd x" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
880 |
by (intro multiplicity_dvd'_nat, auto simp add: aux) |
31719 | 881 |
moreover have "z dvd y" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
882 |
by (intro multiplicity_dvd'_nat, auto simp add: aux) |
31719 | 883 |
moreover have "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z" |
884 |
apply auto |
|
885 |
apply (case_tac "w = 0", auto) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
886 |
apply (erule multiplicity_dvd'_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
887 |
apply (auto intro: dvd_multiplicity_nat simp add: aux) |
31719 | 888 |
done |
889 |
ultimately have "z = gcd x y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
890 |
by (subst gcd_unique_nat [symmetric], blast) |
31719 | 891 |
thus ?thesis |
892 |
unfolding z_def by auto |
|
893 |
qed |
|
894 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
895 |
lemma lcm_eq_nat: |
31719 | 896 |
assumes pos [arith]: "x > 0" "y > 0" |
897 |
shows "lcm (x::nat) y = |
|
898 |
(PROD p: prime_factors x Un prime_factors y. |
|
899 |
p ^ (max (multiplicity p x) (multiplicity p y)))" |
|
900 |
proof - |
|
901 |
def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. |
|
902 |
p ^ (max (multiplicity p x) (multiplicity p y)))" |
|
903 |
have [arith]: "z > 0" |
|
904 |
unfolding z_def by (rule setprod_pos_nat, auto) |
|
905 |
have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = |
|
906 |
max (multiplicity p x) (multiplicity p y)" |
|
907 |
unfolding z_def |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
908 |
apply (subst multiplicity_prod_prime_powers_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
909 |
apply (auto simp add: multiplicity_not_factor_nat) |
31719 | 910 |
done |
911 |
have "x dvd z" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
912 |
by (intro multiplicity_dvd'_nat, auto simp add: aux) |
31719 | 913 |
moreover have "y dvd z" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
914 |
by (intro multiplicity_dvd'_nat, auto simp add: aux) |
31719 | 915 |
moreover have "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w" |
916 |
apply auto |
|
917 |
apply (case_tac "w = 0", auto) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
918 |
apply (rule multiplicity_dvd'_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
919 |
apply (auto intro: dvd_multiplicity_nat simp add: aux) |
31719 | 920 |
done |
921 |
ultimately have "z = lcm x y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
922 |
by (subst lcm_unique_nat [symmetric], blast) |
31719 | 923 |
thus ?thesis |
924 |
unfolding z_def by auto |
|
925 |
qed |
|
926 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
927 |
lemma multiplicity_gcd_nat: |
31719 | 928 |
assumes [arith]: "x > 0" "y > 0" |
929 |
shows "multiplicity (p::nat) (gcd x y) = |
|
930 |
min (multiplicity p x) (multiplicity p y)" |
|
931 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
932 |
apply (subst gcd_eq_nat) |
31719 | 933 |
apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
934 |
apply (subst multiplicity_prod_prime_powers_nat) |
31719 | 935 |
apply auto |
936 |
done |
|
937 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
938 |
lemma multiplicity_lcm_nat: |
31719 | 939 |
assumes [arith]: "x > 0" "y > 0" |
940 |
shows "multiplicity (p::nat) (lcm x y) = |
|
941 |
max (multiplicity p x) (multiplicity p y)" |
|
942 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
943 |
apply (subst lcm_eq_nat) |
31719 | 944 |
apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
945 |
apply (subst multiplicity_prod_prime_powers_nat) |
31719 | 946 |
apply auto |
947 |
done |
|
948 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
949 |
lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)" |
31719 | 950 |
apply (case_tac "x = 0 | y = 0 | z = 0") |
951 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
952 |
apply (rule multiplicity_eq_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
953 |
apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
954 |
lcm_pos_nat) |
31719 | 955 |
done |
956 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
957 |
lemma gcd_lcm_distrib_int: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
958 |
apply (subst (1 2 3) gcd_abs_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
959 |
apply (subst lcm_abs_int) |
31719 | 960 |
apply (subst (2) abs_of_nonneg) |
961 |
apply force |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
962 |
apply (rule gcd_lcm_distrib_nat [transferred]) |
31719 | 963 |
apply auto |
964 |
done |
|
965 |
||
966 |
end |