		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Unary-bitop

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

Definitions and Theorems

Function: unary-bitop

(defun unary-bitop (op x)
  (declare (type (unsigned-byte 2) op))
  (declare (xargs :guard (and (integerp op) (integerp x))))
  (let ((__function__ 'unary-bitop))
    (declare (ignorable __function__))
    (b* ((op (mbe :logic (loghead 2 op) :exec op)))
      (case op
        (0 0)
        (1 (lognot x))
        (2 (lifix x))
        (t -1)))))

Theorem: integerp-of-unary-bitop

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

Theorem: unary-bitop-correct

(defthm unary-bitop-correct
  (b* ((?unary (unary-bitop op x)))
    (equal (logbitp n unary)
           (logbitp (logbit n x) op))))

Theorem: logext-of-unary-bitop

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

Theorem: logtail-of-unary-bitop

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

Theorem: open-unary-bitop

(defthm open-unary-bitop
  (b* ((?unary (unary-bitop op x)))
    (implies (syntaxp (quotep op))
             (equal unary
                    (b* ((op (mbe :logic (loghead 2 op) :exec op)))
                      (case op
                        (0 0)
                        (1 (lognot x))
                        (2 (lifix x))
                        (t -1)))))))

Theorem: unary-bitop-of-ifix-op

(defthm unary-bitop-of-ifix-op
  (equal (unary-bitop (ifix op) x)
         (unary-bitop op x)))

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

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

Theorem: unary-bitop-of-ifix-x

(defthm unary-bitop-of-ifix-x
  (equal (unary-bitop op (ifix x))
         (unary-bitop op x)))

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

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