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