add_mset constructor in multisets
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Mon Sep 05 15:47:50 2016 +0200 (2016-09-05)
changeset 63793e68a0b651eb5
parent 63792 4ccb7e635477
child 63794 bcec0534aeea
add_mset constructor in multisets
NEWS
src/HOL/Algebra/Divisibility.thy
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Multiset_Order.thy
src/HOL/Library/multiset_order_simprocs.ML
src/HOL/Library/multiset_simprocs.ML
src/HOL/Library/multiset_simprocs_util.ML
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Probability/PMF_Impl.thy
src/HOL/ex/Bubblesort.thy
     1.1 --- a/NEWS	Mon Sep 05 15:00:37 2016 +0200
     1.2 +++ b/NEWS	Mon Sep 05 15:47:50 2016 +0200
     1.3 @@ -480,6 +480,7 @@
     1.4      le_multiset_plus_plus_left_iff ~> add_less_cancel_right
     1.5      le_multiset_plus_plus_right_iff ~> add_less_cancel_left
     1.6      add_eq_self_empty_iff ~> add_cancel_left_right
     1.7 +    mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right
     1.8  INCOMPATIBILITY.
     1.9  
    1.10  * Some typeclass constraints about multisets have been reduced from ordered or
    1.11 @@ -496,6 +497,96 @@
    1.12  ordered_ab_semigroup_monoid_add_imp_le.
    1.13  INCOMPATIBILITY.
    1.14  
    1.15 +* Multiset: single has been removed in favor of add_mset that roughly
    1.16 +corresponds to Set.insert. Some theorems have removed or changed:
    1.17 +  single_not_empty ~> add_mset_not_empty or empty_not_add_mset
    1.18 +  fold_mset_insert ~> fold_mset_add_mset
    1.19 +  image_mset_insert ~> image_mset_add_mset
    1.20 +  union_single_eq_diff
    1.21 +  multi_self_add_other_not_self
    1.22 +  diff_single_eq_union
    1.23 +INCOMPATIBILITY.
    1.24 +
    1.25 +* Multiset: some theorems have been changed to use add_mset instead of single:
    1.26 +  mset_add
    1.27 +  multi_self_add_other_not_self
    1.28 +  diff_single_eq_union
    1.29 +  union_single_eq_diff
    1.30 +  union_single_eq_member
    1.31 +  add_eq_conv_diff
    1.32 +  insert_noteq_member
    1.33 +  add_eq_conv_ex
    1.34 +  multi_member_split
    1.35 +  multiset_add_sub_el_shuffle
    1.36 +  mset_subset_eq_insertD
    1.37 +  mset_subset_insertD
    1.38 +  insert_subset_eq_iff
    1.39 +  insert_union_subset_iff
    1.40 +  multi_psub_of_add_self
    1.41 +  inter_add_left1
    1.42 +  inter_add_left2
    1.43 +  inter_add_right1
    1.44 +  inter_add_right2
    1.45 +  sup_union_left1
    1.46 +  sup_union_left2
    1.47 +  sup_union_right1
    1.48 +  sup_union_right2
    1.49 +  size_eq_Suc_imp_eq_union
    1.50 +  multi_nonempty_split
    1.51 +  mset_insort
    1.52 +  mset_update
    1.53 +  mult1I
    1.54 +  less_add
    1.55 +  mset_zip_take_Cons_drop_twice
    1.56 +  rel_mset_Zero
    1.57 +  msed_map_invL
    1.58 +  msed_map_invR
    1.59 +  msed_rel_invL
    1.60 +  msed_rel_invR
    1.61 +  le_multiset_right_total
    1.62 +  multiset_induct
    1.63 +  multiset_induct2_size
    1.64 +  multiset_induct2
    1.65 +INCOMPATIBILITY.
    1.66 +
    1.67 +* Multiset: the definitions of some constants have changed to use add_mset instead
    1.68 +of adding a single element:
    1.69 +  image_mset
    1.70 +  mset
    1.71 +  replicate_mset
    1.72 +  mult1
    1.73 +  pred_mset
    1.74 +  rel_mset'
    1.75 +  mset_insort
    1.76 +INCOMPATIBILITY.
    1.77 +
    1.78 +* Due to the above changes, the attributes of some multiset theorems have
    1.79 +been changed:
    1.80 +  insert_DiffM  [] ~> [simp]
    1.81 +  insert_DiffM2 [simp] ~> []
    1.82 +  diff_add_mset_swap [simp]
    1.83 +  fold_mset_add_mset [simp]
    1.84 +  diff_diff_add [simp] (for multisets only)
    1.85 +  diff_cancel [simp] ~> []
    1.86 +  count_single [simp] ~> []
    1.87 +  set_mset_single [simp] ~> []
    1.88 +  size_multiset_single [simp] ~> []
    1.89 +  size_single [simp] ~> []
    1.90 +  image_mset_single [simp] ~> []
    1.91 +  mset_subset_eq_mono_add_right_cancel [simp] ~> []
    1.92 +  mset_subset_eq_mono_add_left_cancel [simp] ~> []
    1.93 +  fold_mset_single [simp] ~> []
    1.94 +  subset_eq_empty [simp] ~> []
    1.95 +INCOMPATIBILITY.
    1.96 +
    1.97 +* The order of the variables in the second cases of multiset_induct,
    1.98 +multiset_induct2_size, multiset_induct2 has been changed (e.g. Add A a ~> Add a A).
    1.99 +INCOMPATIBILITY.
   1.100 +
   1.101 +* There is now a simplification procedure on multisets. It mimics the behavior
   1.102 +of the procedure on natural numbers.
   1.103 +INCOMPATIBILITY.
   1.104 +
   1.105  * Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
   1.106  INCOMPATIBILITY.
   1.107  
     2.1 --- a/src/HOL/Algebra/Divisibility.thy	Mon Sep 05 15:00:37 2016 +0200
     2.2 +++ b/src/HOL/Algebra/Divisibility.thy	Mon Sep 05 15:47:50 2016 +0200
     2.3 @@ -2051,11 +2051,11 @@
     2.4      from cP csP
     2.5          have tP: "\<forall>x\<in>set (c#cs). P x" by simp
     2.6      from mset a
     2.7 -    have "mset (map (assocs G) (c#cs)) = mset Cs' + {#a#}" by simp
     2.8 +    have "mset (map (assocs G) (c#cs)) = add_mset a (mset Cs')" by simp
     2.9      from tP this
    2.10      show "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and>
    2.11                 mset (map (assocs G) cs) =
    2.12 -               mset Cs' + {#a#}" by fast
    2.13 +               add_mset a (mset Cs')" by fast
    2.14    qed
    2.15    thus ?thesis by (simp add: fmset_def)
    2.16  qed
     3.1 --- a/src/HOL/Library/DAList_Multiset.thy	Mon Sep 05 15:00:37 2016 +0200
     3.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Mon Sep 05 15:47:50 2016 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4  
     3.5  lemma [code, code del]: "Multiset.is_empty = Multiset.is_empty" ..
     3.6  
     3.7 -lemma [code, code del]: "single = single" ..
     3.8 +lemma [code, code del]: "add_mset = add_mset" ..
     3.9  
    3.10  lemma [code, code del]: "plus = (plus :: 'a multiset \<Rightarrow> _)" ..
    3.11  
    3.12 @@ -210,13 +210,15 @@
    3.13    finally show ?thesis by (simp add: is_empty_Bag_impl.rep_eq)
    3.14  qed
    3.15  
    3.16 -lemma single_Bag [code]: "{#x#} = Bag (DAList.update x 1 DAList.empty)"
    3.17 -  by (simp add: multiset_eq_iff alist.Alist_inverse update.rep_eq empty.rep_eq)
    3.18 -
    3.19  lemma union_Bag [code]: "Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)"
    3.20    by (rule multiset_eqI)
    3.21      (simp add: count_of_join_raw alist.Alist_inverse distinct_join_raw join_def)
    3.22  
    3.23 +lemma add_mset_Bag [code]: "add_mset x (Bag xs) =
    3.24 +    Bag (join (\<lambda>x (n1, n2). n1 + n2) (DAList.update x 1 DAList.empty) xs)"
    3.25 +  unfolding add_mset_add_single[of x "Bag xs"] union_Bag[symmetric]
    3.26 +  by (simp add: multiset_eq_iff update.rep_eq empty.rep_eq)
    3.27 +
    3.28  lemma minus_Bag [code]: "Bag xs - Bag ys = Bag (subtract_entries xs ys)"
    3.29    by (rule multiset_eqI)
    3.30      (simp add: count_of_subtract_entries_raw alist.Alist_inverse
    3.31 @@ -386,7 +388,7 @@
    3.32    unfolding image_mset_def
    3.33  proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1])
    3.34    fix a n m
    3.35 -  show "Bag (single_alist_entry (f a) n) + m = ((op + \<circ> single \<circ> f) a ^^ n) m" (is "?l = ?r")
    3.36 +  show "Bag (single_alist_entry (f a) n) + m = ((add_mset \<circ> f) a ^^ n) m" (is "?l = ?r")
    3.37    proof (rule multiset_eqI)
    3.38      fix x
    3.39      have "count ?r x = (if x = f a then n + count m x else count m x)"
     4.1 --- a/src/HOL/Library/Multiset.thy	Mon Sep 05 15:00:37 2016 +0200
     4.2 +++ b/src/HOL/Library/Multiset.thy	Mon Sep 05 15:47:50 2016 +0200
     4.3 @@ -98,21 +98,43 @@
     4.4  
     4.5  end
     4.6  
     4.7 -
     4.8 -lift_definition single :: "'a \<Rightarrow> 'a multiset" is "\<lambda>a b. if b = a then 1 else 0"
     4.9 -by (rule only1_in_multiset)
    4.10 +lemma add_mset_in_multiset:
    4.11 +  assumes M: \<open>M \<in> multiset\<close>
    4.12 +  shows \<open>(\<lambda>b. if b = a then Suc (M b) else M b) \<in> multiset\<close>
    4.13 +  using assms by (simp add: multiset_def insert_Collect[symmetric])
    4.14 +
    4.15 +lift_definition add_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is
    4.16 +  "\<lambda>a M b. if b = a then Suc (M b) else M b"
    4.17 +by (rule add_mset_in_multiset)
    4.18  
    4.19  syntax
    4.20    "_multiset" :: "args \<Rightarrow> 'a multiset"    ("{#(_)#}")
    4.21  translations
    4.22 -  "{#x, xs#}" == "{#x#} + {#xs#}"
    4.23 -  "{#x#}" == "CONST single x"
    4.24 +  "{#x, xs#}" == "CONST add_mset x {#xs#}"
    4.25 +  "{#x#}" == "CONST add_mset x {#}"
    4.26  
    4.27  lemma count_empty [simp]: "count {#} a = 0"
    4.28    by (simp add: zero_multiset.rep_eq)
    4.29  
    4.30 -lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
    4.31 -  by (simp add: single.rep_eq)
    4.32 +lemma count_add_mset [simp]:
    4.33 +  "count (add_mset b A) a = (if b = a then Suc (count A a) else count A a)"
    4.34 +  by (simp add: add_mset.rep_eq)
    4.35 +
    4.36 +lemma count_single: "count {#b#} a = (if b = a then 1 else 0)"
    4.37 +  by simp
    4.38 +
    4.39 +lemma
    4.40 +  add_mset_not_empty [simp]: \<open>add_mset a A \<noteq> {#}\<close> and
    4.41 +  empty_not_add_mset [simp]: "{#} \<noteq> add_mset a A"
    4.42 +  by (auto simp: multiset_eq_iff)
    4.43 +
    4.44 +lemma add_mset_add_mset_same_iff [simp]:
    4.45 +  "add_mset a A = add_mset a B \<longleftrightarrow> A = B"
    4.46 +  by (auto simp: multiset_eq_iff)
    4.47 +
    4.48 +lemma add_mset_commute:
    4.49 +  "add_mset x (add_mset y M) = add_mset y (add_mset x M)"
    4.50 +  by (auto simp: multiset_eq_iff)
    4.51  
    4.52  
    4.53  subsection \<open>Basic operations\<close>
    4.54 @@ -209,7 +231,7 @@
    4.55    "set_mset {#} = {}"
    4.56    by (simp add: set_mset_def)
    4.57  
    4.58 -lemma set_mset_single [simp]:
    4.59 +lemma set_mset_single:
    4.60    "set_mset {#b#} = {b}"
    4.61    by (simp add: set_mset_def)
    4.62  
    4.63 @@ -221,6 +243,10 @@
    4.64    "finite (set_mset M)"
    4.65    using count [of M] by (simp add: multiset_def)
    4.66  
    4.67 +lemma set_mset_add_mset_insert [simp]: \<open>set_mset (add_mset a A) = insert a (set_mset A)\<close>
    4.68 +  by (auto simp del: count_greater_eq_Suc_zero_iff
    4.69 +      simp: count_greater_eq_Suc_zero_iff[symmetric] split: if_splits)
    4.70 +
    4.71  
    4.72  subsubsection \<open>Union\<close>
    4.73  
    4.74 @@ -232,6 +258,17 @@
    4.75    "set_mset (M + N) = set_mset M \<union> set_mset N"
    4.76    by (simp only: set_eq_iff count_greater_zero_iff [symmetric] count_union) simp
    4.77  
    4.78 +lemma union_mset_add_mset_left [simp]:
    4.79 +  "add_mset a A + B = add_mset a (A + B)"
    4.80 +  by (auto simp: multiset_eq_iff)
    4.81 +
    4.82 +lemma union_mset_add_mset_right [simp]:
    4.83 +  "A + add_mset a B = add_mset a (A + B)"
    4.84 +  by (auto simp: multiset_eq_iff)
    4.85 +
    4.86 +lemma add_mset_add_single: \<open>add_mset a A = A + {#a#}\<close>
    4.87 +  by (subst union_mset_add_mset_right, subst add.comm_neutral) standard
    4.88 +
    4.89  
    4.90  subsubsection \<open>Difference\<close>
    4.91  
    4.92 @@ -242,6 +279,10 @@
    4.93    "count (M - N) a = count M a - count N a"
    4.94    by (simp add: minus_multiset.rep_eq)
    4.95  
    4.96 +lemma add_mset_diff_bothsides:
    4.97 +  \<open>add_mset a M - add_mset a A = M - A\<close>
    4.98 +  by (auto simp: multiset_eq_iff)
    4.99 +
   4.100  lemma in_diff_count:
   4.101    "a \<in># M - N \<longleftrightarrow> count N a < count M a"
   4.102    by (simp add: set_mset_def)
   4.103 @@ -284,13 +325,13 @@
   4.104  lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
   4.105    by rule (fact Groups.diff_zero, fact Groups.zero_diff)
   4.106  
   4.107 -lemma diff_cancel [simp]: "A - A = {#}"
   4.108 +lemma diff_cancel: "A - A = {#}"
   4.109    by (fact Groups.diff_cancel)
   4.110  
   4.111 -lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)"
   4.112 +lemma diff_union_cancelR: "M + N - N = (M::'a multiset)"
   4.113    by (fact add_diff_cancel_right')
   4.114  
   4.115 -lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)"
   4.116 +lemma diff_union_cancelL: "N + M - N = (M::'a multiset)"
   4.117    by (fact add_diff_cancel_left')
   4.118  
   4.119  lemma diff_right_commute:
   4.120 @@ -303,24 +344,33 @@
   4.121    shows "M - (N + Q) = M - N - Q"
   4.122    by (rule sym) (fact diff_diff_add)
   4.123  
   4.124 -lemma insert_DiffM: "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
   4.125 +lemma insert_DiffM [simp]: "x \<in># M \<Longrightarrow> add_mset x (M - {#x#}) = M"
   4.126    by (clarsimp simp: multiset_eq_iff)
   4.127  
   4.128 -lemma insert_DiffM2 [simp]: "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
   4.129 -  by (clarsimp simp: multiset_eq_iff)
   4.130 -
   4.131 -lemma diff_union_swap: "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
   4.132 +lemma insert_DiffM2: "x \<in># M \<Longrightarrow> (M - {#x#}) + {#x#} = M"
   4.133 +  by simp
   4.134 +
   4.135 +lemma diff_union_swap: "a \<noteq> b \<Longrightarrow> add_mset b (M - {#a#}) = add_mset b M - {#a#}"
   4.136    by (auto simp add: multiset_eq_iff)
   4.137  
   4.138 +lemma diff_add_mset_swap [simp]: "b \<notin># A \<Longrightarrow> add_mset b M - A = add_mset b (M - A)"
   4.139 +  by (auto simp add: multiset_eq_iff simp: not_in_iff)
   4.140 +
   4.141 +lemma diff_union_swap2 [simp]: "y \<in># M \<Longrightarrow> add_mset x M - {#y#} = add_mset x (M - {#y#})"
   4.142 +  by (metis add_mset_diff_bothsides diff_union_swap diff_zero insert_DiffM)
   4.143 +
   4.144 +lemma diff_diff_add_mset [simp]: "(M::'a multiset) - N - P = M - (N + P)"
   4.145 +  by (rule diff_diff_add)
   4.146 +
   4.147  lemma diff_union_single_conv:
   4.148    "a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})"
   4.149    by (simp add: multiset_eq_iff Suc_le_eq)
   4.150  
   4.151  lemma mset_add [elim?]:
   4.152    assumes "a \<in># A"
   4.153 -  obtains B where "A = B + {#a#}"
   4.154 +  obtains B where "A = add_mset a B"
   4.155  proof -
   4.156 -  from assms have "A = (A - {#a#}) + {#a#}"
   4.157 +  from assms have "A = add_mset a (A - {#a#})"
   4.158      by simp
   4.159    with that show thesis .
   4.160  qed
   4.161 @@ -332,9 +382,6 @@
   4.162  
   4.163  subsubsection \<open>Equality of multisets\<close>
   4.164  
   4.165 -lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
   4.166 -  by (simp add: multiset_eq_iff)
   4.167 -
   4.168  lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
   4.169    by (auto simp add: multiset_eq_iff)
   4.170  
   4.171 @@ -344,20 +391,30 @@
   4.172  lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}"
   4.173    by (auto simp add: multiset_eq_iff)
   4.174  
   4.175 -lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \<longleftrightarrow> False"
   4.176 +lemma multi_self_add_other_not_self [simp]: "M = add_mset x M \<longleftrightarrow> False"
   4.177    by (auto simp add: multiset_eq_iff)
   4.178  
   4.179 +lemma add_mset_remove_trivial [simp]: \<open>add_mset x M - {#x#} = M\<close>
   4.180 +  by (auto simp: multiset_eq_iff)
   4.181 +
   4.182  lemma diff_single_trivial: "\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
   4.183    by (auto simp add: multiset_eq_iff not_in_iff)
   4.184  
   4.185 -lemma diff_single_eq_union: "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = N + {#x#}"
   4.186 +lemma diff_single_eq_union: "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = add_mset x N"
   4.187 +  by auto
   4.188 +
   4.189 +lemma union_single_eq_diff: "add_mset x M = N \<Longrightarrow> M = N - {#x#}"
   4.190 +  unfolding add_mset_add_single[of _ M] by (fact add_implies_diff)
   4.191 +
   4.192 +lemma union_single_eq_member: "add_mset x M = N \<Longrightarrow> x \<in># N"
   4.193    by auto
   4.194  
   4.195 -lemma union_single_eq_diff: "M + {#x#} = N \<Longrightarrow> M = N - {#x#}"
   4.196 -  by (auto dest: sym)
   4.197 -
   4.198 -lemma union_single_eq_member: "M + {#x#} = N \<Longrightarrow> x \<in># N"
   4.199 -  by auto
   4.200 +lemma add_mset_remove_trivial_If:
   4.201 +  "add_mset a (N - {#a#}) = (if a \<in># N then N else add_mset a N)"
   4.202 +  by (simp add: diff_single_trivial)
   4.203 +
   4.204 +lemma add_mset_remove_trivial_eq: \<open>N = add_mset a (N - {#a#}) \<longleftrightarrow> a \<in># N\<close>
   4.205 +  by (auto simp: add_mset_remove_trivial_If)
   4.206  
   4.207  lemma union_is_single:
   4.208    "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N = {#} \<or> M = {#} \<and> N = {#a#}"
   4.209 @@ -372,56 +429,61 @@
   4.210    by (auto simp add: eq_commute [of "{#a#}" "M + N"] union_is_single)
   4.211  
   4.212  lemma add_eq_conv_diff:
   4.213 -  "M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#}"
   4.214 +  "add_mset a M = add_mset b N \<longleftrightarrow> M = N \<and> a = b \<or> M = add_mset b (N - {#a#}) \<and> N = add_mset a (M - {#b#})"
   4.215    (is "?lhs \<longleftrightarrow> ?rhs")
   4.216  (* shorter: by (simp add: multiset_eq_iff) fastforce *)
   4.217  proof
   4.218    show ?lhs if ?rhs
   4.219      using that
   4.220 -    by (auto simp add: add.assoc add.commute [of "{#b#}"])
   4.221 -      (drule sym, simp add: add.assoc [symmetric])
   4.222 +    by (auto simp add: add_mset_commute[of a b])
   4.223    show ?rhs if ?lhs
   4.224    proof (cases "a = b")
   4.225      case True with \<open>?lhs\<close> show ?thesis by simp
   4.226    next
   4.227      case False
   4.228 -    from \<open>?lhs\<close> have "a \<in># N + {#b#}" by (rule union_single_eq_member)
   4.229 +    from \<open>?lhs\<close> have "a \<in># add_mset b N" by (rule union_single_eq_member)
   4.230      with False have "a \<in># N" by auto
   4.231 -    moreover from \<open>?lhs\<close> have "M = N + {#b#} - {#a#}" by (rule union_single_eq_diff)
   4.232 +    moreover from \<open>?lhs\<close> have "M = add_mset b N - {#a#}" by (rule union_single_eq_diff)
   4.233      moreover note False
   4.234 -    ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#a#}"] diff_union_swap)
   4.235 +    ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#a#}"])
   4.236    qed
   4.237  qed
   4.238  
   4.239 +lemma add_mset_eq_single [iff]: "add_mset b M = {#a#} \<longleftrightarrow> b = a \<and> M = {#}"
   4.240 +  by (auto simp: add_eq_conv_diff)
   4.241 +
   4.242 +lemma single_eq_add_mset [iff]: "{#a#} = add_mset b M \<longleftrightarrow> b = a \<and> M = {#}"
   4.243 +  by (auto simp: add_eq_conv_diff)
   4.244 +
   4.245  lemma insert_noteq_member:
   4.246 -  assumes BC: "B + {#b#} = C + {#c#}"
   4.247 +  assumes BC: "add_mset b B = add_mset c C"
   4.248     and bnotc: "b \<noteq> c"
   4.249    shows "c \<in># B"
   4.250  proof -
   4.251 -  have "c \<in># C + {#c#}" by simp
   4.252 +  have "c \<in># add_mset c C" by simp
   4.253    have nc: "\<not> c \<in># {#b#}" using bnotc by simp
   4.254 -  then have "c \<in># B + {#b#}" using BC by simp
   4.255 +  then have "c \<in># add_mset b B" using BC by simp
   4.256    then show "c \<in># B" using nc by simp
   4.257  qed
   4.258  
   4.259  lemma add_eq_conv_ex:
   4.260 -  "(M + {#a#} = N + {#b#}) =
   4.261 -    (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
   4.262 +  "(add_mset a M = add_mset b N) =
   4.263 +    (M = N \<and> a = b \<or> (\<exists>K. M = add_mset b K \<and> N = add_mset a K))"
   4.264    by (auto simp add: add_eq_conv_diff)
   4.265  
   4.266 -lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
   4.267 +lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = add_mset x A"
   4.268    by (rule exI [where x = "M - {#x#}"]) simp
   4.269  
   4.270  lemma multiset_add_sub_el_shuffle:
   4.271    assumes "c \<in># B"
   4.272      and "b \<noteq> c"
   4.273 -  shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}"
   4.274 +  shows "add_mset b (B - {#c#}) = add_mset b B - {#c#}"
   4.275  proof -
   4.276 -  from \<open>c \<in># B\<close> obtain A where B: "B = A + {#c#}"
   4.277 +  from \<open>c \<in># B\<close> obtain A where B: "B = add_mset c A"
   4.278      by (blast dest: multi_member_split)
   4.279 -  have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
   4.280 -  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
   4.281 -    by (simp add: ac_simps)
   4.282 +  have "add_mset b A = add_mset c (add_mset b A) - {#c#}" by simp
   4.283 +  then have "add_mset b A = add_mset b (add_mset c A) - {#c#}"
   4.284 +    by (simp add: ac_simps \<open>b \<noteq> c\<close>)
   4.285    then show ?thesis using B by simp
   4.286  qed
   4.287  
   4.288 @@ -454,6 +516,9 @@
   4.289    by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
   4.290    \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
   4.291  
   4.292 +interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<le>#" "op <#"
   4.293 +  by standard
   4.294 +
   4.295  lemma mset_subset_eqI:
   4.296    "(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B"
   4.297    by (simp add: subseteq_mset_def)
   4.298 @@ -472,36 +537,37 @@
   4.299  interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<le>#" "op <#" "op -"
   4.300    by standard (simp, fact mset_subset_eq_exists_conv)
   4.301  
   4.302 -interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<le>#" "op <#"
   4.303 -  by standard
   4.304 -
   4.305 -lemma mset_subset_eq_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
   4.306 +lemma mset_subset_eq_mono_add_right_cancel: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
   4.307     by (fact subset_mset.add_le_cancel_right)
   4.308 - 
   4.309 -lemma mset_subset_eq_mono_add_left_cancel [simp]: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B"
   4.310 +
   4.311 +lemma mset_subset_eq_mono_add_left_cancel: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B"
   4.312     by (fact subset_mset.add_le_cancel_left)
   4.313 - 
   4.314 +
   4.315  lemma mset_subset_eq_mono_add: "(A::'a multiset) \<subseteq># B \<Longrightarrow> C \<subseteq># D \<Longrightarrow> A + C \<subseteq># B + D"
   4.316     by (fact subset_mset.add_mono)
   4.317 - 
   4.318 +
   4.319  lemma mset_subset_eq_add_left: "(A::'a multiset) \<subseteq># A + B"
   4.320     by simp
   4.321 - 
   4.322 +
   4.323  lemma mset_subset_eq_add_right: "B \<subseteq># (A::'a multiset) + B"
   4.324     by simp
   4.325 - 
   4.326 +
   4.327  lemma single_subset_iff [simp]:
   4.328    "{#a#} \<subseteq># M \<longleftrightarrow> a \<in># M"
   4.329    by (auto simp add: subseteq_mset_def Suc_le_eq)
   4.330  
   4.331  lemma mset_subset_eq_single: "a \<in># B \<Longrightarrow> {#a#} \<subseteq># B"
   4.332    by (simp add: subseteq_mset_def Suc_le_eq)
   4.333 - 
   4.334 +
   4.335 +lemma mset_subset_eq_add_mset_cancel: \<open>add_mset a A \<subseteq># add_mset a B \<longleftrightarrow> A \<subseteq># B\<close>
   4.336 +  unfolding add_mset_add_single[of _ A] add_mset_add_single[of _ B]
   4.337 +  by (rule mset_subset_eq_mono_add_right_cancel)
   4.338 +
   4.339  lemma multiset_diff_union_assoc:
   4.340    fixes A B C D :: "'a multiset"
   4.341    shows "C \<subseteq># B \<Longrightarrow> A + B - C = A + (B - C)"
   4.342    by (fact subset_mset.diff_add_assoc)
   4.343 - 
   4.344 +
   4.345  lemma mset_subset_eq_multiset_union_diff_commute:
   4.346    fixes A B C D :: "'a multiset"
   4.347    shows "B \<subseteq># A \<Longrightarrow> A - B + C = A + C - B"
   4.348 @@ -520,7 +586,7 @@
   4.349      by (simp add: subseteq_mset_def)
   4.350    finally show ?thesis by simp
   4.351  qed
   4.352 -  
   4.353 +
   4.354  lemma mset_subsetD:
   4.355    "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
   4.356    by (auto intro: mset_subset_eqD [of A])
   4.357 @@ -530,7 +596,7 @@
   4.358    by (metis mset_subset_eqD subsetI)
   4.359  
   4.360  lemma mset_subset_eq_insertD:
   4.361 -  "A + {#x#} \<subseteq># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
   4.362 +  "add_mset x A \<subseteq># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
   4.363  apply (rule conjI)
   4.364   apply (simp add: mset_subset_eqD)
   4.365   apply (clarsimp simp: subset_mset_def subseteq_mset_def)
   4.366 @@ -540,7 +606,7 @@
   4.367  done
   4.368  
   4.369  lemma mset_subset_insertD:
   4.370 -  "A + {#x#} \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
   4.371 +  "add_mset x A \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
   4.372    by (rule mset_subset_eq_insertD) simp
   4.373  
   4.374  lemma mset_subset_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
   4.375 @@ -548,9 +614,9 @@
   4.376  
   4.377  lemma empty_le [simp]: "{#} \<subseteq># A"
   4.378    unfolding mset_subset_eq_exists_conv by auto
   4.379 - 
   4.380 +
   4.381  lemma insert_subset_eq_iff:
   4.382 -  "{#a#} + A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B - {#a#}"
   4.383 +  "add_mset a A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B - {#a#}"
   4.384    using le_diff_conv2 [of "Suc 0" "count B a" "count A a"]
   4.385    apply (auto simp add: subseteq_mset_def not_in_iff Suc_le_eq)
   4.386    apply (rule ccontr)
   4.387 @@ -558,24 +624,25 @@
   4.388    done
   4.389  
   4.390  lemma insert_union_subset_iff:
   4.391 -  "{#a#} + A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B - {#a#}"
   4.392 -  by (auto simp add: insert_subset_eq_iff subset_mset_def insert_DiffM)
   4.393 +  "add_mset a A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B - {#a#}"
   4.394 +  by (auto simp add: insert_subset_eq_iff subset_mset_def)
   4.395  
   4.396  lemma subset_eq_diff_conv:
   4.397    "A - C \<subseteq># B \<longleftrightarrow> A \<subseteq># B + C"
   4.398    by (simp add: subseteq_mset_def le_diff_conv)
   4.399  
   4.400 -lemma subset_eq_empty [simp]: "M \<subseteq># {#} \<longleftrightarrow> M = {#}"
   4.401 -  unfolding mset_subset_eq_exists_conv by auto
   4.402 -
   4.403 -lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}"
   4.404 +lemma subset_eq_empty: "M \<subseteq># {#} \<longleftrightarrow> M = {#}"
   4.405 +  by auto
   4.406 +
   4.407 +lemma multi_psub_of_add_self [simp]: "A \<subset># add_mset x A"
   4.408    by (auto simp: subset_mset_def subseteq_mset_def)
   4.409  
   4.410  lemma multi_psub_self[simp]: "(A::'a multiset) \<subset># A = False"
   4.411    by simp
   4.412  
   4.413 -lemma mset_subset_add_bothsides: "N + {#x#} \<subset># M + {#x#} \<Longrightarrow> N \<subset># M"
   4.414 -  by (fact subset_mset.add_less_imp_less_right)
   4.415 +lemma mset_subset_add_mset [simp]: "add_mset x N \<subset># add_mset x M \<longleftrightarrow> N \<subset># M"
   4.416 +  unfolding add_mset_add_single[of _ N] add_mset_add_single[of _ M]
   4.417 +  by (fact subset_mset.add_less_cancel_right)
   4.418  
   4.419  lemma mset_subset_empty_nonempty: "{#} \<subset># S \<longleftrightarrow> S \<noteq> {#}"
   4.420    by (fact subset_mset.zero_less_iff_neq_zero)
   4.421 @@ -657,22 +724,37 @@
   4.422    qed
   4.423  qed
   4.424  
   4.425 +lemma add_mset_inter_add_mset:
   4.426 +  "add_mset a A #\<inter> add_mset a B = add_mset a (A #\<inter> B)"
   4.427 +  by (metis add_mset_add_single add_mset_diff_bothsides diff_subset_eq_self multiset_inter_def
   4.428 +      subset_mset.diff_add_assoc2)
   4.429 +
   4.430 +lemma add_mset_disjoint [simp]:
   4.431 +  "add_mset a A #\<inter> B = {#} \<longleftrightarrow> a \<notin># B \<and> A #\<inter> B = {#}"
   4.432 +  "{#} = add_mset a A #\<inter> B \<longleftrightarrow> a \<notin># B \<and> {#} = A #\<inter> B"
   4.433 +  by (auto simp: disjunct_not_in)
   4.434 +
   4.435 +lemma disjoint_add_mset [simp]:
   4.436 +  "B #\<inter> add_mset a A = {#} \<longleftrightarrow> a \<notin># B \<and> B #\<inter> A = {#}"
   4.437 +  "{#} = A #\<inter> add_mset b B \<longleftrightarrow> b \<notin># A \<and> {#} = A #\<inter> B"
   4.438 +  by (auto simp: disjunct_not_in)
   4.439 +
   4.440  lemma empty_inter [simp]: "{#} #\<inter> M = {#}"
   4.441    by (simp add: multiset_eq_iff)
   4.442  
   4.443  lemma inter_empty [simp]: "M #\<inter> {#} = {#}"
   4.444    by (simp add: multiset_eq_iff)
   4.445  
   4.446 -lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = M #\<inter> N"
   4.447 +lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) #\<inter> N = M #\<inter> N"
   4.448    by (simp add: multiset_eq_iff not_in_iff)
   4.449  
   4.450 -lemma inter_add_left2: "x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = (M #\<inter> (N - {#x#})) + {#x#}"
   4.451 +lemma inter_add_left2: "x \<in># N \<Longrightarrow> (add_mset x M) #\<inter> N = add_mset x (M #\<inter> (N - {#x#}))"
   4.452    by (auto simp add: multiset_eq_iff elim: mset_add)
   4.453  
   4.454 -lemma inter_add_right1: "\<not> x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = N #\<inter> M"
   4.455 +lemma inter_add_right1: "\<not> x \<in># N \<Longrightarrow> N #\<inter> (add_mset x M) = N #\<inter> M"
   4.456    by (simp add: multiset_eq_iff not_in_iff)
   4.457  
   4.458 -lemma inter_add_right2: "x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = ((N - {#x#}) #\<inter> M) + {#x#}"
   4.459 +lemma inter_add_right2: "x \<in># N \<Longrightarrow> N #\<inter> (add_mset x M) = add_mset x ((N - {#x#}) #\<inter> M)"
   4.460    by (auto simp add: multiset_eq_iff elim: mset_add)
   4.461  
   4.462  lemma disjunct_set_mset_diff:
   4.463 @@ -747,16 +829,16 @@
   4.464  lemma sup_empty [simp]: "M #\<union> {#} = M"
   4.465    by (simp add: multiset_eq_iff)
   4.466  
   4.467 -lemma sup_union_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> N) + {#x#}"
   4.468 +lemma sup_union_left1 [simp]: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) #\<union> N = add_mset x (M #\<union> N)"
   4.469    by (simp add: multiset_eq_iff not_in_iff)
   4.470  
   4.471 -lemma sup_union_left2: "x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> (N - {#x#})) + {#x#}"
   4.472 +lemma sup_union_left2: "x \<in># N \<Longrightarrow> (add_mset x M) #\<union> N = add_mset x (M #\<union> (N - {#x#}))"
   4.473    by (simp add: multiset_eq_iff)
   4.474  
   4.475 -lemma sup_union_right1: "\<not> x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = (N #\<union> M) + {#x#}"
   4.476 +lemma sup_union_right1 [simp]: "\<not> x \<in># N \<Longrightarrow> N #\<union> (add_mset x M) = add_mset x (N #\<union> M)"
   4.477    by (simp add: multiset_eq_iff not_in_iff)
   4.478  
   4.479 -lemma sup_union_right2: "x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N - {#x#}) #\<union> M) + {#x#}"
   4.480 +lemma sup_union_right2: "x \<in># N \<Longrightarrow> N #\<union> (add_mset x M) = add_mset x ((N - {#x#}) #\<union> M)"
   4.481    by (simp add: multiset_eq_iff)
   4.482  
   4.483  lemma sup_union_distrib_left:
   4.484 @@ -775,12 +857,105 @@
   4.485    "A + B - A #\<union> B = A #\<inter> B"
   4.486    by (auto simp add: multiset_eq_iff)
   4.487  
   4.488 +lemma add_mset_union:
   4.489 +  \<open>add_mset a A #\<union> add_mset a B = add_mset a (A #\<union> B)\<close>
   4.490 +  by (auto simp: multiset_eq_iff max_def)
   4.491 +
   4.492  
   4.493  subsubsection \<open>Subset is an order\<close>
   4.494  
   4.495  interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto
   4.496  
   4.497  
   4.498 +subsubsection \<open>Simprocs\<close>
   4.499 +
   4.500 +fun repeat_mset :: "nat \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   4.501 +  "repeat_mset 0 _ = {#}" |
   4.502 +  "repeat_mset (Suc n) A = A + repeat_mset n A"
   4.503 +
   4.504 +lemma count_repeat_mset [simp]: "count (repeat_mset i A) a = i * count A a"
   4.505 +  by (induction i) auto
   4.506 +
   4.507 +lemma repeat_mset_right [simp]: "repeat_mset a (repeat_mset b A) = repeat_mset (a * b) A"
   4.508 +  by (auto simp: multiset_eq_iff left_diff_distrib')
   4.509 +
   4.510 +lemma left_diff_repeat_mset_distrib': \<open>repeat_mset (i - j) u = repeat_mset i u - repeat_mset j u\<close>
   4.511 +  by (auto simp: multiset_eq_iff left_diff_distrib')
   4.512 +
   4.513 +lemma mset_diff_add_eq1:
   4.514 +  "j \<le> (i::nat) \<Longrightarrow> ((repeat_mset i u + m) - (repeat_mset j u + n)) = ((repeat_mset (i-j) u + m) - n)"
   4.515 +  by (auto simp: multiset_eq_iff nat_diff_add_eq1)
   4.516 +
   4.517 +lemma mset_diff_add_eq2:
   4.518 +  "i \<le> (j::nat) \<Longrightarrow> ((repeat_mset i u + m) - (repeat_mset j u + n)) = (m - (repeat_mset (j-i) u + n))"
   4.519 +  by (auto simp: multiset_eq_iff nat_diff_add_eq2)
   4.520 +
   4.521 +lemma mset_eq_add_iff1:
   4.522 +   "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m = repeat_mset j u + n) = (repeat_mset (i-j) u + m = n)"
   4.523 +  by (auto simp: multiset_eq_iff nat_eq_add_iff1)
   4.524 +
   4.525 +lemma mset_eq_add_iff2:
   4.526 +   "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m = repeat_mset j u + n) = (m = repeat_mset (j-i) u + n)"
   4.527 +  by (auto simp: multiset_eq_iff nat_eq_add_iff2)
   4.528 +
   4.529 +lemma mset_subseteq_add_iff1:
   4.530 +  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subseteq># repeat_mset j u + n) = (repeat_mset (i-j) u + m \<subseteq># n)"
   4.531 +  by (auto simp add: subseteq_mset_def nat_le_add_iff1)
   4.532 +
   4.533 +lemma mset_subseteq_add_iff2:
   4.534 +  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subseteq># repeat_mset j u + n) = (m \<subseteq># repeat_mset (j-i) u + n)"
   4.535 +  by (auto simp add: subseteq_mset_def nat_le_add_iff2)
   4.536 +
   4.537 +lemma mset_subset_add_iff1:
   4.538 +  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (repeat_mset (i-j) u + m \<subset># n)"
   4.539 +  unfolding subset_mset_def by (simp add: mset_eq_add_iff1 mset_subseteq_add_iff1)
   4.540 +
   4.541 +lemma mset_subset_add_iff2:
   4.542 +  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (m \<subset># repeat_mset (j-i) u + n)"
   4.543 +  unfolding subset_mset_def by (simp add: mset_eq_add_iff2 mset_subseteq_add_iff2)
   4.544 +
   4.545 +lemma left_add_mult_distrib_mset:
   4.546 +  "repeat_mset i u + (repeat_mset j u + k) = repeat_mset (i+j) u + k"
   4.547 +  by (auto simp: multiset_eq_iff add_mult_distrib)
   4.548 +
   4.549 +lemma repeat_mset_cancel1: "repeat_mset a A = repeat_mset a B \<longleftrightarrow> A = B \<or> a = 0"
   4.550 +  by (auto simp: multiset_eq_iff)
   4.551 +
   4.552 +lemma repeat_mset_cancel2: "repeat_mset a A = repeat_mset b A \<longleftrightarrow> a = b \<or> A = {#}"
   4.553 +  by (auto simp: multiset_eq_iff)
   4.554 +
   4.555 +lemma repeat_mset_distrib [simp]:
   4.556 +  "repeat_mset n (A + B) = repeat_mset n A + repeat_mset n B"
   4.557 +  by (auto simp: multiset_eq_iff add_mult_distrib2)
   4.558 +
   4.559 +lemma repeat_mset_distrib_add_mset [simp]:
   4.560 +  "repeat_mset n (add_mset a A) = repeat_mset n {#a#} + repeat_mset n A"
   4.561 +  by (auto simp: multiset_eq_iff)
   4.562 +
   4.563 +ML_file "multiset_simprocs_util.ML"
   4.564 +ML_file "multiset_simprocs.ML"
   4.565 +
   4.566 +simproc_setup mseteq_cancel_numerals
   4.567 +  ("(l::'a multiset) + m = n" | "(l::'a multiset) = m + n" |
   4.568 +   "add_mset a m = n" | "m = add_mset a n") =
   4.569 +  \<open>fn phi => Multiset_Simprocs.eq_cancel_msets\<close>
   4.570 +
   4.571 +simproc_setup msetless_cancel_numerals
   4.572 +  ("(l::'a multiset) + m \<subset># n" | "(l::'a multiset) \<subset># m + n" |
   4.573 +   "add_mset a m \<subset># n" | "m \<subset># add_mset a n") =
   4.574 +  \<open>fn phi => Multiset_Simprocs.subset_cancel_msets\<close>
   4.575 +
   4.576 +simproc_setup msetle_cancel_numerals
   4.577 +  ("(l::'a multiset) + m \<subseteq># n" | "(l::'a multiset) \<subseteq># m + n" |
   4.578 +   "add_mset a m \<subseteq># n" | "m \<subseteq># add_mset a n") =
   4.579 +  \<open>fn phi => Multiset_Simprocs.subseteq_cancel_msets\<close>
   4.580 +
   4.581 +simproc_setup msetdiff_cancel_numerals
   4.582 +  ("((l::'a multiset) + m) - n" | "(l::'a multiset) - (m + n)" |
   4.583 +   "add_mset a m - n" | "m - add_mset a n") =
   4.584 +  \<open>fn phi => Multiset_Simprocs.diff_cancel_msets\<close>
   4.585 +
   4.586 +
   4.587  subsubsection \<open>Conditionally complete lattice\<close>
   4.588  
   4.589  instantiation multiset :: (type) Inf
   4.590 @@ -1001,7 +1176,7 @@
   4.591    finally show ?thesis .
   4.592  qed
   4.593  
   4.594 -lemma in_Sup_multisetD: 
   4.595 +lemma in_Sup_multisetD:
   4.596    assumes "x \<in># Sup A"
   4.597    shows   "\<exists>X\<in>A. x \<in># X"
   4.598  proof -
   4.599 @@ -1044,7 +1219,7 @@
   4.600  lemma filter_empty_mset [simp]: "filter_mset P {#} = {#}"
   4.601    by (rule multiset_eqI) simp
   4.602  
   4.603 -lemma filter_single_mset [simp]: "filter_mset P {#x#} = (if P x then {#x#} else {#})"
   4.604 +lemma filter_single_mset: "filter_mset P {#x#} = (if P x then {#x#} else {#})"
   4.605    by (rule multiset_eqI) simp
   4.606  
   4.607  lemma filter_union_mset [simp]: "filter_mset P (M + N) = filter_mset P M + filter_mset P N"
   4.608 @@ -1056,6 +1231,11 @@
   4.609  lemma filter_inter_mset [simp]: "filter_mset P (M #\<inter> N) = filter_mset P M #\<inter> filter_mset P N"
   4.610    by (rule multiset_eqI) simp
   4.611  
   4.612 +lemma filter_mset_add_mset [simp]:
   4.613 +   "filter_mset P (add_mset x A) =
   4.614 +     (if P x then add_mset x (filter_mset P A) else (filter_mset P A))"
   4.615 +   by (auto simp: multiset_eq_iff)
   4.616 +
   4.617  lemma multiset_filter_subset[simp]: "filter_mset f M \<subseteq># M"
   4.618    by (simp add: mset_subset_eqI)
   4.619  
   4.620 @@ -1091,7 +1271,7 @@
   4.621        case False then have "count M a = 0"
   4.622          by (simp add: not_in_iff)
   4.623        with M show ?thesis by simp
   4.624 -    qed 
   4.625 +    qed
   4.626    qed
   4.627  qed
   4.628  
   4.629 @@ -1103,6 +1283,10 @@
   4.630  lemma wcount_union: "wcount f (M + N) a = wcount f M a + wcount f N a"
   4.631    by (auto simp: wcount_def add_mult_distrib)
   4.632  
   4.633 +lemma wcount_add_mset:
   4.634 +  "wcount f (add_mset x M) a = (if x = a then Suc (f a) else 0) + wcount f M a"
   4.635 +  unfolding add_mset_add_single[of _ M] wcount_union by (auto simp: wcount_def)
   4.636 +
   4.637  definition size_multiset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a multiset \<Rightarrow> nat" where
   4.638    "size_multiset f M = setsum (wcount f M) (set_mset M)"
   4.639  
   4.640 @@ -1126,11 +1310,11 @@
   4.641  lemma size_empty [simp]: "size {#} = 0"
   4.642  by (simp add: size_multiset_overloaded_def)
   4.643  
   4.644 -lemma size_multiset_single [simp]: "size_multiset f {#b#} = Suc (f b)"
   4.645 +lemma size_multiset_single : "size_multiset f {#b#} = Suc (f b)"
   4.646  by (simp add: size_multiset_eq)
   4.647  
   4.648 -lemma size_single [simp]: "size {#b#} = 1"
   4.649 -by (simp add: size_multiset_overloaded_def)
   4.650 +lemma size_single: "size {#b#} = 1"
   4.651 +by (simp add: size_multiset_overloaded_def size_multiset_single)
   4.652  
   4.653  lemma setsum_wcount_Int:
   4.654    "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_mset N) = setsum (wcount f N) A"
   4.655 @@ -1144,6 +1328,13 @@
   4.656  apply (simp add: setsum_wcount_Int)
   4.657  done
   4.658  
   4.659 +lemma size_multiset_add_mset [simp]:
   4.660 +  "size_multiset f (add_mset a M) = Suc (f a) + size_multiset f M"
   4.661 +  unfolding add_mset_add_single[of _ M] size_multiset_union by (auto simp: size_multiset_single)
   4.662 +
   4.663 +lemma size_add_mset [simp]: "size (add_mset a A) = Suc (size A)"
   4.664 +by (simp add: size_multiset_overloaded_def wcount_add_mset)
   4.665 +
   4.666  lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
   4.667  by (auto simp add: size_multiset_overloaded_def)
   4.668  
   4.669 @@ -1165,11 +1356,11 @@
   4.670  
   4.671  lemma size_eq_Suc_imp_eq_union:
   4.672    assumes "size M = Suc n"
   4.673 -  shows "\<exists>a N. M = N + {#a#}"
   4.674 +  shows "\<exists>a N. M = add_mset a N"
   4.675  proof -
   4.676    from assms obtain a where "a \<in># M"
   4.677      by (erule size_eq_Suc_imp_elem [THEN exE])
   4.678 -  then have "M = M - {#a#} + {#a#}" by simp
   4.679 +  then have "M = add_mset a (M - {#a#})" by simp
   4.680    then show ?thesis by blast
   4.681  qed
   4.682  
   4.683 @@ -1195,24 +1386,24 @@
   4.684  
   4.685  theorem multiset_induct [case_names empty add, induct type: multiset]:
   4.686    assumes empty: "P {#}"
   4.687 -  assumes add: "\<And>M x. P M \<Longrightarrow> P (M + {#x#})"
   4.688 +  assumes add: "\<And>x M. P M \<Longrightarrow> P (add_mset x M)"
   4.689    shows "P M"
   4.690  proof (induct n \<equiv> "size M" arbitrary: M)
   4.691    case 0 thus "P M" by (simp add: empty)
   4.692  next
   4.693    case (Suc k)
   4.694 -  obtain N x where "M = N + {#x#}"
   4.695 +  obtain N x where "M = add_mset x N"
   4.696      using \<open>Suc k = size M\<close> [symmetric]
   4.697      using size_eq_Suc_imp_eq_union by fast
   4.698    with Suc add show "P M" by simp
   4.699  qed
   4.700  
   4.701 -lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}"
   4.702 +lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = add_mset a A"
   4.703  by (induct M) auto
   4.704  
   4.705  lemma multiset_cases [cases type]:
   4.706    obtains (empty) "M = {#}"
   4.707 -    | (add) N x where "M = N + {#x#}"
   4.708 +    | (add) x N where "M = add_mset x N"
   4.709    by (induct M) simp_all
   4.710  
   4.711  lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
   4.712 @@ -1227,19 +1418,19 @@
   4.713  proof (induct A arbitrary: B)
   4.714    case (empty M)
   4.715    then have "M \<noteq> {#}" by (simp add: mset_subset_empty_nonempty)
   4.716 -  then obtain M' x where "M = M' + {#x#}"
   4.717 +  then obtain M' x where "M = add_mset x M'"
   4.718      by (blast dest: multi_nonempty_split)
   4.719    then show ?case by simp
   4.720  next
   4.721 -  case (add S x T)
   4.722 +  case (add x S T)
   4.723    have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact
   4.724 -  have SxsubT: "S + {#x#} \<subset># T" by fact
   4.725 +  have SxsubT: "add_mset x S \<subset># T" by fact
   4.726    then have "x \<in># T" and "S \<subset># T"
   4.727      by (auto dest: mset_subset_insertD)
   4.728 -  then obtain T' where T: "T = T' + {#x#}"
   4.729 +  then obtain T' where T: "T = add_mset x T'"
   4.730      by (blast dest: multi_member_split)
   4.731    then have "S \<subset># T'" using SxsubT
   4.732 -    by (blast intro: mset_subset_add_bothsides)
   4.733 +    by simp
   4.734    then have "size S < size T'" using IH by simp
   4.735    then show ?case using T by simp
   4.736  qed
   4.737 @@ -1267,7 +1458,7 @@
   4.738  lemma multi_subset_induct [consumes 2, case_names empty add]:
   4.739    assumes "F \<subseteq># A"
   4.740      and empty: "P {#}"
   4.741 -    and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
   4.742 +    and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (add_mset a F)"
   4.743    shows "P F"
   4.744  proof -
   4.745    from \<open>F \<subseteq># A\<close>
   4.746 @@ -1276,8 +1467,8 @@
   4.747      show "P {#}" by fact
   4.748    next
   4.749      fix x F
   4.750 -    assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "F + {#x#} \<subseteq># A"
   4.751 -    show "P (F + {#x#})"
   4.752 +    assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "add_mset x F \<subseteq># A"
   4.753 +    show "P (add_mset x F)"
   4.754      proof (rule insert)
   4.755        from i show "x \<in># A" by (auto dest: mset_subset_eq_insertD)
   4.756        from i have "F \<subseteq># A" by (auto dest: mset_subset_eq_insertD)
   4.757 @@ -1299,51 +1490,41 @@
   4.758  context comp_fun_commute
   4.759  begin
   4.760  
   4.761 -lemma fold_mset_insert: "fold_mset f s (M + {#x#}) = f x (fold_mset f s M)"
   4.762 +lemma fold_mset_add_mset [simp]: "fold_mset f s (add_mset x M) = f x (fold_mset f s M)"
   4.763  proof -
   4.764    interpret mset: comp_fun_commute "\<lambda>y. f y ^^ count M y"
   4.765      by (fact comp_fun_commute_funpow)
   4.766 -  interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (M + {#x#}) y"
   4.767 +  interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (add_mset x M) y"
   4.768      by (fact comp_fun_commute_funpow)
   4.769    show ?thesis
   4.770    proof (cases "x \<in> set_mset M")
   4.771      case False
   4.772 -    then have *: "count (M + {#x#}) x = 1"
   4.773 +    then have *: "count (add_mset x M) x = 1"
   4.774        by (simp add: not_in_iff)
   4.775 -    from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_mset M) =
   4.776 +    from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (add_mset x M) y) s (set_mset M) =
   4.777        Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_mset M)"
   4.778        by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
   4.779      with False * show ?thesis
   4.780 -      by (simp add: fold_mset_def del: count_union)
   4.781 +      by (simp add: fold_mset_def del: count_add_mset)
   4.782    next
   4.783      case True
   4.784      define N where "N = set_mset M - {x}"
   4.785      from N_def True have *: "set_mset M = insert x N" "x \<notin> N" "finite N" by auto
   4.786 -    then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N =
   4.787 +    then have "Finite_Set.fold (\<lambda>y. f y ^^ count (add_mset x M) y) s N =
   4.788        Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
   4.789        by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
   4.790 -    with * show ?thesis by (simp add: fold_mset_def del: count_union) simp
   4.791 +    with * show ?thesis by (simp add: fold_mset_def del: count_add_mset) simp
   4.792    qed
   4.793  qed
   4.794  
   4.795 -corollary fold_mset_single [simp]: "fold_mset f s {#x#} = f x s"
   4.796 -proof -
   4.797 -  have "fold_mset f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp
   4.798 -  then show ?thesis by simp
   4.799 -qed
   4.800 +corollary fold_mset_single: "fold_mset f s {#x#} = f x s"
   4.801 +  by simp
   4.802  
   4.803  lemma fold_mset_fun_left_comm: "f x (fold_mset f s M) = fold_mset f (f x s) M"
   4.804 -  by (induct M) (simp_all add: fold_mset_insert fun_left_comm)
   4.805 +  by (induct M) (simp_all add: fun_left_comm)
   4.806  
   4.807  lemma fold_mset_union [simp]: "fold_mset f s (M + N) = fold_mset f (fold_mset f s M) N"
   4.808 -proof (induct M)
   4.809 -  case empty then show ?case by simp
   4.810 -next
   4.811 -  case (add M x)
   4.812 -  have "M + {#x#} + N = (M + N) + {#x#}"
   4.813 -    by (simp add: ac_simps)
   4.814 -  with add show ?case by (simp add: fold_mset_insert fold_mset_fun_left_comm)
   4.815 -qed
   4.816 +  by (induct M) (simp_all add: fold_mset_fun_left_comm)
   4.817  
   4.818  lemma fold_mset_fusion:
   4.819    assumes "comp_fun_commute g"
   4.820 @@ -1356,6 +1537,14 @@
   4.821  
   4.822  end
   4.823  
   4.824 +lemma union_fold_mset_add_mset: "A + B = fold_mset add_mset A B"
   4.825 +proof -
   4.826 +  interpret comp_fun_commute add_mset
   4.827 +    by standard auto
   4.828 +  show ?thesis
   4.829 +    by (induction B) auto
   4.830 +qed
   4.831 +
   4.832  text \<open>
   4.833    A note on code generation: When defining some function containing a
   4.834    subterm @{term "fold_mset F"}, code generation is not automatic. When
   4.835 @@ -1370,31 +1559,32 @@
   4.836  subsection \<open>Image\<close>
   4.837  
   4.838  definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
   4.839 -  "image_mset f = fold_mset (plus \<circ> single \<circ> f) {#}"
   4.840 -
   4.841 -lemma comp_fun_commute_mset_image: "comp_fun_commute (plus \<circ> single \<circ> f)"
   4.842 +  "image_mset f = fold_mset (add_mset \<circ> f) {#}"
   4.843 +
   4.844 +lemma comp_fun_commute_mset_image: "comp_fun_commute (add_mset \<circ> f)"
   4.845  proof
   4.846  qed (simp add: ac_simps fun_eq_iff)
   4.847  
   4.848  lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
   4.849    by (simp add: image_mset_def)
   4.850  
   4.851 -lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
   4.852 +lemma image_mset_single: "image_mset f {#x#} = {#f x#}"
   4.853  proof -
   4.854 -  interpret comp_fun_commute "plus \<circ> single \<circ> f"
   4.855 +  interpret comp_fun_commute "add_mset \<circ> f"
   4.856      by (fact comp_fun_commute_mset_image)
   4.857    show ?thesis by (simp add: image_mset_def)
   4.858  qed
   4.859  
   4.860  lemma image_mset_union [simp]: "image_mset f (M + N) = image_mset f M + image_mset f N"
   4.861  proof -
   4.862 -  interpret comp_fun_commute "plus \<circ> single \<circ> f"
   4.863 +  interpret comp_fun_commute "add_mset \<circ> f"
   4.864      by (fact comp_fun_commute_mset_image)
   4.865    show ?thesis by (induct N) (simp_all add: image_mset_def ac_simps)
   4.866  qed
   4.867  
   4.868 -corollary image_mset_insert: "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
   4.869 -  by simp
   4.870 +corollary image_mset_add_mset [simp]:
   4.871 +  "image_mset f (add_mset a M) = add_mset (f a) (image_mset f M)"
   4.872 +  unfolding image_mset_union add_mset_add_single[of a M] by (simp add: image_mset_single)
   4.873  
   4.874  lemma set_image_mset [simp]: "set_mset (image_mset f M) = image f (set_mset M)"
   4.875    by (induct M) simp_all
   4.876 @@ -1406,26 +1596,33 @@
   4.877    by (cases M) auto
   4.878  
   4.879  lemma image_mset_If:
   4.880 -  "image_mset (\<lambda>x. if P x then f x else g x) A = 
   4.881 +  "image_mset (\<lambda>x. if P x then f x else g x) A =
   4.882       image_mset f (filter_mset P A) + image_mset g (filter_mset (\<lambda>x. \<not>P x) A)"
   4.883    by (induction A) (auto simp: add_ac)
   4.884  
   4.885 -lemma image_mset_Diff: 
   4.886 +lemma image_mset_Diff:
   4.887    assumes "B \<subseteq># A"
   4.888    shows   "image_mset f (A - B) = image_mset f A - image_mset f B"
   4.889  proof -
   4.890    have "image_mset f (A - B + B) = image_mset f (A - B) + image_mset f B"
   4.891      by simp
   4.892    also from assms have "A - B + B = A"
   4.893 -    by (simp add: subset_mset.diff_add) 
   4.894 +    by (simp add: subset_mset.diff_add)
   4.895    finally show ?thesis by simp
   4.896  qed
   4.897  
   4.898 -lemma count_image_mset: 
   4.899 +lemma count_image_mset:
   4.900    "count (image_mset f A) x = (\<Sum>y\<in>f -` {x} \<inter> set_mset A. count A y)"
   4.901 -  by (induction A)
   4.902 -     (auto simp: setsum.distrib setsum.delta' intro!: setsum.mono_neutral_left)
   4.903 -
   4.904 +proof (induction A)
   4.905 +  case empty
   4.906 +  then show ?case by simp
   4.907 +next
   4.908 +  case (add x A)
   4.909 +  moreover have *: "(if x = y then Suc n else n) = n + (if x = y then 1 else 0)" for n y
   4.910 +    by simp
   4.911 +  ultimately show ?case
   4.912 +    by (auto simp: setsum.distrib setsum.delta' intro!: setsum.mono_neutral_left)
   4.913 +qed
   4.914  
   4.915  syntax (ASCII)
   4.916    "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ :# _#})")
   4.917 @@ -1486,7 +1683,7 @@
   4.918  
   4.919  primrec mset :: "'a list \<Rightarrow> 'a multiset" where
   4.920    "mset [] = {#}" |
   4.921 -  "mset (a # x) = mset x + {# a #}"
   4.922 +  "mset (a # x) = add_mset a (mset x)"
   4.923  
   4.924  lemma in_multiset_in_set:
   4.925    "x \<in># mset xs \<longleftrightarrow> x \<in> set xs"
   4.926 @@ -1619,14 +1816,14 @@
   4.927    ultimately show ?case by simp
   4.928  qed
   4.929  
   4.930 -lemma mset_insort [simp]: "mset (insort x xs) = mset xs + {#x#}"
   4.931 -  by (induct xs) (simp_all add: ac_simps)
   4.932 +lemma mset_insort [simp]: "mset (insort x xs) = add_mset x (mset xs)"
   4.933 +  by (induct xs) simp_all
   4.934  
   4.935  lemma mset_map[simp]: "mset (map f xs) = image_mset f (mset xs)"
   4.936    by (induct xs) simp_all
   4.937  
   4.938 -global_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"
   4.939 -  defines mset_set = "folding.F (\<lambda>x M. {#x#} + M) {#}"
   4.940 +global_interpretation mset_set: folding add_mset "{#}"
   4.941 +  defines mset_set = "folding.F add_mset {#}"
   4.942    by standard (simp add: fun_eq_iff ac_simps)
   4.943  
   4.944  lemma count_mset_set [simp]:
   4.945 @@ -1647,7 +1844,7 @@
   4.946  lemma elem_mset_set[simp, intro]: "finite A \<Longrightarrow> x \<in># mset_set A \<longleftrightarrow> x \<in> A"
   4.947    by (induct A rule: finite_induct) simp_all
   4.948  
   4.949 -lemma mset_set_Union: 
   4.950 +lemma mset_set_Union:
   4.951    "finite A \<Longrightarrow> finite B \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> mset_set (A \<union> B) = mset_set A + mset_set B"
   4.952    by (induction A rule: finite_induct) (auto simp: add_ac)
   4.953  
   4.954 @@ -1655,12 +1852,12 @@
   4.955    "finite A \<Longrightarrow> filter_mset P (mset_set A) = mset_set {x\<in>A. P x}"
   4.956  proof (induction A rule: finite_induct)
   4.957    case (insert x A)
   4.958 -  from insert.hyps have "filter_mset P (mset_set (insert x A)) = 
   4.959 +  from insert.hyps have "filter_mset P (mset_set (insert x A)) =
   4.960        filter_mset P (mset_set A) + mset_set (if P x then {x} else {})"
   4.961      by (simp add: add_ac)
   4.962    also have "filter_mset P (mset_set A) = mset_set {x\<in>A. P x}"
   4.963      by (rule insert.IH)
   4.964 -  also from insert.hyps 
   4.965 +  also from insert.hyps
   4.966      have "\<dots> + mset_set (if P x then {x} else {}) =
   4.967              mset_set ({x \<in> A. P x} \<union> (if P x then {x} else {}))" (is "_ = mset_set ?A")
   4.968       by (intro mset_set_Union [symmetric]) simp_all
   4.969 @@ -1700,7 +1897,7 @@
   4.970  qed
   4.971  
   4.972  lemma sorted_list_of_multiset_insert [simp]:
   4.973 -  "sorted_list_of_multiset (M + {#x#}) = List.insort x (sorted_list_of_multiset M)"
   4.974 +  "sorted_list_of_multiset (add_mset x M) = List.insort x (sorted_list_of_multiset M)"
   4.975  proof -
   4.976    interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
   4.977    show ?thesis by (simp add: sorted_list_of_multiset_def)
   4.978 @@ -1738,36 +1935,36 @@
   4.979  lemma mset_upt [simp]: "mset [m..<n] = mset_set {m..<n}"
   4.980    by (induction n) (simp_all add: atLeastLessThanSuc add_ac)
   4.981  
   4.982 -lemma image_mset_map_of: 
   4.983 +lemma image_mset_map_of:
   4.984    "distinct (map fst xs) \<Longrightarrow> {#the (map_of xs i). i \<in># mset (map fst xs)#} = mset (map snd xs)"
   4.985  proof (induction xs)
   4.986    case (Cons x xs)
   4.987 -  have "{#the (map_of (x # xs) i). i \<in># mset (map fst (x # xs))#} = 
   4.988 -          {#the (if i = fst x then Some (snd x) else map_of xs i). 
   4.989 -             i \<in># mset (map fst xs)#} + {#snd x#}" (is "_ = ?A + _") by simp
   4.990 +  have "{#the (map_of (x # xs) i). i \<in># mset (map fst (x # xs))#} =
   4.991 +          add_mset (snd x) {#the (if i = fst x then Some (snd x) else map_of xs i).
   4.992 +             i \<in># mset (map fst xs)#}" (is "_ = add_mset _ ?A") by simp
   4.993    also from Cons.prems have "?A = {#the (map_of xs i). i :# mset (map fst xs)#}"
   4.994      by (cases x, intro image_mset_cong) (auto simp: in_multiset_in_set)
   4.995    also from Cons.prems have "\<dots> = mset (map snd xs)" by (intro Cons.IH) simp_all
   4.996    finally show ?case by simp
   4.997 -qed simp_all  
   4.998 +qed simp_all
   4.999  
  4.1000  
  4.1001  subsection \<open>Replicate operation\<close>
  4.1002  
  4.1003  definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
  4.1004 -  "replicate_mset n x = ((op + {#x#}) ^^ n) {#}"
  4.1005 +  "replicate_mset n x = (add_mset x ^^ n) {#}"
  4.1006  
  4.1007  lemma replicate_mset_0[simp]: "replicate_mset 0 x = {#}"
  4.1008    unfolding replicate_mset_def by simp
  4.1009  
  4.1010 -lemma replicate_mset_Suc[simp]: "replicate_mset (Suc n) x = replicate_mset n x + {#x#}"
  4.1011 +lemma replicate_mset_Suc [simp]: "replicate_mset (Suc n) x = add_mset x (replicate_mset n x)"
  4.1012    unfolding replicate_mset_def by (induct n) (auto intro: add.commute)
  4.1013  
  4.1014  lemma in_replicate_mset[simp]: "x \<in># replicate_mset n y \<longleftrightarrow> n > 0 \<and> x = y"
  4.1015    unfolding replicate_mset_def by (induct n) auto
  4.1016  
  4.1017  lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
  4.1018 -  unfolding replicate_mset_def by (induct n) simp_all
  4.1019 +  unfolding replicate_mset_def by (induct n) auto
  4.1020  
  4.1021  lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})"
  4.1022    by (auto split: if_splits)
  4.1023 @@ -1821,12 +2018,15 @@
  4.1024      by (induct N) (simp_all add: left_commute eq_fold)
  4.1025  qed
  4.1026  
  4.1027 +lemma add_mset [simp]: "F (add_mset x N) = x \<^bold>* F N"
  4.1028 +  unfolding add_mset_add_single[of x N] union by (simp add: ac_simps)
  4.1029 +
  4.1030  end
  4.1031  
  4.1032  lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute (op + :: 'a multiset \<Rightarrow> _ \<Rightarrow> _)"
  4.1033    by standard (simp add: add_ac comp_def)
  4.1034  
  4.1035 -declare comp_fun_commute.fold_mset_insert[OF comp_fun_commute_plus_mset, simp]
  4.1036 +declare comp_fun_commute.fold_mset_add_mset[OF comp_fun_commute_plus_mset, simp]
  4.1037  
  4.1038  lemma in_mset_fold_plus_iff[iff]: "x \<in># fold_mset (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
  4.1039    by (induct NN) auto
  4.1040 @@ -1862,9 +2062,10 @@
  4.1041  proof (induct M)
  4.1042    case empty then show ?case by simp
  4.1043  next
  4.1044 -  case (add M x) then show ?case
  4.1045 +  case (add x M) then show ?case
  4.1046      by (cases "x \<in> set_mset M")
  4.1047 -      (simp_all add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb not_in_iff)
  4.1048 +      (simp_all add: size_multiset_overloaded_eq not_in_iff setsum.If_cases Diff_eq[symmetric]
  4.1049 +        setsum.remove)
  4.1050  qed
  4.1051  
  4.1052  lemma size_mset_set [simp]: "size (mset_set A) = card A"
  4.1053 @@ -1945,8 +2146,8 @@
  4.1054    assumes "x \<in># A"
  4.1055    shows "x dvd msetprod A"
  4.1056  proof -
  4.1057 -  from assms have "A = (A - {#x#}) + {#x#}" by simp
  4.1058 -  then obtain B where "A = B + {#x#}" ..
  4.1059 +  from assms have "A = add_mset x (A - {#x#})" by simp
  4.1060 +  then obtain B where "A = add_mset x B" ..
  4.1061    then show ?thesis by simp
  4.1062  qed
  4.1063  
  4.1064 @@ -1966,8 +2167,7 @@
  4.1065  lemma (in semidom_divide) msetprod_minus:
  4.1066    assumes "a \<in># A" and "a \<noteq> 0"
  4.1067    shows "msetprod (A - {#a#}) = msetprod A div a"
  4.1068 -  using assms msetprod_diff [of "{#a#}" A]
  4.1069 -    by (auto simp add: single_subset_iff)
  4.1070 +  using assms msetprod_diff [of "{#a#}" A] by auto
  4.1071  
  4.1072  lemma (in normalization_semidom) normalized_msetprodI:
  4.1073    assumes "\<And>a. a \<in># A \<Longrightarrow> normalize a = a"
  4.1074 @@ -1983,8 +2183,8 @@
  4.1075  begin
  4.1076  
  4.1077  lemma mset_insort [simp]:
  4.1078 -  "mset (insort_key k x xs) = {#x#} + mset xs"
  4.1079 -  by (induct xs) (simp_all add: ac_simps)
  4.1080 +  "mset (insort_key k x xs) = add_mset x (mset xs)"
  4.1081 +  by (induct xs) simp_all
  4.1082  
  4.1083  lemma mset_sort [simp]:
  4.1084    "mset (sort_key k xs) = mset xs"
  4.1085 @@ -2165,7 +2365,7 @@
  4.1086    by (induct xs) (auto intro: subset_mset.order_trans)
  4.1087  
  4.1088  lemma mset_update:
  4.1089 -  "i < length ls \<Longrightarrow> mset (ls[i := v]) = mset ls - {#ls ! i#} + {#v#}"
  4.1090 +  "i < length ls \<Longrightarrow> mset (ls[i := v]) = add_mset v (mset ls - {#ls ! i#})"
  4.1091  proof (induct ls arbitrary: i)
  4.1092    case Nil then show ?case by simp
  4.1093  next
  4.1094 @@ -2176,14 +2376,7 @@
  4.1095    next
  4.1096      case (Suc i')
  4.1097      with Cons show ?thesis
  4.1098 -      apply simp
  4.1099 -      apply (subst add.assoc)
  4.1100 -      apply (subst add.commute [of "{#v#}" "{#x#}"])
  4.1101 -      apply (subst add.assoc [symmetric])
  4.1102 -      apply simp
  4.1103 -      apply (rule mset_subset_eq_multiset_union_diff_commute)
  4.1104 -      apply (simp add: mset_subset_eq_single nth_mem_mset)
  4.1105 -      done
  4.1106 +      by (cases \<open>x = xs ! i'\<close>) auto
  4.1107    qed
  4.1108  qed
  4.1109  
  4.1110 @@ -2198,20 +2391,20 @@
  4.1111  subsubsection \<open>Well-foundedness\<close>
  4.1112  
  4.1113  definition mult1 :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
  4.1114 -  "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
  4.1115 +  "mult1 r = {(N, M). \<exists>a M0 K. M = add_mset a M0 \<and> N = M0 + K \<and>
  4.1116        (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r)}"
  4.1117  
  4.1118  definition mult :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
  4.1119    "mult r = (mult1 r)\<^sup>+"
  4.1120  
  4.1121  lemma mult1I:
  4.1122 -  assumes "M = M0 + {#a#}" and "N = M0 + K" and "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
  4.1123 +  assumes "M = add_mset a M0" and "N = M0 + K" and "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
  4.1124    shows "(N, M) \<in> mult1 r"
  4.1125    using assms unfolding mult1_def by blast
  4.1126  
  4.1127  lemma mult1E:
  4.1128    assumes "(N, M) \<in> mult1 r"
  4.1129 -  obtains a M0 K where "M = M0 + {#a#}" "N = M0 + K" "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
  4.1130 +  obtains a M0 K where "M = add_mset a M0" "N = M0 + K" "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
  4.1131    using assms unfolding mult1_def by blast
  4.1132  
  4.1133  lemma mono_mult1:
  4.1134 @@ -2226,21 +2419,21 @@
  4.1135  by (simp add: mult1_def)
  4.1136  
  4.1137  lemma less_add:
  4.1138 -  assumes mult1: "(N, M0 + {#a#}) \<in> mult1 r"
  4.1139 +  assumes mult1: "(N, add_mset a M0) \<in> mult1 r"
  4.1140    shows
  4.1141 -    "(\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or>
  4.1142 +    "(\<exists>M. (M, M0) \<in> mult1 r \<and> N = add_mset a M) \<or>
  4.1143       (\<exists>K. (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r) \<and> N = M0 + K)"
  4.1144  proof -
  4.1145    let ?r = "\<lambda>K a. \<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r"
  4.1146 -  let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a"
  4.1147 -  obtain a' M0' K where M0: "M0 + {#a#} = M0' + {#a'#}"
  4.1148 +  let ?R = "\<lambda>N M. \<exists>a M0 K. M = add_mset a M0 \<and> N = M0 + K \<and> ?r K a"
  4.1149 +  obtain a' M0' K where M0: "add_mset a M0 = add_mset a' M0'"
  4.1150      and N: "N = M0' + K"
  4.1151      and r: "?r K a'"
  4.1152      using mult1 unfolding mult1_def by auto
  4.1153    show ?thesis (is "?case1 \<or> ?case2")
  4.1154    proof -
  4.1155      from M0 consider "M0 = M0'" "a = a'"
  4.1156 -      | K' where "M0 = K' + {#a'#}" "M0' = K' + {#a#}"
  4.1157 +      | K' where "M0 = add_mset a' K'" "M0' = add_mset a K'"
  4.1158        by atomize_elim (simp only: add_eq_conv_ex)
  4.1159      then show ?thesis
  4.1160      proof cases
  4.1161 @@ -2250,7 +2443,7 @@
  4.1162        then show ?thesis ..
  4.1163      next
  4.1164        case 2
  4.1165 -      from N 2(2) have n: "N = K' + K + {#a#}" by (simp add: ac_simps)
  4.1166 +      from N 2(2) have n: "N = add_mset a (K' + K)" by (simp add: ac_simps)
  4.1167        with r 2(1) have "?R (K' + K) M0" by blast
  4.1168        with n have ?case1 by (simp add: mult1_def)
  4.1169        then show ?thesis ..
  4.1170 @@ -2267,21 +2460,21 @@
  4.1171    {
  4.1172      fix M M0 a
  4.1173      assume M0: "M0 \<in> ?W"
  4.1174 -      and wf_hyp: "\<And>b. (b, a) \<in> r \<Longrightarrow> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
  4.1175 -      and acc_hyp: "\<forall>M. (M, M0) \<in> ?R \<longrightarrow> M + {#a#} \<in> ?W"
  4.1176 -    have "M0 + {#a#} \<in> ?W"
  4.1177 -    proof (rule accI [of "M0 + {#a#}"])
  4.1178 +      and wf_hyp: "\<And>b. (b, a) \<in> r \<Longrightarrow> (\<forall>M \<in> ?W. add_mset b M \<in> ?W)"
  4.1179 +      and acc_hyp: "\<forall>M. (M, M0) \<in> ?R \<longrightarrow> add_mset a M \<in> ?W"
  4.1180 +    have "add_mset a M0 \<in> ?W"
  4.1181 +    proof (rule accI [of "add_mset a M0"])
  4.1182        fix N
  4.1183 -      assume "(N, M0 + {#a#}) \<in> ?R"
  4.1184 -      then consider M where "(M, M0) \<in> ?R" "N = M + {#a#}"
  4.1185 +      assume "(N, add_mset a M0) \<in> ?R"
  4.1186 +      then consider M where "(M, M0) \<in> ?R" "N = add_mset a M"
  4.1187          | K where "\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r" "N = M0 + K"
  4.1188          by atomize_elim (rule less_add)
  4.1189        then show "N \<in> ?W"
  4.1190        proof cases
  4.1191          case 1
  4.1192 -        from acc_hyp have "(M, M0) \<in> ?R \<longrightarrow> M + {#a#} \<in> ?W" ..
  4.1193 -        from this and \<open>(M, M0) \<in> ?R\<close> have "M + {#a#} \<in> ?W" ..
  4.1194 -        then show "N \<in> ?W" by (simp only: \<open>N = M + {#a#}\<close>)
  4.1195 +        from acc_hyp have "(M, M0) \<in> ?R \<longrightarrow> add_mset a M \<in> ?W" ..
  4.1196 +        from this and \<open>(M, M0) \<in> ?R\<close> have "add_mset a M \<in> ?W" ..
  4.1197 +        then show "N \<in> ?W" by (simp only: \<open>N = add_mset a M\<close>)
  4.1198        next
  4.1199          case 2
  4.1200          from this(1) have "M0 + K \<in> ?W"
  4.1201 @@ -2289,12 +2482,12 @@
  4.1202            case empty
  4.1203            from M0 show "M0 + {#} \<in> ?W" by simp
  4.1204          next
  4.1205 -          case (add K x)
  4.1206 +          case (add x K)
  4.1207            from add.prems have "(x, a) \<in> r" by simp
  4.1208 -          with wf_hyp have "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast
  4.1209 +          with wf_hyp have "\<forall>M \<in> ?W. add_mset x M \<in> ?W" by blast
  4.1210            moreover from add have "M0 + K \<in> ?W" by simp
  4.1211 -          ultimately have "(M0 + K) + {#x#} \<in> ?W" ..
  4.1212 -          then show "M0 + (K + {#x#}) \<in> ?W" by (simp only: add.assoc)
  4.1213 +          ultimately have "add_mset x (M0 + K) \<in> ?W" ..
  4.1214 +          then show "M0 + (add_mset x K) \<in> ?W" by simp
  4.1215          qed
  4.1216          then show "N \<in> ?W" by (simp only: 2(2))
  4.1217        qed
  4.1218 @@ -2310,18 +2503,18 @@
  4.1219      qed
  4.1220  
  4.1221      fix M a assume "M \<in> ?W"
  4.1222 -    from \<open>wf r\<close> have "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
  4.1223 +    from \<open>wf r\<close> have "\<forall>M \<in> ?W. add_mset a M \<in> ?W"
  4.1224      proof induct
  4.1225        fix a
  4.1226 -      assume r: "\<And>b. (b, a) \<in> r \<Longrightarrow> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
  4.1227 -      show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
  4.1228 +      assume r: "\<And>b. (b, a) \<in> r \<Longrightarrow> (\<forall>M \<in> ?W. add_mset b M \<in> ?W)"
  4.1229 +      show "\<forall>M \<in> ?W. add_mset a M \<in> ?W"
  4.1230        proof
  4.1231          fix M assume "M \<in> ?W"
  4.1232 -        then show "M + {#a#} \<in> ?W"
  4.1233 +        then show "add_mset a M \<in> ?W"
  4.1234            by (rule acc_induct) (rule tedious_reasoning [OF _ r])
  4.1235        qed
  4.1236      qed
  4.1237 -    from this and \<open>M \<in> ?W\<close> show "M + {#a#} \<in> ?W" ..
  4.1238 +    from this and \<open>M \<in> ?W\<close> show "add_mset a M \<in> ?W" ..
  4.1239    qed
  4.1240  qed
  4.1241  
  4.1242 @@ -2335,38 +2528,38 @@
  4.1243  subsubsection \<open>Closure-free presentation\<close>
  4.1244  
  4.1245  text \<open>One direction.\<close>
  4.1246 -
  4.1247  lemma mult_implies_one_step:
  4.1248    "trans r \<Longrightarrow> (M, N) \<in> mult r \<Longrightarrow>
  4.1249      \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
  4.1250      (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)"
  4.1251  apply (unfold mult_def mult1_def)
  4.1252  apply (erule converse_trancl_induct, clarify)
  4.1253 - apply (rule_tac x = M0 in exI, simp, clarify)
  4.1254 + apply (rule_tac x = M0 in exI, simp)
  4.1255 +apply clarify
  4.1256  apply (case_tac "a \<in># K")
  4.1257   apply (rule_tac x = I in exI)
  4.1258   apply (simp (no_asm))
  4.1259   apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
  4.1260   apply (simp (no_asm_simp) add: add.assoc [symmetric])
  4.1261 - apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong)
  4.1262 - apply (simp add: diff_union_single_conv)
  4.1263 - apply (simp (no_asm_use) add: trans_def)
  4.1264 - apply (metis (no_types, hide_lams) Multiset.diff_right_commute Un_iff diff_single_trivial multi_drop_mem_not_eq)
  4.1265 + apply (drule union_single_eq_diff)
  4.1266 + apply (auto simp: subset_mset.add_diff_assoc dest: in_diffD)[]
  4.1267 + apply (meson transD)
  4.1268  apply (subgoal_tac "a \<in># I")
  4.1269   apply (rule_tac x = "I - {#a#}" in exI)
  4.1270 - apply (rule_tac x = "J + {#a#}" in exI)
  4.1271 + apply (rule_tac x = "add_mset a J" in exI)
  4.1272   apply (rule_tac x = "K + Ka" in exI)
  4.1273   apply (rule conjI)
  4.1274 -  apply (simp add: multiset_eq_iff split: nat_diff_split)
  4.1275 +  apply (simp add: multiset_eq_iff union_single_eq_diff split: nat_diff_split)
  4.1276   apply (rule conjI)
  4.1277 -  apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong, simp)
  4.1278 + apply (drule union_single_eq_diff)
  4.1279 + apply (simp add: add.assoc subset_mset.add_diff_assoc2)
  4.1280 +  apply (simp)
  4.1281    apply (simp add: multiset_eq_iff split: nat_diff_split)
  4.1282   apply (simp (no_asm_use) add: trans_def)
  4.1283 -apply (subgoal_tac "a \<in># (M0 + {#a#})")
  4.1284 +apply (subgoal_tac "a \<in># add_mset a M0")
  4.1285   apply (simp_all add: not_in_iff)
  4.1286   apply blast
  4.1287 - apply (metis add.comm_neutral add_diff_cancel_right' count_eq_zero_iff diff_single_trivial multi_self_add_other_not_self plus_multiset.rep_eq)
  4.1288 -done
  4.1289 +by (metis (no_types, lifting) not_in_iff union_iff union_single_eq_member)
  4.1290  
  4.1291  lemma one_step_implies_mult_aux:
  4.1292    "\<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.1293 @@ -2375,7 +2568,6 @@
  4.1294   apply auto
  4.1295  apply (frule size_eq_Suc_imp_eq_union, clarify)
  4.1296  apply (rename_tac "J'", simp)
  4.1297 -apply (erule notE, auto)
  4.1298  apply (case_tac "J' = {#}")
  4.1299   apply (simp add: mult_def)
  4.1300   apply (rule r_into_trancl)
  4.1301 @@ -2383,14 +2575,18 @@
  4.1302  txt \<open>Now we know @{term "J' \<noteq> {#}"}.\<close>
  4.1303  apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
  4.1304  apply (erule_tac P = "\<forall>k \<in> set_mset K. P k" for P in rev_mp)
  4.1305 -apply (erule ssubst)
  4.1306  apply (simp add: Ball_def, auto)
  4.1307  apply (subgoal_tac
  4.1308    "((I + {# x \<in># K. (x, a) \<in> r #}) + {# x \<in># K. (x, a) \<notin> r #},
  4.1309      (I + {# x \<in># K. (x, a) \<in> r #}) + J') \<in> mult r")
  4.1310 - prefer 2
  4.1311 - apply force
  4.1312 +prefer 2
  4.1313 +  apply (drule_tac x = "I + {# x \<in># K. (x, a) \<in> r#}" in spec)
  4.1314 +  apply (drule_tac x = "J'" in spec)
  4.1315 +  apply (drule_tac x = "{# x \<in># K. (x, a) \<notin> r#}" in spec)
  4.1316 +  apply auto[]
  4.1317  apply (simp (no_asm_use) add: add.assoc [symmetric] mult_def)
  4.1318 +apply (subst (asm)(1) add.assoc)
  4.1319 +apply (subst (asm)(2) multiset_partition[symmetric])
  4.1320  apply (erule trancl_trans)
  4.1321  apply (rule r_into_trancl)
  4.1322  apply (simp add: mult1_def)
  4.1323 @@ -2413,12 +2609,12 @@
  4.1324  proof
  4.1325    assume ?L thus ?R
  4.1326    proof (induct Z)
  4.1327 -    case (add Z z)
  4.1328 -    obtain X' Y' Z' where *: "X + Z + {#z#} = Z' + X'" "Y + Z + {#z#} = Z' + Y'" "Y' \<noteq> {#}"
  4.1329 +    case (add z Z)
  4.1330 +    obtain X' Y' Z' where *: "add_mset z X + Z = Z' + X'" "add_mset z Y + Z = Z' + Y'" "Y' \<noteq> {#}"
  4.1331        "\<forall>x \<in> set_mset X'. \<exists>y \<in> set_mset Y'. (x, y) \<in> s"
  4.1332 -      using mult_implies_one_step[OF `trans s` add(2)] unfolding add.assoc by blast
  4.1333 -    consider Z2 where "Z' = Z2 + {#z#}" | X2 Y2 where "X' = X2 + {#z#}" "Y' = Y2 + {#z#}"
  4.1334 -      using *(1,2) by (metis mset_add union_iff union_single_eq_member)
  4.1335 +      using mult_implies_one_step[OF `trans s` add(2)] by auto
  4.1336 +    consider Z2 where "Z' = add_mset z Z2" | X2 Y2 where "X' = add_mset z X2" "Y' = add_mset z Y2"
  4.1337 +      using *(1,2) by (metis add_mset_remove_trivial_If insert_iff set_mset_add_mset_insert union_iff)
  4.1338      thus ?case
  4.1339      proof (cases)
  4.1340        case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2]
  4.1341 @@ -2508,10 +2704,10 @@
  4.1342  
  4.1343  lemma (in preorder) mult1_lessE:
  4.1344    assumes "(N, M) \<in> mult1 {(a, b). a < b}"
  4.1345 -  obtains a M0 K where "M = M0 + {#a#}" "N = M0 + K"
  4.1346 +  obtains a M0 K where "M = add_mset a M0" "N = M0 + K"
  4.1347      "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
  4.1348  proof -
  4.1349 -  from assms obtain a M0 K where "M = M0 + {#a#}" "N = M0 + K" and
  4.1350 +  from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
  4.1351      *: "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
  4.1352    moreover from * [of a] have "a \<notin># K" by auto
  4.1353    ultimately show thesis by (auto intro: that)
  4.1354 @@ -2706,10 +2902,12 @@
  4.1355      fun msetT T = Type (@{type_name multiset}, [T]);
  4.1356  
  4.1357      fun mk_mset T [] = Const (@{const_abbrev Mempty}, msetT T)
  4.1358 -      | mk_mset T [x] = Const (@{const_name single}, T --> msetT T) $ x
  4.1359 +      | mk_mset T [x] =
  4.1360 +        Const (@{const_name add_mset}, T --> msetT T --> msetT T) $ x $
  4.1361 +          Const (@{const_abbrev Mempty}, msetT T)
  4.1362        | mk_mset T (x :: xs) =
  4.1363 -            Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $
  4.1364 -                  mk_mset T [x] $ mk_mset T xs
  4.1365 +        Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $
  4.1366 +          mk_mset T [x] $ mk_mset T xs
  4.1367  
  4.1368      fun mset_member_tac ctxt m i =
  4.1369        if m <= 0 then
  4.1370 @@ -2759,7 +2957,7 @@
  4.1371  lemma union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))"
  4.1372    by (fact add.left_commute)
  4.1373  
  4.1374 -lemmas union_ac = union_assoc union_commute union_lcomm
  4.1375 +lemmas union_ac = union_assoc union_commute union_lcomm add_mset_commute
  4.1376  
  4.1377  lemma union_right_cancel: "M + K = N + K \<longleftrightarrow> M = (N::'a multiset)"
  4.1378    by (fact add_right_cancel)
  4.1379 @@ -2816,9 +3014,8 @@
  4.1380                   (if maybe_opt then [Const (Nitpick_Model.unrep_mixfix (), elem_T)] else []) of
  4.1381                [] => Const (@{const_name zero_class.zero}, T)
  4.1382              | ts =>
  4.1383 -                foldl1 (fn (t1, t2) =>
  4.1384 -                    Const (@{const_name plus_class.plus}, T --> T --> T) $ t1 $ t2)
  4.1385 -                  (map (curry (op $) (Const (@{const_name single}, elem_T --> T))) ts))
  4.1386 +                foldl1 (fn (s, t) => Const (@{const_name add_mset}, elem_T --> T --> T) $ s $ t)
  4.1387 +                  ts)
  4.1388            end
  4.1389        | multiset_postproc _ _ _ _ t = t
  4.1390    in Nitpick_Model.register_term_postprocessor @{typ "'a multiset"} multiset_postproc end
  4.1391 @@ -2832,23 +3029,23 @@
  4.1392  lemma [code]: "{#} = mset []"
  4.1393    by simp
  4.1394  
  4.1395 +lemma [code]: "add_mset x (mset xs) = mset (x # xs)"
  4.1396 +  by simp
  4.1397 +
  4.1398  lemma [code]: "Multiset.is_empty (mset xs) \<longleftrightarrow> List.null xs"
  4.1399    by (simp add: Multiset.is_empty_def List.null_def)
  4.1400  
  4.1401 -lemma [code]: "{#x#} = mset [x]"
  4.1402 -  by simp
  4.1403 -
  4.1404  lemma union_code [code]: "mset xs + mset ys = mset (xs @ ys)"
  4.1405    by simp
  4.1406  
  4.1407  lemma [code]: "image_mset f (mset xs) = mset (map f xs)"
  4.1408 -  by (simp add: mset_map)
  4.1409 +  by simp
  4.1410  
  4.1411  lemma [code]: "filter_mset f (mset xs) = mset (filter f xs)"
  4.1412    by (simp add: mset_filter)
  4.1413  
  4.1414  lemma [code]: "mset xs - mset ys = mset (fold remove1 ys xs)"
  4.1415 -  by (rule sym, induct ys arbitrary: xs) (simp_all add: diff_add diff_right_commute)
  4.1416 +  by (rule sym, induct ys arbitrary: xs) (simp_all add: diff_add diff_right_commute diff_diff_add)
  4.1417  
  4.1418  lemma [code]:
  4.1419    "mset xs #\<inter> mset ys =
  4.1420 @@ -2930,7 +3127,7 @@
  4.1421      obtain ys1 y ys2 where res: "res = (ys1,y,ys2)" by (cases res, auto)
  4.1422      note Some = Some[unfolded res]
  4.1423      from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp
  4.1424 -    hence id: "mset ys = mset (ys1 @ ys2) + {#x#}"
  4.1425 +    hence id: "mset ys = add_mset x (mset (ys1 @ ys2))"
  4.1426        by (auto simp: ac_simps)
  4.1427      show ?thesis unfolding subset_eq_mset_impl.simps
  4.1428        unfolding Some option.simps split
  4.1429 @@ -2966,7 +3163,7 @@
  4.1430  lemma [code]: "msetprod (mset xs) = fold times xs 1"
  4.1431  proof -
  4.1432    have "\<And>x. fold times xs x = msetprod (mset xs) * x"
  4.1433 -    by (induct xs) (simp_all add: mult.assoc)
  4.1434 +    by (induct xs) (simp_all add: ac_simps)
  4.1435    then show ?thesis by simp
  4.1436  qed
  4.1437  
  4.1438 @@ -3020,7 +3217,7 @@
  4.1439  lemma mset_zip_take_Cons_drop_twice:
  4.1440    assumes "length xs = length ys" "j \<le> length xs"
  4.1441    shows "mset (zip (take j xs @ x # drop j xs) (take j ys @ y # drop j ys)) =
  4.1442 -    mset (zip xs ys) + {#(x, y)#}"
  4.1443 +    add_mset (x,y) (mset (zip xs ys))"
  4.1444    using assms
  4.1445  proof (induct xs ys arbitrary: x y j rule: list_induct2)
  4.1446    case Nil
  4.1447 @@ -3040,7 +3237,7 @@
  4.1448      hence "k \<le> length xs"
  4.1449        using Cons.prems by auto
  4.1450      hence "mset (zip (take k xs @ x # drop k xs) (take k ys @ y # drop k ys)) =
  4.1451 -      mset (zip xs ys) + {#(x, y)#}"
  4.1452 +      add_mset (x,y) (mset (zip xs ys))"
  4.1453        by (rule Cons.hyps(2))
  4.1454      thus ?thesis
  4.1455        unfolding k by (auto simp: add.commute union_lcomm)
  4.1456 @@ -3063,10 +3260,10 @@
  4.1457    define xsa where "xsa = take j xs' @ drop (Suc j) xs'"
  4.1458    have "mset xs' = {#x#} + mset xsa"
  4.1459      unfolding xsa_def using j_len nth_j
  4.1460 -    by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id Cons_nth_drop_Suc
  4.1461 -      mset.simps(2) union_code add.commute)
  4.1462 +    by (metis Cons_nth_drop_Suc union_mset_add_mset_right add_mset_remove_trivial add_diff_cancel_left'
  4.1463 +        append_take_drop_id mset.simps(2) mset_append)
  4.1464    hence ms_x: "mset xsa = mset xs"
  4.1465 -    by (metis Cons.prems add.commute add_right_imp_eq mset.simps(2))
  4.1466 +    by (simp add: Cons.prems)
  4.1467    then obtain ysa where
  4.1468      len_a: "length ysa = length xsa" and ms_a: "mset (zip xsa ysa) = mset (zip xs ys)"
  4.1469      using Cons.hyps(2) by blast
  4.1470 @@ -3113,7 +3310,7 @@
  4.1471  inductive pred_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> bool"
  4.1472  where
  4.1473    "pred_mset P {#}"
  4.1474 -| "\<lbrakk>P a; pred_mset P M\<rbrakk> \<Longrightarrow> pred_mset P (M + {#a#})"
  4.1475 +| "\<lbrakk>P a; pred_mset P M\<rbrakk> \<Longrightarrow> pred_mset P (add_mset a M)"
  4.1476  
  4.1477  bnf "'a multiset"
  4.1478    map: image_mset
  4.1479 @@ -3180,7 +3377,7 @@
  4.1480  inductive rel_mset'
  4.1481  where
  4.1482    Zero[intro]: "rel_mset' R {#} {#}"
  4.1483 -| Plus[intro]: "\<lbrakk>R a b; rel_mset' R M N\<rbrakk> \<Longrightarrow> rel_mset' R (M + {#a#}) (N + {#b#})"
  4.1484 +| Plus[intro]: "\<lbrakk>R a b; rel_mset' R M N\<rbrakk> \<Longrightarrow> rel_mset' R (add_mset a M) (add_mset b N)"
  4.1485  
  4.1486  lemma rel_mset_Zero: "rel_mset R {#} {#}"
  4.1487  unfolding rel_mset_def Grp_def by auto
  4.1488 @@ -3193,13 +3390,13 @@
  4.1489  lemma rel_mset_Plus:
  4.1490    assumes ab: "R a b"
  4.1491      and MN: "rel_mset R M N"
  4.1492 -  shows "rel_mset R (M + {#a#}) (N + {#b#})"
  4.1493 +  shows "rel_mset R (add_mset a M) (add_mset b N)"
  4.1494  proof -
  4.1495 -  have "\<exists>ya. image_mset fst y + {#a#} = image_mset fst ya \<and>
  4.1496 -    image_mset snd y + {#b#} = image_mset snd ya \<and>
  4.1497 +  have "\<exists>ya. add_mset a (image_mset fst y) = image_mset fst ya \<and>
  4.1498 +    add_mset b (image_mset snd y) = image_mset snd ya \<and>
  4.1499      set_mset ya \<subseteq> {(x, y). R x y}"
  4.1500      if "R a b" and "set_mset y \<subseteq> {(x, y). R x y}" for y
  4.1501 -    using that by (intro exI[of _ "y + {#(a,b)#}"]) auto
  4.1502 +    using that by (intro exI[of _ "add_mset (a,b) y"]) auto
  4.1503    thus ?thesis
  4.1504    using assms
  4.1505    unfolding multiset.rel_compp_Grp Grp_def by blast
  4.1506 @@ -3213,8 +3410,8 @@
  4.1507  
  4.1508  lemma multiset_induct2[case_names empty addL addR]:
  4.1509    assumes empty: "P {#} {#}"
  4.1510 -    and addL: "\<And>M N a. P M N \<Longrightarrow> P (M + {#a#}) N"
  4.1511 -    and addR: "\<And>M N a. P M N \<Longrightarrow> P M (N + {#a#})"
  4.1512 +    and addL: "\<And>a M N. P M N \<Longrightarrow> P (add_mset a M) N"
  4.1513 +    and addR: "\<And>a M N. P M N \<Longrightarrow> P M (add_mset a N)"
  4.1514    shows "P M N"
  4.1515  apply(induct N rule: multiset_induct)
  4.1516    apply(induct M rule: multiset_induct, rule empty, erule addL)
  4.1517 @@ -3224,7 +3421,7 @@
  4.1518  lemma multiset_induct2_size[consumes 1, case_names empty add]:
  4.1519    assumes c: "size M = size N"
  4.1520      and empty: "P {#} {#}"
  4.1521 -    and add: "\<And>M N a b. P M N \<Longrightarrow> P (M + {#a#}) (N + {#b#})"
  4.1522 +    and add: "\<And>a b M N a b. P M N \<Longrightarrow> P (add_mset a M) (add_mset b N)"
  4.1523    shows "P M N"
  4.1524    using c
  4.1525  proof (induct M arbitrary: N rule: measure_induct_rule[of size])
  4.1526 @@ -3234,48 +3431,48 @@
  4.1527      case True hence "N = {#}" using less.prems by auto
  4.1528      thus ?thesis using True empty by auto
  4.1529    next
  4.1530 -    case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
  4.1531 +    case False then obtain M1 a where M: "M = add_mset a M1" by (metis multi_nonempty_split)
  4.1532      have "N \<noteq> {#}" using False less.prems by auto
  4.1533 -    then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split)
  4.1534 +    then obtain N1 b where N: "N = add_mset b N1" by (metis multi_nonempty_split)
  4.1535      have "size M1 = size N1" using less.prems unfolding M N by auto
  4.1536      thus ?thesis using M N less.hyps add by auto
  4.1537    qed
  4.1538  qed
  4.1539  
  4.1540  lemma msed_map_invL:
  4.1541 -  assumes "image_mset f (M + {#a#}) = N"
  4.1542 -  shows "\<exists>N1. N = N1 + {#f a#} \<and> image_mset f M = N1"
  4.1543 +  assumes "image_mset f (add_mset a M) = N"
  4.1544 +  shows "\<exists>N1. N = add_mset (f a) N1 \<and> image_mset f M = N1"
  4.1545  proof -
  4.1546    have "f a \<in># N"
  4.1547 -    using assms multiset.set_map[of f "M + {#a#}"] by auto
  4.1548 -  then obtain N1 where N: "N = N1 + {#f a#}" using multi_member_split by metis
  4.1549 +    using assms multiset.set_map[of f "add_mset a M"] by auto
  4.1550 +  then obtain N1 where N: "N = add_mset (f a) N1" using multi_member_split by metis
  4.1551    have "image_mset f M = N1" using assms unfolding N by simp
  4.1552    thus ?thesis using N by blast
  4.1553  qed
  4.1554  
  4.1555  lemma msed_map_invR:
  4.1556 -  assumes "image_mset f M = N + {#b#}"
  4.1557 -  shows "\<exists>M1 a. M = M1 + {#a#} \<and> f a = b \<and> image_mset f M1 = N"
  4.1558 +  assumes "image_mset f M = add_mset b N"
  4.1559 +  shows "\<exists>M1 a. M = add_mset a M1 \<and> f a = b \<and> image_mset f M1 = N"
  4.1560  proof -
  4.1561    obtain a where a: "a \<in># M" and fa: "f a = b"
  4.1562      using multiset.set_map[of f M] unfolding assms
  4.1563      by (metis image_iff union_single_eq_member)
  4.1564 -  then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
  4.1565 +  then obtain M1 where M: "M = add_mset a M1" using multi_member_split by metis
  4.1566    have "image_mset f M1 = N" using assms unfolding M fa[symmetric] by simp
  4.1567    thus ?thesis using M fa by blast
  4.1568  qed
  4.1569  
  4.1570  lemma msed_rel_invL:
  4.1571 -  assumes "rel_mset R (M + {#a#}) N"
  4.1572 -  shows "\<exists>N1 b. N = N1 + {#b#} \<and> R a b \<and> rel_mset R M N1"
  4.1573 +  assumes "rel_mset R (add_mset a M) N"
  4.1574 +  shows "\<exists>N1 b. N = add_mset b N1 \<and> R a b \<and> rel_mset R M N1"
  4.1575  proof -
  4.1576 -  obtain K where KM: "image_mset fst K = M + {#a#}"
  4.1577 +  obtain K where KM: "image_mset fst K = add_mset a M"
  4.1578      and KN: "image_mset snd K = N" and sK: "set_mset K \<subseteq> {(a, b). R a b}"
  4.1579      using assms
  4.1580      unfolding multiset.rel_compp_Grp Grp_def by auto
  4.1581 -  obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
  4.1582 +  obtain K1 ab where K: "K = add_mset ab K1" and a: "fst ab = a"
  4.1583      and K1M: "image_mset fst K1 = M" using msed_map_invR[OF KM] by auto
  4.1584 -  obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "image_mset snd K1 = N1"
  4.1585 +  obtain N1 where N: "N = add_mset (snd ab) N1" and K1N1: "image_mset snd K1 = N1"
  4.1586      using msed_map_invL[OF KN[unfolded K]] by auto
  4.1587    have Rab: "R a (snd ab)" using sK a unfolding K by auto
  4.1588    have "rel_mset R M N1" using sK K1M K1N1
  4.1589 @@ -3284,16 +3481,16 @@
  4.1590  qed
  4.1591  
  4.1592  lemma msed_rel_invR:
  4.1593 -  assumes "rel_mset R M (N + {#b#})"
  4.1594 -  shows "\<exists>M1 a. M = M1 + {#a#} \<and> R a b \<and> rel_mset R M1 N"
  4.1595 +  assumes "rel_mset R M (add_mset b N)"
  4.1596 +  shows "\<exists>M1 a. M = add_mset a M1 \<and> R a b \<and> rel_mset R M1 N"
  4.1597  proof -
  4.1598 -  obtain K where KN: "image_mset snd K = N + {#b#}"
  4.1599 +  obtain K where KN: "image_mset snd K = add_mset b N"
  4.1600      and KM: "image_mset fst K = M" and sK: "set_mset K \<subseteq> {(a, b). R a b}"
  4.1601      using assms
  4.1602      unfolding multiset.rel_compp_Grp Grp_def by auto
  4.1603 -  obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
  4.1604 +  obtain K1 ab where K: "K = add_mset ab K1" and b: "snd ab = b"
  4.1605      and K1N: "image_mset snd K1 = N" using msed_map_invR[OF KN] by auto
  4.1606 -  obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "image_mset fst K1 = M1"
  4.1607 +  obtain M1 where M: "M = add_mset (fst ab) M1" and K1M1: "image_mset fst K1 = M1"
  4.1608      using msed_map_invL[OF KM[unfolded K]] by auto
  4.1609    have Rab: "R (fst ab) b" using sK b unfolding K by auto
  4.1610    have "rel_mset R M1 N" using sK K1N K1M1
  4.1611 @@ -3312,8 +3509,8 @@
  4.1612      case True hence "N = {#}" using c by simp
  4.1613      thus ?thesis using True rel_mset'.Zero by auto
  4.1614    next
  4.1615 -    case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
  4.1616 -    obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "rel_mset R M1 N1"
  4.1617 +    case False then obtain M1 a where M: "M = add_mset a M1" by (metis multi_nonempty_split)
  4.1618 +    obtain N1 b where N: "N = add_mset b N1" and R: "R a b" and ms: "rel_mset R M1 N1"
  4.1619        using msed_rel_invL[OF less.prems[unfolded M]] by auto
  4.1620      have "rel_mset' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp
  4.1621      thus ?thesis using rel_mset'.Plus[of R a b, OF R] unfolding M N by simp
     5.1 --- a/src/HOL/Library/Multiset_Order.thy	Mon Sep 05 15:00:37 2016 +0200
     5.2 +++ b/src/HOL/Library/Multiset_Order.thy	Mon Sep 05 15:47:50 2016 +0200
     5.3 @@ -69,7 +69,7 @@
     5.4      **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x>y. count M x < count N x)"
     5.5      by (simp_all add: less_multiset\<^sub>H\<^sub>O_def)
     5.6    from step(2) obtain M0 a K where
     5.7 -    *: "P = M0 + {#a#}" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
     5.8 +    *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
     5.9      by (blast elim: mult1_lessE)
    5.10    from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits )
    5.11    moreover
    5.12 @@ -180,7 +180,7 @@
    5.13    by (simp add: less_le_not_le subseteq_mset_def)
    5.14  
    5.15  lemma le_multiset_right_total:
    5.16 -  shows "M < M + {#x#}"
    5.17 +  shows "M < add_mset x M"
    5.18    unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
    5.19  
    5.20  lemma less_eq_multiset_empty_left[simp]:
    5.21 @@ -229,6 +229,52 @@
    5.22  
    5.23  end
    5.24  
    5.25 +
    5.26 +subsection \<open>Simprocs\<close>
    5.27 +
    5.28 +lemma mset_le_add_iff1:
    5.29 +  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (repeat_mset (i-j) u + m \<le> n)"
    5.30 +proof -
    5.31 +  assume "j \<le> i"
    5.32 +  then have "j + (i - j) = i"
    5.33 +    using le_add_diff_inverse by blast
    5.34 +  then show ?thesis
    5.35 +    by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
    5.36 +qed
    5.37 +
    5.38 +lemma mset_le_add_iff2:
    5.39 +  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<le> repeat_mset j u + n) = (m \<le> repeat_mset (j-i) u + n)"
    5.40 +proof -
    5.41 +  assume "i \<le> j"
    5.42 +  then have "i + (j - i) = j"
    5.43 +    using le_add_diff_inverse by blast
    5.44 +  then show ?thesis
    5.45 +    by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset)
    5.46 +qed
    5.47 +
    5.48 +lemma mset_less_add_iff1:
    5.49 +  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m < repeat_mset j u + n) = (repeat_mset (i-j) u + m < n)"
    5.50 +  by (simp add: less_le_not_le mset_le_add_iff1 mset_le_add_iff2)
    5.51 +
    5.52 +lemma mset_less_add_iff2:
    5.53 +     "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m < repeat_mset j u + n) = (m < repeat_mset (j-i) u + n)"
    5.54 +  by (simp add: less_le_not_le mset_le_add_iff1 mset_le_add_iff2)
    5.55 +
    5.56 +ML_file "multiset_order_simprocs.ML"
    5.57 +
    5.58 +simproc_setup msetless_cancel_numerals
    5.59 +  ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + n" |
    5.60 +   "add_mset a m < n" | "m < add_mset a n") =
    5.61 +  \<open>fn phi => Multiset_Order_Simprocs.less_cancel_msets\<close>
    5.62 +
    5.63 +simproc_setup msetle_cancel_numerals
    5.64 +  ("(l::'a::preorder multiset) + m \<le> n" | "(l::'a multiset) \<le> m + n" |
    5.65 +   "add_mset a m \<le> n" | "m \<le> add_mset a n") =
    5.66 +  \<open>fn phi => Multiset_Order_Simprocs.le_cancel_msets\<close>
    5.67 +
    5.68 +
    5.69 +subsection \<open>Additional facts and instantiations\<close>
    5.70 +
    5.71  lemma ex_gt_count_imp_le_multiset:
    5.72    "(\<forall>y :: 'a :: order. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
    5.73    unfolding less_multiset\<^sub>H\<^sub>O
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Library/multiset_order_simprocs.ML	Mon Sep 05 15:47:50 2016 +0200
     6.3 @@ -0,0 +1,35 @@
     6.4 +(* Author: Mathias Fleury, MPII
     6.5 +
     6.6 +
     6.7 +Simprocs for multisets ordering, based on the simprocs for nat numerals.
     6.8 +*)
     6.9 +
    6.10 +signature MULTISET_ORDER_SIMPROCS =
    6.11 +sig
    6.12 +  val less_cancel_msets: Proof.context -> cterm -> thm option
    6.13 +  val le_cancel_msets: Proof.context -> cterm -> thm option
    6.14 +end;
    6.15 +
    6.16 +structure Multiset_Order_Simprocs : MULTISET_ORDER_SIMPROCS =
    6.17 +struct
    6.18 +
    6.19 +structure LessCancelMultiset = CancelNumeralsFun
    6.20 + (open Multiset_Cancel_Common
    6.21 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
    6.22 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
    6.23 +  val bal_add1 = @{thm mset_less_add_iff1} RS trans
    6.24 +  val bal_add2 = @{thm mset_less_add_iff2} RS trans
    6.25 +);
    6.26 +
    6.27 +structure LeCancelMultiset = CancelNumeralsFun
    6.28 + (open Multiset_Cancel_Common
    6.29 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
    6.30 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
    6.31 +  val bal_add1 = @{thm mset_le_add_iff1} RS trans
    6.32 +  val bal_add2 = @{thm mset_le_add_iff2} RS trans
    6.33 +);
    6.34 +
    6.35 +val less_cancel_msets = LessCancelMultiset.proc;
    6.36 +val le_cancel_msets = LeCancelMultiset.proc;
    6.37 +
    6.38 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Library/multiset_simprocs.ML	Mon Sep 05 15:47:50 2016 +0200
     7.3 @@ -0,0 +1,56 @@
     7.4 +(* Author: Mathias Fleury, MPII
     7.5 +
     7.6 +
     7.7 +Simprocs for multisets, based on Larry Paulson's simprocs for
     7.8 +natural numbers and numerals.
     7.9 +*)
    7.10 +
    7.11 +signature MULTISET_SIMPROCS =
    7.12 +sig
    7.13 +  val eq_cancel_msets: Proof.context -> cterm -> thm option
    7.14 +  val subset_cancel_msets: Proof.context -> cterm -> thm option
    7.15 +  val subseteq_cancel_msets: Proof.context -> cterm -> thm option
    7.16 +  val diff_cancel_msets: Proof.context -> cterm -> thm option
    7.17 +end;
    7.18 +
    7.19 +structure Multiset_Simprocs : MULTISET_SIMPROCS =
    7.20 +struct
    7.21 +
    7.22 +structure EqCancelMultiset = CancelNumeralsFun
    7.23 + (open Multiset_Cancel_Common
    7.24 +  val mk_bal   = HOLogic.mk_eq
    7.25 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
    7.26 +  val bal_add1 = @{thm mset_eq_add_iff1} RS trans
    7.27 +  val bal_add2 = @{thm mset_eq_add_iff2} RS trans
    7.28 +);
    7.29 +
    7.30 +structure SubsetCancelMultiset = CancelNumeralsFun
    7.31 + (open Multiset_Cancel_Common
    7.32 +  val mk_bal   = HOLogic.mk_binrel @{const_name subset_mset}
    7.33 +  val dest_bal = HOLogic.dest_bin @{const_name subset_mset} dummyT
    7.34 +  val bal_add1 = @{thm mset_subset_add_iff1} RS trans
    7.35 +  val bal_add2 = @{thm mset_subset_add_iff2} RS trans
    7.36 +);
    7.37 +
    7.38 +structure SubseteqCancelMultiset = CancelNumeralsFun
    7.39 + (open Multiset_Cancel_Common
    7.40 +  val mk_bal   = HOLogic.mk_binrel @{const_name subseteq_mset}
    7.41 +  val dest_bal = HOLogic.dest_bin @{const_name subseteq_mset} dummyT
    7.42 +  val bal_add1 = @{thm mset_subseteq_add_iff1} RS trans
    7.43 +  val bal_add2 = @{thm mset_subseteq_add_iff2} RS trans
    7.44 +);
    7.45 +
    7.46 +structure DiffCancelMultiset = CancelNumeralsFun
    7.47 + (open Multiset_Cancel_Common
    7.48 +  val mk_bal   = HOLogic.mk_binop @{const_name Groups.minus}
    7.49 +  val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} dummyT
    7.50 +  val bal_add1 = @{thm mset_diff_add_eq1} RS trans
    7.51 +  val bal_add2 = @{thm mset_diff_add_eq2} RS trans
    7.52 +);
    7.53 +
    7.54 +val eq_cancel_msets = EqCancelMultiset.proc;
    7.55 +val subset_cancel_msets = SubsetCancelMultiset.proc;
    7.56 +val subseteq_cancel_msets = SubseteqCancelMultiset.proc;
    7.57 +val diff_cancel_msets = DiffCancelMultiset.proc;
    7.58 +
    7.59 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Library/multiset_simprocs_util.ML	Mon Sep 05 15:47:50 2016 +0200
     8.3 @@ -0,0 +1,176 @@
     8.4 +(* Author: Mathias Fleury, MPII
     8.5 +
     8.6 +
     8.7 +Datatructure for the cancelation simprocs for multisets, based on Larry Paulson's simprocs for
     8.8 +natural numbers and numerals.
     8.9 +*)
    8.10 +signature MULTISET_CANCEL_COMMON =
    8.11 +sig
    8.12 +  val mk_sum : typ -> term list -> term
    8.13 +  val dest_sum : term -> term list
    8.14 +  val mk_coeff : int * term -> term
    8.15 +  val dest_coeff : term -> int * term
    8.16 +  val find_first_coeff : term -> term list -> int * term list
    8.17 +  val trans_tac : Proof.context -> thm option -> tactic
    8.18 +
    8.19 +  val norm_ss1 : simpset
    8.20 +  val norm_ss2: simpset
    8.21 +  val norm_tac: Proof.context -> tactic
    8.22 +
    8.23 +  val numeral_simp_tac : Proof.context -> tactic
    8.24 +  val simplify_meta_eq : Proof.context -> thm -> thm
    8.25 +  val prove_conv : tactic list -> Proof.context -> thm list -> term * term -> thm option
    8.26 +end;
    8.27 +
    8.28 +structure Multiset_Cancel_Common : MULTISET_CANCEL_COMMON =
    8.29 +struct
    8.30 +
    8.31 +(*** Utilities ***)
    8.32 +
    8.33 +fun mk_repeat_mset (t, u) =
    8.34 +  let
    8.35 +    val T = fastype_of t;
    8.36 +    val U = fastype_of u;
    8.37 +  in Const (@{const_name "repeat_mset"}, T --> U --> U) $ t $ u end;
    8.38 +
    8.39 +(*Maps n to #n for n = 1, 2*)
    8.40 +val numeral_syms = [@{thm numeral_One} RS sym, @{thm numeral_2_eq_2} RS sym,
    8.41 +  @{thm numeral_1_eq_Suc_0} RS sym];
    8.42 +
    8.43 +val numeral_sym_ss =
    8.44 +  simpset_of (put_simpset HOL_basic_ss @{context} addsimps  numeral_syms);
    8.45 +
    8.46 +fun mk_number 1 = HOLogic.numeral_const HOLogic.natT $ HOLogic.one_const
    8.47 +  | mk_number n = HOLogic.mk_number HOLogic.natT n
    8.48 +fun dest_number t = Int.max (0, snd (HOLogic.dest_number t));
    8.49 +
    8.50 +fun find_first_numeral past (t::terms) =
    8.51 +    ((dest_number t, t, rev past @ terms)
    8.52 +    handle TERM _ => find_first_numeral (t::past) terms)
    8.53 +  | find_first_numeral _ [] = raise TERM("find_first_numeral", []);
    8.54 +
    8.55 +fun typed_zero T = Const (@{const_name "Groups.zero"}, T);
    8.56 +val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    8.57 +
    8.58 +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero.*)
    8.59 +fun mk_sum T [] = typed_zero T
    8.60 +  | mk_sum _ [t,u] = mk_plus (t, u)
    8.61 +  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
    8.62 +
    8.63 +val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} dummyT;
    8.64 +
    8.65 +
    8.66 +(*** Other simproc items ***)
    8.67 +
    8.68 +val bin_simps =
    8.69 +  [@{thm numeral_One} RS sym,
    8.70 +   @{thm add_numeral_left},
    8.71 +   @{thm diff_nat_numeral}, @{thm diff_0_eq_0}, @{thm diff_0},
    8.72 +   @{thm mult_numeral_left(1)},
    8.73 +   @{thm if_True}, @{thm if_False}, @{thm not_False_eq_True},
    8.74 +   @{thm nat_0}, @{thm nat_numeral}, @{thm nat_neg_numeral},
    8.75 +   @{thm add_mset_commute}, @{thm repeat_mset.simps(1)}] @
    8.76 +  @{thms arith_simps} @ @{thms rel_simps};
    8.77 +
    8.78 +
    8.79 +(*** CancelNumerals simprocs ***)
    8.80 +
    8.81 +val one = mk_number 1;
    8.82 +
    8.83 +fun mk_prod [] = one
    8.84 +  | mk_prod [t] = t
    8.85 +  | mk_prod (t :: ts) = if t = one then mk_prod ts else mk_repeat_mset (t, mk_prod ts);
    8.86 +
    8.87 +val dest_repeat_mset = HOLogic.dest_bin @{const_name Multiset.repeat_mset} dummyT
    8.88 +
    8.89 +fun dest_repeat_msets t =
    8.90 +  let val (t,u) = dest_repeat_mset t in
    8.91 +    t :: dest_repeat_msets u end
    8.92 +  handle TERM _ => [t];
    8.93 +
    8.94 +fun mk_coeff (k,t) = mk_repeat_mset (mk_number k, t);
    8.95 +
    8.96 +(*Express t as a product of (possibly) a numeral with other factors, sorted*)
    8.97 +fun dest_coeff t =
    8.98 +  let
    8.99 +    val ts = sort Term_Ord.term_ord (dest_repeat_msets t);
   8.100 +    val (n, _, ts') =
   8.101 +      find_first_numeral [] ts
   8.102 +      handle TERM _ => (1, one, ts);
   8.103 +  in (n, mk_prod ts') end;
   8.104 +
   8.105 +(*Find first coefficient-term THAT MATCHES u*)
   8.106 +fun find_first_coeff _ _ [] = raise TERM("find_first_coeff", [])
   8.107 +  | find_first_coeff past u (t::terms) =
   8.108 +    let val (n,u') = dest_coeff t in
   8.109 +      if u aconv u' then (n, rev past @ terms) else find_first_coeff (t::past) u terms end
   8.110 +    handle TERM _ => find_first_coeff (t::past) u terms;
   8.111 +
   8.112 +(*Split up a sum into the list of its constituent terms, on the way replace all the
   8.113 +\<open>add_mset a C\<close> by \<open>add_mset a {#}\<close> and \<open>C\<close>, iff C was not already the empty set*)
   8.114 +fun dest_add_mset (Const (@{const_name add_mset},  typ) $ a $
   8.115 +      Const (@{const_name "Groups.zero_class.zero"}, typ'), ts) =
   8.116 +    Const (@{const_name add_mset},  typ) $ a $ typed_zero typ' :: ts
   8.117 +  | dest_add_mset (Const (@{const_name add_mset},  typ) $ a $ mset, ts) =
   8.118 +    dest_add_mset (mset, Const (@{const_name add_mset}, typ) $ a $
   8.119 +      typed_zero (fastype_of mset) :: ts)
   8.120 +  | dest_add_mset (t, ts) =
   8.121 +    let val (t1,t2) = dest_plus t in
   8.122 +      dest_add_mset (t1, dest_add_mset (t2, ts)) end
   8.123 +    handle TERM _ => (t::ts);
   8.124 +
   8.125 +fun dest_add_mset_sum t = dest_add_mset (t, []);
   8.126 +
   8.127 +val rename_numerals = simplify (put_simpset numeral_sym_ss @{context}) o Thm.transfer @{theory};
   8.128 +
   8.129 +(*Simplify \<open>repeat_mset (Suc 0) n\<close>, \<open>n+0\<close>, and \<open>0+n\<close> to \<open>n\<close>*)
   8.130 +val add_0s  = map rename_numerals [@{thm Groups.add_0}, @{thm Groups.add_0_right}];
   8.131 +val mult_1s = map rename_numerals @{thms repeat_mset.simps(2)[of 0]};
   8.132 +
   8.133 +
   8.134 +(*And these help the simproc return False when appropriate. We use the same list as the nat
   8.135 +version.*)
   8.136 +val contra_rules =
   8.137 +  [@{thm union_mset_add_mset_left}, @{thm union_mset_add_mset_right},
   8.138 +   @{thm empty_not_add_mset}, @{thm add_mset_not_empty},
   8.139 +   @{thm subset_mset.le_zero_eq}, @{thm le_zero_eq}];
   8.140 +
   8.141 +val simplify_meta_eq =
   8.142 +  Arith_Data.simplify_meta_eq
   8.143 +    ([@{thm numeral_1_eq_Suc_0}, @{thm Nat.add_0}, @{thm Nat.add_0_right},
   8.144 +      @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right},
   8.145 +      @{thm Groups.add_0}, @{thm repeat_mset.simps(1)},
   8.146 +      @{thm monoid_add_class.add_0_right}] @
   8.147 +     contra_rules);
   8.148 +
   8.149 +val mk_sum = mk_sum;
   8.150 +val dest_sum = dest_add_mset_sum;
   8.151 +val mk_coeff = mk_coeff;
   8.152 +val dest_coeff = dest_coeff;
   8.153 +val find_first_coeff = find_first_coeff [];
   8.154 +val trans_tac = Numeral_Simprocs.trans_tac;
   8.155 +
   8.156 +val norm_ss1 =
   8.157 +  simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps
   8.158 +    numeral_syms @ add_0s @ mult_1s @ @{thms ac_simps});
   8.159 +
   8.160 +val norm_ss2 =
   8.161 +  simpset_of (put_simpset Numeral_Simprocs.num_ss @{context} addsimps
   8.162 +    bin_simps @
   8.163 +    [@{thm union_mset_add_mset_left},
   8.164 +     @{thm union_mset_add_mset_right}] @
   8.165 +    @{thms ac_simps});
   8.166 +
   8.167 +fun norm_tac ctxt =
   8.168 +  ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
   8.169 +  THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt));
   8.170 +
   8.171 +val mset_simps_ss =
   8.172 +  simpset_of (put_simpset HOL_basic_ss @{context} addsimps bin_simps);
   8.173 +
   8.174 +fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset mset_simps_ss ctxt));
   8.175 +
   8.176 +val simplify_meta_eq = simplify_meta_eq;
   8.177 +val prove_conv = Arith_Data.prove_conv;
   8.178 +
   8.179 +end
     9.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Mon Sep 05 15:00:37 2016 +0200
     9.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Mon Sep 05 15:47:50 2016 +0200
     9.3 @@ -211,8 +211,8 @@
     9.4      case empty then show ?case
     9.5      using \<open>prime_elem p\<close> by (simp add: prime_elem_not_unit)
     9.6    next
     9.7 -    case (add A a)
     9.8 -    then have "p dvd msetprod A * a" by simp
     9.9 +    case (add a A)
    9.10 +    then have "p dvd a * msetprod A" by simp
    9.11      with \<open>prime_elem p\<close> consider (A) "p dvd msetprod A" | (B) "p dvd a"
    9.12        by (blast dest: prime_elem_dvd_multD)
    9.13      then show ?case proof cases
    9.14 @@ -484,10 +484,10 @@
    9.15    case empty
    9.16    thus ?case by simp
    9.17  next
    9.18 -  case (add A p B)
    9.19 +  case (add p A B)
    9.20    hence p: "prime p" by simp
    9.21    define B' where "B' = B - {#p#}"
    9.22 -  from add.prems have "p dvd msetprod B" by (simp add: dvd_mult_right)
    9.23 +  from add.prems have "p dvd msetprod B" by (simp add: dvd_mult_left)
    9.24    with add.prems have "p \<in># B"
    9.25      by (subst (asm) (2) prime_dvd_msetprod_primes_iff) simp_all
    9.26    hence B: "B = B' + {#p#}" by (simp add: B'_def)
    9.27 @@ -498,7 +498,7 @@
    9.28  lemma normalize_msetprod_primes:
    9.29    "(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (msetprod A) = msetprod A"
    9.30  proof (induction A)
    9.31 -  case (add A p)
    9.32 +  case (add p A)
    9.33    hence "prime p" by simp
    9.34    hence "normalize p = p" by simp
    9.35    with add show ?case by (simp add: normalize_mult)
    9.36 @@ -746,7 +746,7 @@
    9.37    from prime_factorization_exists'[OF this] guess A . note A = this
    9.38    from A(1) have "P (unit_factor x * msetprod A)"
    9.39    proof (induction A)
    9.40 -    case (add A p)
    9.41 +    case (add p A)
    9.42      from add.prems have "prime p" by simp
    9.43      moreover from add.prems have "P (unit_factor x * msetprod A)" by (intro add.IH) simp_all
    9.44      ultimately have "P (p * (unit_factor x * msetprod A))" by (rule assms(3))
    9.45 @@ -1127,7 +1127,7 @@
    9.46    shows   "prime_factorization (msetprod A) = A"
    9.47    using assms
    9.48  proof (induction A)
    9.49 -  case (add A p)
    9.50 +  case (add p A)
    9.51    from add.prems[of 0] have "0 \<notin># A" by auto
    9.52    hence "msetprod A \<noteq> 0" by auto
    9.53    with add show ?case
    10.1 --- a/src/HOL/Probability/PMF_Impl.thy	Mon Sep 05 15:00:37 2016 +0200
    10.2 +++ b/src/HOL/Probability/PMF_Impl.thy	Mon Sep 05 15:47:50 2016 +0200
    10.3 @@ -527,6 +527,8 @@
    10.4  instance by standard (simp add: equal_pmf_def)
    10.5  end
    10.6  
    10.7 +definition single :: "'a \<Rightarrow> 'a multiset" where
    10.8 +"single s = {#s#}"
    10.9  
   10.10  definition (in term_syntax)
   10.11    pmfify :: "('a::typerep multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<Rightarrow>
    11.1 --- a/src/HOL/ex/Bubblesort.thy	Mon Sep 05 15:00:37 2016 +0200
    11.2 +++ b/src/HOL/ex/Bubblesort.thy	Mon Sep 05 15:47:50 2016 +0200
    11.3 @@ -58,7 +58,6 @@
    11.4    apply simp
    11.5   apply simp
    11.6  by(auto split: list.splits if_splits dest: bubble_minD_mset)
    11.7 -  (metis add_eq_conv_ex mset_bubble_min mset.simps(2))
    11.8  
    11.9  lemma set_bubblesort: "set (bubblesort xs) = set xs"
   11.10  by(rule mset_bubblesort[THEN mset_eq_setD])