author | wenzelm |
Sat, 04 Nov 2017 12:39:25 +0100 | |
changeset 67001 | b34fbf33a7ea |
parent 66938 | c78ff0aeba4c |
child 67051 | e7e54a0b9197 |
permissions | -rw-r--r-- |
65435 | 1 |
(* Title: HOL/Computational_Algebra/Factorial_Ring.thy |
63924 | 2 |
Author: Manuel Eberl, TU Muenchen |
60804 | 3 |
Author: Florian Haftmann, TU Muenchen |
4 |
*) |
|
5 |
||
6 |
section \<open>Factorial (semi)rings\<close> |
|
7 |
||
8 |
theory Factorial_Ring |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
9 |
imports |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
10 |
Main |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66276
diff
changeset
|
11 |
"HOL-Library.Multiset" |
63498 | 12 |
begin |
13 |
||
63924 | 14 |
subsection \<open>Irreducible and prime elements\<close> |
63498 | 15 |
|
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
16 |
(* TODO: Move ? *) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
17 |
lemma (in semiring_gcd) prod_coprime' [rule_format]: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
18 |
"(\<forall>i\<in>A. gcd a (f i) = 1) \<longrightarrow> gcd a (\<Prod>i\<in>A. f i) = 1" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
19 |
using prod_coprime[of A f a] by (simp add: gcd.commute) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
20 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
21 |
|
63498 | 22 |
context comm_semiring_1 |
62499 | 23 |
begin |
24 |
||
63498 | 25 |
definition irreducible :: "'a \<Rightarrow> bool" where |
26 |
"irreducible p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p = a * b \<longrightarrow> a dvd 1 \<or> b dvd 1)" |
|
27 |
||
28 |
lemma not_irreducible_zero [simp]: "\<not>irreducible 0" |
|
29 |
by (simp add: irreducible_def) |
|
30 |
||
31 |
lemma irreducible_not_unit: "irreducible p \<Longrightarrow> \<not>p dvd 1" |
|
32 |
by (simp add: irreducible_def) |
|
33 |
||
34 |
lemma not_irreducible_one [simp]: "\<not>irreducible 1" |
|
35 |
by (simp add: irreducible_def) |
|
36 |
||
37 |
lemma irreducibleI: |
|
38 |
"p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1) \<Longrightarrow> irreducible p" |
|
39 |
by (simp add: irreducible_def) |
|
40 |
||
41 |
lemma irreducibleD: "irreducible p \<Longrightarrow> p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1" |
|
42 |
by (simp add: irreducible_def) |
|
43 |
||
63633 | 44 |
definition prime_elem :: "'a \<Rightarrow> bool" where |
45 |
"prime_elem p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p dvd (a * b) \<longrightarrow> p dvd a \<or> p dvd b)" |
|
63498 | 46 |
|
63633 | 47 |
lemma not_prime_elem_zero [simp]: "\<not>prime_elem 0" |
48 |
by (simp add: prime_elem_def) |
|
63498 | 49 |
|
63633 | 50 |
lemma prime_elem_not_unit: "prime_elem p \<Longrightarrow> \<not>p dvd 1" |
51 |
by (simp add: prime_elem_def) |
|
63498 | 52 |
|
63633 | 53 |
lemma prime_elemI: |
54 |
"p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b) \<Longrightarrow> prime_elem p" |
|
55 |
by (simp add: prime_elem_def) |
|
63498 | 56 |
|
63633 | 57 |
lemma prime_elem_dvd_multD: |
58 |
"prime_elem p \<Longrightarrow> p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b" |
|
59 |
by (simp add: prime_elem_def) |
|
63498 | 60 |
|
63633 | 61 |
lemma prime_elem_dvd_mult_iff: |
62 |
"prime_elem p \<Longrightarrow> p dvd (a * b) \<longleftrightarrow> p dvd a \<or> p dvd b" |
|
63 |
by (auto simp: prime_elem_def) |
|
63498 | 64 |
|
63633 | 65 |
lemma not_prime_elem_one [simp]: |
66 |
"\<not> prime_elem 1" |
|
67 |
by (auto dest: prime_elem_not_unit) |
|
63498 | 68 |
|
63633 | 69 |
lemma prime_elem_not_zeroI: |
70 |
assumes "prime_elem p" |
|
63498 | 71 |
shows "p \<noteq> 0" |
72 |
using assms by (auto intro: ccontr) |
|
73 |
||
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
74 |
lemma prime_elem_dvd_power: |
63633 | 75 |
"prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x" |
76 |
by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1]) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
77 |
|
63633 | 78 |
lemma prime_elem_dvd_power_iff: |
79 |
"prime_elem p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x" |
|
80 |
by (auto dest: prime_elem_dvd_power intro: dvd_trans) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
81 |
|
63633 | 82 |
lemma prime_elem_imp_nonzero [simp]: |
83 |
"ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 0" |
|
84 |
unfolding ASSUMPTION_def by (rule prime_elem_not_zeroI) |
|
63498 | 85 |
|
63633 | 86 |
lemma prime_elem_imp_not_one [simp]: |
87 |
"ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 1" |
|
63498 | 88 |
unfolding ASSUMPTION_def by auto |
89 |
||
90 |
end |
|
91 |
||
62499 | 92 |
context algebraic_semidom |
60804 | 93 |
begin |
94 |
||
63633 | 95 |
lemma prime_elem_imp_irreducible: |
96 |
assumes "prime_elem p" |
|
63498 | 97 |
shows "irreducible p" |
98 |
proof (rule irreducibleI) |
|
99 |
fix a b |
|
100 |
assume p_eq: "p = a * b" |
|
101 |
with assms have nz: "a \<noteq> 0" "b \<noteq> 0" by auto |
|
102 |
from p_eq have "p dvd a * b" by simp |
|
63633 | 103 |
with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD) |
63498 | 104 |
with \<open>p = a * b\<close> have "a * b dvd 1 * b \<or> a * b dvd a * 1" by auto |
105 |
thus "a dvd 1 \<or> b dvd 1" |
|
106 |
by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)]) |
|
63633 | 107 |
qed (insert assms, simp_all add: prime_elem_def) |
63498 | 108 |
|
63924 | 109 |
lemma (in algebraic_semidom) unit_imp_no_irreducible_divisors: |
110 |
assumes "is_unit x" "irreducible p" |
|
111 |
shows "\<not>p dvd x" |
|
112 |
proof (rule notI) |
|
113 |
assume "p dvd x" |
|
114 |
with \<open>is_unit x\<close> have "is_unit p" |
|
115 |
by (auto intro: dvd_trans) |
|
116 |
with \<open>irreducible p\<close> show False |
|
117 |
by (simp add: irreducible_not_unit) |
|
118 |
qed |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
119 |
|
63924 | 120 |
lemma unit_imp_no_prime_divisors: |
121 |
assumes "is_unit x" "prime_elem p" |
|
122 |
shows "\<not>p dvd x" |
|
123 |
using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] . |
|
124 |
||
63633 | 125 |
lemma prime_elem_mono: |
126 |
assumes "prime_elem p" "\<not>q dvd 1" "q dvd p" |
|
127 |
shows "prime_elem q" |
|
63498 | 128 |
proof - |
129 |
from \<open>q dvd p\<close> obtain r where r: "p = q * r" by (elim dvdE) |
|
130 |
hence "p dvd q * r" by simp |
|
63633 | 131 |
with \<open>prime_elem p\<close> have "p dvd q \<or> p dvd r" by (rule prime_elem_dvd_multD) |
63498 | 132 |
hence "p dvd q" |
133 |
proof |
|
134 |
assume "p dvd r" |
|
135 |
then obtain s where s: "r = p * s" by (elim dvdE) |
|
136 |
from r have "p * 1 = p * (q * s)" by (subst (asm) s) (simp add: mult_ac) |
|
63633 | 137 |
with \<open>prime_elem p\<close> have "q dvd 1" |
63498 | 138 |
by (subst (asm) mult_cancel_left) auto |
139 |
with \<open>\<not>q dvd 1\<close> show ?thesis by contradiction |
|
140 |
qed |
|
141 |
||
142 |
show ?thesis |
|
63633 | 143 |
proof (rule prime_elemI) |
63498 | 144 |
fix a b assume "q dvd (a * b)" |
145 |
with \<open>p dvd q\<close> have "p dvd (a * b)" by (rule dvd_trans) |
|
63633 | 146 |
with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD) |
63498 | 147 |
with \<open>q dvd p\<close> show "q dvd a \<or> q dvd b" by (blast intro: dvd_trans) |
148 |
qed (insert assms, auto) |
|
62499 | 149 |
qed |
150 |
||
63498 | 151 |
lemma irreducibleD': |
152 |
assumes "irreducible a" "b dvd a" |
|
153 |
shows "a dvd b \<or> is_unit b" |
|
154 |
proof - |
|
155 |
from assms obtain c where c: "a = b * c" by (elim dvdE) |
|
156 |
from irreducibleD[OF assms(1) this] have "is_unit b \<or> is_unit c" . |
|
157 |
thus ?thesis by (auto simp: c mult_unit_dvd_iff) |
|
158 |
qed |
|
60804 | 159 |
|
63498 | 160 |
lemma irreducibleI': |
161 |
assumes "a \<noteq> 0" "\<not>is_unit a" "\<And>b. b dvd a \<Longrightarrow> a dvd b \<or> is_unit b" |
|
162 |
shows "irreducible a" |
|
163 |
proof (rule irreducibleI) |
|
164 |
fix b c assume a_eq: "a = b * c" |
|
165 |
hence "a dvd b \<or> is_unit b" by (intro assms) simp_all |
|
166 |
thus "is_unit b \<or> is_unit c" |
|
167 |
proof |
|
168 |
assume "a dvd b" |
|
169 |
hence "b * c dvd b * 1" by (simp add: a_eq) |
|
170 |
moreover from \<open>a \<noteq> 0\<close> a_eq have "b \<noteq> 0" by auto |
|
171 |
ultimately show ?thesis by (subst (asm) dvd_times_left_cancel_iff) auto |
|
172 |
qed blast |
|
173 |
qed (simp_all add: assms(1,2)) |
|
60804 | 174 |
|
63498 | 175 |
lemma irreducible_altdef: |
176 |
"irreducible x \<longleftrightarrow> x \<noteq> 0 \<and> \<not>is_unit x \<and> (\<forall>b. b dvd x \<longrightarrow> x dvd b \<or> is_unit b)" |
|
177 |
using irreducibleI'[of x] irreducibleD'[of x] irreducible_not_unit[of x] by auto |
|
60804 | 178 |
|
63633 | 179 |
lemma prime_elem_multD: |
180 |
assumes "prime_elem (a * b)" |
|
60804 | 181 |
shows "is_unit a \<or> is_unit b" |
182 |
proof - |
|
63633 | 183 |
from assms have "a \<noteq> 0" "b \<noteq> 0" by (auto dest!: prime_elem_not_zeroI) |
184 |
moreover from assms prime_elem_dvd_multD [of "a * b"] have "a * b dvd a \<or> a * b dvd b" |
|
60804 | 185 |
by auto |
186 |
ultimately show ?thesis |
|
187 |
using dvd_times_left_cancel_iff [of a b 1] |
|
188 |
dvd_times_right_cancel_iff [of b a 1] |
|
189 |
by auto |
|
190 |
qed |
|
191 |
||
63633 | 192 |
lemma prime_elemD2: |
193 |
assumes "prime_elem p" and "a dvd p" and "\<not> is_unit a" |
|
60804 | 194 |
shows "p dvd a" |
195 |
proof - |
|
196 |
from \<open>a dvd p\<close> obtain b where "p = a * b" .. |
|
63633 | 197 |
with \<open>prime_elem p\<close> prime_elem_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto |
60804 | 198 |
with \<open>p = a * b\<close> show ?thesis |
199 |
by (auto simp add: mult_unit_dvd_iff) |
|
200 |
qed |
|
201 |
||
63830 | 202 |
lemma prime_elem_dvd_prod_msetE: |
63633 | 203 |
assumes "prime_elem p" |
63830 | 204 |
assumes dvd: "p dvd prod_mset A" |
63633 | 205 |
obtains a where "a \<in># A" and "p dvd a" |
206 |
proof - |
|
207 |
from dvd have "\<exists>a. a \<in># A \<and> p dvd a" |
|
208 |
proof (induct A) |
|
209 |
case empty then show ?case |
|
210 |
using \<open>prime_elem p\<close> by (simp add: prime_elem_not_unit) |
|
211 |
next |
|
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63633
diff
changeset
|
212 |
case (add a A) |
63830 | 213 |
then have "p dvd a * prod_mset A" by simp |
214 |
with \<open>prime_elem p\<close> consider (A) "p dvd prod_mset A" | (B) "p dvd a" |
|
63633 | 215 |
by (blast dest: prime_elem_dvd_multD) |
216 |
then show ?case proof cases |
|
217 |
case B then show ?thesis by auto |
|
218 |
next |
|
219 |
case A |
|
220 |
with add.hyps obtain b where "b \<in># A" "p dvd b" |
|
221 |
by auto |
|
222 |
then show ?thesis by auto |
|
223 |
qed |
|
224 |
qed |
|
225 |
with that show thesis by blast |
|
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
226 |
|
63633 | 227 |
qed |
228 |
||
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
229 |
context |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
230 |
begin |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
231 |
|
63633 | 232 |
private lemma prime_elem_powerD: |
233 |
assumes "prime_elem (p ^ n)" |
|
234 |
shows "prime_elem p \<and> n = 1" |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
235 |
proof (cases n) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
236 |
case (Suc m) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
237 |
note assms |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
238 |
also from Suc have "p ^ n = p * p^m" by simp |
63633 | 239 |
finally have "is_unit p \<or> is_unit (p^m)" by (rule prime_elem_multD) |
240 |
moreover from assms have "\<not>is_unit p" by (simp add: prime_elem_def is_unit_power_iff) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
241 |
ultimately have "is_unit (p ^ m)" by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
242 |
with \<open>\<not>is_unit p\<close> have "m = 0" by (simp add: is_unit_power_iff) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
243 |
with Suc assms show ?thesis by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
244 |
qed (insert assms, simp_all) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
245 |
|
63633 | 246 |
lemma prime_elem_power_iff: |
247 |
"prime_elem (p ^ n) \<longleftrightarrow> prime_elem p \<and> n = 1" |
|
248 |
by (auto dest: prime_elem_powerD) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
249 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
250 |
end |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
251 |
|
63498 | 252 |
lemma irreducible_mult_unit_left: |
253 |
"is_unit a \<Longrightarrow> irreducible (a * p) \<longleftrightarrow> irreducible p" |
|
254 |
by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff |
|
255 |
mult_unit_dvd_iff dvd_mult_unit_iff) |
|
256 |
||
63633 | 257 |
lemma prime_elem_mult_unit_left: |
258 |
"is_unit a \<Longrightarrow> prime_elem (a * p) \<longleftrightarrow> prime_elem p" |
|
259 |
by (auto simp: prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff) |
|
63498 | 260 |
|
63633 | 261 |
lemma prime_elem_dvd_cases: |
262 |
assumes pk: "p*k dvd m*n" and p: "prime_elem p" |
|
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
263 |
shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
264 |
proof - |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
265 |
have "p dvd m*n" using dvd_mult_left pk by blast |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
266 |
then consider "p dvd m" | "p dvd n" |
63633 | 267 |
using p prime_elem_dvd_mult_iff by blast |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
268 |
then show ?thesis |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
269 |
proof cases |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
270 |
case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
271 |
then have "\<exists>x. k dvd x * n \<and> m = p * x" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
272 |
using p pk by (auto simp: mult.assoc) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
273 |
then show ?thesis .. |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
274 |
next |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
275 |
case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) |
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
276 |
with p pk have "\<exists>y. k dvd m*y \<and> n = p*y" |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
277 |
by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
278 |
then show ?thesis .. |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
279 |
qed |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
280 |
qed |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
281 |
|
63633 | 282 |
lemma prime_elem_power_dvd_prod: |
283 |
assumes pc: "p^c dvd m*n" and p: "prime_elem p" |
|
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
284 |
shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
285 |
using pc |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
286 |
proof (induct c arbitrary: m n) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
287 |
case 0 show ?case by simp |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
288 |
next |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
289 |
case (Suc c) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
290 |
consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y" |
63633 | 291 |
using prime_elem_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
292 |
then show ?case |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
293 |
proof cases |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
294 |
case (1 x) |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
295 |
with Suc.hyps[of x n] obtain a b where "a + b = c \<and> p ^ a dvd x \<and> p ^ b dvd n" by blast |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
296 |
with 1 have "Suc a + b = Suc c \<and> p ^ Suc a dvd m \<and> p ^ b dvd n" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
297 |
by (auto intro: mult_dvd_mono) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
298 |
thus ?thesis by blast |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
299 |
next |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
300 |
case (2 y) |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
301 |
with Suc.hyps[of m y] obtain a b where "a + b = c \<and> p ^ a dvd m \<and> p ^ b dvd y" by blast |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
302 |
with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
303 |
by (auto intro: mult_dvd_mono) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
304 |
with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
305 |
by force |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
306 |
qed |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
307 |
qed |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
308 |
|
63633 | 309 |
lemma prime_elem_power_dvd_cases: |
63924 | 310 |
assumes "p ^ c dvd m * n" and "a + b = Suc c" and "prime_elem p" |
311 |
shows "p ^ a dvd m \<or> p ^ b dvd n" |
|
312 |
proof - |
|
313 |
from assms obtain r s |
|
314 |
where "r + s = c \<and> p ^ r dvd m \<and> p ^ s dvd n" |
|
315 |
by (blast dest: prime_elem_power_dvd_prod) |
|
316 |
moreover with assms have |
|
317 |
"a \<le> r \<or> b \<le> s" by arith |
|
318 |
ultimately show ?thesis by (auto intro: power_le_dvd) |
|
319 |
qed |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
320 |
|
63633 | 321 |
lemma prime_elem_not_unit' [simp]: |
322 |
"ASSUMPTION (prime_elem x) \<Longrightarrow> \<not>is_unit x" |
|
323 |
unfolding ASSUMPTION_def by (rule prime_elem_not_unit) |
|
63498 | 324 |
|
63633 | 325 |
lemma prime_elem_dvd_power_iff: |
326 |
assumes "prime_elem p" |
|
62499 | 327 |
shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0" |
63633 | 328 |
using assms by (induct n) (auto dest: prime_elem_not_unit prime_elem_dvd_multD) |
62499 | 329 |
|
330 |
lemma prime_power_dvd_multD: |
|
63633 | 331 |
assumes "prime_elem p" |
62499 | 332 |
assumes "p ^ n dvd a * b" and "n > 0" and "\<not> p dvd a" |
333 |
shows "p ^ n dvd b" |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
334 |
using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close> |
63633 | 335 |
proof (induct n arbitrary: b) |
62499 | 336 |
case 0 then show ?case by simp |
337 |
next |
|
338 |
case (Suc n) show ?case |
|
339 |
proof (cases "n = 0") |
|
63633 | 340 |
case True with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> show ?thesis |
341 |
by (simp add: prime_elem_dvd_mult_iff) |
|
62499 | 342 |
next |
343 |
case False then have "n > 0" by simp |
|
63633 | 344 |
from \<open>prime_elem p\<close> have "p \<noteq> 0" by auto |
62499 | 345 |
from Suc.prems have *: "p * p ^ n dvd a * b" |
346 |
by simp |
|
347 |
then have "p dvd a * b" |
|
348 |
by (rule dvd_mult_left) |
|
63633 | 349 |
with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> have "p dvd b" |
350 |
by (simp add: prime_elem_dvd_mult_iff) |
|
63040 | 351 |
moreover define c where "c = b div p" |
62499 | 352 |
ultimately have b: "b = p * c" by simp |
353 |
with * have "p * p ^ n dvd p * (a * c)" |
|
354 |
by (simp add: ac_simps) |
|
355 |
with \<open>p \<noteq> 0\<close> have "p ^ n dvd a * c" |
|
356 |
by simp |
|
357 |
with Suc.hyps \<open>n > 0\<close> have "p ^ n dvd c" |
|
358 |
by blast |
|
359 |
with \<open>p \<noteq> 0\<close> show ?thesis |
|
360 |
by (simp add: b) |
|
361 |
qed |
|
362 |
qed |
|
363 |
||
63633 | 364 |
end |
365 |
||
63924 | 366 |
|
367 |
subsection \<open>Generalized primes: normalized prime elements\<close> |
|
368 |
||
63633 | 369 |
context normalization_semidom |
370 |
begin |
|
371 |
||
63924 | 372 |
lemma irreducible_normalized_divisors: |
373 |
assumes "irreducible x" "y dvd x" "normalize y = y" |
|
374 |
shows "y = 1 \<or> y = normalize x" |
|
375 |
proof - |
|
376 |
from assms have "is_unit y \<or> x dvd y" by (auto simp: irreducible_altdef) |
|
377 |
thus ?thesis |
|
378 |
proof (elim disjE) |
|
379 |
assume "is_unit y" |
|
380 |
hence "normalize y = 1" by (simp add: is_unit_normalize) |
|
381 |
with assms show ?thesis by simp |
|
382 |
next |
|
383 |
assume "x dvd y" |
|
384 |
with \<open>y dvd x\<close> have "normalize y = normalize x" by (rule associatedI) |
|
385 |
with assms show ?thesis by simp |
|
386 |
qed |
|
387 |
qed |
|
388 |
||
63633 | 389 |
lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x" |
390 |
using irreducible_mult_unit_left[of "1 div unit_factor x" x] |
|
391 |
by (cases "x = 0") (simp_all add: unit_div_commute) |
|
392 |
||
393 |
lemma prime_elem_normalize_iff [simp]: "prime_elem (normalize x) = prime_elem x" |
|
394 |
using prime_elem_mult_unit_left[of "1 div unit_factor x" x] |
|
395 |
by (cases "x = 0") (simp_all add: unit_div_commute) |
|
396 |
||
397 |
lemma prime_elem_associated: |
|
398 |
assumes "prime_elem p" and "prime_elem q" and "q dvd p" |
|
399 |
shows "normalize q = normalize p" |
|
400 |
using \<open>q dvd p\<close> proof (rule associatedI) |
|
401 |
from \<open>prime_elem q\<close> have "\<not> is_unit q" |
|
402 |
by (auto simp add: prime_elem_not_unit) |
|
403 |
with \<open>prime_elem p\<close> \<open>q dvd p\<close> show "p dvd q" |
|
404 |
by (blast intro: prime_elemD2) |
|
405 |
qed |
|
406 |
||
407 |
definition prime :: "'a \<Rightarrow> bool" where |
|
408 |
"prime p \<longleftrightarrow> prime_elem p \<and> normalize p = p" |
|
409 |
||
410 |
lemma not_prime_0 [simp]: "\<not>prime 0" by (simp add: prime_def) |
|
411 |
||
412 |
lemma not_prime_unit: "is_unit x \<Longrightarrow> \<not>prime x" |
|
413 |
using prime_elem_not_unit[of x] by (auto simp add: prime_def) |
|
414 |
||
415 |
lemma not_prime_1 [simp]: "\<not>prime 1" by (simp add: not_prime_unit) |
|
416 |
||
417 |
lemma primeI: "prime_elem x \<Longrightarrow> normalize x = x \<Longrightarrow> prime x" |
|
418 |
by (simp add: prime_def) |
|
419 |
||
420 |
lemma prime_imp_prime_elem [dest]: "prime p \<Longrightarrow> prime_elem p" |
|
421 |
by (simp add: prime_def) |
|
422 |
||
423 |
lemma normalize_prime: "prime p \<Longrightarrow> normalize p = p" |
|
424 |
by (simp add: prime_def) |
|
425 |
||
426 |
lemma prime_normalize_iff [simp]: "prime (normalize p) \<longleftrightarrow> prime_elem p" |
|
427 |
by (auto simp add: prime_def) |
|
428 |
||
429 |
lemma prime_power_iff: |
|
430 |
"prime (p ^ n) \<longleftrightarrow> prime p \<and> n = 1" |
|
431 |
by (auto simp: prime_def prime_elem_power_iff) |
|
432 |
||
433 |
lemma prime_imp_nonzero [simp]: |
|
434 |
"ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 0" |
|
435 |
unfolding ASSUMPTION_def prime_def by auto |
|
436 |
||
437 |
lemma prime_imp_not_one [simp]: |
|
438 |
"ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 1" |
|
439 |
unfolding ASSUMPTION_def by auto |
|
440 |
||
441 |
lemma prime_not_unit' [simp]: |
|
442 |
"ASSUMPTION (prime x) \<Longrightarrow> \<not>is_unit x" |
|
443 |
unfolding ASSUMPTION_def prime_def by auto |
|
444 |
||
445 |
lemma prime_normalize' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> normalize x = x" |
|
446 |
unfolding ASSUMPTION_def prime_def by simp |
|
447 |
||
448 |
lemma unit_factor_prime: "prime x \<Longrightarrow> unit_factor x = 1" |
|
449 |
using unit_factor_normalize[of x] unfolding prime_def by auto |
|
450 |
||
451 |
lemma unit_factor_prime' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> unit_factor x = 1" |
|
452 |
unfolding ASSUMPTION_def by (rule unit_factor_prime) |
|
453 |
||
454 |
lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> prime_elem x" |
|
455 |
by (simp add: prime_def ASSUMPTION_def) |
|
456 |
||
457 |
lemma prime_dvd_multD: "prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b" |
|
458 |
by (intro prime_elem_dvd_multD) simp_all |
|
459 |
||
64631
7705926ee595
removed dangerous simp rule: prime computations can be excessively long
haftmann
parents:
64272
diff
changeset
|
460 |
lemma prime_dvd_mult_iff: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b" |
63633 | 461 |
by (auto dest: prime_dvd_multD) |
462 |
||
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
463 |
lemma prime_dvd_power: |
63633 | 464 |
"prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x" |
465 |
by (auto dest!: prime_elem_dvd_power simp: prime_def) |
|
466 |
||
467 |
lemma prime_dvd_power_iff: |
|
468 |
"prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x" |
|
469 |
by (subst prime_elem_dvd_power_iff) simp_all |
|
470 |
||
63830 | 471 |
lemma prime_dvd_prod_mset_iff: "prime p \<Longrightarrow> p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" |
63633 | 472 |
by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+) |
473 |
||
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
474 |
lemma prime_dvd_prod_iff: "finite A \<Longrightarrow> prime p \<Longrightarrow> p dvd prod f A \<longleftrightarrow> (\<exists>x\<in>A. p dvd f x)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
475 |
by (auto simp: prime_dvd_prod_mset_iff prod_unfold_prod_mset) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
476 |
|
63633 | 477 |
lemma primes_dvd_imp_eq: |
478 |
assumes "prime p" "prime q" "p dvd q" |
|
479 |
shows "p = q" |
|
480 |
proof - |
|
481 |
from assms have "irreducible q" by (simp add: prime_elem_imp_irreducible prime_def) |
|
482 |
from irreducibleD'[OF this \<open>p dvd q\<close>] assms have "q dvd p" by simp |
|
483 |
with \<open>p dvd q\<close> have "normalize p = normalize q" by (rule associatedI) |
|
484 |
with assms show "p = q" by simp |
|
485 |
qed |
|
486 |
||
63830 | 487 |
lemma prime_dvd_prod_mset_primes_iff: |
63633 | 488 |
assumes "prime p" "\<And>q. q \<in># A \<Longrightarrow> prime q" |
63830 | 489 |
shows "p dvd prod_mset A \<longleftrightarrow> p \<in># A" |
63633 | 490 |
proof - |
63830 | 491 |
from assms(1) have "p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" by (rule prime_dvd_prod_mset_iff) |
63633 | 492 |
also from assms have "\<dots> \<longleftrightarrow> p \<in># A" by (auto dest: primes_dvd_imp_eq) |
493 |
finally show ?thesis . |
|
494 |
qed |
|
495 |
||
63830 | 496 |
lemma prod_mset_primes_dvd_imp_subset: |
497 |
assumes "prod_mset A dvd prod_mset B" "\<And>p. p \<in># A \<Longrightarrow> prime p" "\<And>p. p \<in># B \<Longrightarrow> prime p" |
|
63633 | 498 |
shows "A \<subseteq># B" |
499 |
using assms |
|
500 |
proof (induction A arbitrary: B) |
|
501 |
case empty |
|
502 |
thus ?case by simp |
|
503 |
next |
|
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63633
diff
changeset
|
504 |
case (add p A B) |
63633 | 505 |
hence p: "prime p" by simp |
506 |
define B' where "B' = B - {#p#}" |
|
63830 | 507 |
from add.prems have "p dvd prod_mset B" by (simp add: dvd_mult_left) |
63633 | 508 |
with add.prems have "p \<in># B" |
63830 | 509 |
by (subst (asm) (2) prime_dvd_prod_mset_primes_iff) simp_all |
63633 | 510 |
hence B: "B = B' + {#p#}" by (simp add: B'_def) |
511 |
from add.prems p have "A \<subseteq># B'" by (intro add.IH) (simp_all add: B) |
|
512 |
thus ?case by (simp add: B) |
|
513 |
qed |
|
514 |
||
63830 | 515 |
lemma normalize_prod_mset_primes: |
516 |
"(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (prod_mset A) = prod_mset A" |
|
63633 | 517 |
proof (induction A) |
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63633
diff
changeset
|
518 |
case (add p A) |
63633 | 519 |
hence "prime p" by simp |
520 |
hence "normalize p = p" by simp |
|
521 |
with add show ?case by (simp add: normalize_mult) |
|
522 |
qed simp_all |
|
523 |
||
63830 | 524 |
lemma prod_mset_dvd_prod_mset_primes_iff: |
63633 | 525 |
assumes "\<And>x. x \<in># A \<Longrightarrow> prime x" "\<And>x. x \<in># B \<Longrightarrow> prime x" |
63830 | 526 |
shows "prod_mset A dvd prod_mset B \<longleftrightarrow> A \<subseteq># B" |
527 |
using assms by (auto intro: prod_mset_subset_imp_dvd prod_mset_primes_dvd_imp_subset) |
|
63633 | 528 |
|
63830 | 529 |
lemma is_unit_prod_mset_primes_iff: |
63633 | 530 |
assumes "\<And>x. x \<in># A \<Longrightarrow> prime x" |
63830 | 531 |
shows "is_unit (prod_mset A) \<longleftrightarrow> A = {#}" |
63924 | 532 |
by (auto simp add: is_unit_prod_mset_iff) |
533 |
(meson all_not_in_conv assms not_prime_unit set_mset_eq_empty_iff) |
|
63498 | 534 |
|
63830 | 535 |
lemma prod_mset_primes_irreducible_imp_prime: |
536 |
assumes irred: "irreducible (prod_mset A)" |
|
63633 | 537 |
assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x" |
538 |
assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x" |
|
539 |
assumes C: "\<And>x. x \<in># C \<Longrightarrow> prime x" |
|
63830 | 540 |
assumes dvd: "prod_mset A dvd prod_mset B * prod_mset C" |
541 |
shows "prod_mset A dvd prod_mset B \<or> prod_mset A dvd prod_mset C" |
|
63498 | 542 |
proof - |
63830 | 543 |
from dvd have "prod_mset A dvd prod_mset (B + C)" |
63498 | 544 |
by simp |
545 |
with A B C have subset: "A \<subseteq># B + C" |
|
63830 | 546 |
by (subst (asm) prod_mset_dvd_prod_mset_primes_iff) auto |
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
547 |
define A1 and A2 where "A1 = A \<inter># B" and "A2 = A - A1" |
63498 | 548 |
have "A = A1 + A2" unfolding A1_def A2_def |
549 |
by (rule sym, intro subset_mset.add_diff_inverse) simp_all |
|
550 |
from subset have "A1 \<subseteq># B" "A2 \<subseteq># C" |
|
551 |
by (auto simp: A1_def A2_def Multiset.subset_eq_diff_conv Multiset.union_commute) |
|
63830 | 552 |
from \<open>A = A1 + A2\<close> have "prod_mset A = prod_mset A1 * prod_mset A2" by simp |
553 |
from irred and this have "is_unit (prod_mset A1) \<or> is_unit (prod_mset A2)" |
|
63498 | 554 |
by (rule irreducibleD) |
555 |
with A have "A1 = {#} \<or> A2 = {#}" unfolding A1_def A2_def |
|
63830 | 556 |
by (subst (asm) (1 2) is_unit_prod_mset_primes_iff) (auto dest: Multiset.in_diffD) |
63498 | 557 |
with dvd \<open>A = A1 + A2\<close> \<open>A1 \<subseteq># B\<close> \<open>A2 \<subseteq># C\<close> show ?thesis |
63830 | 558 |
by (auto intro: prod_mset_subset_imp_dvd) |
63498 | 559 |
qed |
560 |
||
63830 | 561 |
lemma prod_mset_primes_finite_divisor_powers: |
63633 | 562 |
assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x" |
563 |
assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x" |
|
63498 | 564 |
assumes "A \<noteq> {#}" |
63830 | 565 |
shows "finite {n. prod_mset A ^ n dvd prod_mset B}" |
63498 | 566 |
proof - |
567 |
from \<open>A \<noteq> {#}\<close> obtain x where x: "x \<in># A" by blast |
|
568 |
define m where "m = count B x" |
|
63830 | 569 |
have "{n. prod_mset A ^ n dvd prod_mset B} \<subseteq> {..m}" |
63498 | 570 |
proof safe |
63830 | 571 |
fix n assume dvd: "prod_mset A ^ n dvd prod_mset B" |
572 |
from x have "x ^ n dvd prod_mset A ^ n" by (intro dvd_power_same dvd_prod_mset) |
|
63498 | 573 |
also note dvd |
63830 | 574 |
also have "x ^ n = prod_mset (replicate_mset n x)" by simp |
63498 | 575 |
finally have "replicate_mset n x \<subseteq># B" |
63830 | 576 |
by (rule prod_mset_primes_dvd_imp_subset) (insert A B x, simp_all split: if_splits) |
63498 | 577 |
thus "n \<le> m" by (simp add: count_le_replicate_mset_subset_eq m_def) |
60804 | 578 |
qed |
63498 | 579 |
moreover have "finite {..m}" by simp |
580 |
ultimately show ?thesis by (rule finite_subset) |
|
581 |
qed |
|
582 |
||
63924 | 583 |
end |
63498 | 584 |
|
63924 | 585 |
|
586 |
subsection \<open>In a semiring with GCD, each irreducible element is a prime elements\<close> |
|
63498 | 587 |
|
588 |
context semiring_gcd |
|
589 |
begin |
|
590 |
||
63633 | 591 |
lemma irreducible_imp_prime_elem_gcd: |
63498 | 592 |
assumes "irreducible x" |
63633 | 593 |
shows "prime_elem x" |
594 |
proof (rule prime_elemI) |
|
63498 | 595 |
fix a b assume "x dvd a * b" |
596 |
from dvd_productE[OF this] obtain y z where yz: "x = y * z" "y dvd a" "z dvd b" . |
|
597 |
from \<open>irreducible x\<close> and \<open>x = y * z\<close> have "is_unit y \<or> is_unit z" by (rule irreducibleD) |
|
598 |
with yz show "x dvd a \<or> x dvd b" |
|
599 |
by (auto simp: mult_unit_dvd_iff mult_unit_dvd_iff') |
|
600 |
qed (insert assms, auto simp: irreducible_not_unit) |
|
601 |
||
63633 | 602 |
lemma prime_elem_imp_coprime: |
603 |
assumes "prime_elem p" "\<not>p dvd n" |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
604 |
shows "coprime p n" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
605 |
proof (rule coprimeI) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
606 |
fix d assume "d dvd p" "d dvd n" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
607 |
show "is_unit d" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
608 |
proof (rule ccontr) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
609 |
assume "\<not>is_unit d" |
63633 | 610 |
from \<open>prime_elem p\<close> and \<open>d dvd p\<close> and this have "p dvd d" |
611 |
by (rule prime_elemD2) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
612 |
from this and \<open>d dvd n\<close> have "p dvd n" by (rule dvd_trans) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
613 |
with \<open>\<not>p dvd n\<close> show False by contradiction |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
614 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
615 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
616 |
|
63633 | 617 |
lemma prime_imp_coprime: |
618 |
assumes "prime p" "\<not>p dvd n" |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
619 |
shows "coprime p n" |
63633 | 620 |
using assms by (simp add: prime_elem_imp_coprime) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
621 |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
622 |
lemma prime_elem_imp_power_coprime: |
63633 | 623 |
"prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)" |
624 |
by (auto intro!: coprime_exp dest: prime_elem_imp_coprime simp: gcd.commute) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
625 |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
626 |
lemma prime_imp_power_coprime: |
63633 | 627 |
"prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)" |
628 |
by (simp add: prime_elem_imp_power_coprime) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
629 |
|
63633 | 630 |
lemma prime_elem_divprod_pow: |
631 |
assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b" |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
632 |
shows "p^n dvd a \<or> p^n dvd b" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
633 |
using assms |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
634 |
proof - |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
635 |
from ab p have "\<not>p dvd a \<or> \<not>p dvd b" |
63633 | 636 |
by (auto simp: coprime prime_elem_def) |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
637 |
with p have "coprime (p^n) a \<or> coprime (p^n) b" |
63633 | 638 |
by (auto intro: prime_elem_imp_coprime coprime_exp_left) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
639 |
with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
640 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
641 |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
642 |
lemma primes_coprime: |
63633 | 643 |
"prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q" |
644 |
using prime_imp_coprime primes_dvd_imp_eq by blast |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
645 |
|
63498 | 646 |
end |
647 |
||
648 |
||
63924 | 649 |
subsection \<open>Factorial semirings: algebraic structures with unique prime factorizations\<close> |
650 |
||
63498 | 651 |
class factorial_semiring = normalization_semidom + |
652 |
assumes prime_factorization_exists: |
|
63924 | 653 |
"x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x" |
654 |
||
655 |
text \<open>Alternative characterization\<close> |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
656 |
|
63924 | 657 |
lemma (in normalization_semidom) factorial_semiring_altI_aux: |
658 |
assumes finite_divisors: "\<And>x. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}" |
|
659 |
assumes irreducible_imp_prime_elem: "\<And>x. irreducible x \<Longrightarrow> prime_elem x" |
|
660 |
assumes "x \<noteq> 0" |
|
661 |
shows "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x" |
|
662 |
using \<open>x \<noteq> 0\<close> |
|
663 |
proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct) |
|
664 |
case (less a) |
|
665 |
let ?fctrs = "\<lambda>a. {b. b dvd a \<and> normalize b = b}" |
|
666 |
show ?case |
|
667 |
proof (cases "is_unit a") |
|
668 |
case True |
|
669 |
thus ?thesis by (intro exI[of _ "{#}"]) (auto simp: is_unit_normalize) |
|
670 |
next |
|
671 |
case False |
|
672 |
show ?thesis |
|
673 |
proof (cases "\<exists>b. b dvd a \<and> \<not>is_unit b \<and> \<not>a dvd b") |
|
674 |
case False |
|
675 |
with \<open>\<not>is_unit a\<close> less.prems have "irreducible a" by (auto simp: irreducible_altdef) |
|
676 |
hence "prime_elem a" by (rule irreducible_imp_prime_elem) |
|
677 |
thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto |
|
678 |
next |
|
679 |
case True |
|
680 |
then guess b by (elim exE conjE) note b = this |
|
681 |
||
682 |
from b have "?fctrs b \<subseteq> ?fctrs a" by (auto intro: dvd_trans) |
|
683 |
moreover from b have "normalize a \<notin> ?fctrs b" "normalize a \<in> ?fctrs a" by simp_all |
|
684 |
hence "?fctrs b \<noteq> ?fctrs a" by blast |
|
685 |
ultimately have "?fctrs b \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast |
|
686 |
with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)" |
|
687 |
by (rule psubset_card_mono) |
|
688 |
moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto |
|
689 |
ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize b" |
|
690 |
by (intro less) auto |
|
691 |
then guess A .. note A = this |
|
692 |
||
693 |
define c where "c = a div b" |
|
694 |
from b have c: "a = b * c" by (simp add: c_def) |
|
695 |
from less.prems c have "c \<noteq> 0" by auto |
|
696 |
from b c have "?fctrs c \<subseteq> ?fctrs a" by (auto intro: dvd_trans) |
|
697 |
moreover have "normalize a \<notin> ?fctrs c" |
|
698 |
proof safe |
|
699 |
assume "normalize a dvd c" |
|
700 |
hence "b * c dvd 1 * c" by (simp add: c) |
|
701 |
hence "b dvd 1" by (subst (asm) dvd_times_right_cancel_iff) fact+ |
|
702 |
with b show False by simp |
|
703 |
qed |
|
704 |
with \<open>normalize a \<in> ?fctrs a\<close> have "?fctrs a \<noteq> ?fctrs c" by blast |
|
705 |
ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast |
|
706 |
with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)" |
|
707 |
by (rule psubset_card_mono) |
|
708 |
with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize c" |
|
709 |
by (intro less) auto |
|
710 |
then guess B .. note B = this |
|
711 |
||
712 |
from A B show ?thesis by (intro exI[of _ "A + B"]) (auto simp: c normalize_mult) |
|
713 |
qed |
|
714 |
qed |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
715 |
qed |
63924 | 716 |
|
717 |
lemma factorial_semiring_altI: |
|
718 |
assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}" |
|
719 |
assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x" |
|
720 |
shows "OFCLASS('a :: normalization_semidom, factorial_semiring_class)" |
|
721 |
by intro_classes (rule factorial_semiring_altI_aux[OF assms]) |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
722 |
|
63924 | 723 |
text \<open>Properties\<close> |
724 |
||
725 |
context factorial_semiring |
|
63498 | 726 |
begin |
727 |
||
728 |
lemma prime_factorization_exists': |
|
729 |
assumes "x \<noteq> 0" |
|
63830 | 730 |
obtains A where "\<And>x. x \<in># A \<Longrightarrow> prime x" "prod_mset A = normalize x" |
63498 | 731 |
proof - |
732 |
from prime_factorization_exists[OF assms] obtain A |
|
63830 | 733 |
where A: "\<And>x. x \<in># A \<Longrightarrow> prime_elem x" "prod_mset A = normalize x" by blast |
63498 | 734 |
define A' where "A' = image_mset normalize A" |
63830 | 735 |
have "prod_mset A' = normalize (prod_mset A)" |
736 |
by (simp add: A'_def normalize_prod_mset) |
|
63498 | 737 |
also note A(2) |
63830 | 738 |
finally have "prod_mset A' = normalize x" by simp |
63633 | 739 |
moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> prime x" by (auto simp: prime_def A'_def) |
63498 | 740 |
ultimately show ?thesis by (intro that[of A']) blast |
741 |
qed |
|
742 |
||
63633 | 743 |
lemma irreducible_imp_prime_elem: |
63498 | 744 |
assumes "irreducible x" |
63633 | 745 |
shows "prime_elem x" |
746 |
proof (rule prime_elemI) |
|
63498 | 747 |
fix a b assume dvd: "x dvd a * b" |
748 |
from assms have "x \<noteq> 0" by auto |
|
749 |
show "x dvd a \<or> x dvd b" |
|
750 |
proof (cases "a = 0 \<or> b = 0") |
|
751 |
case False |
|
752 |
hence "a \<noteq> 0" "b \<noteq> 0" by blast+ |
|
753 |
note nz = \<open>x \<noteq> 0\<close> this |
|
754 |
from nz[THEN prime_factorization_exists'] guess A B C . note ABC = this |
|
63830 | 755 |
from assms ABC have "irreducible (prod_mset A)" by simp |
756 |
from dvd prod_mset_primes_irreducible_imp_prime[of A B C, OF this ABC(1,3,5)] ABC(2,4,6) |
|
63498 | 757 |
show ?thesis by (simp add: normalize_mult [symmetric]) |
758 |
qed auto |
|
759 |
qed (insert assms, simp_all add: irreducible_def) |
|
760 |
||
761 |
lemma finite_divisor_powers: |
|
762 |
assumes "y \<noteq> 0" "\<not>is_unit x" |
|
763 |
shows "finite {n. x ^ n dvd y}" |
|
764 |
proof (cases "x = 0") |
|
765 |
case True |
|
766 |
with assms have "{n. x ^ n dvd y} = {0}" by (auto simp: power_0_left) |
|
767 |
thus ?thesis by simp |
|
768 |
next |
|
769 |
case False |
|
770 |
note nz = this \<open>y \<noteq> 0\<close> |
|
771 |
from nz[THEN prime_factorization_exists'] guess A B . note AB = this |
|
772 |
from AB assms have "A \<noteq> {#}" by (auto simp: normalize_1_iff) |
|
63830 | 773 |
from AB(2,4) prod_mset_primes_finite_divisor_powers [of A B, OF AB(1,3) this] |
63498 | 774 |
show ?thesis by (simp add: normalize_power [symmetric]) |
775 |
qed |
|
776 |
||
777 |
lemma finite_prime_divisors: |
|
778 |
assumes "x \<noteq> 0" |
|
63633 | 779 |
shows "finite {p. prime p \<and> p dvd x}" |
63498 | 780 |
proof - |
781 |
from prime_factorization_exists'[OF assms] guess A . note A = this |
|
63633 | 782 |
have "{p. prime p \<and> p dvd x} \<subseteq> set_mset A" |
63498 | 783 |
proof safe |
63633 | 784 |
fix p assume p: "prime p" and dvd: "p dvd x" |
63498 | 785 |
from dvd have "p dvd normalize x" by simp |
63830 | 786 |
also from A have "normalize x = prod_mset A" by simp |
787 |
finally show "p \<in># A" using p A by (subst (asm) prime_dvd_prod_mset_primes_iff) |
|
63498 | 788 |
qed |
789 |
moreover have "finite (set_mset A)" by simp |
|
790 |
ultimately show ?thesis by (rule finite_subset) |
|
60804 | 791 |
qed |
792 |
||
63633 | 793 |
lemma prime_elem_iff_irreducible: "prime_elem x \<longleftrightarrow> irreducible x" |
794 |
by (blast intro: irreducible_imp_prime_elem prime_elem_imp_irreducible) |
|
62499 | 795 |
|
63498 | 796 |
lemma prime_divisor_exists: |
797 |
assumes "a \<noteq> 0" "\<not>is_unit a" |
|
63633 | 798 |
shows "\<exists>b. b dvd a \<and> prime b" |
63498 | 799 |
proof - |
800 |
from prime_factorization_exists'[OF assms(1)] guess A . note A = this |
|
801 |
moreover from A and assms have "A \<noteq> {#}" by auto |
|
802 |
then obtain x where "x \<in># A" by blast |
|
63830 | 803 |
with A(1) have *: "x dvd prod_mset A" "prime x" by (auto simp: dvd_prod_mset) |
63539 | 804 |
with A have "x dvd a" by simp |
805 |
with * show ?thesis by blast |
|
63498 | 806 |
qed |
60804 | 807 |
|
63498 | 808 |
lemma prime_divisors_induct [case_names zero unit factor]: |
63633 | 809 |
assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)" |
63498 | 810 |
shows "P x" |
811 |
proof (cases "x = 0") |
|
812 |
case False |
|
813 |
from prime_factorization_exists'[OF this] guess A . note A = this |
|
63830 | 814 |
from A(1) have "P (unit_factor x * prod_mset A)" |
63498 | 815 |
proof (induction A) |
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63633
diff
changeset
|
816 |
case (add p A) |
63633 | 817 |
from add.prems have "prime p" by simp |
63830 | 818 |
moreover from add.prems have "P (unit_factor x * prod_mset A)" by (intro add.IH) simp_all |
819 |
ultimately have "P (p * (unit_factor x * prod_mset A))" by (rule assms(3)) |
|
63498 | 820 |
thus ?case by (simp add: mult_ac) |
821 |
qed (simp_all add: assms False) |
|
822 |
with A show ?thesis by simp |
|
823 |
qed (simp_all add: assms(1)) |
|
824 |
||
825 |
lemma no_prime_divisors_imp_unit: |
|
63633 | 826 |
assumes "a \<noteq> 0" "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> prime_elem b" |
63498 | 827 |
shows "is_unit a" |
828 |
proof (rule ccontr) |
|
829 |
assume "\<not>is_unit a" |
|
830 |
from prime_divisor_exists[OF assms(1) this] guess b by (elim exE conjE) |
|
63633 | 831 |
with assms(2)[of b] show False by (simp add: prime_def) |
60804 | 832 |
qed |
62499 | 833 |
|
63498 | 834 |
lemma prime_divisorE: |
835 |
assumes "a \<noteq> 0" and "\<not> is_unit a" |
|
63633 | 836 |
obtains p where "prime p" and "p dvd a" |
837 |
using assms no_prime_divisors_imp_unit unfolding prime_def by blast |
|
63498 | 838 |
|
839 |
definition multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where |
|
840 |
"multiplicity p x = (if finite {n. p ^ n dvd x} then Max {n. p ^ n dvd x} else 0)" |
|
841 |
||
842 |
lemma multiplicity_dvd: "p ^ multiplicity p x dvd x" |
|
843 |
proof (cases "finite {n. p ^ n dvd x}") |
|
844 |
case True |
|
845 |
hence "multiplicity p x = Max {n. p ^ n dvd x}" |
|
846 |
by (simp add: multiplicity_def) |
|
847 |
also have "\<dots> \<in> {n. p ^ n dvd x}" |
|
848 |
by (rule Max_in) (auto intro!: True exI[of _ "0::nat"]) |
|
849 |
finally show ?thesis by simp |
|
850 |
qed (simp add: multiplicity_def) |
|
851 |
||
852 |
lemma multiplicity_dvd': "n \<le> multiplicity p x \<Longrightarrow> p ^ n dvd x" |
|
853 |
by (rule dvd_trans[OF le_imp_power_dvd multiplicity_dvd]) |
|
854 |
||
855 |
context |
|
856 |
fixes x p :: 'a |
|
857 |
assumes xp: "x \<noteq> 0" "\<not>is_unit p" |
|
858 |
begin |
|
859 |
||
860 |
lemma multiplicity_eq_Max: "multiplicity p x = Max {n. p ^ n dvd x}" |
|
861 |
using finite_divisor_powers[OF xp] by (simp add: multiplicity_def) |
|
862 |
||
863 |
lemma multiplicity_geI: |
|
864 |
assumes "p ^ n dvd x" |
|
865 |
shows "multiplicity p x \<ge> n" |
|
866 |
proof - |
|
867 |
from assms have "n \<le> Max {n. p ^ n dvd x}" |
|
868 |
by (intro Max_ge finite_divisor_powers xp) simp_all |
|
869 |
thus ?thesis by (subst multiplicity_eq_Max) |
|
870 |
qed |
|
871 |
||
872 |
lemma multiplicity_lessI: |
|
873 |
assumes "\<not>p ^ n dvd x" |
|
874 |
shows "multiplicity p x < n" |
|
875 |
proof (rule ccontr) |
|
876 |
assume "\<not>(n > multiplicity p x)" |
|
877 |
hence "p ^ n dvd x" by (intro multiplicity_dvd') simp |
|
878 |
with assms show False by contradiction |
|
62499 | 879 |
qed |
880 |
||
63498 | 881 |
lemma power_dvd_iff_le_multiplicity: |
882 |
"p ^ n dvd x \<longleftrightarrow> n \<le> multiplicity p x" |
|
883 |
using multiplicity_geI[of n] multiplicity_lessI[of n] by (cases "p ^ n dvd x") auto |
|
884 |
||
885 |
lemma multiplicity_eq_zero_iff: |
|
886 |
shows "multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x" |
|
887 |
using power_dvd_iff_le_multiplicity[of 1] by auto |
|
888 |
||
889 |
lemma multiplicity_gt_zero_iff: |
|
890 |
shows "multiplicity p x > 0 \<longleftrightarrow> p dvd x" |
|
891 |
using power_dvd_iff_le_multiplicity[of 1] by auto |
|
892 |
||
893 |
lemma multiplicity_decompose: |
|
894 |
"\<not>p dvd (x div p ^ multiplicity p x)" |
|
895 |
proof |
|
896 |
assume *: "p dvd x div p ^ multiplicity p x" |
|
897 |
have "x = x div p ^ multiplicity p x * (p ^ multiplicity p x)" |
|
898 |
using multiplicity_dvd[of p x] by simp |
|
899 |
also from * have "x div p ^ multiplicity p x = (x div p ^ multiplicity p x div p) * p" by simp |
|
900 |
also have "x div p ^ multiplicity p x div p * p * p ^ multiplicity p x = |
|
901 |
x div p ^ multiplicity p x div p * p ^ Suc (multiplicity p x)" |
|
902 |
by (simp add: mult_assoc) |
|
903 |
also have "p ^ Suc (multiplicity p x) dvd \<dots>" by (rule dvd_triv_right) |
|
904 |
finally show False by (subst (asm) power_dvd_iff_le_multiplicity) simp |
|
905 |
qed |
|
906 |
||
907 |
lemma multiplicity_decompose': |
|
908 |
obtains y where "x = p ^ multiplicity p x * y" "\<not>p dvd y" |
|
909 |
using that[of "x div p ^ multiplicity p x"] |
|
910 |
by (simp add: multiplicity_decompose multiplicity_dvd) |
|
911 |
||
912 |
end |
|
913 |
||
914 |
lemma multiplicity_zero [simp]: "multiplicity p 0 = 0" |
|
915 |
by (simp add: multiplicity_def) |
|
916 |
||
63633 | 917 |
lemma prime_elem_multiplicity_eq_zero_iff: |
918 |
"prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x" |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
919 |
by (rule multiplicity_eq_zero_iff) simp_all |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
920 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
921 |
lemma prime_multiplicity_other: |
63633 | 922 |
assumes "prime p" "prime q" "p \<noteq> q" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
923 |
shows "multiplicity p q = 0" |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
924 |
using assms by (subst prime_elem_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
925 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
926 |
lemma prime_multiplicity_gt_zero_iff: |
63633 | 927 |
"prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
928 |
by (rule multiplicity_gt_zero_iff) simp_all |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
929 |
|
63498 | 930 |
lemma multiplicity_unit_left: "is_unit p \<Longrightarrow> multiplicity p x = 0" |
931 |
by (simp add: multiplicity_def is_unit_power_iff unit_imp_dvd) |
|
62499 | 932 |
|
63498 | 933 |
lemma multiplicity_unit_right: |
934 |
assumes "is_unit x" |
|
935 |
shows "multiplicity p x = 0" |
|
936 |
proof (cases "is_unit p \<or> x = 0") |
|
937 |
case False |
|
938 |
with multiplicity_lessI[of x p 1] this assms |
|
939 |
show ?thesis by (auto dest: dvd_unit_imp_unit) |
|
940 |
qed (auto simp: multiplicity_unit_left) |
|
941 |
||
942 |
lemma multiplicity_one [simp]: "multiplicity p 1 = 0" |
|
943 |
by (rule multiplicity_unit_right) simp_all |
|
944 |
||
945 |
lemma multiplicity_eqI: |
|
946 |
assumes "p ^ n dvd x" "\<not>p ^ Suc n dvd x" |
|
947 |
shows "multiplicity p x = n" |
|
948 |
proof - |
|
949 |
consider "x = 0" | "is_unit p" | "x \<noteq> 0" "\<not>is_unit p" by blast |
|
950 |
thus ?thesis |
|
951 |
proof cases |
|
952 |
assume xp: "x \<noteq> 0" "\<not>is_unit p" |
|
953 |
from xp assms(1) have "multiplicity p x \<ge> n" by (intro multiplicity_geI) |
|
954 |
moreover from assms(2) xp have "multiplicity p x < Suc n" by (intro multiplicity_lessI) |
|
955 |
ultimately show ?thesis by simp |
|
956 |
next |
|
957 |
assume "is_unit p" |
|
958 |
hence "is_unit (p ^ Suc n)" by (simp add: is_unit_power_iff del: power_Suc) |
|
959 |
hence "p ^ Suc n dvd x" by (rule unit_imp_dvd) |
|
960 |
with \<open>\<not>p ^ Suc n dvd x\<close> show ?thesis by contradiction |
|
961 |
qed (insert assms, simp_all) |
|
962 |
qed |
|
963 |
||
964 |
||
965 |
context |
|
966 |
fixes x p :: 'a |
|
967 |
assumes xp: "x \<noteq> 0" "\<not>is_unit p" |
|
968 |
begin |
|
969 |
||
970 |
lemma multiplicity_times_same: |
|
971 |
assumes "p \<noteq> 0" |
|
972 |
shows "multiplicity p (p * x) = Suc (multiplicity p x)" |
|
973 |
proof (rule multiplicity_eqI) |
|
974 |
show "p ^ Suc (multiplicity p x) dvd p * x" |
|
975 |
by (auto intro!: mult_dvd_mono multiplicity_dvd) |
|
976 |
from xp assms show "\<not> p ^ Suc (Suc (multiplicity p x)) dvd p * x" |
|
977 |
using power_dvd_iff_le_multiplicity[OF xp, of "Suc (multiplicity p x)"] by simp |
|
62499 | 978 |
qed |
979 |
||
980 |
end |
|
981 |
||
63498 | 982 |
lemma multiplicity_same_power': "multiplicity p (p ^ n) = (if p = 0 \<or> is_unit p then 0 else n)" |
983 |
proof - |
|
984 |
consider "p = 0" | "is_unit p" |"p \<noteq> 0" "\<not>is_unit p" by blast |
|
985 |
thus ?thesis |
|
986 |
proof cases |
|
987 |
assume "p \<noteq> 0" "\<not>is_unit p" |
|
988 |
thus ?thesis by (induction n) (simp_all add: multiplicity_times_same) |
|
989 |
qed (simp_all add: power_0_left multiplicity_unit_left) |
|
990 |
qed |
|
62499 | 991 |
|
63498 | 992 |
lemma multiplicity_same_power: |
993 |
"p \<noteq> 0 \<Longrightarrow> \<not>is_unit p \<Longrightarrow> multiplicity p (p ^ n) = n" |
|
994 |
by (simp add: multiplicity_same_power') |
|
995 |
||
63633 | 996 |
lemma multiplicity_prime_elem_times_other: |
997 |
assumes "prime_elem p" "\<not>p dvd q" |
|
63498 | 998 |
shows "multiplicity p (q * x) = multiplicity p x" |
999 |
proof (cases "x = 0") |
|
1000 |
case False |
|
1001 |
show ?thesis |
|
1002 |
proof (rule multiplicity_eqI) |
|
1003 |
have "1 * p ^ multiplicity p x dvd q * x" |
|
1004 |
by (intro mult_dvd_mono multiplicity_dvd) simp_all |
|
1005 |
thus "p ^ multiplicity p x dvd q * x" by simp |
|
62499 | 1006 |
next |
63498 | 1007 |
define n where "n = multiplicity p x" |
1008 |
from assms have "\<not>is_unit p" by simp |
|
1009 |
from multiplicity_decompose'[OF False this] guess y . note y = this [folded n_def] |
|
1010 |
from y have "p ^ Suc n dvd q * x \<longleftrightarrow> p ^ n * p dvd p ^ n * (q * y)" by (simp add: mult_ac) |
|
1011 |
also from assms have "\<dots> \<longleftrightarrow> p dvd q * y" by simp |
|
63633 | 1012 |
also have "\<dots> \<longleftrightarrow> p dvd q \<or> p dvd y" by (rule prime_elem_dvd_mult_iff) fact+ |
63498 | 1013 |
also from assms y have "\<dots> \<longleftrightarrow> False" by simp |
1014 |
finally show "\<not>(p ^ Suc n dvd q * x)" by blast |
|
62499 | 1015 |
qed |
63498 | 1016 |
qed simp_all |
1017 |
||
63924 | 1018 |
lemma multiplicity_self: |
1019 |
assumes "p \<noteq> 0" "\<not>is_unit p" |
|
1020 |
shows "multiplicity p p = 1" |
|
1021 |
proof - |
|
1022 |
from assms have "multiplicity p p = Max {n. p ^ n dvd p}" |
|
1023 |
by (simp add: multiplicity_eq_Max) |
|
1024 |
also from assms have "p ^ n dvd p \<longleftrightarrow> n \<le> 1" for n |
|
1025 |
using dvd_power_iff[of p n 1] by auto |
|
1026 |
hence "{n. p ^ n dvd p} = {..1}" by auto |
|
1027 |
also have "\<dots> = {0,1}" by auto |
|
1028 |
finally show ?thesis by simp |
|
1029 |
qed |
|
1030 |
||
1031 |
lemma multiplicity_times_unit_left: |
|
1032 |
assumes "is_unit c" |
|
1033 |
shows "multiplicity (c * p) x = multiplicity p x" |
|
1034 |
proof - |
|
1035 |
from assms have "{n. (c * p) ^ n dvd x} = {n. p ^ n dvd x}" |
|
1036 |
by (subst mult.commute) (simp add: mult_unit_dvd_iff power_mult_distrib is_unit_power_iff) |
|
1037 |
thus ?thesis by (simp add: multiplicity_def) |
|
1038 |
qed |
|
1039 |
||
1040 |
lemma multiplicity_times_unit_right: |
|
1041 |
assumes "is_unit c" |
|
1042 |
shows "multiplicity p (c * x) = multiplicity p x" |
|
1043 |
proof - |
|
1044 |
from assms have "{n. p ^ n dvd c * x} = {n. p ^ n dvd x}" |
|
1045 |
by (subst mult.commute) (simp add: dvd_mult_unit_iff) |
|
1046 |
thus ?thesis by (simp add: multiplicity_def) |
|
1047 |
qed |
|
1048 |
||
1049 |
lemma multiplicity_normalize_left [simp]: |
|
1050 |
"multiplicity (normalize p) x = multiplicity p x" |
|
1051 |
proof (cases "p = 0") |
|
1052 |
case [simp]: False |
|
1053 |
have "normalize p = (1 div unit_factor p) * p" |
|
1054 |
by (simp add: unit_div_commute is_unit_unit_factor) |
|
1055 |
also have "multiplicity \<dots> x = multiplicity p x" |
|
1056 |
by (rule multiplicity_times_unit_left) (simp add: is_unit_unit_factor) |
|
1057 |
finally show ?thesis . |
|
1058 |
qed simp_all |
|
1059 |
||
1060 |
lemma multiplicity_normalize_right [simp]: |
|
1061 |
"multiplicity p (normalize x) = multiplicity p x" |
|
1062 |
proof (cases "x = 0") |
|
1063 |
case [simp]: False |
|
1064 |
have "normalize x = (1 div unit_factor x) * x" |
|
1065 |
by (simp add: unit_div_commute is_unit_unit_factor) |
|
1066 |
also have "multiplicity p \<dots> = multiplicity p x" |
|
1067 |
by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor) |
|
1068 |
finally show ?thesis . |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1069 |
qed simp_all |
63924 | 1070 |
|
1071 |
lemma multiplicity_prime [simp]: "prime_elem p \<Longrightarrow> multiplicity p p = 1" |
|
1072 |
by (rule multiplicity_self) auto |
|
1073 |
||
1074 |
lemma multiplicity_prime_power [simp]: "prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n" |
|
1075 |
by (subst multiplicity_same_power') auto |
|
1076 |
||
63498 | 1077 |
lift_definition prime_factorization :: "'a \<Rightarrow> 'a multiset" is |
63633 | 1078 |
"\<lambda>x p. if prime p then multiplicity p x else 0" |
63498 | 1079 |
unfolding multiset_def |
1080 |
proof clarify |
|
1081 |
fix x :: 'a |
|
63633 | 1082 |
show "finite {p. 0 < (if prime p then multiplicity p x else 0)}" (is "finite ?A") |
63498 | 1083 |
proof (cases "x = 0") |
1084 |
case False |
|
63633 | 1085 |
from False have "?A \<subseteq> {p. prime p \<and> p dvd x}" |
63498 | 1086 |
by (auto simp: multiplicity_gt_zero_iff) |
63633 | 1087 |
moreover from False have "finite {p. prime p \<and> p dvd x}" |
63498 | 1088 |
by (rule finite_prime_divisors) |
1089 |
ultimately show ?thesis by (rule finite_subset) |
|
1090 |
qed simp_all |
|
1091 |
qed |
|
1092 |
||
63905 | 1093 |
abbreviation prime_factors :: "'a \<Rightarrow> 'a set" where |
1094 |
"prime_factors a \<equiv> set_mset (prime_factorization a)" |
|
1095 |
||
63498 | 1096 |
lemma count_prime_factorization_nonprime: |
63633 | 1097 |
"\<not>prime p \<Longrightarrow> count (prime_factorization x) p = 0" |
63498 | 1098 |
by transfer simp |
1099 |
||
1100 |
lemma count_prime_factorization_prime: |
|
63633 | 1101 |
"prime p \<Longrightarrow> count (prime_factorization x) p = multiplicity p x" |
63498 | 1102 |
by transfer simp |
1103 |
||
1104 |
lemma count_prime_factorization: |
|
63633 | 1105 |
"count (prime_factorization x) p = (if prime p then multiplicity p x else 0)" |
63498 | 1106 |
by transfer simp |
1107 |
||
63924 | 1108 |
lemma dvd_imp_multiplicity_le: |
1109 |
assumes "a dvd b" "b \<noteq> 0" |
|
1110 |
shows "multiplicity p a \<le> multiplicity p b" |
|
1111 |
proof (cases "is_unit p") |
|
1112 |
case False |
|
1113 |
with assms show ?thesis |
|
1114 |
by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)]) |
|
1115 |
qed (insert assms, auto simp: multiplicity_unit_left) |
|
63498 | 1116 |
|
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1117 |
lemma prime_power_inj: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1118 |
assumes "prime a" "a ^ m = a ^ n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1119 |
shows "m = n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1120 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1121 |
have "multiplicity a (a ^ m) = multiplicity a (a ^ n)" by (simp only: assms) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1122 |
thus ?thesis using assms by (subst (asm) (1 2) multiplicity_prime_power) simp_all |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1123 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1124 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1125 |
lemma prime_power_inj': |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1126 |
assumes "prime p" "prime q" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1127 |
assumes "p ^ m = q ^ n" "m > 0" "n > 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1128 |
shows "p = q" "m = n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1129 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1130 |
from assms have "p ^ 1 dvd p ^ m" by (intro le_imp_power_dvd) simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1131 |
also have "p ^ m = q ^ n" by fact |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1132 |
finally have "p dvd q ^ n" by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1133 |
with assms have "p dvd q" using prime_dvd_power[of p q] by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1134 |
with assms show "p = q" by (simp add: primes_dvd_imp_eq) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1135 |
with assms show "m = n" by (simp add: prime_power_inj) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1136 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1137 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1138 |
lemma prime_power_eq_one_iff [simp]: "prime p \<Longrightarrow> p ^ n = 1 \<longleftrightarrow> n = 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1139 |
using prime_power_inj[of p n 0] by auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1140 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1141 |
lemma one_eq_prime_power_iff [simp]: "prime p \<Longrightarrow> 1 = p ^ n \<longleftrightarrow> n = 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1142 |
using prime_power_inj[of p 0 n] by auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1143 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1144 |
lemma prime_power_inj'': |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1145 |
assumes "prime p" "prime q" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1146 |
shows "p ^ m = q ^ n \<longleftrightarrow> (m = 0 \<and> n = 0) \<or> (p = q \<and> m = n)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1147 |
using assms |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1148 |
by (cases "m = 0"; cases "n = 0") |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1149 |
(auto dest: prime_power_inj'[OF assms]) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1150 |
|
63498 | 1151 |
lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}" |
1152 |
by (simp add: multiset_eq_iff count_prime_factorization) |
|
1153 |
||
1154 |
lemma prime_factorization_empty_iff: |
|
1155 |
"prime_factorization x = {#} \<longleftrightarrow> x = 0 \<or> is_unit x" |
|
1156 |
proof |
|
1157 |
assume *: "prime_factorization x = {#}" |
|
1158 |
{ |
|
1159 |
assume x: "x \<noteq> 0" "\<not>is_unit x" |
|
1160 |
{ |
|
63633 | 1161 |
fix p assume p: "prime p" |
63498 | 1162 |
have "count (prime_factorization x) p = 0" by (simp add: *) |
1163 |
also from p have "count (prime_factorization x) p = multiplicity p x" |
|
1164 |
by (rule count_prime_factorization_prime) |
|
1165 |
also from x p have "\<dots> = 0 \<longleftrightarrow> \<not>p dvd x" by (simp add: multiplicity_eq_zero_iff) |
|
1166 |
finally have "\<not>p dvd x" . |
|
1167 |
} |
|
1168 |
with prime_divisor_exists[OF x] have False by blast |
|
1169 |
} |
|
1170 |
thus "x = 0 \<or> is_unit x" by blast |
|
1171 |
next |
|
1172 |
assume "x = 0 \<or> is_unit x" |
|
1173 |
thus "prime_factorization x = {#}" |
|
1174 |
proof |
|
1175 |
assume x: "is_unit x" |
|
1176 |
{ |
|
63633 | 1177 |
fix p assume p: "prime p" |
63498 | 1178 |
from p x have "multiplicity p x = 0" |
1179 |
by (subst multiplicity_eq_zero_iff) |
|
1180 |
(auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors) |
|
1181 |
} |
|
1182 |
thus ?thesis by (simp add: multiset_eq_iff count_prime_factorization) |
|
1183 |
qed simp_all |
|
1184 |
qed |
|
1185 |
||
1186 |
lemma prime_factorization_unit: |
|
1187 |
assumes "is_unit x" |
|
1188 |
shows "prime_factorization x = {#}" |
|
1189 |
proof (rule multiset_eqI) |
|
1190 |
fix p :: 'a |
|
1191 |
show "count (prime_factorization x) p = count {#} p" |
|
63633 | 1192 |
proof (cases "prime p") |
63498 | 1193 |
case True |
1194 |
with assms have "multiplicity p x = 0" |
|
1195 |
by (subst multiplicity_eq_zero_iff) |
|
1196 |
(auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors) |
|
1197 |
with True show ?thesis by (simp add: count_prime_factorization_prime) |
|
1198 |
qed (simp_all add: count_prime_factorization_nonprime) |
|
1199 |
qed |
|
1200 |
||
1201 |
lemma prime_factorization_1 [simp]: "prime_factorization 1 = {#}" |
|
1202 |
by (simp add: prime_factorization_unit) |
|
1203 |
||
1204 |
lemma prime_factorization_times_prime: |
|
63633 | 1205 |
assumes "x \<noteq> 0" "prime p" |
63498 | 1206 |
shows "prime_factorization (p * x) = {#p#} + prime_factorization x" |
1207 |
proof (rule multiset_eqI) |
|
1208 |
fix q :: 'a |
|
63633 | 1209 |
consider "\<not>prime q" | "p = q" | "prime q" "p \<noteq> q" by blast |
63498 | 1210 |
thus "count (prime_factorization (p * x)) q = count ({#p#} + prime_factorization x) q" |
1211 |
proof cases |
|
63633 | 1212 |
assume q: "prime q" "p \<noteq> q" |
63498 | 1213 |
with assms primes_dvd_imp_eq[of q p] have "\<not>q dvd p" by auto |
1214 |
with q assms show ?thesis |
|
63633 | 1215 |
by (simp add: multiplicity_prime_elem_times_other count_prime_factorization) |
63498 | 1216 |
qed (insert assms, auto simp: count_prime_factorization multiplicity_times_same) |
1217 |
qed |
|
1218 |
||
63830 | 1219 |
lemma prod_mset_prime_factorization: |
63498 | 1220 |
assumes "x \<noteq> 0" |
63830 | 1221 |
shows "prod_mset (prime_factorization x) = normalize x" |
63498 | 1222 |
using assms |
1223 |
by (induction x rule: prime_divisors_induct) |
|
1224 |
(simp_all add: prime_factorization_unit prime_factorization_times_prime |
|
1225 |
is_unit_normalize normalize_mult) |
|
1226 |
||
63905 | 1227 |
lemma in_prime_factors_iff: |
1228 |
"p \<in> prime_factors x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p" |
|
63498 | 1229 |
proof - |
63905 | 1230 |
have "p \<in> prime_factors x \<longleftrightarrow> count (prime_factorization x) p > 0" by simp |
63633 | 1231 |
also have "\<dots> \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p" |
63498 | 1232 |
by (subst count_prime_factorization, cases "x = 0") |
1233 |
(auto simp: multiplicity_eq_zero_iff multiplicity_gt_zero_iff) |
|
1234 |
finally show ?thesis . |
|
1235 |
qed |
|
1236 |
||
63905 | 1237 |
lemma in_prime_factors_imp_prime [intro]: |
1238 |
"p \<in> prime_factors x \<Longrightarrow> prime p" |
|
1239 |
by (simp add: in_prime_factors_iff) |
|
63498 | 1240 |
|
63905 | 1241 |
lemma in_prime_factors_imp_dvd [dest]: |
1242 |
"p \<in> prime_factors x \<Longrightarrow> p dvd x" |
|
1243 |
by (simp add: in_prime_factors_iff) |
|
63498 | 1244 |
|
63924 | 1245 |
lemma prime_factorsI: |
1246 |
"x \<noteq> 0 \<Longrightarrow> prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x" |
|
1247 |
by (auto simp: in_prime_factors_iff) |
|
1248 |
||
1249 |
lemma prime_factors_dvd: |
|
1250 |
"x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. prime p \<and> p dvd x}" |
|
1251 |
by (auto intro: prime_factorsI) |
|
1252 |
||
1253 |
lemma prime_factors_multiplicity: |
|
1254 |
"prime_factors n = {p. prime p \<and> multiplicity p n > 0}" |
|
1255 |
by (cases "n = 0") (auto simp add: prime_factors_dvd prime_multiplicity_gt_zero_iff) |
|
63498 | 1256 |
|
1257 |
lemma prime_factorization_prime: |
|
63633 | 1258 |
assumes "prime p" |
63498 | 1259 |
shows "prime_factorization p = {#p#}" |
1260 |
proof (rule multiset_eqI) |
|
1261 |
fix q :: 'a |
|
63633 | 1262 |
consider "\<not>prime q" | "q = p" | "prime q" "q \<noteq> p" by blast |
63498 | 1263 |
thus "count (prime_factorization p) q = count {#p#} q" |
1264 |
by cases (insert assms, auto dest: primes_dvd_imp_eq |
|
1265 |
simp: count_prime_factorization multiplicity_self multiplicity_eq_zero_iff) |
|
1266 |
qed |
|
1267 |
||
63830 | 1268 |
lemma prime_factorization_prod_mset_primes: |
63633 | 1269 |
assumes "\<And>p. p \<in># A \<Longrightarrow> prime p" |
63830 | 1270 |
shows "prime_factorization (prod_mset A) = A" |
63498 | 1271 |
using assms |
1272 |
proof (induction A) |
|
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63633
diff
changeset
|
1273 |
case (add p A) |
63498 | 1274 |
from add.prems[of 0] have "0 \<notin># A" by auto |
63830 | 1275 |
hence "prod_mset A \<noteq> 0" by auto |
63498 | 1276 |
with add show ?case |
1277 |
by (simp_all add: mult_ac prime_factorization_times_prime Multiset.union_commute) |
|
1278 |
qed simp_all |
|
1279 |
||
1280 |
lemma prime_factorization_cong: |
|
1281 |
"normalize x = normalize y \<Longrightarrow> prime_factorization x = prime_factorization y" |
|
1282 |
by (simp add: multiset_eq_iff count_prime_factorization |
|
1283 |
multiplicity_normalize_right [of _ x, symmetric] |
|
1284 |
multiplicity_normalize_right [of _ y, symmetric] |
|
1285 |
del: multiplicity_normalize_right) |
|
1286 |
||
1287 |
lemma prime_factorization_unique: |
|
1288 |
assumes "x \<noteq> 0" "y \<noteq> 0" |
|
1289 |
shows "prime_factorization x = prime_factorization y \<longleftrightarrow> normalize x = normalize y" |
|
1290 |
proof |
|
1291 |
assume "prime_factorization x = prime_factorization y" |
|
63830 | 1292 |
hence "prod_mset (prime_factorization x) = prod_mset (prime_factorization y)" by simp |
1293 |
with assms show "normalize x = normalize y" by (simp add: prod_mset_prime_factorization) |
|
63498 | 1294 |
qed (rule prime_factorization_cong) |
1295 |
||
1296 |
lemma prime_factorization_mult: |
|
1297 |
assumes "x \<noteq> 0" "y \<noteq> 0" |
|
1298 |
shows "prime_factorization (x * y) = prime_factorization x + prime_factorization y" |
|
1299 |
proof - |
|
63830 | 1300 |
have "prime_factorization (prod_mset (prime_factorization (x * y))) = |
1301 |
prime_factorization (prod_mset (prime_factorization x + prime_factorization y))" |
|
1302 |
by (simp add: prod_mset_prime_factorization assms normalize_mult) |
|
1303 |
also have "prime_factorization (prod_mset (prime_factorization (x * y))) = |
|
63498 | 1304 |
prime_factorization (x * y)" |
63905 | 1305 |
by (rule prime_factorization_prod_mset_primes) (simp_all add: in_prime_factors_imp_prime) |
63830 | 1306 |
also have "prime_factorization (prod_mset (prime_factorization x + prime_factorization y)) = |
63498 | 1307 |
prime_factorization x + prime_factorization y" |
63905 | 1308 |
by (rule prime_factorization_prod_mset_primes) (auto simp: in_prime_factors_imp_prime) |
63498 | 1309 |
finally show ?thesis . |
62499 | 1310 |
qed |
1311 |
||
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1312 |
lemma prime_factorization_prod: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1313 |
assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1314 |
shows "prime_factorization (prod f A) = (\<Sum>n\<in>A. prime_factorization (f n))" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1315 |
using assms by (induction A rule: finite_induct) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1316 |
(auto simp: Sup_multiset_empty prime_factorization_mult) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1317 |
|
63924 | 1318 |
lemma prime_elem_multiplicity_mult_distrib: |
1319 |
assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0" |
|
1320 |
shows "multiplicity p (x * y) = multiplicity p x + multiplicity p y" |
|
1321 |
proof - |
|
1322 |
have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)" |
|
1323 |
by (subst count_prime_factorization_prime) (simp_all add: assms) |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1324 |
also from assms |
63924 | 1325 |
have "prime_factorization (x * y) = prime_factorization x + prime_factorization y" |
1326 |
by (intro prime_factorization_mult) |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1327 |
also have "count \<dots> (normalize p) = |
63924 | 1328 |
count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)" |
1329 |
by simp |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1330 |
also have "\<dots> = multiplicity p x + multiplicity p y" |
63924 | 1331 |
by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms) |
1332 |
finally show ?thesis . |
|
1333 |
qed |
|
1334 |
||
1335 |
lemma prime_elem_multiplicity_prod_mset_distrib: |
|
1336 |
assumes "prime_elem p" "0 \<notin># A" |
|
1337 |
shows "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)" |
|
1338 |
using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib) |
|
1339 |
||
1340 |
lemma prime_elem_multiplicity_power_distrib: |
|
1341 |
assumes "prime_elem p" "x \<noteq> 0" |
|
1342 |
shows "multiplicity p (x ^ n) = n * multiplicity p x" |
|
1343 |
using assms prime_elem_multiplicity_prod_mset_distrib [of p "replicate_mset n x"] |
|
1344 |
by simp |
|
1345 |
||
64272 | 1346 |
lemma prime_elem_multiplicity_prod_distrib: |
63924 | 1347 |
assumes "prime_elem p" "0 \<notin> f ` A" "finite A" |
64272 | 1348 |
shows "multiplicity p (prod f A) = (\<Sum>x\<in>A. multiplicity p (f x))" |
63924 | 1349 |
proof - |
64272 | 1350 |
have "multiplicity p (prod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))" |
1351 |
using assms by (subst prod_unfold_prod_mset) |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1352 |
(simp_all add: prime_elem_multiplicity_prod_mset_distrib sum_unfold_sum_mset |
63924 | 1353 |
multiset.map_comp o_def) |
1354 |
also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))" |
|
1355 |
by (induction A rule: finite_induct) simp_all |
|
1356 |
finally show ?thesis . |
|
1357 |
qed |
|
1358 |
||
1359 |
lemma multiplicity_distinct_prime_power: |
|
1360 |
"prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0" |
|
1361 |
by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other) |
|
1362 |
||
63498 | 1363 |
lemma prime_factorization_prime_power: |
63633 | 1364 |
"prime p \<Longrightarrow> prime_factorization (p ^ n) = replicate_mset n p" |
63498 | 1365 |
by (induction n) |
1366 |
(simp_all add: prime_factorization_mult prime_factorization_prime Multiset.union_commute) |
|
1367 |
||
63830 | 1368 |
lemma prime_decomposition: "unit_factor x * prod_mset (prime_factorization x) = x" |
1369 |
by (cases "x = 0") (simp_all add: prod_mset_prime_factorization) |
|
63498 | 1370 |
|
1371 |
lemma prime_factorization_subset_iff_dvd: |
|
1372 |
assumes [simp]: "x \<noteq> 0" "y \<noteq> 0" |
|
1373 |
shows "prime_factorization x \<subseteq># prime_factorization y \<longleftrightarrow> x dvd y" |
|
1374 |
proof - |
|
63830 | 1375 |
have "x dvd y \<longleftrightarrow> prod_mset (prime_factorization x) dvd prod_mset (prime_factorization y)" |
1376 |
by (simp add: prod_mset_prime_factorization) |
|
63498 | 1377 |
also have "\<dots> \<longleftrightarrow> prime_factorization x \<subseteq># prime_factorization y" |
63905 | 1378 |
by (auto intro!: prod_mset_primes_dvd_imp_subset prod_mset_subset_imp_dvd) |
63498 | 1379 |
finally show ?thesis .. |
1380 |
qed |
|
1381 |
||
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1382 |
lemma prime_factorization_subset_imp_dvd: |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1383 |
"x \<noteq> 0 \<Longrightarrow> (prime_factorization x \<subseteq># prime_factorization y) \<Longrightarrow> x dvd y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1384 |
by (cases "y = 0") (simp_all add: prime_factorization_subset_iff_dvd) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1385 |
|
63498 | 1386 |
lemma prime_factorization_divide: |
1387 |
assumes "b dvd a" |
|
1388 |
shows "prime_factorization (a div b) = prime_factorization a - prime_factorization b" |
|
1389 |
proof (cases "a = 0") |
|
1390 |
case [simp]: False |
|
1391 |
from assms have [simp]: "b \<noteq> 0" by auto |
|
1392 |
have "prime_factorization ((a div b) * b) = prime_factorization (a div b) + prime_factorization b" |
|
1393 |
by (intro prime_factorization_mult) (insert assms, auto elim!: dvdE) |
|
1394 |
with assms show ?thesis by simp |
|
1395 |
qed simp_all |
|
1396 |
||
63905 | 1397 |
lemma zero_not_in_prime_factors [simp]: "0 \<notin> prime_factors x" |
1398 |
by (auto dest: in_prime_factors_imp_prime) |
|
63498 | 1399 |
|
63904 | 1400 |
lemma prime_prime_factors: |
63905 | 1401 |
"prime p \<Longrightarrow> prime_factors p = {p}" |
1402 |
by (drule prime_factorization_prime) simp |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1403 |
|
64272 | 1404 |
lemma prod_prime_factors: |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1405 |
assumes "x \<noteq> 0" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1406 |
shows "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1407 |
proof - |
63830 | 1408 |
have "normalize x = prod_mset (prime_factorization x)" |
1409 |
by (simp add: prod_mset_prime_factorization assms) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1410 |
also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)" |
63905 | 1411 |
by (subst prod_mset_multiplicity) simp_all |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1412 |
also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)" |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1413 |
by (intro prod.cong) |
63905 | 1414 |
(simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1415 |
finally show ?thesis .. |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1416 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1417 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1418 |
lemma prime_factorization_unique'': |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1419 |
assumes S_eq: "S = {p. 0 < f p}" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1420 |
and "finite S" |
63633 | 1421 |
and S: "\<forall>p\<in>S. prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)" |
1422 |
shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)" |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1423 |
proof |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1424 |
define A where "A = Abs_multiset f" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1425 |
from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1426 |
with S(2) have nz: "n \<noteq> 0" by auto |
66938 | 1427 |
from S_eq \<open>finite S\<close> have count_A: "count A = f" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1428 |
unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1429 |
from S_eq count_A have set_mset_A: "set_mset A = S" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1430 |
by (simp only: set_mset_def) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1431 |
from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" . |
63830 | 1432 |
also have "\<dots> = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A) |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1433 |
also from nz have "normalize n = prod_mset (prime_factorization n)" |
63830 | 1434 |
by (simp add: prod_mset_prime_factorization) |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1435 |
finally have "prime_factorization (prod_mset A) = |
63830 | 1436 |
prime_factorization (prod_mset (prime_factorization n))" by simp |
1437 |
also from S(1) have "prime_factorization (prod_mset A) = A" |
|
1438 |
by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A) |
|
1439 |
also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n" |
|
63905 | 1440 |
by (intro prime_factorization_prod_mset_primes) auto |
1441 |
finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric]) |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1442 |
|
63633 | 1443 |
show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1444 |
proof safe |
63633 | 1445 |
fix p :: 'a assume p: "prime p" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1446 |
have "multiplicity p n = multiplicity p (normalize n)" by simp |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1447 |
also have "normalize n = prod_mset A" |
63830 | 1448 |
by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A S) |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1449 |
also from p set_mset_A S(1) |
63830 | 1450 |
have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)" |
1451 |
by (intro prime_elem_multiplicity_prod_mset_distrib) auto |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1452 |
also from S(1) p |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1453 |
have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1454 |
by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other) |
66938 | 1455 |
also have "sum_mset \<dots> = f p" |
1456 |
by (simp add: semiring_1_class.sum_mset_delta' count_A) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1457 |
finally show "f p = multiplicity p n" .. |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1458 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1459 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1460 |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1461 |
lemma prime_factors_product: |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1462 |
"x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y" |
63905 | 1463 |
by (simp add: prime_factorization_mult) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1464 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1465 |
lemma dvd_prime_factors [intro]: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1466 |
"y \<noteq> 0 \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<subseteq> prime_factors y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1467 |
by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1468 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1469 |
(* RENAMED multiplicity_dvd *) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1470 |
lemma multiplicity_le_imp_dvd: |
63633 | 1471 |
assumes "x \<noteq> 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x \<le> multiplicity p y" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1472 |
shows "x dvd y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1473 |
proof (cases "y = 0") |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1474 |
case False |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1475 |
from assms this have "prime_factorization x \<subseteq># prime_factorization y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1476 |
by (intro mset_subset_eqI) (auto simp: count_prime_factorization) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1477 |
with assms False show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1478 |
qed auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1479 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1480 |
lemma dvd_multiplicity_eq: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1481 |
"x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1482 |
by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1483 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1484 |
lemma multiplicity_eq_imp_eq: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1485 |
assumes "x \<noteq> 0" "y \<noteq> 0" |
63633 | 1486 |
assumes "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1487 |
shows "normalize x = normalize y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1488 |
using assms by (intro associatedI multiplicity_le_imp_dvd) simp_all |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1489 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1490 |
lemma prime_factorization_unique': |
63633 | 1491 |
assumes "\<forall>p \<in># M. prime p" "\<forall>p \<in># N. prime p" "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1492 |
shows "M = N" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1493 |
proof - |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1494 |
have "prime_factorization (\<Prod>i \<in># M. i) = prime_factorization (\<Prod>i \<in># N. i)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1495 |
by (simp only: assms) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1496 |
also from assms have "prime_factorization (\<Prod>i \<in># M. i) = M" |
63830 | 1497 |
by (subst prime_factorization_prod_mset_primes) simp_all |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1498 |
also from assms have "prime_factorization (\<Prod>i \<in># N. i) = N" |
63830 | 1499 |
by (subst prime_factorization_prod_mset_primes) simp_all |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1500 |
finally show ?thesis . |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1501 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1502 |
|
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1503 |
lemma multiplicity_cong: |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1504 |
"(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> multiplicity p a = multiplicity p b" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1505 |
by (simp add: multiplicity_def) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1506 |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1507 |
lemma not_dvd_imp_multiplicity_0: |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1508 |
assumes "\<not>p dvd x" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1509 |
shows "multiplicity p x = 0" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1510 |
proof - |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1511 |
from assms have "multiplicity p x < 1" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1512 |
by (intro multiplicity_lessI) auto |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1513 |
thus ?thesis by simp |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1514 |
qed |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1515 |
|
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1516 |
lemma inj_on_Prod_primes: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1517 |
assumes "\<And>P p. P \<in> A \<Longrightarrow> p \<in> P \<Longrightarrow> prime p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1518 |
assumes "\<And>P. P \<in> A \<Longrightarrow> finite P" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1519 |
shows "inj_on Prod A" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1520 |
proof (rule inj_onI) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1521 |
fix P Q assume PQ: "P \<in> A" "Q \<in> A" "\<Prod>P = \<Prod>Q" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1522 |
with prime_factorization_unique'[of "mset_set P" "mset_set Q"] assms[of P] assms[of Q] |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1523 |
have "mset_set P = mset_set Q" by (auto simp: prod_unfold_prod_mset) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1524 |
with assms[of P] assms[of Q] PQ show "P = Q" by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1525 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1526 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1527 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1528 |
|
63924 | 1529 |
subsection \<open>GCD and LCM computation with unique factorizations\<close> |
1530 |
||
63498 | 1531 |
definition "gcd_factorial a b = (if a = 0 then normalize b |
1532 |
else if b = 0 then normalize a |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1533 |
else prod_mset (prime_factorization a \<inter># prime_factorization b))" |
63498 | 1534 |
|
1535 |
definition "lcm_factorial a b = (if a = 0 \<or> b = 0 then 0 |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1536 |
else prod_mset (prime_factorization a \<union># prime_factorization b))" |
63498 | 1537 |
|
1538 |
definition "Gcd_factorial A = |
|
63830 | 1539 |
(if A \<subseteq> {0} then 0 else prod_mset (Inf (prime_factorization ` (A - {0}))))" |
63498 | 1540 |
|
1541 |
definition "Lcm_factorial A = |
|
1542 |
(if A = {} then 1 |
|
1543 |
else if 0 \<notin> A \<and> subset_mset.bdd_above (prime_factorization ` (A - {0})) then |
|
63830 | 1544 |
prod_mset (Sup (prime_factorization ` A)) |
63498 | 1545 |
else |
1546 |
0)" |
|
1547 |
||
1548 |
lemma prime_factorization_gcd_factorial: |
|
1549 |
assumes [simp]: "a \<noteq> 0" "b \<noteq> 0" |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1550 |
shows "prime_factorization (gcd_factorial a b) = prime_factorization a \<inter># prime_factorization b" |
63498 | 1551 |
proof - |
1552 |
have "prime_factorization (gcd_factorial a b) = |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1553 |
prime_factorization (prod_mset (prime_factorization a \<inter># prime_factorization b))" |
63498 | 1554 |
by (simp add: gcd_factorial_def) |
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1555 |
also have "\<dots> = prime_factorization a \<inter># prime_factorization b" |
63905 | 1556 |
by (subst prime_factorization_prod_mset_primes) auto |
63498 | 1557 |
finally show ?thesis . |
1558 |
qed |
|
1559 |
||
1560 |
lemma prime_factorization_lcm_factorial: |
|
1561 |
assumes [simp]: "a \<noteq> 0" "b \<noteq> 0" |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1562 |
shows "prime_factorization (lcm_factorial a b) = prime_factorization a \<union># prime_factorization b" |
63498 | 1563 |
proof - |
1564 |
have "prime_factorization (lcm_factorial a b) = |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1565 |
prime_factorization (prod_mset (prime_factorization a \<union># prime_factorization b))" |
63498 | 1566 |
by (simp add: lcm_factorial_def) |
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1567 |
also have "\<dots> = prime_factorization a \<union># prime_factorization b" |
63905 | 1568 |
by (subst prime_factorization_prod_mset_primes) auto |
63498 | 1569 |
finally show ?thesis . |
1570 |
qed |
|
1571 |
||
1572 |
lemma prime_factorization_Gcd_factorial: |
|
1573 |
assumes "\<not>A \<subseteq> {0}" |
|
1574 |
shows "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))" |
|
1575 |
proof - |
|
1576 |
from assms obtain x where x: "x \<in> A - {0}" by auto |
|
1577 |
hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x" |
|
1578 |
by (intro subset_mset.cInf_lower) simp_all |
|
63905 | 1579 |
hence "\<forall>y. y \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> y \<in> prime_factors x" |
63498 | 1580 |
by (auto dest: mset_subset_eqD) |
63905 | 1581 |
with in_prime_factors_imp_prime[of _ x] |
63633 | 1582 |
have "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> prime p" by blast |
63498 | 1583 |
with assms show ?thesis |
63830 | 1584 |
by (simp add: Gcd_factorial_def prime_factorization_prod_mset_primes) |
63498 | 1585 |
qed |
1586 |
||
1587 |
lemma prime_factorization_Lcm_factorial: |
|
1588 |
assumes "0 \<notin> A" "subset_mset.bdd_above (prime_factorization ` A)" |
|
1589 |
shows "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)" |
|
1590 |
proof (cases "A = {}") |
|
1591 |
case True |
|
1592 |
hence "prime_factorization ` A = {}" by auto |
|
1593 |
also have "Sup \<dots> = {#}" by (simp add: Sup_multiset_empty) |
|
1594 |
finally show ?thesis by (simp add: Lcm_factorial_def) |
|
1595 |
next |
|
1596 |
case False |
|
63633 | 1597 |
have "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> prime y" |
63905 | 1598 |
by (auto simp: in_Sup_multiset_iff assms) |
63498 | 1599 |
with assms False show ?thesis |
63830 | 1600 |
by (simp add: Lcm_factorial_def prime_factorization_prod_mset_primes) |
63498 | 1601 |
qed |
1602 |
||
1603 |
lemma gcd_factorial_commute: "gcd_factorial a b = gcd_factorial b a" |
|
1604 |
by (simp add: gcd_factorial_def multiset_inter_commute) |
|
1605 |
||
1606 |
lemma gcd_factorial_dvd1: "gcd_factorial a b dvd a" |
|
1607 |
proof (cases "a = 0 \<or> b = 0") |
|
1608 |
case False |
|
1609 |
hence "gcd_factorial a b \<noteq> 0" by (auto simp: gcd_factorial_def) |
|
1610 |
with False show ?thesis |
|
1611 |
by (subst prime_factorization_subset_iff_dvd [symmetric]) |
|
1612 |
(auto simp: prime_factorization_gcd_factorial) |
|
1613 |
qed (auto simp: gcd_factorial_def) |
|
1614 |
||
1615 |
lemma gcd_factorial_dvd2: "gcd_factorial a b dvd b" |
|
1616 |
by (subst gcd_factorial_commute) (rule gcd_factorial_dvd1) |
|
1617 |
||
1618 |
lemma normalize_gcd_factorial: "normalize (gcd_factorial a b) = gcd_factorial a b" |
|
1619 |
proof - |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1620 |
have "normalize (prod_mset (prime_factorization a \<inter># prime_factorization b)) = |
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1621 |
prod_mset (prime_factorization a \<inter># prime_factorization b)" |
63905 | 1622 |
by (intro normalize_prod_mset_primes) auto |
63498 | 1623 |
thus ?thesis by (simp add: gcd_factorial_def) |
1624 |
qed |
|
1625 |
||
1626 |
lemma gcd_factorial_greatest: "c dvd gcd_factorial a b" if "c dvd a" "c dvd b" for a b c |
|
1627 |
proof (cases "a = 0 \<or> b = 0") |
|
1628 |
case False |
|
1629 |
with that have [simp]: "c \<noteq> 0" by auto |
|
1630 |
let ?p = "prime_factorization" |
|
1631 |
from that False have "?p c \<subseteq># ?p a" "?p c \<subseteq># ?p b" |
|
1632 |
by (simp_all add: prime_factorization_subset_iff_dvd) |
|
1633 |
hence "prime_factorization c \<subseteq># |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1634 |
prime_factorization (prod_mset (prime_factorization a \<inter># prime_factorization b))" |
63905 | 1635 |
using False by (subst prime_factorization_prod_mset_primes) auto |
63498 | 1636 |
with False show ?thesis |
1637 |
by (auto simp: gcd_factorial_def prime_factorization_subset_iff_dvd [symmetric]) |
|
1638 |
qed (auto simp: gcd_factorial_def that) |
|
1639 |
||
1640 |
lemma lcm_factorial_gcd_factorial: |
|
1641 |
"lcm_factorial a b = normalize (a * b) div gcd_factorial a b" for a b |
|
1642 |
proof (cases "a = 0 \<or> b = 0") |
|
1643 |
case False |
|
1644 |
let ?p = "prime_factorization" |
|
63830 | 1645 |
from False have "prod_mset (?p (a * b)) div gcd_factorial a b = |
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1646 |
prod_mset (?p a + ?p b - ?p a \<inter># ?p b)" |
63830 | 1647 |
by (subst prod_mset_diff) (auto simp: lcm_factorial_def gcd_factorial_def |
63498 | 1648 |
prime_factorization_mult subset_mset.le_infI1) |
63830 | 1649 |
also from False have "prod_mset (?p (a * b)) = normalize (a * b)" |
1650 |
by (intro prod_mset_prime_factorization) simp_all |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1651 |
also from False have "prod_mset (?p a + ?p b - ?p a \<inter># ?p b) = lcm_factorial a b" |
63498 | 1652 |
by (simp add: union_diff_inter_eq_sup lcm_factorial_def) |
1653 |
finally show ?thesis .. |
|
1654 |
qed (auto simp: lcm_factorial_def) |
|
1655 |
||
1656 |
lemma normalize_Gcd_factorial: |
|
1657 |
"normalize (Gcd_factorial A) = Gcd_factorial A" |
|
1658 |
proof (cases "A \<subseteq> {0}") |
|
1659 |
case False |
|
1660 |
then obtain x where "x \<in> A" "x \<noteq> 0" by blast |
|
1661 |
hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x" |
|
1662 |
by (intro subset_mset.cInf_lower) auto |
|
63633 | 1663 |
hence "prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p |
63905 | 1664 |
using that by (auto dest: mset_subset_eqD) |
63498 | 1665 |
with False show ?thesis |
63830 | 1666 |
by (auto simp add: Gcd_factorial_def normalize_prod_mset_primes) |
63498 | 1667 |
qed (simp_all add: Gcd_factorial_def) |
1668 |
||
1669 |
lemma Gcd_factorial_eq_0_iff: |
|
1670 |
"Gcd_factorial A = 0 \<longleftrightarrow> A \<subseteq> {0}" |
|
1671 |
by (auto simp: Gcd_factorial_def in_Inf_multiset_iff split: if_splits) |
|
1672 |
||
1673 |
lemma Gcd_factorial_dvd: |
|
1674 |
assumes "x \<in> A" |
|
1675 |
shows "Gcd_factorial A dvd x" |
|
1676 |
proof (cases "x = 0") |
|
1677 |
case False |
|
1678 |
with assms have "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))" |
|
1679 |
by (intro prime_factorization_Gcd_factorial) auto |
|
1680 |
also from False assms have "\<dots> \<subseteq># prime_factorization x" |
|
1681 |
by (intro subset_mset.cInf_lower) auto |
|
1682 |
finally show ?thesis |
|
1683 |
by (subst (asm) prime_factorization_subset_iff_dvd) |
|
1684 |
(insert assms False, auto simp: Gcd_factorial_eq_0_iff) |
|
1685 |
qed simp_all |
|
1686 |
||
1687 |
lemma Gcd_factorial_greatest: |
|
1688 |
assumes "\<And>y. y \<in> A \<Longrightarrow> x dvd y" |
|
1689 |
shows "x dvd Gcd_factorial A" |
|
1690 |
proof (cases "A \<subseteq> {0}") |
|
1691 |
case False |
|
1692 |
from False obtain y where "y \<in> A" "y \<noteq> 0" by auto |
|
1693 |
with assms[of y] have nz: "x \<noteq> 0" by auto |
|
1694 |
from nz assms have "prime_factorization x \<subseteq># prime_factorization y" if "y \<in> A - {0}" for y |
|
1695 |
using that by (subst prime_factorization_subset_iff_dvd) auto |
|
1696 |
with False have "prime_factorization x \<subseteq># Inf (prime_factorization ` (A - {0}))" |
|
1697 |
by (intro subset_mset.cInf_greatest) auto |
|
1698 |
also from False have "\<dots> = prime_factorization (Gcd_factorial A)" |
|
1699 |
by (rule prime_factorization_Gcd_factorial [symmetric]) |
|
1700 |
finally show ?thesis |
|
1701 |
by (subst (asm) prime_factorization_subset_iff_dvd) |
|
1702 |
(insert nz False, auto simp: Gcd_factorial_eq_0_iff) |
|
1703 |
qed (simp_all add: Gcd_factorial_def) |
|
1704 |
||
1705 |
lemma normalize_Lcm_factorial: |
|
1706 |
"normalize (Lcm_factorial A) = Lcm_factorial A" |
|
1707 |
proof (cases "subset_mset.bdd_above (prime_factorization ` A)") |
|
1708 |
case True |
|
63830 | 1709 |
hence "normalize (prod_mset (Sup (prime_factorization ` A))) = |
1710 |
prod_mset (Sup (prime_factorization ` A))" |
|
1711 |
by (intro normalize_prod_mset_primes) |
|
63905 | 1712 |
(auto simp: in_Sup_multiset_iff) |
63498 | 1713 |
with True show ?thesis by (simp add: Lcm_factorial_def) |
1714 |
qed (auto simp: Lcm_factorial_def) |
|
1715 |
||
1716 |
lemma Lcm_factorial_eq_0_iff: |
|
1717 |
"Lcm_factorial A = 0 \<longleftrightarrow> 0 \<in> A \<or> \<not>subset_mset.bdd_above (prime_factorization ` A)" |
|
1718 |
by (auto simp: Lcm_factorial_def in_Sup_multiset_iff) |
|
1719 |
||
1720 |
lemma dvd_Lcm_factorial: |
|
1721 |
assumes "x \<in> A" |
|
1722 |
shows "x dvd Lcm_factorial A" |
|
1723 |
proof (cases "0 \<notin> A \<and> subset_mset.bdd_above (prime_factorization ` A)") |
|
1724 |
case True |
|
1725 |
with assms have [simp]: "0 \<notin> A" "x \<noteq> 0" "A \<noteq> {}" by auto |
|
1726 |
from assms True have "prime_factorization x \<subseteq># Sup (prime_factorization ` A)" |
|
1727 |
by (intro subset_mset.cSup_upper) auto |
|
1728 |
also have "\<dots> = prime_factorization (Lcm_factorial A)" |
|
1729 |
by (rule prime_factorization_Lcm_factorial [symmetric]) (insert True, simp_all) |
|
1730 |
finally show ?thesis |
|
1731 |
by (subst (asm) prime_factorization_subset_iff_dvd) |
|
1732 |
(insert True, auto simp: Lcm_factorial_eq_0_iff) |
|
1733 |
qed (insert assms, auto simp: Lcm_factorial_def) |
|
1734 |
||
1735 |
lemma Lcm_factorial_least: |
|
1736 |
assumes "\<And>y. y \<in> A \<Longrightarrow> y dvd x" |
|
1737 |
shows "Lcm_factorial A dvd x" |
|
1738 |
proof - |
|
1739 |
consider "A = {}" | "0 \<in> A" | "x = 0" | "A \<noteq> {}" "0 \<notin> A" "x \<noteq> 0" by blast |
|
1740 |
thus ?thesis |
|
1741 |
proof cases |
|
1742 |
assume *: "A \<noteq> {}" "0 \<notin> A" "x \<noteq> 0" |
|
1743 |
hence nz: "x \<noteq> 0" if "x \<in> A" for x using that by auto |
|
1744 |
from * have bdd: "subset_mset.bdd_above (prime_factorization ` A)" |
|
1745 |
by (intro subset_mset.bdd_aboveI[of _ "prime_factorization x"]) |
|
1746 |
(auto simp: prime_factorization_subset_iff_dvd nz dest: assms) |
|
1747 |
have "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)" |
|
1748 |
by (rule prime_factorization_Lcm_factorial) fact+ |
|
1749 |
also from * have "\<dots> \<subseteq># prime_factorization x" |
|
1750 |
by (intro subset_mset.cSup_least) |
|
1751 |
(auto simp: prime_factorization_subset_iff_dvd nz dest: assms) |
|
1752 |
finally show ?thesis |
|
1753 |
by (subst (asm) prime_factorization_subset_iff_dvd) |
|
1754 |
(insert * bdd, auto simp: Lcm_factorial_eq_0_iff) |
|
1755 |
qed (auto simp: Lcm_factorial_def dest: assms) |
|
1756 |
qed |
|
1757 |
||
1758 |
lemmas gcd_lcm_factorial = |
|
1759 |
gcd_factorial_dvd1 gcd_factorial_dvd2 gcd_factorial_greatest |
|
1760 |
normalize_gcd_factorial lcm_factorial_gcd_factorial |
|
1761 |
normalize_Gcd_factorial Gcd_factorial_dvd Gcd_factorial_greatest |
|
1762 |
normalize_Lcm_factorial dvd_Lcm_factorial Lcm_factorial_least |
|
1763 |
||
60804 | 1764 |
end |
1765 |
||
63498 | 1766 |
class factorial_semiring_gcd = factorial_semiring + gcd + Gcd + |
1767 |
assumes gcd_eq_gcd_factorial: "gcd a b = gcd_factorial a b" |
|
1768 |
and lcm_eq_lcm_factorial: "lcm a b = lcm_factorial a b" |
|
1769 |
and Gcd_eq_Gcd_factorial: "Gcd A = Gcd_factorial A" |
|
1770 |
and Lcm_eq_Lcm_factorial: "Lcm A = Lcm_factorial A" |
|
60804 | 1771 |
begin |
1772 |
||
63498 | 1773 |
lemma prime_factorization_gcd: |
1774 |
assumes [simp]: "a \<noteq> 0" "b \<noteq> 0" |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1775 |
shows "prime_factorization (gcd a b) = prime_factorization a \<inter># prime_factorization b" |
63498 | 1776 |
by (simp add: gcd_eq_gcd_factorial prime_factorization_gcd_factorial) |
60804 | 1777 |
|
63498 | 1778 |
lemma prime_factorization_lcm: |
1779 |
assumes [simp]: "a \<noteq> 0" "b \<noteq> 0" |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1780 |
shows "prime_factorization (lcm a b) = prime_factorization a \<union># prime_factorization b" |
63498 | 1781 |
by (simp add: lcm_eq_lcm_factorial prime_factorization_lcm_factorial) |
60804 | 1782 |
|
63498 | 1783 |
lemma prime_factorization_Gcd: |
1784 |
assumes "Gcd A \<noteq> 0" |
|
1785 |
shows "prime_factorization (Gcd A) = Inf (prime_factorization ` (A - {0}))" |
|
1786 |
using assms |
|
1787 |
by (simp add: prime_factorization_Gcd_factorial Gcd_eq_Gcd_factorial Gcd_factorial_eq_0_iff) |
|
1788 |
||
1789 |
lemma prime_factorization_Lcm: |
|
1790 |
assumes "Lcm A \<noteq> 0" |
|
1791 |
shows "prime_factorization (Lcm A) = Sup (prime_factorization ` A)" |
|
1792 |
using assms |
|
1793 |
by (simp add: prime_factorization_Lcm_factorial Lcm_eq_Lcm_factorial Lcm_factorial_eq_0_iff) |
|
1794 |
||
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1795 |
lemma prime_factors_gcd [simp]: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1796 |
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> prime_factors (gcd a b) = |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1797 |
prime_factors a \<inter> prime_factors b" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1798 |
by (subst prime_factorization_gcd) auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1799 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1800 |
lemma prime_factors_lcm [simp]: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1801 |
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> prime_factors (lcm a b) = |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1802 |
prime_factors a \<union> prime_factors b" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1803 |
by (subst prime_factorization_lcm) auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1804 |
|
63498 | 1805 |
subclass semiring_gcd |
1806 |
by (standard, unfold gcd_eq_gcd_factorial lcm_eq_lcm_factorial) |
|
1807 |
(rule gcd_lcm_factorial; assumption)+ |
|
1808 |
||
1809 |
subclass semiring_Gcd |
|
1810 |
by (standard, unfold Gcd_eq_Gcd_factorial Lcm_eq_Lcm_factorial) |
|
1811 |
(rule gcd_lcm_factorial; assumption)+ |
|
60804 | 1812 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1813 |
lemma |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1814 |
assumes "x \<noteq> 0" "y \<noteq> 0" |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1815 |
shows gcd_eq_factorial': |
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1816 |
"gcd x y = (\<Prod>p \<in> prime_factors x \<inter> prime_factors y. |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1817 |
p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1") |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1818 |
and lcm_eq_factorial': |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1819 |
"lcm x y = (\<Prod>p \<in> prime_factors x \<union> prime_factors y. |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1820 |
p ^ max (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs2") |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1821 |
proof - |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1822 |
have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1823 |
also have "\<dots> = ?rhs1" |
63905 | 1824 |
by (auto simp: gcd_factorial_def assms prod_mset_multiplicity |
64272 | 1825 |
count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1826 |
finally show "gcd x y = ?rhs1" . |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1827 |
have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1828 |
also have "\<dots> = ?rhs2" |
63905 | 1829 |
by (auto simp: lcm_factorial_def assms prod_mset_multiplicity |
64272 | 1830 |
count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1831 |
finally show "lcm x y = ?rhs2" . |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1832 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1833 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1834 |
lemma |
63633 | 1835 |
assumes "x \<noteq> 0" "y \<noteq> 0" "prime p" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1836 |
shows multiplicity_gcd: "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1837 |
and multiplicity_lcm: "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1838 |
proof - |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1839 |
have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1840 |
also from assms have "multiplicity p \<dots> = min (multiplicity p x) (multiplicity p y)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1841 |
by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_gcd_factorial) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1842 |
finally show "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)" . |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1843 |
have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1844 |
also from assms have "multiplicity p \<dots> = max (multiplicity p x) (multiplicity p y)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1845 |
by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_lcm_factorial) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1846 |
finally show "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)" . |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1847 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1848 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1849 |
lemma gcd_lcm_distrib: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1850 |
"gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1851 |
proof (cases "x = 0 \<or> y = 0 \<or> z = 0") |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1852 |
case True |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1853 |
thus ?thesis |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1854 |
by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1855 |
next |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1856 |
case False |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1857 |
hence "normalize (gcd x (lcm y z)) = normalize (lcm (gcd x y) (gcd x z))" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1858 |
by (intro associatedI prime_factorization_subset_imp_dvd) |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1859 |
(auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1860 |
subset_mset.inf_sup_distrib1) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1861 |
thus ?thesis by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1862 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1863 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1864 |
lemma lcm_gcd_distrib: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1865 |
"lcm x (gcd y z) = gcd (lcm x y) (lcm x z)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1866 |
proof (cases "x = 0 \<or> y = 0 \<or> z = 0") |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1867 |
case True |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1868 |
thus ?thesis |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1869 |
by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1870 |
next |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1871 |
case False |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1872 |
hence "normalize (lcm x (gcd y z)) = normalize (gcd (lcm x y) (lcm x z))" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1873 |
by (intro associatedI prime_factorization_subset_imp_dvd) |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1874 |
(auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1875 |
subset_mset.sup_inf_distrib1) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1876 |
thus ?thesis by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1877 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1878 |
|
60804 | 1879 |
end |
1880 |
||
63498 | 1881 |
class factorial_ring_gcd = factorial_semiring_gcd + idom |
60804 | 1882 |
begin |
1883 |
||
63498 | 1884 |
subclass ring_gcd .. |
60804 | 1885 |
|
63498 | 1886 |
subclass idom_divide .. |
60804 | 1887 |
|
1888 |
end |
|
1889 |
||
1890 |
end |