numerator-and-denominator

Included Books

basic-arithmetic inequalities prefer-times non-linear num-and-denom-helper

other

(in-package "ACL2")

local

(local (include-book "basic-arithmetic"))

local

(local (include-book "inequalities"))

local

(local (include-book "prefer-times"))

local

(local (include-book "non-linear"))

local

(local (include-book "num-and-denom-helper"))

numerator-minustheorem

(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)))))))

denominator-minustheorem

(defthm denominator-minus
  (implies (rationalp x)
    (equal (denominator (- x)) (denominator x)))
  :hints (("Goal" :use (:instance unique-rationalp
       (d (denominator x))
       (n (- (numerator x)))))))

numerator-when-integerpencapsulate

(encapsulate nil
  (local (defthm numerator-integerp-lemma-1
      (implies (rationalp x)
        (equal (* (* (numerator x) (/ (denominator x))) (denominator x))
          (numerator x)))
      :rule-classes nil
      :hints (("Goal" :in-theory (disable rational-implies2)))))
  (local (defthm numerator-integerp-lemma
      (implies (and (rationalp x)
          (equal (* (numerator x) (/ (denominator x))) x))
        (equal (numerator x) (* x (denominator x))))
      :rule-classes nil
      :hints (("Goal" :use (numerator-integerp-lemma-1)
         :in-theory (disable rational-implies2)) ("Goal'" :in-theory (e/d (prefer-*-to-/) (rational-implies2))))))
  (defthm numerator-when-integerp
    (implies (integerp x) (equal (numerator x) x))
    :hints (("Goal" :in-theory (disable rational-implies2)
       :use ((:instance lowest-terms (r x) (q 1) (n (denominator x))) rational-implies2
         numerator-integerp-lemma)))))

integerp==>denominator=1theorem

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

equal-denominator-1theorem

(defthm equal-denominator-1
  (equal (equal (denominator x) 1)
    (or (integerp x) (not (rationalp x))))
  :hints (("Goal" :use (rational-implies2 completion-of-denominator)
     :in-theory (disable rational-implies2))))

*-r-denominator-r-pass1theorem

(defthm *-r-denominator-r-pass1
  (equal (* r (denominator r))
    (if (rationalp r)
      (numerator r)
      (fix r)))
  :hints (("Goal" :use ((:instance rational-implies2 (x r)))
     :in-theory (disable rational-implies2)) ("Goal''" :in-theory (enable prefer-*-to-/))))

numerator-goes-down-by-integer-division-pass1theorem

(defthm numerator-goes-down-by-integer-division-pass1
  (implies (and (integerp x) (< 0 x) (rationalp r))
    (<= (abs (numerator (* (/ x) r))) (abs (numerator r))))
  :hints (("Goal" :use (:instance least-numerator-denominator-<=
       (n (numerator r))
       (d (* x (denominator r)))))))

denominator-lower-bound-pass1theorem

(defthm denominator-lower-bound-pass1
  (implies (and (integerp x) (integerp y) (< 0 y))
    (<= (denominator (* x (/ y))) y))
  :hints (("goal" :use (:instance least-numerator-denominator-<= (n x) (d y)))))

denominator-plus-pass1theorem

(defthm denominator-plus-pass1
  (implies (and (rationalp r) (integerp x))
    (equal (denominator (+ r x)) (denominator r)))
  :hints (("Goal" :use ((:instance unique-rationalp
        (d (denominator r))
        (n (+ (numerator r) (* x (denominator r))))) (:instance nonneg-int-gcd-abs
         (x (numerator r))
         (j x)
         (n (denominator r)))))))