Filtering...

expo

books/rtl/rel9/arithmetic/expo

Included Books

ground-zero negative-syntaxp power2p expo-proofs common-factor-defuns
other
(in-package "ACL2")
include-book
(include-book "ground-zero")
include-book
(include-book "negative-syntaxp")
include-book
(include-book "power2p")
local
(local (include-book "expo-proofs"))
flfunction
(defund fl
  (x)
  (declare (xargs :guard (real/rationalp x)))
  (floor x 1))
expo-measurefunction
(defun expo-measure
  (x)
  (cond ((not (rationalp x)) 0)
    ((< x 0) '(2 . 0))
    ((< x 1) (cons 1 (fl (/ x))))
    (t (fl x))))
expofunction
(defund expo
  (x)
  (declare (xargs :guard t :measure (expo-measure x)))
  (cond ((or (not (rationalp x)) (equal x 0)) 0)
    ((< x 0) (expo (- x)))
    ((< x 1) (1- (expo (* 2 x))))
    ((< x 2) 0)
    (t (1+ (expo (/ x 2))))))
expo-integer-typetheorem
(defthm expo-integer-type
  (integerp (expo x))
  :rule-classes :type-prescription)
in-theory
(in-theory (disable (:type-prescription expo)))
expo-of-not-rationalptheorem
(defthm expo-of-not-rationalp
  (implies (not (rationalp x)) (equal (expo x) 0)))
expo-minustheorem
(defthmd expo-minus (equal (expo (* -1 x)) (expo x)))
expo-minus-erictheorem
(defthm expo-minus-eric
  (implies (syntaxp (negative-syntaxp x))
    (equal (expo x) (expo (* -1 x)))))
other
(theory-invariant (not (and (or (active-runep '(:rewrite expo-minus))
        (active-runep '(:rewrite expo-minus-eric)))
      (active-runep '(:definition expo))))
  :key expo-minus-invariant)
expo-lower-boundtheorem
(defthm expo-lower-bound
  (implies (and (rationalp x) (not (equal x 0)))
    (<= (expt 2 (expo x)) (abs x)))
  :rule-classes :linear)
expo-lower-postheorem
(defthm expo-lower-pos
  (implies (and (< 0 x) (rationalp x))
    (<= (expt 2 (expo x)) x))
  :rule-classes :linear)
expo-upper-boundtheorem
(defthm expo-upper-bound
  (implies (rationalp x) (< (abs x) (expt 2 (1+ (expo x)))))
  :rule-classes :linear)
expo-upper-postheorem
(defthm expo-upper-pos
  (implies (rationalp x) (< x (expt 2 (1+ (expo x)))))
  :rule-classes :linear)
expo-uniquetheorem
(defthm expo-unique
  (implies (and (<= (expt 2 n) (abs x))
      (< (abs x) (expt 2 (1+ n)))
      (rationalp x)
      (integerp n))
    (equal n (expo x)))
  :rule-classes nil)
expo-monotonetheorem
(defthmd expo-monotone
  (implies (and (<= (abs x) (abs y))
      (case-split (rationalp x))
      (case-split (not (equal x 0)))
      (case-split (rationalp y)))
    (<= (expo x) (expo y)))
  :rule-classes :linear)
expo-2**ntheorem
(defthmd expo-2**n
  (implies (integerp n) (equal (expo (expt 2 n)) n)))
expo-expt2theorem
(defthm expo-expt2
  (equal (expo (expt 2 i))
    (if (integerp i)
      i
      0)))
expo-halftheorem
(defthm expo-half
  (implies (and (case-split (rationalp x))
      (case-split (not (equal x 0))))
    (equal (expo (* 1/2 x)) (+ -1 (expo x)))))
other
(theory-invariant (incompatible (:rewrite expo-half) (:definition expo))
  :key expo-half-loops-with-defn-expo)
other
(theory-invariant (incompatible (:rewrite expo-double) (:definition expo))
  :key expo-double-loops-with-defn-expo)
expo-doubletheorem
(defthm expo-double
  (implies (and (case-split (rationalp x))
      (case-split (not (equal x 0))))
    (equal (expo (* 2 x)) (+ 1 (expo x)))))
expo-x+a*2**ktheorem
(defthm expo-x+a*2**k
  (implies (and (< (expo x) k)
      (< 0 a)
      (integerp a)
      (case-split (<= 0 x))
      (case-split (integerp k))
      (case-split (rationalp x)))
    (equal (expo (+ x (* a (expt 2 k))))
      (expo (* a (expt 2 k))))))
expo-x+2**ktheorem
(defthm expo-x+2**k
  (implies (and (< (expo x) k)
      (<= 0 x)
      (case-split (integerp k))
      (case-split (rationalp x)))
    (equal (expo (+ x (expt 2 k))) k)))
expo>=theorem
(defthmd expo>=
  (implies (and (<= (expt 2 n) x) (rationalp x) (integerp n))
    (<= n (expo x)))
  :rule-classes :linear)
expo<=theorem
(defthmd expo<=
  (implies (and (< x (* 2 (expt 2 n)))
      (< 0 x)
      (rationalp x)
      (integerp n))
    (<= (expo x) n))
  :rule-classes :linear)
expo-of-integer-typetheorem
(defthm expo-of-integer-type
  (implies (integerp x)
    (and (integerp (expo x)) (<= 0 (expo x))))
  :rule-classes ((:type-prescription :typed-term (expo x))))
expo-of-integertheorem
(defthm expo-of-integer
  (implies (integerp x) (<= 0 (expo x)))
  :rule-classes (:rewrite))
expo-unique-erictheorem
(defthmd expo-unique-eric
  (implies (and (<= (expt 2 n) (abs x))
      (< (abs x) (expt 2 (1+ n)))
      (rationalp x)
      (integerp n))
    (equal (expo x) n)))
expo-unique-eric-2theorem
(defthm expo-unique-eric-2
  (implies (and (<= (expt 2 n) (abs x))
      (< (abs x) (expt 2 (1+ n)))
      (rationalp x)
      (integerp n))
    (equal (equal (expo x) n) t)))
expo-equality-reduce-to-boundstheorem
(defthmd expo-equality-reduce-to-bounds
  (implies (and (case-split (rationalp x)) (case-split (integerp n)))
    (equal (equal (expo x) n)
      (if (equal 0 x)
        (equal 0 n)
        (and (<= (expt 2 n) (abs x)) (< (abs x) (expt 2 (1+ n))))))))
expo-comparison-rewrite-to-boundtheorem
(defthm expo-comparison-rewrite-to-bound
  (implies (and (syntaxp (not (power2-syntaxp x)))
      (case-split (not (equal 0 x)))
      (integerp k)
      (case-split (rationalp x)))
    (equal (< (expo x) k) (< (abs x) (expt 2 k)))))
expo-comparison-rewrite-to-bound-2theorem
(defthm expo-comparison-rewrite-to-bound-2
  (implies (and (syntaxp (not (power2-syntaxp x)))
      (case-split (not (equal 0 x)))
      (integerp k)
      (case-split (rationalp x)))
    (equal (< k (expo x)) (<= (expt 2 (+ k 1)) (abs x)))))
power2p-expt2-itheorem
(defthm power2p-expt2-i (power2p (expt 2 i)))
expo-expt2-inversetheorem
(defthmd expo-expt2-inverse
  (equal (expo (/ (expt 2 i)))
    (if (integerp i)
      (- i)
      0)))
power2p-shift-specialtheorem
(defthmd power2p-shift-special
  (equal (power2p (* (expt 2 i) x)) (power2p x)))
expo-/-power2p-1theorem
(defthmd expo-/-power2p-1
  (equal (expo (/ (expt 2 i))) (- (expo (expt 2 i)))))
expo-/-power2ptheorem
(defthmd expo-/-power2p
  (implies (power2p x) (equal (expo (/ x)) (- (expo x)))))
expo-/-power2p-alttheorem
(defthm expo-/-power2p-alt
  (implies (and (syntaxp (power2-syntaxp x)) (force (power2p x)))
    (equal (expo (/ x)) (- (expo x)))))
expo-bound-erictheorem
(defthm expo-bound-eric
  (implies (case-split (rationalp x))
    (and (equal (< (* 2 (expt 2 (expo x))) x) nil)
      (equal (< x (* 2 (expt 2 (expo x)))) t)
      (equal (< (expt 2 (+ 1 (expo x))) x) nil)
      (equal (< x (expt 2 (+ 1 (expo x)))) t))))
expo-/-notpower2ptheorem
(defthmd expo-/-notpower2p
  (implies (and (not (power2p x))
      (case-split (not (equal x 0)))
      (<= 0 x)
      (case-split (rationalp x)))
    (equal (expo (/ x)) (+ -1 (- (expo x))))))
power2p-rewritetheorem
(defthmd power2p-rewrite
  (equal (power2p x) (equal x (expt 2 (expo x)))))
expt-comparetheorem
(defthm expt-compare
  (implies (and (syntaxp (and (power2-syntaxp lhs) (power2-syntaxp rhs)))
      (case-split (power2p lhs))
      (case-split (power2p rhs)))
    (equal (< lhs rhs) (< (expo lhs) (expo rhs))))
  :otf-flg t)
expt-compare-equaltheorem
(defthm expt-compare-equal
  (implies (and (syntaxp (and (power2-syntaxp lhs) (power2-syntaxp rhs)))
      (case-split (power2p lhs))
      (case-split (power2p rhs)))
    (equal (equal lhs rhs) (equal (expo lhs) (expo rhs)))))
power2-integertheorem
(defthm power2-integer
  (implies (and (syntaxp (power2-syntaxp x)) (force (power2p x)))
    (equal (integerp x) (<= 0 (expo x)))))
expo-lower-bound-2theorem
(defthm expo-lower-bound-2
  (implies (and (case-split (rationalp x))
      (case-split (<= 0 x))
      (case-split (not (equal x 0))))
    (<= (expt 2 (expo x)) x))
  :rule-classes :linear)
expo-shifttheorem
(defthm expo-shift
  (implies (and (rationalp x) (not (equal x 0)) (integerp n))
    (equal (expo (* (expt 2 n) x)) (+ n (expo x)))))
expo-shift-alttheorem
(defthm expo-shift-alt
  (implies (and (rationalp x) (not (equal x 0)) (integerp n))
    (equal (expo (* x (expt 2 n))) (+ n (expo x)))))
expo-shift-16theorem
(defthm expo-shift-16
  (implies (and (case-split (integerp n))
      (case-split (rationalp x))
      (case-split (not (equal x 0))))
    (equal (expo (* (/ (expt 2 n)) x)) (+ (- n) (expo x)))))
expo-shift-constanttheorem
(defthm expo-shift-constant
  (implies (and (syntaxp (quotep k))
      (equal k (expt 2 (expo k)))
      (rationalp x)
      (not (equal x 0)))
    (equal (expo (* k x)) (+ (expo k) (expo x)))))
include-book
(include-book "common-factor-defuns")
get-expt-factorsfunction
(defun get-expt-factors
  (factor-list)
  (declare (xargs :guard (true-listp factor-list)))
  (if (endp factor-list)
    nil
    (let* ((factor (car factor-list)))
      (if (and (consp factor)
          (or (and (equal (car factor) 'expt)
              (consp (cdr factor))
              (equal (cadr factor) ''2))
            (and (equal (car factor) 'unary-/)
              (consp (cdr factor))
              (consp (cadr factor))
              (equal (caadr factor) 'expt)
              (consp (cdadr factor))
              (equal (cadadr factor) ''2))))
        (cons factor (get-expt-factors (cdr factor-list)))
        (get-expt-factors (cdr factor-list))))))
find-common-expt-factors-to-cancelfunction
(defun find-common-expt-factors-to-cancel
  (expr)
  (declare (xargs :guard (and (pseudo-termp expr))))
  (get-expt-factors (remove-cancelling-factor-pairs (find-common-factors-in-sum-of-products expr))))
bind-k-to-common-expt-factorsfunction
(defund bind-k-to-common-expt-factors
  (expr)
  (declare (xargs :guard-hints (("Goal" :use (:instance remove-cancelling-factor-pairs-preserves-true-listp
           (l (my-intersection-equal (find-common-factors-in-sum-of-products lhs)
               (find-common-factors-in-sum-of-products rhs))))))
      :guard (and (pseudo-termp expr))))
  (let* ((common-factor-list (find-common-expt-factors-to-cancel expr)))
    (if (endp common-factor-list)
      nil
      (list (cons 'k
          (make-product-from-list-of-factors common-factor-list))))))
expo-shift-generaltheorem
(defthm expo-shift-general
  (implies (and (bind-free (bind-k-to-common-expt-factors x) (k))
      (syntaxp (not (equal k x)))
      (force (power2p k))
      (case-split (rationalp x))
      (case-split (not (equal x 0))))
    (equal (expo x) (+ (expo k) (expo (* (/ k) x)))))
  :hints (("goal" :in-theory (enable power2p-rewrite)
     :use (:instance expo-shift (n (- (expo k)))))))
other
(theory-invariant (incompatible (:rewrite expo-shift-general)
    (:rewrite expt-inverse))
  :key expo-shift-general-can-loop-with-expt-inverse)
expo-times-2-not-a-factortheorem
(defthm expo-times-2-not-a-factor
  (implies (rationalp x)
    (equal (integerp (* 1/2 x (/ (expt 2 (expo x)))))
      (equal 0 x))))
expo-a-factor-means-power2theorem
(defthm expo-a-factor-means-power2
  (implies (acl2-numberp x)
    (equal (integerp (* x (/ (expt 2 (expo x)))))
      (or (equal 0 x) (power2p (abs x))))))