		Search-engine friendly clone of the ACL2 documentation.

Obags

Insert

Add (an occurrence of) a value to an obag.

Signature
(insert x bag) → bag1
Arguments: bag — Guard (bagp bag).
Returns: bag1 — Type (bagp bag1).

This is similar to set::insert on osets.

Definitions and Theorems

Function: insert

(defun insert (x bag)
  (declare (xargs :guard (bagp bag)))
  (let ((__function__ 'insert))
    (declare (ignorable __function__))
    (cond ((emptyp bag) (list x))
          ((equal x (head bag)) (cons x bag))
          ((<< x (head bag)) (cons x bag))
          (t (cons (head bag)
                   (insert x (tail bag)))))))

Theorem: bagp-of-insert

(defthm bagp-of-insert
  (b* ((bag1 (insert x bag))) (bagp bag1))
  :rule-classes :rewrite)