author | eberlm <eberlm@in.tum.de> |
Sat, 15 Jul 2017 14:32:02 +0100 | |
changeset 66276 | acc3b7dd0b21 |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
1 |
(* |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
2 |
File: HOL/Number_Theory/Prime_Powers.thy |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
3 |
Author: Manuel Eberl <eberlm@in.tum.de> |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
4 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
5 |
Prime powers and the Mangoldt function |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
6 |
*) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
7 |
section \<open>Prime powers\<close> |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
8 |
theory Prime_Powers |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
9 |
imports Complex_Main "~~/src/HOL/Computational_Algebra/Primes" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
10 |
begin |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
11 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
12 |
definition aprimedivisor :: "'a :: normalization_semidom \<Rightarrow> 'a" where |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
13 |
"aprimedivisor q = (SOME p. prime p \<and> p dvd q)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
14 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
15 |
definition primepow :: "'a :: normalization_semidom \<Rightarrow> bool" where |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
16 |
"primepow n \<longleftrightarrow> (\<exists>p k. prime p \<and> k > 0 \<and> n = p ^ k)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
17 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
18 |
definition primepow_factors :: "'a :: normalization_semidom \<Rightarrow> 'a set" where |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
19 |
"primepow_factors n = {x. primepow x \<and> x dvd n}" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
20 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
21 |
lemma primepow_gt_Suc_0: "primepow n \<Longrightarrow> n > Suc 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
22 |
using one_less_power[of "p::nat" for p] by (auto simp: primepow_def prime_nat_iff) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
23 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
24 |
lemma |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
25 |
assumes "prime p" "p dvd n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
26 |
shows prime_aprimedivisor: "prime (aprimedivisor n)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
27 |
and aprimedivisor_dvd: "aprimedivisor n dvd n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
28 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
29 |
from assms have "\<exists>p. prime p \<and> p dvd n" by auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
30 |
from someI_ex[OF this] show "prime (aprimedivisor n)" "aprimedivisor n dvd n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
31 |
unfolding aprimedivisor_def by (simp_all add: conj_commute) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
32 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
33 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
34 |
lemma |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
35 |
assumes "n \<noteq> 0" "\<not>is_unit (n :: 'a :: factorial_semiring)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
36 |
shows prime_aprimedivisor': "prime (aprimedivisor n)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
37 |
and aprimedivisor_dvd': "aprimedivisor n dvd n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
38 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
39 |
from someI_ex[OF prime_divisor_exists[OF assms]] |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
40 |
show "prime (aprimedivisor n)" "aprimedivisor n dvd n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
41 |
unfolding aprimedivisor_def by (simp_all add: conj_commute) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
42 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
43 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
44 |
lemma aprimedivisor_of_prime [simp]: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
45 |
assumes "prime p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
46 |
shows "aprimedivisor p = p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
47 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
48 |
from assms have "\<exists>q. prime q \<and> q dvd p" by auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
49 |
from someI_ex[OF this, folded aprimedivisor_def] assms show ?thesis |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
50 |
by (auto intro: primes_dvd_imp_eq) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
51 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
52 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
53 |
lemma aprimedivisor_pos_nat: "(n::nat) > 1 \<Longrightarrow> aprimedivisor n > 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
54 |
using aprimedivisor_dvd'[of n] by (auto elim: dvdE intro!: Nat.gr0I) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
55 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
56 |
lemma aprimedivisor_primepow_power: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
57 |
assumes "primepow n" "k > 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
58 |
shows "aprimedivisor (n ^ k) = aprimedivisor n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
59 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
60 |
from assms obtain p l where l: "prime p" "l > 0" "n = p ^ l" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
61 |
by (auto simp: primepow_def) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
62 |
from l assms have *: "prime (aprimedivisor (n ^ k))" "aprimedivisor (n ^ k) dvd n ^ k" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
63 |
by (intro prime_aprimedivisor[of p] aprimedivisor_dvd[of p] dvd_power; |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
64 |
simp add: power_mult [symmetric])+ |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
65 |
from * l have "aprimedivisor (n ^ k) dvd p ^ (l * k)" by (simp add: power_mult) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
66 |
with assms * l have "aprimedivisor (n ^ k) dvd p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
67 |
by (subst (asm) prime_dvd_power_iff) simp_all |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
68 |
with l assms have "aprimedivisor (n ^ k) = p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
69 |
by (intro primes_dvd_imp_eq prime_aprimedivisor l) (auto simp: power_mult [symmetric]) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
70 |
moreover from l have "aprimedivisor n dvd p ^ l" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
71 |
by (auto intro: aprimedivisor_dvd simp: prime_gt_0_nat) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
72 |
with assms l have "aprimedivisor n dvd p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
73 |
by (subst (asm) prime_dvd_power_iff) (auto intro!: prime_aprimedivisor simp: prime_gt_0_nat) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
74 |
with l assms have "aprimedivisor n = p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
75 |
by (intro primes_dvd_imp_eq prime_aprimedivisor l) auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
76 |
ultimately show ?thesis by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
77 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
78 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
79 |
lemma aprimedivisor_prime_power: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
80 |
assumes "prime p" "k > 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
81 |
shows "aprimedivisor (p ^ k) = p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
82 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
83 |
from assms have *: "prime (aprimedivisor (p ^ k))" "aprimedivisor (p ^ k) dvd p ^ k" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
84 |
by (intro prime_aprimedivisor[of p] aprimedivisor_dvd[of p]; simp add: prime_nat_iff)+ |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
85 |
from assms * have "aprimedivisor (p ^ k) dvd p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
86 |
by (subst (asm) prime_dvd_power_iff) simp_all |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
87 |
with assms * show "aprimedivisor (p ^ k) = p" by (intro primes_dvd_imp_eq) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
88 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
89 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
90 |
lemma prime_factorization_primepow: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
91 |
assumes "primepow n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
92 |
shows "prime_factorization n = |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
93 |
replicate_mset (multiplicity (aprimedivisor n) n) (aprimedivisor n)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
94 |
using assms |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
95 |
by (auto simp: primepow_def aprimedivisor_prime_power prime_factorization_prime_power) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
96 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
97 |
lemma primepow_decompose: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
98 |
assumes "primepow n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
99 |
shows "aprimedivisor n ^ multiplicity (aprimedivisor n) n = n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
100 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
101 |
from assms have "n \<noteq> 0" by (intro notI) (auto simp: primepow_def) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
102 |
hence "n = unit_factor n * prod_mset (prime_factorization n)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
103 |
by (subst prod_mset_prime_factorization) simp_all |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
104 |
also from assms have "unit_factor n = 1" by (auto simp: primepow_def unit_factor_power) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
105 |
also have "prime_factorization n = |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
106 |
replicate_mset (multiplicity (aprimedivisor n) n) (aprimedivisor n)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
107 |
by (intro prime_factorization_primepow assms) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
108 |
also have "prod_mset \<dots> = aprimedivisor n ^ multiplicity (aprimedivisor n) n" by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
109 |
finally show ?thesis by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
110 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
111 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
112 |
lemma prime_power_not_one: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
113 |
assumes "prime p" "k > 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
114 |
shows "p ^ k \<noteq> 1" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
115 |
proof |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
116 |
assume "p ^ k = 1" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
117 |
hence "is_unit (p ^ k)" by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
118 |
thus False using assms by (simp add: is_unit_power_iff) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
119 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
120 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
121 |
lemma zero_not_primepow [simp]: "\<not>primepow 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
122 |
by (auto simp: primepow_def) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
123 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
124 |
lemma one_not_primepow [simp]: "\<not>primepow 1" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
125 |
by (auto simp: primepow_def prime_power_not_one) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
126 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
127 |
lemma primepow_not_unit [simp]: "primepow p \<Longrightarrow> \<not>is_unit p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
128 |
by (auto simp: primepow_def is_unit_power_iff) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
129 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
130 |
lemma unit_factor_primepow: "primepow p \<Longrightarrow> unit_factor p = 1" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
131 |
by (auto simp: primepow_def unit_factor_power) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
132 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
133 |
lemma aprimedivisor_primepow: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
134 |
assumes "prime p" "p dvd n" "primepow (n :: 'a :: factorial_semiring)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
135 |
shows "aprimedivisor (p * n) = p" "aprimedivisor n = p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
136 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
137 |
from assms have [simp]: "n \<noteq> 0" by auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
138 |
define q where "q = aprimedivisor n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
139 |
with assms have q: "prime q" by (auto simp: q_def intro!: prime_aprimedivisor) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
140 |
from \<open>primepow n\<close> have n: "n = q ^ multiplicity q n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
141 |
by (simp add: primepow_decompose q_def) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
142 |
have nz: "multiplicity q n \<noteq> 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
143 |
proof |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
144 |
assume "multiplicity q n = 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
145 |
with n have n': "n = unit_factor n" by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
146 |
have "is_unit n" by (subst n', rule unit_factor_is_unit) (insert assms, auto) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
147 |
with assms show False by auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
148 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
149 |
with \<open>prime p\<close> \<open>p dvd n\<close> q have "p dvd q" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
150 |
by (subst (asm) n) (auto intro: prime_dvd_power) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
151 |
with \<open>prime p\<close> q have "p = q" by (intro primes_dvd_imp_eq) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
152 |
thus "aprimedivisor n = p" by (simp add: q_def) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
153 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
154 |
define r where "r = aprimedivisor (p * n)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
155 |
with assms have r: "r dvd (p * n)" "prime r" unfolding r_def |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
156 |
by (intro aprimedivisor_dvd[of p] prime_aprimedivisor[of p]; simp)+ |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
157 |
hence "r dvd q ^ Suc (multiplicity q n)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
158 |
by (subst (asm) n) (auto simp: \<open>p = q\<close> dest: dvd_unit_imp_unit) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
159 |
with r have "r dvd q" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
160 |
by (auto intro: prime_dvd_power_nat simp: prime_dvd_mult_iff dest: prime_dvd_power) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
161 |
with r q have "r = q" by (intro primes_dvd_imp_eq) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
162 |
thus "aprimedivisor (p * n) = p" by (simp add: r_def \<open>p = q\<close>) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
163 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
164 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
165 |
lemma power_eq_prime_powerD: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
166 |
fixes p :: "'a :: factorial_semiring" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
167 |
assumes "prime p" "n > 0" "x ^ n = p ^ k" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
168 |
shows "\<exists>i. normalize x = normalize (p ^ i)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
169 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
170 |
have "normalize x = normalize (p ^ multiplicity p x)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
171 |
proof (rule multiplicity_eq_imp_eq) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
172 |
fix q :: 'a assume "prime q" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
173 |
from assms have "multiplicity q (x ^ n) = multiplicity q (p ^ k)" by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
174 |
with \<open>prime q\<close> and assms have "n * multiplicity q x = k * multiplicity q p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
175 |
by (subst (asm) (1 2) prime_elem_multiplicity_power_distrib) (auto simp: power_0_left) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
176 |
with assms and \<open>prime q\<close> show "multiplicity q x = multiplicity q (p ^ multiplicity p x)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
177 |
by (cases "p = q") (auto simp: multiplicity_distinct_prime_power prime_multiplicity_other) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
178 |
qed (insert assms, auto simp: power_0_left) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
179 |
thus ?thesis by auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
180 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
181 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
182 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
183 |
lemma primepow_power_iff: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
184 |
assumes "unit_factor p = 1" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
185 |
shows "primepow (p ^ n) \<longleftrightarrow> primepow (p :: 'a :: factorial_semiring) \<and> n > 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
186 |
proof safe |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
187 |
assume "primepow (p ^ n)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
188 |
hence n: "n \<noteq> 0" by (auto intro!: Nat.gr0I) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
189 |
thus "n > 0" by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
190 |
from assms have [simp]: "normalize p = p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
191 |
using normalize_mult_unit_factor[of p] by (simp only: mult.right_neutral) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
192 |
from \<open>primepow (p ^ n)\<close> obtain q k where *: "k > 0" "prime q" "p ^ n = q ^ k" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
193 |
by (auto simp: primepow_def) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
194 |
with power_eq_prime_powerD[of q n p k] n |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
195 |
obtain i where eq: "normalize p = normalize (q ^ i)" by auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
196 |
with primepow_not_unit[OF \<open>primepow (p ^ n)\<close>] have "i \<noteq> 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
197 |
by (intro notI) (simp add: normalize_1_iff is_unit_power_iff del: primepow_not_unit) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
198 |
with \<open>normalize p = normalize (q ^ i)\<close> \<open>prime q\<close> show "primepow p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
199 |
by (auto simp: normalize_power primepow_def intro!: exI[of _ q] exI[of _ i]) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
200 |
next |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
201 |
assume "primepow p" "n > 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
202 |
then obtain q k where *: "k > 0" "prime q" "p = q ^ k" by (auto simp: primepow_def) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
203 |
with \<open>n > 0\<close> show "primepow (p ^ n)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
204 |
by (auto simp: primepow_def power_mult intro!: exI[of _ q] exI[of _ "k * n"]) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
205 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
206 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
207 |
lemma primepow_prime [simp]: "prime n \<Longrightarrow> primepow n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
208 |
by (auto simp: primepow_def intro!: exI[of _ n] exI[of _ "1::nat"]) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
209 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
210 |
lemma primepow_prime_power [simp]: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
211 |
"prime (p :: 'a :: factorial_semiring) \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> n > 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
212 |
by (subst primepow_power_iff) auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
213 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
214 |
(* TODO Generalise *) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
215 |
lemma primepow_multD: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
216 |
assumes "primepow (a * b :: nat)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
217 |
shows "a = 1 \<or> primepow a" "b = 1 \<or> primepow b" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
218 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
219 |
from assms obtain p k where k: "k > 0" "a * b = p ^ k" "prime p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
220 |
unfolding primepow_def by auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
221 |
then obtain i j where "a = p ^ i" "b = p ^ j" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
222 |
using prime_power_mult_nat[of p a b] by blast |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
223 |
with \<open>prime p\<close> show "a = 1 \<or> primepow a" "b = 1 \<or> primepow b" by auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
224 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
225 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
226 |
lemma primepow_mult_aprimedivisorI: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
227 |
assumes "primepow (n :: 'a :: factorial_semiring)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
228 |
shows "primepow (aprimedivisor n * n)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
229 |
by (subst (2) primepow_decompose[OF assms, symmetric], subst power_Suc [symmetric], |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
230 |
subst primepow_prime_power) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
231 |
(insert assms, auto intro!: prime_aprimedivisor' dest: primepow_gt_Suc_0) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
232 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
233 |
lemma aprimedivisor_vimage: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
234 |
assumes "prime (p :: 'a :: factorial_semiring)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
235 |
shows "aprimedivisor -` {p} \<inter> primepow_factors n = {p ^ k |k. k > 0 \<and> p ^ k dvd n}" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
236 |
proof safe |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
237 |
fix q assume q: "q \<in> primepow_factors n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
238 |
hence q': "q \<noteq> 0" "q \<noteq> 1" by (auto simp: primepow_def primepow_factors_def prime_power_not_one) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
239 |
let ?n = "multiplicity (aprimedivisor q) q" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
240 |
from q q' have "q = aprimedivisor q ^ ?n \<and> ?n > 0 \<and> aprimedivisor q ^ ?n dvd n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
241 |
using prime_aprimedivisor'[of q] aprimedivisor_dvd'[of q] |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
242 |
by (subst primepow_decompose [symmetric]) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
243 |
(auto simp: primepow_factors_def multiplicity_gt_zero_iff unit_factor_primepow |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
244 |
intro: dvd_trans[OF multiplicity_dvd]) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
245 |
thus "\<exists>k. q = aprimedivisor q ^ k \<and> k > 0 \<and> aprimedivisor q ^ k dvd n" .. |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
246 |
next |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
247 |
fix k :: nat assume k: "p ^ k dvd n" "k > 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
248 |
with assms show "p ^ k \<in> aprimedivisor -` {p}" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
249 |
by (auto simp: aprimedivisor_prime_power) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
250 |
with assms k show "p ^ k \<in> primepow_factors n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
251 |
by (auto simp: primepow_factors_def primepow_def aprimedivisor_prime_power intro: Suc_leI) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
252 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
253 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
254 |
lemma primepow_factors_altdef: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
255 |
fixes x :: "'a :: factorial_semiring" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
256 |
assumes "x \<noteq> 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
257 |
shows "primepow_factors x = {p ^ k |p k. p \<in> prime_factors x \<and> k \<in> {0<.. multiplicity p x}}" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
258 |
proof (intro equalityI subsetI) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
259 |
fix q assume "q \<in> primepow_factors x" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
260 |
then obtain p k where pk: "prime p" "k > 0" "q = p ^ k" "q dvd x" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
261 |
unfolding primepow_factors_def primepow_def by blast |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
262 |
moreover have "k \<le> multiplicity p x" using pk assms by (intro multiplicity_geI) auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
263 |
ultimately show "q \<in> {p ^ k |p k. p \<in> prime_factors x \<and> k \<in> {0<.. multiplicity p x}}" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
264 |
by (auto simp: prime_factors_multiplicity intro!: exI[of _ p] exI[of _ k]) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
265 |
qed (auto simp: primepow_factors_def prime_factors_multiplicity multiplicity_dvd') |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
266 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
267 |
lemma finite_primepow_factors: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
268 |
assumes "x \<noteq> (0 :: 'a :: factorial_semiring)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
269 |
shows "finite (primepow_factors x)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
270 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
271 |
have "finite (SIGMA p:prime_factors x. {0<..multiplicity p x})" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
272 |
by (intro finite_SigmaI) simp_all |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
273 |
hence "finite ((\<lambda>(p,k). p ^ k) ` \<dots>)" (is "finite ?A") by (rule finite_imageI) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
274 |
also have "?A = primepow_factors x" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
275 |
using assms by (subst primepow_factors_altdef) fast+ |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
276 |
finally show ?thesis . |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
277 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
278 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
279 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
280 |
definition mangoldt :: "nat \<Rightarrow> 'a :: real_algebra_1" where |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
281 |
"mangoldt n = (if primepow n then of_real (ln (real (aprimedivisor n))) else 0)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
282 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
283 |
lemma of_real_mangoldt [simp]: "of_real (mangoldt n) = mangoldt n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
284 |
by (simp add: mangoldt_def) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
285 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
286 |
lemma mangoldt_sum: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
287 |
assumes "n \<noteq> 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
288 |
shows "(\<Sum>d | d dvd n. mangoldt d :: 'a :: real_algebra_1) = of_real (ln (real n))" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
289 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
290 |
have "(\<Sum>d | d dvd n. mangoldt d :: 'a) = of_real (\<Sum>d | d dvd n. mangoldt d)" by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
291 |
also have "(\<Sum>d | d dvd n. mangoldt d) = (\<Sum>d \<in> primepow_factors n. ln (real (aprimedivisor d)))" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
292 |
using assms by (intro sum.mono_neutral_cong_right) (auto simp: primepow_factors_def mangoldt_def) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
293 |
also have "\<dots> = ln (real (\<Prod>d \<in> primepow_factors n. aprimedivisor d))" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
294 |
using assms finite_primepow_factors[of n] |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
295 |
by (subst ln_prod [symmetric]) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
296 |
(auto simp: primepow_factors_def intro!: aprimedivisor_pos_nat |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
297 |
intro: Nat.gr0I primepow_gt_Suc_0) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
298 |
also have "primepow_factors n = |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
299 |
(\<lambda>(p,k). p ^ k) ` (SIGMA p:prime_factors n. {0<..multiplicity p n})" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
300 |
(is "_ = _ ` ?A") by (subst primepow_factors_altdef[OF assms]) fast+ |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
301 |
also have "prod aprimedivisor \<dots> = (\<Prod>(p,k)\<in>?A. aprimedivisor (p ^ k))" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
302 |
by (subst prod.reindex) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
303 |
(auto simp: inj_on_def prime_power_inj'' prime_factors_multiplicity |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
304 |
prod.Sigma [symmetric] case_prod_unfold) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
305 |
also have "\<dots> = (\<Prod>(p,k)\<in>?A. p)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
306 |
by (intro prod.cong refl) (auto simp: aprimedivisor_prime_power prime_factors_multiplicity) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
307 |
also have "\<dots> = (\<Prod>x\<in>prime_factors n. \<Prod>k\<in>{0<..multiplicity x n}. x)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
308 |
by (rule prod.Sigma [symmetric]) auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
309 |
also have "\<dots> = (\<Prod>x\<in>prime_factors n. x ^ multiplicity x n)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
310 |
by (intro prod.cong refl) (simp add: prod_constant) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
311 |
also have "\<dots> = n" using assms by (intro prime_factorization_nat [symmetric]) simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
312 |
finally show ?thesis . |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
313 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
314 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
315 |
end |