• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
      • Omaps
      • All-by-membership
      • In
      • Defset
      • Primitives
        • Setp
        • Insert
          • Weak-insert-induction
        • Head
        • Tail
        • Sfix
        • Empty
      • Subset
      • Mergesort
      • Intersect
      • Union
      • Pick-a-point-subset-strategy
      • Delete
      • Difference
      • Cardinality
      • Set
      • Double-containment
      • Intersectp
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Primitives

Insert

(insert a x) adds the element a to the set X.

This is the fundamental set constructor. It is similar to cons for lists, but of course performs an ordered insertion. It respects the non-set convention and treats any ill-formed input as the empty set.

Efficiency note. Insert is O(n). It is very inefficient to call it repeatedly. Instead, consider building sets with mergesort or out of other sets using union.

The :exec version just inlines the set primitives and does one level of loop unrolling. On CCL, it runs about 1.65x faster than the :logic version on the following loop:

;; 1.92 seconds :logic, 1.16 seconds :exec
(let ((acc nil))
 (gc$)
 (time$ (loop for i fixnum from 1 to 10000 do
              (setq acc (set::insert i acc)))))

Definitions and Theorems

Function: insert

(defun
  insert (a x)
  (declare (xargs :guard (setp x)))
  (mbe :logic (cond ((empty x) (list a))
                    ((equal (head x) a) x)
                    ((<< a (head x)) (cons a x))
                    (t (cons (head x) (insert a (tail x)))))
       :exec (cond ((null x) (cons a nil))
                   ((equal (car x) a) x)
                   ((fast-lexorder a (car x)) (cons a x))
                   ((null (cdr x))
                    (cons (car x) (cons a nil)))
                   ((equal (cadr x) a) x)
                   ((fast-lexorder a (cadr x))
                    (cons (car x) (cons a (cdr x))))
                   (t (cons (car x)
                            (cons (cadr x) (insert a (cddr x))))))))

Theorem: insert-produces-set

(defthm insert-produces-set (setp (insert a x)))

Theorem: insert-sfix-cancel

(defthm insert-sfix-cancel
        (equal (insert a (sfix x))
               (insert a x)))

Theorem: insert-never-empty

(defthm insert-never-empty
        (not (empty (insert a x))))

Theorem: insert-when-empty

(defthm insert-when-empty
        (implies (and (syntaxp (not (equal x ''nil)))
                      (empty x))
                 (equal (insert a x) (insert a nil))))

Theorem: head-of-insert-a-nil

(defthm head-of-insert-a-nil
        (equal (head (insert a nil)) a))

Theorem: tail-of-insert-a-nil

(defthm tail-of-insert-a-nil
        (equal (tail (insert a nil)) nil))

Theorem: head-insert

(defthm head-insert
        (equal (head (insert a x))
               (cond ((empty x) a)
                     ((<< a (head x)) a)
                     (t (head x)))))

Theorem: tail-insert

(defthm tail-insert
        (equal (tail (insert a x))
               (cond ((empty x) (sfix x))
                     ((<< a (head x)) (sfix x))
                     ((equal a (head x)) (tail x))
                     (t (insert a (tail x))))))

Theorem: repeated-insert

(defthm repeated-insert
        (equal (insert a (insert a x))
               (insert a x)))

Theorem: insert-insert

(defthm insert-insert
        (equal (insert a (insert b x))
               (insert b (insert a x)))
        :rule-classes ((:rewrite :loop-stopper ((a b)))))

Theorem: insert-head

(defthm insert-head
        (implies (not (empty x))
                 (equal (insert (head x) x) x)))

Theorem: insert-head-tail

(defthm insert-head-tail
        (implies (not (empty x))
                 (equal (insert (head x) (tail x)) x)))

Theorem: insert-induction-case

(defthm insert-induction-case
        (implies (and (not (<< a (head x)))
                      (not (equal a (head x)))
                      (not (empty x)))
                 (equal (insert (head x) (insert a (tail x)))
                        (insert a x))))

Theorem: insert-identity

(defthm insert-identity
        (implies (in a x)
                 (equal (insert a x) x)))

Theorem: in-insert

(defthm in-insert
        (equal (in a (insert b x))
               (or (in a x) (equal a b))))

Subtopics

Weak-insert-induction

Inducting over insert without exposing the set order.