Filtering...

times

books/kestrel/arithmetic-light/times

Included Books

less-than realpart imagpart complex equal-of-booleans
other
(in-package "ACL2")
local
(local (include-book "less-than"))
local
(local (include-book "realpart"))
local
(local (include-book "imagpart"))
local
(local (include-book "complex"))
local
(local (include-book "kestrel/utilities/equal-of-booleans" :dir :system))
integerp-of-*theorem
(defthm integerp-of-*
  (implies (and (integerp x) (integerp y)) (integerp (* x y))))
natp-of-*-when-natp-and-natptheorem
(defthm natp-of-*-when-natp-and-natp
  (implies (and (natp x) (natp y)) (natp (* x y))))
equal-of-0-and-*theorem
(defthm equal-of-0-and-*
  (equal (equal 0 (* x y))
    (or (equal 0 (fix x)) (equal 0 (fix y)))))
*-of-0theorem
(defthm *-of-0 (equal (* 0 x) 0))
commutativity-2-of-*theorem
(defthm commutativity-2-of-*
  (equal (* x (* y z)) (* y (* x z)))
  :hints (("Goal" :use ((:instance associativity-of-*) (:instance associativity-of-* (x y) (y x)))
     :in-theory (disable associativity-of-*))))
*-of-*-combine-constantstheorem
(defthm *-of-*-combine-constants
  (implies (and (syntaxp (quotep y)) (syntaxp (quotep x)))
    (equal (* x (* y z)) (* (* x y) z))))
*-of--1theorem
(defthm *-of--1 (equal (* -1 x) (- x)))
--becomes-*-of--1theorem
(defthmd --becomes-*-of--1 (equal (- x) (* -1 x)))
other
(theory-invariant (incompatible (:rewrite *-of--1)
    (:rewrite --becomes-*-of--1)))
integerp-of-*-threetheorem
(defthmd integerp-of-*-three
  (implies (and (integerp (* x y)) (integerp z))
    (integerp (* x y z)))
  :hints (("Goal" :use (:instance integerp-of-* (x (* x y)) (y z))
     :in-theory (disable integerp-of-*))))
*-of---arg1theorem
(defthm *-of---arg1
  (implies (syntaxp (not (quotep x)))
    (equal (* (- x) y) (- (* x y))))
  :hints (("Goal" :in-theory (e/d (--becomes-*-of--1) (*-of--1)))))
*-of---arg1-gentheorem
(defthmd *-of---arg1-gen
  (equal (* (- x) y) (- (* x y)))
  :hints (("Goal" :in-theory (e/d (--becomes-*-of--1) (*-of--1)))))
*-of---arg2theorem
(defthm *-of---arg2
  (equal (* x (- y)) (- (* x y)))
  :hints (("Goal" :in-theory (e/d (--becomes-*-of--1) (*-of--1)))))
--of-*-push-into-arg1theorem
(defthmd --of-*-push-into-arg1
  (equal (- (* x y)) (* (- x) y)))
other
(theory-invariant (incompatible (:rewrite --of-*-push-into-arg1)
    (:rewrite *-of---arg1)))
--of-*-push-into-arg2theorem
(defthmd --of-*-push-into-arg2
  (equal (- (* x y)) (* x (- y))))
other
(theory-invariant (incompatible (:rewrite --of-*-push-into-arg2)
    (:rewrite *-of---arg2)))
*-both-sidestheorem
(defthmd *-both-sides
  (implies (equal x y) (equal (* z x) (* z y))))
local
(local (defthm *-of-/-same-arg2
    (equal (* x (/ x) y)
      (if (equal 0 (fix x))
        0
        (fix y)))
    :hints (("Goal" :in-theory (disable associativity-of-* commutativity-2-of-*)
       :use (:instance associativity-of-* (y (/ x)) (z y))))))
equal-of-*-and-*-canceltheorem
(defthm equal-of-*-and-*-cancel
  (equal (equal (* x y) (* x z))
    (or (equal (fix x) 0) (equal (fix y) (fix z))))
  :hints (("Goal" :use (:instance *-both-sides (x (* x y)) (y (* x z)) (z (/ x))))))
equal-of-*-and-*-cancel-arg2-arg2theorem
(defthm equal-of-*-and-*-cancel-arg2-arg2
  (equal (equal (* y x) (* z x))
    (or (equal (fix x) 0) (equal (fix y) (fix z))))
  :hints (("Goal" :use (:instance *-both-sides (x (* x y)) (y (* x z)) (z (/ x))))))
