numerator

other

(in-package "ACL2")

local

(local (include-book "denominator"))

local

(local (include-book "../../arithmetic/rationals"))

numerator-when-integerptheorem

(defthm numerator-when-integerp
  (implies (integerp x) (equal (numerator x) x))
  :hints (("Goal" :use (:instance rational-implies2)
     :in-theory (disable rational-implies2))))

equal-of-numerator-sametheorem

(defthm equal-of-numerator-same
  (equal (equal x (numerator x)) (integerp x)))

<-of-numerator-and-0theorem

(defthm <-of-numerator-and-0
  (equal (< (numerator x) 0) (and (rationalp x) (< x 0)))
  :hints (("Goal" :cases ((not (rationalp x)) (and (rationalp x) (< x 0))))))

numerator-of-/-when-integerptheorem

(defthm numerator-of-/-when-integerp
  (implies (integerp x) (equal (numerator (/ x)) (signum x))))

numerator-of--theorem

(defthm numerator-of--
  (equal (numerator (- x)) (- (numerator x))))

local

(local (defthmd not-rationalp-of--
    (implies (and (not (rationalp x)) (complex-rationalp x))
      (not (rationalp (- x))))))

numerator-of-+-of---and--theorem

(defthm numerator-of-+-of---and--
  (equal (numerator (+ (- x) (- y))) (- (numerator (+ x y))))
  :hints (("Goal" :use ((:instance not-rationalp-of-- (x (+ x y))) (:instance numerator-of-- (x (+ x y))))
     :in-theory (disable numerator-of--))))

local

(local (include-book "../../arithmetic/mod-gcd"))

<=-of-numerator-of-*-of-/theorem

(defthm <=-of-numerator-of-*-of-/
  (implies (and (natp i) (posp j))
    (<= (numerator (* i (/ j))) i))
  :hints (("Goal" :use (:instance least-numerator-denominator-<= (n i) (d j))
     :in-theory (disable least-numerator-denominator-<=))))

numerator-of-*-of---arg2theorem

(defthm numerator-of-*-of---arg2
  (equal (numerator (* x (- y))) (- (numerator (* x y))))
  :hints (("Goal" :use (:instance numerator-of-- (x (* x y)))
     :in-theory (disable numerator-of--))))

Included Books