• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
      • Rtl
        • Floating-Point Exceptions and Specification of Elementary Arithmetic Instructions
        • Implementation of Elementary Operations
        • Register-Transfer Logic
          • Bit Vectors
          • Logical Operations
          • Basic Arithmetic Functions
            • Modulus
            • Floor and Ceiling
            • Chop
        • Floating-Point Arithmetic
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• Basic Arithmetic Functions

Chop

Chop

Definitions and Theorems

Function: chop

(defun chop (x k)
  (declare (xargs :guard (and (real/rationalp x) (integerp k))))
  (/ (fl (* (expt 2 k) x)) (expt 2 k)))

Theorem: chop-mod

(defthm chop-mod
  (implies (and (rationalp x) (integerp k))
           (equal (chop x k)
                  (- x (mod x (expt 2 (- k)))))))

Theorem: chop-down

(defthm chop-down
  (implies (and (rationalp x) (integerp n))
           (<= (chop x n) x))
  :rule-classes nil)

Theorem: chop-monotone

(defthm chop-monotone
  (implies (and (rationalp x)
                (rationalp y)
                (integerp n)
                (<= x y))
           (<= (chop x n) (chop y n)))
  :rule-classes nil)

Theorem: chop-chop

(defthm chop-chop
  (implies (and (rationalp x)
                (integerp k)
                (integerp m)
                (<= k m))
           (and (equal (chop (chop x m) k) (chop x k))
                (equal (chop (chop x k) m) (chop x k))
                (<= (chop x k) (chop x m)))))

Theorem: chop-plus

(defthm chop-plus
  (implies (and (rationalp x)
                (rationalp y)
                (integerp k))
           (and (equal (chop (+ x (chop y k)) k)
                       (+ (chop x k) (chop y k)))
                (equal (chop (+ (chop x k) (chop y k)) k)
                       (+ (chop x k) (chop y k)))
                (equal (chop (- x (chop y k)) k)
                       (- (chop x k) (chop y k)))
                (equal (chop (- (chop x k) (chop y k)) k)
                       (- (chop x k) (chop y k))))))

Theorem: chop-shift

(defthm chop-shift
  (implies (and (rationalp x)
                (integerp k)
                (integerp m))
           (equal (chop (* (expt 2 k) x) m)
                  (* (expt 2 k) (chop x (+ k m))))))

Theorem: chop-bound

(defthm chop-bound
  (implies (and (rationalp x)
                (integerp n)
                (natp m))
           (iff (<= n x) (<= n (chop x m))))
  :rule-classes nil)

Theorem: chop-small

(defthm chop-small
  (implies (and (rationalp x)
                (integerp m)
                (< x (expt 2 (- m)))
                (<= (- (expt 2 (- m))) x))
           (equal (chop x m)
                  (if (>= x 0) 0 (- (expt 2 (- m)))))))

Theorem: chop-0

(defthm chop-0
  (implies (and (rationalp x)
                (integerp m)
                (< (abs (chop x m)) (expt 2 (- m))))
           (equal (chop x m) 0)))

Theorem: chop-int-bounds

(defthm chop-int-bounds
  (implies (and (natp k) (natp n) (rationalp x))
           (and (<= (chop (fl (/ x (expt 2 n))) (- k))
                    (/ (chop x (- k)) (expt 2 n)))
                (<= (/ (+ (chop x (- k)) (expt 2 k))
                       (expt 2 n))
                    (+ (chop (fl (/ x (expt 2 n))) (- k))
                       (expt 2 k)))))
  :rule-classes nil)

Theorem: chop-int-neg

(defthm chop-int-neg
  (implies (and (natp k)
                (natp n)
                (rationalp x)
                (rationalp y)
                (= (fl (/ x (expt 2 k)))
                   (fl (/ y (expt 2 k))))
                (not (integerp (/ x (expt 2 k)))))
           (equal (chop (1- (- (fl (/ y (expt 2 n)))))
                        (- k))
                  (chop (- (/ x (expt 2 n))) (- k)))))