renamed multiset_of -> mset
authornipkow
Fri Jun 19 15:55:22 2015 +0200 (2015-06-19)
changeset 60515484559628038
parent 60514 78a82c37b4b2
child 60516 0826b7025d07
renamed multiset_of -> mset
NEWS
src/HOL/Algebra/Divisibility.thy
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Imperative_HOL/ex/Sublist.thy
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/Tree_Multiset.thy
src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
src/HOL/Proofs/Extraction/Euclid.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/UNITY/Comp/AllocBase.thy
src/HOL/ZF/LProd.thy
src/HOL/ex/Bubblesort.thy
src/HOL/ex/MergeSort.thy
src/HOL/ex/Quicksort.thy
     1.1 --- a/NEWS	Thu Jun 18 16:17:51 2015 +0200
     1.2 +++ b/NEWS	Fri Jun 19 15:55:22 2015 +0200
     1.3 @@ -116,8 +116,9 @@
     1.4      (e.g. add_mono ~> subset_mset.add_mono).
     1.5      INCOMPATIBILITY.
     1.6    - Renamed conversions:
     1.7 +      multiset_of ~> mset
     1.8 +      multiset_of_set ~> mset_set
     1.9        set_of ~> set_mset
    1.10 -      multiset_of_set ~> mset_set
    1.11      INCOMPATIBILITY
    1.12    - Renamed lemmas:
    1.13        mset_le_def ~> subseteq_mset_def
     2.1 --- a/src/HOL/Algebra/Divisibility.thy	Thu Jun 18 16:17:51 2015 +0200
     2.2 +++ b/src/HOL/Algebra/Divisibility.thy	Fri Jun 19 15:55:22 2015 +0200
     2.3 @@ -1063,9 +1063,9 @@
     2.4    shows "P (set bs)"
     2.5  proof -
     2.6    from perm
     2.7 -      have "multiset_of as = multiset_of bs"
     2.8 -      by (simp add: multiset_of_eq_perm)
     2.9 -  hence "set as = set bs" by (rule multiset_of_eq_setD)
    2.10 +      have "mset as = mset bs"
    2.11 +      by (simp add: mset_eq_perm)
    2.12 +  hence "set as = set bs" by (rule mset_eq_setD)
    2.13    with as
    2.14        show "P (set bs)" by simp
    2.15  qed
    2.16 @@ -1792,7 +1792,7 @@
    2.17    "assocs G x == eq_closure_of (division_rel G) {x}"
    2.18  
    2.19  definition
    2.20 -  "fmset G as = multiset_of (map (\<lambda>a. assocs G a) as)"
    2.21 +  "fmset G as = mset (map (\<lambda>a. assocs G a) as)"
    2.22  
    2.23  
    2.24  text {* Helper lemmas *}
    2.25 @@ -1840,7 +1840,7 @@
    2.26    assumes prm: "as <~~> bs"
    2.27    shows "fmset G as = fmset G bs"
    2.28  using perm_map[OF prm]
    2.29 -by (simp add: multiset_of_eq_perm fmset_def)
    2.30 +by (simp add: mset_eq_perm fmset_def)
    2.31  
    2.32  lemma (in comm_monoid_cancel) eqc_listassoc_cong:
    2.33    assumes "as [\<sim>] bs"
    2.34 @@ -1923,9 +1923,9 @@
    2.35      and p3: "map (assocs G) as <~~> map (assocs G) bs"
    2.36  
    2.37    from p1
    2.38 -      have "multiset_of (map (assocs G) as) = multiset_of ys"
    2.39 -      by (simp add: multiset_of_eq_perm)
    2.40 -  hence setys: "set (map (assocs G) as) = set ys" by (rule multiset_of_eq_setD)
    2.41 +      have "mset (map (assocs G) as) = mset ys"
    2.42 +      by (simp add: mset_eq_perm)
    2.43 +  hence setys: "set (map (assocs G) as) = set ys" by (rule mset_eq_setD)
    2.44  
    2.45    have "set (map (assocs G) as) = { assocs G x | x. x \<in> set as}" by clarsimp fast
    2.46    with setys have "set ys \<subseteq> { assocs G x | x. x \<in> set as}" by simp
    2.47 @@ -1980,7 +1980,7 @@
    2.48  proof -
    2.49    from mset
    2.50        have mpp: "map (assocs G) as <~~> map (assocs G) bs"
    2.51 -      by (simp add: fmset_def multiset_of_eq_perm)
    2.52 +      by (simp add: fmset_def mset_eq_perm)
    2.53  
    2.54    have "\<exists>cas. cas = map (assocs G) as" by simp
    2.55    from this obtain cas where cas: "cas = map (assocs G) as" by simp
    2.56 @@ -2003,7 +2003,7 @@
    2.57        and tm: "map (assocs G) as' = map (assocs G) bs"
    2.58        by auto
    2.59    from tm have lene: "length as' = length bs" by (rule map_eq_imp_length_eq)
    2.60 -  from tp have "set as = set as'" by (simp add: multiset_of_eq_perm multiset_of_eq_setD)
    2.61 +  from tp have "set as = set as'" by (simp add: mset_eq_perm mset_eq_setD)
    2.62    with ascarr
    2.63        have as'carr: "set as' \<subseteq> carrier G" by simp
    2.64  
    2.65 @@ -2028,13 +2028,13 @@
    2.66    assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
    2.67    shows "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> fmset G cs = Cs"
    2.68  proof -
    2.69 -  have "\<exists>Cs'. Cs = multiset_of Cs'"
    2.70 -      by (rule surjE[OF surj_multiset_of], fast)
    2.71 +  have "\<exists>Cs'. Cs = mset Cs'"
    2.72 +      by (rule surjE[OF surj_mset], fast)
    2.73    from this obtain Cs'
    2.74 -      where Cs: "Cs = multiset_of Cs'"
    2.75 +      where Cs: "Cs = mset Cs'"
    2.76        by auto
    2.77  
    2.78 -  have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> multiset_of (map (assocs G) cs) = Cs"
    2.79 +  have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> mset (map (assocs G) cs) = Cs"
    2.80    using elems
    2.81    unfolding Cs
    2.82      apply (induct Cs', simp)
    2.83 @@ -2042,7 +2042,7 @@
    2.84      fix a Cs' cs 
    2.85      assume ih: "\<And>X. X = a \<or> X \<in> set Cs' \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
    2.86        and csP: "\<forall>x\<in>set cs. P x"
    2.87 -      and mset: "multiset_of (map (assocs G) cs) = multiset_of Cs'"
    2.88 +      and mset: "mset (map (assocs G) cs) = mset Cs'"
    2.89      from ih
    2.90          have "\<exists>x. P x \<and> a = assocs G x" by fast
    2.91      from this obtain c
    2.92 @@ -2052,11 +2052,11 @@
    2.93      from cP csP
    2.94          have tP: "\<forall>x\<in>set (c#cs). P x" by simp
    2.95      from mset a
    2.96 -    have "multiset_of (map (assocs G) (c#cs)) = multiset_of Cs' + {#a#}" by simp
    2.97 +    have "mset (map (assocs G) (c#cs)) = mset Cs' + {#a#}" by simp
    2.98      from tP this
    2.99      show "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and>
   2.100 -               multiset_of (map (assocs G) cs) =
   2.101 -               multiset_of Cs' + {#a#}" by fast
   2.102 +               mset (map (assocs G) cs) =
   2.103 +               mset Cs' + {#a#}" by fast
   2.104    qed
   2.105    thus ?thesis by (simp add: fmset_def)
   2.106  qed
     3.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Thu Jun 18 16:17:51 2015 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jun 19 15:55:22 2015 +0200
     3.3 @@ -34,11 +34,11 @@
     3.4  
     3.5  lemma swap_permutes:
     3.6    assumes "effect (swap a i j) h h' rs"
     3.7 -  shows "multiset_of (Array.get h' a) 
     3.8 -  = multiset_of (Array.get h a)"
     3.9 +  shows "mset (Array.get h' a) 
    3.10 +  = mset (Array.get h a)"
    3.11    using assms
    3.12    unfolding swap_def
    3.13 -  by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE)
    3.14 +  by (auto simp add: Array.length_def mset_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE)
    3.15  
    3.16  function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
    3.17  where
    3.18 @@ -59,8 +59,8 @@
    3.19  
    3.20  lemma part_permutes:
    3.21    assumes "effect (part1 a l r p) h h' rs"
    3.22 -  shows "multiset_of (Array.get h' a) 
    3.23 -  = multiset_of (Array.get h a)"
    3.24 +  shows "mset (Array.get h' a) 
    3.25 +  = mset (Array.get h a)"
    3.26    using assms
    3.27  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    3.28    case (1 a l r p h h' rs)
    3.29 @@ -244,8 +244,8 @@
    3.30  
    3.31  lemma partition_permutes:
    3.32    assumes "effect (partition a l r) h h' rs"
    3.33 -  shows "multiset_of (Array.get h' a) 
    3.34 -  = multiset_of (Array.get h a)"
    3.35 +  shows "mset (Array.get h' a) 
    3.36 +  = mset (Array.get h a)"
    3.37  proof -
    3.38      from assms part_permutes swap_permutes show ?thesis
    3.39        unfolding partition.simps
    3.40 @@ -424,8 +424,8 @@
    3.41  
    3.42  lemma quicksort_permutes:
    3.43    assumes "effect (quicksort a l r) h h' rs"
    3.44 -  shows "multiset_of (Array.get h' a) 
    3.45 -  = multiset_of (Array.get h a)"
    3.46 +  shows "mset (Array.get h' a) 
    3.47 +  = mset (Array.get h a)"
    3.48    using assms
    3.49  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
    3.50    case (1 a l r h h' rs)
    3.51 @@ -533,23 +533,23 @@
    3.52          and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> Array.get h1 a ! p \<le> j"
    3.53          by (auto simp add: all_in_set_subarray_conv)
    3.54        from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
    3.55 -        length_remains 1(5) pivot multiset_of_sublist [of l p "Array.get h1 a" "Array.get h2 a"]
    3.56 -      have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
    3.57 +        length_remains 1(5) pivot mset_sublist [of l p "Array.get h1 a" "Array.get h2 a"]
    3.58 +      have multiset_partconds1: "mset (subarray l p a h2) = mset (subarray l p a h1)"
    3.59          unfolding Array.length_def subarray_def by (cases p, auto)
    3.60        with left_subarray_remains part_conds1 pivot_unchanged
    3.61        have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> Array.get h' a ! p"
    3.62 -        by (simp, subst set_mset_multiset_of[symmetric], simp)
    3.63 +        by (simp, subst set_mset_mset[symmetric], simp)
    3.64            (* -- These steps are the analogous for the right sublist \<dots> *)
    3.65        from quicksort_outer_remains [OF qs1] length_remains
    3.66        have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
    3.67          by (auto simp add: subarray_eq_samelength_iff)
    3.68        from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
    3.69 -        length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
    3.70 -      have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
    3.71 +        length_remains 1(5) pivot mset_sublist [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
    3.72 +      have multiset_partconds2: "mset (subarray (p + 1) (r + 1) a h') = mset (subarray (p + 1) (r + 1) a h2)"
    3.73          unfolding Array.length_def subarray_def by auto
    3.74        with right_subarray_remains part_conds2 pivot_unchanged
    3.75        have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> Array.get h' a ! p \<le> j"
    3.76 -        by (simp, subst set_mset_multiset_of[symmetric], simp)
    3.77 +        by (simp, subst set_mset_mset[symmetric], simp)
    3.78            (* -- Thirdly and finally, we show that the array is sorted
    3.79            following from the facts above. *)
    3.80        from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [Array.get h' a ! p] @ subarray (p + 1) (r + 1) a h'"
     4.1 --- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Thu Jun 18 16:17:51 2015 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Fri Jun 19 15:55:22 2015 +0200
     4.3 @@ -471,26 +471,26 @@
     4.4  unfolding set_sublist' by blast
     4.5  
     4.6  
     4.7 -lemma multiset_of_sublist:
     4.8 +lemma mset_sublist:
     4.9  assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
    4.10  assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
    4.11  assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
    4.12 -assumes multiset: "multiset_of xs = multiset_of ys"
    4.13 -  shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
    4.14 +assumes multiset: "mset xs = mset ys"
    4.15 +  shows "mset (sublist' l r xs) = mset (sublist' l r ys)"
    4.16  proof -
    4.17    from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") 
    4.18      by (simp add: sublist'_append)
    4.19 -  from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
    4.20 +  from multiset have length_eq: "List.length xs = List.length ys" by (rule mset_eq_length)
    4.21    with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") 
    4.22      by (simp add: sublist'_append)
    4.23 -  from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
    4.24 +  from xs_def ys_def multiset have "mset ?xs_long = mset ?ys_long" by simp
    4.25    moreover
    4.26    from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
    4.27      by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
    4.28    moreover
    4.29    from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
    4.30      by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
    4.31 -  ultimately show ?thesis by (simp add: multiset_of_append)
    4.32 +  ultimately show ?thesis by (simp add: mset_append)
    4.33  qed
    4.34  
    4.35  
     5.1 --- a/src/HOL/Library/DAList_Multiset.thy	Thu Jun 18 16:17:51 2015 +0200
     5.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Fri Jun 19 15:55:22 2015 +0200
     5.3 @@ -267,7 +267,7 @@
     5.4  
     5.5  declare multiset_inter_def [code]
     5.6  declare sup_subset_mset_def [code]
     5.7 -declare multiset_of.simps [code]
     5.8 +declare mset.simps [code]
     5.9  
    5.10  
    5.11  fun fold_impl :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<times> nat) list \<Rightarrow> 'b"
     6.1 --- a/src/HOL/Library/Multiset.thy	Thu Jun 18 16:17:51 2015 +0200
     6.2 +++ b/src/HOL/Library/Multiset.thy	Fri Jun 19 15:55:22 2015 +0200
     6.3 @@ -963,46 +963,46 @@
     6.4  
     6.5  subsection \<open>Further conversions\<close>
     6.6  
     6.7 -primrec multiset_of :: "'a list \<Rightarrow> 'a multiset" where
     6.8 -  "multiset_of [] = {#}" |
     6.9 -  "multiset_of (a # x) = multiset_of x + {# a #}"
    6.10 +primrec mset :: "'a list \<Rightarrow> 'a multiset" where
    6.11 +  "mset [] = {#}" |
    6.12 +  "mset (a # x) = mset x + {# a #}"
    6.13  
    6.14  lemma in_multiset_in_set:
    6.15 -  "x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs"
    6.16 +  "x \<in># mset xs \<longleftrightarrow> x \<in> set xs"
    6.17    by (induct xs) simp_all
    6.18  
    6.19 -lemma count_multiset_of:
    6.20 -  "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
    6.21 +lemma count_mset:
    6.22 +  "count (mset xs) x = length (filter (\<lambda>y. x = y) xs)"
    6.23    by (induct xs) simp_all
    6.24  
    6.25 -lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
    6.26 +lemma mset_zero_iff[simp]: "(mset x = {#}) = (x = [])"
    6.27    by (induct x) auto
    6.28  
    6.29 -lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
    6.30 +lemma mset_zero_iff_right[simp]: "({#} = mset x) = (x = [])"
    6.31  by (induct x) auto
    6.32  
    6.33 -lemma set_mset_multiset_of[simp]: "set_mset (multiset_of x) = set x"
    6.34 +lemma set_mset_mset[simp]: "set_mset (mset x) = set x"
    6.35  by (induct x) auto
    6.36  
    6.37 -lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
    6.38 +lemma mem_set_multiset_eq: "x \<in> set xs = (x :# mset xs)"
    6.39  by (induct xs) auto
    6.40  
    6.41 -lemma size_multiset_of [simp]: "size (multiset_of xs) = length xs"
    6.42 +lemma size_mset [simp]: "size (mset xs) = length xs"
    6.43    by (induct xs) simp_all
    6.44  
    6.45 -lemma multiset_of_append [simp]:
    6.46 -  "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
    6.47 +lemma mset_append [simp]:
    6.48 +  "mset (xs @ ys) = mset xs + mset ys"
    6.49    by (induct xs arbitrary: ys) (auto simp: ac_simps)
    6.50  
    6.51 -lemma multiset_of_filter:
    6.52 -  "multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}"
    6.53 +lemma mset_filter:
    6.54 +  "mset (filter P xs) = {#x :# mset xs. P x #}"
    6.55    by (induct xs) simp_all
    6.56  
    6.57 -lemma multiset_of_rev [simp]:
    6.58 -  "multiset_of (rev xs) = multiset_of xs"
    6.59 +lemma mset_rev [simp]:
    6.60 +  "mset (rev xs) = mset xs"
    6.61    by (induct xs) simp_all
    6.62  
    6.63 -lemma surj_multiset_of: "surj multiset_of"
    6.64 +lemma surj_mset: "surj mset"
    6.65  apply (unfold surj_def)
    6.66  apply (rule allI)
    6.67  apply (rule_tac M = y in multiset_induct)
    6.68 @@ -1011,72 +1011,72 @@
    6.69  apply auto
    6.70  done
    6.71  
    6.72 -lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}"
    6.73 +lemma set_count_greater_0: "set x = {a. count (mset x) a > 0}"
    6.74  by (induct x) auto
    6.75  
    6.76  lemma distinct_count_atmost_1:
    6.77 -  "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
    6.78 +  "distinct x = (! a. count (mset x) a = (if a \<in> set x then 1 else 0))"
    6.79  apply (induct x, simp, rule iffI, simp_all)
    6.80  apply (rename_tac a b)
    6.81  apply (rule conjI)
    6.82 -apply (simp_all add: set_mset_multiset_of [THEN sym] del: set_mset_multiset_of)
    6.83 +apply (simp_all add: set_mset_mset [THEN sym] del: set_mset_mset)
    6.84  apply (erule_tac x = a in allE, simp, clarify)
    6.85  apply (erule_tac x = aa in allE, simp)
    6.86  done
    6.87  
    6.88 -lemma multiset_of_eq_setD:
    6.89 -  "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
    6.90 +lemma mset_eq_setD:
    6.91 +  "mset xs = mset ys \<Longrightarrow> set xs = set ys"
    6.92  by (rule) (auto simp add:multiset_eq_iff set_count_greater_0)
    6.93  
    6.94 -lemma set_eq_iff_multiset_of_eq_distinct:
    6.95 +lemma set_eq_iff_mset_eq_distinct:
    6.96    "distinct x \<Longrightarrow> distinct y \<Longrightarrow>
    6.97 -    (set x = set y) = (multiset_of x = multiset_of y)"
    6.98 +    (set x = set y) = (mset x = mset y)"
    6.99  by (auto simp: multiset_eq_iff distinct_count_atmost_1)
   6.100  
   6.101 -lemma set_eq_iff_multiset_of_remdups_eq:
   6.102 -   "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
   6.103 +lemma set_eq_iff_mset_remdups_eq:
   6.104 +   "(set x = set y) = (mset (remdups x) = mset (remdups y))"
   6.105  apply (rule iffI)
   6.106 -apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1])
   6.107 +apply (simp add: set_eq_iff_mset_eq_distinct[THEN iffD1])
   6.108  apply (drule distinct_remdups [THEN distinct_remdups
   6.109 -      [THEN set_eq_iff_multiset_of_eq_distinct [THEN iffD2]]])
   6.110 +      [THEN set_eq_iff_mset_eq_distinct [THEN iffD2]]])
   6.111  apply simp
   6.112  done
   6.113  
   6.114 -lemma multiset_of_compl_union [simp]:
   6.115 -  "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
   6.116 +lemma mset_compl_union [simp]:
   6.117 +  "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
   6.118    by (induct xs) (auto simp: ac_simps)
   6.119  
   6.120 -lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
   6.121 +lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) :# mset ls"
   6.122  apply (induct ls arbitrary: i)
   6.123   apply simp
   6.124  apply (case_tac i)
   6.125   apply auto
   6.126  done
   6.127  
   6.128 -lemma multiset_of_remove1[simp]:
   6.129 -  "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
   6.130 +lemma mset_remove1[simp]:
   6.131 +  "mset (remove1 a xs) = mset xs - {#a#}"
   6.132  by (induct xs) (auto simp add: multiset_eq_iff)
   6.133  
   6.134 -lemma multiset_of_eq_length:
   6.135 -  assumes "multiset_of xs = multiset_of ys"
   6.136 +lemma mset_eq_length:
   6.137 +  assumes "mset xs = mset ys"
   6.138    shows "length xs = length ys"
   6.139 -  using assms by (metis size_multiset_of)
   6.140 -
   6.141 -lemma multiset_of_eq_length_filter:
   6.142 -  assumes "multiset_of xs = multiset_of ys"
   6.143 +  using assms by (metis size_mset)
   6.144 +
   6.145 +lemma mset_eq_length_filter:
   6.146 +  assumes "mset xs = mset ys"
   6.147    shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)"
   6.148 -  using assms by (metis count_multiset_of)
   6.149 +  using assms by (metis count_mset)
   6.150  
   6.151  lemma fold_multiset_equiv:
   6.152    assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
   6.153 -    and equiv: "multiset_of xs = multiset_of ys"
   6.154 +    and equiv: "mset xs = mset ys"
   6.155    shows "List.fold f xs = List.fold f ys"
   6.156  using f equiv [symmetric]
   6.157  proof (induct xs arbitrary: ys)
   6.158    case Nil then show ?case by simp
   6.159  next
   6.160    case (Cons x xs)
   6.161 -  then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
   6.162 +  then have *: "set ys = set (x # xs)" by (blast dest: mset_eq_setD)
   6.163    have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
   6.164      by (rule Cons.prems(1)) (simp_all add: *)
   6.165    moreover from * have "x \<in> set ys" by simp
   6.166 @@ -1085,12 +1085,12 @@
   6.167    ultimately show ?case by simp
   6.168  qed
   6.169  
   6.170 -lemma multiset_of_insort [simp]:
   6.171 -  "multiset_of (insort x xs) = multiset_of xs + {#x#}"
   6.172 +lemma mset_insort [simp]:
   6.173 +  "mset (insort x xs) = mset xs + {#x#}"
   6.174    by (induct xs) (simp_all add: ac_simps)
   6.175  
   6.176 -lemma multiset_of_map:
   6.177 -  "multiset_of (map f xs) = image_mset f (multiset_of xs)"
   6.178 +lemma mset_map:
   6.179 +  "mset (map f xs) = image_mset f (mset xs)"
   6.180    by (induct xs) simp_all
   6.181  
   6.182  definition mset_set :: "'a set \<Rightarrow> 'a multiset"
   6.183 @@ -1154,12 +1154,12 @@
   6.184  
   6.185  end
   6.186  
   6.187 -lemma multiset_of_sorted_list_of_multiset [simp]:
   6.188 -  "multiset_of (sorted_list_of_multiset M) = M"
   6.189 +lemma mset_sorted_list_of_multiset [simp]:
   6.190 +  "mset (sorted_list_of_multiset M) = M"
   6.191  by (induct M) simp_all
   6.192  
   6.193 -lemma sorted_list_of_multiset_multiset_of [simp]:
   6.194 -  "sorted_list_of_multiset (multiset_of xs) = sort xs"
   6.195 +lemma sorted_list_of_multiset_mset [simp]:
   6.196 +  "sorted_list_of_multiset (mset xs) = sort xs"
   6.197  by (induct xs) simp_all
   6.198  
   6.199  lemma finite_set_mset_mset_set[simp]:
   6.200 @@ -1386,12 +1386,12 @@
   6.201  context linorder
   6.202  begin
   6.203  
   6.204 -lemma multiset_of_insort [simp]:
   6.205 -  "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs"
   6.206 +lemma mset_insort [simp]:
   6.207 +  "mset (insort_key k x xs) = {#x#} + mset xs"
   6.208    by (induct xs) (simp_all add: ac_simps)
   6.209  
   6.210 -lemma multiset_of_sort [simp]:
   6.211 -  "multiset_of (sort_key k xs) = multiset_of xs"
   6.212 +lemma mset_sort [simp]:
   6.213 +  "mset (sort_key k xs) = mset xs"
   6.214    by (induct xs) (simp_all add: ac_simps)
   6.215  
   6.216  text \<open>
   6.217 @@ -1400,7 +1400,7 @@
   6.218  \<close>
   6.219  
   6.220  lemma properties_for_sort_key:
   6.221 -  assumes "multiset_of ys = multiset_of xs"
   6.222 +  assumes "mset ys = mset xs"
   6.223    and "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs"
   6.224    and "sorted (map f ys)"
   6.225    shows "sort_key f xs = ys"
   6.226 @@ -1420,14 +1420,14 @@
   6.227  qed
   6.228  
   6.229  lemma properties_for_sort:
   6.230 -  assumes multiset: "multiset_of ys = multiset_of xs"
   6.231 +  assumes multiset: "mset ys = mset xs"
   6.232    and "sorted ys"
   6.233    shows "sort xs = ys"
   6.234  proof (rule properties_for_sort_key)
   6.235 -  from multiset show "multiset_of ys = multiset_of xs" .
   6.236 +  from multiset show "mset ys = mset xs" .
   6.237    from \<open>sorted ys\<close> show "sorted (map (\<lambda>x. x) ys)" by simp
   6.238    from multiset have "\<And>k. length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)"
   6.239 -    by (rule multiset_of_eq_length_filter)
   6.240 +    by (rule mset_eq_length_filter)
   6.241    then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k"
   6.242      by simp
   6.243    then show "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs"
   6.244 @@ -1439,8 +1439,8 @@
   6.245      @ [x\<leftarrow>xs. f x = f (xs ! (length xs div 2))]
   6.246      @ sort_key f [x\<leftarrow>xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs")
   6.247  proof (rule properties_for_sort_key)
   6.248 -  show "multiset_of ?rhs = multiset_of ?lhs"
   6.249 -    by (rule multiset_eqI) (auto simp add: multiset_of_filter)
   6.250 +  show "mset ?rhs = mset ?lhs"
   6.251 +    by (rule multiset_eqI) (auto simp add: mset_filter)
   6.252  next
   6.253    show "sorted (map f ?rhs)"
   6.254      by (auto simp add: sorted_append intro: sorted_map_same)
   6.255 @@ -1523,11 +1523,11 @@
   6.256  
   6.257  hide_const (open) part
   6.258  
   6.259 -lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
   6.260 +lemma mset_remdups_le: "mset (remdups xs) \<le># mset xs"
   6.261    by (induct xs) (auto intro: subset_mset.order_trans)
   6.262  
   6.263 -lemma multiset_of_update:
   6.264 -  "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
   6.265 +lemma mset_update:
   6.266 +  "i < length ls \<Longrightarrow> mset (ls[i := v]) = mset ls - {#ls ! i#} + {#v#}"
   6.267  proof (induct ls arbitrary: i)
   6.268    case Nil then show ?case by simp
   6.269  next
   6.270 @@ -1544,15 +1544,15 @@
   6.271        apply (subst add.assoc [symmetric])
   6.272        apply simp
   6.273        apply (rule mset_le_multiset_union_diff_commute)
   6.274 -      apply (simp add: mset_le_single nth_mem_multiset_of)
   6.275 +      apply (simp add: mset_le_single nth_mem_mset)
   6.276        done
   6.277    qed
   6.278  qed
   6.279  
   6.280 -lemma multiset_of_swap:
   6.281 +lemma mset_swap:
   6.282    "i < length ls \<Longrightarrow> j < length ls \<Longrightarrow>
   6.283 -    multiset_of (ls[j := ls ! i, i := ls ! j]) = multiset_of ls"
   6.284 -  by (cases "i = j") (simp_all add: multiset_of_update nth_mem_multiset_of)
   6.285 +    mset (ls[j := ls ! i, i := ls ! j]) = mset ls"
   6.286 +  by (cases "i = j") (simp_all add: mset_update nth_mem_mset)
   6.287  
   6.288  
   6.289  subsection \<open>The multiset order\<close>
   6.290 @@ -2071,51 +2071,51 @@
   6.291  
   6.292  subsection \<open>Naive implementation using lists\<close>
   6.293  
   6.294 -code_datatype multiset_of
   6.295 +code_datatype mset
   6.296  
   6.297  lemma [code]:
   6.298 -  "{#} = multiset_of []"
   6.299 +  "{#} = mset []"
   6.300    by simp
   6.301  
   6.302  lemma [code]:
   6.303 -  "{#x#} = multiset_of [x]"
   6.304 +  "{#x#} = mset [x]"
   6.305    by simp
   6.306  
   6.307  lemma union_code [code]:
   6.308 -  "multiset_of xs + multiset_of ys = multiset_of (xs @ ys)"
   6.309 +  "mset xs + mset ys = mset (xs @ ys)"
   6.310    by simp
   6.311  
   6.312  lemma [code]:
   6.313 -  "image_mset f (multiset_of xs) = multiset_of (map f xs)"
   6.314 -  by (simp add: multiset_of_map)
   6.315 +  "image_mset f (mset xs) = mset (map f xs)"
   6.316 +  by (simp add: mset_map)
   6.317  
   6.318  lemma [code]:
   6.319 -  "filter_mset f (multiset_of xs) = multiset_of (filter f xs)"
   6.320 -  by (simp add: multiset_of_filter)
   6.321 +  "filter_mset f (mset xs) = mset (filter f xs)"
   6.322 +  by (simp add: mset_filter)
   6.323  
   6.324  lemma [code]:
   6.325 -  "multiset_of xs - multiset_of ys = multiset_of (fold remove1 ys xs)"
   6.326 +  "mset xs - mset ys = mset (fold remove1 ys xs)"
   6.327    by (rule sym, induct ys arbitrary: xs) (simp_all add: diff_add diff_right_commute)
   6.328  
   6.329  lemma [code]:
   6.330 -  "multiset_of xs #\<inter> multiset_of ys =
   6.331 -    multiset_of (snd (fold (\<lambda>x (ys, zs).
   6.332 +  "mset xs #\<inter> mset ys =
   6.333 +    mset (snd (fold (\<lambda>x (ys, zs).
   6.334        if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, [])))"
   6.335  proof -
   6.336 -  have "\<And>zs. multiset_of (snd (fold (\<lambda>x (ys, zs).
   6.337 +  have "\<And>zs. mset (snd (fold (\<lambda>x (ys, zs).
   6.338      if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, zs))) =
   6.339 -      (multiset_of xs #\<inter> multiset_of ys) + multiset_of zs"
   6.340 +      (mset xs #\<inter> mset ys) + mset zs"
   6.341      by (induct xs arbitrary: ys)
   6.342        (auto simp add: mem_set_multiset_eq inter_add_right1 inter_add_right2 ac_simps)
   6.343    then show ?thesis by simp
   6.344  qed
   6.345  
   6.346  lemma [code]:
   6.347 -  "multiset_of xs #\<union> multiset_of ys =
   6.348 -    multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
   6.349 +  "mset xs #\<union> mset ys =
   6.350 +    mset (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
   6.351  proof -
   6.352 -  have "\<And>zs. multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
   6.353 -      (multiset_of xs #\<union> multiset_of ys) + multiset_of zs"
   6.354 +  have "\<And>zs. mset (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
   6.355 +      (mset xs #\<union> mset ys) + mset zs"
   6.356      by (induct xs arbitrary: ys) (simp_all add: multiset_eq_iff)
   6.357    then show ?thesis by simp
   6.358  qed
   6.359 @@ -2123,26 +2123,26 @@
   6.360  declare in_multiset_in_set [code_unfold]
   6.361  
   6.362  lemma [code]:
   6.363 -  "count (multiset_of xs) x = fold (\<lambda>y. if x = y then Suc else id) xs 0"
   6.364 +  "count (mset xs) x = fold (\<lambda>y. if x = y then Suc else id) xs 0"
   6.365  proof -
   6.366 -  have "\<And>n. fold (\<lambda>y. if x = y then Suc else id) xs n = count (multiset_of xs) x + n"
   6.367 +  have "\<And>n. fold (\<lambda>y. if x = y then Suc else id) xs n = count (mset xs) x + n"
   6.368      by (induct xs) simp_all
   6.369    then show ?thesis by simp
   6.370  qed
   6.371  
   6.372 -declare set_mset_multiset_of [code]
   6.373 -
   6.374 -declare sorted_list_of_multiset_multiset_of [code]
   6.375 +declare set_mset_mset [code]
   6.376 +
   6.377 +declare sorted_list_of_multiset_mset [code]
   6.378  
   6.379  lemma [code]: -- \<open>not very efficient, but representation-ignorant!\<close>
   6.380 -  "mset_set A = multiset_of (sorted_list_of_set A)"
   6.381 +  "mset_set A = mset (sorted_list_of_set A)"
   6.382    apply (cases "finite A")
   6.383    apply simp_all
   6.384    apply (induct A rule: finite_induct)
   6.385    apply (simp_all add: add.commute)
   6.386    done
   6.387  
   6.388 -declare size_multiset_of [code]
   6.389 +declare size_mset [code]
   6.390  
   6.391  fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
   6.392    "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
   6.393 @@ -2150,9 +2150,9 @@
   6.394       None \<Rightarrow> None
   6.395     | Some (ys1,_,ys2) \<Rightarrow> ms_lesseq_impl xs (ys1 @ ys2))"
   6.396  
   6.397 -lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> multiset_of xs \<le># multiset_of ys) \<and>
   6.398 -  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> multiset_of xs <# multiset_of ys) \<and>
   6.399 -  (ms_lesseq_impl xs ys = Some False \<longrightarrow> multiset_of xs = multiset_of ys)"
   6.400 +lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> mset xs \<le># mset ys) \<and>
   6.401 +  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> mset xs <# mset ys) \<and>
   6.402 +  (ms_lesseq_impl xs ys = Some False \<longrightarrow> mset xs = mset ys)"
   6.403  proof (induct xs arbitrary: ys)
   6.404    case (Nil ys)
   6.405    show ?case by (auto simp: mset_less_empty_nonempty)
   6.406 @@ -2163,13 +2163,13 @@
   6.407      case None
   6.408      hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
   6.409      {
   6.410 -      assume "multiset_of (x # xs) \<le># multiset_of ys"
   6.411 +      assume "mset (x # xs) \<le># mset ys"
   6.412        from set_mset_mono[OF this] x have False by simp
   6.413      } note nle = this
   6.414      moreover
   6.415      {
   6.416 -      assume "multiset_of (x # xs) <# multiset_of ys"
   6.417 -      hence "multiset_of (x # xs) \<le># multiset_of ys" by auto
   6.418 +      assume "mset (x # xs) <# mset ys"
   6.419 +      hence "mset (x # xs) \<le># mset ys" by auto
   6.420        from nle[OF this] have False .
   6.421      }
   6.422      ultimately show ?thesis using None by auto
   6.423 @@ -2178,7 +2178,7 @@
   6.424      obtain ys1 y ys2 where res: "res = (ys1,y,ys2)" by (cases res, auto)
   6.425      note Some = Some[unfolded res]
   6.426      from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp
   6.427 -    hence id: "multiset_of ys = multiset_of (ys1 @ ys2) + {#x#}"
   6.428 +    hence id: "mset ys = mset (ys1 @ ys2) + {#x#}"
   6.429        by (auto simp: ac_simps)
   6.430      show ?thesis unfolding ms_lesseq_impl.simps
   6.431        unfolding Some option.simps split
   6.432 @@ -2188,10 +2188,10 @@
   6.433    qed
   6.434  qed
   6.435  
   6.436 -lemma [code]: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
   6.437 +lemma [code]: "mset xs \<le># mset ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
   6.438    using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
   6.439  
   6.440 -lemma [code]: "multiset_of xs <# multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
   6.441 +lemma [code]: "mset xs <# mset ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
   6.442    using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
   6.443  
   6.444  instantiation multiset :: (equal) equal
   6.445 @@ -2199,7 +2199,7 @@
   6.446  
   6.447  definition
   6.448    [code del]: "HOL.equal A (B :: 'a multiset) \<longleftrightarrow> A = B"
   6.449 -lemma [code]: "HOL.equal (multiset_of xs) (multiset_of ys) \<longleftrightarrow> ms_lesseq_impl xs ys = Some False"
   6.450 +lemma [code]: "HOL.equal (mset xs) (mset ys) \<longleftrightarrow> ms_lesseq_impl xs ys = Some False"
   6.451    unfolding equal_multiset_def
   6.452    using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
   6.453  
   6.454 @@ -2208,13 +2208,13 @@
   6.455  end
   6.456  
   6.457  lemma [code]:
   6.458 -  "msetsum (multiset_of xs) = listsum xs"
   6.459 +  "msetsum (mset xs) = listsum xs"
   6.460    by (induct xs) (simp_all add: add.commute)
   6.461  
   6.462  lemma [code]:
   6.463 -  "msetprod (multiset_of xs) = fold times xs 1"
   6.464 +  "msetprod (mset xs) = fold times xs 1"
   6.465  proof -
   6.466 -  have "\<And>x. fold times xs x = msetprod (multiset_of xs) * x"
   6.467 +  have "\<And>x. fold times xs x = msetprod (mset xs) * x"
   6.468      by (induct xs) (simp_all add: mult.assoc)
   6.469    then show ?thesis by simp
   6.470  qed
   6.471 @@ -2229,7 +2229,7 @@
   6.472  definition (in term_syntax)
   6.473    msetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
   6.474      \<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   6.475 -  [code_unfold]: "msetify xs = Code_Evaluation.valtermify multiset_of {\<cdot>} xs"
   6.476 +  [code_unfold]: "msetify xs = Code_Evaluation.valtermify mset {\<cdot>} xs"
   6.477  
   6.478  notation fcomp (infixl "\<circ>>" 60)
   6.479  notation scomp (infixl "\<circ>\<rightarrow>" 60)
   6.480 @@ -2264,12 +2264,12 @@
   6.481  subsection \<open>BNF setup\<close>
   6.482  
   6.483  definition rel_mset where
   6.484 -  "rel_mset R X Y \<longleftrightarrow> (\<exists>xs ys. multiset_of xs = X \<and> multiset_of ys = Y \<and> list_all2 R xs ys)"
   6.485 -
   6.486 -lemma multiset_of_zip_take_Cons_drop_twice:
   6.487 +  "rel_mset R X Y \<longleftrightarrow> (\<exists>xs ys. mset xs = X \<and> mset ys = Y \<and> list_all2 R xs ys)"
   6.488 +
   6.489 +lemma mset_zip_take_Cons_drop_twice:
   6.490    assumes "length xs = length ys" "j \<le> length xs"
   6.491 -  shows "multiset_of (zip (take j xs @ x # drop j xs) (take j ys @ y # drop j ys)) =
   6.492 -    multiset_of (zip xs ys) + {#(x, y)#}"
   6.493 +  shows "mset (zip (take j xs @ x # drop j xs) (take j ys @ y # drop j ys)) =
   6.494 +    mset (zip xs ys) + {#(x, y)#}"
   6.495  using assms
   6.496  proof (induct xs ys arbitrary: x y j rule: list_induct2)
   6.497    case Nil
   6.498 @@ -2288,17 +2288,17 @@
   6.499        by (case_tac j) simp
   6.500      hence "k \<le> length xs"
   6.501        using Cons.prems by auto
   6.502 -    hence "multiset_of (zip (take k xs @ x # drop k xs) (take k ys @ y # drop k ys)) =
   6.503 -      multiset_of (zip xs ys) + {#(x, y)#}"
   6.504 +    hence "mset (zip (take k xs @ x # drop k xs) (take k ys @ y # drop k ys)) =
   6.505 +      mset (zip xs ys) + {#(x, y)#}"
   6.506        by (rule Cons.hyps(2))
   6.507      thus ?thesis
   6.508        unfolding k by (auto simp: add.commute union_lcomm)
   6.509    qed
   6.510  qed
   6.511  
   6.512 -lemma ex_multiset_of_zip_left:
   6.513 -  assumes "length xs = length ys" "multiset_of xs' = multiset_of xs"
   6.514 -  shows "\<exists>ys'. length ys' = length xs' \<and> multiset_of (zip xs' ys') = multiset_of (zip xs ys)"
   6.515 +lemma ex_mset_zip_left:
   6.516 +  assumes "length xs = length ys" "mset xs' = mset xs"
   6.517 +  shows "\<exists>ys'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys)"
   6.518  using assms
   6.519  proof (induct xs ys arbitrary: xs' rule: list_induct2)
   6.520    case Nil
   6.521 @@ -2307,57 +2307,57 @@
   6.522  next
   6.523    case (Cons x xs y ys xs')
   6.524    obtain j where j_len: "j < length xs'" and nth_j: "xs' ! j = x"
   6.525 -    by (metis Cons.prems in_set_conv_nth list.set_intros(1) multiset_of_eq_setD)
   6.526 +    by (metis Cons.prems in_set_conv_nth list.set_intros(1) mset_eq_setD)
   6.527  
   6.528    def xsa \<equiv> "take j xs' @ drop (Suc j) xs'"
   6.529 -  have "multiset_of xs' = {#x#} + multiset_of xsa"
   6.530 +  have "mset xs' = {#x#} + mset xsa"
   6.531      unfolding xsa_def using j_len nth_j
   6.532      by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id Cons_nth_drop_Suc
   6.533 -      multiset_of.simps(2) union_code add.commute)
   6.534 -  hence ms_x: "multiset_of xsa = multiset_of xs"
   6.535 -    by (metis Cons.prems add.commute add_right_imp_eq multiset_of.simps(2))
   6.536 +      mset.simps(2) union_code add.commute)
   6.537 +  hence ms_x: "mset xsa = mset xs"
   6.538 +    by (metis Cons.prems add.commute add_right_imp_eq mset.simps(2))
   6.539    then obtain ysa where
   6.540 -    len_a: "length ysa = length xsa" and ms_a: "multiset_of (zip xsa ysa) = multiset_of (zip xs ys)"
   6.541 +    len_a: "length ysa = length xsa" and ms_a: "mset (zip xsa ysa) = mset (zip xs ys)"
   6.542      using Cons.hyps(2) by blast
   6.543  
   6.544    def ys' \<equiv> "take j ysa @ y # drop j ysa"
   6.545    have xs': "xs' = take j xsa @ x # drop j xsa"
   6.546      using ms_x j_len nth_j Cons.prems xsa_def
   6.547      by (metis append_eq_append_conv append_take_drop_id diff_Suc_Suc Cons_nth_drop_Suc length_Cons
   6.548 -      length_drop size_multiset_of)
   6.549 +      length_drop size_mset)
   6.550    have j_len': "j \<le> length xsa"
   6.551      using j_len xs' xsa_def
   6.552      by (metis add_Suc_right append_take_drop_id length_Cons length_append less_eq_Suc_le not_less)
   6.553    have "length ys' = length xs'"
   6.554      unfolding ys'_def using Cons.prems len_a ms_x
   6.555 -    by (metis add_Suc_right append_take_drop_id length_Cons length_append multiset_of_eq_length)
   6.556 -  moreover have "multiset_of (zip xs' ys') = multiset_of (zip (x # xs) (y # ys))"
   6.557 +    by (metis add_Suc_right append_take_drop_id length_Cons length_append mset_eq_length)
   6.558 +  moreover have "mset (zip xs' ys') = mset (zip (x # xs) (y # ys))"
   6.559      unfolding xs' ys'_def
   6.560 -    by (rule trans[OF multiset_of_zip_take_Cons_drop_twice])
   6.561 +    by (rule trans[OF mset_zip_take_Cons_drop_twice])
   6.562        (auto simp: len_a ms_a j_len' add.commute)
   6.563    ultimately show ?case
   6.564      by blast
   6.565  qed
   6.566  
   6.567  lemma list_all2_reorder_left_invariance:
   6.568 -  assumes rel: "list_all2 R xs ys" and ms_x: "multiset_of xs' = multiset_of xs"
   6.569 -  shows "\<exists>ys'. list_all2 R xs' ys' \<and> multiset_of ys' = multiset_of ys"
   6.570 +  assumes rel: "list_all2 R xs ys" and ms_x: "mset xs' = mset xs"
   6.571 +  shows "\<exists>ys'. list_all2 R xs' ys' \<and> mset ys' = mset ys"
   6.572  proof -
   6.573    have len: "length xs = length ys"
   6.574      using rel list_all2_conv_all_nth by auto
   6.575    obtain ys' where
   6.576 -    len': "length xs' = length ys'" and ms_xy: "multiset_of (zip xs' ys') = multiset_of (zip xs ys)"
   6.577 -    using len ms_x by (metis ex_multiset_of_zip_left)
   6.578 +    len': "length xs' = length ys'" and ms_xy: "mset (zip xs' ys') = mset (zip xs ys)"
   6.579 +    using len ms_x by (metis ex_mset_zip_left)
   6.580    have "list_all2 R xs' ys'"
   6.581 -    using assms(1) len' ms_xy unfolding list_all2_iff by (blast dest: multiset_of_eq_setD)
   6.582 -  moreover have "multiset_of ys' = multiset_of ys"
   6.583 -    using len len' ms_xy map_snd_zip multiset_of_map by metis
   6.584 +    using assms(1) len' ms_xy unfolding list_all2_iff by (blast dest: mset_eq_setD)
   6.585 +  moreover have "mset ys' = mset ys"
   6.586 +    using len len' ms_xy map_snd_zip mset_map by metis
   6.587    ultimately show ?thesis
   6.588      by blast
   6.589  qed
   6.590  
   6.591 -lemma ex_multiset_of: "\<exists>xs. multiset_of xs = X"
   6.592 -  by (induct X) (simp, metis multiset_of.simps(2))
   6.593 +lemma ex_mset: "\<exists>xs. mset xs = X"
   6.594 +  by (induct X) (simp, metis mset.simps(2))
   6.595  
   6.596  bnf "'a multiset"
   6.597    map: image_mset
   6.598 @@ -2403,19 +2403,19 @@
   6.599      unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
   6.600      apply (rule ext)+
   6.601      apply auto
   6.602 -     apply (rule_tac x = "multiset_of (zip xs ys)" in exI; auto)
   6.603 -        apply (metis list_all2_lengthD map_fst_zip multiset_of_map)
   6.604 +     apply (rule_tac x = "mset (zip xs ys)" in exI; auto)
   6.605 +        apply (metis list_all2_lengthD map_fst_zip mset_map)
   6.606         apply (auto simp: list_all2_iff)[1]
   6.607 -      apply (metis list_all2_lengthD map_snd_zip multiset_of_map)
   6.608 +      apply (metis list_all2_lengthD map_snd_zip mset_map)
   6.609       apply (auto simp: list_all2_iff)[1]
   6.610      apply (rename_tac XY)
   6.611 -    apply (cut_tac X = XY in ex_multiset_of)
   6.612 +    apply (cut_tac X = XY in ex_mset)
   6.613      apply (erule exE)
   6.614      apply (rename_tac xys)
   6.615      apply (rule_tac x = "map fst xys" in exI)
   6.616 -    apply (auto simp: multiset_of_map)
   6.617 +    apply (auto simp: mset_map)
   6.618      apply (rule_tac x = "map snd xys" in exI)
   6.619 -    apply (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
   6.620 +    apply (auto simp: mset_map list_all2I subset_eq zip_map_fst_snd)
   6.621      done
   6.622  next
   6.623    show "\<And>z. z \<in> set_mset {#} \<Longrightarrow> False"
     7.1 --- a/src/HOL/Library/Permutation.thy	Thu Jun 18 16:17:51 2015 +0200
     7.2 +++ b/src/HOL/Library/Permutation.thy	Fri Jun 19 15:55:22 2015 +0200
     7.3 @@ -120,7 +120,7 @@
     7.4    apply (blast intro: perm_append_swap)
     7.5    done
     7.6  
     7.7 -lemma multiset_of_eq_perm: "multiset_of xs = multiset_of ys \<longleftrightarrow> xs <~~> ys"
     7.8 +lemma mset_eq_perm: "mset xs = mset ys \<longleftrightarrow> xs <~~> ys"
     7.9    apply (rule iffI)
    7.10    apply (erule_tac [2] perm.induct)
    7.11    apply (simp_all add: union_ac)
    7.12 @@ -140,15 +140,15 @@
    7.13    apply simp
    7.14    done
    7.15  
    7.16 -lemma multiset_of_le_perm_append: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
    7.17 -  apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
    7.18 -  apply (insert surj_multiset_of)
    7.19 +lemma mset_le_perm_append: "mset xs \<le># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
    7.20 +  apply (auto simp: mset_eq_perm[THEN sym] mset_le_exists_conv)
    7.21 +  apply (insert surj_mset)
    7.22    apply (drule surjD)
    7.23    apply (blast intro: sym)+
    7.24    done
    7.25  
    7.26  lemma perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys"
    7.27 -  by (metis multiset_of_eq_perm multiset_of_eq_setD)
    7.28 +  by (metis mset_eq_perm mset_eq_setD)
    7.29  
    7.30  lemma perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys"
    7.31    apply (induct pred: perm)
     8.1 --- a/src/HOL/Library/Tree_Multiset.thy	Thu Jun 18 16:17:51 2015 +0200
     8.2 +++ b/src/HOL/Library/Tree_Multiset.thy	Fri Jun 19 15:55:22 2015 +0200
     8.3 @@ -26,10 +26,10 @@
     8.4  lemma mset_iff_set_tree: "x \<in># mset_tree t \<longleftrightarrow> x \<in> set_tree t"
     8.5  by(induction t arbitrary: x) auto
     8.6  
     8.7 -lemma multiset_of_preorder[simp]: "multiset_of (preorder t) = mset_tree t"
     8.8 +lemma mset_preorder[simp]: "mset (preorder t) = mset_tree t"
     8.9  by (induction t) (auto simp: ac_simps)
    8.10  
    8.11 -lemma multiset_of_inorder[simp]: "multiset_of (inorder t) = mset_tree t"
    8.12 +lemma mset_inorder[simp]: "mset (inorder t) = mset_tree t"
    8.13  by (induction t) (auto simp: ac_simps)
    8.14  
    8.15  lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
     9.1 --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Thu Jun 18 16:17:51 2015 +0200
     9.2 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Fri Jun 19 15:55:22 2015 +0200
     9.3 @@ -239,9 +239,9 @@
     9.4    assumes "t xs = t ys"
     9.5    shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
     9.6  proof -
     9.7 -  have "count (multiset_of xs) = count (multiset_of ys)"
     9.8 -    using assms by (simp add: fun_eq_iff count_multiset_of t_def)
     9.9 -  then have "xs <~~> ys" unfolding multiset_of_eq_perm count_inject .
    9.10 +  have "count (mset xs) = count (mset ys)"
    9.11 +    using assms by (simp add: fun_eq_iff count_mset t_def)
    9.12 +  then have "xs <~~> ys" unfolding mset_eq_perm count_inject .
    9.13    then show ?thesis by (rule permutation_Ex_bij)
    9.14  qed
    9.15  
    10.1 --- a/src/HOL/Proofs/Extraction/Euclid.thy	Thu Jun 18 16:17:51 2015 +0200
    10.2 +++ b/src/HOL/Proofs/Extraction/Euclid.thy	Fri Jun 19 15:55:22 2015 +0200
    10.3 @@ -123,7 +123,7 @@
    10.4    qed
    10.5  qed
    10.6  
    10.7 -lemma dvd_prod [iff]: "n dvd (PROD m\<Colon>nat:#multiset_of (n # ns). m)"
    10.8 +lemma dvd_prod [iff]: "n dvd (PROD m\<Colon>nat:#mset (n # ns). m)"
    10.9    by (simp add: msetprod_Un msetprod_singleton)
   10.10  
   10.11  definition all_prime :: "nat list \<Rightarrow> bool" where
   10.12 @@ -140,13 +140,13 @@
   10.13  
   10.14  lemma split_all_prime:
   10.15    assumes "all_prime ms" and "all_prime ns"
   10.16 -  shows "\<exists>qs. all_prime qs \<and> (PROD m\<Colon>nat:#multiset_of qs. m) =
   10.17 -    (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
   10.18 +  shows "\<exists>qs. all_prime qs \<and> (PROD m\<Colon>nat:#mset qs. m) =
   10.19 +    (PROD m\<Colon>nat:#mset ms. m) * (PROD m\<Colon>nat:#mset ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
   10.20  proof -
   10.21    from assms have "all_prime (ms @ ns)"
   10.22      by (simp add: all_prime_append)
   10.23 -  moreover from assms have "(PROD m\<Colon>nat:#multiset_of (ms @ ns). m) =
   10.24 -    (PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)"
   10.25 +  moreover from assms have "(PROD m\<Colon>nat:#mset (ms @ ns). m) =
   10.26 +    (PROD m\<Colon>nat:#mset ms. m) * (PROD m\<Colon>nat:#mset ns. m)"
   10.27      by (simp add: msetprod_Un)
   10.28    ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" ..
   10.29    then show ?thesis ..
   10.30 @@ -154,11 +154,11 @@
   10.31  
   10.32  lemma all_prime_nempty_g_one:
   10.33    assumes "all_prime ps" and "ps \<noteq> []"
   10.34 -  shows "Suc 0 < (PROD m\<Colon>nat:#multiset_of ps. m)"
   10.35 +  shows "Suc 0 < (PROD m\<Colon>nat:#mset ps. m)"
   10.36    using `ps \<noteq> []` `all_prime ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
   10.37      (simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
   10.38  
   10.39 -lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = n)"
   10.40 +lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#mset ps. m) = n)"
   10.41  proof (induct n rule: nat_wf_ind)
   10.42    case (1 n)
   10.43    from `Suc 0 < n`
   10.44 @@ -169,21 +169,21 @@
   10.45      assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
   10.46      then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n"
   10.47        and kn: "k < n" and nmk: "n = m * k" by iprover
   10.48 -    from mn and m have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = m" by (rule 1)
   10.49 -    then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(PROD m\<Colon>nat:#multiset_of ps1. m) = m"
   10.50 +    from mn and m have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#mset ps. m) = m" by (rule 1)
   10.51 +    then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(PROD m\<Colon>nat:#mset ps1. m) = m"
   10.52        by iprover
   10.53 -    from kn and k have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = k" by (rule 1)
   10.54 -    then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(PROD m\<Colon>nat:#multiset_of ps2. m) = k"
   10.55 +    from kn and k have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#mset ps. m) = k" by (rule 1)
   10.56 +    then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(PROD m\<Colon>nat:#mset ps2. m) = k"
   10.57        by iprover
   10.58      from `all_prime ps1` `all_prime ps2`
   10.59 -    have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) =
   10.60 -      (PROD m\<Colon>nat:#multiset_of ps1. m) * (PROD m\<Colon>nat:#multiset_of ps2. m)"
   10.61 +    have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#mset ps. m) =
   10.62 +      (PROD m\<Colon>nat:#mset ps1. m) * (PROD m\<Colon>nat:#mset ps2. m)"
   10.63        by (rule split_all_prime)
   10.64      with prod_ps1_m prod_ps2_k nmk show ?thesis by simp
   10.65    next
   10.66      assume "prime n" then have "all_prime [n]" by (simp add: all_prime_simps)
   10.67 -    moreover have "(PROD m\<Colon>nat:#multiset_of [n]. m) = n" by (simp add: msetprod_singleton)
   10.68 -    ultimately have "all_prime [n] \<and> (PROD m\<Colon>nat:#multiset_of [n]. m) = n" ..
   10.69 +    moreover have "(PROD m\<Colon>nat:#mset [n]. m) = n" by (simp add: msetprod_singleton)
   10.70 +    ultimately have "all_prime [n] \<and> (PROD m\<Colon>nat:#mset [n]. m) = n" ..
   10.71      then show ?thesis ..
   10.72    qed
   10.73  qed
   10.74 @@ -193,7 +193,7 @@
   10.75    shows "\<exists>p. prime p \<and> p dvd n"
   10.76  proof -
   10.77    from N obtain ps where "all_prime ps"
   10.78 -    and prod_ps: "n = (PROD m\<Colon>nat:#multiset_of ps. m)" using factor_exists
   10.79 +    and prod_ps: "n = (PROD m\<Colon>nat:#mset ps. m)" using factor_exists
   10.80      by simp iprover
   10.81    with N have "ps \<noteq> []"
   10.82      by (auto simp add: all_prime_nempty_g_one msetprod_empty)
    11.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Thu Jun 18 16:17:51 2015 +0200
    11.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Jun 19 15:55:22 2015 +0200
    11.3 @@ -338,8 +338,8 @@
    11.4    case True
    11.5    then have "\<And>x y. x \<in> set (remdups xs) \<Longrightarrow> y \<in> set (remdups xs) \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
    11.6      by (rule rsp_foldE)
    11.7 -  moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)"
    11.8 -    by (simp add: set_eq_iff_multiset_of_remdups_eq)
    11.9 +  moreover from assms have "mset (remdups xs) = mset (remdups ys)"
   11.10 +    by (simp add: set_eq_iff_mset_remdups_eq)
   11.11    ultimately have "fold f (remdups xs) = fold f (remdups ys)"
   11.12      by (rule fold_multiset_equiv)
   11.13    with True show ?thesis by (simp add: fold_once_fold_remdups)
    12.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jun 18 16:17:51 2015 +0200
    12.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Fri Jun 19 15:55:22 2015 +0200
    12.3 @@ -17,7 +17,7 @@
    12.4    "tokens [] = 0"
    12.5  | "tokens (x#xs) = x + tokens xs"
    12.6  
    12.7 -abbreviation (input) "bag_of \<equiv> multiset_of"
    12.8 +abbreviation (input) "bag_of \<equiv> mset"
    12.9  
   12.10  lemma setsum_fun_mono [rule_format]:
   12.11       "!!f :: nat=>nat.  
    13.1 --- a/src/HOL/ZF/LProd.thy	Thu Jun 18 16:17:51 2015 +0200
    13.2 +++ b/src/HOL/ZF/LProd.thy	Fri Jun 19 15:55:22 2015 +0200
    13.3 @@ -34,7 +34,7 @@
    13.4  lemma lprod_subset: "S \<subseteq> R \<Longrightarrow> lprod S \<subseteq> lprod R"
    13.5    by (auto intro: lprod_subset_elem)
    13.6  
    13.7 -lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (multiset_of as, multiset_of bs) \<in> mult R"
    13.8 +lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (mset as, mset bs) \<in> mult R"
    13.9  proof (induct as bs rule: lprod.induct)
   13.10    case (lprod_single a b)
   13.11    note step = one_step_implies_mult[
   13.12 @@ -43,9 +43,9 @@
   13.13  next
   13.14    case (lprod_list ah at bh bt a b)
   13.15    then have transR: "trans R" by auto
   13.16 -  have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
   13.17 +  have as: "mset (ah @ a # at) = mset (ah @ at) + {#a#}" (is "_ = ?ma + _")
   13.18      by (simp add: algebra_simps)
   13.19 -  have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
   13.20 +  have bs: "mset (bh @ b # bt) = mset (bh @ bt) + {#b#}" (is "_ = ?mb + _")
   13.21      by (simp add: algebra_simps)
   13.22    from lprod_list have "(?ma, ?mb) \<in> mult R"
   13.23      by auto
   13.24 @@ -86,9 +86,9 @@
   13.25    assumes wf_R: "wf R"
   13.26    shows "wf (lprod R)"
   13.27  proof -
   13.28 -  have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) multiset_of"
   13.29 +  have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) mset"
   13.30      by (auto simp add: lprod_implies_mult trans_trancl)
   13.31 -  note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="multiset_of", 
   13.32 +  note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="mset", 
   13.33      OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset]
   13.34    note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
   13.35    show ?thesis by (auto intro: lprod)
    14.1 --- a/src/HOL/ex/Bubblesort.thy	Thu Jun 18 16:17:51 2015 +0200
    14.2 +++ b/src/HOL/ex/Bubblesort.thy	Fri Jun 19 15:55:22 2015 +0200
    14.3 @@ -41,7 +41,7 @@
    14.4      by(auto simp: size_bubble_min dest!: bubble_minD_size split: list.splits if_splits)
    14.5  qed
    14.6  
    14.7 -lemma mset_bubble_min: "multiset_of (bubble_min xs) = multiset_of xs"
    14.8 +lemma mset_bubble_min: "mset (bubble_min xs) = mset xs"
    14.9  apply(induction xs rule: bubble_min.induct)
   14.10    apply simp
   14.11   apply simp
   14.12 @@ -49,19 +49,19 @@
   14.13  done
   14.14  
   14.15  lemma bubble_minD_mset:
   14.16 -  "bubble_min (xs) = ys \<Longrightarrow> multiset_of xs = multiset_of ys"
   14.17 +  "bubble_min (xs) = ys \<Longrightarrow> mset xs = mset ys"
   14.18  by(auto simp: mset_bubble_min)
   14.19  
   14.20  lemma mset_bubblesort:
   14.21 -  "multiset_of (bubblesort xs) = multiset_of xs"
   14.22 +  "mset (bubblesort xs) = mset xs"
   14.23  apply(induction xs rule: bubblesort.induct)
   14.24    apply simp
   14.25   apply simp
   14.26  by(auto split: list.splits if_splits dest: bubble_minD_mset)
   14.27 -  (metis add_eq_conv_ex mset_bubble_min multiset_of.simps(2))
   14.28 +  (metis add_eq_conv_ex mset_bubble_min mset.simps(2))
   14.29  
   14.30  lemma set_bubblesort: "set (bubblesort xs) = set xs"
   14.31 -by(rule mset_bubblesort[THEN multiset_of_eq_setD])
   14.32 +by(rule mset_bubblesort[THEN mset_eq_setD])
   14.33  
   14.34  lemma bubble_min_min: "bubble_min xs = y#ys \<Longrightarrow> z \<in> set ys \<Longrightarrow> y \<le> z"
   14.35  apply(induction xs arbitrary: y ys z rule: bubble_min.induct)
    15.1 --- a/src/HOL/ex/MergeSort.thy	Thu Jun 18 16:17:51 2015 +0200
    15.2 +++ b/src/HOL/ex/MergeSort.thy	Fri Jun 19 15:55:22 2015 +0200
    15.3 @@ -19,8 +19,8 @@
    15.4  | "merge xs [] = xs"
    15.5  | "merge [] ys = ys"
    15.6  
    15.7 -lemma multiset_of_merge [simp]:
    15.8 -  "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"
    15.9 +lemma mset_merge [simp]:
   15.10 +  "mset (merge xs ys) = mset xs + mset ys"
   15.11    by (induct xs ys rule: merge.induct) (simp_all add: ac_simps)
   15.12  
   15.13  lemma set_merge [simp]:
   15.14 @@ -42,14 +42,14 @@
   15.15    "sorted (msort xs)"
   15.16    by (induct xs rule: msort.induct) simp_all
   15.17  
   15.18 -lemma multiset_of_msort:
   15.19 -  "multiset_of (msort xs) = multiset_of xs"
   15.20 +lemma mset_msort:
   15.21 +  "mset (msort xs) = mset xs"
   15.22    by (induct xs rule: msort.induct)
   15.23 -    (simp_all, metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
   15.24 +    (simp_all, metis append_take_drop_id drop_Suc_Cons mset.simps(2) mset_append take_Suc_Cons)
   15.25  
   15.26  theorem msort_sort:
   15.27    "sort = msort"
   15.28 -  by (rule ext, rule properties_for_sort) (fact multiset_of_msort sorted_msort)+
   15.29 +  by (rule ext, rule properties_for_sort) (fact mset_msort sorted_msort)+
   15.30  
   15.31  end
   15.32  
    16.1 --- a/src/HOL/ex/Quicksort.thy	Thu Jun 18 16:17:51 2015 +0200
    16.2 +++ b/src/HOL/ex/Quicksort.thy	Fri Jun 19 15:55:22 2015 +0200
    16.3 @@ -21,7 +21,7 @@
    16.4    by (simp_all add: not_le)
    16.5  
    16.6  lemma quicksort_permutes [simp]:
    16.7 -  "multiset_of (quicksort xs) = multiset_of xs"
    16.8 +  "mset (quicksort xs) = mset xs"
    16.9    by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
   16.10  
   16.11  lemma set_quicksort [simp]: "set (quicksort xs) = set xs"