		Search-engine friendly clone of the ACL2 documentation.

Bitops/rotate

Rotate-right-1

Rotate a bit-vector by a single place to the right.

Signature
(rotate-right-1 x width) → rotated
Arguments: x — The bit vector to be rotated right.
Guard (integerp x).; width — The width of x.
Guard (posp width).
Returns: rotated — Type (natp rotated).

Definitions and Theorems

Function: rotate-right-1

(defun rotate-right-1 (x width)
       (declare (xargs :guard (and (integerp x) (posp width))))
       (let ((__function__ 'rotate-right-1))
            (declare (ignorable __function__))
            (cond ((zp width) 0)
                  ((equal width 1) (loghead 1 x))
                  (t (let ((x (loghead width x)))
                          (logior (ash (logbit 0 x) (1- width))
                                  (ash x -1)))))))

Theorem: natp-of-rotate-right-1

(defthm acl2::natp-of-rotate-right-1
        (b* ((rotated (rotate-right-1 x width)))
            (natp rotated))
        :rule-classes :type-prescription)

Theorem: int-equiv-implies-equal-rotate-right-1-1

(defthm int-equiv-implies-equal-rotate-right-1-1
        (implies (int-equiv x x-equiv)
                 (equal (rotate-right-1 x width)
                        (rotate-right-1 x-equiv width)))
        :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-rotate-right-1-2

(defthm nat-equiv-implies-equal-rotate-right-1-2
        (implies (nat-equiv width width-equiv)
                 (equal (rotate-right-1 x width)
                        (rotate-right-1 x width-equiv)))
        :rule-classes (:congruence))

Theorem: logbitp-of-rotate-right-1-split

(defthm logbitp-of-rotate-right-1-split
        (equal (logbitp n (rotate-right-1 x width))
               (b* ((n (nfix n)) (width (nfix width)))
                   (cond ((>= n width) nil)
                         ((equal n (- width 1)) (logbitp 0 x))
                         (t (logbitp (+ 1 n) x))))))

Theorem: unsigned-byte-p-of-rotate-right-1

(defthm unsigned-byte-p-of-rotate-right-1
        (implies (natp width)
                 (unsigned-byte-p width (rotate-right-1 x width))))