# HG changeset patch # User eberlm # 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 \Irreducible and prime elements\ +(* TODO: Move ? *) +lemma (in semiring_gcd) prod_coprime' [rule_format]: + "(\i\A. gcd a (f i) = 1) \ gcd a (\i\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 \ p dvd prod_mset A \ (\x. x \# A \ 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 \ prime p \ p dvd prod f A \ (\x\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 \ p ^ n = 1 \ n = 0" + using prime_power_inj[of p n 0] by auto + +lemma one_eq_prime_power_iff [simp]: "prime p \ 1 = p ^ n \ 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 \ (m = 0 \ n = 0) \ (p = q \ 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" "\x. x \ A \ f x \ 0" + shows "prime_factorization (prod f A) = (\n\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 \ 0" "y \ 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 "\P p. P \ A \ p \ P \ prime p" + assumes "\P. P \ A \ finite P" + shows "inj_on Prod A" +proof (rule inj_onI) + fix P Q assume PQ: "P \ A" "Q \ A" "\P = \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 \GCD and LCM computation with unique factorizations\ @@ -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 \ 0 \ b \ 0 \ prime_factors (gcd a b) = + prime_factors a \ prime_factors b" + by (subst prime_factorization_gcd) auto + +lemma prime_factors_lcm [simp]: + "a \ 0 \ b \ 0 \ prime_factors (lcm a b) = + prime_factors a \ 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 + + n-th powers in general and n-th roots of natural numbers +*) +section \$n$-th powers and roots of naturals\ +theory Nth_Powers + imports Primes +begin + +subsection \The set of $n$-th powers\ + +definition is_nth_power :: "nat \ 'a :: monoid_mult \ bool" where + "is_nth_power n x \ (\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 \ is_nth_power n x" + by (auto simp: is_nth_power_def) + +lemma is_nth_powerE: "is_nth_power n x \ (\y. x = y ^ n \ P) \ P" + by (auto simp: is_nth_power_def) + + +abbreviation is_square where "is_square \ is_nth_power 2" + +lemma is_zeroth_power [simp]: "is_nth_power 0 x \ 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 \ 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) \ 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) \ (\p. prime p \ 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 \ 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 *: "\p. prime p \ n dvd multiplicity p x" + have "multiplicity p ((\p\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 \ prime_factors x" + using that and \prime p\ 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 ((\p\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 (\p\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) \ (\p. prime p \ 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 \ 0" "b \ 0" "n > 0" + for a b :: nat unfolding is_nth_power_conv_multiplicity_nat[OF \n > 0\] + proof safe + fix p :: nat assume p: "prime p" + from \coprime a b\ have "\(p dvd a \ 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) \ is_nth_power n a \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) \ 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 ^ \ = (m ^ (n' div n)) ^ n" by (simp add: power_mult) + also have "is_nth_power n \" by simp + finally show ?thesis . +qed + +definition is_nth_power_nat :: "nat \ nat \ 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 (\k\{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 \The $n$-root of a natural number\ + +definition nth_root_nat :: "nat \ nat \ nat" where + "nth_root_nat k n = (if k = 0 then 0 else Max {m. m ^ k \ 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 \ n} \ {..n}" +proof safe + fix m assume "m ^ k \ n" + show "m \ n" + proof (cases "m = 0") + case False + with assms have "m ^ 1 \ m ^ k" by (intro power_increasing) simp_all + also note \m ^ k \ n\ + finally show ?thesis by simp + qed simp_all +qed + +lemma nth_root_nat_aux2: + assumes "k > 0" + shows "finite {m::nat. m ^ k \ n}" "{m::nat. m ^ k \ n} \ {}" +proof - + from assms have "{m. m ^ k \ n} \ {..n}" by (rule nth_root_nat_aux1) + moreover have "finite {..n}" by simp + ultimately show "finite {m::nat. m ^ k \ n}" by (rule finite_subset) +next + from assms show "{m::nat. m ^ k \ n} \ {}" 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 \ n" + and nth_root_nat_ge: "x ^ k \ n \ x \ 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 \k > 0\ have "nth_root_nat k n ^ k \ 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 \ n" "(m + 1) ^ k > n" + shows "nth_root_nat k n = m" +proof (cases "k > 0") + case True + from nth_root_nat_less[OF \k > 0\ assms(2)] + have "nth_root_nat k n \ m" by simp + moreover from \k > 0\ and assms(1) have "nth_root_nat k n \ 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 \ 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 \ 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 (\m. m ^ k \ n) {..n}))" +proof (cases "k > 0") + case True + hence "{m. m ^ k \ n} \ {..n}" by (rule nth_root_nat_aux1) + hence "Set.filter (\m. m ^ k \ n) {..n} = {m. m ^ k \ 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 \ nat \ nat \ nat \ nat" where + "nth_root_nat_aux m k acc n = + (let acc' = (k + 1) ^ m + in if k \ n \ acc' > n then k else nth_root_nat_aux m (k+1) acc' n)" + by auto +termination by (relation "measure (\(_,k,_,n). n - k)", goal_cases) auto + +lemma nth_root_nat_aux_le: + assumes "k ^ m \ n" "m > 0" + shows "nth_root_nat_aux m k (k ^ m) n ^ m \ 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 \ k" + proof - + note that + also have "k < Suc k ^ 1" by simp + also from \m > 0\ have "\ \ 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 \ 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 \ n = 0 then 0 else if m = 1 \ 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 \ 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 ^ \ = (n ^ (m div k)) ^ k" by (simp add: power_mult) + also from assms have "nth_root_nat k \ = n ^ (m div k)" by simp + finally show ?thesis . +qed + +lemma nth_root_nat_mono: + assumes "m \ n" + shows "nth_root_nat k m \ 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 + + Squarefreeness and decomposition of ring elements into square part and squarefree part +*) +section \Squarefreeness\ +theory Squarefree +imports Primes +begin + +(* TODO: Generalise to n-th powers *) + +definition squarefree :: "'a :: comm_monoid_mult \ bool" where + "squarefree n \ (\x. x ^ 2 dvd n \ x dvd 1)" + +lemma squarefreeI: "(\x. x ^ 2 dvd n \ x dvd 1) \ squarefree n" + by (auto simp: squarefree_def) + +lemma squarefreeD: "squarefree n \ x ^ 2 dvd n \ x dvd 1" + by (auto simp: squarefree_def) + +lemma not_squarefreeI: "x ^ 2 dvd n \ \x dvd 1 \ \squarefree n" + by (auto simp: squarefree_def) + +lemma not_squarefreeE [case_names square_dvd]: + "\squarefree n \ (\x. x ^ 2 dvd n \ \x dvd 1 \ P) \ P" + by (auto simp: squarefree_def) + +lemma not_squarefree_0 [simp]: "\squarefree (0 :: 'a :: comm_semiring_1)" + by (rule not_squarefreeI[of 0]) auto + +lemma squarefree_factorial_semiring: + assumes "n \ 0" + shows "squarefree (n :: 'a :: factorial_semiring) \ (\p. prime p \ \p ^ 2 dvd n)" + unfolding squarefree_def +proof safe + assume *: "\p. prime p \ \p ^ 2 dvd n" + fix x :: 'a assume x: "x ^ 2 dvd n" + { + assume "\is_unit x" + moreover from assms and x have "x \ 0" by auto + ultimately obtain p where "p dvd x" "prime p" + using prime_divisor_exists by blast + with * have "\p ^ 2 dvd n" by blast + moreover from \p dvd x\ have "p ^ 2 dvd x ^ 2" by (rule dvd_power_same) + ultimately have "\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 \ 0" + shows "squarefree (n :: 'a :: factorial_semiring) \ + (\p\prime_factors n. multiplicity p n = 1)" +proof (subst squarefree_factorial_semiring [OF assms], safe) + fix p assume "\p\#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 \ 0" + shows "squarefree (n :: 'a :: factorial_semiring) \ + (\p. prime p \ multiplicity p n \ 1)" + by (subst squarefree_factorial_semiring'[OF assms]) (auto simp: prime_factors_multiplicity) + +lemma squarefree_unit [simp]: "is_unit n \ 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) \ squarefree n" + by (simp add: squarefree_def) + +lemma squarefree_mono: "a dvd b \ squarefree b \ 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 \ 0" by auto + show ?thesis + proof (subst squarefree_factorial_semiring [OF \p \ 0\]; safe) + fix q assume *: "prime q" "q^2 dvd p" + with assms have "multiplicity q p \ 2" by (intro multiplicity_geI) auto + thus False using assms \prime q\ 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 \ 0" by auto + show ?thesis unfolding squarefree_factorial_semiring'[OF nz] + proof + fix p assume p: "p \ prime_factors (a * b)" + { + assume "p dvd a \ 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 "\(p dvd a \ p dvd b)" by blast + moreover from p have "p dvd a \ 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 \ 'b :: factorial_semiring_gcd" + assumes "\a b. a \ A \ b \ A \ a \ b \ coprime (f a) (f b)" + assumes "\a. a \ A \ 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 \ squarefree (n ^ m) \ squarefree n" + by (cases m) (auto dest: squarefree_multD) + +lemma squarefree_power_iff: + "squarefree (n ^ m) \ m = 0 \ is_unit n \ (squarefree n \ m = 1)" +proof safe + assume "squarefree (n ^ m)" "m > 0" "\is_unit n" + show "m = 1" + proof (rule ccontr) + assume "m \ 1" + with \m > 0\ have "n ^ 2 dvd n ^ m" by (intro le_imp_power_dvd) auto + from this and \\is_unit n\ have "\squarefree (n ^ m)" by (rule not_squarefreeI) + with \squarefree (n ^ m)\ show False by contradiction + qed +qed (auto simp: is_unit_power_iff dest: squarefree_powerD) + +definition squarefree_nat :: "nat \ bool" where + [code_abbrev]: "squarefree_nat = squarefree" + +lemma squarefree_nat_code_naive [code]: + "squarefree_nat n \ n \ 0 \ (\k\{2..n}. \k ^ 2 dvd n)" +proof safe + assume *: "\k\{2..n}. \ 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 \ n" by (intro dvd_imp_le) + with bspec[OF *, of k] k have "\k > 1" by (intro notI) auto + moreover from k and n have "k \ 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 \ 'a" where + "square_part n = (if n = 0 then 0 else + normalize (\p\prime_factors n. p ^ (multiplicity p n div 2)))" + +lemma square_part_nonzero: + "n \ 0 \ square_part n = normalize (\p\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 \ 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 \ 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 "\ = 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 "\ = 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 \ 0" "y \ 0" + shows "x dvd y \ (\p. prime p \ multiplicity p x \ 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 \ x ^ 2 dvd n" +proof (cases "x = 0"; cases "n = 0") + assume nz: "x \ 0" "n \ 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 \ '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 \ 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 \ 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 "\ = 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 \ 0" + using squarefree_decompose[of n] by (cases "n \ 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 \ 0" by auto + have "multiplicity p n mod 2 + 2 * (multiplicity p n div 2) = multiplicity p n" by simp + also have "\ = multiplicity p (squarefree_part n * square_part n ^ 2)" + by (subst squarefree_decompose[of n]) simp + also from assms n have "\ = 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) \ 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 \ 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 "\ = 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 \ 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 \ set xs \ count (mset xs) x > 0" + by (induction xs) auto + +lemma count_mset_0_iff [simp]: "count (mset xs) x = 0 \ x \ set xs" + by (induction xs) auto + lemma mset_single_iff[iff]: "mset xs = {#x#} \ 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 (\n. {#n#}) A = mset_set A" + by (induction A rule: infinite_finite_induct) auto + lemma count_mset_set [simp]: "finite A \ x \ A \ count (mset_set A) x = 1" (is "PROP ?P") "\ finite A \ count (mset_set A) x = 0" (is "PROP ?Q") @@ -2001,6 +2010,25 @@ lemma mset_set_set: "distinct xs \ mset_set (set xs) = mset xs" by (induction xs) simp_all +lemma count_mset_set': "count (mset_set A) x = (if finite A \ x \ A then 1 else 0)" + by auto + +lemma subset_imp_msubset_mset_set: + assumes "A \ B" "finite B" + shows "mset_set A \# 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 \ count (mset_set B) x" + by (cases "x \ A"; cases "x \ B") auto +qed + +lemma mset_set_set_mset_msubset: "mset_set (set_mset A) \# A" +proof (rule mset_subset_eqI) + fix x show "count (mset_set (set_mset A)) x \ count A x" + by (cases "x \# 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 \# mset_set B \ A \ 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 \ A = B" +proof - + from assms have "mset_set A = mset_set B \ set_mset (mset_set A) = set_mset (mset_set B)" + by (intro iffI equalityI set_mset_mono) auto + also from assms have "\ \ 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 \Comprehensive number theory\ 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 + + Prime powers and the Mangoldt function +*) +section \Prime powers\ +theory Prime_Powers + imports Complex_Main "~~/src/HOL/Computational_Algebra/Primes" +begin + +definition aprimedivisor :: "'a :: normalization_semidom \ 'a" where + "aprimedivisor q = (SOME p. prime p \ p dvd q)" + +definition primepow :: "'a :: normalization_semidom \ bool" where + "primepow n \ (\p k. prime p \ k > 0 \ n = p ^ k)" + +definition primepow_factors :: "'a :: normalization_semidom \ 'a set" where + "primepow_factors n = {x. primepow x \ x dvd n}" + +lemma primepow_gt_Suc_0: "primepow n \ 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 "\p. prime p \ 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 \ 0" "\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 "\q. prime q \ 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 \ 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 \ 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 \ = 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 \ 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]: "\primepow 0" + by (auto simp: primepow_def) + +lemma one_not_primepow [simp]: "\primepow 1" + by (auto simp: primepow_def prime_power_not_one) + +lemma primepow_not_unit [simp]: "primepow p \ \is_unit p" + by (auto simp: primepow_def is_unit_power_iff) + +lemma unit_factor_primepow: "primepow p \ 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 \ 0" by auto + define q where "q = aprimedivisor n" + with assms have q: "prime q" by (auto simp: q_def intro!: prime_aprimedivisor) + from \primepow n\ have n: "n = q ^ multiplicity q n" + by (simp add: primepow_decompose q_def) + have nz: "multiplicity q n \ 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 \prime p\ \p dvd n\ q have "p dvd q" + by (subst (asm) n) (auto intro: prime_dvd_power) + with \prime p\ 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: \p = q\ 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 \p = q\) +qed + +lemma power_eq_prime_powerD: + fixes p :: "'a :: factorial_semiring" + assumes "prime p" "n > 0" "x ^ n = p ^ k" + shows "\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 \prime q\ 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 \prime q\ 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) \ primepow (p :: 'a :: factorial_semiring) \ n > 0" +proof safe + assume "primepow (p ^ n)" + hence n: "n \ 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 \primepow (p ^ n)\ 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 \primepow (p ^ n)\] have "i \ 0" + by (intro notI) (simp add: normalize_1_iff is_unit_power_iff del: primepow_not_unit) + with \normalize p = normalize (q ^ i)\ \prime q\ 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 \n > 0\ 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 \ 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) \ primepow (p ^ n) \ n > 0" + by (subst primepow_power_iff) auto + +(* TODO Generalise *) +lemma primepow_multD: + assumes "primepow (a * b :: nat)" + shows "a = 1 \ primepow a" "b = 1 \ 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 \prime p\ show "a = 1 \ primepow a" "b = 1 \ 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} \ primepow_factors n = {p ^ k |k. k > 0 \ p ^ k dvd n}" +proof safe + fix q assume q: "q \ primepow_factors n" + hence q': "q \ 0" "q \ 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 \ ?n > 0 \ 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 "\k. q = aprimedivisor q ^ k \ k > 0 \ aprimedivisor q ^ k dvd n" .. +next + fix k :: nat assume k: "p ^ k dvd n" "k > 0" + with assms show "p ^ k \ aprimedivisor -` {p}" + by (auto simp: aprimedivisor_prime_power) + with assms k show "p ^ k \ 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 \ 0" + shows "primepow_factors x = {p ^ k |p k. p \ prime_factors x \ k \ {0<.. multiplicity p x}}" +proof (intro equalityI subsetI) + fix q assume "q \ 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 \ multiplicity p x" using pk assms by (intro multiplicity_geI) auto + ultimately show "q \ {p ^ k |p k. p \ prime_factors x \ k \ {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 \ (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 ((\(p,k). p ^ k) ` \)" (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 \ '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 \ 0" + shows "(\d | d dvd n. mangoldt d :: 'a :: real_algebra_1) = of_real (ln (real n))" +proof - + have "(\d | d dvd n. mangoldt d :: 'a) = of_real (\d | d dvd n. mangoldt d)" by simp + also have "(\d | d dvd n. mangoldt d) = (\d \ 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 "\ = ln (real (\d \ 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 = + (\(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 \ = (\(p,k)\?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 "\ = (\(p,k)\?A. p)" + by (intro prod.cong refl) (auto simp: aprimedivisor_prime_power prime_factors_multiplicity) + also have "\ = (\x\prime_factors n. \k\{0<..multiplicity x n}. x)" + by (rule prod.Sigma [symmetric]) auto + also have "\ = (\x\prime_factors n. x ^ multiplicity x n)" + by (intro prod.cong refl) (simp add: prod_constant) + also have "\ = n" using assms by (intro prime_factorization_nat [symmetric]) simp + finally show ?thesis . +qed + +end \ No newline at end of file