# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1500125522 -3600
# Node ID acc3b7dd0b215e0566b54f5cb7f38de0ad615068
# Parent  2c1d223c5417a8eb506d9bf79b789d1a770773d1
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory

diff -r 2c1d223c5417 -r acc3b7dd0b21 src/HOL/Computational_Algebra/Computational_Algebra.thy
--- 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
diff -r 2c1d223c5417 -r acc3b7dd0b21 src/HOL/Computational_Algebra/Factorial_Ring.thy
--- 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)+
diff -r 2c1d223c5417 -r acc3b7dd0b21 src/HOL/Computational_Algebra/Nth_Powers.thy
--- /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
diff -r 2c1d223c5417 -r acc3b7dd0b21 src/HOL/Computational_Algebra/Squarefree.thy
--- /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
diff -r 2c1d223c5417 -r acc3b7dd0b21 src/HOL/Library/Multiset.thy
--- 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"
diff -r 2c1d223c5417 -r acc3b7dd0b21 src/HOL/Number_Theory/Number_Theory.thy
--- 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
diff -r 2c1d223c5417 -r acc3b7dd0b21 src/HOL/Number_Theory/Prime_Powers.thy
--- /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