numerator-and-denominator

(in-package "ACL2")

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

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

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

(defthm numerator-zero
  (implies (rationalp x)
    (equal (equal (numerator x) 0) (equal x 0)))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (equal x 0) (equal (numerator x) 0)))))

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

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

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

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

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

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

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

(defthm |(* r (denominator r))|
  (implies (rationalp r)
    (equal (* r (denominator r)) (numerator r))))

(defthm /r-when-abs-numerator=1
  (and (implies (equal (numerator r) 1)
      (equal (/ r) (denominator r)))
    (implies (equal (numerator r) -1)
      (equal (/ r) (- (denominator r)))))
  :hints (("Goal" :use ((:instance rational-implies2 (x r)))
     :in-theory (disable rational-implies2))))

(in-theory (disable /r-when-abs-numerator=1))

(defthm |(equal (/ r) (denominator r))|
  (implies (rationalp r)
    (equal (equal (/ r) (denominator r))
      (equal (numerator r) 1))))

(defthm |(equal (/ r) (- (denominator r)))|
  (implies (rationalp r)
    (equal (equal (/ r) (- (denominator r)))
      (equal (numerator r) -1))))

(defthm numerator-goes-down-by-integer-division-linear
  (implies (and (integerp x) (< 0 x) (rationalp r))
    (<= (abs (numerator (* (/ x) r))) (abs (numerator r))))
  :hints (("Goal" :use numerator-goes-down-by-integer-division-pass1))
  :rule-classes ((:linear :corollary (implies (and (integerp x) (< 0 x) (rationalp r) (<= 0 r))
       (<= (numerator (* (/ x) r)) (numerator r)))) (:linear :corollary (implies (and (integerp x) (< 0 x) (rationalp r) (<= 0 r))
        (<= (numerator (* r (/ x))) (numerator r))))
    (:linear :corollary (implies (and (integerp x) (< 0 x) (rationalp r) (<= r 0))
        (<= (numerator r) (numerator (* (/ x) r)))))
    (:linear :corollary (implies (and (integerp x) (< 0 x) (rationalp r) (<= r 0))
        (<= (numerator r) (numerator (* r (/ x))))))))

(defthm denominator-bound
  (implies (and (integerp x) (integerp y) (< 0 y))
    (<= (denominator (* x (/ y))) y))
  :rule-classes ((:linear :corollary (implies (and (integerp x) (integerp y) (< 0 y))
       (<= (denominator (* x (/ y))) y))) (:linear :corollary (implies (and (integerp x) (integerp y) (< 0 y))
        (<= (denominator (* (/ y) x)) y)))))

(defthm |(denominator (+ x r))|
  (and (implies (and (rationalp r) (integerp x))
      (equal (denominator (+ x r)) (denominator r)))
    (implies (and (rationalp r) (integerp x))
      (equal (denominator (+ r x)) (denominator r)))))