		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Binary-bitop-swap

Signature
(binary-bitop-swap op) → swap
Arguments: op — Guard (integerp op).
Returns: swap — Type (integerp swap).

Definitions and Theorems

Function: binary-bitop-swap

(defun binary-bitop-swap (op)
  (declare (type (unsigned-byte 4) op))
  (declare (xargs :guard (integerp op)))
  (let ((__function__ 'binary-bitop-swap))
    (declare (ignorable __function__))
    (b* ((op (mbe :logic (loghead 4 op) :exec op))
         (same 9)
         (x&~y 2)
         (y&~x 4))
      (logior (logand same op)
              (ash (logand x&~y op) 1)
              (ash (logand y&~x op) -1)))))

Theorem: integerp-of-binary-bitop-swap

(defthm integerp-of-binary-bitop-swap
  (b* ((swap (binary-bitop-swap op)))
    (integerp swap))
  :rule-classes :type-prescription)

Theorem: unsigned-byte-p-of-binary-bitop-swap

(defthm unsigned-byte-p-of-binary-bitop-swap
  (b* ((?swap (binary-bitop-swap op)))
    (unsigned-byte-p 4 swap)))

Theorem: binary-bitop-swap-correct

(defthm binary-bitop-swap-correct
  (equal (binary-bitop (binary-bitop-swap op)
                       x y)
         (binary-bitop op y x)))

Theorem: binary-bitop-swap-of-ifix-op

(defthm binary-bitop-swap-of-ifix-op
  (equal (binary-bitop-swap (ifix op))
         (binary-bitop-swap op)))

Theorem: binary-bitop-swap-int-equiv-congruence-on-op

(defthm binary-bitop-swap-int-equiv-congruence-on-op
  (implies (int-equiv op op-equiv)
           (equal (binary-bitop-swap op)
                  (binary-bitop-swap op-equiv)))
  :rule-classes :congruence)