equal-of-*-and-*-cancel-arg2-arg2+theorem
(defthm equal-of-*-and-*-cancel-arg2-arg2+
  (equal (equal (* y x) (* z x w))
    (or (equal (fix x) 0) (equal (fix y) (fix (* z w)))))
  :hints (("Goal" :use (:instance *-both-sides (x (* x y)) (y (* x z w)) (z (/ x))))))
<-of-*-and-0theorem
(defthm <-of-*-and-0
  (implies (and (rationalp x) (rationalp y))
    (equal (< (* x y) 0)
      (or (and (< x 0) (< 0 y)) (and (< y 0) (< 0 x)))))
  :hints (("Goal" :cases ((< x 0) (and (< 0 x) (< y 0)) (and (< 0 x) (< 0 y))))))
<-of-0-and-*theorem
(defthm <-of-0-and-*
  (implies (and (rationalp x) (rationalp y))
    (equal (< 0 (* x y))
      (or (and (< x 0) (< y 0)) (and (< 0 y) (< 0 x))))))
<-of-*-and-*-canceltheorem
(defthm <-of-*-and-*-cancel
  (implies (and (< 0 y) (rationalp x1) (rationalp x2) (rationalp y))
    (equal (< (* x1 y) (* x2 y)) (< x1 x2)))
  :hints (("Goal" :cases ((< x1 x2))
     :use ((:instance positive (x (- x2 x1))) (:instance positive (x (- x1 x2)))))))
<-of-*-and-*-cancel-gentheorem
(defthm <-of-*-and-*-cancel-gen
  (implies (and (rationalp x1) (rationalp x2) (rationalp y))
    (equal (< (* x1 y) (* x2 y))
      (if (< 0 y)
        (< x1 x2)
        (if (equal 0 y)
          nil
          (< x2 x1)))))
  :hints (("Goal" :use ((:instance <-of-*-and-*-cancel) (:instance <-of-*-and-*-cancel (y (- y))))
     :in-theory (disable <-of-*-and-*-cancel))))
<-of-*-and-*-cancel-arg1-and-arg1theorem
(defthm <-of-*-and-*-cancel-arg1-and-arg1
  (implies (and (< 0 y) (rationalp x1) (rationalp x2) (rationalp y))
    (equal (< (* y x1) (* y x2)) (< x1 x2)))
  :hints (("Goal" :use <-of-*-and-*-cancel
     :in-theory (disable <-of-*-and-*-cancel))))
<-of-*-and-*-cancel-arg1-and-arg2theorem
(defthm <-of-*-and-*-cancel-arg1-and-arg2
  (implies (and (< 0 y) (rationalp x1) (rationalp x2) (rationalp y))
    (equal (< (* y x1) (* x2 y)) (< x1 x2)))
  :hints (("Goal" :use <-of-*-and-*-cancel
     :in-theory (disable <-of-*-and-*-cancel))))
<-of-*-and-*-cancel-arg2-and-arg1theorem
(defthm <-of-*-and-*-cancel-arg2-and-arg1
  (implies (and (< 0 y) (rationalp x1) (rationalp x2) (rationalp y))
    (equal (< (* x1 y) (* y x2)) (< x1 x2)))
  :hints (("Goal" :use <-of-*-and-*-cancel
     :in-theory (disable <-of-*-and-*-cancel))))
local
(local (defthm <-of-*-and-*-same-helper
    (implies (and (< x1 x2) (< 0 y) (rationalp y))
      (< (* x1 y) (* x2 y)))
    :hints (("Goal" :cases ((and (rationalp x1) (rationalp x2)) (and (rationalp x1) (complex-rationalp x2))
         (and (rationalp x1) (not (acl2-numberp x2)))
         (and (complex-rationalp x1) (rationalp x2))
         (and (complex-rationalp x1) (complex-rationalp x2))
         (and (rationalp x1) (not (acl2-numberp x2)))
         (and (not (acl2-numberp x1)) (rationalp x2))
         (and (not (acl2-numberp x1)) (complex-rationalp x2))
         (and (not (acl2-numberp x1)) (not (acl2-numberp x2))))
       :use (:instance positive (x (- x1 x2)))
       :in-theory (enable <-when-rationalp-and-complex-rationalp
         <-when-complex-rationalp-and-rationalp
         <-when-complex-rationalp-and-complex-rationalp)))))
