renamed Multiset.set_of to the canonical set_mset
authornipkow
Wed Jun 17 17:21:11 2015 +0200 (2015-06-17)
changeset 60495d7ff0a1df90a
parent 60492 db0f4f4c17c7
child 60496 12f58a22eb11
renamed Multiset.set_of to the canonical set_mset
src/HOL/Algebra/Divisibility.thy
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Multiset_Order.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/Tree_Multiset.thy
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/ZF/LProd.thy
     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Tue Jun 16 20:50:00 2015 +0100
     1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Wed Jun 17 17:21:11 2015 +0200
     1.3 @@ -2025,7 +2025,7 @@
     1.4  subsubsection {* Interpreting multisets as factorizations *}
     1.5  
     1.6  lemma (in monoid) mset_fmsetEx:
     1.7 -  assumes elems: "\<And>X. X \<in> set_of Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
     1.8 +  assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
     1.9    shows "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> fmset G cs = Cs"
    1.10  proof -
    1.11    have "\<exists>Cs'. Cs = multiset_of Cs'"
    1.12 @@ -2062,7 +2062,7 @@
    1.13  qed
    1.14  
    1.15  lemma (in monoid) mset_wfactorsEx:
    1.16 -  assumes elems: "\<And>X. X \<in> set_of Cs 
    1.17 +  assumes elems: "\<And>X. X \<in> set_mset Cs 
    1.18                        \<Longrightarrow> \<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"
    1.19    shows "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = Cs"
    1.20  proof -
    1.21 @@ -2171,7 +2171,7 @@
    1.22      fix X
    1.23      assume "count (fmset G as) X < count (fmset G bs) X"
    1.24      hence "0 < count (fmset G bs) X" by simp
    1.25 -    hence "X \<in> set_of (fmset G bs)" by simp
    1.26 +    hence "X \<in> set_mset (fmset G bs)" by simp
    1.27      hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
    1.28      hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct bs) auto
    1.29      from this obtain x
    1.30 @@ -2595,8 +2595,8 @@
    1.31                 fmset G cs = fmset G as #\<inter> fmset G bs"
    1.32    proof (intro mset_wfactorsEx)
    1.33      fix X
    1.34 -    assume "X \<in> set_of (fmset G as #\<inter> fmset G bs)"
    1.35 -    hence "X \<in> set_of (fmset G as)" by (simp add: multiset_inter_def)
    1.36 +    assume "X \<in> set_mset (fmset G as #\<inter> fmset G bs)"
    1.37 +    hence "X \<in> set_mset (fmset G as)" by (simp add: multiset_inter_def)
    1.38      hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
    1.39      hence "\<exists>x. X = assocs G x \<and> x \<in> set as" by (induct as) auto
    1.40      from this obtain x
    1.41 @@ -2673,12 +2673,12 @@
    1.42                 fmset G cs = (fmset G as - fmset G bs) + fmset G bs"
    1.43    proof (intro mset_wfactorsEx)
    1.44      fix X
    1.45 -    assume "X \<in> set_of ((fmset G as - fmset G bs) + fmset G bs)"
    1.46 -    hence "X \<in> set_of (fmset G as) \<or> X \<in> set_of (fmset G bs)"
    1.47 +    assume "X \<in> set_mset ((fmset G as - fmset G bs) + fmset G bs)"
    1.48 +    hence "X \<in> set_mset (fmset G as) \<or> X \<in> set_mset (fmset G bs)"
    1.49         by (cases "X :# fmset G bs", simp, simp)
    1.50      moreover
    1.51      {
    1.52 -      assume "X \<in> set_of (fmset G as)"
    1.53 +      assume "X \<in> set_mset (fmset G as)"
    1.54        hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
    1.55        hence "\<exists>x. x \<in> set as \<and> X = assocs G x" by (induct as) auto
    1.56        from this obtain x
    1.57 @@ -2693,7 +2693,7 @@
    1.58      }
    1.59      moreover
    1.60      {
    1.61 -      assume "X \<in> set_of (fmset G bs)"
    1.62 +      assume "X \<in> set_mset (fmset G bs)"
    1.63        hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
    1.64        hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct as) auto
    1.65        from this obtain x
     2.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jun 16 20:50:00 2015 +0100
     2.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Wed Jun 17 17:21:11 2015 +0200
     2.3 @@ -538,7 +538,7 @@
     2.4          unfolding Array.length_def subarray_def by (cases p, auto)
     2.5        with left_subarray_remains part_conds1 pivot_unchanged
     2.6        have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> Array.get h' a ! p"
     2.7 -        by (simp, subst set_of_multiset_of[symmetric], simp)
     2.8 +        by (simp, subst set_mset_multiset_of[symmetric], simp)
     2.9            (* -- These steps are the analogous for the right sublist \<dots> *)
    2.10        from quicksort_outer_remains [OF qs1] length_remains
    2.11        have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
    2.12 @@ -549,7 +549,7 @@
    2.13          unfolding Array.length_def subarray_def by auto
    2.14        with right_subarray_remains part_conds2 pivot_unchanged
    2.15        have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> Array.get h' a ! p \<le> j"
    2.16 -        by (simp, subst set_of_multiset_of[symmetric], simp)
    2.17 +        by (simp, subst set_mset_multiset_of[symmetric], simp)
    2.18            (* -- Thirdly and finally, we show that the array is sorted
    2.19            following from the facts above. *)
    2.20        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'"
     3.1 --- a/src/HOL/Library/DAList_Multiset.thy	Tue Jun 16 20:50:00 2015 +0100
     3.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Wed Jun 17 17:21:11 2015 +0200
     3.3 @@ -34,7 +34,7 @@
     3.4  
     3.5  lemma [code, code del]: "msetprod = msetprod" ..
     3.6  
     3.7 -lemma [code, code del]: "set_of = set_of" ..
     3.8 +lemma [code, code del]: "set_mset = set_mset" ..
     3.9  
    3.10  lemma [code, code del]: "sorted_list_of_multiset = sorted_list_of_multiset" ..
    3.11  
    3.12 @@ -403,15 +403,15 @@
    3.13  qed
    3.14  
    3.15  
    3.16 -lemma set_of_fold: "set_of A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _")
    3.17 +lemma set_mset_fold: "set_mset A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _")
    3.18  proof -
    3.19    interpret comp_fun_commute ?f by default auto
    3.20    show ?thesis by (induct A) auto
    3.21  qed
    3.22  
    3.23 -lemma set_of_Bag[code]:
    3.24 -  "set_of (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (if n = 0 then (\<lambda>m. m) else insert a)) {} ms"
    3.25 -  unfolding set_of_fold
    3.26 +lemma set_mset_Bag[code]:
    3.27 +  "set_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (if n = 0 then (\<lambda>m. m) else insert a)) {} ms"
    3.28 +  unfolding set_mset_fold
    3.29  proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1])
    3.30    fix a n x
    3.31    show "(if n = 0 then \<lambda>m. m else insert a) x = (insert a ^^ n) x" (is "?l n = ?r n")
     4.1 --- a/src/HOL/Library/Multiset.thy	Tue Jun 16 20:50:00 2015 +0100
     4.2 +++ b/src/HOL/Library/Multiset.thy	Wed Jun 17 17:21:11 2015 +0200
     4.3 @@ -549,37 +549,37 @@
     4.4  
     4.5  subsubsection {* Set of elements *}
     4.6  
     4.7 -definition set_of :: "'a multiset => 'a set" where
     4.8 -  "set_of M = {x. x :# M}"
     4.9 -
    4.10 -lemma set_of_empty [simp]: "set_of {#} = {}"
    4.11 -by (simp add: set_of_def)
    4.12 -
    4.13 -lemma set_of_single [simp]: "set_of {#b#} = {b}"
    4.14 -by (simp add: set_of_def)
    4.15 -
    4.16 -lemma set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N"
    4.17 -by (auto simp add: set_of_def)
    4.18 -
    4.19 -lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
    4.20 -by (auto simp add: set_of_def multiset_eq_iff)
    4.21 -
    4.22 -lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
    4.23 -by (auto simp add: set_of_def)
    4.24 -
    4.25 -lemma set_of_filter [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}"
    4.26 -by (auto simp add: set_of_def)
    4.27 -
    4.28 -lemma finite_set_of [iff]: "finite (set_of M)"
    4.29 -  using count [of M] by (simp add: multiset_def set_of_def)
    4.30 +definition set_mset :: "'a multiset => 'a set" where
    4.31 +  "set_mset M = {x. x :# M}"
    4.32 +
    4.33 +lemma set_mset_empty [simp]: "set_mset {#} = {}"
    4.34 +by (simp add: set_mset_def)
    4.35 +
    4.36 +lemma set_mset_single [simp]: "set_mset {#b#} = {b}"
    4.37 +by (simp add: set_mset_def)
    4.38 +
    4.39 +lemma set_mset_union [simp]: "set_mset (M + N) = set_mset M \<union> set_mset N"
    4.40 +by (auto simp add: set_mset_def)
    4.41 +
    4.42 +lemma set_mset_eq_empty_iff [simp]: "(set_mset M = {}) = (M = {#})"
    4.43 +by (auto simp add: set_mset_def multiset_eq_iff)
    4.44 +
    4.45 +lemma mem_set_mset_iff [simp]: "(x \<in> set_mset M) = (x :# M)"
    4.46 +by (auto simp add: set_mset_def)
    4.47 +
    4.48 +lemma set_mset_filter [simp]: "set_mset {# x:#M. P x #} = set_mset M \<inter> {x. P x}"
    4.49 +by (auto simp add: set_mset_def)
    4.50 +
    4.51 +lemma finite_set_mset [iff]: "finite (set_mset M)"
    4.52 +  using count [of M] by (simp add: multiset_def set_mset_def)
    4.53  
    4.54  lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
    4.55 -  unfolding set_of_def[symmetric] by simp
    4.56 -
    4.57 -lemma set_of_mono: "A \<le># B \<Longrightarrow> set_of A \<subseteq> set_of B"
    4.58 -  by (metis mset_leD subsetI mem_set_of_iff)
    4.59 -
    4.60 -lemma ball_set_of_iff: "(\<forall>x \<in> set_of M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
    4.61 +  unfolding set_mset_def[symmetric] by simp
    4.62 +
    4.63 +lemma set_mset_mono: "A \<le># B \<Longrightarrow> set_mset A \<subseteq> set_mset B"
    4.64 +  by (metis mset_leD subsetI mem_set_mset_iff)
    4.65 +
    4.66 +lemma ball_set_mset_iff: "(\<forall>x \<in> set_mset M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
    4.67    by auto
    4.68  
    4.69  
    4.70 @@ -591,7 +591,7 @@
    4.71    by (auto simp: wcount_def add_mult_distrib)
    4.72  
    4.73  definition size_multiset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a multiset \<Rightarrow> nat" where
    4.74 -  "size_multiset f M = setsum (wcount f M) (set_of M)"
    4.75 +  "size_multiset f M = setsum (wcount f M) (set_mset M)"
    4.76  
    4.77  lemmas size_multiset_eq = size_multiset_def[unfolded wcount_def]
    4.78  
    4.79 @@ -617,10 +617,10 @@
    4.80  by (simp add: size_multiset_overloaded_def)
    4.81  
    4.82  lemma setsum_wcount_Int:
    4.83 -  "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_of N) = setsum (wcount f N) A"
    4.84 +  "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_mset N) = setsum (wcount f N) A"
    4.85  apply (induct rule: finite_induct)
    4.86   apply simp
    4.87 -apply (simp add: Int_insert_left set_of_def wcount_def)
    4.88 +apply (simp add: Int_insert_left set_mset_def wcount_def)
    4.89  done
    4.90  
    4.91  lemma size_multiset_union [simp]:
    4.92 @@ -772,7 +772,7 @@
    4.93  
    4.94  definition fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
    4.95  where
    4.96 -  "fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)"
    4.97 +  "fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_mset M)"
    4.98  
    4.99  lemma fold_mset_empty [simp]:
   4.100    "fold_mset f s {#} = s"
   4.101 @@ -789,18 +789,18 @@
   4.102    interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (M + {#x#}) y"
   4.103      by (fact comp_fun_commute_funpow)
   4.104    show ?thesis
   4.105 -  proof (cases "x \<in> set_of M")
   4.106 +  proof (cases "x \<in> set_mset M")
   4.107      case False
   4.108      then have *: "count (M + {#x#}) x = 1" by simp
   4.109 -    from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_of M) =
   4.110 -      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_of M)"
   4.111 +    from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_mset M) =
   4.112 +      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_mset M)"
   4.113        by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
   4.114      with False * show ?thesis
   4.115        by (simp add: fold_mset_def del: count_union)
   4.116    next
   4.117      case True
   4.118 -    def N \<equiv> "set_of M - {x}"
   4.119 -    from N_def True have *: "set_of M = insert x N" "x \<notin> N" "finite N" by auto
   4.120 +    def N \<equiv> "set_mset M - {x}"
   4.121 +    from N_def True have *: "set_mset M = insert x N" "x \<notin> N" "finite N" by auto
   4.122      then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N =
   4.123        Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
   4.124        by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
   4.125 @@ -884,8 +884,8 @@
   4.126    "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
   4.127    by simp
   4.128  
   4.129 -lemma set_of_image_mset [simp]:
   4.130 -  "set_of (image_mset f M) = image f (set_of M)"
   4.131 +lemma set_mset_image_mset [simp]:
   4.132 +  "set_mset (image_mset f M) = image f (set_mset M)"
   4.133    by (induct M) simp_all
   4.134  
   4.135  lemma size_image_mset [simp]:
   4.136 @@ -927,8 +927,8 @@
   4.137    @{term "{#x+x|x:#M. x<c#}"}.
   4.138  *}
   4.139  
   4.140 -lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_of M"
   4.141 -  by (metis mem_set_of_iff set_of_image_mset)
   4.142 +lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M"
   4.143 +  by (metis mem_set_mset_iff set_mset_image_mset)
   4.144  
   4.145  functor image_mset: image_mset
   4.146  proof -
   4.147 @@ -981,7 +981,7 @@
   4.148  lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
   4.149  by (induct x) auto
   4.150  
   4.151 -lemma set_of_multiset_of[simp]: "set_of (multiset_of x) = set x"
   4.152 +lemma set_mset_multiset_of[simp]: "set_mset (multiset_of x) = set x"
   4.153  by (induct x) auto
   4.154  
   4.155  lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
   4.156 @@ -1019,7 +1019,7 @@
   4.157  apply (induct x, simp, rule iffI, simp_all)
   4.158  apply (rename_tac a b)
   4.159  apply (rule conjI)
   4.160 -apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
   4.161 +apply (simp_all add: set_mset_multiset_of [THEN sym] del: set_mset_multiset_of)
   4.162  apply (erule_tac x = a in allE, simp, clarify)
   4.163  apply (erule_tac x = aa in allE, simp)
   4.164  done
   4.165 @@ -1046,10 +1046,6 @@
   4.166    "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
   4.167    by (induct xs) (auto simp: ac_simps)
   4.168  
   4.169 -lemma count_multiset_of_length_filter:
   4.170 -  "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
   4.171 -  by (induct xs) auto
   4.172 -
   4.173  lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
   4.174  apply (induct ls arbitrary: i)
   4.175   apply simp
   4.176 @@ -1166,18 +1162,18 @@
   4.177    "sorted_list_of_multiset (multiset_of xs) = sort xs"
   4.178    by (induct xs) simp_all
   4.179  
   4.180 -lemma finite_set_of_multiset_of_set:
   4.181 +lemma finite_set_mset_multiset_of_set:
   4.182    assumes "finite A"
   4.183 -  shows "set_of (multiset_of_set A) = A"
   4.184 +  shows "set_mset (multiset_of_set A) = A"
   4.185    using assms by (induct A) simp_all
   4.186  
   4.187 -lemma infinite_set_of_multiset_of_set:
   4.188 +lemma infinite_set_mset_multiset_of_set:
   4.189    assumes "\<not> finite A"
   4.190 -  shows "set_of (multiset_of_set A) = {}"
   4.191 +  shows "set_mset (multiset_of_set A) = {}"
   4.192    using assms by simp
   4.193  
   4.194  lemma set_sorted_list_of_multiset [simp]:
   4.195 -  "set (sorted_list_of_multiset M) = set_of M"
   4.196 +  "set (sorted_list_of_multiset M) = set_mset M"
   4.197    by (induct M) (simp_all add: set_insort)
   4.198  
   4.199  lemma sorted_list_of_multiset_of_set [simp]:
   4.200 @@ -1261,8 +1257,8 @@
   4.201    case empty then show ?case by simp
   4.202  next
   4.203    case (add M x) then show ?case
   4.204 -    by (cases "x \<in> set_of M")
   4.205 -      (simp_all del: mem_set_of_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
   4.206 +    by (cases "x \<in> set_mset M")
   4.207 +      (simp_all del: mem_set_mset_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
   4.208  qed
   4.209  
   4.210  
   4.211 @@ -1271,7 +1267,7 @@
   4.212  
   4.213  notation (xsymbols) Union_mset ("\<Union>#_" [900] 900)
   4.214  
   4.215 -lemma set_of_Union_mset[simp]: "set_of (\<Union># MM) = (\<Union>M \<in> set_of MM. set_of M)"
   4.216 +lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
   4.217    by (induct MM) auto
   4.218  
   4.219  lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
   4.220 @@ -1324,7 +1320,7 @@
   4.221    by (cases "finite A") (induct A rule: finite_induct, simp_all)
   4.222  
   4.223  lemma msetprod_multiplicity:
   4.224 -  "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
   4.225 +  "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_mset M)"
   4.226    by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
   4.227  
   4.228  end
   4.229 @@ -1371,7 +1367,7 @@
   4.230  lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
   4.231    unfolding replicate_mset_def by (induct n) simp_all
   4.232  
   4.233 -lemma set_of_replicate_mset_subset[simp]: "set_of (replicate_mset n x) = (if n = 0 then {} else {x})"
   4.234 +lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})"
   4.235    by (auto split: if_splits)
   4.236  
   4.237  lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
   4.238 @@ -1695,8 +1691,8 @@
   4.239  lemma mult_implies_one_step:
   4.240    "trans r ==> (M, N) \<in> mult r ==>
   4.241      \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
   4.242 -    (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)"
   4.243 -apply (unfold mult_def mult1_def set_of_def)
   4.244 +    (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)"
   4.245 +apply (unfold mult_def mult1_def set_mset_def)
   4.246  apply (erule converse_trancl_induct, clarify)
   4.247   apply (rule_tac x = M0 in exI, simp, clarify)
   4.248  apply (case_tac "a :# K")
   4.249 @@ -1726,7 +1722,7 @@
   4.250  
   4.251  lemma one_step_implies_mult_aux:
   4.252    "trans r ==>
   4.253 -    \<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))
   4.254 +    \<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))
   4.255        --> (I + K, I + J) \<in> mult r"
   4.256  apply (induct_tac n, auto)
   4.257  apply (frule size_eq_Suc_imp_eq_union, clarify)
   4.258 @@ -1735,10 +1731,10 @@
   4.259  apply (case_tac "J' = {#}")
   4.260   apply (simp add: mult_def)
   4.261   apply (rule r_into_trancl)
   4.262 - apply (simp add: mult1_def set_of_def, blast)
   4.263 + apply (simp add: mult1_def set_mset_def, blast)
   4.264  txt {* Now we know @{term "J' \<noteq> {#}"}. *}
   4.265  apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
   4.266 -apply (erule_tac P = "\<forall>k \<in> set_of K. P k" for P in rev_mp)
   4.267 +apply (erule_tac P = "\<forall>k \<in> set_mset K. P k" for P in rev_mp)
   4.268  apply (erule ssubst)
   4.269  apply (simp add: Ball_def, auto)
   4.270  apply (subgoal_tac
   4.271 @@ -1749,14 +1745,14 @@
   4.272  apply (simp (no_asm_use) add: add.assoc [symmetric] mult_def)
   4.273  apply (erule trancl_trans)
   4.274  apply (rule r_into_trancl)
   4.275 -apply (simp add: mult1_def set_of_def)
   4.276 +apply (simp add: mult1_def set_mset_def)
   4.277  apply (rule_tac x = a in exI)
   4.278  apply (rule_tac x = "I + J'" in exI)
   4.279  apply (simp add: ac_simps)
   4.280  done
   4.281  
   4.282  lemma one_step_implies_mult:
   4.283 -  "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r
   4.284 +  "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
   4.285      ==> (I + K, I + J) \<in> mult r"
   4.286  using one_step_implies_mult_aux by blast
   4.287  
   4.288 @@ -1783,14 +1779,14 @@
   4.289        by (rule transI) simp
   4.290      moreover note MM
   4.291      ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
   4.292 -      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
   4.293 +      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
   4.294        by (rule mult_implies_one_step)
   4.295      then obtain I J K where "M = I + J" and "M = I + K"
   4.296 -      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
   4.297 -    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
   4.298 -    have "finite (set_of K)" by simp
   4.299 +      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
   4.300 +    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
   4.301 +    have "finite (set_mset K)" by simp
   4.302      moreover note aux2
   4.303 -    ultimately have "set_of K = {}"
   4.304 +    ultimately have "set_mset K = {}"
   4.305        by (induct rule: finite_induct) (auto intro: order_less_trans)
   4.306      with aux1 show False by simp
   4.307    qed
   4.308 @@ -1851,12 +1847,12 @@
   4.309  by (auto intro: wf_mult1 wf_trancl simp: mult_def)
   4.310  
   4.311  lemma smsI:
   4.312 -  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
   4.313 +  "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
   4.314    unfolding ms_strict_def
   4.315  by (rule one_step_implies_mult) (auto simp add: max_strict_def pair_less_def elim!:max_ext.cases)
   4.316  
   4.317  lemma wmsI:
   4.318 -  "(set_of A, set_of B) \<in> max_strict \<or> A = {#} \<and> B = {#}
   4.319 +  "(set_mset A, set_mset B) \<in> max_strict \<or> A = {#} \<and> B = {#}
   4.320    \<Longrightarrow> (Z + A, Z + B) \<in> ms_weak"
   4.321  unfolding ms_weak_def ms_strict_def
   4.322  by (auto simp add: pair_less_def max_strict_def elim!:max_ext.cases intro: one_step_implies_mult)
   4.323 @@ -1872,7 +1868,7 @@
   4.324  
   4.325  lemma pw_leq_split:
   4.326    assumes "pw_leq X Y"
   4.327 -  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 = {#}))"
   4.328 +  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 = {#}))"
   4.329    using assms
   4.330  proof (induct)
   4.331    case pw_leq_empty thus ?case by auto
   4.332 @@ -1880,7 +1876,7 @@
   4.333    case (pw_leq_step x y X Y)
   4.334    then obtain A B Z where
   4.335      [simp]: "X = A + Z" "Y = B + Z"
   4.336 -      and 1[simp]: "(set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#})"
   4.337 +      and 1[simp]: "(set_mset A, set_mset B) \<in> max_strict \<or> (B = {#} \<and> A = {#})"
   4.338      by auto
   4.339    from pw_leq_step have "x = y \<or> (x, y) \<in> pair_less"
   4.340      unfolding pair_leq_def by auto
   4.341 @@ -1890,7 +1886,7 @@
   4.342      have
   4.343        "{#x#} + X = A + ({#y#}+Z)
   4.344        \<and> {#y#} + Y = B + ({#y#}+Z)
   4.345 -      \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
   4.346 +      \<and> ((set_mset A, set_mset B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
   4.347        by (auto simp: ac_simps)
   4.348      thus ?case by (intro exI)
   4.349    next
   4.350 @@ -1900,7 +1896,7 @@
   4.351        "{#y#} + Y = ?B' + Z"
   4.352        by (auto simp add: ac_simps)
   4.353      moreover have
   4.354 -      "(set_of ?A', set_of ?B') \<in> max_strict"
   4.355 +      "(set_mset ?A', set_mset ?B') \<in> max_strict"
   4.356        using 1 A unfolding max_strict_def
   4.357        by (auto elim!: max_ext.cases)
   4.358      ultimately show ?thesis by blast
   4.359 @@ -1909,22 +1905,22 @@
   4.360  
   4.361  lemma
   4.362    assumes pwleq: "pw_leq Z Z'"
   4.363 -  shows ms_strictI: "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
   4.364 -  and   ms_weakI1:  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
   4.365 +  shows ms_strictI: "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
   4.366 +  and   ms_weakI1:  "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
   4.367    and   ms_weakI2:  "(Z + {#}, Z' + {#}) \<in> ms_weak"
   4.368  proof -
   4.369    from pw_leq_split[OF pwleq]
   4.370    obtain A' B' Z''
   4.371      where [simp]: "Z = A' + Z''" "Z' = B' + Z''"
   4.372 -    and mx_or_empty: "(set_of A', set_of B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
   4.373 +    and mx_or_empty: "(set_mset A', set_mset B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
   4.374      by blast
   4.375    {
   4.376 -    assume max: "(set_of A, set_of B) \<in> max_strict"
   4.377 +    assume max: "(set_mset A, set_mset B) \<in> max_strict"
   4.378      from mx_or_empty
   4.379      have "(Z'' + (A + A'), Z'' + (B + B')) \<in> ms_strict"
   4.380      proof
   4.381 -      assume max': "(set_of A', set_of B') \<in> max_strict"
   4.382 -      with max have "(set_of (A + A'), set_of (B + B')) \<in> max_strict"
   4.383 +      assume max': "(set_mset A', set_mset B') \<in> max_strict"
   4.384 +      with max have "(set_mset (A + A'), set_mset (B + B')) \<in> max_strict"
   4.385          by (auto simp: max_strict_def intro: max_ext_additive)
   4.386        thus ?thesis by (rule smsI)
   4.387      next
   4.388 @@ -1972,14 +1968,14 @@
   4.389        ORELSE (rtac @{thm pw_leq_lstep} i)
   4.390        ORELSE (rtac @{thm pw_leq_empty} i)
   4.391  
   4.392 -  val set_of_simps = [@{thm set_of_empty}, @{thm set_of_single}, @{thm set_of_union},
   4.393 +  val set_mset_simps = [@{thm set_mset_empty}, @{thm set_mset_single}, @{thm set_mset_union},
   4.394                        @{thm Un_insert_left}, @{thm Un_empty_left}]
   4.395  in
   4.396    ScnpReconstruct.multiset_setup (ScnpReconstruct.Multiset
   4.397    {
   4.398      msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv,
   4.399      mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
   4.400 -    mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_of_simps,
   4.401 +    mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_mset_simps,
   4.402      smsI'= @{thm ms_strictI}, wmsI2''= @{thm ms_weakI2}, wmsI1= @{thm ms_weakI1},
   4.403      reduction_pair= @{thm ms_reduction_pair}
   4.404    })
   4.405 @@ -2136,7 +2132,7 @@
   4.406    then show ?thesis by simp
   4.407  qed
   4.408  
   4.409 -declare set_of_multiset_of [code]
   4.410 +declare set_mset_multiset_of [code]
   4.411  
   4.412  declare sorted_list_of_multiset_multiset_of [code]
   4.413  
   4.414 @@ -2170,7 +2166,7 @@
   4.415      hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
   4.416      {
   4.417        assume "multiset_of (x # xs) \<le># multiset_of ys"
   4.418 -      from set_of_mono[OF this] x have False by simp
   4.419 +      from set_mset_mono[OF this] x have False by simp
   4.420      } note nle = this
   4.421      moreover
   4.422      {
   4.423 @@ -2367,7 +2363,7 @@
   4.424  
   4.425  bnf "'a multiset"
   4.426    map: image_mset
   4.427 -  sets: set_of
   4.428 +  sets: set_mset
   4.429    bd: natLeq
   4.430    wits: "{#}"
   4.431    rel: rel_mset
   4.432 @@ -2379,11 +2375,11 @@
   4.433      unfolding comp_def by (rule ext) (simp add: comp_def image_mset.compositionality)
   4.434  next
   4.435    fix X :: "'a multiset"
   4.436 -  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"
   4.437 +  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"
   4.438      by (induct X, (simp (no_asm))+,
   4.439 -      metis One_nat_def Un_iff count_single mem_set_of_iff set_of_union zero_less_Suc)
   4.440 +      metis One_nat_def Un_iff count_single mem_set_mset_iff set_mset_union zero_less_Suc)
   4.441  next
   4.442 -  show "\<And>f. set_of \<circ> image_mset f = op ` f \<circ> set_of"
   4.443 +  show "\<And>f. set_mset \<circ> image_mset f = op ` f \<circ> set_mset"
   4.444      by auto
   4.445  next
   4.446    show "card_order natLeq"
   4.447 @@ -2392,7 +2388,7 @@
   4.448    show "BNF_Cardinal_Arithmetic.cinfinite natLeq"
   4.449      by (rule natLeq_cinfinite)
   4.450  next
   4.451 -  show "\<And>X. ordLeq3 (card_of (set_of X)) natLeq"
   4.452 +  show "\<And>X. ordLeq3 (card_of (set_mset X)) natLeq"
   4.453      by transfer
   4.454        (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
   4.455  next
   4.456 @@ -2404,8 +2400,8 @@
   4.457      by (auto intro: list_all2_trans)
   4.458  next
   4.459    show "\<And>R. rel_mset R =
   4.460 -    (BNF_Def.Grp {x. set_of x \<subseteq> {(x, y). R x y}} (image_mset fst))\<inverse>\<inverse> OO
   4.461 -    BNF_Def.Grp {x. set_of x \<subseteq> {(x, y). R x y}} (image_mset snd)"
   4.462 +    (BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset fst))\<inverse>\<inverse> OO
   4.463 +    BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset snd)"
   4.464      unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
   4.465      apply (rule ext)+
   4.466      apply auto
   4.467 @@ -2424,7 +2420,7 @@
   4.468      apply (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
   4.469      done
   4.470  next
   4.471 -  show "\<And>z. z \<in> set_of {#} \<Longrightarrow> False"
   4.472 +  show "\<And>z. z \<in> set_mset {#} \<Longrightarrow> False"
   4.473      by auto
   4.474  qed
   4.475  
   4.476 @@ -2444,10 +2440,10 @@
   4.477  assumes ab: "R a b" and MN: "rel_mset R M N"
   4.478  shows "rel_mset R (M + {#a#}) (N + {#b#})"
   4.479  proof-
   4.480 -  {fix y assume "R a b" and "set_of y \<subseteq> {(x, y). R x y}"
   4.481 +  {fix y assume "R a b" and "set_mset y \<subseteq> {(x, y). R x y}"
   4.482     hence "\<exists>ya. image_mset fst y + {#a#} = image_mset fst ya \<and>
   4.483                 image_mset snd y + {#b#} = image_mset snd ya \<and>
   4.484 -               set_of ya \<subseteq> {(x, y). R x y}"
   4.485 +               set_mset ya \<subseteq> {(x, y). R x y}"
   4.486     apply(intro exI[of _ "y + {#(a,b)#}"]) by auto
   4.487    }
   4.488    thus ?thesis
   4.489 @@ -2510,7 +2506,7 @@
   4.490  proof-
   4.491    obtain a where a: "a \<in># M" and fa: "f a = b"
   4.492    using multiset.set_map[of f M] unfolding assms
   4.493 -  by (metis image_iff mem_set_of_iff union_single_eq_member)
   4.494 +  by (metis image_iff mem_set_mset_iff union_single_eq_member)
   4.495    then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
   4.496    have "image_mset f M1 = N" using assms unfolding M fa[symmetric] by simp
   4.497    thus ?thesis using M fa by blast
   4.498 @@ -2521,7 +2517,7 @@
   4.499  shows "\<exists>N1 b. N = N1 + {#b#} \<and> R a b \<and> rel_mset R M N1"
   4.500  proof-
   4.501    obtain K where KM: "image_mset fst K = M + {#a#}"
   4.502 -  and KN: "image_mset snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
   4.503 +  and KN: "image_mset snd K = N" and sK: "set_mset K \<subseteq> {(a, b). R a b}"
   4.504    using assms
   4.505    unfolding multiset.rel_compp_Grp Grp_def by auto
   4.506    obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
   4.507 @@ -2539,7 +2535,7 @@
   4.508  shows "\<exists>M1 a. M = M1 + {#a#} \<and> R a b \<and> rel_mset R M1 N"
   4.509  proof-
   4.510    obtain K where KN: "image_mset snd K = N + {#b#}"
   4.511 -  and KM: "image_mset fst K = M" and sK: "set_of K \<subseteq> {(a, b). R a b}"
   4.512 +  and KM: "image_mset fst K = M" and sK: "set_mset K \<subseteq> {(a, b). R a b}"
   4.513    using assms
   4.514    unfolding multiset.rel_compp_Grp Grp_def by auto
   4.515    obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
     5.1 --- a/src/HOL/Library/Multiset_Order.thy	Tue Jun 16 20:50:00 2015 +0100
     5.2 +++ b/src/HOL/Library/Multiset_Order.thy	Wed Jun 17 17:21:11 2015 +0200
     5.3 @@ -47,14 +47,14 @@
     5.4      moreover
     5.5      assume "(M, M) \<in> mult {(x, y). x < y}"
     5.6      ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
     5.7 -      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
     5.8 +      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
     5.9        by (rule mult_implies_one_step)
    5.10      then obtain I J K where "M = I + J" and "M = I + K"
    5.11 -      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
    5.12 -    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
    5.13 -    have "finite (set_of K)" by simp
    5.14 +      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
    5.15 +    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
    5.16 +    have "finite (set_mset K)" by simp
    5.17      moreover note aux2
    5.18 -    ultimately have "set_of K = {}"
    5.19 +    ultimately have "set_mset K = {}"
    5.20        by (induct rule: finite_induct)
    5.21         (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
    5.22      with aux1 show False by simp
     6.1 --- a/src/HOL/Library/Permutation.thy	Tue Jun 16 20:50:00 2015 +0100
     6.2 +++ b/src/HOL/Library/Permutation.thy	Wed Jun 17 17:21:11 2015 +0200
     6.3 @@ -136,7 +136,7 @@
     6.4    apply (erule perm.trans)
     6.5    apply (rule perm_sym)
     6.6    apply (erule perm_remove)
     6.7 -  apply (drule_tac f=set_of in arg_cong)
     6.8 +  apply (drule_tac f=set_mset in arg_cong)
     6.9    apply simp
    6.10    done
    6.11  
     7.1 --- a/src/HOL/Library/Tree_Multiset.thy	Tue Jun 16 20:50:00 2015 +0100
     7.2 +++ b/src/HOL/Library/Tree_Multiset.thy	Wed Jun 17 17:21:11 2015 +0200
     7.3 @@ -14,7 +14,7 @@
     7.4  "mset_tree Leaf = {#}" |
     7.5  "mset_tree (Node l a r) = {#a#} + mset_tree l + mset_tree r"
     7.6  
     7.7 -lemma set_of_mset_tree[simp]: "set_of (mset_tree t) = set_tree t"
     7.8 +lemma set_mset_tree[simp]: "set_mset (mset_tree t) = set_tree t"
     7.9  by(induction t) auto
    7.10  
    7.11  lemma size_mset_tree[simp]: "size(mset_tree t) = size t"
     8.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Tue Jun 16 20:50:00 2015 +0100
     8.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Jun 17 17:21:11 2015 +0200
     8.3 @@ -37,67 +37,67 @@
     8.4  subsection {* unique factorization: multiset version *}
     8.5  
     8.6  lemma multiset_prime_factorization_exists [rule_format]: "n > 0 --> 
     8.7 -    (EX M. (ALL (p::nat) : set_of M. prime p) & n = (PROD i :# M. i))"
     8.8 +    (EX M. (ALL (p::nat) : set_mset M. prime p) & n = (PROD i :# M. i))"
     8.9  proof (rule nat_less_induct, clarify)
    8.10    fix n :: nat
    8.11 -  assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_of M. prime p) & m = 
    8.12 +  assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_mset M. prime p) & m = 
    8.13        (PROD i :# M. i))"
    8.14    assume "(n::nat) > 0"
    8.15    then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
    8.16      by arith
    8.17    moreover {
    8.18      assume "n = 1"
    8.19 -    then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)" by auto
    8.20 +    then have "(ALL p : set_mset {#}. prime p) & n = (PROD i :# {#}. i)" by auto
    8.21    } moreover {
    8.22      assume "n > 1" and "prime n"
    8.23 -    then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
    8.24 +    then have "(ALL p : set_mset {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
    8.25        by auto
    8.26    } moreover {
    8.27      assume "n > 1" and "~ prime n"
    8.28      with not_prime_eq_prod_nat
    8.29      obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
    8.30        by blast
    8.31 -    with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
    8.32 -        and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
    8.33 +    with ih obtain Q R where "(ALL p : set_mset Q. prime p) & m = (PROD i:#Q. i)"
    8.34 +        and "(ALL p: set_mset R. prime p) & k = (PROD i:#R. i)"
    8.35        by blast
    8.36 -    then have "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
    8.37 +    then have "(ALL p: set_mset (Q + R). prime p) & n = (PROD i :# Q + R. i)"
    8.38        by (auto simp add: n msetprod_Un)
    8.39 -    then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
    8.40 +    then have "EX M. (ALL p : set_mset M. prime p) & n = (PROD i :# M. i)"..
    8.41    }
    8.42 -  ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)"
    8.43 +  ultimately show "EX M. (ALL p : set_mset M. prime p) & n = (PROD i::nat:#M. i)"
    8.44      by blast
    8.45  qed
    8.46  
    8.47  lemma multiset_prime_factorization_unique_aux:
    8.48    fixes a :: nat
    8.49 -  assumes "(ALL p : set_of M. prime p)" and
    8.50 -    "(ALL p : set_of N. prime p)" and
    8.51 +  assumes "(ALL p : set_mset M. prime p)" and
    8.52 +    "(ALL p : set_mset N. prime p)" and
    8.53      "(PROD i :# M. i) dvd (PROD i:# N. i)"
    8.54    shows
    8.55      "count M a <= count N a"
    8.56  proof cases
    8.57 -  assume M: "a : set_of M"
    8.58 +  assume M: "a : set_mset M"
    8.59    with assms have a: "prime a" by auto
    8.60    with M have "a ^ count M a dvd (PROD i :# M. i)"
    8.61      by (auto simp add: msetprod_multiplicity)
    8.62    also have "... dvd (PROD i :# N. i)" by (rule assms)
    8.63 -  also have "... = (PROD i : (set_of N). i ^ (count N i))"
    8.64 +  also have "... = (PROD i : (set_mset N). i ^ (count N i))"
    8.65      by (simp add: msetprod_multiplicity)
    8.66 -  also have "... = a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
    8.67 +  also have "... = a^(count N a) * (PROD i : (set_mset N - {a}). i ^ (count N i))"
    8.68    proof (cases)
    8.69 -    assume "a : set_of N"
    8.70 -    then have b: "set_of N = {a} Un (set_of N - {a})"
    8.71 +    assume "a : set_mset N"
    8.72 +    then have b: "set_mset N = {a} Un (set_mset N - {a})"
    8.73        by auto
    8.74      then show ?thesis
    8.75        by (subst (1) b, subst setprod.union_disjoint, auto)
    8.76    next
    8.77 -    assume "a ~: set_of N" 
    8.78 +    assume "a ~: set_mset N" 
    8.79      then show ?thesis by auto
    8.80    qed
    8.81    finally have "a ^ count M a dvd 
    8.82 -      a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
    8.83 +      a^(count N a) * (PROD i : (set_mset N - {a}). i ^ (count N i))".
    8.84    moreover
    8.85 -  have "coprime (a ^ count M a) (PROD i : (set_of N - {a}). i ^ (count N i))"
    8.86 +  have "coprime (a ^ count M a) (PROD i : (set_mset N - {a}). i ^ (count N i))"
    8.87      apply (subst gcd_commute_nat)
    8.88      apply (rule setprod_coprime_nat)
    8.89      apply (rule primes_imp_powers_coprime_nat)
    8.90 @@ -111,13 +111,13 @@
    8.91      apply auto
    8.92      done
    8.93  next
    8.94 -  assume "a ~: set_of M"
    8.95 +  assume "a ~: set_mset M"
    8.96    then show ?thesis by auto
    8.97  qed
    8.98  
    8.99  lemma multiset_prime_factorization_unique:
   8.100 -  assumes "(ALL (p::nat) : set_of M. prime p)" and
   8.101 -    "(ALL p : set_of N. prime p)" and
   8.102 +  assumes "(ALL (p::nat) : set_mset M. prime p)" and
   8.103 +    "(ALL p : set_mset N. prime p)" and
   8.104      "(PROD i :# M. i) = (PROD i:# N. i)"
   8.105    shows
   8.106      "M = N"
   8.107 @@ -137,12 +137,12 @@
   8.108  definition multiset_prime_factorization :: "nat => nat multiset"
   8.109  where
   8.110    "multiset_prime_factorization n ==
   8.111 -     if n > 0 then (THE M. ((ALL p : set_of M. prime p) & 
   8.112 +     if n > 0 then (THE M. ((ALL p : set_mset M. prime p) & 
   8.113         n = (PROD i :# M. i)))
   8.114       else {#}"
   8.115  
   8.116  lemma multiset_prime_factorization: "n > 0 ==>
   8.117 -    (ALL p : set_of (multiset_prime_factorization n). prime p) &
   8.118 +    (ALL p : set_mset (multiset_prime_factorization n). prime p) &
   8.119         n = (PROD i :# (multiset_prime_factorization n). i)"
   8.120    apply (unfold multiset_prime_factorization_def)
   8.121    apply clarsimp
   8.122 @@ -169,7 +169,7 @@
   8.123    where "multiplicity_nat p n = count (multiset_prime_factorization n) p"
   8.124  
   8.125  definition prime_factors_nat :: "nat \<Rightarrow> nat set"
   8.126 -  where "prime_factors_nat n = set_of (multiset_prime_factorization n)"
   8.127 +  where "prime_factors_nat n = set_mset (multiset_prime_factorization n)"
   8.128  
   8.129  instance ..
   8.130  
   8.131 @@ -306,12 +306,12 @@
   8.132      apply force
   8.133      apply force
   8.134      using assms
   8.135 -    apply (simp add: set_of_def msetprod_multiplicity)
   8.136 +    apply (simp add: set_mset_def msetprod_multiplicity)
   8.137      done
   8.138    with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
   8.139      by simp
   8.140    with S_eq show ?thesis
   8.141 -    by (simp add: set_of_def multiset_def prime_factors_nat_def multiplicity_nat_def)
   8.142 +    by (simp add: set_mset_def multiset_def prime_factors_nat_def multiplicity_nat_def)
   8.143  qed
   8.144  
   8.145  lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
   8.146 @@ -435,7 +435,7 @@
   8.147    apply (cases "n = 0")
   8.148    apply auto
   8.149    apply (frule multiset_prime_factorization)
   8.150 -  apply (auto simp add: set_of_def multiplicity_nat_def)
   8.151 +  apply (auto simp add: set_mset_def multiplicity_nat_def)
   8.152    done
   8.153  
   8.154  lemma multiplicity_not_factor_nat [simp]: 
     9.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Jun 16 20:50:00 2015 +0100
     9.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Jun 17 17:21:11 2015 +0200
     9.3 @@ -1413,7 +1413,7 @@
     9.4  lemma pmf_of_multiset[simp]: "pmf pmf_of_multiset x = count M x / size M"
     9.5    by transfer rule
     9.6  
     9.7 -lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_of M"
     9.8 +lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_mset M"
     9.9    by (auto simp: set_pmf_iff)
    9.10  
    9.11  end
    10.1 --- a/src/HOL/ZF/LProd.thy	Tue Jun 16 20:50:00 2015 +0100
    10.2 +++ b/src/HOL/ZF/LProd.thy	Wed Jun 17 17:21:11 2015 +0200
    10.3 @@ -50,10 +50,10 @@
    10.4    from lprod_list have "(?ma, ?mb) \<in> mult R"
    10.5      by auto
    10.6    with mult_implies_one_step[OF transR] have 
    10.7 -    "\<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)"
    10.8 +    "\<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)"
    10.9      by blast
   10.10    then obtain I J K where 
   10.11 -    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)"
   10.12 +    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)"
   10.13      by blast   
   10.14    show ?case
   10.15    proof (cases "a = b")