arith2

other

(in-package "ACL2")

include-book

(include-book "fp2")

include-book

(include-book "predicate")

include-book

(include-book "product")

include-book

(include-book "../../../meta/meta-times-equal")

include-book

(include-book "../../../meta/meta-plus-equal")

include-book

(include-book "../../../meta/meta-plus-lessp")

collect-constants-in-equal-of-sumstheorem

(defthm collect-constants-in-equal-of-sums
  (implies (and (syntaxp (and (quotep c1) (quotep c2)))
      (case-split (acl2-numberp c1)))
    (and (equal (equal (+ c2 x) c1) (equal (fix x) (- c1 c2)))
      (equal (equal c1 (+ c2 x)) (equal (fix x) (- c1 c2))))))

collect-constants-in-equal-of-sums-2theorem

(defthm collect-constants-in-equal-of-sums-2
  (implies (syntaxp (and (quotep c1) (quotep c2)))
    (and (equal (equal (+ c2 x) (+ c1 y))
        (equal (fix x) (+ (- c1 c2) y))))))

collect-constants-in-<-of-sumstheorem

(defthm collect-constants-in-<-of-sums
  (implies (syntaxp (and (quotep c1) (quotep c2)))
    (and (equal (< (+ c2 x) c1) (< x (- c1 c2)))
      (equal (< c1 (+ c2 x)) (< (- c1 c2) x)))))

collect-constants-in-<-of-sums-2theorem

(defthm collect-constants-in-<-of-sums-2
  (implies (syntaxp (and (quotep c1) (quotep c2)))
    (equal (< (+ c2 x) (+ c1 y)) (< x (+ (- c1 c2) y)))))

mult-both-sides-of-<-by-positivetheorem

(defthmd mult-both-sides-of-<-by-positive
  (implies (and (<= 0 c) (rationalp c) (case-split (< 0 c)))
    (equal (< (* c a) (* c b)) (< a b))))

include-book

(include-book "../../../meta/meta-times-equal")

include-book

(include-book "../../../meta/meta-plus-equal")

include-book

(include-book "../../../meta/meta-plus-lessp")

mult-both-sides-of-equaltheorem

(defthm mult-both-sides-of-equal
  (implies (and (case-split (acl2-numberp a))
      (case-split (acl2-numberp b))
      (case-split (acl2-numberp c)))
    (equal (equal (* a c) (* b c))
      (if (equal c 0)
        t
        (equal a b))))
  :rule-classes nil)

rearr-neg-erictheorem

(defthm rearr-neg-eric
  (implies (and (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp d))
    (equal (equal (+ a (* -1 b) c) d) (equal (+ a c) (+ b d)))))

collect-constants-with-divisiontheorem

(defthm collect-constants-with-division
  (implies (and (syntaxp (and (quotep c1) (quotep c2)))
      (rationalp c2)
      (acl2-numberp c1)
      (not (equal c2 0))
      (rationalp x))
    (equal (equal c1 (* c2 x)) (equal (/ c1 c2) x))))

cancel-in-prods-<-case-x->-0theorem

(defthmd cancel-in-prods-<-case-x->-0
  (implies (and (rationalp x) (< 0 x) (rationalp a) (rationalp b))
    (equal (< (* x a) (* x b)) (< a b))))

cancel-in-prods-<-case-x-<-0theorem

(defthmd cancel-in-prods-<-case-x-<-0
  (implies (and (rationalp x) (> 0 x) (rationalp a) (rationalp b))
    (equal (< (* x a) (* x b)) (> a b))))

cancel-in-prods-<theorem

(defthmd cancel-in-prods-<
  (implies (and (rationalp a) (rationalp b) (rationalp c))
    (equal (< (* a b) (* a c))
      (if (equal 0 a)
        nil
        (if (> a 0)
          (< b c)
          (> b c)))))
  :hints (("Goal" :in-theory (enable cancel-in-prods-<-case-x-<-0
       cancel-in-prods-<-case-x->-0))))

move-a-negative-coefftheorem

(defthmd move-a-negative-coeff
  (equal (< (+ a (* -1 b)) c) (< a (+ b c))))

rearr-negative-coeffs-<-sums-blahtheorem

(defthm rearr-negative-coeffs-<-sums-blah
  (equal (< (+ a e (* -1 c)) b) (< (+ a e) (+ (* c) b)))
  :hints (("Goal" :use (:instance move-a-negative-coeff
       (a (+ a e))
       (b (* c))
       (c b)))))

collect-constant-mults-<-1-of-2-with-1-of-2-term-len-2theorem

(defthm collect-constant-mults-<-1-of-2-with-1-of-2-term-len-2
  (implies (and (syntaxp (and (quotep c1) (quotep c2)))
      (rationalp c1)
      (rationalp c2)
      (rationalp a)
      (rationalp b)
      (rationalp c)
      (rationalp d))
    (equal (< (+ (* c1 c d) a) (+ (* c2 c d) b))
      (< (+ (* (- c1 c2) c d) a) b))))

include-book

(include-book "inverted-factor")

<-transitivetheorem

(defthm <-transitive
  (implies (and (< a b) (< b c)) (< a c))
  :rule-classes nil)

<=-transitivetheorem

(defthm <=-transitive
  (implies (and (<= a b) (<= b c)) (<= a c))
  :rule-classes nil)

