		Search-engine friendly clone of the ACL2 documentation.

Bitops/rotate

Rotate-left-1

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

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

Definitions and Theorems

Function: rotate-left-1

(defun rotate-left-1 (x width)
  (declare (xargs :guard (and (integerp x) (posp width))))
  (let ((__function__ 'rotate-left-1))
    (declare (ignorable __function__))
    (b* (((when (mbe :logic (zp width) :exec nil))
          0)
         (msb (logbit (- width 1) x))
         (chop (loghead (- width 1) x)))
      (logcons msb chop))))

Theorem: natp-of-rotate-left-1

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

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

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

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

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

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

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

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

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