author | haftmann |
Fri, 26 Feb 2016 22:44:11 +0100 | |
changeset 62430 | 9527ff088c15 |
parent 62429 | 25271ff79171 |
child 63534 | 523b488b15c9 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Number_Theory/UniqueFactorization.thy |
31719 | 2 |
Author: Jeremy Avigad |
3 |
||
41541 | 4 |
Note: there were previous Isabelle formalizations of unique |
5 |
factorization due to Thomas Marthedal Rasmussen, and, building on |
|
60527 | 6 |
that, by Jeremy Avigad and David Gray. |
31719 | 7 |
*) |
8 |
||
60527 | 9 |
section \<open>Unique factorization for the natural numbers and the integers\<close> |
31719 | 10 |
|
11 |
theory UniqueFactorization |
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40461
diff
changeset
|
12 |
imports Cong "~~/src/HOL/Library/Multiset" |
31719 | 13 |
begin |
14 |
||
15 |
(* As a simp or intro rule, |
|
16 |
||
17 |
prime p \<Longrightarrow> p > 0 |
|
18 |
||
60527 | 19 |
wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it |
31719 | 20 |
leads to the backchaining |
21 |
||
60527 | 22 |
x > 0 |
23 |
prime x |
|
24 |
x \<in># M which is, unfortunately, |
|
31719 | 25 |
count M x > 0 |
26 |
*) |
|
27 |
||
28 |
(* Here is a version of set product for multisets. Is it worth moving |
|
60527 | 29 |
to multiset.thy? If so, one should similarly define msetsum for abelian |
30 |
semirings, using of_nat. Also, is it worth developing bounded quantifiers |
|
31 |
"\<forall>i \<in># M. P i"? |
|
31719 | 32 |
*) |
33 |
||
34 |
||
60527 | 35 |
subsection \<open>Unique factorization: multiset version\<close> |
31719 | 36 |
|
60527 | 37 |
lemma multiset_prime_factorization_exists: |
38 |
"n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))" |
|
39 |
proof (induct n rule: nat_less_induct) |
|
31719 | 40 |
fix n :: nat |
60527 | 41 |
assume ih: "\<forall>m < n. 0 < m \<longrightarrow> (\<exists>M. (\<forall>p\<in>set_mset M. prime p) \<and> m = (\<Prod>i \<in># M. i))" |
42 |
assume "n > 0" |
|
43 |
then consider "n = 1" | "n > 1" "prime n" | "n > 1" "\<not> prime n" |
|
31719 | 44 |
by arith |
60567 | 45 |
then show "\<exists>M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i\<in>#M. i)" |
60527 | 46 |
proof cases |
47 |
case 1 |
|
48 |
then have "(\<forall>p\<in>set_mset {#}. prime p) \<and> n = (\<Prod>i \<in># {#}. i)" |
|
49824 | 49 |
by auto |
60527 | 50 |
then show ?thesis .. |
51 |
next |
|
52 |
case 2 |
|
53 |
then have "(\<forall>p\<in>set_mset {#n#}. prime p) \<and> n = (\<Prod>i \<in># {#n#}. i)" |
|
54 |
by auto |
|
55 |
then show ?thesis .. |
|
56 |
next |
|
57 |
case 3 |
|
44872 | 58 |
with not_prime_eq_prod_nat |
60527 | 59 |
obtain m k where n: "n = m * k" "1 < m" "m < n" "1 < k" "k < n" |
44872 | 60 |
by blast |
60527 | 61 |
with ih obtain Q R where "(\<forall>p \<in> set_mset Q. prime p) \<and> m = (\<Prod>i\<in>#Q. i)" |
62 |
and "(\<forall>p\<in>set_mset R. prime p) \<and> k = (\<Prod>i\<in>#R. i)" |
|
31719 | 63 |
by blast |
60527 | 64 |
then have "(\<forall>p\<in>set_mset (Q + R). prime p) \<and> n = (\<Prod>i \<in># Q + R. i)" |
41541 | 65 |
by (auto simp add: n msetprod_Un) |
60527 | 66 |
then show ?thesis .. |
67 |
qed |
|
31719 | 68 |
qed |
69 |
||
70 |
lemma multiset_prime_factorization_unique_aux: |
|
71 |
fixes a :: nat |
|
60527 | 72 |
assumes "\<forall>p\<in>set_mset M. prime p" |
73 |
and "\<forall>p\<in>set_mset N. prime p" |
|
74 |
and "(\<Prod>i \<in># M. i) dvd (\<Prod>i \<in># N. i)" |
|
75 |
shows "count M a \<le> count N a" |
|
76 |
proof (cases "a \<in> set_mset M") |
|
77 |
case True |
|
78 |
with assms have a: "prime a" |
|
79 |
by auto |
|
80 |
with True have "a ^ count M a dvd (\<Prod>i \<in># M. i)" |
|
59010 | 81 |
by (auto simp add: msetprod_multiplicity) |
60527 | 82 |
also have "\<dots> dvd (\<Prod>i \<in># N. i)" |
83 |
by (rule assms) |
|
84 |
also have "\<dots> = (\<Prod>i \<in> set_mset N. i ^ count N i)" |
|
49824 | 85 |
by (simp add: msetprod_multiplicity) |
60527 | 86 |
also have "\<dots> = a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" |
87 |
proof (cases "a \<in> set_mset N") |
|
88 |
case True |
|
89 |
then have b: "set_mset N = {a} \<union> (set_mset N - {a})" |
|
44872 | 90 |
by auto |
91 |
then show ?thesis |
|
57418 | 92 |
by (subst (1) b, subst setprod.union_disjoint, auto) |
44872 | 93 |
next |
60527 | 94 |
case False |
95 |
then show ?thesis |
|
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62429
diff
changeset
|
96 |
by (auto simp add: not_in_iff) |
44872 | 97 |
qed |
60527 | 98 |
finally have "a ^ count M a dvd a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" . |
44872 | 99 |
moreover |
60527 | 100 |
have "coprime (a ^ count M a) (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" |
62348 | 101 |
apply (subst gcd.commute) |
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62349
diff
changeset
|
102 |
apply (rule setprod_coprime) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
103 |
apply (rule primes_imp_powers_coprime_nat) |
60527 | 104 |
using assms True |
41541 | 105 |
apply auto |
31719 | 106 |
done |
60527 | 107 |
ultimately have "a ^ count M a dvd a ^ count N a" |
62348 | 108 |
by (elim coprime_dvd_mult) |
60527 | 109 |
with a show ?thesis |
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61714
diff
changeset
|
110 |
using power_dvd_imp_le prime_def by blast |
31719 | 111 |
next |
60527 | 112 |
case False |
113 |
then show ?thesis |
|
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62429
diff
changeset
|
114 |
by (auto simp add: not_in_iff) |
31719 | 115 |
qed |
116 |
||
117 |
lemma multiset_prime_factorization_unique: |
|
60527 | 118 |
assumes "\<forall>p::nat \<in> set_mset M. prime p" |
119 |
and "\<forall>p \<in> set_mset N. prime p" |
|
120 |
and "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)" |
|
121 |
shows "M = N" |
|
31719 | 122 |
proof - |
60527 | 123 |
have "count M a = count N a" for a |
124 |
proof - |
|
125 |
from assms have "count M a \<le> count N a" |
|
126 |
by (intro multiset_prime_factorization_unique_aux, auto) |
|
127 |
moreover from assms have "count N a \<le> count M a" |
|
128 |
by (intro multiset_prime_factorization_unique_aux, auto) |
|
129 |
ultimately show ?thesis |
|
31719 | 130 |
by auto |
60527 | 131 |
qed |
132 |
then show ?thesis |
|
133 |
by (simp add: multiset_eq_iff) |
|
31719 | 134 |
qed |
135 |
||
60527 | 136 |
definition multiset_prime_factorization :: "nat \<Rightarrow> nat multiset" |
44872 | 137 |
where |
60527 | 138 |
"multiset_prime_factorization n = |
139 |
(if n > 0 |
|
140 |
then THE M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i) |
|
141 |
else {#})" |
|
31719 | 142 |
|
60527 | 143 |
lemma multiset_prime_factorization: "n > 0 \<Longrightarrow> |
144 |
(\<forall>p \<in> set_mset (multiset_prime_factorization n). prime p) \<and> |
|
145 |
n = (\<Prod>i \<in># (multiset_prime_factorization n). i)" |
|
31719 | 146 |
apply (unfold multiset_prime_factorization_def) |
147 |
apply clarsimp |
|
148 |
apply (frule multiset_prime_factorization_exists) |
|
149 |
apply clarify |
|
150 |
apply (rule theI) |
|
49719 | 151 |
apply (insert multiset_prime_factorization_unique) |
152 |
apply auto |
|
60527 | 153 |
done |
31719 | 154 |
|
155 |
||
60527 | 156 |
subsection \<open>Prime factors and multiplicity for nat and int\<close> |
31719 | 157 |
|
158 |
class unique_factorization = |
|
44872 | 159 |
fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" |
160 |
and prime_factors :: "'a \<Rightarrow> 'a set" |
|
31719 | 161 |
|
60527 | 162 |
text \<open>Definitions for the natural numbers.\<close> |
31719 | 163 |
instantiation nat :: unique_factorization |
164 |
begin |
|
165 |
||
44872 | 166 |
definition multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
167 |
where "multiplicity_nat p n = count (multiset_prime_factorization n) p" |
|
31719 | 168 |
|
44872 | 169 |
definition prime_factors_nat :: "nat \<Rightarrow> nat set" |
60495 | 170 |
where "prime_factors_nat n = set_mset (multiset_prime_factorization n)" |
31719 | 171 |
|
44872 | 172 |
instance .. |
31719 | 173 |
|
174 |
end |
|
175 |
||
60527 | 176 |
text \<open>Definitions for the integers.\<close> |
31719 | 177 |
instantiation int :: unique_factorization |
178 |
begin |
|
179 |
||
44872 | 180 |
definition multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat" |
181 |
where "multiplicity_int p n = multiplicity (nat p) (nat n)" |
|
31719 | 182 |
|
44872 | 183 |
definition prime_factors_int :: "int \<Rightarrow> int set" |
184 |
where "prime_factors_int n = int ` (prime_factors (nat n))" |
|
31719 | 185 |
|
44872 | 186 |
instance .. |
31719 | 187 |
|
188 |
end |
|
189 |
||
190 |
||
60526 | 191 |
subsection \<open>Set up transfer\<close> |
31719 | 192 |
|
44872 | 193 |
lemma transfer_nat_int_prime_factors: "prime_factors (nat n) = nat ` prime_factors n" |
194 |
unfolding prime_factors_int_def |
|
195 |
apply auto |
|
196 |
apply (subst transfer_int_nat_set_return_embed) |
|
197 |
apply assumption |
|
198 |
done |
|
31719 | 199 |
|
60527 | 200 |
lemma transfer_nat_int_prime_factors_closure: "n \<ge> 0 \<Longrightarrow> nat_set (prime_factors n)" |
31719 | 201 |
by (auto simp add: nat_set_def prime_factors_int_def) |
202 |
||
60527 | 203 |
lemma transfer_nat_int_multiplicity: |
204 |
"p \<ge> 0 \<Longrightarrow> n \<ge> 0 \<Longrightarrow> multiplicity (nat p) (nat n) = multiplicity p n" |
|
31719 | 205 |
by (auto simp add: multiplicity_int_def) |
206 |
||
60527 | 207 |
declare transfer_morphism_nat_int[transfer add return: |
31719 | 208 |
transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure |
209 |
transfer_nat_int_multiplicity] |
|
210 |
||
44872 | 211 |
lemma transfer_int_nat_prime_factors: "prime_factors (int n) = int ` prime_factors n" |
31719 | 212 |
unfolding prime_factors_int_def by auto |
213 |
||
60527 | 214 |
lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> nat_set (prime_factors n)" |
31719 | 215 |
by (simp only: transfer_nat_int_prime_factors_closure is_nat_def) |
216 |
||
60527 | 217 |
lemma transfer_int_nat_multiplicity: "multiplicity (int p) (int n) = multiplicity p n" |
31719 | 218 |
by (auto simp add: multiplicity_int_def) |
219 |
||
60527 | 220 |
declare transfer_morphism_int_nat[transfer add return: |
31719 | 221 |
transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure |
222 |
transfer_int_nat_multiplicity] |
|
223 |
||
224 |
||
60527 | 225 |
subsection \<open>Properties of prime factors and multiplicity for nat and int\<close> |
31719 | 226 |
|
60527 | 227 |
lemma prime_factors_ge_0_int [elim]: |
228 |
fixes n :: int |
|
229 |
shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0" |
|
44872 | 230 |
unfolding prime_factors_int_def by auto |
31719 | 231 |
|
60527 | 232 |
lemma prime_factors_prime_nat [intro]: |
233 |
fixes n :: nat |
|
234 |
shows "p \<in> prime_factors n \<Longrightarrow> prime p" |
|
44872 | 235 |
apply (cases "n = 0") |
31719 | 236 |
apply (simp add: prime_factors_nat_def multiset_prime_factorization_def) |
237 |
apply (auto simp add: prime_factors_nat_def multiset_prime_factorization) |
|
41541 | 238 |
done |
31719 | 239 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
240 |
lemma prime_factors_prime_int [intro]: |
60527 | 241 |
fixes n :: int |
242 |
assumes "n \<ge> 0" and "p \<in> prime_factors n" |
|
31719 | 243 |
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
|
244 |
apply (rule prime_factors_prime_nat [transferred, of n p, simplified]) |
41541 | 245 |
using assms apply auto |
246 |
done |
|
31719 | 247 |
|
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61714
diff
changeset
|
248 |
lemma prime_factors_gt_0_nat: |
60527 | 249 |
fixes p :: nat |
250 |
shows "p \<in> prime_factors x \<Longrightarrow> p > 0" |
|
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61714
diff
changeset
|
251 |
using prime_factors_prime_nat by force |
31719 | 252 |
|
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61714
diff
changeset
|
253 |
lemma prime_factors_gt_0_int: |
60527 | 254 |
shows "x \<ge> 0 \<Longrightarrow> p \<in> prime_factors x \<Longrightarrow> int p > (0::int)" |
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61714
diff
changeset
|
255 |
by (simp add: prime_factors_gt_0_nat) |
31719 | 256 |
|
60527 | 257 |
lemma prime_factors_finite_nat [iff]: |
258 |
fixes n :: nat |
|
259 |
shows "finite (prime_factors n)" |
|
44872 | 260 |
unfolding prime_factors_nat_def by auto |
31719 | 261 |
|
60527 | 262 |
lemma prime_factors_finite_int [iff]: |
263 |
fixes n :: int |
|
264 |
shows "finite (prime_factors n)" |
|
44872 | 265 |
unfolding prime_factors_int_def by auto |
31719 | 266 |
|
60527 | 267 |
lemma prime_factors_altdef_nat: |
268 |
fixes n :: nat |
|
269 |
shows "prime_factors n = {p. multiplicity p n > 0}" |
|
31719 | 270 |
by (force simp add: prime_factors_nat_def multiplicity_nat_def) |
271 |
||
60527 | 272 |
lemma prime_factors_altdef_int: |
273 |
fixes n :: int |
|
274 |
shows "prime_factors n = {p. p \<ge> 0 \<and> multiplicity p n > 0}" |
|
31719 | 275 |
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
|
276 |
apply (subst prime_factors_altdef_nat) |
31719 | 277 |
apply (auto simp add: image_def) |
41541 | 278 |
done |
31719 | 279 |
|
60527 | 280 |
lemma prime_factorization_nat: |
281 |
fixes n :: nat |
|
282 |
shows "n > 0 \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)" |
|
44872 | 283 |
apply (frule multiset_prime_factorization) |
49824 | 284 |
apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_multiplicity) |
44872 | 285 |
done |
31719 | 286 |
|
60527 | 287 |
lemma prime_factorization_int: |
288 |
fixes n :: int |
|
289 |
assumes "n > 0" |
|
290 |
shows "n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
291 |
apply (rule prime_factorization_nat [transferred, of n]) |
41541 | 292 |
using assms apply auto |
293 |
done |
|
31719 | 294 |
|
60527 | 295 |
lemma prime_factorization_unique_nat: |
49718 | 296 |
fixes f :: "nat \<Rightarrow> _" |
60527 | 297 |
assumes S_eq: "S = {p. 0 < f p}" |
298 |
and "finite S" |
|
61714 | 299 |
and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)" |
49718 | 300 |
shows "S = prime_factors n \<and> (\<forall>p. f p = multiplicity p n)" |
301 |
proof - |
|
302 |
from assms have "f \<in> multiset" |
|
303 |
by (auto simp add: multiset_def) |
|
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61714
diff
changeset
|
304 |
moreover from assms have "n > 0" |
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61714
diff
changeset
|
305 |
by (auto intro: prime_gt_0_nat) |
49718 | 306 |
ultimately have "multiset_prime_factorization n = Abs_multiset f" |
307 |
apply (unfold multiset_prime_factorization_def) |
|
308 |
apply (subst if_P, assumption) |
|
309 |
apply (rule the1_equality) |
|
310 |
apply (rule ex_ex1I) |
|
311 |
apply (rule multiset_prime_factorization_exists, assumption) |
|
312 |
apply (rule multiset_prime_factorization_unique) |
|
313 |
apply force |
|
314 |
apply force |
|
315 |
apply force |
|
61714 | 316 |
using S S_eq apply (simp add: set_mset_def msetprod_multiplicity) |
49718 | 317 |
done |
60526 | 318 |
with \<open>f \<in> multiset\<close> have "count (multiset_prime_factorization n) = f" |
59010 | 319 |
by simp |
49718 | 320 |
with S_eq show ?thesis |
60495 | 321 |
by (simp add: set_mset_def multiset_def prime_factors_nat_def multiplicity_nat_def) |
49718 | 322 |
qed |
31719 | 323 |
|
60527 | 324 |
lemma prime_factors_characterization_nat: |
325 |
"S = {p. 0 < f (p::nat)} \<Longrightarrow> |
|
326 |
finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S" |
|
327 |
by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric]) |
|
31719 | 328 |
|
60527 | 329 |
lemma prime_factors_characterization'_nat: |
31719 | 330 |
"finite {p. 0 < f (p::nat)} \<Longrightarrow> |
60527 | 331 |
(\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> |
332 |
prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}" |
|
333 |
by (rule prime_factors_characterization_nat) auto |
|
31719 | 334 |
|
335 |
(* A minor glitch:*) |
|
60527 | 336 |
thm prime_factors_characterization'_nat |
337 |
[where f = "\<lambda>x. f (int (x::nat))", |
|
338 |
transferred direction: nat "op \<le> (0::int)", rule_format] |
|
31719 | 339 |
|
340 |
(* |
|
60527 | 341 |
Transfer isn't smart enough to know that the "0 < f p" should |
342 |
remain a comparison between nats. But the transfer still works. |
|
31719 | 343 |
*) |
344 |
||
60527 | 345 |
lemma primes_characterization'_int [rule_format]: |
346 |
"finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow> |
|
347 |
prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}" |
|
348 |
using prime_factors_characterization'_nat |
|
349 |
[where f = "\<lambda>x. f (int (x::nat))", |
|
350 |
transferred direction: nat "op \<le> (0::int)"] |
|
351 |
by auto |
|
31719 | 352 |
|
60527 | 353 |
lemma prime_factors_characterization_int: |
354 |
"S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow> |
|
355 |
\<forall>p\<in>S. prime (nat p) \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S" |
|
31719 | 356 |
apply simp |
60527 | 357 |
apply (subgoal_tac "{p. 0 < f p} = {p. 0 \<le> p \<and> 0 < f p}") |
31719 | 358 |
apply (simp only:) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
359 |
apply (subst primes_characterization'_int) |
61714 | 360 |
apply simp_all |
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
|
361 |
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
|
362 |
apply (metis le_cases nat_le_0 zero_not_prime_nat) |
44872 | 363 |
done |
31719 | 364 |
|
60527 | 365 |
lemma multiplicity_characterization_nat: |
366 |
"S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> |
|
367 |
n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p" |
|
44872 | 368 |
apply (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, symmetric]) |
369 |
apply auto |
|
370 |
done |
|
31719 | 371 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
372 |
lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow> |
60527 | 373 |
(\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> |
374 |
multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p" |
|
44872 | 375 |
apply (intro impI) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
376 |
apply (rule multiplicity_characterization_nat) |
31719 | 377 |
apply auto |
44872 | 378 |
done |
31719 | 379 |
|
60527 | 380 |
lemma multiplicity_characterization'_int [rule_format]: |
381 |
"finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> |
|
382 |
(\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p \<ge> 0 \<Longrightarrow> |
|
383 |
multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p" |
|
384 |
apply (insert multiplicity_characterization'_nat |
|
385 |
[where f = "\<lambda>x. f (int (x::nat))", |
|
386 |
transferred direction: nat "op \<le> (0::int)", rule_format]) |
|
31719 | 387 |
apply auto |
44872 | 388 |
done |
31719 | 389 |
|
60527 | 390 |
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> |
391 |
finite S \<Longrightarrow> \<forall>p\<in>S. prime (nat p) \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> |
|
392 |
p \<ge> 0 \<Longrightarrow> multiplicity p n = f p" |
|
31719 | 393 |
apply simp |
60527 | 394 |
apply (subgoal_tac "{p. 0 < f p} = {p. 0 \<le> p \<and> 0 < f p}") |
31719 | 395 |
apply (simp only:) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
396 |
apply (subst multiplicity_characterization'_int) |
61714 | 397 |
apply simp_all |
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
|
398 |
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
|
399 |
apply (metis le_cases nat_le_0 zero_not_prime_nat) |
44872 | 400 |
done |
31719 | 401 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
402 |
lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0" |
31719 | 403 |
by (simp add: multiplicity_nat_def multiset_prime_factorization_def) |
404 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
405 |
lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0" |
60527 | 406 |
by (simp add: multiplicity_int_def) |
31719 | 407 |
|
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset
|
408 |
lemma multiplicity_one_nat': "multiplicity p (1::nat) = 0" |
60527 | 409 |
by (subst multiplicity_characterization_nat [where f = "\<lambda>x. 0"], auto) |
31719 | 410 |
|
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset
|
411 |
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
|
412 |
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
|
413 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
414 |
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
|
415 |
by (metis multiplicity_int_def multiplicity_one_nat' transfer_nat_int_numerals(2)) |
31719 | 416 |
|
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
|
417 |
lemma multiplicity_prime_nat [simp]: "prime p \<Longrightarrow> multiplicity p p = 1" |
60527 | 418 |
apply (subst multiplicity_characterization_nat [where f = "\<lambda>q. if q = p then 1 else 0"]) |
31719 | 419 |
apply auto |
60527 | 420 |
apply (metis (full_types) less_not_refl) |
421 |
done |
|
31719 | 422 |
|
60527 | 423 |
lemma multiplicity_prime_power_nat [simp]: "prime p \<Longrightarrow> multiplicity p (p ^ n) = n" |
44872 | 424 |
apply (cases "n = 0") |
31719 | 425 |
apply auto |
60527 | 426 |
apply (subst multiplicity_characterization_nat [where f = "\<lambda>q. if q = p then n else 0"]) |
31719 | 427 |
apply auto |
60527 | 428 |
apply (metis (full_types) less_not_refl) |
429 |
done |
|
31719 | 430 |
|
60527 | 431 |
lemma multiplicity_prime_power_int [simp]: "prime p \<Longrightarrow> multiplicity p (int p ^ n) = 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
|
432 |
by (metis multiplicity_prime_power_nat of_nat_power transfer_int_nat_multiplicity) |
31719 | 433 |
|
60527 | 434 |
lemma multiplicity_nonprime_nat [simp]: |
435 |
fixes p n :: nat |
|
436 |
shows "\<not> prime p \<Longrightarrow> multiplicity p n = 0" |
|
44872 | 437 |
apply (cases "n = 0") |
31719 | 438 |
apply auto |
439 |
apply (frule multiset_prime_factorization) |
|
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62429
diff
changeset
|
440 |
apply (auto simp add: multiplicity_nat_def count_eq_zero_iff) |
44872 | 441 |
done |
31719 | 442 |
|
60527 | 443 |
lemma multiplicity_not_factor_nat [simp]: |
444 |
fixes p n :: nat |
|
445 |
shows "p \<notin> prime_factors n \<Longrightarrow> multiplicity p n = 0" |
|
44872 | 446 |
apply (subst (asm) prime_factors_altdef_nat) |
447 |
apply auto |
|
448 |
done |
|
31719 | 449 |
|
60527 | 450 |
lemma multiplicity_not_factor_int [simp]: |
451 |
fixes n :: int |
|
452 |
shows "p \<ge> 0 \<Longrightarrow> p \<notin> prime_factors n \<Longrightarrow> multiplicity p n = 0" |
|
44872 | 453 |
apply (subst (asm) prime_factors_altdef_int) |
454 |
apply auto |
|
455 |
done |
|
31719 | 456 |
|
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset
|
457 |
(*FIXME: messy*) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
458 |
lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> |
60527 | 459 |
(prime_factors k) \<union> (prime_factors l) = prime_factors (k * l) \<and> |
460 |
(\<forall>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
|
461 |
apply (rule prime_factorization_unique_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
462 |
apply (simp only: prime_factors_altdef_nat) |
31719 | 463 |
apply auto |
464 |
apply (subst power_add) |
|
57418 | 465 |
apply (subst setprod.distrib) |
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset
|
466 |
apply (rule arg_cong2 [where f = "\<lambda>x y. x*y"]) |
60527 | 467 |
apply (subgoal_tac "prime_factors k \<union> prime_factors l = prime_factors k \<union> |
31719 | 468 |
(prime_factors l - prime_factors k)") |
469 |
apply (erule ssubst) |
|
57418 | 470 |
apply (subst setprod.union_disjoint) |
31719 | 471 |
apply auto |
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset
|
472 |
apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const) |
60527 | 473 |
apply (subgoal_tac "prime_factors k \<union> prime_factors l = prime_factors l \<union> |
31719 | 474 |
(prime_factors k - prime_factors l)") |
475 |
apply (erule ssubst) |
|
57418 | 476 |
apply (subst setprod.union_disjoint) |
31719 | 477 |
apply auto |
60527 | 478 |
apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) = |
31719 | 479 |
(\<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
|
480 |
apply auto |
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset
|
481 |
apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const) |
44872 | 482 |
done |
31719 | 483 |
|
60527 | 484 |
(* transfer doesn't have the same problem here with the right |
31719 | 485 |
choice of rules. *) |
486 |
||
60527 | 487 |
lemma multiplicity_product_aux_int: |
31719 | 488 |
assumes "(k::int) > 0" and "l > 0" |
60527 | 489 |
shows "prime_factors k \<union> prime_factors l = prime_factors (k * l) \<and> |
490 |
(\<forall>p \<ge> 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
|
491 |
apply (rule multiplicity_product_aux_nat [transferred, of l k]) |
41541 | 492 |
using assms apply auto |
493 |
done |
|
31719 | 494 |
|
60527 | 495 |
lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = |
496 |
prime_factors k \<union> prime_factors l" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
497 |
by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric]) |
31719 | 498 |
|
60527 | 499 |
lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = |
500 |
prime_factors k \<union> prime_factors l" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
501 |
by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric]) |
31719 | 502 |
|
60527 | 503 |
lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) = |
31719 | 504 |
multiplicity p k + multiplicity p l" |
60527 | 505 |
by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, symmetric]) |
31719 | 506 |
|
60527 | 507 |
lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow> |
31719 | 508 |
multiplicity p (k * l) = multiplicity p k + multiplicity p l" |
60527 | 509 |
by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, symmetric]) |
31719 | 510 |
|
60527 | 511 |
lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> \<forall>x\<in>S. f x > 0 \<Longrightarrow> |
512 |
multiplicity (p::nat) (\<Prod>x \<in> S. f x) = (\<Sum>x \<in> S. multiplicity p (f x))" |
|
31719 | 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 |
|
60527 | 520 |
an implicit quantifier over functions (f), and, second, because the |
521 |
product over the multiplicity should not be translated to an integer |
|
31719 | 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 |
||
60527 | 528 |
lemma transfer_nat_int_sum_prod_closure3: "(\<Sum>x \<in> A. int (f x)) \<ge> 0" "(\<Prod>x \<in> A. int (f x)) \<ge> 0" |
529 |
apply (rule setsum_nonneg; auto) |
|
530 |
apply (rule setprod_nonneg; auto) |
|
44872 | 531 |
done |
31719 | 532 |
|
60527 | 533 |
declare transfer_morphism_nat_int[transfer |
31719 | 534 |
add return: transfer_nat_int_sum_prod_closure3 |
535 |
del: transfer_nat_int_sum_prod2 (1)] |
|
536 |
||
60527 | 537 |
lemma multiplicity_setprod_int: "p \<ge> 0 \<Longrightarrow> finite S \<Longrightarrow> \<forall>x\<in>S. f x > 0 \<Longrightarrow> |
538 |
multiplicity (p::int) (\<Prod>x \<in> S. f x) = (\<Sum>x \<in> S. multiplicity p (f x))" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
539 |
apply (frule multiplicity_setprod_nat |
60527 | 540 |
[where f = "\<lambda>x. nat(int(nat(f x)))", |
541 |
transferred direction: nat "op \<le> (0::int)"]) |
|
31719 | 542 |
apply auto |
57418 | 543 |
apply (subst (asm) setprod.cong) |
31719 | 544 |
apply (rule refl) |
545 |
apply (rule if_P) |
|
546 |
apply auto |
|
57418 | 547 |
apply (rule setsum.cong) |
31719 | 548 |
apply auto |
44872 | 549 |
done |
31719 | 550 |
|
60527 | 551 |
declare transfer_morphism_nat_int[transfer |
31719 | 552 |
add return: transfer_nat_int_sum_prod2 (1)] |
553 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
554 |
lemma multiplicity_prod_prime_powers_nat: |
60527 | 555 |
"finite S \<Longrightarrow> \<forall>p\<in>S. prime (p::nat) \<Longrightarrow> |
556 |
multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)" |
|
557 |
apply (subgoal_tac "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ (\<lambda>x. if x \<in> S then f x else 0) p)") |
|
31719 | 558 |
apply (erule ssubst) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
559 |
apply (subst multiplicity_characterization_nat) |
31719 | 560 |
prefer 5 apply (rule refl) |
561 |
apply (rule refl) |
|
562 |
apply auto |
|
57418 | 563 |
apply (subst setprod.mono_neutral_right) |
31719 | 564 |
apply assumption |
565 |
prefer 3 |
|
57418 | 566 |
apply (rule setprod.cong) |
31719 | 567 |
apply (rule refl) |
568 |
apply auto |
|
60527 | 569 |
done |
31719 | 570 |
|
571 |
(* Here the issue with transfer is the implicit quantifier over S *) |
|
572 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
573 |
lemma multiplicity_prod_prime_powers_int: |
60527 | 574 |
"(p::int) \<ge> 0 \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime (nat p) \<Longrightarrow> |
575 |
multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)" |
|
31719 | 576 |
apply (subgoal_tac "int ` nat ` S = S") |
60527 | 577 |
apply (frule multiplicity_prod_prime_powers_nat |
578 |
[where f = "\<lambda>x. f(int x)" and S = "nat ` S", transferred]) |
|
31719 | 579 |
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
|
580 |
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
|
581 |
apply (metis (full_types) image_iff int_nat_eq less_le less_linear nat_0_iff zero_not_prime_nat) |
44872 | 582 |
done |
31719 | 583 |
|
60527 | 584 |
lemma multiplicity_distinct_prime_power_nat: |
585 |
"prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0" |
|
586 |
apply (subgoal_tac "q ^ n = setprod (\<lambda>x. x ^ n) {q}") |
|
31719 | 587 |
apply (erule ssubst) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
588 |
apply (subst multiplicity_prod_prime_powers_nat) |
31719 | 589 |
apply auto |
44872 | 590 |
done |
31719 | 591 |
|
60527 | 592 |
lemma multiplicity_distinct_prime_power_int: |
593 |
"prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (int q ^ n) = 0" |
|
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
|
594 |
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
|
595 |
|
44872 | 596 |
lemma dvd_multiplicity_nat: |
60527 | 597 |
fixes x y :: nat |
598 |
shows "0 < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x \<le> multiplicity p y" |
|
44872 | 599 |
apply (cases "x = 0") |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
600 |
apply (auto simp add: dvd_def multiplicity_product_nat) |
44872 | 601 |
done |
31719 | 602 |
|
60527 | 603 |
lemma dvd_multiplicity_int: |
604 |
fixes p x y :: int |
|
605 |
shows "0 < y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x dvd y \<Longrightarrow> p \<ge> 0 \<Longrightarrow> multiplicity p x \<le> multiplicity p y" |
|
44872 | 606 |
apply (cases "x = 0") |
31719 | 607 |
apply (auto simp add: dvd_def) |
608 |
apply (subgoal_tac "0 < k") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
609 |
apply (auto simp add: multiplicity_product_int) |
31719 | 610 |
apply (erule zero_less_mult_pos) |
611 |
apply arith |
|
44872 | 612 |
done |
31719 | 613 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
614 |
lemma dvd_prime_factors_nat [intro]: |
60527 | 615 |
fixes x y :: nat |
616 |
shows "0 < y \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<le> prime_factors y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
617 |
apply (simp only: prime_factors_altdef_nat) |
31719 | 618 |
apply auto |
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54611
diff
changeset
|
619 |
apply (metis dvd_multiplicity_nat le_0_eq neq0_conv) |
44872 | 620 |
done |
31719 | 621 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
622 |
lemma dvd_prime_factors_int [intro]: |
60527 | 623 |
fixes x y :: int |
624 |
shows "0 < y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<le> prime_factors y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
625 |
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
|
626 |
apply (metis dvd_multiplicity_int le_0_eq neq0_conv) |
44872 | 627 |
done |
31719 | 628 |
|
60527 | 629 |
lemma multiplicity_dvd_nat: |
630 |
fixes x y :: nat |
|
631 |
shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> \<forall>p. multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
632 |
apply (subst prime_factorization_nat [of x], assumption) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
633 |
apply (subst prime_factorization_nat [of y], assumption) |
31719 | 634 |
apply (rule setprod_dvd_setprod_subset2) |
635 |
apply force |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
636 |
apply (subst prime_factors_altdef_nat)+ |
31719 | 637 |
apply auto |
40461 | 638 |
apply (metis gr0I le_0_eq less_not_refl) |
639 |
apply (metis le_imp_power_dvd) |
|
44872 | 640 |
done |
31719 | 641 |
|
60527 | 642 |
lemma multiplicity_dvd_int: |
643 |
fixes x y :: int |
|
644 |
shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> \<forall>p\<ge>0. multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
645 |
apply (subst prime_factorization_int [of x], assumption) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
646 |
apply (subst prime_factorization_int [of y], assumption) |
31719 | 647 |
apply (rule setprod_dvd_setprod_subset2) |
648 |
apply force |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
649 |
apply (subst prime_factors_altdef_int)+ |
31719 | 650 |
apply auto |
40461 | 651 |
apply (metis le_imp_power_dvd prime_factors_ge_0_int) |
44872 | 652 |
done |
31719 | 653 |
|
60527 | 654 |
lemma multiplicity_dvd'_nat: |
655 |
fixes x y :: nat |
|
62349
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
656 |
assumes "0 < x" |
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
657 |
assumes "\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y" |
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
658 |
shows "x dvd y" |
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
659 |
using dvd_0_right assms by (metis (no_types) le0 multiplicity_dvd_nat multiplicity_nonprime_nat not_gr0) |
31719 | 660 |
|
60527 | 661 |
lemma multiplicity_dvd'_int: |
662 |
fixes x y :: int |
|
663 |
shows "0 < x \<Longrightarrow> 0 \<le> y \<Longrightarrow> |
|
31719 | 664 |
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y" |
62348 | 665 |
by (metis dvd_int_iff abs_of_nat multiplicity_dvd'_nat multiplicity_int_def nat_int |
60527 | 666 |
zero_le_imp_eq_int zero_less_imp_eq_int) |
31719 | 667 |
|
60527 | 668 |
lemma dvd_multiplicity_eq_nat: |
669 |
fixes x y :: nat |
|
670 |
shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
671 |
by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat) |
31719 | 672 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
673 |
lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> |
60527 | 674 |
(x dvd y) = (\<forall>p\<ge>0. multiplicity p x \<le> multiplicity p y)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
675 |
by (auto intro: dvd_multiplicity_int multiplicity_dvd_int) |
31719 | 676 |
|
60527 | 677 |
lemma prime_factors_altdef2_nat: |
678 |
fixes n :: nat |
|
679 |
shows "n > 0 \<Longrightarrow> p \<in> prime_factors n \<longleftrightarrow> prime p \<and> p dvd n" |
|
44872 | 680 |
apply (cases "prime p") |
31719 | 681 |
apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
682 |
apply (subst prime_factorization_nat [where n = n], assumption) |
60527 | 683 |
apply (rule dvd_trans) |
31719 | 684 |
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
|
685 |
apply (subst (asm) prime_factors_altdef_nat, force) |
59010 | 686 |
apply rule |
31719 | 687 |
apply auto |
60527 | 688 |
apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 |
689 |
le_antisym multiplicity_not_factor_nat multiplicity_prime_nat) |
|
44872 | 690 |
done |
31719 | 691 |
|
60527 | 692 |
lemma prime_factors_altdef2_int: |
693 |
fixes n :: int |
|
694 |
assumes "n > 0" |
|
695 |
shows "p \<in> prime_factors n \<longleftrightarrow> prime p \<and> p dvd n" |
|
696 |
using assms by (simp add: prime_factors_altdef2_nat [transferred]) |
|
31719 | 697 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
698 |
lemma multiplicity_eq_nat: |
60527 | 699 |
fixes x and y::nat |
700 |
assumes [arith]: "x > 0" "y > 0" |
|
701 |
and mult_eq [simp]: "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y" |
|
31719 | 702 |
shows "x = y" |
33657 | 703 |
apply (rule dvd_antisym) |
60527 | 704 |
apply (auto intro: multiplicity_dvd'_nat) |
44872 | 705 |
done |
31719 | 706 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
707 |
lemma multiplicity_eq_int: |
60527 | 708 |
fixes x y :: int |
709 |
assumes [arith]: "x > 0" "y > 0" |
|
710 |
and mult_eq [simp]: "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y" |
|
31719 | 711 |
shows "x = y" |
33657 | 712 |
apply (rule dvd_antisym [transferred]) |
60527 | 713 |
apply (auto intro: multiplicity_dvd'_int) |
44872 | 714 |
done |
31719 | 715 |
|
716 |
||
60526 | 717 |
subsection \<open>An application\<close> |
31719 | 718 |
|
60527 | 719 |
lemma gcd_eq_nat: |
720 |
fixes x y :: nat |
|
31719 | 721 |
assumes pos [arith]: "x > 0" "y > 0" |
60527 | 722 |
shows "gcd x y = |
723 |
(\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ min (multiplicity p x) (multiplicity p y))" |
|
724 |
(is "_ = ?z") |
|
31719 | 725 |
proof - |
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61714
diff
changeset
|
726 |
have [arith]: "?z > 0" |
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61714
diff
changeset
|
727 |
using prime_factors_gt_0_nat by auto |
60527 | 728 |
have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = min (multiplicity p x) (multiplicity p y)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
729 |
apply (subst multiplicity_prod_prime_powers_nat) |
41541 | 730 |
apply auto |
31719 | 731 |
done |
60527 | 732 |
have "?z dvd x" |
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61714
diff
changeset
|
733 |
by (intro multiplicity_dvd'_nat) (auto simp add: aux intro: prime_gt_0_nat) |
60527 | 734 |
moreover have "?z dvd y" |
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61714
diff
changeset
|
735 |
by (intro multiplicity_dvd'_nat) (auto simp add: aux intro: prime_gt_0_nat) |
60527 | 736 |
moreover have "w dvd x \<and> w dvd y \<longrightarrow> w dvd ?z" for w |
737 |
proof (cases "w = 0") |
|
738 |
case True |
|
739 |
then show ?thesis by simp |
|
740 |
next |
|
741 |
case False |
|
742 |
then show ?thesis |
|
743 |
apply auto |
|
744 |
apply (erule multiplicity_dvd'_nat) |
|
745 |
apply (auto intro: dvd_multiplicity_nat simp add: aux) |
|
746 |
done |
|
747 |
qed |
|
748 |
ultimately have "?z = gcd x y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
749 |
by (subst gcd_unique_nat [symmetric], blast) |
44872 | 750 |
then show ?thesis |
60527 | 751 |
by auto |
31719 | 752 |
qed |
753 |
||
60527 | 754 |
lemma lcm_eq_nat: |
31719 | 755 |
assumes pos [arith]: "x > 0" "y > 0" |
60527 | 756 |
shows "lcm (x::nat) y = |
757 |
(\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ max (multiplicity p x) (multiplicity p y))" |
|
758 |
(is "_ = ?z") |
|
31719 | 759 |
proof - |
60527 | 760 |
have [arith]: "?z > 0" |
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61714
diff
changeset
|
761 |
by (auto intro: prime_gt_0_nat) |
60527 | 762 |
have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = max (multiplicity p x) (multiplicity p y)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
763 |
apply (subst multiplicity_prod_prime_powers_nat) |
41541 | 764 |
apply auto |
31719 | 765 |
done |
60527 | 766 |
have "x dvd ?z" |
767 |
by (intro multiplicity_dvd'_nat) (auto simp add: aux) |
|
768 |
moreover have "y dvd ?z" |
|
769 |
by (intro multiplicity_dvd'_nat) (auto simp add: aux) |
|
770 |
moreover have "x dvd w \<and> y dvd w \<longrightarrow> ?z dvd w" for w |
|
771 |
proof (cases "w = 0") |
|
772 |
case True |
|
773 |
then show ?thesis by auto |
|
774 |
next |
|
775 |
case False |
|
776 |
then show ?thesis |
|
777 |
apply auto |
|
778 |
apply (rule multiplicity_dvd'_nat) |
|
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61714
diff
changeset
|
779 |
apply (auto intro: prime_gt_0_nat dvd_multiplicity_nat simp add: aux) |
60527 | 780 |
done |
781 |
qed |
|
782 |
ultimately have "?z = lcm x y" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
783 |
by (subst lcm_unique_nat [symmetric], blast) |
44872 | 784 |
then show ?thesis |
60527 | 785 |
by auto |
31719 | 786 |
qed |
787 |
||
60527 | 788 |
lemma multiplicity_gcd_nat: |
789 |
fixes p x y :: nat |
|
31719 | 790 |
assumes [arith]: "x > 0" "y > 0" |
60527 | 791 |
shows "multiplicity p (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
|
792 |
apply (subst gcd_eq_nat) |
31719 | 793 |
apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
794 |
apply (subst multiplicity_prod_prime_powers_nat) |
31719 | 795 |
apply auto |
44872 | 796 |
done |
31719 | 797 |
|
60527 | 798 |
lemma multiplicity_lcm_nat: |
799 |
fixes p x y :: nat |
|
31719 | 800 |
assumes [arith]: "x > 0" "y > 0" |
60527 | 801 |
shows "multiplicity p (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
|
802 |
apply (subst lcm_eq_nat) |
31719 | 803 |
apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
804 |
apply (subst multiplicity_prod_prime_powers_nat) |
31719 | 805 |
apply auto |
44872 | 806 |
done |
31719 | 807 |
|
60527 | 808 |
lemma gcd_lcm_distrib_nat: |
809 |
fixes x y z :: nat |
|
810 |
shows "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" |
|
811 |
apply (cases "x = 0 | y = 0 | z = 0") |
|
31719 | 812 |
apply auto |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
813 |
apply (rule multiplicity_eq_nat) |
44872 | 814 |
apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat lcm_pos_nat) |
815 |
done |
|
31719 | 816 |
|
60527 | 817 |
lemma gcd_lcm_distrib_int: |
818 |
fixes x y z :: int |
|
819 |
shows "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
820 |
apply (subst (1 2 3) gcd_abs_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
821 |
apply (subst lcm_abs_int) |
31719 | 822 |
apply (subst (2) abs_of_nonneg) |
823 |
apply force |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
824 |
apply (rule gcd_lcm_distrib_nat [transferred]) |
31719 | 825 |
apply auto |
44872 | 826 |
done |
31719 | 827 |
|
828 |
end |