		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-truncate

Signature
(sparseint$-truncate width x) → new-x
Arguments: width — Guard (posp width).; x — Guard (sparseint$-p x).
Returns: new-x — Type (sparseint$-p new-x).

Definitions and Theorems

Function: sparseint$-truncate

(defun sparseint$-truncate (width x)
  (declare (xargs :guard (and (posp width) (sparseint$-p x))))
  (let ((__function__ 'sparseint$-truncate))
    (declare (ignorable __function__))
    (sparseint$-case x :leaf (sparseint$-fix x)
                     :concat
                     (if (< x.width (lposfix width))
                         (sparseint$-fix x)
                       (sparseint$-truncate width x.lsbs)))))

Theorem: sparseint$-p-of-sparseint$-truncate

(defthm sparseint$-p-of-sparseint$-truncate
  (b* ((new-x (sparseint$-truncate width x)))
    (sparseint$-p new-x))
  :rule-classes :rewrite)

Theorem: loghead-of-sparseint$-truncate

(defthm loghead-of-sparseint$-truncate
  (b* ((?new-x (sparseint$-truncate width x)))
    (implies (equal width1 (pos-fix width))
             (equal (loghead width1 (sparseint$-val new-x))
                    (loghead width1 (sparseint$-val x))))))

Theorem: logapp-of-sparseint$-truncate

(defthm logapp-of-sparseint$-truncate
  (b* ((?new-x (sparseint$-truncate width x)))
    (implies (equal width1 (pos-fix width))
             (equal (logapp width1 (sparseint$-val new-x) y)
                    (logapp width1 (sparseint$-val x) y)))))

Theorem: sparseint$-height-correctp-of-sparseint$-truncate

(defthm sparseint$-height-correctp-of-sparseint$-truncate
  (b* ((?new-x (sparseint$-truncate width x)))
    (implies (sparseint$-height-correctp x)
             (sparseint$-height-correctp new-x))))

Theorem: height-of-sparseint$-truncate

(defthm height-of-sparseint$-truncate
  (b* ((?new-x (sparseint$-truncate width x)))
    (<= (sparseint$-height new-x)
        (sparseint$-height x)))
  :rule-classes :linear)

Theorem: sparseint$-truncate-of-pos-fix-width

(defthm sparseint$-truncate-of-pos-fix-width
  (equal (sparseint$-truncate (pos-fix width) x)
         (sparseint$-truncate width x)))

Theorem: sparseint$-truncate-pos-equiv-congruence-on-width

(defthm sparseint$-truncate-pos-equiv-congruence-on-width
  (implies (pos-equiv width width-equiv)
           (equal (sparseint$-truncate width x)
                  (sparseint$-truncate width-equiv x)))
  :rule-classes :congruence)

Theorem: sparseint$-truncate-of-sparseint$-fix-x

(defthm sparseint$-truncate-of-sparseint$-fix-x
  (equal (sparseint$-truncate width (sparseint$-fix x))
         (sparseint$-truncate width x)))

Theorem: sparseint$-truncate-sparseint$-equiv-congruence-on-x

(defthm sparseint$-truncate-sparseint$-equiv-congruence-on-x
  (implies (sparseint$-equiv x x-equiv)
           (equal (sparseint$-truncate width x)
                  (sparseint$-truncate width x-equiv)))
  :rule-classes :congruence)