		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Binary-bitop

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

Definitions and Theorems

Function: binary-bitop

(defun binary-bitop (op x y)
  (declare (type (unsigned-byte 4) op))
  (declare (xargs :guard (and (integerp op)
                              (integerp x)
                              (integerp y))))
  (let ((__function__ 'binary-bitop))
    (declare (ignorable __function__))
    (b* ((op (mbe :logic (loghead 4 op) :exec op)))
      (case op
        (0 0)
        (1 (lognor x y))
        (2 (logandc2 x y))
        (3 (lognot y))
        (4 (logandc1 x y))
        (5 (lognot x))
        (6 (logxor x y))
        (7 (lognand x y))
        (8 (logand x y))
        (9 (logeqv x y))
        (10 (lifix x))
        (11 (logorc2 x y))
        (12 (lifix y))
        (13 (logorc1 x y))
        (14 (logior x y))
        (t -1)))))

Theorem: integerp-of-binary-bitop

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

Theorem: binary-bitop-correct

(defthm binary-bitop-correct
  (b* ((?binary (binary-bitop op x y)))
    (equal (logbitp n binary)
           (logbitp (+ (logbit n x) (* 2 (logbit n y)))
                    op))))

Theorem: logext-of-binary-bitop

(defthm logext-of-binary-bitop
  (b* ((?binary (binary-bitop op x y)))
    (equal (logext n binary)
           (binary-bitop op (logext n x)
                         (logext n y)))))

Theorem: logtail-of-binary-bitop

(defthm logtail-of-binary-bitop
  (b* ((?binary (binary-bitop op x y)))
    (equal (logtail n binary)
           (binary-bitop op (logtail n x)
                         (logtail n y)))))

Theorem: open-binary-bitop

(defthm open-binary-bitop
  (b* ((?binary (binary-bitop op x y)))
    (implies (syntaxp (quotep op))
             (equal binary
                    (b* ((op (mbe :logic (loghead 4 op) :exec op)))
                      (case op
                        (0 0)
                        (1 (lognor x y))
                        (2 (logandc2 x y))
                        (3 (lognot y))
                        (4 (logandc1 x y))
                        (5 (lognot x))
                        (6 (logxor x y))
                        (7 (lognand x y))
                        (8 (logand x y))
                        (9 (logeqv x y))
                        (10 (lifix x))
                        (11 (logorc2 x y))
                        (12 (lifix y))
                        (13 (logorc1 x y))
                        (14 (logior x y))
                        (t -1)))))))

Theorem: binary-bitop-of-ifix-op

(defthm binary-bitop-of-ifix-op
  (equal (binary-bitop (ifix op) x y)
         (binary-bitop op x y)))

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

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

Theorem: binary-bitop-of-ifix-x

(defthm binary-bitop-of-ifix-x
  (equal (binary-bitop op (ifix x) y)
         (binary-bitop op x y)))

Theorem: binary-bitop-int-equiv-congruence-on-x

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

Theorem: binary-bitop-of-ifix-y

(defthm binary-bitop-of-ifix-y
  (equal (binary-bitop op x (ifix y))
         (binary-bitop op x y)))

Theorem: binary-bitop-int-equiv-congruence-on-y

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