Filtering...

basic-helper

books/arithmetic-3/bind-free/basic-helper

Included Books

top default-hint
other
(in-package "ACL2")
local
(local (include-book "../pass1/top"))
local
(local (include-book "default-hint"))
other
(set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
     hist
     pspv)))
local
(local (in-theory (disable functional-commutativity-of-minus-*-right
      functional-commutativity-of-minus-*-left)))
local
(local (in-arithmetic-theory '((:rewrite arith-associativity-of-*) (:rewrite arith-commutativity-of-*)
      (:rewrite arith-commutativity-2-of-*)
      (:rewrite arith-unicity-of-1)
      (:rewrite arith-times-zero)
      (:rewrite arith-inverse-of-*-1)
      (:rewrite arith-inverse-of-*-2)
      (:rewrite arith-inverse-of-*-3)
      (:rewrite arith-functional-self-inversion-of-/)
      (:rewrite arith-distributivity-of-/-over-*)
      (:rewrite arith-reciprocal-minusa)
      (:rewrite arith-distributivity-1)
      (:rewrite arith-distributivity-2)
      (:rewrite arith-fold-consts-in-*)
      (:rewrite arith-expt-0)
      (:rewrite arith-expt-1)
      (:rewrite arith-expt-minus-1)
      (:rewrite arith-functional-commutativity-of-expt-/)
      (:rewrite arith-expt-minus-exponent)
      (:rewrite arith-expt-negative-constant-exponent)
      (:rewrite arith-exponents-multiply)
      (:rewrite arith-distributivity-of-expt-over-*)
      (:rewrite arith-fix-revealed)
      (:rewrite arith-rational-implies2)
      (:rewrite arith-exponents-add-1)
      (:rewrite arith-exponents-add-for-nonpos-exponentsa)
      (:rewrite arith-exponents-add-for-nonneg-exponentsa)
      (:rewrite arith-exponents-add-2))))
local
(local (defun ind
    (x)
    (if (integerp x)
      (cond ((equal x 0) t)
        ((equal x -1) t)
        ((equal x 1) t)
        ((< 0 x) (ind (- x 2)))
        ((< x 0) (ind (+ x 2))))
      t)))
local
(local (encapsulate nil
    (local (defthm hack1a (implies (integerp x) (integerp (+ -1 x)))))
    (local (defthm hack1b (implies (integerp x) (integerp (+ x 1)))))
    (defthm odd-and-even
      (implies (and (integerp x) (not (integerp (* 1/2 x))))
        (integerp (+ -1/2 (* 1/2 x))))
      :hints (("Goal" :induct (ind x)) ("Subgoal *1/5'''" :use ((:instance hack1a (x (+ 1/2 r)))))
        ("Subgoal *1/4'''" :use ((:instance hack1b (x (+ -3/2 r))))))
      :rule-classes :type-prescription)))
expt-type-prescription-negative-base-even-exponentencapsulate
(encapsulate nil
  (local (defthm expt-x-2
      (implies (and (rationalp x) (not (equal x 0)))
        (< 0 (expt x 2)))))
  (local (defthm <-0-expt-x-2
      (implies (and (< r 0) (rationalp r) (integerp i))
        (< 0 (expt (expt r i) 2)))
      :hints (("Goal" :use ((:instance expt-x-2 (x (expt r i))))))))
  (defthm expt-type-prescription-negative-base-even-exponent
    (implies (and (< r 0)
        (rationalp r)
        (integerp i)
        (integerp (* 1/2 i)))
      (< 0 (expt r i)))
    :rule-classes (:type-prescription :generalize)
    :hints (("Goal" :use ((:instance <-0-expt-x-2 (i (* 1/2 i)))))))
  (local (defthm reduce
      (implies (and (integerp i) (rationalp r) (not (equal r 0)))
        (equal (expt r i) (* r (expt r (- i 1)))))))
  (defthm expt-type-prescription-negative-base-odd-exponent
    (implies (and (< r 0)
        (rationalp r)
        (integerp i)
        (not (integerp (* 1/2 i))))
      (< (expt r i) 0))
    :rule-classes (:type-prescription :generalize)
    :hints (("Goal" :use ((:instance expt-type-prescription-negative-base-even-exponent
          (r r)
          (i (- i 1))) (:instance reduce))
       :in-theory (disable reduce)))))
local
(local (in-theory (enable functional-commutativity-of-minus-*-right
      functional-commutativity-of-minus-*-left)))
expt-negative-base-even-exponenttheorem
(defthm expt-negative-base-even-exponent
  (implies (and (integerp i) (integerp (* 1/2 i)))
    (equal (expt (- r) i) (expt r i)))
  :hints (("Goal" :induct (ind i))))
expt-negative-base-odd-exponentencapsulate
(encapsulate nil
  (local (defthm expt-negative-base-odd-exponent-hack
      (implies (and (integerp i) (not (integerp (* 1/2 i))))
        (equal (expt (* -1 r) i) (* -1 (expt r i))))
      :hints (("Goal" :induct (ind i)))
      :rule-classes nil))
  (local (defthm hack654 (equal (* -1 x) (- x))))
  (defthm expt-negative-base-odd-exponent
    (implies (and (integerp i) (not (integerp (* 1/2 i))))
      (equal (expt (- r) i) (- (expt r i))))
    :hints (("Goal" :use expt-negative-base-odd-exponent-hack))))