# HG changeset patch
# User nipkow
# Date 1434554480 -7200
# Node ID 12f58a22eb110d414622dbadb49b01fc606e12ed
# Parent  e726f88232d33d60c3be1077a96f2b56695c4bf3# Parent  d7ff0a1df90a59e24f55ec2ae32054ac8036d6ec
merged

diff -r e726f88232d3 -r 12f58a22eb11 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Wed Jun 17 15:15:52 2015 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Wed Jun 17 17:21:20 2015 +0200
@@ -2025,7 +2025,7 @@
 subsubsection {* Interpreting multisets as factorizations *}
 
 lemma (in monoid) mset_fmsetEx:
-  assumes elems: "\<And>X. X \<in> set_of Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
+  assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
   shows "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> fmset G cs = Cs"
 proof -
   have "\<exists>Cs'. Cs = multiset_of Cs'"
@@ -2062,7 +2062,7 @@
 qed
 
 lemma (in monoid) mset_wfactorsEx:
-  assumes elems: "\<And>X. X \<in> set_of Cs 
+  assumes elems: "\<And>X. X \<in> set_mset Cs 
                       \<Longrightarrow> \<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"
   shows "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = Cs"
 proof -
@@ -2171,7 +2171,7 @@
     fix X
     assume "count (fmset G as) X < count (fmset G bs) X"
     hence "0 < count (fmset G bs) X" by simp
-    hence "X \<in> set_of (fmset G bs)" by simp
+    hence "X \<in> set_mset (fmset G bs)" by simp
     hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
     hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct bs) auto
     from this obtain x
@@ -2595,8 +2595,8 @@
                fmset G cs = fmset G as #\<inter> fmset G bs"
   proof (intro mset_wfactorsEx)
     fix X
-    assume "X \<in> set_of (fmset G as #\<inter> fmset G bs)"
-    hence "X \<in> set_of (fmset G as)" by (simp add: multiset_inter_def)
+    assume "X \<in> set_mset (fmset G as #\<inter> fmset G bs)"
+    hence "X \<in> set_mset (fmset G as)" by (simp add: multiset_inter_def)
     hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
     hence "\<exists>x. X = assocs G x \<and> x \<in> set as" by (induct as) auto
     from this obtain x
@@ -2673,12 +2673,12 @@
                fmset G cs = (fmset G as - fmset G bs) + fmset G bs"
   proof (intro mset_wfactorsEx)
     fix X
-    assume "X \<in> set_of ((fmset G as - fmset G bs) + fmset G bs)"
-    hence "X \<in> set_of (fmset G as) \<or> X \<in> set_of (fmset G bs)"
+    assume "X \<in> set_mset ((fmset G as - fmset G bs) + fmset G bs)"
+    hence "X \<in> set_mset (fmset G as) \<or> X \<in> set_mset (fmset G bs)"
        by (cases "X :# fmset G bs", simp, simp)
     moreover
     {
-      assume "X \<in> set_of (fmset G as)"
+      assume "X \<in> set_mset (fmset G as)"
       hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
       hence "\<exists>x. x \<in> set as \<and> X = assocs G x" by (induct as) auto
       from this obtain x
@@ -2693,7 +2693,7 @@
     }
     moreover
     {
-      assume "X \<in> set_of (fmset G bs)"
+      assume "X \<in> set_mset (fmset G bs)"
       hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
       hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct as) auto
       from this obtain x
diff -r e726f88232d3 -r 12f58a22eb11 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Wed Jun 17 15:15:52 2015 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Wed Jun 17 17:21:20 2015 +0200
@@ -538,7 +538,7 @@
         unfolding Array.length_def subarray_def by (cases p, auto)
       with left_subarray_remains part_conds1 pivot_unchanged
       have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> Array.get h' a ! p"
-        by (simp, subst set_of_multiset_of[symmetric], simp)
+        by (simp, subst set_mset_multiset_of[symmetric], simp)
           (* -- These steps are the analogous for the right sublist \<dots> *)
       from quicksort_outer_remains [OF qs1] length_remains
       have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
@@ -549,7 +549,7 @@
         unfolding Array.length_def subarray_def by auto
       with right_subarray_remains part_conds2 pivot_unchanged
       have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> Array.get h' a ! p \<le> j"
-        by (simp, subst set_of_multiset_of[symmetric], simp)
+        by (simp, subst set_mset_multiset_of[symmetric], simp)
           (* -- Thirdly and finally, we show that the array is sorted
           following from the facts above. *)
       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'"
