src/HOL/Library/Multiset.thy
changeset 60515 484559628038
parent 60513 55c7316f76d6
child 60606 e5cb9271e339
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Jun 18 16:17:51 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Jun 19 15:55:22 2015 +0200
     1.3 @@ -963,46 +963,46 @@
     1.4  
     1.5  subsection \<open>Further conversions\<close>
     1.6  
     1.7 -primrec multiset_of :: "'a list \<Rightarrow> 'a multiset" where
     1.8 -  "multiset_of [] = {#}" |
     1.9 -  "multiset_of (a # x) = multiset_of x + {# a #}"
    1.10 +primrec mset :: "'a list \<Rightarrow> 'a multiset" where
    1.11 +  "mset [] = {#}" |
    1.12 +  "mset (a # x) = mset x + {# a #}"
    1.13  
    1.14  lemma in_multiset_in_set:
    1.15 -  "x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs"
    1.16 +  "x \<in># mset xs \<longleftrightarrow> x \<in> set xs"
    1.17    by (induct xs) simp_all
    1.18  
    1.19 -lemma count_multiset_of:
    1.20 -  "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
    1.21 +lemma count_mset:
    1.22 +  "count (mset xs) x = length (filter (\<lambda>y. x = y) xs)"
    1.23    by (induct xs) simp_all
    1.24  
    1.25 -lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
    1.26 +lemma mset_zero_iff[simp]: "(mset x = {#}) = (x = [])"
    1.27    by (induct x) auto
    1.28  
    1.29 -lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
    1.30 +lemma mset_zero_iff_right[simp]: "({#} = mset x) = (x = [])"
    1.31  by (induct x) auto
    1.32  
    1.33 -lemma set_mset_multiset_of[simp]: "set_mset (multiset_of x) = set x"
    1.34 +lemma set_mset_mset[simp]: "set_mset (mset x) = set x"
    1.35  by (induct x) auto
    1.36  
    1.37 -lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
    1.38 +lemma mem_set_multiset_eq: "x \<in> set xs = (x :# mset xs)"
    1.39  by (induct xs) auto
    1.40  
    1.41 -lemma size_multiset_of [simp]: "size (multiset_of xs) = length xs"
    1.42 +lemma size_mset [simp]: "size (mset xs) = length xs"
    1.43    by (induct xs) simp_all
    1.44  
    1.45 -lemma multiset_of_append [simp]:
    1.46 -  "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
    1.47 +lemma mset_append [simp]:
    1.48 +  "mset (xs @ ys) = mset xs + mset ys"
    1.49    by (induct xs arbitrary: ys) (auto simp: ac_simps)
    1.50  
    1.51 -lemma multiset_of_filter:
    1.52 -  "multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}"
    1.53 +lemma mset_filter:
    1.54 +  "mset (filter P xs) = {#x :# mset xs. P x #}"
    1.55    by (induct xs) simp_all
    1.56  
    1.57 -lemma multiset_of_rev [simp]:
    1.58 -  "multiset_of (rev xs) = multiset_of xs"
    1.59 +lemma mset_rev [simp]:
    1.60 +  "mset (rev xs) = mset xs"
    1.61    by (induct xs) simp_all
    1.62  
    1.63 -lemma surj_multiset_of: "surj multiset_of"
    1.64 +lemma surj_mset: "surj mset"
    1.65  apply (unfold surj_def)
    1.66  apply (rule allI)
    1.67  apply (rule_tac M = y in multiset_induct)
    1.68 @@ -1011,72 +1011,72 @@
    1.69  apply auto
    1.70  done
    1.71  
    1.72 -lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}"
    1.73 +lemma set_count_greater_0: "set x = {a. count (mset x) a > 0}"
    1.74  by (induct x) auto
    1.75  
    1.76  lemma distinct_count_atmost_1:
    1.77 -  "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
    1.78 +  "distinct x = (! a. count (mset x) a = (if a \<in> set x then 1 else 0))"
    1.79  apply (induct x, simp, rule iffI, simp_all)
    1.80  apply (rename_tac a b)
    1.81  apply (rule conjI)
    1.82 -apply (simp_all add: set_mset_multiset_of [THEN sym] del: set_mset_multiset_of)
    1.83 +apply (simp_all add: set_mset_mset [THEN sym] del: set_mset_mset)
    1.84  apply (erule_tac x = a in allE, simp, clarify)
    1.85  apply (erule_tac x = aa in allE, simp)
    1.86  done
    1.87  
    1.88 -lemma multiset_of_eq_setD:
    1.89 -  "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
    1.90 +lemma mset_eq_setD:
    1.91 +  "mset xs = mset ys \<Longrightarrow> set xs = set ys"
    1.92  by (rule) (auto simp add:multiset_eq_iff set_count_greater_0)
    1.93  
    1.94 -lemma set_eq_iff_multiset_of_eq_distinct:
    1.95 +lemma set_eq_iff_mset_eq_distinct:
    1.96    "distinct x \<Longrightarrow> distinct y \<Longrightarrow>
    1.97 -    (set x = set y) = (multiset_of x = multiset_of y)"
    1.98 +    (set x = set y) = (mset x = mset y)"
    1.99  by (auto simp: multiset_eq_iff distinct_count_atmost_1)
   1.100  
   1.101 -lemma set_eq_iff_multiset_of_remdups_eq:
   1.102 -   "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
   1.103 +lemma set_eq_iff_mset_remdups_eq:
   1.104 +   "(set x = set y) = (mset (remdups x) = mset (remdups y))"
   1.105  apply (rule iffI)
   1.106 -apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1])
   1.107 +apply (simp add: set_eq_iff_mset_eq_distinct[THEN iffD1])
   1.108  apply (drule distinct_remdups [THEN distinct_remdups
   1.109 -      [THEN set_eq_iff_multiset_of_eq_distinct [THEN iffD2]]])
   1.110 +      [THEN set_eq_iff_mset_eq_distinct [THEN iffD2]]])
   1.111  apply simp
   1.112  done
   1.113  
   1.114 -lemma multiset_of_compl_union [simp]:
   1.115 -  "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
   1.116 +lemma mset_compl_union [simp]:
   1.117 +  "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
   1.118    by (induct xs) (auto simp: ac_simps)
   1.119  
   1.120 -lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
   1.121 +lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) :# mset ls"
   1.122  apply (induct ls arbitrary: i)
   1.123   apply simp
   1.124  apply (case_tac i)
   1.125   apply auto
   1.126  done
   1.127  
   1.128 -lemma multiset_of_remove1[simp]:
   1.129 -  "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
   1.130 +lemma mset_remove1[simp]:
   1.131 +  "mset (remove1 a xs) = mset xs - {#a#}"
   1.132  by (induct xs) (auto simp add: multiset_eq_iff)
   1.133  
   1.134 -lemma multiset_of_eq_length:
   1.135 -  assumes "multiset_of xs = multiset_of ys"
   1.136 +lemma mset_eq_length:
   1.137 +  assumes "mset xs = mset ys"
   1.138    shows "length xs = length ys"
   1.139 -  using assms by (metis size_multiset_of)
   1.140 -
   1.141 -lemma multiset_of_eq_length_filter:
   1.142 -  assumes "multiset_of xs = multiset_of ys"
   1.143 +  using assms by (metis size_mset)
   1.144 +
   1.145 +lemma mset_eq_length_filter:
   1.146 +  assumes "mset xs = mset ys"
   1.147    shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)"
   1.148 -  using assms by (metis count_multiset_of)
   1.149 +  using assms by (metis count_mset)
   1.150  
   1.151  lemma fold_multiset_equiv:
   1.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"
   1.153 -    and equiv: "multiset_of xs = multiset_of ys"
   1.154 +    and equiv: "mset xs = mset ys"
   1.155    shows "List.fold f xs = List.fold f ys"
   1.156  using f equiv [symmetric]
   1.157  proof (induct xs arbitrary: ys)
   1.158    case Nil then show ?case by simp
   1.159  next
   1.160    case (Cons x xs)
   1.161 -  then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
   1.162 +  then have *: "set ys = set (x # xs)" by (blast dest: mset_eq_setD)
   1.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"
   1.164      by (rule Cons.prems(1)) (simp_all add: *)
   1.165    moreover from * have "x \<in> set ys" by simp
   1.166 @@ -1085,12 +1085,12 @@
   1.167    ultimately show ?case by simp
   1.168  qed
   1.169  
   1.170 -lemma multiset_of_insort [simp]:
   1.171 -  "multiset_of (insort x xs) = multiset_of xs + {#x#}"
   1.172 +lemma mset_insort [simp]:
   1.173 +  "mset (insort x xs) = mset xs + {#x#}"
   1.174    by (induct xs) (simp_all add: ac_simps)
   1.175  
   1.176 -lemma multiset_of_map:
   1.177 -  "multiset_of (map f xs) = image_mset f (multiset_of xs)"
   1.178 +lemma mset_map:
   1.179 +  "mset (map f xs) = image_mset f (mset xs)"
   1.180    by (induct xs) simp_all
   1.181  
   1.182  definition mset_set :: "'a set \<Rightarrow> 'a multiset"
   1.183 @@ -1154,12 +1154,12 @@
   1.184  
   1.185  end
   1.186  
   1.187 -lemma multiset_of_sorted_list_of_multiset [simp]:
   1.188 -  "multiset_of (sorted_list_of_multiset M) = M"
   1.189 +lemma mset_sorted_list_of_multiset [simp]:
   1.190 +  "mset (sorted_list_of_multiset M) = M"
   1.191  by (induct M) simp_all
   1.192  
   1.193 -lemma sorted_list_of_multiset_multiset_of [simp]:
   1.194 -  "sorted_list_of_multiset (multiset_of xs) = sort xs"
   1.195 +lemma sorted_list_of_multiset_mset [simp]:
   1.196 +  "sorted_list_of_multiset (mset xs) = sort xs"
   1.197  by (induct xs) simp_all
   1.198  
   1.199  lemma finite_set_mset_mset_set[simp]:
   1.200 @@ -1386,12 +1386,12 @@
   1.201  context linorder
   1.202  begin
   1.203  
   1.204 -lemma multiset_of_insort [simp]:
   1.205 -  "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs"
   1.206 +lemma mset_insort [simp]:
   1.207 +  "mset (insort_key k x xs) = {#x#} + mset xs"
   1.208    by (induct xs) (simp_all add: ac_simps)
   1.209  
   1.210 -lemma multiset_of_sort [simp]:
   1.211 -  "multiset_of (sort_key k xs) = multiset_of xs"
   1.212 +lemma mset_sort [simp]:
   1.213 +  "mset (sort_key k xs) = mset xs"
   1.214    by (induct xs) (simp_all add: ac_simps)
   1.215  
   1.216  text \<open>
   1.217 @@ -1400,7 +1400,7 @@
   1.218  \<close>
   1.219  
   1.220  lemma properties_for_sort_key:
   1.221 -  assumes "multiset_of ys = multiset_of xs"
   1.222 +  assumes "mset ys = mset xs"
   1.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"
   1.224    and "sorted (map f ys)"
   1.225    shows "sort_key f xs = ys"
   1.226 @@ -1420,14 +1420,14 @@
   1.227  qed
   1.228  
   1.229  lemma properties_for_sort:
   1.230 -  assumes multiset: "multiset_of ys = multiset_of xs"
   1.231 +  assumes multiset: "mset ys = mset xs"
   1.232    and "sorted ys"
   1.233    shows "sort xs = ys"
   1.234  proof (rule properties_for_sort_key)
   1.235 -  from multiset show "multiset_of ys = multiset_of xs" .
   1.236 +  from multiset show "mset ys = mset xs" .
   1.237    from \<open>sorted ys\<close> show "sorted (map (\<lambda>x. x) ys)" by simp
   1.238    from multiset have "\<And>k. length (filter (\<lambda>y. k = y) ys) = length (filter (\<lambda>x. k = x) xs)"
   1.239 -    by (rule multiset_of_eq_length_filter)
   1.240 +    by (rule mset_eq_length_filter)
   1.241    then have "\<And>k. replicate (length (filter (\<lambda>y. k = y) ys)) k = replicate (length (filter (\<lambda>x. k = x) xs)) k"
   1.242      by simp
   1.243    then show "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>y. k = y) ys = filter (\<lambda>x. k = x) xs"
   1.244 @@ -1439,8 +1439,8 @@
   1.245      @ [x\<leftarrow>xs. f x = f (xs ! (length xs div 2))]
   1.246      @ sort_key f [x\<leftarrow>xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs")
   1.247  proof (rule properties_for_sort_key)
   1.248 -  show "multiset_of ?rhs = multiset_of ?lhs"
   1.249 -    by (rule multiset_eqI) (auto simp add: multiset_of_filter)
   1.250 +  show "mset ?rhs = mset ?lhs"
   1.251 +    by (rule multiset_eqI) (auto simp add: mset_filter)
   1.252  next
   1.253    show "sorted (map f ?rhs)"
   1.254      by (auto simp add: sorted_append intro: sorted_map_same)
   1.255 @@ -1523,11 +1523,11 @@
   1.256  
   1.257  hide_const (open) part
   1.258  
   1.259 -lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
   1.260 +lemma mset_remdups_le: "mset (remdups xs) \<le># mset xs"
   1.261    by (induct xs) (auto intro: subset_mset.order_trans)
   1.262  
   1.263 -lemma multiset_of_update:
   1.264 -  "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
   1.265 +lemma mset_update:
   1.266 +  "i < length ls \<Longrightarrow> mset (ls[i := v]) = mset ls - {#ls ! i#} + {#v#}"
   1.267  proof (induct ls arbitrary: i)
   1.268    case Nil then show ?case by simp
   1.269  next
   1.270 @@ -1544,15 +1544,15 @@
   1.271        apply (subst add.assoc [symmetric])
   1.272        apply simp
   1.273        apply (rule mset_le_multiset_union_diff_commute)
   1.274 -      apply (simp add: mset_le_single nth_mem_multiset_of)
   1.275 +      apply (simp add: mset_le_single nth_mem_mset)
   1.276        done
   1.277    qed
   1.278  qed
   1.279  
   1.280 -lemma multiset_of_swap:
   1.281 +lemma mset_swap:
   1.282    "i < length ls \<Longrightarrow> j < length ls \<Longrightarrow>
   1.283 -    multiset_of (ls[j := ls ! i, i := ls ! j]) = multiset_of ls"
   1.284 -  by (cases "i = j") (simp_all add: multiset_of_update nth_mem_multiset_of)
   1.285 +    mset (ls[j := ls ! i, i := ls ! j]) = mset ls"
   1.286 +  by (cases "i = j") (simp_all add: mset_update nth_mem_mset)
   1.287  
   1.288  
   1.289  subsection \<open>The multiset order\<close>
   1.290 @@ -2071,51 +2071,51 @@
   1.291  
   1.292  subsection \<open>Naive implementation using lists\<close>
   1.293  
   1.294 -code_datatype multiset_of
   1.295 +code_datatype mset
   1.296  
   1.297  lemma [code]:
   1.298 -  "{#} = multiset_of []"
   1.299 +  "{#} = mset []"
   1.300    by simp
   1.301  
   1.302  lemma [code]:
   1.303 -  "{#x#} = multiset_of [x]"
   1.304 +  "{#x#} = mset [x]"
   1.305    by simp
   1.306  
   1.307  lemma union_code [code]:
   1.308 -  "multiset_of xs + multiset_of ys = multiset_of (xs @ ys)"
   1.309 +  "mset xs + mset ys = mset (xs @ ys)"
   1.310    by simp
   1.311  
   1.312  lemma [code]:
   1.313 -  "image_mset f (multiset_of xs) = multiset_of (map f xs)"
   1.314 -  by (simp add: multiset_of_map)
   1.315 +  "image_mset f (mset xs) = mset (map f xs)"
   1.316 +  by (simp add: mset_map)
   1.317  
   1.318  lemma [code]:
   1.319 -  "filter_mset f (multiset_of xs) = multiset_of (filter f xs)"
   1.320 -  by (simp add: multiset_of_filter)
   1.321 +  "filter_mset f (mset xs) = mset (filter f xs)"
   1.322 +  by (simp add: mset_filter)
   1.323  
   1.324  lemma [code]:
   1.325 -  "multiset_of xs - multiset_of ys = multiset_of (fold remove1 ys xs)"
   1.326 +  "mset xs - mset ys = mset (fold remove1 ys xs)"
   1.327    by (rule sym, induct ys arbitrary: xs) (simp_all add: diff_add diff_right_commute)
   1.328  
   1.329  lemma [code]:
   1.330 -  "multiset_of xs #\<inter> multiset_of ys =
   1.331 -    multiset_of (snd (fold (\<lambda>x (ys, zs).
   1.332 +  "mset xs #\<inter> mset ys =
   1.333 +    mset (snd (fold (\<lambda>x (ys, zs).
   1.334        if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, [])))"
   1.335  proof -
   1.336 -  have "\<And>zs. multiset_of (snd (fold (\<lambda>x (ys, zs).
   1.337 +  have "\<And>zs. mset (snd (fold (\<lambda>x (ys, zs).
   1.338      if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, zs))) =
   1.339 -      (multiset_of xs #\<inter> multiset_of ys) + multiset_of zs"
   1.340 +      (mset xs #\<inter> mset ys) + mset zs"
   1.341      by (induct xs arbitrary: ys)
   1.342        (auto simp add: mem_set_multiset_eq inter_add_right1 inter_add_right2 ac_simps)
   1.343    then show ?thesis by simp
   1.344  qed
   1.345  
   1.346  lemma [code]:
   1.347 -  "multiset_of xs #\<union> multiset_of ys =
   1.348 -    multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
   1.349 +  "mset xs #\<union> mset ys =
   1.350 +    mset (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
   1.351  proof -
   1.352 -  have "\<And>zs. multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
   1.353 -      (multiset_of xs #\<union> multiset_of ys) + multiset_of zs"
   1.354 +  have "\<And>zs. mset (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
   1.355 +      (mset xs #\<union> mset ys) + mset zs"
   1.356      by (induct xs arbitrary: ys) (simp_all add: multiset_eq_iff)
   1.357    then show ?thesis by simp
   1.358  qed
   1.359 @@ -2123,26 +2123,26 @@
   1.360  declare in_multiset_in_set [code_unfold]
   1.361  
   1.362  lemma [code]:
   1.363 -  "count (multiset_of xs) x = fold (\<lambda>y. if x = y then Suc else id) xs 0"
   1.364 +  "count (mset xs) x = fold (\<lambda>y. if x = y then Suc else id) xs 0"
   1.365  proof -
   1.366 -  have "\<And>n. fold (\<lambda>y. if x = y then Suc else id) xs n = count (multiset_of xs) x + n"
   1.367 +  have "\<And>n. fold (\<lambda>y. if x = y then Suc else id) xs n = count (mset xs) x + n"
   1.368      by (induct xs) simp_all
   1.369    then show ?thesis by simp
   1.370  qed
   1.371  
   1.372 -declare set_mset_multiset_of [code]
   1.373 -
   1.374 -declare sorted_list_of_multiset_multiset_of [code]
   1.375 +declare set_mset_mset [code]
   1.376 +
   1.377 +declare sorted_list_of_multiset_mset [code]
   1.378  
   1.379  lemma [code]: -- \<open>not very efficient, but representation-ignorant!\<close>
   1.380 -  "mset_set A = multiset_of (sorted_list_of_set A)"
   1.381 +  "mset_set A = mset (sorted_list_of_set A)"
   1.382    apply (cases "finite A")
   1.383    apply simp_all
   1.384    apply (induct A rule: finite_induct)
   1.385    apply (simp_all add: add.commute)
   1.386    done
   1.387  
   1.388 -declare size_multiset_of [code]
   1.389 +declare size_mset [code]
   1.390  
   1.391  fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
   1.392    "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
   1.393 @@ -2150,9 +2150,9 @@
   1.394       None \<Rightarrow> None
   1.395     | Some (ys1,_,ys2) \<Rightarrow> ms_lesseq_impl xs (ys1 @ ys2))"
   1.396  
   1.397 -lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> multiset_of xs \<le># multiset_of ys) \<and>
   1.398 -  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> multiset_of xs <# multiset_of ys) \<and>
   1.399 -  (ms_lesseq_impl xs ys = Some False \<longrightarrow> multiset_of xs = multiset_of ys)"
   1.400 +lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> mset xs \<le># mset ys) \<and>
   1.401 +  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> mset xs <# mset ys) \<and>
   1.402 +  (ms_lesseq_impl xs ys = Some False \<longrightarrow> mset xs = mset ys)"
   1.403  proof (induct xs arbitrary: ys)
   1.404    case (Nil ys)
   1.405    show ?case by (auto simp: mset_less_empty_nonempty)
   1.406 @@ -2163,13 +2163,13 @@
   1.407      case None
   1.408      hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
   1.409      {
   1.410 -      assume "multiset_of (x # xs) \<le># multiset_of ys"
   1.411 +      assume "mset (x # xs) \<le># mset ys"
   1.412        from set_mset_mono[OF this] x have False by simp
   1.413      } note nle = this
   1.414      moreover
   1.415      {
   1.416 -      assume "multiset_of (x # xs) <# multiset_of ys"
   1.417 -      hence "multiset_of (x # xs) \<le># multiset_of ys" by auto
   1.418 +      assume "mset (x # xs) <# mset ys"
   1.419 +      hence "mset (x # xs) \<le># mset ys" by auto
   1.420        from nle[OF this] have False .
   1.421      }
   1.422      ultimately show ?thesis using None by auto
   1.423 @@ -2178,7 +2178,7 @@
   1.424      obtain ys1 y ys2 where res: "res = (ys1,y,ys2)" by (cases res, auto)
   1.425      note Some = Some[unfolded res]
   1.426      from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp
   1.427 -    hence id: "multiset_of ys = multiset_of (ys1 @ ys2) + {#x#}"
   1.428 +    hence id: "mset ys = mset (ys1 @ ys2) + {#x#}"
   1.429        by (auto simp: ac_simps)
   1.430      show ?thesis unfolding ms_lesseq_impl.simps
   1.431        unfolding Some option.simps split
   1.432 @@ -2188,10 +2188,10 @@
   1.433    qed
   1.434  qed
   1.435  
   1.436 -lemma [code]: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
   1.437 +lemma [code]: "mset xs \<le># mset ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
   1.438    using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
   1.439  
   1.440 -lemma [code]: "multiset_of xs <# multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
   1.441 +lemma [code]: "mset xs <# mset ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
   1.442    using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
   1.443  
   1.444  instantiation multiset :: (equal) equal
   1.445 @@ -2199,7 +2199,7 @@
   1.446  
   1.447  definition
   1.448    [code del]: "HOL.equal A (B :: 'a multiset) \<longleftrightarrow> A = B"
   1.449 -lemma [code]: "HOL.equal (multiset_of xs) (multiset_of ys) \<longleftrightarrow> ms_lesseq_impl xs ys = Some False"
   1.450 +lemma [code]: "HOL.equal (mset xs) (mset ys) \<longleftrightarrow> ms_lesseq_impl xs ys = Some False"
   1.451    unfolding equal_multiset_def
   1.452    using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
   1.453  
   1.454 @@ -2208,13 +2208,13 @@
   1.455  end
   1.456  
   1.457  lemma [code]:
   1.458 -  "msetsum (multiset_of xs) = listsum xs"
   1.459 +  "msetsum (mset xs) = listsum xs"
   1.460    by (induct xs) (simp_all add: add.commute)
   1.461  
   1.462  lemma [code]:
   1.463 -  "msetprod (multiset_of xs) = fold times xs 1"
   1.464 +  "msetprod (mset xs) = fold times xs 1"
   1.465  proof -
   1.466 -  have "\<And>x. fold times xs x = msetprod (multiset_of xs) * x"
   1.467 +  have "\<And>x. fold times xs x = msetprod (mset xs) * x"
   1.468      by (induct xs) (simp_all add: mult.assoc)
   1.469    then show ?thesis by simp
   1.470  qed
   1.471 @@ -2229,7 +2229,7 @@
   1.472  definition (in term_syntax)
   1.473    msetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
   1.474      \<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   1.475 -  [code_unfold]: "msetify xs = Code_Evaluation.valtermify multiset_of {\<cdot>} xs"
   1.476 +  [code_unfold]: "msetify xs = Code_Evaluation.valtermify mset {\<cdot>} xs"
   1.477  
   1.478  notation fcomp (infixl "\<circ>>" 60)
   1.479  notation scomp (infixl "\<circ>\<rightarrow>" 60)
   1.480 @@ -2264,12 +2264,12 @@
   1.481  subsection \<open>BNF setup\<close>
   1.482  
   1.483  definition rel_mset where
   1.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)"
   1.485 -
   1.486 -lemma multiset_of_zip_take_Cons_drop_twice:
   1.487 +  "rel_mset R X Y \<longleftrightarrow> (\<exists>xs ys. mset xs = X \<and> mset ys = Y \<and> list_all2 R xs ys)"
   1.488 +
   1.489 +lemma mset_zip_take_Cons_drop_twice:
   1.490    assumes "length xs = length ys" "j \<le> length xs"
   1.491 -  shows "multiset_of (zip (take j xs @ x # drop j xs) (take j ys @ y # drop j ys)) =
   1.492 -    multiset_of (zip xs ys) + {#(x, y)#}"
   1.493 +  shows "mset (zip (take j xs @ x # drop j xs) (take j ys @ y # drop j ys)) =
   1.494 +    mset (zip xs ys) + {#(x, y)#}"
   1.495  using assms
   1.496  proof (induct xs ys arbitrary: x y j rule: list_induct2)
   1.497    case Nil
   1.498 @@ -2288,17 +2288,17 @@
   1.499        by (case_tac j) simp
   1.500      hence "k \<le> length xs"
   1.501        using Cons.prems by auto
   1.502 -    hence "multiset_of (zip (take k xs @ x # drop k xs) (take k ys @ y # drop k ys)) =
   1.503 -      multiset_of (zip xs ys) + {#(x, y)#}"
   1.504 +    hence "mset (zip (take k xs @ x # drop k xs) (take k ys @ y # drop k ys)) =
   1.505 +      mset (zip xs ys) + {#(x, y)#}"
   1.506        by (rule Cons.hyps(2))
   1.507      thus ?thesis
   1.508        unfolding k by (auto simp: add.commute union_lcomm)
   1.509    qed
   1.510  qed
   1.511  
   1.512 -lemma ex_multiset_of_zip_left:
   1.513 -  assumes "length xs = length ys" "multiset_of xs' = multiset_of xs"
   1.514 -  shows "\<exists>ys'. length ys' = length xs' \<and> multiset_of (zip xs' ys') = multiset_of (zip xs ys)"
   1.515 +lemma ex_mset_zip_left:
   1.516 +  assumes "length xs = length ys" "mset xs' = mset xs"
   1.517 +  shows "\<exists>ys'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys)"
   1.518  using assms
   1.519  proof (induct xs ys arbitrary: xs' rule: list_induct2)
   1.520    case Nil
   1.521 @@ -2307,57 +2307,57 @@
   1.522  next
   1.523    case (Cons x xs y ys xs')
   1.524    obtain j where j_len: "j < length xs'" and nth_j: "xs' ! j = x"
   1.525 -    by (metis Cons.prems in_set_conv_nth list.set_intros(1) multiset_of_eq_setD)
   1.526 +    by (metis Cons.prems in_set_conv_nth list.set_intros(1) mset_eq_setD)
   1.527  
   1.528    def xsa \<equiv> "take j xs' @ drop (Suc j) xs'"
   1.529 -  have "multiset_of xs' = {#x#} + multiset_of xsa"
   1.530 +  have "mset xs' = {#x#} + mset xsa"
   1.531      unfolding xsa_def using j_len nth_j
   1.532      by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id Cons_nth_drop_Suc
   1.533 -      multiset_of.simps(2) union_code add.commute)
   1.534 -  hence ms_x: "multiset_of xsa = multiset_of xs"
   1.535 -    by (metis Cons.prems add.commute add_right_imp_eq multiset_of.simps(2))
   1.536 +      mset.simps(2) union_code add.commute)
   1.537 +  hence ms_x: "mset xsa = mset xs"
   1.538 +    by (metis Cons.prems add.commute add_right_imp_eq mset.simps(2))
   1.539    then obtain ysa where
   1.540 -    len_a: "length ysa = length xsa" and ms_a: "multiset_of (zip xsa ysa) = multiset_of (zip xs ys)"
   1.541 +    len_a: "length ysa = length xsa" and ms_a: "mset (zip xsa ysa) = mset (zip xs ys)"
   1.542      using Cons.hyps(2) by blast
   1.543  
   1.544    def ys' \<equiv> "take j ysa @ y # drop j ysa"
   1.545    have xs': "xs' = take j xsa @ x # drop j xsa"
   1.546      using ms_x j_len nth_j Cons.prems xsa_def
   1.547      by (metis append_eq_append_conv append_take_drop_id diff_Suc_Suc Cons_nth_drop_Suc length_Cons
   1.548 -      length_drop size_multiset_of)
   1.549 +      length_drop size_mset)
   1.550    have j_len': "j \<le> length xsa"
   1.551      using j_len xs' xsa_def
   1.552      by (metis add_Suc_right append_take_drop_id length_Cons length_append less_eq_Suc_le not_less)
   1.553    have "length ys' = length xs'"
   1.554      unfolding ys'_def using Cons.prems len_a ms_x
   1.555 -    by (metis add_Suc_right append_take_drop_id length_Cons length_append multiset_of_eq_length)
   1.556 -  moreover have "multiset_of (zip xs' ys') = multiset_of (zip (x # xs) (y # ys))"
   1.557 +    by (metis add_Suc_right append_take_drop_id length_Cons length_append mset_eq_length)
   1.558 +  moreover have "mset (zip xs' ys') = mset (zip (x # xs) (y # ys))"
   1.559      unfolding xs' ys'_def
   1.560 -    by (rule trans[OF multiset_of_zip_take_Cons_drop_twice])
   1.561 +    by (rule trans[OF mset_zip_take_Cons_drop_twice])
   1.562        (auto simp: len_a ms_a j_len' add.commute)
   1.563    ultimately show ?case
   1.564      by blast
   1.565  qed
   1.566  
   1.567  lemma list_all2_reorder_left_invariance:
   1.568 -  assumes rel: "list_all2 R xs ys" and ms_x: "multiset_of xs' = multiset_of xs"
   1.569 -  shows "\<exists>ys'. list_all2 R xs' ys' \<and> multiset_of ys' = multiset_of ys"
   1.570 +  assumes rel: "list_all2 R xs ys" and ms_x: "mset xs' = mset xs"
   1.571 +  shows "\<exists>ys'. list_all2 R xs' ys' \<and> mset ys' = mset ys"
   1.572  proof -
   1.573    have len: "length xs = length ys"
   1.574      using rel list_all2_conv_all_nth by auto
   1.575    obtain ys' where
   1.576 -    len': "length xs' = length ys'" and ms_xy: "multiset_of (zip xs' ys') = multiset_of (zip xs ys)"
   1.577 -    using len ms_x by (metis ex_multiset_of_zip_left)
   1.578 +    len': "length xs' = length ys'" and ms_xy: "mset (zip xs' ys') = mset (zip xs ys)"
   1.579 +    using len ms_x by (metis ex_mset_zip_left)
   1.580    have "list_all2 R xs' ys'"
   1.581 -    using assms(1) len' ms_xy unfolding list_all2_iff by (blast dest: multiset_of_eq_setD)
   1.582 -  moreover have "multiset_of ys' = multiset_of ys"
   1.583 -    using len len' ms_xy map_snd_zip multiset_of_map by metis
   1.584 +    using assms(1) len' ms_xy unfolding list_all2_iff by (blast dest: mset_eq_setD)
   1.585 +  moreover have "mset ys' = mset ys"
   1.586 +    using len len' ms_xy map_snd_zip mset_map by metis
   1.587    ultimately show ?thesis
   1.588      by blast
   1.589  qed
   1.590  
   1.591 -lemma ex_multiset_of: "\<exists>xs. multiset_of xs = X"
   1.592 -  by (induct X) (simp, metis multiset_of.simps(2))
   1.593 +lemma ex_mset: "\<exists>xs. mset xs = X"
   1.594 +  by (induct X) (simp, metis mset.simps(2))
   1.595  
   1.596  bnf "'a multiset"
   1.597    map: image_mset
   1.598 @@ -2403,19 +2403,19 @@
   1.599      unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
   1.600      apply (rule ext)+
   1.601      apply auto
   1.602 -     apply (rule_tac x = "multiset_of (zip xs ys)" in exI; auto)
   1.603 -        apply (metis list_all2_lengthD map_fst_zip multiset_of_map)
   1.604 +     apply (rule_tac x = "mset (zip xs ys)" in exI; auto)
   1.605 +        apply (metis list_all2_lengthD map_fst_zip mset_map)
   1.606         apply (auto simp: list_all2_iff)[1]
   1.607 -      apply (metis list_all2_lengthD map_snd_zip multiset_of_map)
   1.608 +      apply (metis list_all2_lengthD map_snd_zip mset_map)
   1.609       apply (auto simp: list_all2_iff)[1]
   1.610      apply (rename_tac XY)
   1.611 -    apply (cut_tac X = XY in ex_multiset_of)
   1.612 +    apply (cut_tac X = XY in ex_mset)
   1.613      apply (erule exE)
   1.614      apply (rename_tac xys)
   1.615      apply (rule_tac x = "map fst xys" in exI)
   1.616 -    apply (auto simp: multiset_of_map)
   1.617 +    apply (auto simp: mset_map)
   1.618      apply (rule_tac x = "map snd xys" in exI)
   1.619 -    apply (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd)
   1.620 +    apply (auto simp: mset_map list_all2I subset_eq zip_map_fst_snd)
   1.621      done
   1.622  next
   1.623    show "\<And>z. z \<in> set_mset {#} \<Longrightarrow> False"