Theory Sub_Sums

(*
    Author:     René Thiemann
    License:    BSD
*)
section ‹Calculating All Possible Sums of Sub-Multisets›
theory Sub_Sums
  imports 
    Main 
    "HOL-Library.Multiset"
begin

fun sub_mset_sums :: "'a :: comm_monoid_add list ⇒ 'a set" where
  "sub_mset_sums [] = {0}"
| "sub_mset_sums (x # xs) = (let S = sub_mset_sums xs in S ∪ ( (+) x) ` S)" 

lemma subset_add_mset: "ys ⊆# add_mset x zs ⟷ (ys ⊆# zs ∨ (∃ xs. xs ⊆# zs ∧ ys = add_mset x xs))" 
  (is "?l = ?r")
proof 
  have sub: "ys ⊆# zs ⟹ ys ⊆# add_mset x zs"
    by (metis add_mset_remove_trivial diff_subset_eq_self subset_mset.dual_order.trans)
  assume ?r
  thus ?l using sub by auto
next
  assume l: ?l
  show ?r
  proof (cases "x ∈# ys")
    case True
    define xs where "xs = (ys - {# x #})" 
    from True have ys: "ys = add_mset x xs" unfolding xs_def by auto 
    from l[unfolded ys] have "xs ⊆# zs" by auto
    thus ?r unfolding ys by auto
  next
    case False
    with l have "ys ⊆# zs" by (simp add: subset_mset.le_iff_sup)
    thus ?thesis by auto
  qed
qed

lemma sub_mset_sums[simp]: "sub_mset_sums xs = sum_mset ` { ys. ys ⊆# mset xs }" 
proof (induct xs)
  case (Cons x xs)
  have id: "{ys. ys ⊆# mset (x # xs)} = {ys. ys ⊆# mset xs} ∪ {add_mset x ys | ys. ys ⊆# mset xs}" 
    unfolding mset.simps subset_add_mset by auto
  show ?case unfolding sub_mset_sums.simps Let_def Cons id image_Un 
    by force
qed auto

end