denominator - ACL2 Book

Included Books

other

(in-package "ACL2")

local

(local (include-book "../../arithmetic/rationals"))

denominator-when-integerptheorem

(defthm denominator-when-integerp
  (implies (integerp x) (equal (denominator x) 1))
  :hints (("Goal" :in-theory (enable numerator))))

equal-of-1-and-denominatortheorem

(defthm equal-of-1-and-denominator
  (equal (equal 1 (denominator x)) (integerp (rfix x))))

denominator-of-/-when-integerptheorem

(defthm denominator-of-/-when-integerp
  (implies (integerp x)
    (equal (denominator (/ x))
      (if (equal x 0)
        1
        (abs x))))
  :hints (("Goal" :use ((:instance rational-implies2 (x (/ x))) numerator-/x)
     :in-theory (disable numerator-/x
       rational-implies2
       *-r-denominator-r
       numerator-when-integerp))))

denominator-of--theorem

(defthm denominator-of--
  (equal (denominator (- x))
    (if (rationalp x)
      (denominator x)
      1)))

denominator-of-+-of---and--theorem

(defthm denominator-of-+-of---and--
  (equal (denominator (+ (- x) (- y))) (denominator (+ x y)))
  :hints (("Goal" :use (:instance denominator-of-- (x (+ x y)))
     :in-theory (disable denominator-of--))))

local

(local (include-book "../../arithmetic/mod-gcd"))

<=-of-denominator-of-*-of-/theorem

(defthm <=-of-denominator-of-*-of-/
  (implies (and (integerp i) (posp j))
    (<= (denominator (* i (/ j))) j))
  :hints (("Goal" :use (:instance least-numerator-denominator-<= (n i) (d j))
     :in-theory (disable least-numerator-denominator-<=))))

denominator-of-*-of---arg2theorem

(defthm denominator-of-*-of---arg2
  (equal (denominator (* x (- y))) (denominator (* x y)))
  :hints (("Goal" :use (:instance denominator-of-- (x (* x y)))
     :in-theory (disable denominator-of--))))