		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 ((empty 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)