diff -r e726f88232d3 -r 12f58a22eb11 src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Wed Jun 17 15:15:52 2015 +0100
+++ b/src/HOL/Library/DAList_Multiset.thy	Wed Jun 17 17:21:20 2015 +0200
@@ -34,7 +34,7 @@
 
 lemma [code, code del]: "msetprod = msetprod" ..
 
-lemma [code, code del]: "set_of = set_of" ..
+lemma [code, code del]: "set_mset = set_mset" ..
 
 lemma [code, code del]: "sorted_list_of_multiset = sorted_list_of_multiset" ..
 
@@ -403,15 +403,15 @@
 qed
 
 
-lemma set_of_fold: "set_of A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _")
+lemma set_mset_fold: "set_mset A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _")
 proof -
   interpret comp_fun_commute ?f by default auto
   show ?thesis by (induct A) auto
 qed
 
-lemma set_of_Bag[code]:
-  "set_of (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (if n = 0 then (\<lambda>m. m) else insert a)) {} ms"
-  unfolding set_of_fold
+lemma set_mset_Bag[code]:
+  "set_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (if n = 0 then (\<lambda>m. m) else insert a)) {} ms"
+  unfolding set_mset_fold
 proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1])
   fix a n x
   show "(if n = 0 then \<lambda>m. m else insert a) x = (insert a ^^ n) x" (is "?l n = ?r n")
diff -r e726f88232d3 -r 12f58a22eb11 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Jun 17 15:15:52 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Jun 17 17:21:20 2015 +0200
@@ -549,37 +549,37 @@
 
 subsubsection {* Set of elements *}
 
-definition set_of :: "'a multiset => 'a set" where
-  "set_of M = {x. x :# M}"
-
-lemma set_of_empty [simp]: "set_of {#} = {}"
-by (simp add: set_of_def)
-
-lemma set_of_single [simp]: "set_of {#b#} = {b}"
-by (simp add: set_of_def)
-
-lemma set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N"
-by (auto simp add: set_of_def)
-
-lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
-by (auto simp add: set_of_def multiset_eq_iff)
-
-lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
-by (auto simp add: set_of_def)
-
-lemma set_of_filter [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}"
-by (auto simp add: set_of_def)
-
-lemma finite_set_of [iff]: "finite (set_of M)"
-  using count [of M] by (simp add: multiset_def set_of_def)
+definition set_mset :: "'a multiset => 'a set" where
+  "set_mset M = {x. x :# M}"
+
+lemma set_mset_empty [simp]: "set_mset {#} = {}"
+by (simp add: set_mset_def)
+
+lemma set_mset_single [simp]: "set_mset {#b#} = {b}"
+by (simp add: set_mset_def)
+
+lemma set_mset_union [simp]: "set_mset (M + N) = set_mset M \<union> set_mset N"
+by (auto simp add: set_mset_def)
+
+lemma set_mset_eq_empty_iff [simp]: "(set_mset M = {}) = (M = {#})"
+by (auto simp add: set_mset_def multiset_eq_iff)
+
+lemma mem_set_mset_iff [simp]: "(x \<in> set_mset M) = (x :# M)"
+by (auto simp add: set_mset_def)
+
+lemma set_mset_filter [simp]: "set_mset {# x:#M. P x #} = set_mset M \<inter> {x. P x}"
+by (auto simp add: set_mset_def)
+
+lemma finite_set_mset [iff]: "finite (set_mset M)"
+  using count [of M] by (simp add: multiset_def set_mset_def)
 
 lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
-  unfolding set_of_def[symmetric] by simp
-
-lemma set_of_mono: "A \<le># B \<Longrightarrow> set_of A \<subseteq> set_of B"
-  by (metis mset_leD subsetI mem_set_of_iff)
-
-lemma ball_set_of_iff: "(\<forall>x \<in> set_of M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
+  unfolding set_mset_def[symmetric] by simp
+
+lemma set_mset_mono: "A \<le># B \<Longrightarrow> set_mset A \<subseteq> set_mset B"
+  by (metis mset_leD subsetI mem_set_mset_iff)
+
+lemma ball_set_mset_iff: "(\<forall>x \<in> set_mset M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
   by auto
 
 
@@ -591,7 +591,7 @@
   by (auto simp: wcount_def add_mult_distrib)
 
 definition size_multiset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a multiset \<Rightarrow> nat" where
-  "size_multiset f M = setsum (wcount f M) (set_of M)"
+  "size_multiset f M = setsum (wcount f M) (set_mset M)"
 
 lemmas size_multiset_eq = size_multiset_def[unfolded wcount_def]
 
@@ -617,10 +617,10 @@
 by (simp add: size_multiset_overloaded_def)
 
 lemma setsum_wcount_Int:
