Filtering...

product-proofs

books/rtl/rel9/arithmetic/product-proofs

Included Books

predicate fp2
other
(in-package "ACL2")
local
(local (include-book "predicate"))
local
(local (include-book "fp2"))
local
(local (defthm hack2
    (implies (and (< y 0) (rationalp x) (case-split (< x 0)))
      (<= 0 (* x y)))))
product-less-than-zero-1theorem
(defthm product-less-than-zero-1
  (implies (case-split (not (complex-rationalp x)))
    (equal (< (* x y) 0)
      (if (< x 0)
        (< 0 y)
        (if (equal 0 x)
          nil
          (if (not (acl2-numberp x))
            nil
            (< y 0))))))
  :otf-flg t
  :hints (("Goal" :cases ((and (rationalp x) (rationalp y)) (and (complex-rationalp x) (rationalp y))
       (and (not (acl2-numberp x)) (rationalp y))
       (and (rationalp x) (complex-rationalp y))
       (and (complex-rationalp x) (complex-rationalp y))
       (and (not (acl2-numberp x)) (complex-rationalp y))))))
product-less-than-zero-2theorem
(defthm product-less-than-zero-2
  (implies (case-split (not (complex-rationalp y)))
    (equal (< (* x y) 0)
      (or (and (< x 0) (< 0 y)) (and (< y 0) (< 0 x)))))
  :hints (("Goal" :in-theory (disable product-less-than-zero-1)
     :use (:instance product-less-than-zero-1 (x y) (y x)))))
product-less-than-zerotheorem
(defthm product-less-than-zero
  (implies (case-split (or (not (complex-rationalp x)) (not (complex-rationalp y))))
    (equal (< (* x y) 0)
      (if (< x 0)
        (< 0 y)
        (if (equal 0 x)
          nil
          (if (not (acl2-numberp x))
            nil
            (< y 0)))))))
product-greater-than-zerotheorem
(defthm product-greater-than-zero
  (implies (case-split (not (complex-rationalp y)))
    (equal (< 0 (* x y))
      (or (and (< 0 x) (< 0 y)) (and (< y 0) (< x 0)))))
  :hints (("Goal" :cases (complex-rationalp x))))
product-greater-than-zero-2theorem
(defthm product-greater-than-zero-2
  (implies (case-split (not (complex-rationalp x)))
    (equal (< 0 (* x y))
      (or (and (< 0 x) (< 0 y)) (and (< y 0) (< x 0)))))
  :hints (("Goal" :in-theory (disable product-greater-than-zero)
     :use (:instance product-greater-than-zero (x y) (y x)))))
product-equal-zerotheorem
(defthm product-equal-zero
  (equal (equal 0 (* x y))
    (if (not (acl2-numberp x))
      t
      (if (not (acl2-numberp y))
        t
        (if (equal 0 x)
          t
          (equal 0 y)))))
  :hints (("Goal" :cases (complex-rationalp x))))