Included Books
other
(in-package "ACL2")
include-book
(include-book "power2p")
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 "fl-expt"))
local
(local (include-book "mod"))
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-shift-pull-inside-modtheorem
(defthmd fl-shift-pull-inside-mod (implies (and (<= j i) (case-split (integerp i)) (case-split (integerp j))) (equal (fl (* (/ (expt 2 j)) (mod x (expt 2 i)))) (mod (fl (* x (/ (expt 2 j)))) (expt 2 (- i j))))) :hints (("Goal" :in-theory (enable mod expt-split))))
mod-integerp-when-y-is-power-of-2theorem
(defthm mod-integerp-when-y-is-power-of-2 (implies (integerp x) (integerp (mod x (expt 2 i)))) :rule-classes (:rewrite :type-prescription) :hints (("Goal" :cases ((< i 0)))))
mod-integerp-when-y-is-power-of-2-gentheorem
(defthm mod-integerp-when-y-is-power-of-2-gen (implies (and (integerp x) (syntaxp (power2-syntaxp y)) (force (power2p y))) (integerp (mod x y))) :rule-classes (:rewrite :type-prescription) :hints (("Goal" :in-theory (enable power2p-rewrite))))
mod-pull-inside-fl-shiftencapsulate
(encapsulate nil (local (defthm mod-pull-inside-fl-shift-usual-case (implies (and (<= 0 i) (case-split (integerp i)) (case-split (integerp j))) (equal (mod (fl (* x (/ (expt 2 j)))) (expt 2 i)) (fl (* (/ (expt 2 j)) (mod x (expt 2 (+ i j))))))) :otf-flg t :hints (("Goal" :use ((:instance fl-def-linear-part-1 (x (* x (/ (expt 2 i)) (/ (expt 2 j))))) (:instance fl-def-linear-part-2 (x (* x (/ (expt 2 i)) (/ (expt 2 j)))))) :in-theory (set-difference-theories (enable mod expt-split) '(fl-weak-monotone fl-def-linear-part-1 fl-def-linear-part-2)))))) (local (defthm mod-pull-inside-fl-shift-other-case (implies (and (< i 0) (case-split (integerp i)) (case-split (integerp j))) (equal (mod (fl (* x (/ (expt 2 j)))) (expt 2 i)) (fl (* (/ (expt 2 j)) (mod x (expt 2 (+ i j))))))) :otf-flg t :hints (("Goal" :use ((:instance <-transitive (a x) (b (+ (* (expt 2 i) (expt 2 j)) (* (expt 2 i) (expt 2 j) (fl (* x (/ (expt 2 i)) (/ (expt 2 j))))))) (c (+ (expt 2 j) (* (expt 2 i) (expt 2 j) (fl (* x (/ (expt 2 i)) (/ (expt 2 j)))))))) (:instance fl-def-linear-part-1 (x (* x (/ (expt 2 i)) (/ (expt 2 j))))) (:instance fl-def-linear-part-2 (x (* x (/ (expt 2 i)) (/ (expt 2 j)))))) :in-theory (set-difference-theories (enable mod expt-split) '(fl-weak-monotone fl-def-linear-part-1 fl-def-linear-part-2)))))) (defthm mod-pull-inside-fl-shift (implies (and (case-split (integerp i)) (case-split (integerp j))) (equal (mod (fl (* x (/ (expt 2 j)))) (expt 2 i)) (fl (* (/ (expt 2 j)) (mod x (expt 2 (+ i j))))))) :otf-flg t :hints (("goal" :cases ((<= 0 i))))))
mod-pull-inside-fl-shift-alttheorem
(defthm mod-pull-inside-fl-shift-alt (implies (and (integerp i) (integerp j)) (equal (mod (fl (* (/ (expt 2 j)) x)) (expt 2 i)) (fl (* (/ (expt 2 j)) (mod x (expt 2 (+ i j))))))))
mod-pull-inside-fl-shift-alt-alttheorem
(defthm mod-pull-inside-fl-shift-alt-alt (implies (and (integerp i) (integerp j)) (equal (mod (fl (* (/ (expt 2 j)) x)) (* 2 (expt 2 i))) (fl (* (/ (expt 2 j)) (mod x (expt 2 (+ i 1 j))))))) :hints (("Goal" :in-theory (set-difference-theories (enable expt-split) '(mod-pull-inside-fl-shift mod-pull-inside-fl-shift-alt)) :use (:instance mod-pull-inside-fl-shift (i (+ i 1))))))
mod-pull-inside-fl-shift-alt-alt-alttheorem
(defthm mod-pull-inside-fl-shift-alt-alt-alt (implies (and (integerp j)) (equal (mod (fl (* (/ (expt 2 j)) x)) 2) (fl (* (/ (expt 2 j)) (mod x (expt 2 (+ 1 j))))))) :hints (("Goal" :in-theory (set-difference-theories (enable expt-split) '(mod-pull-inside-fl-shift mod-pull-inside-fl-shift-alt mod-pull-inside-fl-shift-alt-alt)) :use (:instance mod-pull-inside-fl-shift-alt-alt (i 0)))))
mod-pull-inside-fl-shift-alt-alt-alt-alttheorem
(defthm mod-pull-inside-fl-shift-alt-alt-alt-alt (implies (and (integerp j)) (equal (mod (fl (* x (/ (expt 2 j)))) 2) (fl (* (/ (expt 2 j)) (mod x (expt 2 (+ 1 j))))))) :hints (("Goal" :in-theory (set-difference-theories (enable expt-split) '(mod-pull-inside-fl-shift mod-pull-inside-fl-shift-alt mod-pull-inside-fl-shift-alt-alt mod-pull-inside-fl-shift-alt-alt-alt)) :use (:instance mod-pull-inside-fl-shift-alt-alt (i 0)))))
fl-mod-zerotheorem
(defthm fl-mod-zero (implies (and (<= i2 i1) (integerp i1) (integerp i2)) (equal (fl (* (/ (expt 2 i1)) (mod x (expt 2 i2)))) 0)))
mod-pull-inside-fl-shift-alt-5theorem
(defthm mod-pull-inside-fl-shift-alt-5 (implies (and (integerp i) (integerp j)) (equal (mod (fl (* (/ (expt 2 j)) x)) (* 2 (expt 2 i))) (fl (* (/ (expt 2 j)) (mod x (expt 2 (+ 1 i j))))))) :hints (("Goal" :in-theory (set-difference-theories (enable expt-split) '(mod-pull-inside-fl-shift mod-pull-inside-fl-shift-alt mod-pull-inside-fl-shift-alt-alt mod-pull-inside-fl-shift-alt-alt-alt)) :use (:instance mod-pull-inside-fl-shift-alt (i (+ i 1))))))
mod-pull-inside-fl-shift-alt-6theorem
(defthm mod-pull-inside-fl-shift-alt-6 (implies (and (integerp i) (integerp j) (integerp k)) (equal (mod (fl (* x (/ (expt 2 j)))) (* 2 (expt 2 i) (/ (expt 2 k)))) (fl (* (/ (expt 2 j)) (mod x (expt 2 (+ 1 (- k) i j))))))) :hints (("Goal" :in-theory (set-difference-theories (enable expt-split) '(mod-pull-inside-fl-shift mod-pull-inside-fl-shift-alt mod-pull-inside-fl-shift-alt-alt mod-pull-inside-fl-shift-alt-alt-alt)) :use (:instance mod-pull-inside-fl-shift-alt (i (+ i (- k) 1))))))
mod-mod-erictheorem
(defthmd mod-mod-eric (implies (and (<= i1 i2) (case-split (integerp i1)) (case-split (integerp i2))) (= (mod (mod x (expt 2 i2)) (expt 2 i1)) (mod x (expt 2 i1)))))
mod-of-mod-cortheorem
(defthmd mod-of-mod-cor (implies (and (<= b a) (case-split (integerp b)) (case-split (integerp a))) (equal (mod (mod x (expt 2 a)) (expt 2 b)) (mod x (expt 2 b)))) :hints (("Goal" :in-theory (enable mod-mod-eric))))