Filtering...

mini-theories

books/arithmetic-3/pass1/mini-theories

Included Books

basic-arithmetic inequalities prefer-times expt
other
(in-package "ACL2")
local
(local (include-book "basic-arithmetic"))
local
(local (include-book "inequalities"))
local
(local (include-book "prefer-times"))
local
(local (include-book "expt"))
rewrite-linear-equalities-to-ifftheorem
(defthm rewrite-linear-equalities-to-iff
  (equal (equal (< w x) (< y z)) (iff (< w x) (< y z))))
in-theory
(in-theory (disable rewrite-linear-equalities-to-iff))
uniqueness-of-*-inversesencapsulate
(encapsulate nil
  (local (defthm uniqueness-of-*-inverses-lemma-2
      (equal (equal (* x y) 1)
        (and (not (equal x 0)) (acl2-numberp x) (equal y (/ x))))))
  (defthm uniqueness-of-*-inverses
    (equal (equal (* x y) 1)
      (and (not (equal (fix x) 0)) (equal y (/ x))))
    :hints (("Goal" :in-theory (disable equal-/)))))
in-theory
(in-theory (disable uniqueness-of-*-inverses))
other
(theory-invariant (not (and (active-runep '(:rewrite uniqueness-of-*-inverses))
      (active-runep '(:rewrite equal-/)))))
expts-add-aggressivetheorem
(defthm expts-add-aggressive
  (implies (and (integerp i) (integerp j))
    (equal (expt x (+ i j))
      (if (equal (+ i j) 0)
        1
        (if (equal (fix x) 0)
          0
          (* (expt x i) (expt x j)))))))
expts-add-inversetheorem
(defthm expts-add-inverse
  (implies (and (integerp i) (integerp j))
    (equal (* (expt x i) (expt x j))
      (if (and (equal i 0) (equal j 0))
        1
        (if (equal (fix x) 0)
          0
          (expt x (+ i j)))))))
in-theory
(in-theory (disable expts-add-aggressive expts-add-inverse))