		Search-engine friendly clone of the ACL2 documentation.

Sparseint

Sparseint-ash

Shift a sparseint by some amount, positive or negative

Signature
(sparseint-ash x shift) → ash
Arguments: x — Guard (sparseint-p x).; shift — Guard (integerp shift).
Returns: ash — Type (sparseint-p ash).

Definitions and Theorems

Function: sparseint-ash

(defun sparseint-ash (x shift)
  (declare (xargs :guard (and (sparseint-p x) (integerp shift))))
  (let ((__function__ 'sparseint-ash))
    (declare (ignorable __function__))
    (b* ((shift (lifix shift)))
      (cond ((eql shift 0) (sparseint-fix x))
            ((< shift 0)
             (sparseint-rightshift (- shift) x))
            (t (sparseint-concatenate shift 0 x))))))

Theorem: sparseint-p-of-sparseint-ash

(defthm sparseint-p-of-sparseint-ash
  (b* ((ash (sparseint-ash x shift)))
    (sparseint-p ash))
  :rule-classes :rewrite)

Theorem: sparseint-ash-correct

(defthm sparseint-ash-correct
  (b* ((common-lisp::?ash (sparseint-ash x shift)))
    (equal (sparseint-val ash)
           (ash (sparseint-val x) shift))))

Theorem: sparseint-ash-of-sparseint-fix-x

(defthm sparseint-ash-of-sparseint-fix-x
  (equal (sparseint-ash (sparseint-fix x) shift)
         (sparseint-ash x shift)))

Theorem: sparseint-ash-sparseint-equiv-congruence-on-x

(defthm sparseint-ash-sparseint-equiv-congruence-on-x
  (implies (sparseint-equiv x x-equiv)
           (equal (sparseint-ash x shift)
                  (sparseint-ash x-equiv shift)))
  :rule-classes :congruence)

Theorem: sparseint-ash-of-ifix-shift

(defthm sparseint-ash-of-ifix-shift
  (equal (sparseint-ash x (ifix shift))
         (sparseint-ash x shift)))

Theorem: sparseint-ash-int-equiv-congruence-on-shift

(defthm sparseint-ash-int-equiv-congruence-on-shift
  (implies (int-equiv shift shift-equiv)
           (equal (sparseint-ash x shift)
                  (sparseint-ash x shift-equiv)))
  :rule-classes :congruence)