Quotient Refinement
Theorem:
(defthm init-approx (implies (and (rationalp a) (rationalp b) (rationalp y) (rationalp ep) (not (zp p)) (> a 0) (> b 0) (<= (abs (- 1 (* b y))) ep)) (<= (abs (- 1 (* (/ b a) (rne (* a y) p)))) (+ ep (* (expt 2 (- p)) (1+ ep))))) :rule-classes nil)
Theorem:
(defthm r-exactp (implies (and (rationalp a) (rationalp b) (integerp p) (> p 1) (exactp a p) (exactp b p) (<= 1 a) (< a 2) (<= 1 b) (< b 2) (rationalp q) (exactp q p) (< (abs (- (/ a b) q)) (expt 2 (- (1+ (if (> a b) 0 -1)) p)))) (exactp (- a (* b q)) p)) :rule-classes nil)
Theorem:
(defthm markstein-lemma (let ((e (if (> a b) 0 -1)) (r (- a (* b q)))) (implies (and (rationalp a) (rationalp b) (rationalp q) (rationalp y) (integerp p) (<= 1 a) (< a 2) (<= 1 b) (< b 2) (> p 1) (exactp a p) (exactp b p) (exactp q p) (< (abs (- 1 (* b y))) (/ (expt 2 p))) (< (abs (- (/ a b) q)) (expt 2 (- (1+ e) p))) (ieee-rounding-mode-p mode)) (= (rnd (+ q (* r y)) mode p) (rnd (/ a b) mode p)))) :rule-classes nil)
Theorem:
(defthm quotient-refinement-1 (implies (and (rationalp a) (rationalp b) (rationalp y) (rationalp q0) (rationalp ep) (rationalp de) (not (zp p)) (<= 1 a) (< a 2) (<= 1 b) (< b 2) (<= (abs (- 1 (* b y))) ep) (<= (abs (- 1 (* (/ b a) q0))) de)) (let* ((r (rne (- a (* b q0)) p)) (q (rne (+ q0 (* r y)) p))) (<= (abs (- q (/ a b))) (* (/ a b) (+ (expt 2 (- p)) (* (1+ (expt 2 (- p))) de ep) (* (expt 2 (- p)) de (1+ ep)) (* (expt 2 (- (* 2 p))) de (1+ ep))))))) :rule-classes nil)
Theorem:
(defthm quotient-refinement-2 (implies (and (rationalp a) (rationalp b) (rationalp y) (rationalp q0) (rationalp ep) (rationalp de) (not (zp p)) (<= 1 a) (< a 2) (<= 1 b) (< b 2) (<= (abs (- 1 (* b y))) ep) (<= (abs (- 1 (* (/ b a) q0))) de) (< (+ (* ep de) (* (expt 2 (- p)) de (1+ ep))) (expt 2 (- (1+ p))))) (let* ((r (rne (- a (* b q0)) p)) (q (rne (+ q0 (* r y)) p)) (e (if (> a b) 0 -1))) (< (abs (- q (/ a b))) (expt 2 (- (1+ e) p))))) :rule-classes nil)