src/HOL/Library/Multiset.thy
 changeset 51623 1194b438426a parent 51600 197e25f13f0c child 52289 83ce5d2841e7
1.1 --- a/src/HOL/Library/Multiset.thy	Thu Apr 04 22:29:59 2013 +0200
1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Apr 04 22:46:14 2013 +0200
1.3 @@ -438,6 +438,55 @@
1.4    by (simp add: multiset_eq_iff)
1.7 +subsubsection {* Bounded union *}
1.8 +
1.9 +instantiation multiset :: (type) semilattice_sup
1.10 +begin
1.11 +
1.12 +definition sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
1.13 +  "sup_multiset A B = A + (B - A)"
1.14 +
1.15 +instance
1.16 +proof -
1.17 +  have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" by arith
1.18 +  show "OFCLASS('a multiset, semilattice_sup_class)"
1.19 +    by default (auto simp add: sup_multiset_def mset_le_def aux)
1.20 +qed
1.21 +
1.22 +end
1.23 +
1.24 +abbreviation sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<union>" 70) where
1.25 +  "sup_multiset \<equiv> sup"
1.26 +
1.27 +lemma sup_multiset_count [simp]:
1.28 +  "count (A #\<union> B) x = max (count A x) (count B x)"
1.29 +  by (simp add: sup_multiset_def)
1.30 +
1.31 +lemma empty_sup [simp]:
1.32 +  "{#} #\<union> M = M"
1.33 +  by (simp add: multiset_eq_iff)
1.34 +
1.35 +lemma sup_empty [simp]:
1.36 +  "M #\<union> {#} = M"
1.37 +  by (simp add: multiset_eq_iff)
1.38 +
1.40 +  "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> N) + {#x#}"
1.41 +  by (simp add: multiset_eq_iff)
1.42 +
1.44 +  "x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> (N - {#x#})) + {#x#}"
1.45 +  by (simp add: multiset_eq_iff)
1.46 +
1.48 +  "\<not> x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = (N #\<union> M) + {#x#}"
1.49 +  by (simp add: multiset_eq_iff)
1.50 +
1.52 +  "x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N - {#x#}) #\<union> M) + {#x#}"
1.53 +  by (simp add: multiset_eq_iff)
1.54 +
1.55 +
1.56  subsubsection {* Filter (with comprehension syntax) *}
1.58  text {* Multiset comprehension *}
1.59 @@ -1982,8 +2031,18 @@
1.60    have "\<And>zs. multiset_of (snd (fold (\<lambda>x (ys, zs).
1.61      if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, zs))) =
1.62        (multiset_of xs #\<inter> multiset_of ys) + multiset_of zs"
1.63 -  by (induct xs arbitrary: ys)
1.65 +    by (induct xs arbitrary: ys)