sup on multisets

--- a/src/HOL/Library/DAList_Multiset.thy	Thu Apr 04 22:29:59 2013 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy	Thu Apr 04 22:46:14 2013 +0200
@@ -11,6 +11,14 @@
 text {* Delete prexisting code equations *}
 
 lemma [code, code del]:
+  "{#} = {#}"
+  ..
+
+lemma [code, code del]:
+  "single = single"
+  ..
+
+lemma [code, code del]:
   "plus = (plus :: 'a multiset \<Rightarrow> _)"
   ..
 
@@ -23,6 +31,10 @@
   ..
 
 lemma [code, code del]:
+  "sup = (sup :: 'a multiset \<Rightarrow> _)"
+  ..
+
+lemma [code, code del]:
   "image_mset = image_mset"
   ..
 
@@ -222,11 +234,8 @@
 qed
 
 declare multiset_inter_def [code]
-
-lemma [code]:
-  "multiset_of [] = {#}"
-  "multiset_of (x # xs) = multiset_of xs + {#x#}"
-  by simp_all
+declare sup_multiset_def [code]
+declare multiset_of.simps [code]
 
 instantiation multiset :: (exhaustive) exhaustive
 begin

--- a/src/HOL/Library/Multiset.thy	Thu Apr 04 22:29:59 2013 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Apr 04 22:46:14 2013 +0200
@@ -438,6 +438,55 @@
   by (simp add: multiset_eq_iff)
 
 
+subsubsection {* Bounded union *}
+
+instantiation multiset :: (type) semilattice_sup
+begin
+
+definition sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
+  "sup_multiset A B = A + (B - A)"
+
+instance
+proof -
+  have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" by arith
+  show "OFCLASS('a multiset, semilattice_sup_class)"
+    by default (auto simp add: sup_multiset_def mset_le_def aux)
+qed
+
+end
+
+abbreviation sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<union>" 70) where
+  "sup_multiset \<equiv> sup"
+
+lemma sup_multiset_count [simp]:
+  "count (A #\<union> B) x = max (count A x) (count B x)"
+  by (simp add: sup_multiset_def)
+
+lemma empty_sup [simp]:
+  "{#} #\<union> M = M"
+  by (simp add: multiset_eq_iff)
+
+lemma sup_empty [simp]:
+  "M #\<union> {#} = M"
+  by (simp add: multiset_eq_iff)
+
+lemma sup_add_left1:
+  "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> N) + {#x#}"
+  by (simp add: multiset_eq_iff)
+
+lemma sup_add_left2:
+  "x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> (N - {#x#})) + {#x#}"
+  by (simp add: multiset_eq_iff)
+
+lemma sup_add_right1:
+  "\<not> x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = (N #\<union> M) + {#x#}"
+  by (simp add: multiset_eq_iff)
+
+lemma sup_add_right2:
+  "x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N - {#x#}) #\<union> M) + {#x#}"
+  by (simp add: multiset_eq_iff)
+
+
 subsubsection {* Filter (with comprehension syntax) *}
 
 text {* Multiset comprehension *}
@@ -1982,8 +2031,18 @@
   have "\<And>zs. multiset_of (snd (fold (\<lambda>x (ys, zs).
     if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, zs))) =
       (multiset_of xs #\<inter> multiset_of ys) + multiset_of zs"
-  by (induct xs arbitrary: ys)
-    (auto simp add: mem_set_multiset_eq inter_add_right1 inter_add_right2 ac_simps)
+    by (induct xs arbitrary: ys)
+      (auto simp add: mem_set_multiset_eq inter_add_right1 inter_add_right2 ac_simps)
+  then show ?thesis by simp
+qed
+
+lemma [code]:
+  "multiset_of xs #\<union> multiset_of ys =
+    multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
+proof -
+  have "\<And>zs. multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
+      (multiset_of xs #\<union> multiset_of ys) + multiset_of zs"
+    by (induct xs arbitrary: ys) (simp_all add: multiset_eq_iff)
   then show ?thesis by simp
 qed