msetsum -> set_mset, msetprod -> prod_mset
authornipkow
Fri Sep 09 15:12:40 2016 +0200 (2016-09-09)
changeset 638302ea3725a34bd
parent 63829 6a05c8cbf7de
child 63831 ea7471c921f5
msetsum -> set_mset, msetprod -> prod_mset
NEWS
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Polynomial_Factorial.thy
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Proofs/Extraction/Euclid.thy
     1.1 --- a/NEWS	Fri Sep 09 14:15:16 2016 +0200
     1.2 +++ b/NEWS	Fri Sep 09 15:12:40 2016 +0200
     1.3 @@ -603,6 +603,10 @@
     1.4  of the procedure on natural numbers.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Renamed sums and products of multisets:
     1.8 +  msetsum ~> sum_mset
     1.9 +  msetprod ~> prod_mset
    1.10 +
    1.11  * The lemma one_step_implies_mult_aux on multisets has been removed, use
    1.12  one_step_implies_mult instead.
    1.13  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Library/DAList_Multiset.thy	Fri Sep 09 14:15:16 2016 +0200
     2.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Fri Sep 09 15:12:40 2016 +0200
     2.3 @@ -32,9 +32,9 @@
     2.4  
     2.5  lemma [code, code del]: "size = (size :: _ multiset \<Rightarrow> nat)" ..
     2.6  
     2.7 -lemma [code, code del]: "msetsum = msetsum" ..
     2.8 +lemma [code, code del]: "sum_mset = sum_mset" ..
     2.9  
    2.10 -lemma [code, code del]: "msetprod = msetprod" ..
    2.11 +lemma [code, code del]: "prod_mset = prod_mset" ..
    2.12  
    2.13  lemma [code, code del]: "set_mset = set_mset" ..
    2.14  
    2.15 @@ -403,8 +403,8 @@
    2.16  
    2.17  (* we cannot use (\<lambda>a n. op + (a * n)) for folding, since * is not defined
    2.18     in comm_monoid_add *)
    2.19 -lemma msetsum_Bag[code]: "msetsum (Bag ms) = DAList_Multiset.fold (\<lambda>a n. ((op + a) ^^ n)) 0 ms"
    2.20 -  unfolding msetsum.eq_fold
    2.21 +lemma sum_mset_Bag[code]: "sum_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. ((op + a) ^^ n)) 0 ms"
    2.22 +  unfolding sum_mset.eq_fold
    2.23    apply (rule comp_fun_commute.DAList_Multiset_fold)
    2.24    apply unfold_locales
    2.25    apply (auto simp: ac_simps)
    2.26 @@ -412,8 +412,8 @@
    2.27  
    2.28  (* we cannot use (\<lambda>a n. op * (a ^ n)) for folding, since ^ is not defined
    2.29     in comm_monoid_mult *)
    2.30 -lemma msetprod_Bag[code]: "msetprod (Bag ms) = DAList_Multiset.fold (\<lambda>a n. ((op * a) ^^ n)) 1 ms"
    2.31 -  unfolding msetprod.eq_fold
    2.32 +lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. ((op * a) ^^ n)) 1 ms"
    2.33 +  unfolding prod_mset.eq_fold
    2.34    apply (rule comp_fun_commute.DAList_Multiset_fold)
    2.35    apply unfold_locales
    2.36    apply (auto simp: ac_simps)
     3.1 --- a/src/HOL/Library/Multiset.thy	Fri Sep 09 14:15:16 2016 +0200
     3.2 +++ b/src/HOL/Library/Multiset.thy	Fri Sep 09 15:12:40 2016 +0200
     3.3 @@ -2044,31 +2044,31 @@
     3.4  context comm_monoid_add
     3.5  begin
     3.6  
     3.7 -sublocale msetsum: comm_monoid_mset plus 0
     3.8 -  defines msetsum = msetsum.F ..
     3.9 -
    3.10 -lemma (in semiring_1) msetsum_replicate_mset [simp]:
    3.11 -  "msetsum (replicate_mset n a) = of_nat n * a"
    3.12 +sublocale sum_mset: comm_monoid_mset plus 0
    3.13 +  defines sum_mset = sum_mset.F ..
    3.14 +
    3.15 +lemma (in semiring_1) sum_mset_replicate_mset [simp]:
    3.16 +  "sum_mset (replicate_mset n a) = of_nat n * a"
    3.17    by (induct n) (simp_all add: algebra_simps)
    3.18  
    3.19 -lemma setsum_unfold_msetsum:
    3.20 -  "setsum f A = msetsum (image_mset f (mset_set A))"
    3.21 +lemma setsum_unfold_sum_mset:
    3.22 +  "setsum f A = sum_mset (image_mset f (mset_set A))"
    3.23    by (cases "finite A") (induct A rule: finite_induct, simp_all)
    3.24  
    3.25 -lemma msetsum_delta: "msetsum (image_mset (\<lambda>x. if x = y then c else 0) A) = c * count A y"
    3.26 +lemma sum_mset_delta: "sum_mset (image_mset (\<lambda>x. if x = y then c else 0) A) = c * count A y"
    3.27    by (induction A) simp_all
    3.28  
    3.29 -lemma msetsum_delta': "msetsum (image_mset (\<lambda>x. if y = x then c else 0) A) = c * count A y"
    3.30 +lemma sum_mset_delta': "sum_mset (image_mset (\<lambda>x. if y = x then c else 0) A) = c * count A y"
    3.31    by (induction A) simp_all
    3.32  
    3.33  end
    3.34  
    3.35 -lemma msetsum_diff:
    3.36 +lemma sum_mset_diff:
    3.37    fixes M N :: "('a :: ordered_cancel_comm_monoid_diff) multiset"
    3.38 -  shows "N \<subseteq># M \<Longrightarrow> msetsum (M - N) = msetsum M - msetsum N"
    3.39 -  by (metis add_diff_cancel_right' msetsum.union subset_mset.diff_add)
    3.40 -
    3.41 -lemma size_eq_msetsum: "size M = msetsum (image_mset (\<lambda>_. 1) M)"
    3.42 +  shows "N \<subseteq># M \<Longrightarrow> sum_mset (M - N) = sum_mset M - sum_mset N"
    3.43 +  by (metis add_diff_cancel_right' sum_mset.union subset_mset.diff_add)
    3.44 +
    3.45 +lemma size_eq_sum_mset: "size M = sum_mset (image_mset (\<lambda>_. 1) M)"
    3.46  proof (induct M)
    3.47    case empty then show ?case by simp
    3.48  next
    3.49 @@ -2079,17 +2079,17 @@
    3.50  qed
    3.51  
    3.52  lemma size_mset_set [simp]: "size (mset_set A) = card A"
    3.53 -  by (simp only: size_eq_msetsum card_eq_setsum setsum_unfold_msetsum)
    3.54 +  by (simp only: size_eq_sum_mset card_eq_setsum setsum_unfold_sum_mset)
    3.55  
    3.56  syntax (ASCII)
    3.57 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3SUM _:#_. _)" [0, 51, 10] 10)
    3.58 +  "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3SUM _:#_. _)" [0, 51, 10] 10)
    3.59  syntax
    3.60 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
    3.61 +  "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
    3.62  translations
    3.63 -  "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
    3.64 +  "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST sum_mset (CONST image_mset (\<lambda>i. b) A)"
    3.65  
    3.66  abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
    3.67 -  where "\<Union># MM \<equiv> msetsum MM" \<comment> \<open>FIXME ambiguous notation --
    3.68 +  where "\<Union># MM \<equiv> sum_mset MM" \<comment> \<open>FIXME ambiguous notation --
    3.69      could likewise refer to \<open>\<Squnion>#\<close>\<close>
    3.70  
    3.71  lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
    3.72 @@ -2113,78 +2113,78 @@
    3.73  context comm_monoid_mult
    3.74  begin
    3.75  
    3.76 -sublocale msetprod: comm_monoid_mset times 1
    3.77 -  defines msetprod = msetprod.F ..
    3.78 -
    3.79 -lemma msetprod_empty:
    3.80 -  "msetprod {#} = 1"
    3.81 -  by (fact msetprod.empty)
    3.82 -
    3.83 -lemma msetprod_singleton:
    3.84 -  "msetprod {#x#} = x"
    3.85 -  by (fact msetprod.singleton)
    3.86 -
    3.87 -lemma msetprod_Un:
    3.88 -  "msetprod (A + B) = msetprod A * msetprod B"
    3.89 -  by (fact msetprod.union)
    3.90 -
    3.91 -lemma msetprod_replicate_mset [simp]:
    3.92 -  "msetprod (replicate_mset n a) = a ^ n"
    3.93 +sublocale prod_mset: comm_monoid_mset times 1
    3.94 +  defines prod_mset = prod_mset.F ..
    3.95 +
    3.96 +lemma prod_mset_empty:
    3.97 +  "prod_mset {#} = 1"
    3.98 +  by (fact prod_mset.empty)
    3.99 +
   3.100 +lemma prod_mset_singleton:
   3.101 +  "prod_mset {#x#} = x"
   3.102 +  by (fact prod_mset.singleton)
   3.103 +
   3.104 +lemma prod_mset_Un:
   3.105 +  "prod_mset (A + B) = prod_mset A * prod_mset B"
   3.106 +  by (fact prod_mset.union)
   3.107 +
   3.108 +lemma prod_mset_replicate_mset [simp]:
   3.109 +  "prod_mset (replicate_mset n a) = a ^ n"
   3.110    by (induct n) simp_all
   3.111  
   3.112 -lemma setprod_unfold_msetprod:
   3.113 -  "setprod f A = msetprod (image_mset f (mset_set A))"
   3.114 +lemma setprod_unfold_prod_mset:
   3.115 +  "setprod f A = prod_mset (image_mset f (mset_set A))"
   3.116    by (cases "finite A") (induct A rule: finite_induct, simp_all)
   3.117  
   3.118 -lemma msetprod_multiplicity:
   3.119 -  "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_mset M)"
   3.120 -  by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
   3.121 -
   3.122 -lemma msetprod_delta: "msetprod (image_mset (\<lambda>x. if x = y then c else 1) A) = c ^ count A y"
   3.123 +lemma prod_mset_multiplicity:
   3.124 +  "prod_mset M = setprod (\<lambda>x. x ^ count M x) (set_mset M)"
   3.125 +  by (simp add: fold_mset_def setprod.eq_fold prod_mset.eq_fold funpow_times_power comp_def)
   3.126 +
   3.127 +lemma prod_mset_delta: "prod_mset (image_mset (\<lambda>x. if x = y then c else 1) A) = c ^ count A y"
   3.128    by (induction A) simp_all
   3.129  
   3.130 -lemma msetprod_delta': "msetprod (image_mset (\<lambda>x. if y = x then c else 1) A) = c ^ count A y"
   3.131 +lemma prod_mset_delta': "prod_mset (image_mset (\<lambda>x. if y = x then c else 1) A) = c ^ count A y"
   3.132    by (induction A) simp_all
   3.133  
   3.134  end
   3.135  
   3.136  syntax (ASCII)
   3.137 -  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3PROD _:#_. _)" [0, 51, 10] 10)
   3.138 +  "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3PROD _:#_. _)" [0, 51, 10] 10)
   3.139  syntax
   3.140 -  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
   3.141 +  "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
   3.142  translations
   3.143 -  "\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST msetprod (CONST image_mset (\<lambda>i. b) A)"
   3.144 -
   3.145 -lemma (in comm_semiring_1) dvd_msetprod:
   3.146 +  "\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST prod_mset (CONST image_mset (\<lambda>i. b) A)"
   3.147 +
   3.148 +lemma (in comm_semiring_1) dvd_prod_mset:
   3.149    assumes "x \<in># A"
   3.150 -  shows "x dvd msetprod A"
   3.151 +  shows "x dvd prod_mset A"
   3.152  proof -
   3.153    from assms have "A = add_mset x (A - {#x#})" by simp
   3.154    then obtain B where "A = add_mset x B" ..
   3.155    then show ?thesis by simp
   3.156  qed
   3.157  
   3.158 -lemma (in semidom) msetprod_zero_iff [iff]:
   3.159 -  "msetprod A = 0 \<longleftrightarrow> 0 \<in># A"
   3.160 +lemma (in semidom) prod_mset_zero_iff [iff]:
   3.161 +  "prod_mset A = 0 \<longleftrightarrow> 0 \<in># A"
   3.162    by (induct A) auto
   3.163  
   3.164 -lemma (in semidom_divide) msetprod_diff:
   3.165 +lemma (in semidom_divide) prod_mset_diff:
   3.166    assumes "B \<subseteq># A" and "0 \<notin># B"
   3.167 -  shows "msetprod (A - B) = msetprod A div msetprod B"
   3.168 +  shows "prod_mset (A - B) = prod_mset A div prod_mset B"
   3.169  proof -
   3.170    from assms obtain C where "A = B + C"
   3.171      by (metis subset_mset.add_diff_inverse)
   3.172    with assms show ?thesis by simp
   3.173  qed
   3.174  
   3.175 -lemma (in semidom_divide) msetprod_minus:
   3.176 +lemma (in semidom_divide) prod_mset_minus:
   3.177    assumes "a \<in># A" and "a \<noteq> 0"
   3.178 -  shows "msetprod (A - {#a#}) = msetprod A div a"
   3.179 -  using assms msetprod_diff [of "{#a#}" A] by auto
   3.180 -
   3.181 -lemma (in normalization_semidom) normalized_msetprodI:
   3.182 +  shows "prod_mset (A - {#a#}) = prod_mset A div a"
   3.183 +  using assms prod_mset_diff [of "{#a#}" A] by auto
   3.184 +
   3.185 +lemma (in normalization_semidom) normalized_prod_msetI:
   3.186    assumes "\<And>a. a \<in># A \<Longrightarrow> normalize a = a"
   3.187 -  shows "normalize (msetprod A) = msetprod A"
   3.188 +  shows "normalize (prod_mset A) = prod_mset A"
   3.189    using assms by (induct A) (simp_all add: normalize_mult)
   3.190  
   3.191  
   3.192 @@ -3167,12 +3167,12 @@
   3.193  
   3.194  end
   3.195  
   3.196 -lemma [code]: "msetsum (mset xs) = listsum xs"
   3.197 +lemma [code]: "sum_mset (mset xs) = listsum xs"
   3.198    by (induct xs) simp_all
   3.199  
   3.200 -lemma [code]: "msetprod (mset xs) = fold times xs 1"
   3.201 +lemma [code]: "prod_mset (mset xs) = fold times xs 1"
   3.202  proof -
   3.203 -  have "\<And>x. fold times xs x = msetprod (mset xs) * x"
   3.204 +  have "\<And>x. fold times xs x = prod_mset (mset xs) * x"
   3.205      by (induct xs) (simp_all add: ac_simps)
   3.206    then show ?thesis by simp
   3.207  qed
   3.208 @@ -3537,10 +3537,11 @@
   3.209  
   3.210  subsection \<open>Size setup\<close>
   3.211  
   3.212 -lemma multiset_size_o_map: "size_multiset g \<circ> image_mset f = size_multiset (g \<circ> f)"
   3.213 -  apply (rule ext)
   3.214 -  subgoal for x by (induct x) auto
   3.215 -  done
   3.216 +lemma multiset_size_o_map:
   3.217 +  "size_multiset g \<circ> image_mset f = size_multiset (g \<circ> f)"
   3.218 +apply (rule ext)
   3.219 +subgoal for x by (induct x) auto
   3.220 +done
   3.221  
   3.222  setup \<open>
   3.223    BNF_LFP_Size.register_size_global @{type_name multiset} @{const_name size_multiset}
     4.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Fri Sep 09 14:15:16 2016 +0200
     4.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Fri Sep 09 15:12:40 2016 +0200
     4.3 @@ -16,11 +16,11 @@
     4.4  
     4.5  subsection \<open>Prelude\<close>
     4.6  
     4.7 -lemma msetprod_mult: 
     4.8 -  "msetprod (image_mset (\<lambda>x. f x * g x) A) = msetprod (image_mset f A) * msetprod (image_mset g A)"
     4.9 +lemma prod_mset_mult: 
    4.10 +  "prod_mset (image_mset (\<lambda>x. f x * g x) A) = prod_mset (image_mset f A) * prod_mset (image_mset g A)"
    4.11    by (induction A) (simp_all add: mult_ac)
    4.12    
    4.13 -lemma msetprod_const: "msetprod (image_mset (\<lambda>_. c) A) = c ^ size A"
    4.14 +lemma prod_mset_const: "prod_mset (image_mset (\<lambda>_. c) A) = c ^ size A"
    4.15    by (induction A) (simp_all add: mult_ac)
    4.16    
    4.17  lemma dvd_field_iff: "x dvd y \<longleftrightarrow> (x = 0 \<longrightarrow> y = (0::'a::field))"
    4.18 @@ -341,7 +341,7 @@
    4.19  
    4.20  subsection \<open>Various facts about polynomials\<close>
    4.21  
    4.22 -lemma msetprod_const_poly: "msetprod (image_mset (\<lambda>x. [:f x:]) A) = [:msetprod (image_mset f A):]"
    4.23 +lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
    4.24    by (induction A) (simp_all add: one_poly_def mult_ac)
    4.25  
    4.26  lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
    4.27 @@ -679,8 +679,8 @@
    4.28  lemma fract_poly_dvd: "p dvd q \<Longrightarrow> fract_poly p dvd fract_poly q"
    4.29    by (auto elim!: dvdE)
    4.30  
    4.31 -lemma msetprod_fract_poly: 
    4.32 -  "msetprod (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (msetprod (image_mset f A))"
    4.33 +lemma prod_mset_fract_poly: 
    4.34 +  "prod_mset (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (prod_mset (image_mset f A))"
    4.35    by (induction A) (simp_all add: mult_ac)
    4.36    
    4.37  lemma is_unit_fract_poly_iff:
    4.38 @@ -961,9 +961,9 @@
    4.39    shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q"
    4.40    by (auto elim!: dvdE simp: primitive_part_mult)
    4.41  
    4.42 -lemma content_msetprod: 
    4.43 +lemma content_prod_mset: 
    4.44    fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
    4.45 -  shows "content (msetprod A) = msetprod (image_mset content A)"
    4.46 +  shows "content (prod_mset A) = prod_mset (image_mset content A)"
    4.47    by (induction A) (simp_all add: content_mult mult_ac)
    4.48  
    4.49  lemma fract_poly_dvdD:
    4.50 @@ -1046,14 +1046,14 @@
    4.51        comm_semiring_1.irreducible_def[OF A] comm_semiring_1.prime_elem_def[OF A] by blast
    4.52  qed
    4.53  
    4.54 -lemma field_poly_msetprod_prime_factorization:
    4.55 +lemma field_poly_prod_mset_prime_factorization:
    4.56    assumes "(x :: 'a :: field poly) \<noteq> 0"
    4.57 -  shows   "msetprod (field_poly.prime_factorization x) = normalize_field_poly x"
    4.58 +  shows   "prod_mset (field_poly.prime_factorization x) = normalize_field_poly x"
    4.59  proof -
    4.60    have A: "class.comm_monoid_mult op * (1 :: 'a poly)" ..
    4.61 -  have "comm_monoid_mult.msetprod op * (1 :: 'a poly) = msetprod"
    4.62 -    by (intro ext) (simp add: comm_monoid_mult.msetprod_def[OF A] msetprod_def)
    4.63 -  with field_poly.msetprod_prime_factorization[OF assms] show ?thesis by simp
    4.64 +  have "comm_monoid_mult.prod_mset op * (1 :: 'a poly) = prod_mset"
    4.65 +    by (intro ext) (simp add: comm_monoid_mult.prod_mset_def[OF A] prod_mset_def)
    4.66 +  with field_poly.prod_mset_prime_factorization[OF assms] show ?thesis by simp
    4.67  qed
    4.68  
    4.69  lemma field_poly_in_prime_factorization_imp_prime:
    4.70 @@ -1248,32 +1248,32 @@
    4.71  private lemma poly_prime_factorization_exists_content_1:
    4.72    fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
    4.73    assumes "p \<noteq> 0" "content p = 1"
    4.74 -  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize p"
    4.75 +  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"
    4.76  proof -
    4.77    let ?P = "field_poly.prime_factorization (fract_poly p)"
    4.78 -  define c where "c = msetprod (image_mset fract_content ?P)"
    4.79 +  define c where "c = prod_mset (image_mset fract_content ?P)"
    4.80    define c' where "c' = c * to_fract (lead_coeff p)"
    4.81 -  define e where "e = msetprod (image_mset primitive_part_fract ?P)"
    4.82 +  define e where "e = prod_mset (image_mset primitive_part_fract ?P)"
    4.83    define A where "A = image_mset (normalize \<circ> primitive_part_fract) ?P"
    4.84    have "content e = (\<Prod>x\<in>#field_poly.prime_factorization (map_poly to_fract p). 
    4.85                        content (primitive_part_fract x))"
    4.86 -    by (simp add: e_def content_msetprod multiset.map_comp o_def)
    4.87 +    by (simp add: e_def content_prod_mset multiset.map_comp o_def)
    4.88    also have "image_mset (\<lambda>x. content (primitive_part_fract x)) ?P = image_mset (\<lambda>_. 1) ?P"
    4.89      by (intro image_mset_cong content_primitive_part_fract) auto
    4.90 -  finally have content_e: "content e = 1" by (simp add: msetprod_const)    
    4.91 +  finally have content_e: "content e = 1" by (simp add: prod_mset_const)    
    4.92    
    4.93    have "fract_poly p = unit_factor_field_poly (fract_poly p) * 
    4.94            normalize_field_poly (fract_poly p)" by simp
    4.95    also have "unit_factor_field_poly (fract_poly p) = [:to_fract (lead_coeff p):]" 
    4.96      by (simp add: unit_factor_field_poly_def lead_coeff_def monom_0 degree_map_poly coeff_map_poly)
    4.97 -  also from assms have "normalize_field_poly (fract_poly p) = msetprod ?P" 
    4.98 -    by (subst field_poly_msetprod_prime_factorization) simp_all
    4.99 -  also have "\<dots> = msetprod (image_mset id ?P)" by simp
   4.100 +  also from assms have "normalize_field_poly (fract_poly p) = prod_mset ?P" 
   4.101 +    by (subst field_poly_prod_mset_prime_factorization) simp_all
   4.102 +  also have "\<dots> = prod_mset (image_mset id ?P)" by simp
   4.103    also have "image_mset id ?P = 
   4.104                 image_mset (\<lambda>x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P"
   4.105      by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract)
   4.106 -  also have "msetprod \<dots> = smult c (fract_poly e)"
   4.107 -    by (subst msetprod_mult) (simp_all add: msetprod_fract_poly msetprod_const_poly c_def e_def)
   4.108 +  also have "prod_mset \<dots> = smult c (fract_poly e)"
   4.109 +    by (subst prod_mset_mult) (simp_all add: prod_mset_fract_poly prod_mset_const_poly c_def e_def)
   4.110    also have "[:to_fract (lead_coeff p):] * \<dots> = smult c' (fract_poly e)"
   4.111      by (simp add: c'_def)
   4.112    finally have eq: "fract_poly p = smult c' (fract_poly e)" .
   4.113 @@ -1291,28 +1291,28 @@
   4.114    hence "p = [:b:] * e" by simp
   4.115    with b have "normalize p = normalize e" 
   4.116      by (simp only: normalize_mult) (simp add: is_unit_normalize is_unit_poly_iff)
   4.117 -  also have "normalize e = msetprod A"
   4.118 -    by (simp add: multiset.map_comp e_def A_def normalize_msetprod)
   4.119 -  finally have "msetprod A = normalize p" ..
   4.120 +  also have "normalize e = prod_mset A"
   4.121 +    by (simp add: multiset.map_comp e_def A_def normalize_prod_mset)
   4.122 +  finally have "prod_mset A = normalize p" ..
   4.123    
   4.124    have "prime_elem p" if "p \<in># A" for p
   4.125      using that by (auto simp: A_def prime_elem_primitive_part_fract prime_elem_imp_irreducible 
   4.126                          dest!: field_poly_in_prime_factorization_imp_prime )
   4.127 -  from this and \<open>msetprod A = normalize p\<close> show ?thesis
   4.128 +  from this and \<open>prod_mset A = normalize p\<close> show ?thesis
   4.129      by (intro exI[of _ A]) blast
   4.130  qed
   4.131  
   4.132  lemma poly_prime_factorization_exists:
   4.133    fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
   4.134    assumes "p \<noteq> 0"
   4.135 -  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize p"
   4.136 +  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"
   4.137  proof -
   4.138    define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
   4.139 -  have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize (primitive_part p)"
   4.140 +  have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize (primitive_part p)"
   4.141      by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
   4.142    then guess A by (elim exE conjE) note A = this
   4.143 -  moreover from assms have "msetprod B = [:content p:]"
   4.144 -    by (simp add: B_def msetprod_const_poly msetprod_prime_factorization)
   4.145 +  moreover from assms have "prod_mset B = [:content p:]"
   4.146 +    by (simp add: B_def prod_mset_const_poly prod_mset_prime_factorization)
   4.147    moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p"
   4.148      by (auto simp: B_def intro: lift_prime_elem_poly dest: in_prime_factorization_imp_prime)
   4.149    ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
     5.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Fri Sep 09 14:15:16 2016 +0200
     5.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Fri Sep 09 15:12:40 2016 +0200
     5.3 @@ -201,9 +201,9 @@
     5.4      by (auto simp add: mult_unit_dvd_iff)
     5.5  qed
     5.6  
     5.7 -lemma prime_elem_dvd_msetprodE:
     5.8 +lemma prime_elem_dvd_prod_msetE:
     5.9    assumes "prime_elem p"
    5.10 -  assumes dvd: "p dvd msetprod A"
    5.11 +  assumes dvd: "p dvd prod_mset A"
    5.12    obtains a where "a \<in># A" and "p dvd a"
    5.13  proof -
    5.14    from dvd have "\<exists>a. a \<in># A \<and> p dvd a"
    5.15 @@ -212,8 +212,8 @@
    5.16      using \<open>prime_elem p\<close> by (simp add: prime_elem_not_unit)
    5.17    next
    5.18      case (add a A)
    5.19 -    then have "p dvd a * msetprod A" by simp
    5.20 -    with \<open>prime_elem p\<close> consider (A) "p dvd msetprod A" | (B) "p dvd a"
    5.21 +    then have "p dvd a * prod_mset A" by simp
    5.22 +    with \<open>prime_elem p\<close> consider (A) "p dvd prod_mset A" | (B) "p dvd a"
    5.23        by (blast dest: prime_elem_dvd_multD)
    5.24      then show ?case proof cases
    5.25        case B then show ?thesis by auto
    5.26 @@ -444,17 +444,17 @@
    5.27    "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
    5.28    by (subst prime_elem_dvd_power_iff) simp_all
    5.29  
    5.30 -lemma msetprod_subset_imp_dvd:
    5.31 +lemma prod_mset_subset_imp_dvd:
    5.32    assumes "A \<subseteq># B"
    5.33 -  shows   "msetprod A dvd msetprod B"
    5.34 +  shows   "prod_mset A dvd prod_mset B"
    5.35  proof -
    5.36    from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
    5.37 -  also have "msetprod \<dots> = msetprod (B - A) * msetprod A" by simp
    5.38 -  also have "msetprod A dvd \<dots>" by simp
    5.39 +  also have "prod_mset \<dots> = prod_mset (B - A) * prod_mset A" by simp
    5.40 +  also have "prod_mset A dvd \<dots>" by simp
    5.41    finally show ?thesis .
    5.42  qed
    5.43  
    5.44 -lemma prime_dvd_msetprod_iff: "prime p \<Longrightarrow> p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
    5.45 +lemma prime_dvd_prod_mset_iff: "prime p \<Longrightarrow> p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
    5.46    by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+)
    5.47  
    5.48  lemma primes_dvd_imp_eq:
    5.49 @@ -467,17 +467,17 @@
    5.50    with assms show "p = q" by simp
    5.51  qed
    5.52  
    5.53 -lemma prime_dvd_msetprod_primes_iff:
    5.54 +lemma prime_dvd_prod_mset_primes_iff:
    5.55    assumes "prime p" "\<And>q. q \<in># A \<Longrightarrow> prime q"
    5.56 -  shows   "p dvd msetprod A \<longleftrightarrow> p \<in># A"
    5.57 +  shows   "p dvd prod_mset A \<longleftrightarrow> p \<in># A"
    5.58  proof -
    5.59 -  from assms(1) have "p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" by (rule prime_dvd_msetprod_iff)
    5.60 +  from assms(1) have "p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" by (rule prime_dvd_prod_mset_iff)
    5.61    also from assms have "\<dots> \<longleftrightarrow> p \<in># A" by (auto dest: primes_dvd_imp_eq)
    5.62    finally show ?thesis .
    5.63  qed
    5.64  
    5.65 -lemma msetprod_primes_dvd_imp_subset:
    5.66 -  assumes "msetprod A dvd msetprod B" "\<And>p. p \<in># A \<Longrightarrow> prime p" "\<And>p. p \<in># B \<Longrightarrow> prime p"
    5.67 +lemma prod_mset_primes_dvd_imp_subset:
    5.68 +  assumes "prod_mset A dvd prod_mset B" "\<And>p. p \<in># A \<Longrightarrow> prime p" "\<And>p. p \<in># B \<Longrightarrow> prime p"
    5.69    shows   "A \<subseteq># B"
    5.70  using assms
    5.71  proof (induction A arbitrary: B)
    5.72 @@ -487,16 +487,16 @@
    5.73    case (add p A B)
    5.74    hence p: "prime p" by simp
    5.75    define B' where "B' = B - {#p#}"
    5.76 -  from add.prems have "p dvd msetprod B" by (simp add: dvd_mult_left)
    5.77 +  from add.prems have "p dvd prod_mset B" by (simp add: dvd_mult_left)
    5.78    with add.prems have "p \<in># B"
    5.79 -    by (subst (asm) (2) prime_dvd_msetprod_primes_iff) simp_all
    5.80 +    by (subst (asm) (2) prime_dvd_prod_mset_primes_iff) simp_all
    5.81    hence B: "B = B' + {#p#}" by (simp add: B'_def)
    5.82    from add.prems p have "A \<subseteq># B'" by (intro add.IH) (simp_all add: B)
    5.83    thus ?case by (simp add: B)
    5.84  qed
    5.85  
    5.86 -lemma normalize_msetprod_primes:
    5.87 -  "(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (msetprod A) = msetprod A"
    5.88 +lemma normalize_prod_mset_primes:
    5.89 +  "(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (prod_mset A) = prod_mset A"
    5.90  proof (induction A)
    5.91    case (add p A)
    5.92    hence "prime p" by simp
    5.93 @@ -504,56 +504,56 @@
    5.94    with add show ?case by (simp add: normalize_mult)
    5.95  qed simp_all
    5.96  
    5.97 -lemma msetprod_dvd_msetprod_primes_iff:
    5.98 +lemma prod_mset_dvd_prod_mset_primes_iff:
    5.99    assumes "\<And>x. x \<in># A \<Longrightarrow> prime x" "\<And>x. x \<in># B \<Longrightarrow> prime x"
   5.100 -  shows   "msetprod A dvd msetprod B \<longleftrightarrow> A \<subseteq># B"
   5.101 -  using assms by (auto intro: msetprod_subset_imp_dvd msetprod_primes_dvd_imp_subset)
   5.102 +  shows   "prod_mset A dvd prod_mset B \<longleftrightarrow> A \<subseteq># B"
   5.103 +  using assms by (auto intro: prod_mset_subset_imp_dvd prod_mset_primes_dvd_imp_subset)
   5.104  
   5.105 -lemma is_unit_msetprod_iff:
   5.106 -  "is_unit (msetprod A) \<longleftrightarrow> (\<forall>x. x \<in># A \<longrightarrow> is_unit x)"
   5.107 +lemma is_unit_prod_mset_iff:
   5.108 +  "is_unit (prod_mset A) \<longleftrightarrow> (\<forall>x. x \<in># A \<longrightarrow> is_unit x)"
   5.109    by (induction A) (auto simp: is_unit_mult_iff)
   5.110  
   5.111  lemma multiset_emptyI: "(\<And>x. x \<notin># A) \<Longrightarrow> A = {#}"
   5.112    by (intro multiset_eqI) (simp_all add: count_eq_zero_iff)
   5.113  
   5.114 -lemma is_unit_msetprod_primes_iff:
   5.115 +lemma is_unit_prod_mset_primes_iff:
   5.116    assumes "\<And>x. x \<in># A \<Longrightarrow> prime x"
   5.117 -  shows   "is_unit (msetprod A) \<longleftrightarrow> A = {#}"
   5.118 +  shows   "is_unit (prod_mset A) \<longleftrightarrow> A = {#}"
   5.119  proof
   5.120 -  assume unit: "is_unit (msetprod A)"
   5.121 +  assume unit: "is_unit (prod_mset A)"
   5.122    show "A = {#}"
   5.123    proof (intro multiset_emptyI notI)
   5.124      fix x assume "x \<in># A"
   5.125 -    with unit have "is_unit x" by (subst (asm) is_unit_msetprod_iff) blast
   5.126 +    with unit have "is_unit x" by (subst (asm) is_unit_prod_mset_iff) blast
   5.127      moreover from \<open>x \<in># A\<close> have "prime x" by (rule assms)
   5.128      ultimately show False by simp
   5.129    qed
   5.130  qed simp_all
   5.131  
   5.132 -lemma msetprod_primes_irreducible_imp_prime:
   5.133 -  assumes irred: "irreducible (msetprod A)"
   5.134 +lemma prod_mset_primes_irreducible_imp_prime:
   5.135 +  assumes irred: "irreducible (prod_mset A)"
   5.136    assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
   5.137    assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
   5.138    assumes C: "\<And>x. x \<in># C \<Longrightarrow> prime x"
   5.139 -  assumes dvd: "msetprod A dvd msetprod B * msetprod C"
   5.140 -  shows   "msetprod A dvd msetprod B \<or> msetprod A dvd msetprod C"
   5.141 +  assumes dvd: "prod_mset A dvd prod_mset B * prod_mset C"
   5.142 +  shows   "prod_mset A dvd prod_mset B \<or> prod_mset A dvd prod_mset C"
   5.143  proof -
   5.144 -  from dvd have "msetprod A dvd msetprod (B + C)"
   5.145 +  from dvd have "prod_mset A dvd prod_mset (B + C)"
   5.146      by simp
   5.147    with A B C have subset: "A \<subseteq># B + C"
   5.148 -    by (subst (asm) msetprod_dvd_msetprod_primes_iff) auto
   5.149 +    by (subst (asm) prod_mset_dvd_prod_mset_primes_iff) auto
   5.150    define A1 and A2 where "A1 = A #\<inter> B" and "A2 = A - A1"
   5.151    have "A = A1 + A2" unfolding A1_def A2_def
   5.152      by (rule sym, intro subset_mset.add_diff_inverse) simp_all
   5.153    from subset have "A1 \<subseteq># B" "A2 \<subseteq># C"
   5.154      by (auto simp: A1_def A2_def Multiset.subset_eq_diff_conv Multiset.union_commute)
   5.155 -  from \<open>A = A1 + A2\<close> have "msetprod A = msetprod A1 * msetprod A2" by simp
   5.156 -  from irred and this have "is_unit (msetprod A1) \<or> is_unit (msetprod A2)"
   5.157 +  from \<open>A = A1 + A2\<close> have "prod_mset A = prod_mset A1 * prod_mset A2" by simp
   5.158 +  from irred and this have "is_unit (prod_mset A1) \<or> is_unit (prod_mset A2)"
   5.159      by (rule irreducibleD)
   5.160    with A have "A1 = {#} \<or> A2 = {#}" unfolding A1_def A2_def
   5.161 -    by (subst (asm) (1 2) is_unit_msetprod_primes_iff) (auto dest: Multiset.in_diffD)
   5.162 +    by (subst (asm) (1 2) is_unit_prod_mset_primes_iff) (auto dest: Multiset.in_diffD)
   5.163    with dvd \<open>A = A1 + A2\<close> \<open>A1 \<subseteq># B\<close> \<open>A2 \<subseteq># C\<close> show ?thesis
   5.164 -    by (auto intro: msetprod_subset_imp_dvd)
   5.165 +    by (auto intro: prod_mset_subset_imp_dvd)
   5.166  qed
   5.167  
   5.168  lemma multiset_nonemptyE [elim]:
   5.169 @@ -564,30 +564,30 @@
   5.170    with that show ?thesis by blast
   5.171  qed
   5.172  
   5.173 -lemma msetprod_primes_finite_divisor_powers:
   5.174 +lemma prod_mset_primes_finite_divisor_powers:
   5.175    assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
   5.176    assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
   5.177    assumes "A \<noteq> {#}"
   5.178 -  shows   "finite {n. msetprod A ^ n dvd msetprod B}"
   5.179 +  shows   "finite {n. prod_mset A ^ n dvd prod_mset B}"
   5.180  proof -
   5.181    from \<open>A \<noteq> {#}\<close> obtain x where x: "x \<in># A" by blast
   5.182    define m where "m = count B x"
   5.183 -  have "{n. msetprod A ^ n dvd msetprod B} \<subseteq> {..m}"
   5.184 +  have "{n. prod_mset A ^ n dvd prod_mset B} \<subseteq> {..m}"
   5.185    proof safe
   5.186 -    fix n assume dvd: "msetprod A ^ n dvd msetprod B"
   5.187 -    from x have "x ^ n dvd msetprod A ^ n" by (intro dvd_power_same dvd_msetprod)
   5.188 +    fix n assume dvd: "prod_mset A ^ n dvd prod_mset B"
   5.189 +    from x have "x ^ n dvd prod_mset A ^ n" by (intro dvd_power_same dvd_prod_mset)
   5.190      also note dvd
   5.191 -    also have "x ^ n = msetprod (replicate_mset n x)" by simp
   5.192 +    also have "x ^ n = prod_mset (replicate_mset n x)" by simp
   5.193      finally have "replicate_mset n x \<subseteq># B"
   5.194 -      by (rule msetprod_primes_dvd_imp_subset) (insert A B x, simp_all split: if_splits)
   5.195 +      by (rule prod_mset_primes_dvd_imp_subset) (insert A B x, simp_all split: if_splits)
   5.196      thus "n \<le> m" by (simp add: count_le_replicate_mset_subset_eq m_def)
   5.197    qed
   5.198    moreover have "finite {..m}" by simp
   5.199    ultimately show ?thesis by (rule finite_subset)
   5.200  qed
   5.201  
   5.202 -lemma normalize_msetprod:
   5.203 -  "normalize (msetprod A) = msetprod (image_mset normalize A)"
   5.204 +lemma normalize_prod_mset:
   5.205 +  "normalize (prod_mset A) = prod_mset (image_mset normalize A)"
   5.206    by (induction A) (simp_all add: normalize_mult mult_ac)
   5.207  
   5.208  end
   5.209 @@ -655,20 +655,20 @@
   5.210  
   5.211  class factorial_semiring = normalization_semidom +
   5.212    assumes prime_factorization_exists:
   5.213 -            "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize x"
   5.214 +            "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
   5.215  begin
   5.216  
   5.217  lemma prime_factorization_exists':
   5.218    assumes "x \<noteq> 0"
   5.219 -  obtains A where "\<And>x. x \<in># A \<Longrightarrow> prime x" "msetprod A = normalize x"
   5.220 +  obtains A where "\<And>x. x \<in># A \<Longrightarrow> prime x" "prod_mset A = normalize x"
   5.221  proof -
   5.222    from prime_factorization_exists[OF assms] obtain A
   5.223 -    where A: "\<And>x. x \<in># A \<Longrightarrow> prime_elem x" "msetprod A = normalize x" by blast
   5.224 +    where A: "\<And>x. x \<in># A \<Longrightarrow> prime_elem x" "prod_mset A = normalize x" by blast
   5.225    define A' where "A' = image_mset normalize A"
   5.226 -  have "msetprod A' = normalize (msetprod A)"
   5.227 -    by (simp add: A'_def normalize_msetprod)
   5.228 +  have "prod_mset A' = normalize (prod_mset A)"
   5.229 +    by (simp add: A'_def normalize_prod_mset)
   5.230    also note A(2)
   5.231 -  finally have "msetprod A' = normalize x" by simp
   5.232 +  finally have "prod_mset A' = normalize x" by simp
   5.233    moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> prime x" by (auto simp: prime_def A'_def)
   5.234    ultimately show ?thesis by (intro that[of A']) blast
   5.235  qed
   5.236 @@ -685,8 +685,8 @@
   5.237      hence "a \<noteq> 0" "b \<noteq> 0" by blast+
   5.238      note nz = \<open>x \<noteq> 0\<close> this
   5.239      from nz[THEN prime_factorization_exists'] guess A B C . note ABC = this
   5.240 -    from assms ABC have "irreducible (msetprod A)" by simp
   5.241 -    from dvd msetprod_primes_irreducible_imp_prime[of A B C, OF this ABC(1,3,5)] ABC(2,4,6)
   5.242 +    from assms ABC have "irreducible (prod_mset A)" by simp
   5.243 +    from dvd prod_mset_primes_irreducible_imp_prime[of A B C, OF this ABC(1,3,5)] ABC(2,4,6)
   5.244        show ?thesis by (simp add: normalize_mult [symmetric])
   5.245    qed auto
   5.246  qed (insert assms, simp_all add: irreducible_def)
   5.247 @@ -703,7 +703,7 @@
   5.248    note nz = this \<open>y \<noteq> 0\<close>
   5.249    from nz[THEN prime_factorization_exists'] guess A B . note AB = this
   5.250    from AB assms have "A \<noteq> {#}" by (auto simp: normalize_1_iff)
   5.251 -  from AB(2,4) msetprod_primes_finite_divisor_powers [of A B, OF AB(1,3) this]
   5.252 +  from AB(2,4) prod_mset_primes_finite_divisor_powers [of A B, OF AB(1,3) this]
   5.253      show ?thesis by (simp add: normalize_power [symmetric])
   5.254  qed
   5.255  
   5.256 @@ -716,8 +716,8 @@
   5.257    proof safe
   5.258      fix p assume p: "prime p" and dvd: "p dvd x"
   5.259      from dvd have "p dvd normalize x" by simp
   5.260 -    also from A have "normalize x = msetprod A" by simp
   5.261 -    finally show "p \<in># A" using p A by (subst (asm) prime_dvd_msetprod_primes_iff)
   5.262 +    also from A have "normalize x = prod_mset A" by simp
   5.263 +    finally show "p \<in># A" using p A by (subst (asm) prime_dvd_prod_mset_primes_iff)
   5.264    qed
   5.265    moreover have "finite (set_mset A)" by simp
   5.266    ultimately show ?thesis by (rule finite_subset)
   5.267 @@ -733,7 +733,7 @@
   5.268    from prime_factorization_exists'[OF assms(1)] guess A . note A = this
   5.269    moreover from A and assms have "A \<noteq> {#}" by auto
   5.270    then obtain x where "x \<in># A" by blast
   5.271 -  with A(1) have *: "x dvd msetprod A" "prime x" by (auto simp: dvd_msetprod)
   5.272 +  with A(1) have *: "x dvd prod_mset A" "prime x" by (auto simp: dvd_prod_mset)
   5.273    with A have "x dvd a" by simp
   5.274    with * show ?thesis by blast
   5.275  qed
   5.276 @@ -744,12 +744,12 @@
   5.277  proof (cases "x = 0")
   5.278    case False
   5.279    from prime_factorization_exists'[OF this] guess A . note A = this
   5.280 -  from A(1) have "P (unit_factor x * msetprod A)"
   5.281 +  from A(1) have "P (unit_factor x * prod_mset A)"
   5.282    proof (induction A)
   5.283      case (add p A)
   5.284      from add.prems have "prime p" by simp
   5.285 -    moreover from add.prems have "P (unit_factor x * msetprod A)" by (intro add.IH) simp_all
   5.286 -    ultimately have "P (p * (unit_factor x * msetprod A))" by (rule assms(3))
   5.287 +    moreover from add.prems have "P (unit_factor x * prod_mset A)" by (intro add.IH) simp_all
   5.288 +    ultimately have "P (p * (unit_factor x * prod_mset A))" by (rule assms(3))
   5.289      thus ?case by (simp add: mult_ac)
   5.290    qed (simp_all add: assms False)
   5.291    with A show ?thesis by simp
   5.292 @@ -1072,9 +1072,9 @@
   5.293    qed (insert assms, auto simp: count_prime_factorization multiplicity_times_same)
   5.294  qed
   5.295  
   5.296 -lemma msetprod_prime_factorization:
   5.297 +lemma prod_mset_prime_factorization:
   5.298    assumes "x \<noteq> 0"
   5.299 -  shows   "msetprod (prime_factorization x) = normalize x"
   5.300 +  shows   "prod_mset (prime_factorization x) = normalize x"
   5.301    using assms
   5.302    by (induction x rule: prime_divisors_induct)
   5.303       (simp_all add: prime_factorization_unit prime_factorization_times_prime
   5.304 @@ -1122,14 +1122,14 @@
   5.305                  simp: count_prime_factorization multiplicity_self multiplicity_eq_zero_iff)
   5.306  qed
   5.307  
   5.308 -lemma prime_factorization_msetprod_primes:
   5.309 +lemma prime_factorization_prod_mset_primes:
   5.310    assumes "\<And>p. p \<in># A \<Longrightarrow> prime p"
   5.311 -  shows   "prime_factorization (msetprod A) = A"
   5.312 +  shows   "prime_factorization (prod_mset A) = A"
   5.313    using assms
   5.314  proof (induction A)
   5.315    case (add p A)
   5.316    from add.prems[of 0] have "0 \<notin># A" by auto
   5.317 -  hence "msetprod A \<noteq> 0" by auto
   5.318 +  hence "prod_mset A \<noteq> 0" by auto
   5.319    with add show ?case
   5.320      by (simp_all add: mult_ac prime_factorization_times_prime Multiset.union_commute)
   5.321  qed simp_all
   5.322 @@ -1184,23 +1184,23 @@
   5.323    shows   "prime_factorization x = prime_factorization y \<longleftrightarrow> normalize x = normalize y"
   5.324  proof
   5.325    assume "prime_factorization x = prime_factorization y"
   5.326 -  hence "msetprod (prime_factorization x) = msetprod (prime_factorization y)" by simp
   5.327 -  with assms show "normalize x = normalize y" by (simp add: msetprod_prime_factorization)
   5.328 +  hence "prod_mset (prime_factorization x) = prod_mset (prime_factorization y)" by simp
   5.329 +  with assms show "normalize x = normalize y" by (simp add: prod_mset_prime_factorization)
   5.330  qed (rule prime_factorization_cong)
   5.331  
   5.332  lemma prime_factorization_mult:
   5.333    assumes "x \<noteq> 0" "y \<noteq> 0"
   5.334    shows   "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
   5.335  proof -
   5.336 -  have "prime_factorization (msetprod (prime_factorization (x * y))) =
   5.337 -          prime_factorization (msetprod (prime_factorization x + prime_factorization y))"
   5.338 -    by (simp add: msetprod_prime_factorization assms normalize_mult)
   5.339 -  also have "prime_factorization (msetprod (prime_factorization (x * y))) =
   5.340 +  have "prime_factorization (prod_mset (prime_factorization (x * y))) =
   5.341 +          prime_factorization (prod_mset (prime_factorization x + prime_factorization y))"
   5.342 +    by (simp add: prod_mset_prime_factorization assms normalize_mult)
   5.343 +  also have "prime_factorization (prod_mset (prime_factorization (x * y))) =
   5.344                 prime_factorization (x * y)"
   5.345 -    by (rule prime_factorization_msetprod_primes) (simp_all add: in_prime_factorization_imp_prime)
   5.346 -  also have "prime_factorization (msetprod (prime_factorization x + prime_factorization y)) =
   5.347 +    by (rule prime_factorization_prod_mset_primes) (simp_all add: in_prime_factorization_imp_prime)
   5.348 +  also have "prime_factorization (prod_mset (prime_factorization x + prime_factorization y)) =
   5.349                 prime_factorization x + prime_factorization y"
   5.350 -    by (rule prime_factorization_msetprod_primes) (auto simp: in_prime_factorization_imp_prime)
   5.351 +    by (rule prime_factorization_prod_mset_primes) (auto simp: in_prime_factorization_imp_prime)
   5.352    finally show ?thesis .
   5.353  qed
   5.354  
   5.355 @@ -1209,17 +1209,17 @@
   5.356    by (induction n)
   5.357       (simp_all add: prime_factorization_mult prime_factorization_prime Multiset.union_commute)
   5.358  
   5.359 -lemma prime_decomposition: "unit_factor x * msetprod (prime_factorization x) = x"
   5.360 -  by (cases "x = 0") (simp_all add: msetprod_prime_factorization)
   5.361 +lemma prime_decomposition: "unit_factor x * prod_mset (prime_factorization x) = x"
   5.362 +  by (cases "x = 0") (simp_all add: prod_mset_prime_factorization)
   5.363  
   5.364  lemma prime_factorization_subset_iff_dvd:
   5.365    assumes [simp]: "x \<noteq> 0" "y \<noteq> 0"
   5.366    shows   "prime_factorization x \<subseteq># prime_factorization y \<longleftrightarrow> x dvd y"
   5.367  proof -
   5.368 -  have "x dvd y \<longleftrightarrow> msetprod (prime_factorization x) dvd msetprod (prime_factorization y)"
   5.369 -    by (simp add: msetprod_prime_factorization)
   5.370 +  have "x dvd y \<longleftrightarrow> prod_mset (prime_factorization x) dvd prod_mset (prime_factorization y)"
   5.371 +    by (simp add: prod_mset_prime_factorization)
   5.372    also have "\<dots> \<longleftrightarrow> prime_factorization x \<subseteq># prime_factorization y"
   5.373 -    by (auto intro!: msetprod_primes_dvd_imp_subset msetprod_subset_imp_dvd
   5.374 +    by (auto intro!: prod_mset_primes_dvd_imp_subset prod_mset_subset_imp_dvd
   5.375                       in_prime_factorization_imp_prime)
   5.376    finally show ?thesis ..
   5.377  qed
   5.378 @@ -1265,9 +1265,9 @@
   5.379    shows   "multiplicity p (x ^ n) = n * multiplicity p x"
   5.380    by (induction n) (simp_all add: assms prime_elem_multiplicity_mult_distrib)
   5.381  
   5.382 -lemma prime_elem_multiplicity_msetprod_distrib:
   5.383 +lemma prime_elem_multiplicity_prod_mset_distrib:
   5.384    assumes "prime_elem p" "0 \<notin># A"
   5.385 -  shows   "multiplicity p (msetprod A) = msetsum (image_mset (multiplicity p) A)"
   5.386 +  shows   "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)"
   5.387    using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib)
   5.388  
   5.389  lemma prime_elem_multiplicity_setprod_distrib:
   5.390 @@ -1275,8 +1275,8 @@
   5.391    shows   "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
   5.392  proof -
   5.393    have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
   5.394 -    using assms by (subst setprod_unfold_msetprod)
   5.395 -                   (simp_all add: prime_elem_multiplicity_msetprod_distrib setsum_unfold_msetsum 
   5.396 +    using assms by (subst setprod_unfold_prod_mset)
   5.397 +                   (simp_all add: prime_elem_multiplicity_prod_mset_distrib setsum_unfold_sum_mset 
   5.398                        multiset.map_comp o_def)
   5.399    also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
   5.400      by (induction A rule: finite_induct) simp_all
   5.401 @@ -1316,10 +1316,10 @@
   5.402    assumes "x \<noteq> 0"
   5.403    shows   "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
   5.404  proof -
   5.405 -  have "normalize x = msetprod (prime_factorization x)"
   5.406 -    by (simp add: msetprod_prime_factorization assms)
   5.407 +  have "normalize x = prod_mset (prime_factorization x)"
   5.408 +    by (simp add: prod_mset_prime_factorization assms)
   5.409    also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
   5.410 -    by (subst msetprod_multiplicity) (simp_all add: prime_factors_def)
   5.411 +    by (subst prod_mset_multiplicity) (simp_all add: prime_factors_def)
   5.412    also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
   5.413      by (intro setprod.cong) 
   5.414        (simp_all add: assms count_prime_factorization_prime prime_factors_prime)
   5.415 @@ -1347,30 +1347,30 @@
   5.416    from S_eq count_A have set_mset_A: "set_mset A = S"
   5.417      by (simp only: set_mset_def)
   5.418    from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
   5.419 -  also have "\<dots> = msetprod A" by (simp add: msetprod_multiplicity S_eq set_mset_A count_A)
   5.420 -  also from nz have "normalize n = msetprod (prime_factorization n)" 
   5.421 -    by (simp add: msetprod_prime_factorization)
   5.422 -  finally have "prime_factorization (msetprod A) = 
   5.423 -                  prime_factorization (msetprod (prime_factorization n))" by simp
   5.424 -  also from S(1) have "prime_factorization (msetprod A) = A"
   5.425 -    by (intro prime_factorization_msetprod_primes) (auto simp: set_mset_A)
   5.426 -  also have "prime_factorization (msetprod (prime_factorization n)) = prime_factorization n"
   5.427 -    by (intro prime_factorization_msetprod_primes) (auto dest: in_prime_factorization_imp_prime)
   5.428 +  also have "\<dots> = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A)
   5.429 +  also from nz have "normalize n = prod_mset (prime_factorization n)" 
   5.430 +    by (simp add: prod_mset_prime_factorization)
   5.431 +  finally have "prime_factorization (prod_mset A) = 
   5.432 +                  prime_factorization (prod_mset (prime_factorization n))" by simp
   5.433 +  also from S(1) have "prime_factorization (prod_mset A) = A"
   5.434 +    by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A)
   5.435 +  also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n"
   5.436 +    by (intro prime_factorization_prod_mset_primes) (auto dest: in_prime_factorization_imp_prime)
   5.437    finally show "S = prime_factors n" by (simp add: prime_factors_def set_mset_A [symmetric])
   5.438    
   5.439    show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
   5.440    proof safe
   5.441      fix p :: 'a assume p: "prime p"
   5.442      have "multiplicity p n = multiplicity p (normalize n)" by simp
   5.443 -    also have "normalize n = msetprod A" 
   5.444 -      by (simp add: msetprod_multiplicity S_eq set_mset_A count_A S)
   5.445 +    also have "normalize n = prod_mset A" 
   5.446 +      by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A S)
   5.447      also from p set_mset_A S(1) 
   5.448 -    have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
   5.449 -      by (intro prime_elem_multiplicity_msetprod_distrib) auto
   5.450 +    have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
   5.451 +      by (intro prime_elem_multiplicity_prod_mset_distrib) auto
   5.452      also from S(1) p
   5.453      have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
   5.454        by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
   5.455 -    also have "msetsum \<dots> = f p" by (simp add: msetsum_delta' count_A)
   5.456 +    also have "sum_mset \<dots> = f p" by (simp add: sum_mset_delta' count_A)
   5.457      finally show "f p = multiplicity p n" ..
   5.458    qed
   5.459  qed
   5.460 @@ -1434,9 +1434,9 @@
   5.461    have "prime_factorization (\<Prod>i \<in># M. i) = prime_factorization (\<Prod>i \<in># N. i)"
   5.462      by (simp only: assms)
   5.463    also from assms have "prime_factorization (\<Prod>i \<in># M. i) = M"
   5.464 -    by (subst prime_factorization_msetprod_primes) simp_all
   5.465 +    by (subst prime_factorization_prod_mset_primes) simp_all
   5.466    also from assms have "prime_factorization (\<Prod>i \<in># N. i) = N"
   5.467 -    by (subst prime_factorization_msetprod_primes) simp_all
   5.468 +    by (subst prime_factorization_prod_mset_primes) simp_all
   5.469    finally show ?thesis .
   5.470  qed
   5.471  
   5.472 @@ -1456,18 +1456,18 @@
   5.473  
   5.474  definition "gcd_factorial a b = (if a = 0 then normalize b
   5.475       else if b = 0 then normalize a
   5.476 -     else msetprod (prime_factorization a #\<inter> prime_factorization b))"
   5.477 +     else prod_mset (prime_factorization a #\<inter> prime_factorization b))"
   5.478  
   5.479  definition "lcm_factorial a b = (if a = 0 \<or> b = 0 then 0
   5.480 -     else msetprod (prime_factorization a #\<union> prime_factorization b))"
   5.481 +     else prod_mset (prime_factorization a #\<union> prime_factorization b))"
   5.482  
   5.483  definition "Gcd_factorial A =
   5.484 -  (if A \<subseteq> {0} then 0 else msetprod (Inf (prime_factorization ` (A - {0}))))"
   5.485 +  (if A \<subseteq> {0} then 0 else prod_mset (Inf (prime_factorization ` (A - {0}))))"
   5.486  
   5.487  definition "Lcm_factorial A =
   5.488    (if A = {} then 1
   5.489     else if 0 \<notin> A \<and> subset_mset.bdd_above (prime_factorization ` (A - {0})) then
   5.490 -     msetprod (Sup (prime_factorization ` A))
   5.491 +     prod_mset (Sup (prime_factorization ` A))
   5.492     else
   5.493       0)"
   5.494  
   5.495 @@ -1476,10 +1476,10 @@
   5.496    shows   "prime_factorization (gcd_factorial a b) = prime_factorization a #\<inter> prime_factorization b"
   5.497  proof -
   5.498    have "prime_factorization (gcd_factorial a b) =
   5.499 -          prime_factorization (msetprod (prime_factorization a #\<inter> prime_factorization b))"
   5.500 +          prime_factorization (prod_mset (prime_factorization a #\<inter> prime_factorization b))"
   5.501      by (simp add: gcd_factorial_def)
   5.502    also have "\<dots> = prime_factorization a #\<inter> prime_factorization b"
   5.503 -    by (subst prime_factorization_msetprod_primes) (auto simp add: in_prime_factorization_imp_prime)
   5.504 +    by (subst prime_factorization_prod_mset_primes) (auto simp add: in_prime_factorization_imp_prime)
   5.505    finally show ?thesis .
   5.506  qed
   5.507  
   5.508 @@ -1488,10 +1488,10 @@
   5.509    shows   "prime_factorization (lcm_factorial a b) = prime_factorization a #\<union> prime_factorization b"
   5.510  proof -
   5.511    have "prime_factorization (lcm_factorial a b) =
   5.512 -          prime_factorization (msetprod (prime_factorization a #\<union> prime_factorization b))"
   5.513 +          prime_factorization (prod_mset (prime_factorization a #\<union> prime_factorization b))"
   5.514      by (simp add: lcm_factorial_def)
   5.515    also have "\<dots> = prime_factorization a #\<union> prime_factorization b"
   5.516 -    by (subst prime_factorization_msetprod_primes) (auto simp add: in_prime_factorization_imp_prime)
   5.517 +    by (subst prime_factorization_prod_mset_primes) (auto simp add: in_prime_factorization_imp_prime)
   5.518    finally show ?thesis .
   5.519  qed
   5.520  
   5.521 @@ -1507,7 +1507,7 @@
   5.522    with in_prime_factorization_imp_prime[of _ x]
   5.523      have "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> prime p" by blast
   5.524    with assms show ?thesis
   5.525 -    by (simp add: Gcd_factorial_def prime_factorization_msetprod_primes)
   5.526 +    by (simp add: Gcd_factorial_def prime_factorization_prod_mset_primes)
   5.527  qed
   5.528  
   5.529  lemma prime_factorization_Lcm_factorial:
   5.530 @@ -1523,7 +1523,7 @@
   5.531    have "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> prime y"
   5.532      by (auto simp: in_Sup_multiset_iff assms in_prime_factorization_imp_prime)
   5.533    with assms False show ?thesis
   5.534 -    by (simp add: Lcm_factorial_def prime_factorization_msetprod_primes)
   5.535 +    by (simp add: Lcm_factorial_def prime_factorization_prod_mset_primes)
   5.536  qed
   5.537  
   5.538  lemma gcd_factorial_commute: "gcd_factorial a b = gcd_factorial b a"
   5.539 @@ -1543,9 +1543,9 @@
   5.540  
   5.541  lemma normalize_gcd_factorial: "normalize (gcd_factorial a b) = gcd_factorial a b"
   5.542  proof -
   5.543 -  have "normalize (msetprod (prime_factorization a #\<inter> prime_factorization b)) =
   5.544 -          msetprod (prime_factorization a #\<inter> prime_factorization b)"
   5.545 -    by (intro normalize_msetprod_primes) (auto simp: in_prime_factorization_imp_prime)
   5.546 +  have "normalize (prod_mset (prime_factorization a #\<inter> prime_factorization b)) =
   5.547 +          prod_mset (prime_factorization a #\<inter> prime_factorization b)"
   5.548 +    by (intro normalize_prod_mset_primes) (auto simp: in_prime_factorization_imp_prime)
   5.549    thus ?thesis by (simp add: gcd_factorial_def)
   5.550  qed
   5.551  
   5.552 @@ -1557,8 +1557,8 @@
   5.553    from that False have "?p c \<subseteq># ?p a" "?p c \<subseteq># ?p b"
   5.554      by (simp_all add: prime_factorization_subset_iff_dvd)
   5.555    hence "prime_factorization c \<subseteq>#
   5.556 -           prime_factorization (msetprod (prime_factorization a #\<inter> prime_factorization b))"
   5.557 -    using False by (subst prime_factorization_msetprod_primes)
   5.558 +           prime_factorization (prod_mset (prime_factorization a #\<inter> prime_factorization b))"
   5.559 +    using False by (subst prime_factorization_prod_mset_primes)
   5.560                     (auto simp: in_prime_factorization_imp_prime)
   5.561    with False show ?thesis
   5.562      by (auto simp: gcd_factorial_def prime_factorization_subset_iff_dvd [symmetric])
   5.563 @@ -1569,13 +1569,13 @@
   5.564  proof (cases "a = 0 \<or> b = 0")
   5.565    case False
   5.566    let ?p = "prime_factorization"
   5.567 -  from False have "msetprod (?p (a * b)) div gcd_factorial a b =
   5.568 -                     msetprod (?p a + ?p b - ?p a #\<inter> ?p b)"
   5.569 -    by (subst msetprod_diff) (auto simp: lcm_factorial_def gcd_factorial_def
   5.570 +  from False have "prod_mset (?p (a * b)) div gcd_factorial a b =
   5.571 +                     prod_mset (?p a + ?p b - ?p a #\<inter> ?p b)"
   5.572 +    by (subst prod_mset_diff) (auto simp: lcm_factorial_def gcd_factorial_def
   5.573                                  prime_factorization_mult subset_mset.le_infI1)
   5.574 -  also from False have "msetprod (?p (a * b)) = normalize (a * b)"
   5.575 -    by (intro msetprod_prime_factorization) simp_all
   5.576 -  also from False have "msetprod (?p a + ?p b - ?p a #\<inter> ?p b) = lcm_factorial a b"
   5.577 +  also from False have "prod_mset (?p (a * b)) = normalize (a * b)"
   5.578 +    by (intro prod_mset_prime_factorization) simp_all
   5.579 +  also from False have "prod_mset (?p a + ?p b - ?p a #\<inter> ?p b) = lcm_factorial a b"
   5.580      by (simp add: union_diff_inter_eq_sup lcm_factorial_def)
   5.581    finally show ?thesis ..
   5.582  qed (auto simp: lcm_factorial_def)
   5.583 @@ -1590,7 +1590,7 @@
   5.584    hence "prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p
   5.585      using that by (auto dest: mset_subset_eqD intro: in_prime_factorization_imp_prime)
   5.586    with False show ?thesis
   5.587 -    by (auto simp add: Gcd_factorial_def normalize_msetprod_primes)
   5.588 +    by (auto simp add: Gcd_factorial_def normalize_prod_mset_primes)
   5.589  qed (simp_all add: Gcd_factorial_def)
   5.590  
   5.591  lemma Gcd_factorial_eq_0_iff:
   5.592 @@ -1634,9 +1634,9 @@
   5.593    "normalize (Lcm_factorial A) = Lcm_factorial A"
   5.594  proof (cases "subset_mset.bdd_above (prime_factorization ` A)")
   5.595    case True
   5.596 -  hence "normalize (msetprod (Sup (prime_factorization ` A))) =
   5.597 -           msetprod (Sup (prime_factorization ` A))"
   5.598 -    by (intro normalize_msetprod_primes)
   5.599 +  hence "normalize (prod_mset (Sup (prime_factorization ` A))) =
   5.600 +           prod_mset (Sup (prime_factorization ` A))"
   5.601 +    by (intro normalize_prod_mset_primes)
   5.602         (auto simp: in_Sup_multiset_iff in_prime_factorization_imp_prime)
   5.603    with True show ?thesis by (simp add: Lcm_factorial_def)
   5.604  qed (auto simp: Lcm_factorial_def)
   5.605 @@ -1695,7 +1695,7 @@
   5.606    assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
   5.607    assumes irreducible_imp_prime_elem: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
   5.608    assumes "(x::'a) \<noteq> 0"
   5.609 -  shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize x"
   5.610 +  shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
   5.611  using \<open>x \<noteq> 0\<close>
   5.612  proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct)
   5.613    case (less a)
   5.614 @@ -1723,7 +1723,7 @@
   5.615        with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)"
   5.616          by (rule psubset_card_mono)
   5.617        moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
   5.618 -      ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize b"
   5.619 +      ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize b"
   5.620          by (intro less) auto
   5.621        then guess A .. note A = this
   5.622  
   5.623 @@ -1742,7 +1742,7 @@
   5.624        ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
   5.625        with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)"
   5.626          by (rule psubset_card_mono)
   5.627 -      with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize c"
   5.628 +      with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize c"
   5.629          by (intro less) auto
   5.630        then guess B .. note B = this
   5.631  
   5.632 @@ -1806,12 +1806,12 @@
   5.633  proof -
   5.634    have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
   5.635    also have "\<dots> = ?rhs1"
   5.636 -    by (auto simp: gcd_factorial_def assms msetprod_multiplicity set_mset_prime_factorization
   5.637 +    by (auto simp: gcd_factorial_def assms prod_mset_multiplicity set_mset_prime_factorization
   5.638            count_prime_factorization_prime dest: prime_factors_prime intro!: setprod.cong)
   5.639    finally show "gcd x y = ?rhs1" .
   5.640    have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
   5.641    also have "\<dots> = ?rhs2"
   5.642 -    by (auto simp: lcm_factorial_def assms msetprod_multiplicity set_mset_prime_factorization
   5.643 +    by (auto simp: lcm_factorial_def assms prod_mset_multiplicity set_mset_prime_factorization
   5.644            count_prime_factorization_prime dest: prime_factors_prime intro!: setprod.cong)
   5.645    finally show "lcm x y = ?rhs2" .
   5.646  qed
     6.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Fri Sep 09 14:15:16 2016 +0200
     6.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Fri Sep 09 15:12:40 2016 +0200
     6.3 @@ -653,9 +653,9 @@
     6.4  proof -
     6.5    have "\<exists>xs. mset xs = prime_factorization n" by (rule ex_mset)
     6.6    then guess xs .. note xs = this
     6.7 -  from assms have "n = msetprod (prime_factorization n)" 
     6.8 -    by (simp add: msetprod_prime_factorization)
     6.9 -  also have "\<dots> = msetprod (mset xs)" by (simp add: xs)
    6.10 +  from assms have "n = prod_mset (prime_factorization n)" 
    6.11 +    by (simp add: prod_mset_prime_factorization)
    6.12 +  also have "\<dots> = prod_mset (mset xs)" by (simp add: xs)
    6.13    also have "\<dots> = foldr op * xs 1" by (induction xs) simp_all
    6.14    finally have "foldr op * xs 1 = n" ..
    6.15    moreover have "\<forall>p\<in>#mset xs. prime p"
     7.1 --- a/src/HOL/Number_Theory/Primes.thy	Fri Sep 09 14:15:16 2016 +0200
     7.2 +++ b/src/HOL/Number_Theory/Primes.thy	Fri Sep 09 15:12:40 2016 +0200
     7.3 @@ -470,19 +470,19 @@
     7.4    unfolding prime_factors_def 
     7.5    by (auto split: if_splits simp: prime_def dest!: in_prime_factorization_imp_prime)
     7.6  
     7.7 -lemma msetprod_prime_factorization_int:
     7.8 +lemma prod_mset_prime_factorization_int:
     7.9    fixes n :: int
    7.10    assumes "n > 0"
    7.11 -  shows   "msetprod (prime_factorization n) = n"
    7.12 -  using assms by (simp add: msetprod_prime_factorization)
    7.13 +  shows   "prod_mset (prime_factorization n) = n"
    7.14 +  using assms by (simp add: prod_mset_prime_factorization)
    7.15  
    7.16  lemma prime_factorization_exists_nat:
    7.17    "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
    7.18    using prime_factorization_exists[of n] by (auto simp: prime_def)
    7.19  
    7.20 -lemma msetprod_prime_factorization_nat [simp]: 
    7.21 -  "(n::nat) > 0 \<Longrightarrow> msetprod (prime_factorization n) = n"
    7.22 -  by (subst msetprod_prime_factorization) simp_all
    7.23 +lemma prod_mset_prime_factorization_nat [simp]: 
    7.24 +  "(n::nat) > 0 \<Longrightarrow> prod_mset (prime_factorization n) = n"
    7.25 +  by (subst prod_mset_prime_factorization) simp_all
    7.26  
    7.27  lemma prime_factorization_nat:
    7.28      "n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
    7.29 @@ -587,13 +587,13 @@
    7.30      by (intro setprod.cong) (auto simp: g_def)
    7.31    also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
    7.32      by (intro setprod.mono_neutral_right) (auto simp: g_def set_mset_A)
    7.33 -  also have "\<dots> = msetprod A"
    7.34 -    by (auto simp: msetprod_multiplicity count_A set_mset_A intro!: setprod.cong)
    7.35 -  also from assms have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
    7.36 -    by (subst prime_elem_multiplicity_msetprod_distrib) (auto dest: prime)
    7.37 +  also have "\<dots> = prod_mset A"
    7.38 +    by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: setprod.cong)
    7.39 +  also from assms have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
    7.40 +    by (subst prime_elem_multiplicity_prod_mset_distrib) (auto dest: prime)
    7.41    also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
    7.42      by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
    7.43 -  also have "msetsum \<dots> = (if p \<in> S then f p else 0)" by (simp add: msetsum_delta count_A g_def)
    7.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)
    7.45    finally show ?thesis .
    7.46  qed
    7.47  
     8.1 --- a/src/HOL/Proofs/Extraction/Euclid.thy	Fri Sep 09 14:15:16 2016 +0200
     8.2 +++ b/src/HOL/Proofs/Extraction/Euclid.thy	Fri Sep 09 15:12:40 2016 +0200
     8.3 @@ -119,7 +119,7 @@
     8.4  qed
     8.5  
     8.6  lemma dvd_prod [iff]: "n dvd (\<Prod>m::nat \<in># mset (n # ns). m)"
     8.7 -  by (simp add: msetprod_Un)
     8.8 +  by (simp add: prod_mset_Un)
     8.9  
    8.10  definition all_prime :: "nat list \<Rightarrow> bool"
    8.11    where "all_prime ps \<longleftrightarrow> (\<forall>p\<in>set ps. prime p)"
    8.12 @@ -142,7 +142,7 @@
    8.13      by (simp add: all_prime_append)
    8.14    moreover
    8.15    have "(\<Prod>m::nat \<in># mset (ms @ ns). m) = (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)"
    8.16 -    using assms by (simp add: msetprod_Un)
    8.17 +    using assms by (simp add: prod_mset_Un)
    8.18    ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" ..
    8.19    then show ?thesis ..
    8.20  qed
    8.21 @@ -153,7 +153,7 @@
    8.22    using \<open>ps \<noteq> []\<close> \<open>all_prime ps\<close>
    8.23    unfolding One_nat_def [symmetric]
    8.24    by (induct ps rule: list_nonempty_induct)
    8.25 -    (simp_all add: all_prime_simps msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
    8.26 +    (simp_all add: all_prime_simps prod_mset_Un prime_gt_1_nat less_1_mult del: One_nat_def)
    8.27  
    8.28  lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = n)"
    8.29  proof (induct n rule: nat_wf_ind)
    8.30 @@ -182,7 +182,7 @@
    8.31      with prod_ps1_m prod_ps2_k nmk show ?thesis by simp
    8.32    next
    8.33      assume "prime n" then have "all_prime [n]" by (simp add: all_prime_simps)
    8.34 -    moreover have "(\<Prod>m::nat \<in># mset [n]. m) = n" by (simp add: msetprod_singleton)
    8.35 +    moreover have "(\<Prod>m::nat \<in># mset [n]. m) = n" by (simp)
    8.36      ultimately have "all_prime [n] \<and> (\<Prod>m::nat \<in># mset [n]. m) = n" ..
    8.37      then show ?thesis ..
    8.38    qed