--- a/src/HOL/Computational_Algebra/Computational_Algebra.thy Wed Jul 12 18:42:32 2017 +0200
+++ b/src/HOL/Computational_Algebra/Computational_Algebra.thy Sat Jul 15 14:32:02 2017 +0100
@@ -9,9 +9,11 @@
Fraction_Field
Fundamental_Theorem_Algebra
Normalized_Fraction
+ Nth_Powers
Polynomial_FPS
Polynomial
Primes
+ Squarefree
begin
end
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Wed Jul 12 18:42:32 2017 +0200
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Sat Jul 15 14:32:02 2017 +0100
@@ -13,6 +13,12 @@
subsection \<open>Irreducible and prime elements\<close>
+(* TODO: Move ? *)
+lemma (in semiring_gcd) prod_coprime' [rule_format]:
+ "(\<forall>i\<in>A. gcd a (f i) = 1) \<longrightarrow> gcd a (\<Prod>i\<in>A. f i) = 1"
+ using prod_coprime[of A f a] by (simp add: gcd.commute)
+
+
context comm_semiring_1
begin
@@ -217,6 +223,7 @@
qed
qed
with that show thesis by blast
+
qed
context
@@ -464,6 +471,9 @@
lemma prime_dvd_prod_mset_iff: "prime p \<Longrightarrow> p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+)
+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)"
+ by (auto simp: prime_dvd_prod_mset_iff prod_unfold_prod_mset)
+
lemma primes_dvd_imp_eq:
assumes "prime p" "prime q" "p dvd q"
shows "p = q"
@@ -1104,6 +1114,40 @@
by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)])
qed (insert assms, auto simp: multiplicity_unit_left)
+lemma prime_power_inj:
+ assumes "prime a" "a ^ m = a ^ n"
+ shows "m = n"
+proof -
+ have "multiplicity a (a ^ m) = multiplicity a (a ^ n)" by (simp only: assms)
+ thus ?thesis using assms by (subst (asm) (1 2) multiplicity_prime_power) simp_all
+qed
+
+lemma prime_power_inj':
+ assumes "prime p" "prime q"
+ assumes "p ^ m = q ^ n" "m > 0" "n > 0"
+ shows "p = q" "m = n"
+proof -
+ from assms have "p ^ 1 dvd p ^ m" by (intro le_imp_power_dvd) simp
+ also have "p ^ m = q ^ n" by fact
+ finally have "p dvd q ^ n" by simp
+ with assms have "p dvd q" using prime_dvd_power[of p q] by simp
+ with assms show "p = q" by (simp add: primes_dvd_imp_eq)
+ with assms show "m = n" by (simp add: prime_power_inj)
+qed
+
+lemma prime_power_eq_one_iff [simp]: "prime p \<Longrightarrow> p ^ n = 1 \<longleftrightarrow> n = 0"
+ using prime_power_inj[of p n 0] by auto
+
+lemma one_eq_prime_power_iff [simp]: "prime p \<Longrightarrow> 1 = p ^ n \<longleftrightarrow> n = 0"
+ using prime_power_inj[of p 0 n] by auto
+
+lemma prime_power_inj'':
+ assumes "prime p" "prime q"
+ shows "p ^ m = q ^ n \<longleftrightarrow> (m = 0 \<and> n = 0) \<or> (p = q \<and> m = n)"
+ using assms
+ by (cases "m = 0"; cases "n = 0")
+ (auto dest: prime_power_inj'[OF assms])
+
lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}"
by (simp add: multiset_eq_iff count_prime_factorization)
@@ -1265,6 +1309,12 @@
finally show ?thesis .
qed
+lemma prime_factorization_prod:
+ assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
+ shows "prime_factorization (prod f A) = (\<Sum>n\<in>A. prime_factorization (f n))"
+ using assms by (induction A rule: finite_induct)
+ (auto simp: Sup_multiset_empty prime_factorization_mult)
+
lemma prime_elem_multiplicity_mult_distrib:
assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
shows "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
@@ -1462,6 +1512,18 @@
thus ?thesis by simp
qed
+lemma inj_on_Prod_primes:
+ assumes "\<And>P p. P \<in> A \<Longrightarrow> p \<in> P \<Longrightarrow> prime p"
+ assumes "\<And>P. P \<in> A \<Longrightarrow> finite P"
+ shows "inj_on Prod A"
+proof (rule inj_onI)
+ fix P Q assume PQ: "P \<in> A" "Q \<in> A" "\<Prod>P = \<Prod>Q"
+ with prime_factorization_unique'[of "mset_set P" "mset_set Q"] assms[of P] assms[of Q]
+ have "mset_set P = mset_set Q" by (auto simp: prod_unfold_prod_mset)
+ with assms[of P] assms[of Q] PQ show "P = Q" by simp
+qed
+
+
subsection \<open>GCD and LCM computation with unique factorizations\<close>
@@ -1729,6 +1791,16 @@
using assms
by (simp add: prime_factorization_Lcm_factorial Lcm_eq_Lcm_factorial Lcm_factorial_eq_0_iff)
+lemma prime_factors_gcd [simp]:
+ "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> prime_factors (gcd a b) =
+ prime_factors a \<inter> prime_factors b"
+ by (subst prime_factorization_gcd) auto
+
+lemma prime_factors_lcm [simp]:
+ "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> prime_factors (lcm a b) =
+ prime_factors a \<union> prime_factors b"
+ by (subst prime_factorization_lcm) auto
+
subclass semiring_gcd
by (standard, unfold gcd_eq_gcd_factorial lcm_eq_lcm_factorial)
(rule gcd_lcm_factorial; assumption)+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Computational_Algebra/Nth_Powers.thy Sat Jul 15 14:32:02 2017 +0100
@@ -0,0 +1,307 @@
+(*
+ File: HOL/Computational_Algebra/Nth_Powers.thy
+ Author: Manuel Eberl <eberlm@in.tum.de>
+
+ n-th powers in general and n-th roots of natural numbers
+*)
+section \<open>$n$-th powers and roots of naturals\<close>
+theory Nth_Powers
+ imports Primes
+begin
+
+subsection \<open>The set of $n$-th powers\<close>
+
+definition is_nth_power :: "nat \<Rightarrow> 'a :: monoid_mult \<Rightarrow> bool" where
+ "is_nth_power n x \<longleftrightarrow> (\<exists>y. x = y ^ n)"
+
+lemma is_nth_power_nth_power [simp, intro]: "is_nth_power n (x ^ n)"
+ by (auto simp add: is_nth_power_def)
+
+lemma is_nth_powerI [intro?]: "x = y ^ n \<Longrightarrow> is_nth_power n x"
+ by (auto simp: is_nth_power_def)
+
+lemma is_nth_powerE: "is_nth_power n x \<Longrightarrow> (\<And>y. x = y ^ n \<Longrightarrow> P) \<Longrightarrow> P"
+ by (auto simp: is_nth_power_def)
+
+
+abbreviation is_square where "is_square \<equiv> is_nth_power 2"
+
+lemma is_zeroth_power [simp]: "is_nth_power 0 x \<longleftrightarrow> x = 1"
+ by (simp add: is_nth_power_def)
+
+lemma is_first_power [simp]: "is_nth_power 1 x"
+ by (simp add: is_nth_power_def)
+
+lemma is_first_power' [simp]: "is_nth_power (Suc 0) x"
+ by (simp add: is_nth_power_def)
+
+lemma is_nth_power_0 [simp]: "n > 0 \<Longrightarrow> is_nth_power n (0 :: 'a :: semiring_1)"
+ by (auto simp: is_nth_power_def power_0_left intro!: exI[of _ 0])
+
+lemma is_nth_power_0_iff [simp]: "is_nth_power n (0 :: 'a :: semiring_1) \<longleftrightarrow> n > 0"
+ by (cases n) auto
+
+lemma is_nth_power_1 [simp]: "is_nth_power n 1"
+ by (auto simp: is_nth_power_def intro!: exI[of _ 1])
+
+lemma is_nth_power_Suc_0 [simp]: "is_nth_power n (Suc 0)"
+ by (simp add: One_nat_def [symmetric] del: One_nat_def)
+
+lemma is_nth_power_conv_multiplicity:
+ fixes x :: "'a :: factorial_semiring"
+ assumes "n > 0"
+ shows "is_nth_power n (normalize x) \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)"
+proof (cases "x = 0")
+ case False
+ show ?thesis
+ proof (safe intro!: is_nth_powerI elim!: is_nth_powerE)
+ fix y p :: 'a assume *: "normalize x = y ^ n" "prime p"
+ with assms and False have [simp]: "y \<noteq> 0" by (auto simp: power_0_left)
+ have "multiplicity p x = multiplicity p (y ^ n)"
+ by (subst *(1) [symmetric]) simp
+ with False and * and assms show "n dvd multiplicity p x"
+ by (auto simp: prime_elem_multiplicity_power_distrib)
+ next
+ assume *: "\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x"
+ have "multiplicity p ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n) =
+ multiplicity p x" if "prime p" for p
+ proof -
+ from that and * have "n dvd multiplicity p x" by blast
+ have "multiplicity p x = 0" if "p \<notin> prime_factors x"
+ using that and \<open>prime p\<close> by (simp add: prime_factors_multiplicity)
+ with that and * and assms show ?thesis unfolding prod_power_distrib power_mult [symmetric]
+ by (subst multiplicity_prod_prime_powers) (auto simp: in_prime_factors_imp_prime elim: dvdE)
+ qed
+ with assms False
+ have "normalize x = normalize ((\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n)"
+ by (intro multiplicity_eq_imp_eq) (auto simp: multiplicity_prod_prime_powers)
+ thus "normalize x = normalize (\<Prod>p\<in>prime_factors x. p ^ (multiplicity p x div n)) ^ n"
+ by (simp add: normalize_power)
+ qed
+qed (insert assms, auto)
+
+lemma is_nth_power_conv_multiplicity_nat:
+ assumes "n > 0"
+ shows "is_nth_power n (x :: nat) \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)"
+ using is_nth_power_conv_multiplicity[OF assms, of x] by simp
+
+lemma is_nth_power_mult:
+ assumes "is_nth_power n a" "is_nth_power n b"
+ shows "is_nth_power n (a * b :: 'a :: comm_monoid_mult)"
+proof -
+ from assms obtain a' b' where "a = a' ^ n" "b = b' ^ n" by (auto elim!: is_nth_powerE)
+ hence "a * b = (a' * b') ^ n" by (simp add: power_mult_distrib)
+ thus ?thesis by (rule is_nth_powerI)
+qed
+
+lemma is_nth_power_mult_coprime_natD:
+ fixes a b :: nat
+ assumes "coprime a b" "is_nth_power n (a * b)" "a > 0" "b > 0"
+ shows "is_nth_power n a" "is_nth_power n b"
+proof -
+ have A: "is_nth_power n a" if "coprime a b" "is_nth_power n (a * b)" "a \<noteq> 0" "b \<noteq> 0" "n > 0"
+ for a b :: nat unfolding is_nth_power_conv_multiplicity_nat[OF \<open>n > 0\<close>]
+ proof safe
+ fix p :: nat assume p: "prime p"
+ from \<open>coprime a b\<close> have "\<not>(p dvd a \<and> p dvd b)"
+ using coprime_common_divisor_nat[of a b p] p by auto
+ moreover from that and p
+ have "n dvd multiplicity p a + multiplicity p b"
+ by (auto simp: is_nth_power_conv_multiplicity_nat prime_elem_multiplicity_mult_distrib)
+ ultimately show "n dvd multiplicity p a"
+ by (auto simp: not_dvd_imp_multiplicity_0)
+ qed
+ from A[of a b] assms show "is_nth_power n a" by (cases "n = 0") simp_all
+ from A[of b a] assms show "is_nth_power n b"
+ by (cases "n = 0") (simp_all add: gcd.commute mult.commute)
+qed
+
+lemma is_nth_power_mult_coprime_nat_iff:
+ fixes a b :: nat
+ assumes "coprime a b"
+ shows "is_nth_power n (a * b) \<longleftrightarrow> is_nth_power n a \<and>is_nth_power n b"
+ using assms
+ by (cases "a = 0"; cases "b = 0")
+ (auto intro: is_nth_power_mult dest: is_nth_power_mult_coprime_natD[of a b n]
+ simp del: One_nat_def)
+
+lemma is_nth_power_prime_power_nat_iff:
+ fixes p :: nat assumes "prime p"
+ shows "is_nth_power n (p ^ k) \<longleftrightarrow> n dvd k"
+ using assms
+ by (cases "n > 0")
+ (auto simp: is_nth_power_conv_multiplicity_nat prime_elem_multiplicity_power_distrib)
+
+lemma is_nth_power_nth_power':
+ assumes "n dvd n'"
+ shows "is_nth_power n (m ^ n')"
+proof -
+ from assms have "n' = n' div n * n" by simp
+ also have "m ^ \<dots> = (m ^ (n' div n)) ^ n" by (simp add: power_mult)
+ also have "is_nth_power n \<dots>" by simp
+ finally show ?thesis .
+qed
+
+definition is_nth_power_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+ where [code_abbrev]: "is_nth_power_nat = is_nth_power"
+
+lemma is_nth_power_nat_code [code]:
+ "is_nth_power_nat n m =
+ (if n = 0 then m = 1
+ else if m = 0 then n > 0
+ else if n = 1 then True
+ else (\<exists>k\<in>{1..m}. k ^ n = m))"
+ by (auto simp: is_nth_power_nat_def is_nth_power_def power_eq_iff_eq_base self_le_power)
+
+
+(* TODO: Harmonise with Discrete.sqrt *)
+
+subsection \<open>The $n$-root of a natural number\<close>
+
+definition nth_root_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+ "nth_root_nat k n = (if k = 0 then 0 else Max {m. m ^ k \<le> n})"
+
+lemma zeroth_root_nat [simp]: "nth_root_nat 0 n = 0"
+ by (simp add: nth_root_nat_def)
+
+lemma nth_root_nat_aux1:
+ assumes "k > 0"
+ shows "{m::nat. m ^ k \<le> n} \<subseteq> {..n}"
+proof safe
+ fix m assume "m ^ k \<le> n"
+ show "m \<le> n"
+ proof (cases "m = 0")
+ case False
+ with assms have "m ^ 1 \<le> m ^ k" by (intro power_increasing) simp_all
+ also note \<open>m ^ k \<le> n\<close>
+ finally show ?thesis by simp
+ qed simp_all
+qed
+
+lemma nth_root_nat_aux2:
+ assumes "k > 0"
+ shows "finite {m::nat. m ^ k \<le> n}" "{m::nat. m ^ k \<le> n} \<noteq> {}"
+proof -
+ from assms have "{m. m ^ k \<le> n} \<subseteq> {..n}" by (rule nth_root_nat_aux1)
+ moreover have "finite {..n}" by simp
+ ultimately show "finite {m::nat. m ^ k \<le> n}" by (rule finite_subset)
+next
+ from assms show "{m::nat. m ^ k \<le> n} \<noteq> {}" by (auto intro!: exI[of _ 0] simp: power_0_left)
+qed
+
+lemma
+ assumes "k > 0"
+ shows nth_root_nat_power_le: "nth_root_nat k n ^ k \<le> n"
+ and nth_root_nat_ge: "x ^ k \<le> n \<Longrightarrow> x \<le> nth_root_nat k n"
+ using Max_in[OF nth_root_nat_aux2[OF assms], of n]
+ Max_ge[OF nth_root_nat_aux2(1)[OF assms], of x n] assms
+ by (auto simp: nth_root_nat_def)
+
+lemma nth_root_nat_less:
+ assumes "k > 0" "x ^ k > n"
+ shows "nth_root_nat k n < x"
+proof -
+ from \<open>k > 0\<close> have "nth_root_nat k n ^ k \<le> n" by (rule nth_root_nat_power_le)
+ also have "n < x ^ k" by fact
+ finally show ?thesis by (rule power_less_imp_less_base) simp_all
+qed
+
+lemma nth_root_nat_unique:
+ assumes "m ^ k \<le> n" "(m + 1) ^ k > n"
+ shows "nth_root_nat k n = m"
+proof (cases "k > 0")
+ case True
+ from nth_root_nat_less[OF \<open>k > 0\<close> assms(2)]
+ have "nth_root_nat k n \<le> m" by simp
+ moreover from \<open>k > 0\<close> and assms(1) have "nth_root_nat k n \<ge> m"
+ by (intro nth_root_nat_ge)
+ ultimately show ?thesis by (rule antisym)
+qed (insert assms, auto)
+
+lemma nth_root_nat_0 [simp]: "nth_root_nat k 0 = 0" by (simp add: nth_root_nat_def)
+lemma nth_root_nat_1 [simp]: "k > 0 \<Longrightarrow> nth_root_nat k 1 = 1"
+ by (rule nth_root_nat_unique) (auto simp del: One_nat_def)
+lemma nth_root_nat_Suc_0 [simp]: "k > 0 \<Longrightarrow> nth_root_nat k (Suc 0) = Suc 0"
+ using nth_root_nat_1 by (simp del: nth_root_nat_1)
+
+lemma first_root_nat [simp]: "nth_root_nat 1 n = n"
+ by (intro nth_root_nat_unique) auto
+
+lemma first_root_nat' [simp]: "nth_root_nat (Suc 0) n = n"
+ by (intro nth_root_nat_unique) auto
+
+
+lemma nth_root_nat_code_naive':
+ "nth_root_nat k n = (if k = 0 then 0 else Max (Set.filter (\<lambda>m. m ^ k \<le> n) {..n}))"
+proof (cases "k > 0")
+ case True
+ hence "{m. m ^ k \<le> n} \<subseteq> {..n}" by (rule nth_root_nat_aux1)
+ hence "Set.filter (\<lambda>m. m ^ k \<le> n) {..n} = {m. m ^ k \<le> n}"
+ by (auto simp: Set.filter_def)
+ with True show ?thesis by (simp add: nth_root_nat_def Set.filter_def)
+qed simp
+
+function nth_root_nat_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
+ "nth_root_nat_aux m k acc n =
+ (let acc' = (k + 1) ^ m
+ in if k \<ge> n \<or> acc' > n then k else nth_root_nat_aux m (k+1) acc' n)"
+ by auto
+termination by (relation "measure (\<lambda>(_,k,_,n). n - k)", goal_cases) auto
+
+lemma nth_root_nat_aux_le:
+ assumes "k ^ m \<le> n" "m > 0"
+ shows "nth_root_nat_aux m k (k ^ m) n ^ m \<le> n"
+ using assms
+ by (induction m k "k ^ m" n rule: nth_root_nat_aux.induct) (auto simp: Let_def)
+
+lemma nth_root_nat_aux_gt:
+ assumes "m > 0"
+ shows "(nth_root_nat_aux m k (k ^ m) n + 1) ^ m > n"
+ using assms
+proof (induction m k "k ^ m" n rule: nth_root_nat_aux.induct)
+ case (1 m k n)
+ have "n < Suc k ^ m" if "n \<le> k"
+ proof -
+ note that
+ also have "k < Suc k ^ 1" by simp
+ also from \<open>m > 0\<close> have "\<dots> \<le> Suc k ^ m" by (intro power_increasing) simp_all
+ finally show ?thesis .
+ qed
+ with 1 show ?case by (auto simp: Let_def)
+qed
+
+lemma nth_root_nat_aux_correct:
+ assumes "k ^ m \<le> n" "m > 0"
+ shows "nth_root_nat_aux m k (k ^ m) n = nth_root_nat m n"
+ by (rule sym, intro nth_root_nat_unique nth_root_nat_aux_le nth_root_nat_aux_gt assms)
+
+lemma nth_root_nat_naive_code [code]:
+ "nth_root_nat m n = (if m = 0 \<or> n = 0 then 0 else if m = 1 \<or> n = 1 then n else
+ nth_root_nat_aux m 1 1 n)"
+ using nth_root_nat_aux_correct[of 1 m n] by (auto simp: )
+
+
+lemma nth_root_nat_nth_power [simp]: "k > 0 \<Longrightarrow> nth_root_nat k (n ^ k) = n"
+ by (intro nth_root_nat_unique order.refl power_strict_mono) simp_all
+
+lemma nth_root_nat_nth_power':
+ assumes "k > 0" "k dvd m"
+ shows "nth_root_nat k (n ^ m) = n ^ (m div k)"
+proof -
+ from assms have "m = (m div k) * k" by simp
+ also have "n ^ \<dots> = (n ^ (m div k)) ^ k" by (simp add: power_mult)
+ also from assms have "nth_root_nat k \<dots> = n ^ (m div k)" by simp
+ finally show ?thesis .
+qed
+
+lemma nth_root_nat_mono:
+ assumes "m \<le> n"
+ shows "nth_root_nat k m \<le> nth_root_nat k n"
+proof (cases "k = 0")
+ case False
+ with assms show ?thesis unfolding nth_root_nat_def
+ using nth_root_nat_aux2[of k m] nth_root_nat_aux2[of k n]
+ by (auto intro!: Max_mono)
+qed auto
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Computational_Algebra/Squarefree.thy Sat Jul 15 14:32:02 2017 +0100
@@ -0,0 +1,360 @@
+(*
+ File: HOL/Computational_Algebra/Squarefree.thy
+ Author: Manuel Eberl <eberlm@in.tum.de>
+
+ Squarefreeness and decomposition of ring elements into square part and squarefree part
+*)
+section \<open>Squarefreeness\<close>
+theory Squarefree
+imports Primes
+begin
+
+(* TODO: Generalise to n-th powers *)
+
+definition squarefree :: "'a :: comm_monoid_mult \<Rightarrow> bool" where
+ "squarefree n \<longleftrightarrow> (\<forall>x. x ^ 2 dvd n \<longrightarrow> x dvd 1)"
+
+lemma squarefreeI: "(\<And>x. x ^ 2 dvd n \<Longrightarrow> x dvd 1) \<Longrightarrow> squarefree n"
+ by (auto simp: squarefree_def)
+
+lemma squarefreeD: "squarefree n \<Longrightarrow> x ^ 2 dvd n \<Longrightarrow> x dvd 1"
+ by (auto simp: squarefree_def)
+
+lemma not_squarefreeI: "x ^ 2 dvd n \<Longrightarrow> \<not>x dvd 1 \<Longrightarrow> \<not>squarefree n"
+ by (auto simp: squarefree_def)
+
+lemma not_squarefreeE [case_names square_dvd]:
+ "\<not>squarefree n \<Longrightarrow> (\<And>x. x ^ 2 dvd n \<Longrightarrow> \<not>x dvd 1 \<Longrightarrow> P) \<Longrightarrow> P"
+ by (auto simp: squarefree_def)
+
+lemma not_squarefree_0 [simp]: "\<not>squarefree (0 :: 'a :: comm_semiring_1)"
+ by (rule not_squarefreeI[of 0]) auto
+
+lemma squarefree_factorial_semiring:
+ assumes "n \<noteq> 0"
+ shows "squarefree (n :: 'a :: factorial_semiring) \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> \<not>p ^ 2 dvd n)"
+ unfolding squarefree_def
+proof safe
+ assume *: "\<forall>p. prime p \<longrightarrow> \<not>p ^ 2 dvd n"
+ fix x :: 'a assume x: "x ^ 2 dvd n"
+ {
+ assume "\<not>is_unit x"
+ moreover from assms and x have "x \<noteq> 0" by auto
+ ultimately obtain p where "p dvd x" "prime p"
+ using prime_divisor_exists by blast
+ with * have "\<not>p ^ 2 dvd n" by blast
+ moreover from \<open>p dvd x\<close> have "p ^ 2 dvd x ^ 2" by (rule dvd_power_same)
+ ultimately have "\<not>x ^ 2 dvd n" by (blast dest: dvd_trans)
+ with x have False by contradiction
+ }
+ thus "is_unit x" by blast
+qed auto
+
+lemma squarefree_factorial_semiring':
+ assumes "n \<noteq> 0"
+ shows "squarefree (n :: 'a :: factorial_semiring) \<longleftrightarrow>
+ (\<forall>p\<in>prime_factors n. multiplicity p n = 1)"
+proof (subst squarefree_factorial_semiring [OF assms], safe)
+ fix p assume "\<forall>p\<in>#prime_factorization n. multiplicity p n = 1" "prime p" "p^2 dvd n"
+ with assms show False
+ by (cases "p dvd n")
+ (auto simp: prime_factors_dvd power_dvd_iff_le_multiplicity not_dvd_imp_multiplicity_0)
+qed (auto intro!: multiplicity_eqI simp: power2_eq_square [symmetric])
+
+lemma squarefree_factorial_semiring'':
+ assumes "n \<noteq> 0"
+ shows "squarefree (n :: 'a :: factorial_semiring) \<longleftrightarrow>
+ (\<forall>p. prime p \<longrightarrow> multiplicity p n \<le> 1)"
+ by (subst squarefree_factorial_semiring'[OF assms]) (auto simp: prime_factors_multiplicity)
+
+lemma squarefree_unit [simp]: "is_unit n \<Longrightarrow> squarefree n"
+proof (rule squarefreeI)
+ fix x assume "x^2 dvd n" "n dvd 1"
+ hence "is_unit (x^2)" by (rule dvd_unit_imp_unit)
+ thus "is_unit x" by (simp add: is_unit_power_iff)
+qed
+
+lemma squarefree_1 [simp]: "squarefree (1 :: 'a :: algebraic_semidom)"
+ by simp
+
+lemma squarefree_minus [simp]: "squarefree (-n :: 'a :: comm_ring_1) \<longleftrightarrow> squarefree n"
+ by (simp add: squarefree_def)
+
+lemma squarefree_mono: "a dvd b \<Longrightarrow> squarefree b \<Longrightarrow> squarefree a"
+ by (auto simp: squarefree_def intro: dvd_trans)
+
+lemma squarefree_multD:
+ assumes "squarefree (a * b)"
+ shows "squarefree a" "squarefree b"
+ by (rule squarefree_mono[OF _ assms], simp)+
+
+lemma squarefree_prime_elem:
+ assumes "prime_elem (p :: 'a :: factorial_semiring)"
+ shows "squarefree p"
+proof -
+ from assms have "p \<noteq> 0" by auto
+ show ?thesis
+ proof (subst squarefree_factorial_semiring [OF \<open>p \<noteq> 0\<close>]; safe)
+ fix q assume *: "prime q" "q^2 dvd p"
+ with assms have "multiplicity q p \<ge> 2" by (intro multiplicity_geI) auto
+ thus False using assms \<open>prime q\<close> prime_multiplicity_other[of q "normalize p"]
+ by (cases "q = normalize p") simp_all
+ qed
+qed
+
+lemma squarefree_prime:
+ assumes "prime (p :: 'a :: factorial_semiring)"
+ shows "squarefree p"
+ using assms by (intro squarefree_prime_elem) auto
+
+lemma squarefree_mult_coprime:
+ fixes a b :: "'a :: factorial_semiring_gcd"
+ assumes "coprime a b" "squarefree a" "squarefree b"
+ shows "squarefree (a * b)"
+proof -
+ from assms have nz: "a * b \<noteq> 0" by auto
+ show ?thesis unfolding squarefree_factorial_semiring'[OF nz]
+ proof
+ fix p assume p: "p \<in> prime_factors (a * b)"
+ {
+ assume "p dvd a \<and> p dvd b"
+ hence "p dvd gcd a b" by simp
+ also have "gcd a b = 1" by fact
+ finally have False using nz using p by (auto simp: prime_factors_dvd)
+ }
+ hence "\<not>(p dvd a \<and> p dvd b)" by blast
+ moreover from p have "p dvd a \<or> p dvd b" using nz
+ by (auto simp: prime_factors_dvd prime_dvd_mult_iff)
+ ultimately show "multiplicity p (a * b) = 1" using nz p assms(2,3)
+ by (auto simp: prime_elem_multiplicity_mult_distrib prime_factors_multiplicity
+ not_dvd_imp_multiplicity_0 squarefree_factorial_semiring')
+ qed
+qed
+
+lemma squarefree_prod_coprime:
+ fixes f :: "'a \<Rightarrow> 'b :: factorial_semiring_gcd"
+ assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime (f a) (f b)"
+ assumes "\<And>a. a \<in> A \<Longrightarrow> squarefree (f a)"
+ shows "squarefree (prod f A)"
+ using assms
+ by (induction A rule: infinite_finite_induct)
+ (auto intro!: squarefree_mult_coprime prod_coprime')
+
+lemma squarefree_powerD: "m > 0 \<Longrightarrow> squarefree (n ^ m) \<Longrightarrow> squarefree n"
+ by (cases m) (auto dest: squarefree_multD)
+
+lemma squarefree_power_iff:
+ "squarefree (n ^ m) \<longleftrightarrow> m = 0 \<or> is_unit n \<or> (squarefree n \<and> m = 1)"
+proof safe
+ assume "squarefree (n ^ m)" "m > 0" "\<not>is_unit n"
+ show "m = 1"
+ proof (rule ccontr)
+ assume "m \<noteq> 1"
+ with \<open>m > 0\<close> have "n ^ 2 dvd n ^ m" by (intro le_imp_power_dvd) auto
+ from this and \<open>\<not>is_unit n\<close> have "\<not>squarefree (n ^ m)" by (rule not_squarefreeI)
+ with \<open>squarefree (n ^ m)\<close> show False by contradiction
+ qed
+qed (auto simp: is_unit_power_iff dest: squarefree_powerD)
+
+definition squarefree_nat :: "nat \<Rightarrow> bool" where
+ [code_abbrev]: "squarefree_nat = squarefree"
+
+lemma squarefree_nat_code_naive [code]:
+ "squarefree_nat n \<longleftrightarrow> n \<noteq> 0 \<and> (\<forall>k\<in>{2..n}. \<not>k ^ 2 dvd n)"
+proof safe
+ assume *: "\<forall>k\<in>{2..n}. \<not> k\<^sup>2 dvd n" and n: "n > 0"
+ show "squarefree_nat n" unfolding squarefree_nat_def
+ proof (rule squarefreeI)
+ fix k assume k: "k ^ 2 dvd n"
+ have "k dvd n" by (rule dvd_trans[OF _ k]) auto
+ with n have "k \<le> n" by (intro dvd_imp_le)
+ with bspec[OF *, of k] k have "\<not>k > 1" by (intro notI) auto
+ moreover from k and n have "k \<noteq> 0" by (intro notI) auto
+ ultimately have "k = 1" by presburger
+ thus "is_unit k" by simp
+ qed
+qed (auto simp: squarefree_nat_def squarefree_def intro!: Nat.gr0I)
+
+
+
+definition square_part :: "'a :: factorial_semiring \<Rightarrow> 'a" where
+ "square_part n = (if n = 0 then 0 else
+ normalize (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n div 2)))"
+
+lemma square_part_nonzero:
+ "n \<noteq> 0 \<Longrightarrow> square_part n = normalize (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n div 2))"
+ by (simp add: square_part_def)
+
+lemma square_part_0 [simp]: "square_part 0 = 0"
+ by (simp add: square_part_def)
+
+lemma square_part_unit [simp]: "is_unit x \<Longrightarrow> square_part x = 1"
+ by (auto simp: square_part_def prime_factorization_unit)
+
+lemma square_part_1 [simp]: "square_part 1 = 1"
+ by simp
+
+lemma square_part_0_iff [simp]: "square_part n = 0 \<longleftrightarrow> n = 0"
+ by (simp add: square_part_def)
+
+lemma normalize_uminus [simp]:
+ "normalize (-x :: 'a :: {normalization_semidom, comm_ring_1}) = normalize x"
+ by (rule associatedI) auto
+
+lemma multiplicity_uminus_right [simp]:
+ "multiplicity (x :: 'a :: {factorial_semiring, comm_ring_1}) (-y) = multiplicity x y"
+proof -
+ have "multiplicity x (-y) = multiplicity x (normalize (-y))"
+ by (rule multiplicity_normalize_right [symmetric])
+ also have "\<dots> = multiplicity x y" by simp
+ finally show ?thesis .
+qed
+
+lemma multiplicity_uminus_left [simp]:
+ "multiplicity (-x :: 'a :: {factorial_semiring, comm_ring_1}) y = multiplicity x y"
+proof -
+ have "multiplicity (-x) y = multiplicity (normalize (-x)) y"
+ by (rule multiplicity_normalize_left [symmetric])
+ also have "\<dots> = multiplicity x y" by simp
+ finally show ?thesis .
+qed
+
+lemma prime_factorization_uminus [simp]:
+ "prime_factorization (-x :: 'a :: {factorial_semiring, comm_ring_1}) = prime_factorization x"
+ by (rule prime_factorization_cong) simp_all
+
+lemma square_part_uminus [simp]:
+ "square_part (-x :: 'a :: {factorial_semiring, comm_ring_1}) = square_part x"
+ by (simp add: square_part_def)
+
+lemma prime_multiplicity_square_part:
+ assumes "prime p"
+ shows "multiplicity p (square_part n) = multiplicity p n div 2"
+proof (cases "n = 0")
+ case False
+ thus ?thesis unfolding square_part_nonzero[OF False] multiplicity_normalize_right
+ using finite_prime_divisors[of n] assms
+ by (subst multiplicity_prod_prime_powers)
+ (auto simp: not_dvd_imp_multiplicity_0 prime_factors_dvd multiplicity_prod_prime_powers)
+qed auto
+
+lemma square_part_square_dvd [simp, intro]: "square_part n ^ 2 dvd n"
+proof (cases "n = 0")
+ case False
+ thus ?thesis
+ by (intro multiplicity_le_imp_dvd)
+ (auto simp: prime_multiplicity_square_part prime_elem_multiplicity_power_distrib)
+qed auto
+
+lemma prime_multiplicity_le_imp_dvd:
+ assumes "x \<noteq> 0" "y \<noteq> 0"
+ shows "x dvd y \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y)"
+ using assms by (auto intro: multiplicity_le_imp_dvd dvd_imp_multiplicity_le)
+
+lemma dvd_square_part_iff: "x dvd square_part n \<longleftrightarrow> x ^ 2 dvd n"
+proof (cases "x = 0"; cases "n = 0")
+ assume nz: "x \<noteq> 0" "n \<noteq> 0"
+ thus ?thesis
+ by (subst (1 2) prime_multiplicity_le_imp_dvd)
+ (auto simp: prime_multiplicity_square_part prime_elem_multiplicity_power_distrib)
+qed auto
+
+
+definition squarefree_part :: "'a :: factorial_semiring \<Rightarrow> 'a" where
+ "squarefree_part n = (if n = 0 then 1 else n div square_part n ^ 2)"
+
+lemma squarefree_part_0 [simp]: "squarefree_part 0 = 1"
+ by (simp add: squarefree_part_def)
+
+lemma squarefree_part_unit [simp]: "is_unit n \<Longrightarrow> squarefree_part n = n"
+ by (auto simp add: squarefree_part_def)
+
+lemma squarefree_part_1 [simp]: "squarefree_part 1 = 1"
+ by simp
+
+lemma squarefree_decompose: "n = squarefree_part n * square_part n ^ 2"
+ by (simp add: squarefree_part_def)
+
+lemma squarefree_part_uminus [simp]:
+ assumes "x \<noteq> 0"
+ shows "squarefree_part (-x :: 'a :: {factorial_semiring, comm_ring_1}) = -squarefree_part x"
+proof -
+ have "-(squarefree_part x * square_part x ^ 2) = -x"
+ by (subst squarefree_decompose [symmetric]) auto
+ also have "\<dots> = squarefree_part (-x) * square_part (-x) ^ 2" by (rule squarefree_decompose)
+ finally have "(- squarefree_part x) * square_part x ^ 2 =
+ squarefree_part (-x) * square_part x ^ 2" by simp
+ thus ?thesis using assms by (subst (asm) mult_right_cancel) auto
+qed
+
+lemma squarefree_part_nonzero [simp]: "squarefree_part n \<noteq> 0"
+ using squarefree_decompose[of n] by (cases "n \<noteq> 0") auto
+
+lemma prime_multiplicity_squarefree_part:
+ assumes "prime p"
+ shows "multiplicity p (squarefree_part n) = multiplicity p n mod 2"
+proof (cases "n = 0")
+ case False
+ hence n: "n \<noteq> 0" by auto
+ have "multiplicity p n mod 2 + 2 * (multiplicity p n div 2) = multiplicity p n" by simp
+ also have "\<dots> = multiplicity p (squarefree_part n * square_part n ^ 2)"
+ by (subst squarefree_decompose[of n]) simp
+ also from assms n have "\<dots> = multiplicity p (squarefree_part n) + 2 * (multiplicity p n div 2)"
+ by (subst prime_elem_multiplicity_mult_distrib)
+ (auto simp: prime_elem_multiplicity_power_distrib prime_multiplicity_square_part)
+ finally show ?thesis by (subst (asm) add_right_cancel) simp
+qed auto
+
+lemma prime_multiplicity_squarefree_part_le_Suc_0 [intro]:
+ assumes "prime p"
+ shows "multiplicity p (squarefree_part n) \<le> Suc 0"
+ by (simp add: assms prime_multiplicity_squarefree_part)
+
+lemma squarefree_squarefree_part [simp, intro]: "squarefree (squarefree_part n)"
+ by (subst squarefree_factorial_semiring'')
+ (auto simp: prime_multiplicity_squarefree_part_le_Suc_0)
+
+lemma squarefree_decomposition_unique:
+ assumes "square_part m = square_part n"
+ assumes "squarefree_part m = squarefree_part n"
+ shows "m = n"
+ by (subst (1 2) squarefree_decompose) (simp_all add: assms)
+
+lemma normalize_square_part [simp]: "normalize (square_part x) = square_part x"
+ by (simp add: square_part_def)
+
+lemma square_part_even_power': "square_part (x ^ (2 * n)) = normalize (x ^ n)"
+proof (cases "x = 0")
+ case False
+ have "normalize (square_part (x ^ (2 * n))) = normalize (x ^ n)" using False
+ by (intro multiplicity_eq_imp_eq)
+ (auto simp: prime_multiplicity_square_part prime_elem_multiplicity_power_distrib)
+ thus ?thesis by simp
+qed (auto simp: power_0_left)
+
+lemma square_part_even_power: "even n \<Longrightarrow> square_part (x ^ n) = normalize (x ^ (n div 2))"
+ by (subst square_part_even_power' [symmetric]) auto
+
+lemma square_part_odd_power': "square_part (x ^ (Suc (2 * n))) = normalize (x ^ n * square_part x)"
+proof (cases "x = 0")
+ case False
+ have "normalize (square_part (x ^ (Suc (2 * n)))) = normalize (square_part x * x ^ n)"
+ proof (rule multiplicity_eq_imp_eq, goal_cases)
+ case (3 p)
+ hence "multiplicity p (square_part (x ^ Suc (2 * n))) =
+ (2 * (n * multiplicity p x) + multiplicity p x) div 2"
+ by (subst prime_multiplicity_square_part)
+ (auto simp: False prime_elem_multiplicity_power_distrib algebra_simps simp del: power_Suc)
+ also from 3 False have "\<dots> = multiplicity p (square_part x * x ^ n)"
+ by (subst div_mult_self4) (auto simp: prime_multiplicity_square_part
+ prime_elem_multiplicity_mult_distrib prime_elem_multiplicity_power_distrib)
+ finally show ?case .
+ qed (insert False, auto)
+ thus ?thesis by (simp add: mult_ac)
+qed auto
+
+lemma square_part_odd_power:
+ "odd n \<Longrightarrow> square_part (x ^ n) = normalize (x ^ (n div 2) * square_part x)"
+ by (subst square_part_odd_power' [symmetric]) auto
+
+end
\ No newline at end of file
--- a/src/HOL/Library/Multiset.thy Wed Jul 12 18:42:32 2017 +0200
+++ b/src/HOL/Library/Multiset.thy Sat Jul 15 14:32:02 2017 +0100
@@ -1813,6 +1813,12 @@
lemma mset_zero_iff_right[simp]: "({#} = mset x) = (x = [])"
by (induct x) auto
+lemma count_mset_gt_0: "x \<in> set xs \<Longrightarrow> count (mset xs) x > 0"
+ by (induction xs) auto
+
+lemma count_mset_0_iff [simp]: "count (mset xs) x = 0 \<longleftrightarrow> x \<notin> set xs"
+ by (induction xs) auto
+
lemma mset_single_iff[iff]: "mset xs = {#x#} \<longleftrightarrow> xs = [x]"
by (cases xs) auto
@@ -1949,6 +1955,9 @@
defines mset_set = "folding.F add_mset {#}"
by standard (simp add: fun_eq_iff)
+lemma sum_multiset_singleton [simp]: "sum (\<lambda>n. {#n#}) A = mset_set A"
+ by (induction A rule: infinite_finite_induct) auto
+
lemma count_mset_set [simp]:
"finite A \<Longrightarrow> x \<in> A \<Longrightarrow> count (mset_set A) x = 1" (is "PROP ?P")
"\<not> finite A \<Longrightarrow> count (mset_set A) x = 0" (is "PROP ?Q")
@@ -2001,6 +2010,25 @@
lemma mset_set_set: "distinct xs \<Longrightarrow> mset_set (set xs) = mset xs"
by (induction xs) simp_all
+lemma count_mset_set': "count (mset_set A) x = (if finite A \<and> x \<in> A then 1 else 0)"
+ by auto
+
+lemma subset_imp_msubset_mset_set:
+ assumes "A \<subseteq> B" "finite B"
+ shows "mset_set A \<subseteq># mset_set B"
+proof (rule mset_subset_eqI)
+ fix x :: 'a
+ from assms have "finite A" by (rule finite_subset)
+ with assms show "count (mset_set A) x \<le> count (mset_set B) x"
+ by (cases "x \<in> A"; cases "x \<in> B") auto
+qed
+
+lemma mset_set_set_mset_msubset: "mset_set (set_mset A) \<subseteq># A"
+proof (rule mset_subset_eqI)
+ fix x show "count (mset_set (set_mset A)) x \<le> count A x"
+ by (cases "x \<in># A") simp_all
+qed
+
context linorder
begin
@@ -2071,6 +2099,23 @@
finally show ?case by simp
qed simp_all
+lemma msubset_mset_set_iff [simp]:
+ assumes "finite A" "finite B"
+ shows "mset_set A \<subseteq># mset_set B \<longleftrightarrow> A \<subseteq> B"
+ using subset_imp_msubset_mset_set[of A B]
+ set_mset_mono[of "mset_set A" "mset_set B"] assms by auto
+
+lemma mset_set_eq_iff [simp]:
+ assumes "finite A" "finite B"
+ shows "mset_set A = mset_set B \<longleftrightarrow> A = B"
+proof -
+ from assms have "mset_set A = mset_set B \<longleftrightarrow> set_mset (mset_set A) = set_mset (mset_set B)"
+ by (intro iffI equalityI set_mset_mono) auto
+ also from assms have "\<dots> \<longleftrightarrow> A = B" by simp
+ finally show ?thesis .
+qed
+
+
(* Contributed by Lukas Bulwahn *)
lemma image_mset_mset_set:
assumes "inj_on f A"
--- a/src/HOL/Number_Theory/Number_Theory.thy Wed Jul 12 18:42:32 2017 +0200
+++ b/src/HOL/Number_Theory/Number_Theory.thy Sat Jul 15 14:32:02 2017 +0100
@@ -2,7 +2,7 @@
section \<open>Comprehensive number theory\<close>
theory Number_Theory
-imports Fib Residues Eratosthenes Quadratic_Reciprocity Pocklington
+imports Fib Residues Eratosthenes Quadratic_Reciprocity Pocklington Prime_Powers
begin
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Number_Theory/Prime_Powers.thy Sat Jul 15 14:32:02 2017 +0100
@@ -0,0 +1,315 @@
+(*
+ File: HOL/Number_Theory/Prime_Powers.thy
+ Author: Manuel Eberl <eberlm@in.tum.de>
+
+ Prime powers and the Mangoldt function
+*)
+section \<open>Prime powers\<close>
+theory Prime_Powers
+ imports Complex_Main "~~/src/HOL/Computational_Algebra/Primes"
+begin
+
+definition aprimedivisor :: "'a :: normalization_semidom \<Rightarrow> 'a" where
+ "aprimedivisor q = (SOME p. prime p \<and> p dvd q)"
+
+definition primepow :: "'a :: normalization_semidom \<Rightarrow> bool" where
+ "primepow n \<longleftrightarrow> (\<exists>p k. prime p \<and> k > 0 \<and> n = p ^ k)"
+
+definition primepow_factors :: "'a :: normalization_semidom \<Rightarrow> 'a set" where
+ "primepow_factors n = {x. primepow x \<and> x dvd n}"
+
+lemma primepow_gt_Suc_0: "primepow n \<Longrightarrow> n > Suc 0"
+ using one_less_power[of "p::nat" for p] by (auto simp: primepow_def prime_nat_iff)
+
+lemma
+ assumes "prime p" "p dvd n"
+ shows prime_aprimedivisor: "prime (aprimedivisor n)"
+ and aprimedivisor_dvd: "aprimedivisor n dvd n"
+proof -
+ from assms have "\<exists>p. prime p \<and> p dvd n" by auto
+ from someI_ex[OF this] show "prime (aprimedivisor n)" "aprimedivisor n dvd n"
+ unfolding aprimedivisor_def by (simp_all add: conj_commute)
+qed
+
+lemma
+ assumes "n \<noteq> 0" "\<not>is_unit (n :: 'a :: factorial_semiring)"
+ shows prime_aprimedivisor': "prime (aprimedivisor n)"
+ and aprimedivisor_dvd': "aprimedivisor n dvd n"
+proof -
+ from someI_ex[OF prime_divisor_exists[OF assms]]
+ show "prime (aprimedivisor n)" "aprimedivisor n dvd n"
+ unfolding aprimedivisor_def by (simp_all add: conj_commute)
+qed
+
+lemma aprimedivisor_of_prime [simp]:
+ assumes "prime p"
+ shows "aprimedivisor p = p"
+proof -
+ from assms have "\<exists>q. prime q \<and> q dvd p" by auto
+ from someI_ex[OF this, folded aprimedivisor_def] assms show ?thesis
+ by (auto intro: primes_dvd_imp_eq)
+qed
+
+lemma aprimedivisor_pos_nat: "(n::nat) > 1 \<Longrightarrow> aprimedivisor n > 0"
+ using aprimedivisor_dvd'[of n] by (auto elim: dvdE intro!: Nat.gr0I)
+
+lemma aprimedivisor_primepow_power:
+ assumes "primepow n" "k > 0"
+ shows "aprimedivisor (n ^ k) = aprimedivisor n"
+proof -
+ from assms obtain p l where l: "prime p" "l > 0" "n = p ^ l"
+ by (auto simp: primepow_def)
+ from l assms have *: "prime (aprimedivisor (n ^ k))" "aprimedivisor (n ^ k) dvd n ^ k"
+ by (intro prime_aprimedivisor[of p] aprimedivisor_dvd[of p] dvd_power;
+ simp add: power_mult [symmetric])+
+ from * l have "aprimedivisor (n ^ k) dvd p ^ (l * k)" by (simp add: power_mult)
+ with assms * l have "aprimedivisor (n ^ k) dvd p"
+ by (subst (asm) prime_dvd_power_iff) simp_all
+ with l assms have "aprimedivisor (n ^ k) = p"
+ by (intro primes_dvd_imp_eq prime_aprimedivisor l) (auto simp: power_mult [symmetric])
+ moreover from l have "aprimedivisor n dvd p ^ l"
+ by (auto intro: aprimedivisor_dvd simp: prime_gt_0_nat)
+ with assms l have "aprimedivisor n dvd p"
+ by (subst (asm) prime_dvd_power_iff) (auto intro!: prime_aprimedivisor simp: prime_gt_0_nat)
+ with l assms have "aprimedivisor n = p"
+ by (intro primes_dvd_imp_eq prime_aprimedivisor l) auto
+ ultimately show ?thesis by simp
+qed
+
+lemma aprimedivisor_prime_power:
+ assumes "prime p" "k > 0"
+ shows "aprimedivisor (p ^ k) = p"
+proof -
+ from assms have *: "prime (aprimedivisor (p ^ k))" "aprimedivisor (p ^ k) dvd p ^ k"
+ by (intro prime_aprimedivisor[of p] aprimedivisor_dvd[of p]; simp add: prime_nat_iff)+
+ from assms * have "aprimedivisor (p ^ k) dvd p"
+ by (subst (asm) prime_dvd_power_iff) simp_all
+ with assms * show "aprimedivisor (p ^ k) = p" by (intro primes_dvd_imp_eq)
+qed
+
+lemma prime_factorization_primepow:
+ assumes "primepow n"
+ shows "prime_factorization n =
+ replicate_mset (multiplicity (aprimedivisor n) n) (aprimedivisor n)"
+ using assms
+ by (auto simp: primepow_def aprimedivisor_prime_power prime_factorization_prime_power)
+
+lemma primepow_decompose:
+ assumes "primepow n"
+ shows "aprimedivisor n ^ multiplicity (aprimedivisor n) n = n"
+proof -
+ from assms have "n \<noteq> 0" by (intro notI) (auto simp: primepow_def)
+ hence "n = unit_factor n * prod_mset (prime_factorization n)"
+ by (subst prod_mset_prime_factorization) simp_all
+ also from assms have "unit_factor n = 1" by (auto simp: primepow_def unit_factor_power)
+ also have "prime_factorization n =
+ replicate_mset (multiplicity (aprimedivisor n) n) (aprimedivisor n)"
+ by (intro prime_factorization_primepow assms)
+ also have "prod_mset \<dots> = aprimedivisor n ^ multiplicity (aprimedivisor n) n" by simp
+ finally show ?thesis by simp
+qed
+
+lemma prime_power_not_one:
+ assumes "prime p" "k > 0"
+ shows "p ^ k \<noteq> 1"
+proof
+ assume "p ^ k = 1"
+ hence "is_unit (p ^ k)" by simp
+ thus False using assms by (simp add: is_unit_power_iff)
+qed
+
+lemma zero_not_primepow [simp]: "\<not>primepow 0"
+ by (auto simp: primepow_def)
+
+lemma one_not_primepow [simp]: "\<not>primepow 1"
+ by (auto simp: primepow_def prime_power_not_one)
+
+lemma primepow_not_unit [simp]: "primepow p \<Longrightarrow> \<not>is_unit p"
+ by (auto simp: primepow_def is_unit_power_iff)
+
+lemma unit_factor_primepow: "primepow p \<Longrightarrow> unit_factor p = 1"
+ by (auto simp: primepow_def unit_factor_power)
+
+lemma aprimedivisor_primepow:
+ assumes "prime p" "p dvd n" "primepow (n :: 'a :: factorial_semiring)"
+ shows "aprimedivisor (p * n) = p" "aprimedivisor n = p"
+proof -
+ from assms have [simp]: "n \<noteq> 0" by auto
+ define q where "q = aprimedivisor n"
+ with assms have q: "prime q" by (auto simp: q_def intro!: prime_aprimedivisor)
+ from \<open>primepow n\<close> have n: "n = q ^ multiplicity q n"
+ by (simp add: primepow_decompose q_def)
+ have nz: "multiplicity q n \<noteq> 0"
+ proof
+ assume "multiplicity q n = 0"
+ with n have n': "n = unit_factor n" by simp
+ have "is_unit n" by (subst n', rule unit_factor_is_unit) (insert assms, auto)
+ with assms show False by auto
+ qed
+ with \<open>prime p\<close> \<open>p dvd n\<close> q have "p dvd q"
+ by (subst (asm) n) (auto intro: prime_dvd_power)
+ with \<open>prime p\<close> q have "p = q" by (intro primes_dvd_imp_eq)
+ thus "aprimedivisor n = p" by (simp add: q_def)
+
+ define r where "r = aprimedivisor (p * n)"
+ with assms have r: "r dvd (p * n)" "prime r" unfolding r_def
+ by (intro aprimedivisor_dvd[of p] prime_aprimedivisor[of p]; simp)+
+ hence "r dvd q ^ Suc (multiplicity q n)"
+ by (subst (asm) n) (auto simp: \<open>p = q\<close> dest: dvd_unit_imp_unit)
+ with r have "r dvd q"
+ by (auto intro: prime_dvd_power_nat simp: prime_dvd_mult_iff dest: prime_dvd_power)
+ with r q have "r = q" by (intro primes_dvd_imp_eq)
+ thus "aprimedivisor (p * n) = p" by (simp add: r_def \<open>p = q\<close>)
+qed
+
+lemma power_eq_prime_powerD:
+ fixes p :: "'a :: factorial_semiring"
+ assumes "prime p" "n > 0" "x ^ n = p ^ k"
+ shows "\<exists>i. normalize x = normalize (p ^ i)"
+proof -
+ have "normalize x = normalize (p ^ multiplicity p x)"
+ proof (rule multiplicity_eq_imp_eq)
+ fix q :: 'a assume "prime q"
+ from assms have "multiplicity q (x ^ n) = multiplicity q (p ^ k)" by simp
+ with \<open>prime q\<close> and assms have "n * multiplicity q x = k * multiplicity q p"
+ by (subst (asm) (1 2) prime_elem_multiplicity_power_distrib) (auto simp: power_0_left)
+ with assms and \<open>prime q\<close> show "multiplicity q x = multiplicity q (p ^ multiplicity p x)"
+ by (cases "p = q") (auto simp: multiplicity_distinct_prime_power prime_multiplicity_other)
+ qed (insert assms, auto simp: power_0_left)
+ thus ?thesis by auto
+qed
+
+
+lemma primepow_power_iff:
+ assumes "unit_factor p = 1"
+ shows "primepow (p ^ n) \<longleftrightarrow> primepow (p :: 'a :: factorial_semiring) \<and> n > 0"
+proof safe
+ assume "primepow (p ^ n)"
+ hence n: "n \<noteq> 0" by (auto intro!: Nat.gr0I)
+ thus "n > 0" by simp
+ from assms have [simp]: "normalize p = p"
+ using normalize_mult_unit_factor[of p] by (simp only: mult.right_neutral)
+ from \<open>primepow (p ^ n)\<close> obtain q k where *: "k > 0" "prime q" "p ^ n = q ^ k"
+ by (auto simp: primepow_def)
+ with power_eq_prime_powerD[of q n p k] n
+ obtain i where eq: "normalize p = normalize (q ^ i)" by auto
+ with primepow_not_unit[OF \<open>primepow (p ^ n)\<close>] have "i \<noteq> 0"
+ by (intro notI) (simp add: normalize_1_iff is_unit_power_iff del: primepow_not_unit)
+ with \<open>normalize p = normalize (q ^ i)\<close> \<open>prime q\<close> show "primepow p"
+ by (auto simp: normalize_power primepow_def intro!: exI[of _ q] exI[of _ i])
+next
+ assume "primepow p" "n > 0"
+ then obtain q k where *: "k > 0" "prime q" "p = q ^ k" by (auto simp: primepow_def)
+ with \<open>n > 0\<close> show "primepow (p ^ n)"
+ by (auto simp: primepow_def power_mult intro!: exI[of _ q] exI[of _ "k * n"])
+qed
+
+lemma primepow_prime [simp]: "prime n \<Longrightarrow> primepow n"
+ by (auto simp: primepow_def intro!: exI[of _ n] exI[of _ "1::nat"])
+
+lemma primepow_prime_power [simp]:
+ "prime (p :: 'a :: factorial_semiring) \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> n > 0"
+ by (subst primepow_power_iff) auto
+
+(* TODO Generalise *)
+lemma primepow_multD:
+ assumes "primepow (a * b :: nat)"
+ shows "a = 1 \<or> primepow a" "b = 1 \<or> primepow b"
+proof -
+ from assms obtain p k where k: "k > 0" "a * b = p ^ k" "prime p"
+ unfolding primepow_def by auto
+ then obtain i j where "a = p ^ i" "b = p ^ j"
+ using prime_power_mult_nat[of p a b] by blast
+ with \<open>prime p\<close> show "a = 1 \<or> primepow a" "b = 1 \<or> primepow b" by auto
+qed
+
+lemma primepow_mult_aprimedivisorI:
+ assumes "primepow (n :: 'a :: factorial_semiring)"
+ shows "primepow (aprimedivisor n * n)"
+ by (subst (2) primepow_decompose[OF assms, symmetric], subst power_Suc [symmetric],
+ subst primepow_prime_power)
+ (insert assms, auto intro!: prime_aprimedivisor' dest: primepow_gt_Suc_0)
+
+lemma aprimedivisor_vimage:
+ assumes "prime (p :: 'a :: factorial_semiring)"
+ shows "aprimedivisor -` {p} \<inter> primepow_factors n = {p ^ k |k. k > 0 \<and> p ^ k dvd n}"
+proof safe
+ fix q assume q: "q \<in> primepow_factors n"
+ hence q': "q \<noteq> 0" "q \<noteq> 1" by (auto simp: primepow_def primepow_factors_def prime_power_not_one)
+ let ?n = "multiplicity (aprimedivisor q) q"
+ from q q' have "q = aprimedivisor q ^ ?n \<and> ?n > 0 \<and> aprimedivisor q ^ ?n dvd n"
+ using prime_aprimedivisor'[of q] aprimedivisor_dvd'[of q]
+ by (subst primepow_decompose [symmetric])
+ (auto simp: primepow_factors_def multiplicity_gt_zero_iff unit_factor_primepow
+ intro: dvd_trans[OF multiplicity_dvd])
+ thus "\<exists>k. q = aprimedivisor q ^ k \<and> k > 0 \<and> aprimedivisor q ^ k dvd n" ..
+next
+ fix k :: nat assume k: "p ^ k dvd n" "k > 0"
+ with assms show "p ^ k \<in> aprimedivisor -` {p}"
+ by (auto simp: aprimedivisor_prime_power)
+ with assms k show "p ^ k \<in> primepow_factors n"
+ by (auto simp: primepow_factors_def primepow_def aprimedivisor_prime_power intro: Suc_leI)
+qed
+
+lemma primepow_factors_altdef:
+ fixes x :: "'a :: factorial_semiring"
+ assumes "x \<noteq> 0"
+ shows "primepow_factors x = {p ^ k |p k. p \<in> prime_factors x \<and> k \<in> {0<.. multiplicity p x}}"
+proof (intro equalityI subsetI)
+ fix q assume "q \<in> primepow_factors x"
+ then obtain p k where pk: "prime p" "k > 0" "q = p ^ k" "q dvd x"
+ unfolding primepow_factors_def primepow_def by blast
+ moreover have "k \<le> multiplicity p x" using pk assms by (intro multiplicity_geI) auto
+ ultimately show "q \<in> {p ^ k |p k. p \<in> prime_factors x \<and> k \<in> {0<.. multiplicity p x}}"
+ by (auto simp: prime_factors_multiplicity intro!: exI[of _ p] exI[of _ k])
+qed (auto simp: primepow_factors_def prime_factors_multiplicity multiplicity_dvd')
+
+lemma finite_primepow_factors:
+ assumes "x \<noteq> (0 :: 'a :: factorial_semiring)"
+ shows "finite (primepow_factors x)"
+proof -
+ have "finite (SIGMA p:prime_factors x. {0<..multiplicity p x})"
+ by (intro finite_SigmaI) simp_all
+ hence "finite ((\<lambda>(p,k). p ^ k) ` \<dots>)" (is "finite ?A") by (rule finite_imageI)
+ also have "?A = primepow_factors x"
+ using assms by (subst primepow_factors_altdef) fast+
+ finally show ?thesis .
+qed
+
+
+definition mangoldt :: "nat \<Rightarrow> 'a :: real_algebra_1" where
+ "mangoldt n = (if primepow n then of_real (ln (real (aprimedivisor n))) else 0)"
+
+lemma of_real_mangoldt [simp]: "of_real (mangoldt n) = mangoldt n"
+ by (simp add: mangoldt_def)
+
+lemma mangoldt_sum:
+ assumes "n \<noteq> 0"
+ shows "(\<Sum>d | d dvd n. mangoldt d :: 'a :: real_algebra_1) = of_real (ln (real n))"
+proof -
+ have "(\<Sum>d | d dvd n. mangoldt d :: 'a) = of_real (\<Sum>d | d dvd n. mangoldt d)" by simp
+ also have "(\<Sum>d | d dvd n. mangoldt d) = (\<Sum>d \<in> primepow_factors n. ln (real (aprimedivisor d)))"
+ using assms by (intro sum.mono_neutral_cong_right) (auto simp: primepow_factors_def mangoldt_def)
+ also have "\<dots> = ln (real (\<Prod>d \<in> primepow_factors n. aprimedivisor d))"
+ using assms finite_primepow_factors[of n]
+ by (subst ln_prod [symmetric])
+ (auto simp: primepow_factors_def intro!: aprimedivisor_pos_nat
+ intro: Nat.gr0I primepow_gt_Suc_0)
+ also have "primepow_factors n =
+ (\<lambda>(p,k). p ^ k) ` (SIGMA p:prime_factors n. {0<..multiplicity p n})"
+ (is "_ = _ ` ?A") by (subst primepow_factors_altdef[OF assms]) fast+
+ also have "prod aprimedivisor \<dots> = (\<Prod>(p,k)\<in>?A. aprimedivisor (p ^ k))"
+ by (subst prod.reindex)
+ (auto simp: inj_on_def prime_power_inj'' prime_factors_multiplicity
+ prod.Sigma [symmetric] case_prod_unfold)
+ also have "\<dots> = (\<Prod>(p,k)\<in>?A. p)"
+ by (intro prod.cong refl) (auto simp: aprimedivisor_prime_power prime_factors_multiplicity)
+ also have "\<dots> = (\<Prod>x\<in>prime_factors n. \<Prod>k\<in>{0<..multiplicity x n}. x)"
+ by (rule prod.Sigma [symmetric]) auto
+ also have "\<dots> = (\<Prod>x\<in>prime_factors n. x ^ multiplicity x n)"
+ by (intro prod.cong refl) (simp add: prod_constant)
+ also have "\<dots> = n" using assms by (intro prime_factorization_nat [symmetric]) simp
+ finally show ?thesis .
+qed
+
+end
\ No newline at end of file