numerator-and-denominator

other

(in-package "ACL2")

local

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

|(* (/ (denominator x)) (numerator x))|theorem

(defthm |(* (/ (denominator x)) (numerator x))|
  (implies (rationalp x)
    (equal (* (/ (denominator x)) (numerator x)) x)))

local

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

|(< 0 (numerator x))|theorem

(defthm |(< 0 (numerator x))|
  (implies (rationalp x) (equal (< 0 (numerator x)) (< 0 x))))

numerator-type-prescription-positivetheorem

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

numerator-type-prescription-non-negativetheorem

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

|(< (numerator x) 0)|theorem

(defthm |(< (numerator x) 0)|
  (implies (rationalp x) (equal (< (numerator x) 0) (< x 0))))

numerator-type-prescription-negativetheorem

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

numerator-type-prescription-non-positivetheorem

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

|(numerator (- i))|theorem

(defthm |(numerator (- i))|
  (equal (numerator (- i)) (- (numerator i))))

|(denominator (- x))|theorem

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

|integerp x in (numerator x)|theorem

(defthm |integerp x in (numerator x)|
  (implies (integerp x) (equal (numerator x) x)))

|integerp x in (denominator x)|theorem

(defthm |integerp x in (denominator x)|
  (implies (integerp x) (equal (denominator x) 1)))

|(equal (denominator x) 1)|theorem

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

|(* r (denominator r))|theorem

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

Included Books