Filtering...

prefer-times

books/arithmetic-2/pass1/prefer-times

Included Books

basic-arithmetic inequalities
other
(in-package "ACL2")
local
(local (include-book "basic-arithmetic"))
local
(local (include-book "inequalities"))
local
(local (defthm iff-equal
    (equal (equal (< w x) (< y z)) (iff (< w x) (< y z)))))
equal-*-/-1theorem
(defthm equal-*-/-1
  (equal (equal (* (/ x) y) z)
    (if (equal (fix x) 0)
      (equal z 0)
      (and (acl2-numberp z) (equal (fix y) (* x z))))))
equal-*-/-2theorem
(defthm equal-*-/-2
  (equal (equal (* y (/ x)) z)
    (if (equal (fix x) 0)
      (equal z 0)
      (and (acl2-numberp z) (equal (fix y) (* z x))))))
local
(local (defthm times-one
    (implies (acl2-numberp x) (equal (* 1 x) x))))
local
(local (defthm times-minus-one
    (implies (acl2-numberp x) (equal (* -1 x) (- x)))))
normalize-<-/-to-*-1theorem
(defthm normalize-<-/-to-*-1
  (implies (and (real/rationalp x) (real/rationalp y))
    (equal (< x (/ y))
      (cond ((< y 0) (< 1 (* x y)))
        ((< 0 y) (< (* x y) 1))
        (t (< x 0)))))
  :hints (("Goal" :use ((:instance <-*-right-cancel (x x) (y (/ y)) (z y)) (:instance right-cancellation-for-* (x x) (y (/ y)) (z y)))
     :in-theory (disable equal-/))))
normalize-<-/-to-*-2theorem
(defthm normalize-<-/-to-*-2
  (implies (and (real/rationalp x) (real/rationalp y))
    (equal (< (/ y) x)
      (cond ((< y 0) (< (* x y) 1))
        ((< 0 y) (< 1 (* x y)))
        (t (< 0 x)))))
  :hints (("Goal" :use ((:instance <-*-right-cancel (x (/ y)) (y x) (z y)) (:instance right-cancellation-for-* (x (/ y)) (y x) (z y)))
     :in-theory (disable equal-/ normalize-<-/-to-*-1))))
normalize-<-/-to-*-3-1theorem
(defthm normalize-<-/-to-*-3-1
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (real/rationalp z))
    (equal (< x (* y (/ z)))
      (cond ((< z 0) (< y (* x z)))
        ((< 0 z) (< (* x z) y))
        (t (< x 0)))))
  :hints (("Goal" :use ((:instance <-*-right-cancel (x x) (y (* y (/ z))) (z z))))))
normalize-<-/-to-*-3-2theorem
(defthm normalize-<-/-to-*-3-2
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (real/rationalp z))
    (equal (< x (* (/ z) y))
      (cond ((< z 0) (< y (* x z)))
        ((< 0 z) (< (* x z) y))
        (t (< x 0))))))
normalize-<-/-to-*-3-3theorem
(defthm normalize-<-/-to-*-3-3
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (real/rationalp z))
    (equal (< (* y (/ z)) x)
      (cond ((< z 0) (< (* x z) y))
        ((< 0 z) (< y (* x z)))
        (t (< 0 x)))))
  :hints (("Goal" :use ((:instance <-*-right-cancel (x (* y (/ z))) (y x) (z z)))
     :in-theory (disable normalize-<-/-to-*-3-1))))
normalize-<-/-to-*-3-4theorem
(defthm normalize-<-/-to-*-3-4
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (real/rationalp z))
    (equal (< (* (/ z) y) x)
      (cond ((< z 0) (< (* x z) y))
        ((< 0 z) (< y (* x z)))
        (t (< 0 x))))))
other
(deftheory prefer-*-to-/
  '(equal-*-/-1 equal-*-/-2
    normalize-<-/-to-*-1
    normalize-<-/-to-*-2
    normalize-<-/-to-*-3-1
    normalize-<-/-to-*-3-2
    normalize-<-/-to-*-3-3
    normalize-<-/-to-*-3-4))
in-theory
(in-theory (disable prefer-*-to-/))