Filtering...

unary-divide

books/rtl/rel9/arithmetic/unary-divide

Included Books

predicate fp2 inverted-factor
other
(in-package "ACL2")
local
(local (include-book "predicate"))
local
(local (include-book "fp2"))
local
(local (include-book "inverted-factor"))
unary-divide-less-than-zerotheorem
(defthm unary-divide-less-than-zero
  (implies (case-split (not (complex-rationalp x)))
    (equal (< (/ x) 0) (< x 0))))
unary-divide-greater-than-zerotheorem
(defthm unary-divide-greater-than-zero
  (implies (case-split (not (complex-rationalp x)))
    (equal (< 0 (/ x)) (< 0 x))))
unary-divide-equal-0theorem
(defthm unary-divide-equal-0
  (implies (case-split (acl2-numberp x))
    (equal (equal 0 (/ x)) (equal 0 x))))
unary-divide-equal-non-zero-constanttheorem
(defthm unary-divide-equal-non-zero-constant
  (implies (and (syntaxp (and (quotep k)))
      (case-split (acl2-numberp x))
      (case-split (acl2-numberp k)))
    (equal (equal k (/ x)) (equal (/ k) x))))
unary-divide-less-than-non-zero-constanttheorem
(defthm unary-divide-less-than-non-zero-constant
  (implies (and (syntaxp (and (quotep k) (not (equal 0 (cadr k)))))
      (<= 0 k)
      (case-split (<= 0 x))
      (case-split (not (equal 0 k)))
      (case-split (not (equal 0 x)))
      (case-split (rationalp x))
      (case-split (rationalp k)))
    (equal (< (/ x) k) (< (/ k) x))))
unary-divide-greater-than-non-zero-constanttheorem
(defthm unary-divide-greater-than-non-zero-constant
  (implies (and (syntaxp (and (quotep k) (not (equal 0 (cadr k)))))
      (<= 0 k)
      (case-split (<= 0 x))
      (case-split (not (equal 0 k)))
      (case-split (not (equal 0 x)))
      (case-split (rationalp x))
      (case-split (rationalp k)))
    (equal (< k (/ x)) (< x (/ 1 k)))))