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