local
(local (defthm <=-of-*-and-*-same-helper
    (implies (and (<= x1 x2) (<= 0 y) (rationalp y))
      (<= (* x1 y) (* x2 y)))
    :hints (("Goal" :use <-of-*-and-*-same-helper
       :in-theory (disable <-of-*-and-*-same-helper)
       :cases ((and (rationalp x1) (rationalp x2)) (and (rationalp x1) (complex-rationalp x2))
         (and (rationalp x1) (not (acl2-numberp x2)))
         (and (complex-rationalp x1) (rationalp x2))
         (and (complex-rationalp x1) (complex-rationalp x2))
         (and (rationalp x1) (not (acl2-numberp x2)))
         (and (not (acl2-numberp x1)) (rationalp x2))
         (and (not (acl2-numberp x1)) (complex-rationalp x2))
         (and (not (acl2-numberp x1)) (not (acl2-numberp x2))))))))
<-of-*-and-*-same-forward-1theorem
(defthm <-of-*-and-*-same-forward-1
  (implies (and (< x1 x2) (< 0 y) (rationalp y))
    (< (* x1 y) (* x2 y)))
  :rule-classes ((:forward-chaining :trigger-terms ((* x1 y)))))
<-of-*-and-*-same-forward-2theorem
(defthm <-of-*-and-*-same-forward-2
  (implies (and (< x1 x2) (< 0 y) (rationalp y))
    (< (* x1 y) (* x2 y)))
  :rule-classes ((:forward-chaining :trigger-terms ((* x2 y))))
  :hints (("Goal" :use <-of-*-and-*-same-forward-1)))
<-of-*-and-*-same-forward-3theorem
(defthm <-of-*-and-*-same-forward-3
  (implies (and (< x1 x2) (< 0 y) (rationalp y))
    (< (* y x1) (* y x2)))
  :rule-classes ((:forward-chaining :trigger-terms ((* y x1))))
  :hints (("Goal" :use <-of-*-and-*-same-forward-1)))
<-of-*-and-*-same-forward-4theorem
(defthm <-of-*-and-*-same-forward-4
  (implies (and (< x1 x2) (< 0 y) (rationalp y))
    (< (* y x1) (* y x2)))
  :rule-classes ((:forward-chaining :trigger-terms ((* y x2))))
  :hints (("Goal" :use <-of-*-and-*-same-forward-1)))
<-of-*-and-*-same-linear-1theorem
(defthm <-of-*-and-*-same-linear-1
  (implies (and (< x1 x2) (< 0 y) (rationalp y))
    (< (* x1 y) (* x2 y)))
  :rule-classes ((:linear :trigger-terms ((* x1 y)))))
<-of-*-and-*-same-linear-2theorem
(defthm <-of-*-and-*-same-linear-2
  (implies (and (< x1 x2) (< 0 y) (rationalp y))
    (< (* x1 y) (* x2 y)))
  :rule-classes ((:linear :trigger-terms ((* x2 y))))
  :hints (("Goal" :use <-of-*-and-*-same-linear-1)))
<-of-*-and-*-same-linear-3theorem
(defthm <-of-*-and-*-same-linear-3
  (implies (and (< x1 x2) (< 0 y) (rationalp y))
    (< (* y x1) (* y x2)))
  :rule-classes ((:linear :trigger-terms ((* y x1))))
  :hints (("Goal" :use <-of-*-and-*-same-linear-1)))
<-of-*-and-*-same-linear-4theorem
(defthm <-of-*-and-*-same-linear-4
  (implies (and (< x1 x2) (< 0 y) (rationalp y))
    (< (* y x1) (* y x2)))
  :rule-classes ((:linear :trigger-terms ((* y x2))))
  :hints (("Goal" :use <-of-*-and-*-same-linear-1)))
other
(deftheory <-of-*-and-*-same-linear
  '(<-of-*-and-*-same-linear-1 <-of-*-and-*-same-linear-2
    <-of-*-and-*-same-linear-3
    <-of-*-and-*-same-linear-4)
  :redundant-okp t)
<=-of-*-and-*-same-forward-1theorem
(defthm <=-of-*-and-*-same-forward-1
  (implies (and (<= x1 x2) (<= 0 y) (rationalp y))
    (<= (* x1 y) (* x2 y)))
  :hints (("Goal" :cases ((equal 0 y))))
  :rule-classes ((:forward-chaining :trigger-terms ((* x1 y)))))
