60804
|
1 |
(* Title: HOL/Number_Theory/Factorial_Ring.thy
|
|
2 |
Author: Florian Haftmann, TU Muenchen
|
|
3 |
*)
|
|
4 |
|
|
5 |
section \<open>Factorial (semi)rings\<close>
|
|
6 |
|
|
7 |
theory Factorial_Ring
|
|
8 |
imports Main Primes "~~/src/HOL/Library/Multiset" (*"~~/src/HOL/Library/Polynomial"*)
|
|
9 |
begin
|
|
10 |
|
|
11 |
context algebraic_semidom
|
|
12 |
begin
|
|
13 |
|
|
14 |
lemma is_unit_mult_iff:
|
|
15 |
"is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" (is "?P \<longleftrightarrow> ?Q")
|
|
16 |
by (auto dest: dvd_mult_left dvd_mult_right)
|
|
17 |
|
|
18 |
lemma is_unit_power_iff:
|
|
19 |
"is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
|
|
20 |
by (induct n) (auto simp add: is_unit_mult_iff)
|
|
21 |
|
|
22 |
lemma subset_divisors_dvd:
|
|
23 |
"{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
|
|
24 |
by (auto simp add: subset_iff intro: dvd_trans)
|
|
25 |
|
|
26 |
lemma strict_subset_divisors_dvd:
|
|
27 |
"{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
|
|
28 |
by (auto simp add: subset_iff intro: dvd_trans)
|
|
29 |
|
|
30 |
end
|
|
31 |
|
|
32 |
class factorial_semiring = normalization_semidom +
|
|
33 |
assumes finite_divisors: "a \<noteq> 0 \<Longrightarrow> finite {b. b dvd a \<and> normalize b = b}"
|
|
34 |
fixes is_prime :: "'a \<Rightarrow> bool"
|
|
35 |
assumes not_is_prime_zero [simp]: "\<not> is_prime 0"
|
|
36 |
and is_prime_not_unit: "is_prime p \<Longrightarrow> \<not> is_unit p"
|
|
37 |
and no_prime_divisorsI: "(\<And>b. b dvd a \<Longrightarrow> \<not> is_prime b) \<Longrightarrow> is_unit a"
|
|
38 |
assumes is_primeI: "p \<noteq> 0 \<Longrightarrow> \<not> is_unit p \<Longrightarrow> (\<And>a. a dvd p \<Longrightarrow> \<not> is_unit a \<Longrightarrow> p dvd a) \<Longrightarrow> is_prime p"
|
|
39 |
and is_primeD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
|
|
40 |
begin
|
|
41 |
|
|
42 |
lemma not_is_prime_one [simp]:
|
|
43 |
"\<not> is_prime 1"
|
|
44 |
by (auto dest: is_prime_not_unit)
|
|
45 |
|
|
46 |
lemma is_prime_not_zeroI:
|
|
47 |
assumes "is_prime p"
|
|
48 |
shows "p \<noteq> 0"
|
|
49 |
using assms by (auto intro: ccontr)
|
|
50 |
|
|
51 |
lemma is_prime_multD:
|
|
52 |
assumes "is_prime (a * b)"
|
|
53 |
shows "is_unit a \<or> is_unit b"
|
|
54 |
proof -
|
|
55 |
from assms have "a \<noteq> 0" "b \<noteq> 0" by auto
|
|
56 |
moreover from assms is_primeD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
|
|
57 |
by auto
|
|
58 |
ultimately show ?thesis
|
|
59 |
using dvd_times_left_cancel_iff [of a b 1]
|
|
60 |
dvd_times_right_cancel_iff [of b a 1]
|
|
61 |
by auto
|
|
62 |
qed
|
|
63 |
|
|
64 |
lemma is_primeD2:
|
|
65 |
assumes "is_prime p" and "a dvd p" and "\<not> is_unit a"
|
|
66 |
shows "p dvd a"
|
|
67 |
proof -
|
|
68 |
from \<open>a dvd p\<close> obtain b where "p = a * b" ..
|
|
69 |
with \<open>is_prime p\<close> is_prime_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
|
|
70 |
with \<open>p = a * b\<close> show ?thesis
|
|
71 |
by (auto simp add: mult_unit_dvd_iff)
|
|
72 |
qed
|
|
73 |
|
|
74 |
lemma is_prime_mult_unit_left:
|
|
75 |
assumes "is_prime p"
|
|
76 |
and "is_unit a"
|
|
77 |
shows "is_prime (a * p)"
|
|
78 |
proof (rule is_primeI)
|
|
79 |
from assms show "a * p \<noteq> 0" "\<not> is_unit (a * p)"
|
|
80 |
by (auto simp add: is_unit_mult_iff is_prime_not_unit)
|
|
81 |
show "a * p dvd b" if "b dvd a * p" "\<not> is_unit b" for b
|
|
82 |
proof -
|
|
83 |
from that \<open>is_unit a\<close> have "b dvd p"
|
|
84 |
using dvd_mult_unit_iff [of a b p] by (simp add: ac_simps)
|
|
85 |
with \<open>is_prime p\<close> \<open>\<not> is_unit b\<close> have "p dvd b"
|
|
86 |
using is_primeD2 [of p b] by auto
|
|
87 |
with \<open>is_unit a\<close> show ?thesis
|
|
88 |
using mult_unit_dvd_iff [of a p b] by (simp add: ac_simps)
|
|
89 |
qed
|
|
90 |
qed
|
|
91 |
|
|
92 |
lemma is_primeI2:
|
|
93 |
assumes "p \<noteq> 0"
|
|
94 |
assumes "\<not> is_unit p"
|
|
95 |
assumes P: "\<And>a b. p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
|
|
96 |
shows "is_prime p"
|
|
97 |
using \<open>p \<noteq> 0\<close> \<open>\<not> is_unit p\<close> proof (rule is_primeI)
|
|
98 |
fix a
|
|
99 |
assume "a dvd p"
|
|
100 |
then obtain b where "p = a * b" ..
|
|
101 |
with \<open>p \<noteq> 0\<close> have "b \<noteq> 0" by simp
|
|
102 |
moreover from \<open>p = a * b\<close> P have "p dvd a \<or> p dvd b" by auto
|
|
103 |
moreover assume "\<not> is_unit a"
|
|
104 |
ultimately show "p dvd a"
|
|
105 |
using dvd_times_right_cancel_iff [of b a 1] \<open>p = a * b\<close> by auto
|
|
106 |
qed
|
|
107 |
|
|
108 |
lemma not_is_prime_divisorE:
|
|
109 |
assumes "a \<noteq> 0" and "\<not> is_unit a" and "\<not> is_prime a"
|
|
110 |
obtains b where "b dvd a" and "\<not> is_unit b" and "\<not> a dvd b"
|
|
111 |
proof -
|
|
112 |
from assms have "\<exists>b. b dvd a \<and> \<not> is_unit b \<and> \<not> a dvd b"
|
|
113 |
by (auto intro: is_primeI)
|
|
114 |
with that show thesis by blast
|
|
115 |
qed
|
|
116 |
|
|
117 |
lemma prime_divisorE:
|
|
118 |
assumes "a \<noteq> 0" and "\<not> is_unit a"
|
|
119 |
obtains p where "is_prime p" and "p dvd a"
|
|
120 |
using assms no_prime_divisorsI [of a] by blast
|
|
121 |
|
|
122 |
lemma prime_dvd_mult_iff:
|
|
123 |
assumes "is_prime p"
|
|
124 |
shows "p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
|
|
125 |
using assms by (auto dest: is_primeD)
|
|
126 |
|
|
127 |
lemma prime_dvd_power_iff:
|
|
128 |
assumes "is_prime p"
|
|
129 |
shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
|
|
130 |
using assms by (induct n) (auto dest: is_prime_not_unit is_primeD)
|
|
131 |
|
|
132 |
lemma is_prime_normalize_iff [simp]:
|
|
133 |
"is_prime (normalize p) \<longleftrightarrow> is_prime p" (is "?P \<longleftrightarrow> ?Q")
|
|
134 |
proof
|
|
135 |
assume ?Q show ?P
|
|
136 |
by (rule is_primeI) (insert \<open>?Q\<close>, simp_all add: is_prime_not_zeroI is_prime_not_unit is_primeD2)
|
|
137 |
next
|
|
138 |
assume ?P show ?Q
|
|
139 |
by (rule is_primeI)
|
|
140 |
(insert is_prime_not_zeroI [of "normalize p"] is_prime_not_unit [of "normalize p"] is_primeD2 [of "normalize p"] \<open>?P\<close>, simp_all)
|
|
141 |
qed
|
|
142 |
|
|
143 |
lemma is_prime_inj_power:
|
|
144 |
assumes "is_prime p"
|
|
145 |
shows "inj (op ^ p)"
|
|
146 |
proof (rule injI, rule ccontr)
|
|
147 |
fix m n :: nat
|
|
148 |
have [simp]: "p ^ q = 1 \<longleftrightarrow> q = 0" (is "?P \<longleftrightarrow> ?Q") for q
|
|
149 |
proof
|
|
150 |
assume ?Q then show ?P by simp
|
|
151 |
next
|
|
152 |
assume ?P then have "is_unit (p ^ q)" by simp
|
|
153 |
with assms show ?Q by (auto simp add: is_unit_power_iff is_prime_not_unit)
|
|
154 |
qed
|
|
155 |
have *: False if "p ^ m = p ^ n" and "m > n" for m n
|
|
156 |
proof -
|
|
157 |
from assms have "p \<noteq> 0"
|
|
158 |
by (rule is_prime_not_zeroI)
|
|
159 |
then have "p ^ n \<noteq> 0"
|
|
160 |
by (induct n) simp_all
|
|
161 |
from that have "m = n + (m - n)" and "m - n > 0" by arith+
|
|
162 |
then obtain q where "m = n + q" and "q > 0" ..
|
|
163 |
with that have "p ^ n * p ^ q = p ^ n * 1" by (simp add: power_add)
|
|
164 |
with \<open>p ^ n \<noteq> 0\<close> have "p ^ q = 1"
|
|
165 |
using mult_left_cancel [of "p ^ n" "p ^ q" 1] by simp
|
|
166 |
with \<open>q > 0\<close> show ?thesis by simp
|
|
167 |
qed
|
|
168 |
assume "m \<noteq> n"
|
|
169 |
then have "m > n \<or> m < n" by arith
|
|
170 |
moreover assume "p ^ m = p ^ n"
|
|
171 |
ultimately show False using * [of m n] * [of n m] by auto
|
|
172 |
qed
|
|
173 |
|
|
174 |
lemma prime_unique:
|
|
175 |
assumes "is_prime q" and "is_prime p" and "q dvd p"
|
|
176 |
shows "normalize q = normalize p"
|
|
177 |
proof -
|
|
178 |
from assms have "p dvd q"
|
|
179 |
by (auto dest: is_primeD2 [of p] is_prime_not_unit [of q])
|
|
180 |
with assms show ?thesis
|
|
181 |
by (auto intro: associatedI)
|
|
182 |
qed
|
|
183 |
|
|
184 |
lemma exists_factorization:
|
|
185 |
assumes "a \<noteq> 0"
|
|
186 |
obtains P where "\<And>p. p \<in># P \<Longrightarrow> is_prime p" "msetprod P = normalize a"
|
|
187 |
proof -
|
|
188 |
let ?prime_factors = "\<lambda>a. {p. p dvd a \<and> is_prime p \<and> normalize p = p}"
|
|
189 |
have "?prime_factors a \<subseteq> {b. b dvd a \<and> normalize b = b}" by auto
|
|
190 |
moreover from assms have "finite {b. b dvd a \<and> normalize b = b}"
|
|
191 |
by (rule finite_divisors)
|
|
192 |
ultimately have "finite (?prime_factors a)" by (rule finite_subset)
|
|
193 |
then show thesis using \<open>a \<noteq> 0\<close> that proof (induct "?prime_factors a" arbitrary: thesis a)
|
|
194 |
case empty then have
|
|
195 |
P: "\<And>b. is_prime b \<Longrightarrow> b dvd a \<Longrightarrow> normalize b \<noteq> b" and "a \<noteq> 0"
|
|
196 |
by auto
|
|
197 |
have "is_unit a"
|
|
198 |
proof (rule no_prime_divisorsI)
|
|
199 |
fix b
|
|
200 |
assume "b dvd a"
|
|
201 |
then show "\<not> is_prime b"
|
|
202 |
using P [of "normalize b"] by auto
|
|
203 |
qed
|
|
204 |
then have "\<And>p. p \<in># {#} \<Longrightarrow> is_prime p" and "msetprod {#} = normalize a"
|
|
205 |
by (simp_all add: is_unit_normalize)
|
|
206 |
with empty show thesis by blast
|
|
207 |
next
|
|
208 |
case (insert p P)
|
|
209 |
from \<open>insert p P = ?prime_factors a\<close>
|
|
210 |
have "p dvd a" and "is_prime p" and "normalize p = p"
|
|
211 |
by auto
|
|
212 |
obtain n where "n > 0" and "p ^ n dvd a" and "\<not> p ^ Suc n dvd a"
|
|
213 |
proof (rule that)
|
|
214 |
def N \<equiv> "{n. p ^ n dvd a}"
|
|
215 |
from is_prime_inj_power \<open>is_prime p\<close> have "inj (op ^ p)" .
|
|
216 |
then have "inj_on (op ^ p) U" for U
|
|
217 |
by (rule subset_inj_on) simp
|
|
218 |
moreover have "op ^ p ` N \<subseteq> {b. b dvd a \<and> normalize b = b}"
|
|
219 |
by (auto simp add: normalize_power \<open>normalize p = p\<close> N_def)
|
|
220 |
ultimately have "finite N"
|
|
221 |
by (rule inj_on_finite) (simp add: finite_divisors \<open>a \<noteq> 0\<close>)
|
|
222 |
from N_def \<open>a \<noteq> 0\<close> have "0 \<in> N" by (simp add: N_def)
|
|
223 |
then have "N \<noteq> {}" by blast
|
|
224 |
note * = \<open>finite N\<close> \<open>N \<noteq> {}\<close>
|
|
225 |
from N_def \<open>p dvd a\<close> have "1 \<in> N" by simp
|
|
226 |
with * show "Max N > 0"
|
|
227 |
by (auto simp add: Max_gr_iff)
|
|
228 |
from * have "Max N \<in> N" by (rule Max_in)
|
|
229 |
then show "p ^ Max N dvd a" by (simp add: N_def)
|
|
230 |
from * have "\<forall>n\<in>N. n \<le> Max N"
|
|
231 |
by (simp add: Max_le_iff [symmetric])
|
|
232 |
then have "p ^ Suc (Max N) dvd a \<Longrightarrow> Suc (Max N) \<le> Max N"
|
|
233 |
by (rule bspec) (simp add: N_def)
|
|
234 |
then show "\<not> p ^ Suc (Max N) dvd a"
|
|
235 |
by auto
|
|
236 |
qed
|
|
237 |
from \<open>p ^ n dvd a\<close> obtain c where "a = p ^ n * c" ..
|
|
238 |
with \<open>\<not> p ^ Suc n dvd a\<close> have "\<not> p dvd c"
|
|
239 |
by (auto elim: dvdE simp add: ac_simps)
|
|
240 |
have "?prime_factors a - {p} = ?prime_factors c" (is "?A = ?B")
|
|
241 |
proof (rule set_eqI)
|
|
242 |
fix q
|
|
243 |
show "q \<in> ?A \<longleftrightarrow> q \<in> ?B"
|
|
244 |
using \<open>normalize p = p\<close> \<open>is_prime p\<close> \<open>a = p ^ n * c\<close> \<open>\<not> p dvd c\<close>
|
|
245 |
prime_unique [of q p]
|
|
246 |
by (auto simp add: prime_dvd_power_iff prime_dvd_mult_iff)
|
|
247 |
qed
|
|
248 |
moreover from insert have "P = ?prime_factors a - {p}"
|
|
249 |
by auto
|
|
250 |
ultimately have "P = ?prime_factors c"
|
|
251 |
by simp
|
|
252 |
moreover from \<open>a \<noteq> 0\<close> \<open>a = p ^ n * c\<close> have "c \<noteq> 0"
|
|
253 |
by auto
|
|
254 |
ultimately obtain P where "\<And>p. p \<in># P \<Longrightarrow> is_prime p" "msetprod P = normalize c"
|
|
255 |
using insert(3) by blast
|
|
256 |
with \<open>is_prime p\<close> \<open>a = p ^ n * c\<close> \<open>normalize p = p\<close>
|
|
257 |
have "\<And>q. q \<in># P + (replicate_mset n p) \<longrightarrow> is_prime q" "msetprod (P + replicate_mset n p) = normalize a"
|
|
258 |
by (auto simp add: ac_simps normalize_mult normalize_power)
|
|
259 |
with insert(6) show thesis by blast
|
|
260 |
qed
|
|
261 |
qed
|
|
262 |
|
|
263 |
end
|
|
264 |
|
|
265 |
instantiation nat :: factorial_semiring
|
|
266 |
begin
|
|
267 |
|
|
268 |
definition is_prime_nat :: "nat \<Rightarrow> bool"
|
|
269 |
where
|
|
270 |
"is_prime_nat p \<longleftrightarrow> (1 < p \<and> (\<forall>n. n dvd p \<longrightarrow> n = 1 \<or> n = p))"
|
|
271 |
|
|
272 |
lemma is_prime_eq_prime:
|
|
273 |
"is_prime = prime"
|
|
274 |
by (simp add: fun_eq_iff prime_def is_prime_nat_def)
|
|
275 |
|
|
276 |
instance proof
|
|
277 |
show "\<not> is_prime (0::nat)" by (simp add: is_prime_nat_def)
|
|
278 |
show "\<not> is_unit p" if "is_prime p" for p :: nat
|
|
279 |
using that by (simp add: is_prime_nat_def)
|
|
280 |
next
|
|
281 |
fix p :: nat
|
|
282 |
assume "p \<noteq> 0" and "\<not> is_unit p"
|
|
283 |
then have "p > 1" by simp
|
|
284 |
assume P: "\<And>n. n dvd p \<Longrightarrow> \<not> is_unit n \<Longrightarrow> p dvd n"
|
|
285 |
have "n = 1" if "n dvd p" "n \<noteq> p" for n
|
|
286 |
proof (rule ccontr)
|
|
287 |
assume "n \<noteq> 1"
|
|
288 |
with that P have "p dvd n" by auto
|
|
289 |
with \<open>n dvd p\<close> have "n = p" by (rule dvd_antisym)
|
|
290 |
with that show False by simp
|
|
291 |
qed
|
|
292 |
with \<open>p > 1\<close> show "is_prime p" by (auto simp add: is_prime_nat_def)
|
|
293 |
next
|
|
294 |
fix p m n :: nat
|
|
295 |
assume "is_prime p"
|
|
296 |
then have "prime p" by (simp add: is_prime_eq_prime)
|
|
297 |
moreover assume "p dvd m * n"
|
|
298 |
ultimately show "p dvd m \<or> p dvd n"
|
|
299 |
by (rule prime_dvd_mult_nat)
|
|
300 |
next
|
|
301 |
fix n :: nat
|
|
302 |
show "is_unit n" if "\<And>m. m dvd n \<Longrightarrow> \<not> is_prime m"
|
|
303 |
using that prime_factor_nat by (auto simp add: is_prime_eq_prime)
|
|
304 |
qed simp
|
|
305 |
|
|
306 |
end
|
|
307 |
|
|
308 |
instantiation int :: factorial_semiring
|
|
309 |
begin
|
|
310 |
|
|
311 |
definition is_prime_int :: "int \<Rightarrow> bool"
|
|
312 |
where
|
|
313 |
"is_prime_int p \<longleftrightarrow> is_prime (nat \<bar>p\<bar>)"
|
|
314 |
|
|
315 |
lemma is_prime_int_iff [simp]:
|
|
316 |
"is_prime (int n) \<longleftrightarrow> is_prime n"
|
|
317 |
by (simp add: is_prime_int_def)
|
|
318 |
|
|
319 |
lemma is_prime_nat_abs_iff [simp]:
|
|
320 |
"is_prime (nat \<bar>k\<bar>) \<longleftrightarrow> is_prime k"
|
|
321 |
by (simp add: is_prime_int_def)
|
|
322 |
|
|
323 |
instance proof
|
|
324 |
show "\<not> is_prime (0::int)" by (simp add: is_prime_int_def)
|
|
325 |
show "\<not> is_unit p" if "is_prime p" for p :: int
|
|
326 |
using that is_prime_not_unit [of "nat \<bar>p\<bar>"] by simp
|
|
327 |
next
|
|
328 |
fix p :: int
|
|
329 |
assume P: "\<And>k. k dvd p \<Longrightarrow> \<not> is_unit k \<Longrightarrow> p dvd k"
|
|
330 |
have "nat \<bar>p\<bar> dvd n" if "n dvd nat \<bar>p\<bar>" and "n \<noteq> Suc 0" for n :: nat
|
|
331 |
proof -
|
|
332 |
from that have "int n dvd p" by (simp add: int_dvd_iff)
|
|
333 |
moreover from that have "\<not> is_unit (int n)" by simp
|
|
334 |
ultimately have "p dvd int n" by (rule P)
|
|
335 |
with that have "p dvd int n" by auto
|
|
336 |
then show ?thesis by (simp add: dvd_int_iff)
|
|
337 |
qed
|
|
338 |
moreover assume "p \<noteq> 0" and "\<not> is_unit p"
|
|
339 |
ultimately have "is_prime (nat \<bar>p\<bar>)" by (intro is_primeI) auto
|
|
340 |
then show "is_prime p" by simp
|
|
341 |
next
|
|
342 |
fix p k l :: int
|
|
343 |
assume "is_prime p"
|
|
344 |
then have *: "is_prime (nat \<bar>p\<bar>)" by simp
|
|
345 |
assume "p dvd k * l"
|
|
346 |
then have "nat \<bar>p\<bar> dvd nat \<bar>k * l\<bar>"
|
62348
|
347 |
by (simp add: dvd_int_unfold_dvd_nat)
|
60804
|
348 |
then have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> * nat \<bar>l\<bar>"
|
|
349 |
by (simp add: abs_mult nat_mult_distrib)
|
|
350 |
with * have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> \<or> nat \<bar>p\<bar> dvd nat \<bar>l\<bar>"
|
|
351 |
using is_primeD [of "nat \<bar>p\<bar>"] by auto
|
|
352 |
then show "p dvd k \<or> p dvd l"
|
62348
|
353 |
by (simp add: dvd_int_unfold_dvd_nat)
|
60804
|
354 |
next
|
|
355 |
fix k :: int
|
|
356 |
assume P: "\<And>l. l dvd k \<Longrightarrow> \<not> is_prime l"
|
|
357 |
have "is_unit (nat \<bar>k\<bar>)"
|
|
358 |
proof (rule no_prime_divisorsI)
|
|
359 |
fix m
|
|
360 |
assume "m dvd nat \<bar>k\<bar>"
|
|
361 |
then have "int m dvd k" by (simp add: int_dvd_iff)
|
|
362 |
then have "\<not> is_prime (int m)" by (rule P)
|
|
363 |
then show "\<not> is_prime m" by simp
|
|
364 |
qed
|
|
365 |
then show "is_unit k" by simp
|
|
366 |
qed simp
|
|
367 |
|
|
368 |
end
|
|
369 |
|
|
370 |
end
|