sup on multisets
authorhaftmann
Thu Apr 04 22:46:14 2013 +0200 (2013-04-04)
changeset 516231194b438426a
parent 51622 183f30bc11de
child 51624 c839ccebf2fb
sup on multisets
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/DAList_Multiset.thy	Thu Apr 04 22:29:59 2013 +0200
     1.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Thu Apr 04 22:46:14 2013 +0200
     1.3 @@ -11,6 +11,14 @@
     1.4  text {* Delete prexisting code equations *}
     1.5  
     1.6  lemma [code, code del]:
     1.7 +  "{#} = {#}"
     1.8 +  ..
     1.9 +
    1.10 +lemma [code, code del]:
    1.11 +  "single = single"
    1.12 +  ..
    1.13 +
    1.14 +lemma [code, code del]:
    1.15    "plus = (plus :: 'a multiset \<Rightarrow> _)"
    1.16    ..
    1.17  
    1.18 @@ -23,6 +31,10 @@
    1.19    ..
    1.20  
    1.21  lemma [code, code del]:
    1.22 +  "sup = (sup :: 'a multiset \<Rightarrow> _)"
    1.23 +  ..
    1.24 +
    1.25 +lemma [code, code del]:
    1.26    "image_mset = image_mset"
    1.27    ..
    1.28  
    1.29 @@ -222,11 +234,8 @@
    1.30  qed
    1.31  
    1.32  declare multiset_inter_def [code]
    1.33 -
    1.34 -lemma [code]:
    1.35 -  "multiset_of [] = {#}"
    1.36 -  "multiset_of (x # xs) = multiset_of xs + {#x#}"
    1.37 -  by simp_all
    1.38 +declare sup_multiset_def [code]
    1.39 +declare multiset_of.simps [code]
    1.40  
    1.41  instantiation multiset :: (exhaustive) exhaustive
    1.42  begin
     2.1 --- a/src/HOL/Library/Multiset.thy	Thu Apr 04 22:29:59 2013 +0200
     2.2 +++ b/src/HOL/Library/Multiset.thy	Thu Apr 04 22:46:14 2013 +0200
     2.3 @@ -438,6 +438,55 @@
     2.4    by (simp add: multiset_eq_iff)
     2.5  
     2.6  
     2.7 +subsubsection {* Bounded union *}
     2.8 +
     2.9 +instantiation multiset :: (type) semilattice_sup
    2.10 +begin
    2.11 +
    2.12 +definition sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
    2.13 +  "sup_multiset A B = A + (B - A)"
    2.14 +
    2.15 +instance
    2.16 +proof -
    2.17 +  have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" by arith
    2.18 +  show "OFCLASS('a multiset, semilattice_sup_class)"
    2.19 +    by default (auto simp add: sup_multiset_def mset_le_def aux)
    2.20 +qed
    2.21 +
    2.22 +end
    2.23 +
    2.24 +abbreviation sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<union>" 70) where
    2.25 +  "sup_multiset \<equiv> sup"
    2.26 +
    2.27 +lemma sup_multiset_count [simp]:
    2.28 +  "count (A #\<union> B) x = max (count A x) (count B x)"
    2.29 +  by (simp add: sup_multiset_def)
    2.30 +
    2.31 +lemma empty_sup [simp]:
    2.32 +  "{#} #\<union> M = M"
    2.33 +  by (simp add: multiset_eq_iff)
    2.34 +
    2.35 +lemma sup_empty [simp]:
    2.36 +  "M #\<union> {#} = M"
    2.37 +  by (simp add: multiset_eq_iff)
    2.38 +
    2.39 +lemma sup_add_left1:
    2.40 +  "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> N) + {#x#}"
    2.41 +  by (simp add: multiset_eq_iff)
    2.42 +
    2.43 +lemma sup_add_left2:
    2.44 +  "x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> (N - {#x#})) + {#x#}"
    2.45 +  by (simp add: multiset_eq_iff)
    2.46 +
    2.47 +lemma sup_add_right1:
    2.48 +  "\<not> x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = (N #\<union> M) + {#x#}"
    2.49 +  by (simp add: multiset_eq_iff)
    2.50 +
    2.51 +lemma sup_add_right2:
    2.52 +  "x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N - {#x#}) #\<union> M) + {#x#}"
    2.53 +  by (simp add: multiset_eq_iff)
    2.54 +
    2.55 +
    2.56  subsubsection {* Filter (with comprehension syntax) *}
    2.57  
    2.58  text {* Multiset comprehension *}
    2.59 @@ -1982,8 +2031,18 @@
    2.60    have "\<And>zs. multiset_of (snd (fold (\<lambda>x (ys, zs).
    2.61      if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, zs))) =
    2.62        (multiset_of xs #\<inter> multiset_of ys) + multiset_of zs"
    2.63 -  by (induct xs arbitrary: ys)
    2.64 -    (auto simp add: mem_set_multiset_eq inter_add_right1 inter_add_right2 ac_simps)
    2.65 +    by (induct xs arbitrary: ys)
    2.66 +      (auto simp add: mem_set_multiset_eq inter_add_right1 inter_add_right2 ac_simps)
    2.67 +  then show ?thesis by simp
    2.68 +qed
    2.69 +
    2.70 +lemma [code]:
    2.71 +  "multiset_of xs #\<union> multiset_of ys =
    2.72 +    multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, [])))"
    2.73 +proof -
    2.74 +  have "\<And>zs. multiset_of (split append (fold (\<lambda>x (ys, zs). (remove1 x ys, x # zs)) xs (ys, zs))) =
    2.75 +      (multiset_of xs #\<union> multiset_of ys) + multiset_of zs"
    2.76 +    by (induct xs arbitrary: ys) (simp_all add: multiset_eq_iff)
    2.77    then show ?thesis by simp
    2.78  qed
    2.79