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

• 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 (emptyp 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-emptyp-x

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

Theorem: union-emptyp-y

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

Theorem: union-emptyp

(defthm union-emptyp
  (equal (emptyp (union x y))
         (and (emptyp x) (emptyp 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)))