		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))))