		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Int-to-sparseint$

Signature
(int-to-sparseint$ x) → sint
Arguments: x — Guard (integerp x).
Returns: sint — Type (sparseint$-p sint).

Definitions and Theorems

Function: int-to-sparseint$$inline

(defun int-to-sparseint$$inline (x)
  (declare (xargs :guard (integerp x)))
  (let ((__function__ 'int-to-sparseint$))
    (declare (ignorable __function__))
    (mbe :logic
         (b* (((mv sint ?height ?width)
               (int-to-sparseint$-rec x (+ 1 (integer-length x))
                                      0)))
           sint)
         :exec
         (if (< (+ 1 (integer-length x))
                (sparseint$-leaf-bitlimit))
             x
           (b* (((mv sint ?height ?width)
                 (int-to-sparseint$-rec x (+ 1 (integer-length x))
                                        0)))
             sint)))))

Theorem: sparseint$-p-of-int-to-sparseint$

(defthm sparseint$-p-of-int-to-sparseint$
  (b* ((sint (int-to-sparseint$$inline x)))
    (sparseint$-p sint))
  :rule-classes :rewrite)

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

(defthm sparseint$-height-correctp-of-int-to-sparseint$
  (b* ((?sint (int-to-sparseint$$inline x)))
    (sparseint$-height-correctp sint)))

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

(defthm sparseint$-val-of-int-to-sparseint$
  (b* ((?sint (int-to-sparseint$$inline x)))
    (equal (sparseint$-val sint) (ifix x))))

Theorem: int-to-sparseint$$inline-of-ifix-x

(defthm int-to-sparseint$$inline-of-ifix-x
  (equal (int-to-sparseint$$inline (ifix x))
         (int-to-sparseint$$inline x)))

Theorem: int-to-sparseint$$inline-int-equiv-congruence-on-x

(defthm int-to-sparseint$$inline-int-equiv-congruence-on-x
  (implies (int-equiv x x-equiv)
           (equal (int-to-sparseint$$inline x)
                  (int-to-sparseint$$inline x-equiv)))
  :rule-classes :congruence)