<=-of-*-and-*-same-forward-2theorem
(defthm <=-of-*-and-*-same-forward-2
  (implies (and (<= x1 x2) (<= 0 y) (rationalp y))
    (<= (* x1 y) (* x2 y)))
  :rule-classes ((:forward-chaining :trigger-terms ((* x2 y))))
  :hints (("Goal" :use <=-of-*-and-*-same-forward-1)))
<=-of-*-and-*-same-forward-3theorem
(defthm <=-of-*-and-*-same-forward-3
  (implies (and (<= x1 x2) (<= 0 y) (rationalp y))
    (<= (* y x1) (* y x2)))
  :rule-classes ((:forward-chaining :trigger-terms ((* y x1))))
  :hints (("Goal" :use <=-of-*-and-*-same-forward-1)))
<=-of-*-and-*-same-forward-4theorem
(defthm <=-of-*-and-*-same-forward-4
  (implies (and (<= x1 x2) (<= 0 y) (rationalp y))
    (<= (* y x1) (* y x2)))
  :rule-classes ((:forward-chaining :trigger-terms ((* y x2))))
  :hints (("Goal" :use <=-of-*-and-*-same-forward-1)))
<=-of-*-and-*-same-lineartheorem
(defthm <=-of-*-and-*-same-linear
  (implies (and (<= x1 x2) (<= 0 y) (rationalp y))
    (<= (* x1 y) (* x2 y)))
  :rule-classes :linear)
<=-of-*-and-*-same-alt-lineartheorem
(defthm <=-of-*-and-*-same-alt-linear
  (implies (and (<= x1 x2) (<= 0 y) (rationalp y))
    (<= (* y x1) (* y x2)))
  :hints (("Goal" :use <=-of-*-and-*-same-linear
     :in-theory (disable <=-of-*-and-*-same-linear)))
  :rule-classes :linear)
<-of-*-cancel-1theorem
(defthm <-of-*-cancel-1
  (implies (and (< 0 y) (rationalp y) (rationalp x))
    (equal (< y (* x y)) (< 1 x)))
  :hints (("Goal" :use (:instance <-of-*-and-*-cancel (x1 1) (x2 x))
     :in-theory (disable <-of-*-and-*-cancel))))
<-of-*-cancel-2theorem
(defthm <-of-*-cancel-2
  (implies (and (< 0 y) (rationalp y) (rationalp x))
    (equal (< (* x y) y) (< x 1)))
  :hints (("Goal" :use (:instance <-of-*-and-*-cancel (x1 x) (x2 1))
     :in-theory (disable <-of-*-and-*-cancel))))
<-of-*-same-arg2theorem
(defthm <-of-*-same-arg2
  (implies (and (<= 0 x) (rationalp y) (rationalp x))
    (equal (< x (* x y))
      (if (equal x 0)
        nil
        (< 1 y))))
  :hints (("Goal" :use (:instance <-of-*-and-*-cancel (x1 1) (x2 y) (y x))
     :in-theory (disable <-of-*-and-*-cancel))))
<-of-*-same-arg3theorem
(defthm <-of-*-same-arg3
  (implies (and (<= 0 x) (rationalp y) (rationalp x))
    (equal (< (* x y) x)
      (if (equal x 0)
        nil
        (< y 1))))
  :hints (("Goal" :use (:instance <-of-*-and-*-cancel (x1 y) (x2 1) (y x))
     :in-theory (disable <-of-*-and-*-cancel))))
<-of-*-same-linear-specialtheorem
(defthm <-of-*-same-linear-special
  (implies (and (< 1 y) (< 0 x) (rationalp x)) (< x (* x y)))
  :rule-classes :linear :hints (("Goal" :use (:instance <-of-*-and-*-same-forward-1 (x1 1) (x2 y) (y x))
     :in-theory (disable <-of-*-and-*-same-forward-1))))
<-of-*-same-linear-2theorem
(defthm <-of-*-same-linear-2
  (implies (and (<= 1 y) (<= 0 x) (rationalp x))
    (<= x (* x y)))
  :rule-classes :linear)
