nonnegative-integer-quotient

Included Books

times times-and-divide plus numerator denominator

other

(in-package "ACL2")

local

(local (include-book "times"))

local

(local (include-book "times-and-divide"))

local

(local (include-book "plus"))

local

(local (include-book "numerator"))

local

(local (include-book "denominator"))

in-theory

(in-theory (disable nonnegative-integer-quotient))

*-of-/-and---sametheorem

(defthm *-of-/-and---same
  (equal (* (/ y) (- y))
    (if (equal (fix y) 0)
      0
      -1))
  :hints (("Goal" :in-theory (e/d (--becomes-*-of--1) (*-of--1)))))

local

(local (defthmd integerp-squeeze
    (implies (and (< 0 x) (< x 1)) (not (integerp x)))))

local

(local (defun nonnegative-integer-quotient-double-induct
    (i1 i2 j)
    (if (or (= (nfix j) 0) (< (ifix i1) j))
      (list i1 i2 j)
      (+ 1
        (nonnegative-integer-quotient-double-induct (- i1 j)
          (- i2 j)
          j)))))

nonnegative-integer-quotient-weak-monotonetheorem

(defthm nonnegative-integer-quotient-weak-monotone
  (implies (and (<= i1 i2) (integerp i1) (integerp i2))
    (<= (nonnegative-integer-quotient i1 j)
      (nonnegative-integer-quotient i2 j)))
  :hints (("Goal" :induct (nonnegative-integer-quotient-double-induct i1 i2 j)
     :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-upper-bound-lineartheorem

(defthm nonnegative-integer-quotient-upper-bound-linear
  (implies (and (integerp i) (<= 0 i) (integerp j) (<= 0 j))
    (<= (nonnegative-integer-quotient i j) (/ i j)))
  :rule-classes ((:linear :trigger-terms ((nonnegative-integer-quotient i j))))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-upper-bound-linear-stricttheorem

(defthm nonnegative-integer-quotient-upper-bound-linear-strict
  (implies (and (not (integerp (/ i j)))
      (integerp i)
      (<= 0 i)
      (integerp j)
      (<= 0 j))
    (< (nonnegative-integer-quotient i j) (/ i j)))
  :rule-classes ((:linear :trigger-terms ((nonnegative-integer-quotient i j))))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-of-+-of---sametheorem

(defthmd nonnegative-integer-quotient-of-+-of---same
  (implies (and (<= j i) (integerp i) (posp j))
    (equal (nonnegative-integer-quotient (+ i (- j)) j)
      (+ -1 (nonnegative-integer-quotient i j))))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-of-0-arg1theorem

(defthm nonnegative-integer-quotient-of-0-arg1
  (equal (nonnegative-integer-quotient 0 j) 0)
  :hints (("Goal" :expand (nonnegative-integer-quotient 0 j)
     :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-of-0-arg2theorem

(defthm nonnegative-integer-quotient-of-0-arg2
  (equal (nonnegative-integer-quotient i 0) 0)
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

equal-of-nonnegative-integer-quotient-and-0theorem

(defthm equal-of-nonnegative-integer-quotient-and-0
  (implies (and (natp i) (natp j))
    (equal (equal (nonnegative-integer-quotient i j) 0)
      (if (equal 0 j)
        t
        (< i j))))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

local

(local (defun nonnegative-integer-quotient-double-double-induct
    (i1 i2 j1 j2)
    (if (or (= (nfix j2) 0) (< (ifix i2) j2))
      (list i1 i2 j1 j2)
      (+ 1
        (nonnegative-integer-quotient-double-double-induct (- i1 j1)
          (- i2 j2)
          j1
          j2)))))

nonnegative-integer-quotient-weak-monotone-gentheorem

(defthm nonnegative-integer-quotient-weak-monotone-gen
  (implies (and (<= i1 i2)
      (<= j2 j1)
      (integerp i1)
      (integerp i2)
      (integerp j1)
      (posp j2))
    (<= (nonnegative-integer-quotient i1 j1)
      (nonnegative-integer-quotient i2 j2)))
  :hints (("Goal" :induct (nonnegative-integer-quotient-double-double-induct i1
       i2
       j1
       j2)
     :expand (nonnegative-integer-quotient i2 j2)
     :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-weak-monotone-arg2theorem

(defthm nonnegative-integer-quotient-weak-monotone-arg2
  (implies (and (<= j1 j2) (integerp i) (posp j1) (integerp j2))
    (<= (nonnegative-integer-quotient i j2)
      (nonnegative-integer-quotient i j1)))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-lower-bound-linear2theorem

(defthm nonnegative-integer-quotient-lower-bound-linear2
  (implies (and (integerp i) (natp j))
    (<= (+ -1 (/ j) (/ i j)) (nonnegative-integer-quotient i j)))
  :rule-classes ((:linear :trigger-terms ((nonnegative-integer-quotient i j))))
  :hints (("subgoal *1/1" :use (:instance <-of-*-and-*-cancel
       (x1 0)
       (x2 (+ -1 (/ j) (* i (/ j))))
       (y j))) ("Goal" :in-theory (e/d (nonnegative-integer-quotient nonnegative-integer-quotient-of-+-of---same)
        (<-of-*-and-*-cancel)))))

nonnegative-integer-quotient-of-1-arg2theorem

(defthm nonnegative-integer-quotient-of-1-arg2
  (implies (natp i)
    (equal (nonnegative-integer-quotient i 1) i))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-when-not-natp-arg1theorem

(defthm nonnegative-integer-quotient-when-not-natp-arg1
  (implies (not (natp i))
    (equal (nonnegative-integer-quotient i j) 0))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-when-<theorem

(defthm nonnegative-integer-quotient-when-<
  (implies (and (< i j) (natp i) (integerp j))
    (equal (nonnegative-integer-quotient i j) 0))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

<=-of-nonnegative-integer-quotient-of-numerator-and-denominator-sametheorem

(defthm <=-of-nonnegative-integer-quotient-of-numerator-and-denominator-same
  (implies (<= 0 x)
    (<= (nonnegative-integer-quotient (numerator x) (denominator x))
      x))
  :hints (("Goal" :cases ((rationalp x)))))

<=-of---of-nonnegative-integer-quotient-of---of-numerator-and-denominator-sametheorem

(defthm <=-of---of-nonnegative-integer-quotient-of---of-numerator-and-denominator-same
  (implies (<= x 0)
    (<= x
      (- (nonnegative-integer-quotient (- (numerator x))
          (denominator x)))))
  :hints (("Goal" :use (:instance <=-of-nonnegative-integer-quotient-of-numerator-and-denominator-same
       (x (- x)))
     :in-theory (disable <=-of-nonnegative-integer-quotient-of-numerator-and-denominator-same))))

nonnegative-integer-quotient-when-equal-of-quotientstheorem

(defthmd nonnegative-integer-quotient-when-equal-of-quotients
  (implies (and (equal (/ i1 j1) (/ i2 j2))
      (integerp i1)
      (integerp i2)
      (integerp j1)
      (integerp j2)
      (< 0 j1)
      (< 0 j2))
    (equal (nonnegative-integer-quotient i1 j1)
      (nonnegative-integer-quotient i2 j2)))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-when-multipletheorem

(defthm nonnegative-integer-quotient-when-multiple
  (implies (and (integerp (/ i j)) (natp i) (posp j))
    (equal (nonnegative-integer-quotient i j) (/ i j)))
  :hints (("Goal" :in-theory (enable nonnegative-integer-quotient))))

nonnegative-integer-quotient-of-2theorem

(defthmd nonnegative-integer-quotient-of-2
  (implies (natp i)
    (equal (nonnegative-integer-quotient i 2)
      (if (evenp i)
        (/ i 2)
        (+ -1/2 (/ i 2)))))
  :hints (("Subgoal *1/1" :cases ((equal 1 i))) ("Goal" :in-theory (enable nonnegative-integer-quotient))))