		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-plus-int

Signature
(sparseint$-plus-int offset x x.height y cin) → (mv sum height)
Arguments: offset — Guard (natp offset).; x — Guard (sparseint$-p x).; x.height — Guard (natp x.height).; y — Guard (integerp y).; cin — Guard (bitp cin).
Returns: sum — Type (sparseint$-p sum).; height — Type (equal height (sparseint$-height sum)).

Definitions and Theorems

Function: sparseint$-plus-int

(defun sparseint$-plus-int (offset x x.height y cin)
 (declare (xargs :guard (and (natp offset)
                             (sparseint$-p x)
                             (natp x.height)
                             (integerp y)
                             (bitp cin))))
 (declare
      (xargs :guard (and (sparseint$-height-correctp x)
                         (equal x.height (sparseint$-height x)))))
 (let ((__function__ 'sparseint$-plus-int))
  (declare (ignorable __function__))
  (b* ((offset (lnfix offset))
       (y (lifix y))
       (cin (lbfix cin))
       (x.height (mbe :logic (sparseint$-height x)
                      :exec x.height)))
   (sparseint$-case
     x :leaf
     (b* ((xval (logtail offset x.val))
          (sum (sum-with-cin cin xval y)))
       (mv (sparseint$-leaf sum) 0))
     :concat
     (b*
      ((x.msbs.height
            (mbe :logic (sparseint$-height x.msbs)
                 :exec (- x.height (if x.lsbs-taller 2 1))))
       ((when (<= x.width offset))
        (sparseint$-plus-int (- offset x.width)
                             x.msbs x.msbs.height y cin))
       (width1 (- x.width offset))
       (x.lsbs.height
            (mbe :logic (sparseint$-height x.lsbs)
                 :exec (- x.height (if x.msbs-taller 2 1))))
       ((mv lsbs-sum lsbs-sum-height lsbs-cout)
        (sparseint$-plus-int-width
             width1 offset x.lsbs
             x.lsbs.height (bignum-logext width1 y)
             cin))
       ((mv msbs-sum msbs-sum-height)
        (sparseint$-plus-int 0
                             x.msbs x.msbs.height (logtail width1 y)
                             lsbs-cout))
       ((mv sum-concat sum-height)
        (sparseint$-concatenate-rebalance
             width1 lsbs-sum lsbs-sum-height
             msbs-sum msbs-sum-height)))
      (mv sum-concat sum-height))))))

Theorem: sparseint$-p-of-sparseint$-plus-int.sum

(defthm sparseint$-p-of-sparseint$-plus-int.sum
  (b* (((mv ?sum ?height)
        (sparseint$-plus-int offset x x.height y cin)))
    (sparseint$-p sum))
  :rule-classes :rewrite)

Theorem: return-type-of-sparseint$-plus-int.height

(defthm return-type-of-sparseint$-plus-int.height
  (b* (((mv ?sum ?height)
        (sparseint$-plus-int offset x x.height y cin)))
    (equal height (sparseint$-height sum)))
  :rule-classes :rewrite)

Theorem: sparseint$-height-correctp-of-sparseint$-plus-int

(defthm sparseint$-height-correctp-of-sparseint$-plus-int
  (b* (((mv ?sum ?height)
        (sparseint$-plus-int offset x x.height y cin)))
    (implies (sparseint$-height-correctp x)
             (sparseint$-height-correctp sum))))

Theorem: sparseint$-val-of-sparseint$-plus-int

(defthm sparseint$-val-of-sparseint$-plus-int
  (b* (((mv ?sum ?height)
        (sparseint$-plus-int offset x x.height y cin)))
    (equal (sparseint$-val sum)
           (sum-with-cin cin (logtail offset (sparseint$-val x))
                         y))))

Theorem: sparseint$-plus-int-of-nfix-offset

(defthm sparseint$-plus-int-of-nfix-offset
  (equal (sparseint$-plus-int (nfix offset)
                              x x.height y cin)
         (sparseint$-plus-int offset x x.height y cin)))

Theorem: sparseint$-plus-int-nat-equiv-congruence-on-offset

(defthm sparseint$-plus-int-nat-equiv-congruence-on-offset
  (implies
       (nat-equiv offset offset-equiv)
       (equal (sparseint$-plus-int offset x x.height y cin)
              (sparseint$-plus-int offset-equiv x x.height y cin)))
  :rule-classes :congruence)

Theorem: sparseint$-plus-int-of-sparseint$-fix-x

(defthm sparseint$-plus-int-of-sparseint$-fix-x
  (equal (sparseint$-plus-int offset (sparseint$-fix x)
                              x.height y cin)
         (sparseint$-plus-int offset x x.height y cin)))

Theorem: sparseint$-plus-int-sparseint$-equiv-congruence-on-x

(defthm sparseint$-plus-int-sparseint$-equiv-congruence-on-x
  (implies
       (sparseint$-equiv x x-equiv)
       (equal (sparseint$-plus-int offset x x.height y cin)
              (sparseint$-plus-int offset x-equiv x.height y cin)))
  :rule-classes :congruence)

Theorem: sparseint$-plus-int-of-nfix-x.height

(defthm sparseint$-plus-int-of-nfix-x.height
  (equal (sparseint$-plus-int offset x (nfix x.height)
                              y cin)
         (sparseint$-plus-int offset x x.height y cin)))

Theorem: sparseint$-plus-int-nat-equiv-congruence-on-x.height

(defthm sparseint$-plus-int-nat-equiv-congruence-on-x.height
  (implies
       (nat-equiv x.height x.height-equiv)
       (equal (sparseint$-plus-int offset x x.height y cin)
              (sparseint$-plus-int offset x x.height-equiv y cin)))
  :rule-classes :congruence)

Theorem: sparseint$-plus-int-of-ifix-y

(defthm sparseint$-plus-int-of-ifix-y
  (equal (sparseint$-plus-int offset x x.height (ifix y)
                              cin)
         (sparseint$-plus-int offset x x.height y cin)))

Theorem: sparseint$-plus-int-int-equiv-congruence-on-y

(defthm sparseint$-plus-int-int-equiv-congruence-on-y
  (implies
       (int-equiv y y-equiv)
       (equal (sparseint$-plus-int offset x x.height y cin)
              (sparseint$-plus-int offset x x.height y-equiv cin)))
  :rule-classes :congruence)

Theorem: sparseint$-plus-int-of-bfix-cin

(defthm sparseint$-plus-int-of-bfix-cin
  (equal (sparseint$-plus-int offset x x.height y (bfix cin))
         (sparseint$-plus-int offset x x.height y cin)))

Theorem: sparseint$-plus-int-bit-equiv-congruence-on-cin

(defthm sparseint$-plus-int-bit-equiv-congruence-on-cin
  (implies
       (bit-equiv cin cin-equiv)
       (equal (sparseint$-plus-int offset x x.height y cin)
              (sparseint$-plus-int offset x x.height y cin-equiv)))
  :rule-classes :congruence)