Filtering...

prefer-times

books/arithmetic-3/pass1/prefer-times

Included Books

basic-arithmetic inequalities
other
(in-package "ACL2")
local
(local (include-book "basic-arithmetic"))
local
(local (include-book "inequalities"))
other
(set-default-hints '((nonlinearp-default-hint-pass1 stable-under-simplificationp
     hist
     pspv)))
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)))))
local
(local (in-arithmetic-theory '((:rewrite commutativity-of-*) (:rewrite commutativity-2-of-*)
      (:rewrite inverse-of-*)
      (:rewrite times-one)
      (:rewrite times-minus-one))))
normalize-<-/-to-*-1theorem
(defthm normalize-<-/-to-*-1
  (implies (and (rationalp x) (rationalp y))
    (equal (< x (/ y))
      (cond ((< y 0) (< 1 (* x y)))
        ((< 0 y) (< (* x y) 1))
        (t (< x 0))))))
normalize-<-/-to-*-2theorem
(defthm normalize-<-/-to-*-2
  (implies (and (rationalp x) (rationalp y))
    (equal (< (/ y) x)
      (cond ((< y 0) (< (* x y) 1))
        ((< 0 y) (< 1 (* x y)))
        (t (< 0 x))))))
normalize-<-/-to-*-3-1theorem
(defthm normalize-<-/-to-*-3-1
  (implies (and (rationalp x) (rationalp y) (rationalp z))
    (equal (< x (* y (/ z)))
      (cond ((< z 0) (< y (* x z)))
        ((< 0 z) (< (* x z) y))
        (t (< x 0))))))
normalize-<-/-to-*-3-2theorem
(defthm normalize-<-/-to-*-3-2
  (implies (and (rationalp x) (rationalp y) (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 (rationalp x) (rationalp y) (rationalp z))
    (equal (< (* y (/ z)) x)
      (cond ((< z 0) (< (* x z) y))
        ((< 0 z) (< y (* x z)))
        (t (< 0 x))))))
normalize-<-/-to-*-3-4theorem
(defthm normalize-<-/-to-*-3-4
  (implies (and (rationalp x) (rationalp y) (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-/))