src/HOL/Number_Theory/Primes.thy
changeset 63830 2ea3725a34bd
parent 63766 695d60817cb1
child 63904 b8482e12a2a8
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Fri Sep 09 14:15:16 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Fri Sep 09 15:12:40 2016 +0200
     1.3 @@ -470,19 +470,19 @@
     1.4    unfolding prime_factors_def 
     1.5    by (auto split: if_splits simp: prime_def dest!: in_prime_factorization_imp_prime)
     1.6  
     1.7 -lemma msetprod_prime_factorization_int:
     1.8 +lemma prod_mset_prime_factorization_int:
     1.9    fixes n :: int
    1.10    assumes "n > 0"
    1.11 -  shows   "msetprod (prime_factorization n) = n"
    1.12 -  using assms by (simp add: msetprod_prime_factorization)
    1.13 +  shows   "prod_mset (prime_factorization n) = n"
    1.14 +  using assms by (simp add: prod_mset_prime_factorization)
    1.15  
    1.16  lemma prime_factorization_exists_nat:
    1.17    "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
    1.18    using prime_factorization_exists[of n] by (auto simp: prime_def)
    1.19  
    1.20 -lemma msetprod_prime_factorization_nat [simp]: 
    1.21 -  "(n::nat) > 0 \<Longrightarrow> msetprod (prime_factorization n) = n"
    1.22 -  by (subst msetprod_prime_factorization) simp_all
    1.23 +lemma prod_mset_prime_factorization_nat [simp]: 
    1.24 +  "(n::nat) > 0 \<Longrightarrow> prod_mset (prime_factorization n) = n"
    1.25 +  by (subst prod_mset_prime_factorization) simp_all
    1.26  
    1.27  lemma prime_factorization_nat:
    1.28      "n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
    1.29 @@ -587,13 +587,13 @@
    1.30      by (intro setprod.cong) (auto simp: g_def)
    1.31    also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
    1.32      by (intro setprod.mono_neutral_right) (auto simp: g_def set_mset_A)
    1.33 -  also have "\<dots> = msetprod A"
    1.34 -    by (auto simp: msetprod_multiplicity count_A set_mset_A intro!: setprod.cong)
    1.35 -  also from assms have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
    1.36 -    by (subst prime_elem_multiplicity_msetprod_distrib) (auto dest: prime)
    1.37 +  also have "\<dots> = prod_mset A"
    1.38 +    by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: setprod.cong)
    1.39 +  also from assms have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
    1.40 +    by (subst prime_elem_multiplicity_prod_mset_distrib) (auto dest: prime)
    1.41    also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
    1.42      by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
    1.43 -  also have "msetsum \<dots> = (if p \<in> S then f p else 0)" by (simp add: msetsum_delta count_A g_def)
    1.44 +  also have "sum_mset \<dots> = (if p \<in> S then f p else 0)" by (simp add: sum_mset_delta count_A g_def)
    1.45    finally show ?thesis .
    1.46  qed
    1.47