• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
      • Bitsets
      • Sbitsets
        • Sbitset-members
        • Sbitset-pairp
        • Sbitsetp
        • Sbitset-intersect
        • Sbitset-difference
        • Sbitset-union
        • Sbitset-singleton
        • Sbitset-fix
      • Reasoning
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Sbitsets

Sbitset-union

(sbitset-union X Y ...) constructs the set X U Y U ....

Macro: sbitset-union

(defmacro sbitset-union (&rest args)
  (cond ((atom args) nil)
        ((atom (cdr args)) (car args))
        (t (xxxjoin 'sbitset-binary-union args))))

Definitions and Theorems

Function: sbitset-union-exec

(defun sbitset-union-exec (x y)
 (declare (xargs :guard (and (sbitsetp x) (sbitsetp y))))
 (let ((__function__ 'sbitset-union-exec))
   (declare (ignorable __function__))
   (b*
    (((when (atom x)) y)
     ((when (atom y)) x)
     (x1 (car x))
     (y1 (car y))
     ((the unsigned-byte x1.offset)
      (sbitset-pair-offset x1))
     ((the unsigned-byte y1.offset)
      (sbitset-pair-offset y1))
     ((when (< x1.offset y1.offset))
      (cons x1 (sbitset-union-exec (cdr x) y)))
     ((unless (eql x1.offset y1.offset))
      (cons y1 (sbitset-union-exec x (cdr y))))
     (x1.block (sbitset-pair-block x1))
     (y1.block (sbitset-pair-block y1))
     (new-block
          (the-sbitset-block (logior (the-sbitset-block x1.block)
                                     (the-sbitset-block y1.block))))
     (new-pair (sbitset-pair x1.offset new-block)))
    (cons new-pair
          (sbitset-union-exec (cdr x) (cdr y))))))

Function: sbitset-binary-union$inline

(defun sbitset-binary-union$inline (x y)
  (declare (xargs :guard (and (sbitsetp x) (sbitsetp y))))
  (let ((__function__ 'sbitset-binary-union))
    (declare (ignorable __function__))
    (mbe :logic (sbitset-union-exec (sbitset-fix x)
                                    (sbitset-fix y))
         :exec (sbitset-union-exec x y))))

Theorem: sbitsetp-of-sbitset-union-exec

(defthm sbitsetp-of-sbitset-union-exec
  (implies (and (sbitsetp x) (sbitsetp y))
           (sbitsetp (sbitset-union-exec x y))))

Theorem: sbitset-of-sbitset-union

(defthm sbitset-of-sbitset-union
  (sbitsetp (sbitset-union x y)))

Theorem: sbitset-members-of-sbitset-union

(defthm sbitset-members-of-sbitset-union
  (equal (sbitset-members (sbitset-union x y))
         (union (sbitset-members x)
                (sbitset-members y))))