numerator-and-denominator

other

(in-package "ACL2")

local

(local (include-book "../pass1/top"))

rational-implies2theorem

(defthm rational-implies2
  (implies (rationalp x)
    (equal (* (/ (denominator x)) (numerator x)) x)))

local

(local (in-theory (enable rewrite-linear-equalities-to-iff)))

numerator-positivetheorem

(defthm numerator-positive
  (implies (rationalp x) (equal (< 0 (numerator x)) (< 0 x)))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (rationalp x) (< 0 x)) (< 0 (numerator x))))
    (:type-prescription :corollary (implies (and (rationalp x) (<= 0 x)) (<= 0 (numerator x))))))

numerator-negativetheorem

(defthm numerator-negative
  (implies (rationalp x) (equal (< (numerator x) 0) (< x 0)))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (rationalp x) (< x 0)) (< (numerator x) 0)))
    (:type-prescription :corollary (implies (and (rationalp x) (<= x 0)) (<= (numerator x) 0)))))

numerator-minustheorem

(defthm numerator-minus
  (equal (numerator (- i)) (- (numerator i))))

denominator-minustheorem

(defthm denominator-minus
  (implies (rationalp x)
    (equal (denominator (- x)) (denominator x))))

integerp==>numerator-=-xtheorem

(defthm integerp==>numerator-=-x
  (implies (integerp x) (equal (numerator x) x)))

integerp==>denominator-=-1theorem

(defthm integerp==>denominator-=-1
  (implies (integerp x) (equal (denominator x) 1)))

equal-denominator-1theorem

(defthm equal-denominator-1
  (equal (equal (denominator x) 1)
    (or (integerp x) (not (rationalp x)))))

*-r-denominator-rtheorem

(defthm *-r-denominator-r
  (equal (* r (denominator r))
    (if (rationalp r)
      (numerator r)
      (fix r))))

numerator-and-denominator

Included Books