A library of omaps (ordered maps), i.e. finite maps represented as strictly ordered alists.

This is related to the library of osets (ordered sets), i.e. finite sets represented as strictly ordered lists.
Like osets capture (up to isomorphism)
the mathematical notion of finite sets (over ACL2 objects),
omaps capture (up to isomorphism)
the mathematical notion of finite maps (over ACL2 objects).
In particular, omap equality is `equal`.

Since the total order on ACL2 values is lexicographic on `cons` pairs,
an omap is an oset of `cons` pairs;
furthermore, an omap is an alist.
While then, in principle,
some oset and alist operations could be used on omaps,
this library provides versions of those oset and alist operations
that have stronger guards
(i.e. requiring omaps instead of just osets or alists)
and that treat non-omaps as the empty omap.
That is, the omap operations respect a `non-map convention'
analogous to the non-set convention respected by the oset operations;
some of the latter are, analogously,
versions of list operations (e.g. `set::head` for `car`),
motivated by the fact that the list operations
do not respect the non-set convention.

The omap operations
`mapp`,
`mfix`,
`empty`,
`head`,
`tail`, and
`update`
are ``primitive'' in the same sense as the oset primitives: their logical definitions depend on
the underlying representation as alists,
and provide replacements of alist operations
that respect the `non-map convention'.
The logical definitions of the other omap operations
are in terms of the primitive operations,
without reference to the underlying alist representation.

There are different logically equivalent ways to define omap 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
provably 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 omaps abstractly
(i.e. without regard to their underlying alist representation),
using the theorems provided by this library.
The current theorems are preliminary
and could be improved and extended if needed.
The empty omap is

Since osets are in the

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

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

Compared to the records in

- Defomap
- Generate a
fixtype of omaps whose keys and values have specified fixtypes. - Update
- Set a key to a value in an omap.
- Mapp
- Recognize omaps.
- In
- Check if a key is in an omap.
- Update*
- Update a map with another map.
- Size
- Size of an omap.
- Keys
- Oset of the keys of an omap.
- From-lists
- Build an omap from a list of keys and a list of corresponding values.
- Update-induction-on-maps
- Induction on omaps based on
abstract characterization of
`update`. - Compatiblep
- Check if two omaps are compatible, in the sense that they map their common keys to the same values.
- Head
- Smallest key, and associated value, of a non-empty omap.
- Tail
- Rest of a non-empty omap after removing its smallest pair.
- Restrict
- Restrict an omap to a set of keys.
- Map
- A fixtype of omaps.
- Submap
- Check if an omap is a submap of another omap.
- Rlookup
- Set of keys to which a value is associated.
- Empty
- Check if an omap is empty.
- In*
- Check if every key in a set is in an omap.
- Rlookup*
- Set of keys to which any value in a set is associated.
- Lookup*
- Set of values associated to a set of keys in an omap.
- Values
- Oset of the values of an omap.
- Delete*
- Remove keys, and associated values, from an omap.
- Delete
- Remove a key, and associated value, from an omap.
- Mfix
- Fixing function for omaps.
- Lookup
- Value associated to a key in an omap.
- Head-val
- Value associated to the smallest key of a non-empty omap.
- Head-key
- Smallest key of a non-empty omap.
- Omap-induction2
- Induction on two omaps, applying
`tail`to both. - Omap-order-rules
- Some rules involving the ordering in omaps.