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.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.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.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.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