expt

other

(in-package "ACL2")

natpfunction

(defun natp
  (x)
  (declare (xargs :guard t))
  (and (integerp x) (<= 0 x)))

flfunction

(defund fl
  (x)
  (declare (xargs :guard (real/rationalp x)))
  (floor x 1))

include-book

(include-book "ground-zero")

include-book

(include-book "negative-syntaxp")

local

(local (include-book "expt-proofs"))

a16theorem

(defthm a16
  (equal (expt (* a b) i) (* (expt a i) (expt b i))))

expt-splittheorem

(defthmd expt-split
  (implies (and (integerp i)
      (integerp j)
      (case-split (acl2-numberp r))
      (case-split (not (equal r 0))))
    (equal (expt r (+ i j)) (* (expt r i) (expt r j)))))

other

(theory-invariant (not (and (active-runep '(:rewrite expt-split))
      (active-runep '(:rewrite a15))))
  :key expt-split-invariant)

other

(theory-invariant (not (and (active-runep '(:rewrite expt-split))
      (active-runep '(:definition expt))))
  :key expt-split-invariant-2)

expt-2-positive-rational-typetheorem

(defthm expt-2-positive-rational-type
  (and (rationalp (expt 2 i)) (< 0 (expt 2 i)))
  :rule-classes (:rewrite (:type-prescription :typed-term (expt 2 i))))

expt-2-positive-integer-typetheorem

(defthm expt-2-positive-integer-type
  (implies (<= 0 i)
    (and (integerp (expt 2 i)) (< 0 (expt 2 i))))
  :rule-classes (:type-prescription))

a14theorem

(defthm a14
  (and (implies (and (integerp i) (<= 0 i) (<= 0 j))
      (and (integerp (expt i j)) (<= 0 (expt i j))))
    (implies (and (rationalp i) (not (equal i 0)))
      (not (equal (expt i j) 0))))
  :rule-classes ((:type-prescription :corollary (implies (and (integerp i) (<= 0 i) (<= 0 j))
       (and (integerp (expt i j)) (<= 0 (expt i j))))) (:type-prescription :corollary (implies (and (rationalp i) (not (equal i 0)))
        (not (equal (expt i j) 0))))))

expt-2-integerptheorem

(defthm expt-2-integerp
  (implies (<= 0 i) (integerp (expt 2 i))))

expt-2-type-lineartheorem

(defthm expt-2-type-linear
  (implies (<= 0 i) (<= 1 (expt 2 i)))
  :rule-classes ((:linear :trigger-terms ((expt 2 i)))))

expt-strong-monotonetheorem

(defthmd expt-strong-monotone
  (implies (and (integerp n) (integerp m))
    (equal (< (expt 2 n) (expt 2 m)) (< n m))))

expt2-integertheorem

(defthm expt2-integer
  (implies (case-split (integerp i))
    (equal (integerp (expt 2 i)) (<= 0 i))))

expt-strong-monotone-lineartheorem

(defthmd expt-strong-monotone-linear
  (implies (and (< n m)
      (case-split (integerp n))
      (case-split (integerp m)))
    (< (expt 2 n) (expt 2 m)))
  :rule-classes ((:linear :match-free :all)))

expt-weak-monotonetheorem

(defthmd expt-weak-monotone
  (implies (and (integerp n) (integerp m))
    (equal (<= (expt 2 n) (expt 2 m)) (<= n m))))

expt-weak-monotone-lineartheorem

(defthmd expt-weak-monotone-linear
  (implies (and (<= n m)
      (case-split (integerp n))
      (case-split (integerp m)))
    (<= (expt 2 n) (expt 2 m)))
  :rule-classes ((:linear :match-free :all)))

expt-between-one-and-twotheorem

(defthmd expt-between-one-and-two
  (implies (and (<= 1 (expt 2 i)) (< (expt 2 i) 2))
    (equal (expt 2 i) 1)))

expt-with-i-non-integertheorem

(defthm expt-with-i-non-integer
  (implies (not (integerp i)) (equal (expt r i) 1)))

expt-minus-helpertheorem

(defthmd expt-minus-helper
  (equal (expt r (* -1 i)) (/ (expt r i))))

expt-minustheorem

(defthmd expt-minus
  (implies (syntaxp (negative-syntaxp i))
    (equal (expt r i) (/ (expt r (* -1 i))))))

expt-inversetheorem

(defthmd expt-inverse
  (equal (/ (expt 2 i)) (expt 2 (* -1 i))))

other

(theory-invariant (not (and (active-runep '(:rewrite expt-minus))
      (active-runep '(:rewrite expt-inverse))))
  :key expt-minus-invariant)

a15theorem

(defthmd a15
  (implies (and (rationalp i)
      (not (equal i 0))
      (integerp j1)
      (integerp j2))
    (and (equal (* (expt i j1) (expt i j2)) (expt i (+ j1 j2)))
      (equal (* (expt i j1) (* (expt i j2) x))
        (* (expt i (+ j1 j2)) x)))))

expt-r-0theorem

(defthm expt-r-0 (equal (expt r 0) 1))

expt-0-itheorem

(defthm expt-0-i
  (implies (and (case-split (integerp i))
      (case-split (not (equal 0 i))))
    (equal (expt 0 i) 0)))

in-theory

(in-theory (disable (:executable-counterpart expt)))

other

(set-compile-fns t)

expt-executefunction

(defun expt-execute (r i) (expt r i))

expt-execute-rewritetheorem

(defthm expt-execute-rewrite
  (implies (and (syntaxp (and (quotep r) (quotep i) (< (abs (cadr i)) 1000))))
    (equal (expt r i) (expt-execute r i))))

expt2-constants-collect-special-1theorem

(defthm expt2-constants-collect-special-1
  (implies (and (syntaxp (and (quotep i1) (quotep i2)))
      (case-split (rationalp y))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (equal (* (expt 2 i1) (/ (expt 2 i2)) y)
      (* (expt 2 (- i1 i2)) y))))

expt2-constants-collect-special-2theorem

(defthm expt2-constants-collect-special-2
  (implies (and (syntaxp (and (quotep i1) (quotep i2)))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (equal (* (expt 2 i1) (/ (expt 2 i2))) (expt 2 (- i1 i2)))))

expt2-constants-collect-special-4theorem

(defthm expt2-constants-collect-special-4
  (implies (and (syntaxp (and (quotep i1) (quotep i2)))
      (case-split (rationalp y))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (equal (* (/ (expt 2 i2)) (expt 2 i1) y)
      (* (expt 2 (- i1 i2)) y))))

expt2-constants-collect-special-5theorem

(defthm expt2-constants-collect-special-5
  (implies (and (syntaxp (and (quotep i1) (quotep i2)))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (equal (* (/ (expt 2 i2)) (expt 2 i1)) (expt 2 (- i1 i2)))))

expt2-constants-collect-special-6theorem

(defthm expt2-constants-collect-special-6
  (implies (and (syntaxp (and (quotep i1) (quotep i2)))
      (case-split (rationalp x))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (equal (* (expt 2 i2) x (expt 2 i1))
      (* (expt 2 (+ i1 i2)) x))))

expt2-constants-collect-special-3theorem

(defthm expt2-constants-collect-special-3
  (implies (and (syntaxp (and (quotep i1) (quotep i2)))
      (case-split (rationalp x))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (equal (equal (* x (expt 2 i1)) (expt 2 i2))
      (equal x (expt 2 (- i2 i1))))))

expt2-1-to-1theorem

(defthm expt2-1-to-1
  (implies (and (integerp i1) (integerp i2))
    (equal (equal (expt 2 i1) (expt 2 i2)) (equal i1 i2))))

expt-eventheorem

(defthm expt-even
  (implies (and (< 0 i) (case-split (integerp i)))
    (integerp (* 1/2 (expt 2 i)))))

expt-quotient-integerptheorem

(defthm expt-quotient-integerp
  (implies (and (<= j i)
      (case-split (integerp i))
      (case-split (integerp j)))
    (integerp (* (expt 2 i) (/ (expt 2 j)))))
  :rule-classes (:rewrite :type-prescription))

expt-quotient-integerp-alttheorem

(defthm expt-quotient-integerp-alt
  (implies (and (<= j i)
      (case-split (integerp i))
      (case-split (integerp j)))
    (integerp (* (/ (expt 2 j)) (expt 2 i))))
  :rule-classes (:rewrite :type-prescription))

expt-prod-integer-3-termstheorem

(defthm expt-prod-integer-3-terms
  (implies (and (integerp n) (<= 0 (+ i j)) (integerp i) (integerp j))
    (integerp (* (expt 2 i) (expt 2 j) n))))

expt2-inverse-integertheorem

(defthm expt2-inverse-integer
  (implies (case-split (integerp i))
    (equal (integerp (/ (expt 2 i))) (<= i 0))))

expt-prod-integer-3-terms-2theorem

(defthm expt-prod-integer-3-terms-2
  (implies (and (<= 0 (+ i (- j) (- l)))
      (integerp i)
      (integerp j)
      (integerp l))
    (integerp (* (expt 2 i) (/ (expt 2 j)) (/ (expt 2 l))))))

expt2-inverse-eventheorem

(defthm expt2-inverse-even
  (implies (case-split (integerp i))
    (equal (integerp (* 1/2 (/ (expt 2 i)))) (<= (+ 1 i) 0))))

expt-2-split-product-indextheorem

(defthmd expt-2-split-product-index
  (implies (and (syntaxp (not (quotep i)))
      (case-split (rationalp r))
      (case-split (integerp i)))
    (equal (expt r (* 2 i)) (* (expt r i) (expt r i)))))

expt-bigger-than-itheorem

(defthm expt-bigger-than-i
  (implies (integerp i) (< i (expt 2 i))))

expt-compare-with-doubletheorem

(defthmd expt-compare-with-double
  (implies (and (integerp x) (integerp i))
    (equal (< (* 2 x) (expt 2 i)) (< x (expt 2 (+ -1 i))))))

expt-2-reduce-leading-constant-gentheorem

(defthmd expt-2-reduce-leading-constant-gen
  (implies (case-split (integerp (+ k d)))
    (equal (expt 2 (+ k d))
      (* (expt 2 (fl k)) (expt 2 (+ (mod k 1) d))))))

expt-2-reduce-leading-constanttheorem

(defthmd expt-2-reduce-leading-constant
  (implies (and (syntaxp (and (quotep k) (or (>= (cadr k) 1) (< (cadr k) 0))))
      (case-split (integerp (+ k d))))
    (equal (expt 2 (+ k d))
      (* (expt 2 (fl k)) (expt 2 (+ (mod k 1) d))))))

expt-combinetheorem

(defthmd expt-combine
  (implies (and (case-split (rationalp r))
      (case-split (not (equal r 0)))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (and (equal (* (expt r i1) (expt r i2)) (expt r (+ i1 i2)))
      (equal (* (expt r i1) (* (expt r i2) x))
        (* (expt r (+ i1 i2)) x)))))

expt-with-small-ntheorem

(defthm expt-with-small-n
  (implies (<= n 0) (<= (expt 2 n) 1))
  :rule-classes (:linear))

even-not-equal-oddtheorem

(defthmd even-not-equal-odd
  (implies (and (evenp x) (oddp y)) (not (equal x y))))

expt-2-is-not-oddtheorem

(defthm expt-2-is-not-odd
  (implies (and (evenp x) (< 0 i) (integerp i))
    (equal (equal (expt 2 i) (+ 1 x)) nil)))

expt-with-product-exponenttheorem

(defthmd expt-with-product-exponent
  (implies (and (syntaxp (not (quotep i))) (case-split (integerp i)))
    (equal (expt 2 (* 2 i)) (* (expt 2 i) (expt 2 i)))))

natp-expttheorem

(defthmd natp-expt
  (implies (natp n)
    (and (integerp (expt 2 n)) (< 0 (expt 2 n))))
  :rule-classes (:type-prescription :rewrite))

expt-exceeds-another-by-more-than-1theorem

(defthm expt-exceeds-another-by-more-than-1
  (implies (and (<= 0 i) (<= 0 j) (integerp i) (integerp j))
    (implies (< (+ 1 i) j) (< (+ 1 (expt 2 i)) (expt 2 j)))))

expt-exceeds-2theorem

(defthm expt-exceeds-2
  (implies (and (< i j) (<= 0 i) (<= 0 j) (integerp i) (integerp j))
    (<= (+ 1 (expt 2 i)) (expt 2 j)))
  :rule-classes (:rewrite :linear))

expt-with-i-non-integer-specialtheorem

(defthm expt-with-i-non-integer-special
  (implies (not (integerp i))
    (equal (expt 2 (+ -1 i))
      (if (acl2-numberp i)
        1
        1/2))))

Included Books