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