-  "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_of N) = setsum (wcount f N) A"
+  "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_mset N) = setsum (wcount f N) A"
 apply (induct rule: finite_induct)
  apply simp
-apply (simp add: Int_insert_left set_of_def wcount_def)
+apply (simp add: Int_insert_left set_mset_def wcount_def)
 done
 
 lemma size_multiset_union [simp]:
@@ -772,7 +772,7 @@
 
 definition fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
 where
-  "fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)"
+  "fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_mset M)"
 
 lemma fold_mset_empty [simp]:
   "fold_mset f s {#} = s"
@@ -789,18 +789,18 @@
   interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (M + {#x#}) y"
     by (fact comp_fun_commute_funpow)
   show ?thesis
-  proof (cases "x \<in> set_of M")
+  proof (cases "x \<in> set_mset M")
     case False
     then have *: "count (M + {#x#}) x = 1" by simp
-    from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_of M) =
-      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_of M)"
+    from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_mset M) =
+      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_mset M)"
       by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
     with False * show ?thesis
       by (simp add: fold_mset_def del: count_union)
   next
     case True
-    def N \<equiv> "set_of M - {x}"
-    from N_def True have *: "set_of M = insert x N" "x \<notin> N" "finite N" by auto
+    def N \<equiv> "set_mset M - {x}"
+    from N_def True have *: "set_mset M = insert x N" "x \<notin> N" "finite N" by auto
     then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N =
       Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
       by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
@@ -884,8 +884,8 @@
   "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
   by simp
 
-lemma set_of_image_mset [simp]:
-  "set_of (image_mset f M) = image f (set_of M)"
+lemma set_mset_image_mset [simp]:
+  "set_mset (image_mset f M) = image f (set_mset M)"
   by (induct M) simp_all
 
 lemma size_image_mset [simp]:
@@ -927,8 +927,8 @@
   @{term "{#x+x|x:#M. x<c#}"}.
 *}
 
-lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_of M"
-  by (metis mem_set_of_iff set_of_image_mset)
+lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M"
+  by (metis mem_set_mset_iff set_mset_image_mset)
 
 functor image_mset: image_mset
 proof -
@@ -981,7 +981,7 @@
 lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
 by (induct x) auto
 
-lemma set_of_multiset_of[simp]: "set_of (multiset_of x) = set x"
+lemma set_mset_multiset_of[simp]: "set_mset (multiset_of x) = set x"
 by (induct x) auto
 
 lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
@@ -1019,7 +1019,7 @@
 apply (induct x, simp, rule iffI, simp_all)
 apply (rename_tac a b)
 apply (rule conjI)
-apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
+apply (simp_all add: set_mset_multiset_of [THEN sym] del: set_mset_multiset_of)
 apply (erule_tac x = a in allE, simp, clarify)
 apply (erule_tac x = aa in allE, simp)
 done
@@ -1046,10 +1046,6 @@
   "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
   by (induct xs) (auto simp: ac_simps)
 
-lemma count_multiset_of_length_filter:
-  "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
-  by (induct xs) auto
-
 lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
 apply (induct ls arbitrary: i)
  apply simp
@@ -1166,18 +1162,18 @@
   "sorted_list_of_multiset (multiset_of xs) = sort xs"
   by (induct xs) simp_all
 
-lemma finite_set_of_multiset_of_set:
+lemma finite_set_mset_multiset_of_set:
   assumes "finite A"
-  shows "set_of (multiset_of_set A) = A"
+  shows "set_mset (multiset_of_set A) = A"
   using assms by (induct A) simp_all
 
-lemma infinite_set_of_multiset_of_set:
+lemma infinite_set_mset_multiset_of_set:
   assumes "\<not> finite A"
-  shows "set_of (multiset_of_set A) = {}"
+  shows "set_mset (multiset_of_set A) = {}"
   using assms by simp
 
 lemma set_sorted_list_of_multiset [simp]:
-  "set (sorted_list_of_multiset M) = set_of M"
+  "set (sorted_list_of_multiset M) = set_mset M"
   by (induct M) (simp_all add: set_insort)
 
 lemma sorted_list_of_multiset_of_set [simp]:
@@ -1261,8 +1257,8 @@
   case empty then show ?case by simp
 next
   case (add M x) then show ?case
