4 |
4 |
5 Prime powers and the Mangoldt function |
5 Prime powers and the Mangoldt function |
6 *) |
6 *) |
7 section \<open>Prime powers\<close> |
7 section \<open>Prime powers\<close> |
8 theory Prime_Powers |
8 theory Prime_Powers |
9 imports Complex_Main "HOL-Computational_Algebra.Primes" |
9 imports Complex_Main "HOL-Computational_Algebra.Primes" "HOL-Library.FuncSet" |
10 begin |
10 begin |
11 |
11 |
12 definition aprimedivisor :: "'a :: normalization_semidom \<Rightarrow> 'a" where |
12 definition aprimedivisor :: "'a :: normalization_semidom \<Rightarrow> 'a" where |
13 "aprimedivisor q = (SOME p. prime p \<and> p dvd q)" |
13 "aprimedivisor q = (SOME p. prime p \<and> p dvd q)" |
14 |
14 |
208 by (auto simp: primepow_def intro!: exI[of _ n] exI[of _ "1::nat"]) |
208 by (auto simp: primepow_def intro!: exI[of _ n] exI[of _ "1::nat"]) |
209 |
209 |
210 lemma primepow_prime_power [simp]: |
210 lemma primepow_prime_power [simp]: |
211 "prime (p :: 'a :: factorial_semiring) \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> n > 0" |
211 "prime (p :: 'a :: factorial_semiring) \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> n > 0" |
212 by (subst primepow_power_iff) auto |
212 by (subst primepow_power_iff) auto |
|
213 |
|
214 lemma bij_betw_primepows: |
|
215 "bij_betw (\<lambda>(p,k). p ^ Suc k :: 'a :: factorial_semiring) |
|
216 (Collect prime \<times> UNIV) (Collect primepow)" |
|
217 proof (rule bij_betwI [where ?g = "(\<lambda>n. (aprimedivisor n, multiplicity (aprimedivisor n) n - 1))"], |
|
218 goal_cases) |
|
219 case 1 |
|
220 show "(\<lambda>(p, k). p ^ Suc k :: 'a) \<in> Collect prime \<times> UNIV \<rightarrow> Collect primepow" |
|
221 by (auto intro!: primepow_prime_power simp del: power_Suc ) |
|
222 next |
|
223 case 2 |
|
224 show ?case |
|
225 by (auto simp: primepow_def prime_aprimedivisor) |
|
226 next |
|
227 case (3 n) |
|
228 thus ?case |
|
229 by (auto simp: aprimedivisor_prime_power simp del: power_Suc) |
|
230 next |
|
231 case (4 n) |
|
232 hence *: "0 < multiplicity (aprimedivisor n) n" |
|
233 by (subst prime_multiplicity_gt_zero_iff) |
|
234 (auto intro!: prime_imp_prime_elem aprimedivisor_dvd simp: primepow_def prime_aprimedivisor) |
|
235 have "aprimedivisor n * aprimedivisor n ^ (multiplicity (aprimedivisor n) n - Suc 0) = |
|
236 aprimedivisor n ^ Suc (multiplicity (aprimedivisor n) n - Suc 0)" by simp |
|
237 also from * have "Suc (multiplicity (aprimedivisor n) n - Suc 0) = |
|
238 multiplicity (aprimedivisor n) n" |
|
239 by (subst Suc_diff_Suc) (auto simp: prime_multiplicity_gt_zero_iff) |
|
240 also have "aprimedivisor n ^ \<dots> = n" |
|
241 using 4 by (subst primepow_decompose) auto |
|
242 finally show ?case by auto |
|
243 qed |
213 |
244 |
214 (* TODO Generalise *) |
245 (* TODO Generalise *) |
215 lemma primepow_multD: |
246 lemma primepow_multD: |
216 assumes "primepow (a * b :: nat)" |
247 assumes "primepow (a * b :: nat)" |
217 shows "a = 1 \<or> primepow a" "b = 1 \<or> primepow b" |
248 shows "a = 1 \<or> primepow a" "b = 1 \<or> primepow b" |