• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
      • Omaps
      • All-by-membership
      • In
      • Defset
      • Primitives
      • 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

• Std/osets

Union

(union x y) constructs the union of X and Y.

The logical definition is very simple, and the essential correctness property is given by union-in.

The execution uses a better, O(n) algorithm to merge the sets by exploiting the set order.

Definitions and Theorems

Function: union

(defun union (x y)
       (declare (xargs :guard (and (setp x) (setp y))))
       (mbe :logic (if (empty x)
                       (sfix y)
                       (insert (head x) (union (tail x) y)))
            :exec (fast-union x y nil)))

Theorem: union-set

(defthm union-set (setp (union x y)))

Theorem: union-sfix-cancel-x

(defthm union-sfix-cancel-x
        (equal (union (sfix x) y) (union x y)))

Theorem: union-sfix-cancel-y

(defthm union-sfix-cancel-y
        (equal (union x (sfix y)) (union x y)))

Theorem: union-empty-x

(defthm union-empty-x
        (implies (empty x)
                 (equal (union x y) (sfix y))))

Theorem: union-empty-y

(defthm union-empty-y
        (implies (empty y)
                 (equal (union x y) (sfix x))))

Theorem: union-empty

(defthm union-empty
        (equal (empty (union x y))
               (and (empty x) (empty y))))

Theorem: union-in

(defthm union-in
        (equal (in a (union x y))
               (or (in a x) (in a y))))

Theorem: union-symmetric

(defthm union-symmetric
        (equal (union x y) (union y x))
        :rule-classes ((:rewrite :loop-stopper ((x y)))))

Theorem: union-subset-x

(defthm union-subset-x (subset x (union x y)))

Theorem: union-subset-y

(defthm union-subset-y (subset y (union x y)))

Theorem: union-insert-x

(defthm union-insert-x
        (equal (union (insert a x) y)
               (insert a (union x y))))

Theorem: union-insert-y

(defthm union-insert-y
        (equal (union x (insert a y))
               (insert a (union x y))))

Theorem: union-with-subset-left

(defthm union-with-subset-left
        (implies (subset x y)
                 (equal (union x y) (sfix y)))
        :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: union-with-subset-right

(defthm union-with-subset-right
        (implies (subset x y)
                 (equal (union y x) (sfix y)))
        :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: union-self

(defthm union-self (equal (union x x) (sfix x)))

Theorem: union-associative

(defthm union-associative
        (equal (union (union x y) z)
               (union x (union y z))))

Theorem: union-commutative

(defthm union-commutative
        (equal (union x (union y z))
               (union y (union x z)))
        :rule-classes ((:rewrite :loop-stopper ((x y)))))

Theorem: union-outer-cancel

(defthm union-outer-cancel
        (equal (union x (union x z))
               (union x z)))