Filtering...

fl-expt

books/rtl/rel9/arithmetic/fl-expt

Included Books

numerator denominator nniq arith2 ground-zero floor integerp rationalp unary-divide expt expo power2p fl
other
(in-package "ACL2")
local
(local (include-book "numerator"))
local
(local (include-book "denominator"))
local
(local (include-book "nniq"))
local
(local (include-book "arith2"))
local
(local (include-book "ground-zero"))
local
(local (include-book "floor"))
local
(local (include-book "integerp"))
local
(local (include-book "rationalp"))
local
(local (include-book "unary-divide"))
local
(local (include-book "expt"))
local
(local (include-book "expo"))
local
(local (include-book "power2p"))
local
(local (include-book "fl"))
local
(local (in-theory (enable expt-minus)))
flfunction
(defun fl
  (x)
  (declare (xargs :guard (real/rationalp x)))
  (floor x 1))
fl-simptheorem
(defthm fl-simp
  (implies (case-split (rationalp x))
    (equal (fl (* 1/2 (fl (* x (/ (expt 2 n))))))
      (fl (* 1/2 x (/ (expt 2 n))))))
  :hints (("Goal" :in-theory (disable fl-def-linear)
     :use ((:instance fl-unique
        (x (* 1/2 (fl (* x (/ (expt 2 n))))))
        (n (fl (* 1/2 x (/ (expt 2 n)))))) (:instance fl-def-linear (x (* 1/2 x (/ (expt 2 n)))))))))
fl-shift-flencapsulate
(encapsulate nil
  (local (defthm fl-shift-fl-case-1
      (implies (<= 0 m)
        (equal (fl (* (fl x) (/ (expt 2 m))))
          (fl (* x (/ (expt 2 m))))))
      :hints (("Goal" :cases ((rationalp x))))))
  (local (defthm fl-shift-fl-case-2
      (implies (and (< m 0) (case-split (integerp m)))
        (equal (fl (* (fl x) (/ (expt 2 m))))
          (* (fl x) (/ (expt 2 m)))))
      :hints (("Goal" :in-theory (disable fl-int)
         :use (:instance fl-int (x (* (/ (expt 2 m)) (fl x))))))))
  (defthm fl-shift-fl
    (implies (case-split (integerp m))
      (equal (fl (* (/ (expt 2 m)) (fl x)))
        (if (<= 0 m)
          (fl (* (/ (expt 2 m)) x))
          (* (/ (expt 2 m)) (fl x)))))
    :hints (("Goal" :cases ((< m 0))))))
fl-shift-fl-2-factorstheorem
(defthm fl-shift-fl-2-factors
  (implies (and (case-split (integerp m)) (case-split (integerp n)))
    (equal (fl (* (/ (expt 2 m)) (expt 2 n) (fl x)))
      (if (<= 0 (- m n))
        (fl (* (/ (expt 2 (- m n))) x))
        (* (/ (expt 2 (- m n))) (fl x)))))
  :hints (("Goal" :in-theory (set-difference-theories (enable expt-split) '(fl-shift-fl))
     :use (:instance fl-shift-fl (m (- m n))))))
fl-shift-fl-2-factors-2theorem
(defthm fl-shift-fl-2-factors-2
  (implies (and (case-split (integerp m)) (case-split (integerp n)))
    (equal (fl (* (expt 2 n) (/ (expt 2 m)) (fl x)))
      (if (<= 0 (- m n))
        (fl (* (/ (expt 2 (- m n))) x))
        (* (/ (expt 2 (- m n))) (fl x)))))
  :hints (("Goal" :in-theory (set-difference-theories (enable expt-split)
       '(fl-shift-fl expo-comparison-rewrite-to-bound))
     :use (:instance fl-shift-fl (m (- m n))))))
fl-shift-fl-by-1theorem
(defthm fl-shift-fl-by-1
  (equal (fl (* 1/2 (fl x))) (fl (* 1/2 x)))
  :hints (("Goal" :use (:instance fl-shift-fl (m 1)))))