		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-concatenate

Signature
(sparseint$-concatenate width lsbs msbs) → concat
Arguments: width — Guard (natp width).; lsbs — Guard (sparseint$-p lsbs).; msbs — Guard (sparseint$-p msbs).
Returns: concat — Type (sparseint$-p concat).

Definitions and Theorems

Function: sparseint$-concatenate

(defun sparseint$-concatenate (width lsbs msbs)
  (declare (xargs :guard (and (natp width)
                              (sparseint$-p lsbs)
                              (sparseint$-p msbs))))
  (declare (xargs :guard (and (sparseint$-height-correctp lsbs)
                              (sparseint$-height-correctp msbs))))
  (let ((__function__ 'sparseint$-concatenate))
    (declare (ignorable __function__))
    (b* (((when (eql (lnfix width) 0))
          (sparseint$-fix msbs))
         ((mv ans ?height)
          (sparseint$-concatenate-rebalance
               width lsbs (sparseint$-height lsbs)
               msbs (sparseint$-height msbs))))
      ans)))

Theorem: sparseint$-p-of-sparseint$-concatenate

(defthm sparseint$-p-of-sparseint$-concatenate
  (b* ((concat (sparseint$-concatenate width lsbs msbs)))
    (sparseint$-p concat))
  :rule-classes :rewrite)

Theorem: sparseint$-height-correct-of-sparseint$-concatenate

(defthm sparseint$-height-correct-of-sparseint$-concatenate
  (b* ((?concat (sparseint$-concatenate width lsbs msbs)))
    (implies (and (sparseint$-height-correctp lsbs)
                  (sparseint$-height-correctp msbs))
             (sparseint$-height-correctp concat))))

Theorem: sparseint$-concatenate-correct

(defthm sparseint$-concatenate-correct
  (b* ((?concat (sparseint$-concatenate width lsbs msbs)))
    (equal (sparseint$-val concat)
           (logapp width (sparseint$-val lsbs)
                   (sparseint$-val msbs)))))

Theorem: height-of-sparseint$-concatenate

(defthm height-of-sparseint$-concatenate
  (b* ((?concat (sparseint$-concatenate width lsbs msbs)))
    (implies (and (sparseint$-height-correctp lsbs)
                  (sparseint$-height-correctp msbs))
             (<= (sparseint$-height concat)
                 (+ 1
                    (max (sparseint$-height lsbs)
                         (sparseint$-height msbs))))))
  :rule-classes :linear)

Theorem: sparseint$-concatenate-of-nfix-width

(defthm sparseint$-concatenate-of-nfix-width
  (equal (sparseint$-concatenate (nfix width)
                                 lsbs msbs)
         (sparseint$-concatenate width lsbs msbs)))

Theorem: sparseint$-concatenate-nat-equiv-congruence-on-width

(defthm sparseint$-concatenate-nat-equiv-congruence-on-width
  (implies (nat-equiv width width-equiv)
           (equal (sparseint$-concatenate width lsbs msbs)
                  (sparseint$-concatenate width-equiv lsbs msbs)))
  :rule-classes :congruence)

Theorem: sparseint$-concatenate-of-sparseint$-fix-lsbs

(defthm sparseint$-concatenate-of-sparseint$-fix-lsbs
  (equal (sparseint$-concatenate width (sparseint$-fix lsbs)
                                 msbs)
         (sparseint$-concatenate width lsbs msbs)))

Theorem: sparseint$-concatenate-sparseint$-equiv-congruence-on-lsbs

(defthm sparseint$-concatenate-sparseint$-equiv-congruence-on-lsbs
  (implies (sparseint$-equiv lsbs lsbs-equiv)
           (equal (sparseint$-concatenate width lsbs msbs)
                  (sparseint$-concatenate width lsbs-equiv msbs)))
  :rule-classes :congruence)

Theorem: sparseint$-concatenate-of-sparseint$-fix-msbs

(defthm sparseint$-concatenate-of-sparseint$-fix-msbs
  (equal (sparseint$-concatenate width lsbs (sparseint$-fix msbs))
         (sparseint$-concatenate width lsbs msbs)))

Theorem: sparseint$-concatenate-sparseint$-equiv-congruence-on-msbs

(defthm sparseint$-concatenate-sparseint$-equiv-congruence-on-msbs
  (implies (sparseint$-equiv msbs msbs-equiv)
           (equal (sparseint$-concatenate width lsbs msbs)
                  (sparseint$-concatenate width lsbs msbs-equiv)))
  :rule-classes :congruence)