		Search-engine friendly clone of the ACL2 documentation.

Limited-shifts

Limshift-loghead-of-ash

Computes (loghead width (ash x shift-amt)).

Signature
(limshift-loghead-of-ash width x shift-amt) → shifted
Arguments: width — Guard (natp width).; x — Guard (integerp x).; shift-amt — Guard (integerp shift-amt).
Returns: shifted — Type (integerp shifted).

Definitions and Theorems

Function: limshift-loghead-of-ash

(defun
    limshift-loghead-of-ash
    (width x shift-amt)
    (declare (xargs :guard (and (natp width)
                                (integerp x)
                                (integerp shift-amt))))
    (let ((__function__ 'limshift-loghead-of-ash))
         (declare (ignorable __function__))
         (b* ((shift-amt (lifix shift-amt))
              (x (lifix x))
              (width (lnfix width))
              ((when (< shift-amt 0))
               (loghead width (logtail (- shift-amt) x)))
              (shift-amt-limited (logcollapse (integer-length width)
                                              shift-amt)))
             (loghead width (ash x shift-amt-limited)))))

Theorem: integerp-of-limshift-loghead-of-ash

(defthm integerp-of-limshift-loghead-of-ash
        (b* ((shifted (limshift-loghead-of-ash width x shift-amt)))
            (integerp shifted))
        :rule-classes :type-prescription)

Theorem: limshift-loghead-of-ash-correct

(defthm limshift-loghead-of-ash-correct
        (equal (limshift-loghead-of-ash width x shift-amt)
               (loghead width (ash x shift-amt))))