Rounding Away from Zero
Function:
(defun raz (x n) (declare (xargs :guard (and (real/rationalp x) (integerp n)))) (* (sgn x) (cg (* (expt 2 (1- n)) (sig x))) (expt 2 (- (1+ (expo x)) n))))
Theorem:
(defthm raz-rewrite (implies (and (rationalp x) (integerp n) (> n 0)) (equal (raz x n) (* (sgn x) (cg (* (expt 2 (- (1- n) (expo x))) (abs x))) (expt 2 (- (1+ (expo x)) n))))))
Theorem:
(defthm abs-raz (implies (and (rationalp x) (integerp n)) (equal (abs (raz x n)) (* (cg (* (expt 2 (1- n)) (sig x))) (expt 2 (- (1+ (expo x)) n))))))
Theorem:
(defthm raz-integer-type-prescription (implies (and (>= (expo x) n) (case-split (integerp n))) (integerp (raz x n))) :rule-classes :type-prescription)
Theorem:
(defthm sgn-raz (equal (sgn (raz x n)) (sgn x)))
Theorem:
(defthm raz-positive (implies (and (< 0 x) (case-split (rationalp x))) (< 0 (raz x n))) :rule-classes (:rewrite :linear))
Theorem:
(defthm raz-negative (implies (and (< x 0) (case-split (rationalp x))) (< (raz x n) 0)) :rule-classes (:rewrite :linear))
Theorem:
(defthm raz-0 (equal (raz 0 n) 0))
Theorem:
(defthm raz-minus (equal (raz (- x) n) (- (raz x n))))
Theorem:
(defthm raz-shift (implies (integerp n) (= (raz (* x (expt 2 k)) n) (* (raz x n) (expt 2 k)))) :rule-classes nil)
Theorem:
(defthm raz-neg-bits (implies (and (<= n 0) (rationalp x) (integerp n)) (equal (raz x n) (* (sgn x) (expt 2 (+ 1 (expo x) (- n)))))))
Theorem:
(defthm raz-lower-bound (implies (and (case-split (rationalp x)) (case-split (integerp n))) (>= (abs (raz x n)) (abs x))) :rule-classes :linear)
Theorem:
(defthm raz-lower-pos (implies (and (>= x 0) (case-split (rationalp x)) (case-split (integerp n))) (>= (raz x n) x)) :rule-classes :linear)
Theorem:
(defthm raz-upper-bound (implies (and (rationalp x) (integerp n) (> n 0)) (< (abs (raz x n)) (+ (abs x) (expt 2 (- (1+ (expo x)) n))))) :rule-classes :linear)
Theorem:
(defthm raz-diff (implies (and (rationalp x) (integerp n) (> n 0)) (< (abs (- (raz x n) x)) (expt 2 (- (1+ (expo x)) n)))) :rule-classes :linear)
Theorem:
(defthm raz-expo-upper (implies (and (rationalp x) (not (= x 0)) (natp n)) (<= (abs (raz x n)) (expt 2 (1+ (expo x))))) :rule-classes nil)
Theorem:
(defthm expo-raz-upper-bound (implies (and (rationalp x) (natp n)) (<= (expo (raz x n)) (1+ (expo x)))) :rule-classes :linear)
Theorem:
(defthm expo-raz-lower-bound (implies (and (rationalp x) (natp n)) (>= (expo (raz x n)) (expo x))) :rule-classes :linear)
Theorem:
(defthm expo-raz (implies (and (rationalp x) (natp n) (not (= (abs (raz x n)) (expt 2 (1+ (expo x)))))) (equal (expo (raz x n)) (expo x))))
Theorem:
(defthm raz-exactp-a (implies (case-split (< 0 n)) (exactp (raz x n) n)))
Theorem:
(defthm raz-exactp-b (implies (and (rationalp x) (integerp n) (> n 0)) (iff (exactp x n) (= x (raz x n)))))
Theorem:
(defthm raz-exactp-c (implies (and (exactp a n) (>= a x) (rationalp x) (integerp n) (> n 0) (rationalp a)) (>= a (raz x n))) :rule-classes nil)
Theorem:
(defthm raz-squeeze (implies (and (rationalp x) (rationalp a) (> x a) (> a 0) (not (zp n)) (exactp a n) (<= x (fp+ a n))) (equal (raz x n) (fp+ a n))))
Theorem:
(defthm raz-up (implies (and (rationalp x) (integerp k) (not (zp n)) (not (zp m)) (< m n) (< (abs x) (expt 2 k)) (= (abs (raz x n)) (expt 2 k))) (equal (abs (raz x m)) (expt 2 k))))
Theorem:
(defthm raz-monotone (implies (and (rationalp x) (rationalp y) (integerp n) (<= x y)) (<= (raz x n) (raz y n))) :rule-classes :linear)
Theorem:
(defthm rtz-raz (implies (and (rationalp x) (> x 0) (integerp n) (> n 0) (not (exactp x n))) (equal (raz x n) (+ (rtz x n) (expt 2 (+ (expo x) 1 (- n)))))))
Theorem:
(defthm raz-midpoint (implies (and (natp n) (rationalp x) (> x 0) (exactp x (1+ n)) (not (exactp x n))) (equal (raz x n) (+ x (expt 2 (- (expo x) n))))))
Theorem:
(defthm raz-raz (implies (and (rationalp x) (>= x 0) (integerp n) (integerp m) (> m 0) (>= n m)) (equal (raz (raz x n) m) (raz x m))))
Theorem:
(defthm plus-raz (implies (and (exactp x (+ k (- (expo x) (expo y)))) (rationalp x) (>= x 0) (rationalp y) (>= y 0) (integerp k)) (= (+ x (raz y k)) (raz (+ x y) (+ k (- (expo (+ x y)) (expo y)))))) :rule-classes nil)
Theorem:
(defthm minus-rtz-raz (implies (and (rationalp x) (> x 0) (rationalp y) (> y 0) (< y x) (integerp k) (> k 0) (> (+ k (- (expo (- x y)) (expo y))) 0) (exactp x (+ k (- (expo x) (expo y))))) (= (- x (rtz y k)) (raz (- x y) (+ k (- (expo (- x y)) (expo y)))))) :rule-classes nil)
Theorem:
(defthm rtz-plus-minus (implies (and (rationalp x) (rationalp y) (not (= x 0)) (not (= y 0)) (not (= (+ x y) 0)) (integerp k) (> k 0) (= k1 (+ k (- (expo x) (expo y)))) (= k2 (+ k (expo (+ x y)) (- (expo y)))) (exactp x k1) (> k2 0)) (= (+ x (rtz y k)) (if (= (sgn (+ x y)) (sgn y)) (rtz (+ x y) k2) (raz (+ x y) k2)))) :rule-classes nil)
Theorem:
(defthm raz-impl (implies (and (rationalp x) (> x 0) (integerp n) (> n 0) (integerp m) (>= m n) (exactp x m)) (equal (raz x n) (rtz (+ x (expt 2 (- (1+ (expo x)) n)) (- (expt 2 (- (1+ (expo x)) m)))) n))))