<-and-<=-transitivitytheorem

(defthm <-and-<=-transitivity
  (implies (and (< a b) (<= b c)) (< a c))
  :rule-classes nil)

<=-and-<-transitivitytheorem

(defthm <=-and-<-transitivity
  (implies (and (< a b) (<= b c)) (< a c))
  :rule-classes nil)

equal-transitivetheorem

(defthm equal-transitive
  (implies (and (equal a b) (equal b c)) (equal a c))
  :rule-classes nil)

collect-againtheorem

(defthm collect-again
  (implies (and (syntaxp (quotep k)) (rationalp x) (rationalp y))
    (equal (< (+ x y) (* k x)) (< y (* (- k 1) x)))))

natpfunction

(defun natp
  (x)
  (declare (xargs :guard t))
  (and (integerp x) (<= 0 x)))

in-theory

(in-theory (enable natp))

two-natps-add-to-1theorem

(defthm two-natps-add-to-1
  (implies (and (natp n) (natp x))
    (equal (equal 1 (+ x n))
      (or (and (equal x 1) (equal n 0))
        (and (equal x 0) (equal n 1))))))

nonneg-+theorem

(defthm nonneg-+
  (implies (and (<= 0 x) (<= 0 y)) (not (< (+ x y) 0))))

nonneg-+-typetheorem

(defthm nonneg-+-type
  (implies (and (<= 0 x) (<= 0 y)) (not (< (+ x y) 0)))
  :rule-classes (:type-prescription))

move-negative-constant-1theorem

(defthm move-negative-constant-1
  (implies (and (syntaxp (and (quotep k) (< (cadr k) 0)))
      (acl2-numberp x)
      (acl2-numberp y))
    (equal (equal x (+ k y)) (equal (+ x (- k)) y))))

rationalp-sumtheorem

(defthm rationalp-sum
  (implies (rationalp k)
    (and (equal (rationalp (+ k x)) (not (complex-rationalp x)))
      (equal (rationalp (+ x k)) (not (complex-rationalp x))))))

rationalp-prodtheorem

(defthm rationalp-prod
  (implies (and (rationalp k) (case-split (not (equal k 0))))
    (and (equal (rationalp (* k x)) (not (complex-rationalp x)))
      (equal (rationalp (* x k)) (not (complex-rationalp x))))))

complex-rationalp-prodtheorem

(defthm complex-rationalp-prod
  (implies (and (rationalp k) (case-split (not (equal k 0))))
    (and (equal (complex-rationalp (* k x)) (complex-rationalp x))
      (equal (complex-rationalp (* x k)) (complex-rationalp x)))))

collect-1theorem

(defthm collect-1
  (implies (and (syntaxp (and (quotep k) (quotep j)))
      (rationalp k)
      (rationalp j)
      (rationalp x)
      (rationalp y))
    (equal (< (+ y (* k x)) (* j x)) (< (+ (* (- k j) x) y) 0))))

collect-2theorem

(defthm collect-2
  (implies (and (syntaxp (and (quotep k) (quotep j)))
      (rationalp k)
      (rationalp j)
      (rationalp x)
      (rationalp y))
    (equal (< (+ (* k x) y) (* j x)) (< (+ (* (- k j) x) y) 0))))

collect-anothertheorem

(defthm collect-another
  (implies (and (syntaxp (and (quotep k) (quotep j)))
      (rationalp k)
      (rationalp j)
      (rationalp x)
      (rationalp y)
      (rationalp z))
    (equal (< (+ (* k x) y) (+ (* j x) z))
      (< (+ (* (- k j) x) y) z))))

collect-in-<-of-sums-2theorem

(defthm collect-in-<-of-sums-2
  (implies (syntaxp (and (quotep k) (quotep j)))
    (equal (< (+ a (* k x) d) (+ b e (* j x) f))
      (< (+ a d) (+ b e (* (- j k) x) f)))))

collect-in-<-of-sums-1theorem

(defthm collect-in-<-of-sums-1
  (implies (syntaxp (and (quotep k) (quotep j)))
    (equal (< (+ a d (* k x) y) (+ b e f z (* j x) g))
      (< (+ a d y) (+ b e f z (* (- j k) x) g)))))

cancel-in-sum-equal-zero-1theorem

(defthm cancel-in-sum-equal-zero-1
  (implies (and (rationalp y)
      (case-split (not (equal 0 y)))
      (rationalp x1)
      (rationalp x2)
      (rationalp x3)
      (rationalp x4)
      (rationalp x5)
      (rationalp x6))
    (equal (equal 0 (+ (* y x1) (* x2 y x3) (* y x4) (* x5 y x6)))
      (equal 0 (+ x1 (* x2 x3) x4 (* x5 x6)))))
  :hints (("Goal" :in-theory (disable product-equal-zero)
     :use (:instance product-equal-zero
       (x y)
       (y (+ x1 (* x2 x3) x4 (* x5 x6)))))))

integerp-implies-not-complex-rationalptheorem

(defthm integerp-implies-not-complex-rationalp
  (implies (integerp x) (not (complex-rationalp x))))

<-of-two-inversestheorem

(defthm <-of-two-inverses
  (implies (and (rationalp x) (rationalp y) (< 0 y) (< 0 x))
    (equal (< (/ x) (/ y)) (< y x))))

Included Books