opaque union MultiSet<T>

opaque define cnt : (fn <T> MultiSet<T> -> (fn T -> UInt))

auto cnt_empty

cnt_empty: (all T:type. (all x:T. cnt(@m_empty<T>())(x) = 0))

cnt_equal: (all T:type, A:MultiSet<T>, B:MultiSet<T>. (if cnt(A) = cnt(B) then A = B))

auto cnt_equal_equal

cnt_equal_equal: (all T:type, A:MultiSet<T>, B:MultiSet<T>. (cnt(A) = cnt(B)) = (A = B))

auto cnt_one

cnt_one: (all T:type. (all x:T. cnt(m_one(x))(x) = 1))

cnt_sum: (all T:type. (all A:MultiSet<T>, B:MultiSet<T>, x:T. cnt(A ⨄ B)(x) = cnt(A)(x) + cnt(B)(x)))

auto empty_m_sum

empty_m_sum: (all T:type. (all A:MultiSet<T>. @m_empty<T>() ⨄ A = A))

opaque define m_empty : (fn <T>  -> MultiSet<T>)

opaque define m_one : (fn <T> T -> MultiSet<T>)

m_sum_assoc: (all T:type. (all A:MultiSet<T>, B:MultiSet<T>, C:MultiSet<T>. (A ⨄ B) ⨄ C = A ⨄ (B ⨄ C)))

m_sum_commutes: (all T:type. (all A:MultiSet<T>, B:MultiSet<T>. A ⨄ B = B ⨄ A))

auto m_sum_empty

m_sum_empty: (all T:type. (all A:MultiSet<T>. A ⨄ @m_empty<T>() = A))

opaque define operator ⨄ : (fn <T> (MultiSet<T>, MultiSet<T>) -> MultiSet<T>)

define set_of_mset : (fn <T> MultiSet<T> -> Set<T>) = generic T {
      fun M {
        set_of_pred(fun x { (if cnt(M)(x) = 0 then false else true) })
      }
    }

som_empty: (all T:type. set_of_mset(@m_empty<T>()) = @empty_set<T>())

som_one_single: (all T:type. (all x:T. set_of_mset(m_one(x)) = single(x)))

som_union: (all T:type. (all A:MultiSet<T>, B:MultiSet<T>. set_of_mset(A ⨄ B) = set_of_mset(A) ∪ set_of_mset(B)))