mini-theories

(in-package "ACL2")

(local (include-book "mini-theories-helper"))

(defthm |(- x)| (equal (- x) (* -1 x)))

(in-theory (disable |(- x)|))

(theory-invariant (not (and (active-runep '(:rewrite |(* -1 x)|))
      (active-runep '(:rewrite |(- x)|))))
  :error t)

(defthm |(/ x)|
  (equal (/ x) (expt x -1))
  :hints (("Goal" :expand (expt x -1))))

(in-theory (disable |(/ x)|))

(theory-invariant (not (and (active-runep '(:rewrite |(expt x -1)|))
      (active-runep '(:rewrite |(/ x)|))))
  :error t)

(defthm rewrite-linear-equalities-to-iff
  (equal (equal (< w x) (< y z)) (iff (< w x) (< y z))))

(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))

(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))

(defthm expt-type-prescription-nonpositive-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 expt-type-prescription-negative-base-even-exponent)))))

(defthm expt-type-prescription-nonpositive-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-odd-exponent)))))

(defthm expt-negative-base-even-exponent
  (implies (and (rationalp r) (integerp i) (integerp (* 1/2 i)))
    (equal (expt (* -1 r) i) (expt r i))))

(defthm expt-negative-base-odd-exponent
  (implies (and (rationalp r) (integerp i) (not (integerp (* 1/2 i))))
    (equal (expt (* -1 r) i) (* -1 (expt r i)))))