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-rtheorem

(defthm *-r-denominator-r
  (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-/))))