<-of-*-and-*-lineartheorem
(defthm <-of-*-and-*-linear
  (implies (and (< x1 x2)
      (<= y1 y2)
      (<= 0 x1)
      (< 0 y1)
      (rationalp x2)
      (rationalp y1))
    (< (* x1 y1) (* x2 y2)))
  :rule-classes :linear :hints (("Goal" :use ((:instance <-of-*-and-*-same-linear-1 (y y1)) (:instance <-of-*-and-*-same-linear-1
         (x1 y1)
         (x2 y2)
         (y x2)))
     :in-theory (disable <-of-*-and-*-cancel
       <-of-*-and-*-same-helper
       <-of-*-and-*-same-forward-1
       <-of-*-and-*-same-forward-2))))
<-of-*-and-*theorem
(defthm <-of-*-and-*
  (implies (and (< x1 x2)
      (<= y1 y2)
      (<= 0 x1)
      (<= 0 y1)
      (rationalp x2)
      (rationalp y1))
    (equal (< (* x1 y1) (* x2 y2))
      (if (= 0 y1)
        (< 0 (* x2 y2))
        t)))
  :hints (("Goal" :use ((:instance <-of-*-and-*-same-linear-1 (y y1)) (:instance <-of-*-and-*-same-linear-1
         (x1 y1)
         (x2 y2)
         (y x2)))
     :in-theory (disable <-of-*-and-*-cancel
       <-of-*-and-*-same-helper
       <-of-*-and-*-same-forward-1
       <-of-*-and-*-same-forward-2))))
equal-of-*-and-constanttheorem
(defthm equal-of-*-and-constant
  (implies (and (syntaxp (and (quotep k1) (quotep k2)))
      (acl2-numberp k2)
      (not (equal 0 k2)))
    (equal (equal k1 (* k2 x))
      (and (acl2-numberp k1) (equal (/ k1 k2) (fix x)))))
  :hints (("Goal" :in-theory (disable inverse-of-* associativity-of-*)
     :use ((:instance inverse-of-* (x k2)) (:instance associativity-of-* (x k2) (y (/ k2)) (z x))))))
<-of-constant-and-*-of-constanttheorem
(defthm <-of-constant-and-*-of-constant
  (implies (and (syntaxp (and (quotep k1) (quotep k2)))
      (< 0 k2)
      (rationalp k1)
      (rationalp k2))
    (equal (< k1 (* k2 x)) (< (/ k1 k2) x)))
  :hints (("Goal" :in-theory (disable inverse-of-* associativity-of-*)
     :use ((:instance inverse-of-* (x k2)) (:instance associativity-of-* (x k2) (y (/ k2)) (z x))))))
<-of-*-of-constant-and-constanttheorem
(defthm <-of-*-of-constant-and-constant
  (implies (and (syntaxp (and (quotep k1) (quotep k2)))
      (< 0 k2)
      (rationalp k1)
      (rationalp k2))
    (equal (< (* k2 x) k1) (< x (/ k1 k2))))
  :hints (("Goal" :in-theory (disable inverse-of-* associativity-of-*)
     :use ((:instance inverse-of-* (x k2)) (:instance associativity-of-* (x k2) (y (/ k2)) (z x))))))
<-of---of-*-same-arg1theorem
(defthm <-of---of-*-same-arg1
  (implies (and (rationalp i) (rationalp j))
    (equal (< i (- (* i j)))
      (if (< i 0)
        (< -1 j)
        (if (equal 0 i)
          nil
          (< j -1)))))
  :hints (("Goal" :use (:instance <-of-*-and-*-cancel-gen (y i) (x1 1) (x2 (- j)))
     :in-theory (disable <-of-*-and-*-cancel-gen))))
equal-of-*-cancel-arg1+theorem
(defthm equal-of-*-cancel-arg1+
  (equal (equal (* x y) x)
    (and (acl2-numberp x)
      (if (equal 0 x)
        t
        (equal y 1))))
  :hints (("Goal" :use (:instance equal-of-*-and-*-cancel (z 1))
     :in-theory (disable equal-of-*-and-*-cancel))))
realpart-of-*theorem
(defthm realpart-of-*
  (equal (realpart (* x y))
    (- (* (realpart x) (realpart y))
      (* (imagpart x) (imagpart y))))
  :hints (("Goal" :in-theory (enable complex-opener))))
imagpart-of-*theorem
(defthm imagpart-of-*
  (equal (imagpart (* x y))
    (+ (* (realpart x) (imagpart y))
      (* (imagpart x) (realpart y))))
  :hints (("Goal" :in-theory (enable complex-opener))))