-- =============================================================
-- Theory of Bags.
-- =============================================================

-- ********
--! FUNS
-- ********

-- Bag should be an ADT, not an algebraic DT.
-- By declaring the bag operations primitive, we cannot unfold them.

data Bag a = Bag

primitive emptybag     "emptybag"     :: Bag a
primitive nonemptybag  "nonemptybag"  :: a -> Bag a -> Bag a
primitive singletonbag "singletonbag" :: a -> Bag a
primitive unionbag     "unionbag"     :: Bag a -> Bag a -> Bag a
primitive without      "without"      :: Bag a -> a -> Bag a
primitive elembag      "elembag"      :: a -> Bag a -> Bool
primitive equals       "equals"       :: Bag a -> Bag a -> Bool
primitive minbag       "minbag"       :: Bag a -> a

-- Construction of a bag from a list.

elementsof :: [a] -> Bag a
elementsof [] = emptybag
elementsof (x:xs) = nonemptybag x (elementsof xs)

-- ********
--! RULES
-- ********

-- -------------------------------------------------------------
-- Constructive part of the specification.
-- -------------------------------------------------------------

-- singletonbag is a derived constructor.

bag_singleton e =
  []
  |=
  singletonbag e
  <=>
  nonemptybag e emptybag

-- unionbag is a derived constructor.

bag_union_empty b =
  []
  |=
  emptybag `unionbag` b
  <=>
  b

bag_union_nonempty e b1 b2 =
  []
  |=
  nonemptybag e b1 `unionbag` b2
  <=>
  nonemptybag e (b1 `unionbag` b2)

-- Axioms for without.

bag_without_empty e =
  []
  |=
  emptybag `without` e
  <=>
  emptybag

bag_without_nonempty b e1 e2 =
  []
  |=
  nonemptybag e1 b `without` e2
  <=>
  if e1 == e2 then b else nonemptybag e1 (b `without` e2)

-- Axioms for elembag.

bag_elem_empty e =
  []
  |=
  e `elembag` emptybag
  <=>
  False

bag_elem_nonempty b e1 e2 =
  []
  |=
  e1 `elembag` nonemptybag e2 b
  <=>
  e1 == e2 || e1 `elembag` b

-- The equality of two bags is sufficiently defined by the following rule.
-- The other cases are covered by reflexivity and commutativity.

bag_equals e b1 b2 =
  []
  |=
  nonemptybag e b1 `equals` b2
  <=>
  e `elembag` b2 && b1 `equals` (b2 `without` e)

-- -------------------------------------------------------------
-- Non-constructive part of the specification.
-- -------------------------------------------------------------

-- The minimum is specified according to construction from lists.
-- We have minbag . elementsof = minimum (where defined).

bag_minimum_list x xs =
  []
  |=
  minbag (elementsof (x:xs))
  <=>
  minimum (x:xs)

-- -------------------------------------------------------------
-- Observational equality.
-- -------------------------------------------------------------

bag_add_union_equals b1 b2 b3 =
  []
  |=
  b1 `equals` b2
  <=>
  (b3 `unionbag` b1) `equals` (b3 `unionbag` b2)

bag_equals_in_min b1 b2 cn =
  []
  |=
  b1 `equals` b2 && cn (minbag b1)
  <=>
  b1 `equals` b2 && cn (minbag b2)

-- ********
--! CLAUSES
-- ********

reflexive equals
transitive equals
commutative equals

associative unionbag
commutative unionbag