rationals

(in-package "ACL2")

(defsection more-rational-identities
  :parents (arithmetic-1 numerator denominator)
  :short "Rules about @(see numerator) and @(see denominator) in the
@('arithmetic/rationals') book."
  (defthm denominator-unary-minus
    (implies (rationalp x)
      (equal (denominator (- x)) (denominator x)))
    :hints (("Goal" :use (:instance unique-rationalp
         (d (denominator x))
         (n (- (numerator x)))))))
  (defthm numerator-goes-down-by-integer-division
    (implies (and (integerp x) (< 0 x) (rationalp r))
      (<= (abs (numerator (* (/ x) r))) (abs (numerator r))))
    :rule-classes ((:linear :corollary (implies (and (integerp x) (< 0 x) (rationalp r) (>= r 0))
         (<= (numerator (* (/ x) r)) (numerator r)))) (:linear :corollary (implies (and (integerp x) (< 0 x) (rationalp r) (<= r 0))
          (<= (numerator r) (numerator (* (/ x) r))))))
    :hints (("Goal" :use (:instance least-numerator-denominator-<=
         (n (numerator r))
         (d (* x (denominator r)))))))
  (defthm denominator-plus
    (implies (and (rationalp r) (integerp i))
      (equal (denominator (+ i r)) (denominator r)))
    :hints (("Goal" :use ((:instance unique-rationalp
          (d (denominator r))
          (n (+ (numerator r) (* i (denominator r))))) (:instance nonneg-int-gcd-abs
           (x (numerator r))
           (j i)
           (n (denominator r)))))))
  (defthm numerator-minus
    (equal (numerator (- i)) (- (numerator i)))
    :hints (("Goal" :cases ((rationalp i))) ("Subgoal 1" :use (:instance unique-rationalp
          (d (denominator i))
          (n (- (numerator i)))))))
  (defthm numerator-/x
    (implies (and (integerp x) (not (equal x 0)))
      (equal (numerator (/ x)) (signum x)))
    :hints (("Goal" :use (:instance unique-rationalp (n (signum x)) (d (abs x)))))))