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