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.5  
     1.6  
     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.39 +lemma sup_add_left1:
    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.43 +lemma sup_add_left2:
    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.47 +lemma sup_add_right1:
    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.51 +lemma sup_add_right2:
    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.57  
    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.64 -    (auto simp add: mem_set_multiset_eq inter_add_right1 inter_add_right2 ac_simps)
    1.65 +    by (induct xs arbitrary: ys)
    1.66 +      (auto simp add: mem_set_multiset_eq inter_add_right1 inter_add_right2 ac_simps)
    1.67 +  then show ?thesis by simp
    1.68 +qed
    1.69 +
    1.70 +lemma [code]:
    1.71 +  "multiset_of xs #\<union> multiset_of ys =
    1.72 +    multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
    1.73 +proof -
    1.74 +  have "\<And>zs. multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
    1.75 +      (multiset_of xs #\<union> multiset_of ys) + multiset_of zs"
    1.76 +    by (induct xs arbitrary: ys) (simp_all add: multiset_eq_iff)
    1.77    then show ?thesis by simp
    1.78  qed
    1.79