-    by (cases "x \<in> set_of M")
-      (simp_all del: mem_set_of_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
+    by (cases "x \<in> set_mset M")
+      (simp_all del: mem_set_mset_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
 qed
 
 
@@ -1271,7 +1267,7 @@
 
 notation (xsymbols) Union_mset ("\<Union>#_" [900] 900)
 
-lemma set_of_Union_mset[simp]: "set_of (\<Union># MM) = (\<Union>M \<in> set_of MM. set_of M)"
+lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
   by (induct MM) auto
 
 lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
@@ -1324,7 +1320,7 @@
   by (cases "finite A") (induct A rule: finite_induct, simp_all)
 
 lemma msetprod_multiplicity:
-  "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
+  "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_mset M)"
   by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
 
 end
@@ -1371,7 +1367,7 @@
 lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
   unfolding replicate_mset_def by (induct n) simp_all
 
-lemma set_of_replicate_mset_subset[simp]: "set_of (replicate_mset n x) = (if n = 0 then {} else {x})"
+lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})"
   by (auto split: if_splits)
 
 lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
@@ -1695,8 +1691,8 @@
 lemma mult_implies_one_step:
   "trans r ==> (M, N) \<in> mult r ==>
     \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
-    (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)"
-apply (unfold mult_def mult1_def set_of_def)
+    (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)"
+apply (unfold mult_def mult1_def set_mset_def)
 apply (erule converse_trancl_induct, clarify)
  apply (rule_tac x = M0 in exI, simp, clarify)
 apply (case_tac "a :# K")
@@ -1726,7 +1722,7 @@
 
 lemma one_step_implies_mult_aux:
   "trans r ==>
-    \<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r))
+    \<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r))
       --> (I + K, I + J) \<in> mult r"
 apply (induct_tac n, auto)
 apply (frule size_eq_Suc_imp_eq_union, clarify)
@@ -1735,10 +1731,10 @@
 apply (case_tac "J' = {#}")
  apply (simp add: mult_def)
  apply (rule r_into_trancl)
- apply (simp add: mult1_def set_of_def, blast)
+ apply (simp add: mult1_def set_mset_def, blast)
 txt {* Now we know @{term "J' \<noteq> {#}"}. *}
 apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
