A library of obags (ordered bags), i.e. finite bags (a.k.a. multisets) represented as non-strictly ordered lists.

This is related to the library of osets (ordered sets), i.e. finite sets represented as strictly ordered lists.
The lists that represent obags are non-strictly ordered,
i.e. they may have (contiguous) duplicate elements.
Like osets capture (up to isomorphism)
the mathematical notion of finite sets (over ACL2 objects),
obags capture (up to isomorphism)
the mathematical notion of finite bags (over ACL2 objects).
In particular, obag equality is `equal`.

Since obags are lists,
in principle some list operations could be used on obags.
However, this library provides versions of those list operations
that have stronger guards (i.e. requiring obags instead of just lists)
and that treat non-obags as the empty obag.
That is, the obag operations respect a `non-bag convention'
analogous to the non-set convention respected by the oset operations;
some of the latter are, analogously,
versions of list operations (e.g. `head` for `car`),
motivated by the fact that the list operations
do not respect the non-set convention.

The obag operations
`bagp`,
`bfix`,
`emptyp`,
`head`,
`tail`, and
`insert`
are ``primitive'' in the same sense as the oset primitives: their logical definitions depend on
the underlying representation as lists,
and provide replacements of list operations
that respect the `non-bag convention'.
The logical definitions of the other obag operations
are in terms of the primitive operations,
without reference to the underlying list representation.

There are different logically equivalent ways to define obag operations.
The current definitions (as well as their names) are preliminary
and could be improved if needed;
these definitions favor ease of reasoning over efficiency of execution,
but, as done in osets, `mbe` could be used to provide
equivalent efficient definitions for execution.
As it is often possible to reason about osets abstractly
(i.e. without regard to their underlying list representation),
it should be often possible to reason about obags abstractly
(i.e. without regard to their underlying list representation),
using the theorems provided by this library.
The current theorems are preliminary
and could be improved and extended if needed.
The empty obag is

Since osets are in the

This obag library is in the same

This obag library could become a new `ACL2::std/osets`.

Compared to using the built-in ACL2::lists to represent bags,
obags are closer to the mathematical notion of bags,
at the cost of maintaining their non-strict order.
These tradeoffs are analogous to the ones between using osets
and using the built-in ACL2::lists to represent sets.
The bag library in

- Bagp
- Recognize obags.
- Bag
- A fixtype of obags.
- Tail
- Rest of a non-empty obag after removing an occurrence of its smallest element.
- Head
- Smallest element of a non-empty obag.
- Emptyp
- Check if an obag is empty.
- Subbag
- Check if (every occurrence of) every value in the first obag is also (an occurrence of) a value in the second obag.
- Intersect
- Intersection of all (the occurrences of) all the elements of two obags.
- Union
- Union of all (the occurrences of) all the elements of two obags.
- Insert
- Add (an occurrence of) a value to an obag.
- Difference
- Remove from the first obag all (the occurrences of) the elements of the second obag.
- Delete
- Remove (an occurrence of) a value from an obag.
- Cardinality
- Number of (occurrences of) elements in an obag.
- Bfix
- Fixing function for obags.
- In
- Check if a values occurs in an obag.
- Occs
- Number of occurrences of a value in an obag.