-apply (erule_tac P = "\<forall>k \<in> set_of K. P k" for P in rev_mp)
+apply (erule_tac P = "\<forall>k \<in> set_mset K. P k" for P in rev_mp)
 apply (erule ssubst)
 apply (simp add: Ball_def, auto)
 apply (subgoal_tac
@@ -1749,14 +1745,14 @@
 apply (simp (no_asm_use) add: add.assoc [symmetric] mult_def)
 apply (erule trancl_trans)
 apply (rule r_into_trancl)
-apply (simp add: mult1_def set_of_def)
+apply (simp add: mult1_def set_mset_def)
 apply (rule_tac x = a in exI)
 apply (rule_tac x = "I + J'" in exI)
 apply (simp add: ac_simps)
 done
 
 lemma one_step_implies_mult:
-  "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r
+  "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
     ==> (I + K, I + J) \<in> mult r"
 using one_step_implies_mult_aux by blast
 
@@ -1783,14 +1779,14 @@
       by (rule transI) simp
     moreover note MM
     ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
-      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
+      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
       by (rule mult_implies_one_step)
     then obtain I J K where "M = I + J" and "M = I + K"
-      and "J \<noteq> {#}" and "(\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})" by blast
-    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
-    have "finite (set_of K)" by simp
+      and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
+    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
+    have "finite (set_mset K)" by simp
     moreover note aux2
-    ultimately have "set_of K = {}"
+    ultimately have "set_mset K = {}"
       by (induct rule: finite_induct) (auto intro: order_less_trans)
     with aux1 show False by simp
   qed
@@ -1851,12 +1847,12 @@
 by (auto intro: wf_mult1 wf_trancl simp: mult_def)
 
 lemma smsI:
-  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
+  "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
   unfolding ms_strict_def
 by (rule one_step_implies_mult) (auto simp add: max_strict_def pair_less_def elim!:max_ext.cases)
 
 lemma wmsI:
-  "(set_of A, set_of B) \<in> max_strict \<or> A = {#} \<and> B = {#}
+  "(set_mset A, set_mset B) \<in> max_strict \<or> A = {#} \<and> B = {#}
   \<Longrightarrow> (Z + A, Z + B) \<in> ms_weak"
 unfolding ms_weak_def ms_strict_def
 by (auto simp add: pair_less_def max_strict_def elim!:max_ext.cases intro: one_step_implies_mult)
@@ -1872,7 +1868,7 @@
 
 lemma pw_leq_split:
   assumes "pw_leq X Y"
-  shows "\<exists>A B Z. X = A + Z \<and> Y = B + Z \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
+  shows "\<exists>A B Z. X = A + Z \<and> Y = B + Z \<and> ((set_mset A, set_mset B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
   using assms
 proof (induct)
   case pw_leq_empty thus ?case by auto
@@ -1880,7 +1876,7 @@
   case (pw_leq_step x y X Y)
   then obtain A B Z where
     [simp]: "X = A + Z" "Y = B + Z"
-      and 1[simp]: "(set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#})"
+      and 1[simp]: "(set_mset A, set_mset B) \<in> max_strict \<or> (B = {#} \<and> A = {#})"
     by auto
   from pw_leq_step have "x = y \<or> (x, y) \<in> pair_less"
     unfolding pair_leq_def by auto
@@ -1890,7 +1886,7 @@
     have
       "{#x#} + X = A + ({#y#}+Z)
       \<and> {#y#} + Y = B + ({#y#}+Z)
-      \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
+      \<and> ((set_mset A, set_mset B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
       by (auto simp: ac_simps)
     thus ?case by (intro exI)
   next
@@ -1900,7 +1896,7 @@
       "{#y#} + Y = ?B' + Z"
       by (auto simp add: ac_simps)
     moreover have
-      "(set_of ?A', set_of ?B') \<in> max_strict"
+      "(set_mset ?A', set_mset ?B') \<in> max_strict"
       using 1 A unfolding max_strict_def
       by (auto elim!: max_ext.cases)
     ultimately show ?thesis by blast
@@ -1909,22 +1905,22 @@
 
 lemma
   assumes pwleq: "pw_leq Z Z'"
-  shows ms_strictI: "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
-  and   ms_weakI1:  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
+  shows ms_strictI: "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
+  and   ms_weakI1:  "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
   and   ms_weakI2:  "(Z + {#}, Z' + {#}) \<in> ms_weak"
 proof -
   from pw_leq_split[OF pwleq]
   obtain A' B' Z''
     where [simp]: "Z = A' + Z''" "Z' = B' + Z''"
-    and mx_or_empty: "(set_of A', set_of B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
+    and mx_or_empty: "(set_mset A', set_mset B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
     by blast
   {
-    assume max: "(set_of A, set_of B) \<in> max_strict"
+    assume max: "(set_mset A, set_mset B) \<in> max_strict"
     from mx_or_empty
     have "(Z'' + (A + A'), Z'' + (B + B')) \<in> ms_strict"
     proof
-      assume max': "(set_of A', set_of B') \<in> max_strict"
-      with max have "(set_of (A + A'), set_of (B + B')) \<in> max_strict"
+      assume max': "(set_mset A', set_mset B') \<in> max_strict"
+      with max have "(set_mset (A + A'), set_mset (B + B')) \<in> max_strict"
         by (auto simp: max_strict_def intro: max_ext_additive)
       thus ?thesis by (rule smsI)
     next
@@ -1972,14 +1968,14 @@
       ORELSE (rtac @{thm pw_leq_lstep} i)
       ORELSE (rtac @{thm pw_leq_empty} i)
 
-  val set_of_simps = [@{thm set_of_empty}, @{thm set_of_single}, @{thm set_of_union},
+  val set_mset_simps = [@{thm set_mset_empty}, @{thm set_mset_single}, @{thm set_mset_union},
                       @{thm Un_insert_left}, @{thm Un_empty_left}]
 in
   ScnpReconstruct.multiset_setup (ScnpReconstruct.Multiset
   {
     msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv,
     mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
-    mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_of_simps,
+    mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_mset_simps,
     smsI'= @{thm ms_strictI}, wmsI2''= @{thm ms_weakI2}, wmsI1= @{thm ms_weakI1},
     reduction_pair= @{thm ms_reduction_pair}
   })
@@ -2136,7 +2132,7 @@
   then show ?thesis by simp
 qed
 
-declare set_of_multiset_of [code]
+declare set_mset_multiset_of [code]
 
 declare sorted_list_of_multiset_multiset_of [code]
 
@@ -2170,7 +2166,7 @@
     hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
     {
       assume "multiset_of (x # xs) \<le># multiset_of ys"
-      from set_of_mono[OF this] x have False by simp
+      from set_mset_mono[OF this] x have False by simp
     } note nle = this
     moreover
     {
@@ -2367,7 +2363,7 @@
 
 bnf "'a multiset"
   map: image_mset
-  sets: set_of
+  sets: set_mset
   bd: natLeq
   wits: "{#}"
   rel: rel_mset
@@ -2379,11 +2375,11 @@
     unfolding comp_def by (rule ext) (simp add: comp_def image_mset.compositionality)
 next
   fix X :: "'a multiset"
-  show "\<And>f g. (\<And>z. z \<in> set_of X \<Longrightarrow> f z = g z) \<Longrightarrow> image_mset f X = image_mset g X"
+  show "\<And>f g. (\<And>z. z \<in> set_mset X \<Longrightarrow> f z = g z) \<Longrightarrow> image_mset f X = image_mset g X"
     by (induct X, (simp (no_asm))+,
-      metis One_nat_def Un_iff count_single mem_set_of_iff set_of_union zero_less_Suc)
+      metis One_nat_def Un_iff count_single mem_set_mset_iff set_mset_union zero_less_Suc)
 next
-  show "\<And>f. set_of \<circ> image_mset f = op ` f \<circ> set_of"
+  show "\<And>f. set_mset \<circ> image_mset f = op ` f \<circ> set_mset"
     by auto
 next
   show "card_order natLeq"
@@ -2392,7 +2388,7 @@
   show "BNF_Cardinal_Arithmetic.cinfinite natLeq"
     by (rule natLeq_cinfinite)
 next
-  show "\<And>X. ordLeq3 (card_of (set_of X)) natLeq"
+  show "\<And>X. ordLeq3 (card_of (set_mset X)) natLeq"
     by transfer
       (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
 next
@@ -2404,8 +2400,8 @@
     by (auto intro: list_all2_trans)
 next
   show "\<And>R. rel_mset R =
-    (BNF_Def.Grp {x. set_of x \<subseteq> {(x, y). R x y}} (image_mset fst))\<inverse>\<inverse> OO
-    BNF_Def.Grp {x. set_of x \<subseteq> {(x, y). R x y}} (image_mset snd)"
+    (BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset fst))\<inverse>\<inverse> OO
+    BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset snd)"
     unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
     apply (rule ext)+
     apply auto
@@ -2424,7 +2420,7 @@
     apply (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
     done
 next
-  show "\<And>z. z \<in> set_of {#} \<Longrightarrow> False"
+  show "\<And>z. z \<in> set_mset {#} \<Longrightarrow> False"
     by auto
 qed
 
@@ -2444,10 +2440,10 @@
 assumes ab: "R a b" and MN: "rel_mset R M N"
 shows "rel_mset R (M + {#a#}) (N + {#b#})"
 proof-
-  {fix y assume "R a b" and "set_of y \<subseteq> {(x, y). R x y}"
+  {fix y assume "R a b" and "set_mset y \<subseteq> {(x, y). R x y}"
    hence "\<exists>ya. image_mset fst y + {#a#} = image_mset fst ya \<and>
                image_mset snd y + {#b#} = image_mset snd ya \<and>
-               set_of ya \<subseteq> {(x, y). R x y}"
+               set_mset ya \<subseteq> {(x, y). R x y}"
    apply(intro exI[of _ "y + {#(a,b)#}"]) by auto
   }
   thus ?thesis
@@ -2510,7 +2506,7 @@
 proof-
   obtain a where a: "a \<in># M" and fa: "f a = b"
   using multiset.set_map[of f M] unfolding assms
-  by (metis image_iff mem_set_of_iff union_single_eq_member)
+  by (metis image_iff mem_set_mset_iff union_single_eq_member)
   then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
   have "image_mset f M1 = N" using assms unfolding M fa[symmetric] by simp
   thus ?thesis using M fa by blast
@@ -2521,7 +2517,7 @@
 shows "\<exists>N1 b. N = N1 + {#b#} \<and> R a b \<and> rel_mset R M N1"
 proof-
   obtain K where KM: "image_mset fst K = M + {#a#}"
-  and KN: "image_mset snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
+  and KN: "image_mset snd K = N" and sK: "set_mset K \<subseteq> {(a, b). R a b}"
   using assms
   unfolding multiset.rel_compp_Grp Grp_def by auto
   obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
@@ -2539,7 +2535,7 @@
 shows "\<exists>M1 a. M = M1 + {#a#} \<and> R a b \<and> rel_mset R M1 N"
 proof-
   obtain K where KN: "image_mset snd K = N + {#b#}"
-  and KM: "image_mset fst K = M" and sK: "set_of K \<subseteq> {(a, b). R a b}"
+  and KM: "image_mset fst K = M" and sK: "set_mset K \<subseteq> {(a, b). R a b}"
   using assms
   unfolding multiset.rel_compp_Grp Grp_def by auto
   obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
diff -r e726f88232d3 -r 12f58a22eb11 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Wed Jun 17 15:15:52 2015 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Wed Jun 17 17:21:20 2015 +0200
@@ -47,14 +47,14 @@
     moreover
     assume "(M, M) \<in> mult {(x, y). x < y}"
     ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
-      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
+      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
       by (rule mult_implies_one_step)
     then obtain I J K where "M = I + J" and "M = I + K"
-      and "J \<noteq> {#}" and "(\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})" by blast
-    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
-    have "finite (set_of K)" by simp
+      and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
+    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
+    have "finite (set_mset K)" by simp
     moreover note aux2
-    ultimately have "set_of K = {}"
+    ultimately have "set_mset K = {}"
       by (induct rule: finite_induct)
        (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
     with aux1 show False by simp
diff -r e726f88232d3 -r 12f58a22eb11 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Wed Jun 17 15:15:52 2015 +0100
+++ b/src/HOL/Library/Permutation.thy	Wed Jun 17 17:21:20 2015 +0200
@@ -136,7 +136,7 @@
   apply (erule perm.trans)
   apply (rule perm_sym)
   apply (erule perm_remove)
-  apply (drule_tac f=set_of in arg_cong)
+  apply (drule_tac f=set_mset in arg_cong)
   apply simp
   done
 
diff -r e726f88232d3 -r 12f58a22eb11 src/HOL/Library/Tree_Multiset.thy
--- a/src/HOL/Library/Tree_Multiset.thy	Wed Jun 17 15:15:52 2015 +0100
+++ b/src/HOL/Library/Tree_Multiset.thy	Wed Jun 17 17:21:20 2015 +0200
@@ -14,7 +14,7 @@
 "mset_tree Leaf = {#}" |
 "mset_tree (Node l a r) = {#a#} + mset_tree l + mset_tree r"
 
-lemma set_of_mset_tree[simp]: "set_of (mset_tree t) = set_tree t"
+lemma set_mset_tree[simp]: "set_mset (mset_tree t) = set_tree t"
 by(induction t) auto
 
 lemma size_mset_tree[simp]: "size(mset_tree t) = size t"
diff -r e726f88232d3 -r 12f58a22eb11 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Jun 17 15:15:52 2015 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Jun 17 17:21:20 2015 +0200
@@ -37,67 +37,67 @@
 subsection {* unique factorization: multiset version *}
 
 lemma multiset_prime_factorization_exists [rule_format]: "n > 0 --> 
-    (EX M. (ALL (p::nat) : set_of M. prime p) & n = (PROD i :# M. i))"
+    (EX M. (ALL (p::nat) : set_mset M. prime p) & n = (PROD i :# M. i))"
 proof (rule nat_less_induct, clarify)
   fix n :: nat
-  assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_of M. prime p) & m = 
+  assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_mset M. prime p) & m = 
       (PROD i :# M. i))"
   assume "(n::nat) > 0"
   then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
     by arith
   moreover {
     assume "n = 1"
-    then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)" by auto
+    then have "(ALL p : set_mset {#}. prime p) & n = (PROD i :# {#}. i)" by auto
   } moreover {
     assume "n > 1" and "prime n"
-    then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
+    then have "(ALL p : set_mset {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
       by auto
   } moreover {
     assume "n > 1" and "~ prime n"
     with not_prime_eq_prod_nat
     obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
       by blast
-    with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
-        and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
+    with ih obtain Q R where "(ALL p : set_mset Q. prime p) & m = (PROD i:#Q. i)"
+        and "(ALL p: set_mset R. prime p) & k = (PROD i:#R. i)"
       by blast
-    then have "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
+    then have "(ALL p: set_mset (Q + R). prime p) & n = (PROD i :# Q + R. i)"
       by (auto simp add: n msetprod_Un)
-    then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
+    then have "EX M. (ALL p : set_mset M. prime p) & n = (PROD i :# M. i)"..
   }
-  ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)"
+  ultimately show "EX M. (ALL p : set_mset M. prime p) & n = (PROD i::nat:#M. i)"
     by blast
 qed
 
 lemma multiset_prime_factorization_unique_aux:
   fixes a :: nat
-  assumes "(ALL p : set_of M. prime p)" and
-    "(ALL p : set_of N. prime p)" and
+  assumes "(ALL p : set_mset M. prime p)" and
+    "(ALL p : set_mset N. prime p)" and
     "(PROD i :# M. i) dvd (PROD i:# N. i)"
   shows
     "count M a <= count N a"
 proof cases
-  assume M: "a : set_of M"
+  assume M: "a : set_mset M"
   with assms have a: "prime a" by auto
   with M have "a ^ count M a dvd (PROD i :# M. i)"
     by (auto simp add: msetprod_multiplicity)
   also have "... dvd (PROD i :# N. i)" by (rule assms)
-  also have "... = (PROD i : (set_of N). i ^ (count N i))"
+  also have "... = (PROD i : (set_mset N). i ^ (count N i))"
     by (simp add: msetprod_multiplicity)
-  also have "... = a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
+  also have "... = a^(count N a) * (PROD i : (set_mset N - {a}). i ^ (count N i))"
   proof (cases)
-    assume "a : set_of N"
-    then have b: "set_of N = {a} Un (set_of N - {a})"
+    assume "a : set_mset N"
+    then have b: "set_mset N = {a} Un (set_mset N - {a})"
       by auto
     then show ?thesis
       by (subst (1) b, subst setprod.union_disjoint, auto)
   next
-    assume "a ~: set_of N" 
+    assume "a ~: set_mset N" 
     then show ?thesis by auto
   qed
   finally have "a ^ count M a dvd 
-      a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
+      a^(count N a) * (PROD i : (set_mset N - {a}). i ^ (count N i))".
   moreover
-  have "coprime (a ^ count M a) (PROD i : (set_of N - {a}). i ^ (count N i))"
+  have "coprime (a ^ count M a) (PROD i : (set_mset N - {a}). i ^ (count N i))"
     apply (subst gcd_commute_nat)
     apply (rule setprod_coprime_nat)
     apply (rule primes_imp_powers_coprime_nat)
@@ -111,13 +111,13 @@
     apply auto
     done
 next
-  assume "a ~: set_of M"
+  assume "a ~: set_mset M"
   then show ?thesis by auto
 qed
 
 lemma multiset_prime_factorization_unique:
-  assumes "(ALL (p::nat) : set_of M. prime p)" and
-    "(ALL p : set_of N. prime p)" and
+  assumes "(ALL (p::nat) : set_mset M. prime p)" and
+    "(ALL p : set_mset N. prime p)" and
     "(PROD i :# M. i) = (PROD i:# N. i)"
   shows
     "M = N"
@@ -137,12 +137,12 @@
 definition multiset_prime_factorization :: "nat => nat multiset"
 where
   "multiset_prime_factorization n ==
-     if n > 0 then (THE M. ((ALL p : set_of M. prime p) & 
+     if n > 0 then (THE M. ((ALL p : set_mset M. prime p) & 
        n = (PROD i :# M. i)))
      else {#}"
 
 lemma multiset_prime_factorization: "n > 0 ==>
-    (ALL p : set_of (multiset_prime_factorization n). prime p) &
+    (ALL p : set_mset (multiset_prime_factorization n). prime p) &
        n = (PROD i :# (multiset_prime_factorization n). i)"
   apply (unfold multiset_prime_factorization_def)
   apply clarsimp
@@ -169,7 +169,7 @@
   where "multiplicity_nat p n = count (multiset_prime_factorization n) p"
 
 definition prime_factors_nat :: "nat \<Rightarrow> nat set"
-  where "prime_factors_nat n = set_of (multiset_prime_factorization n)"
+  where "prime_factors_nat n = set_mset (multiset_prime_factorization n)"
 
 instance ..
 
@@ -306,12 +306,12 @@
     apply force
     apply force
     using assms
-    apply (simp add: set_of_def msetprod_multiplicity)
+    apply (simp add: set_mset_def msetprod_multiplicity)
     done
   with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
     by simp
   with S_eq show ?thesis
-    by (simp add: set_of_def multiset_def prime_factors_nat_def multiplicity_nat_def)
+    by (simp add: set_mset_def multiset_def prime_factors_nat_def multiplicity_nat_def)
 qed
 
 lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
@@ -435,7 +435,7 @@
   apply (cases "n = 0")
   apply auto
   apply (frule multiset_prime_factorization)
-  apply (auto simp add: set_of_def multiplicity_nat_def)
+  apply (auto simp add: set_mset_def multiplicity_nat_def)
   done
 
 lemma multiplicity_not_factor_nat [simp]: 
diff -r e726f88232d3 -r 12f58a22eb11 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Jun 17 15:15:52 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Jun 17 17:21:20 2015 +0200
@@ -1413,7 +1413,7 @@
 lemma pmf_of_multiset[simp]: "pmf pmf_of_multiset x = count M x / size M"
   by transfer rule
 
-lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_of M"
+lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_mset M"
   by (auto simp: set_pmf_iff)
 
 end
diff -r e726f88232d3 -r 12f58a22eb11 src/HOL/ZF/LProd.thy
--- a/src/HOL/ZF/LProd.thy	Wed Jun 17 15:15:52 2015 +0100
+++ b/src/HOL/ZF/LProd.thy	Wed Jun 17 17:21:20 2015 +0200
@@ -50,10 +50,10 @@
   from lprod_list have "(?ma, ?mb) \<in> mult R"
     by auto
   with mult_implies_one_step[OF transR] have 
-    "\<exists>I J K. ?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> R)"
+    "\<exists>I J K. ?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> R)"
     by blast
   then obtain I J K where 
-    decomposed: "?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> R)"
+    decomposed: "?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> R)"
     by blast   
   show ?case
   proof (cases "a = b")