denominator - ACL2 Book

Included Books

other

(in-package "ACL2")

local

(local (include-book "ground-zero"))

local

(local (include-book "fp2"))

denominator-positive-integer-type-prescriptiontheorem

(defthm denominator-positive-integer-type-prescription
  (and (< 0 (denominator x)) (integerp (denominator x)))
  :rule-classes (:type-prescription))

denominator-positivetheorem

(defthm denominator-positive
  (< 0 (denominator x))
  :rule-classes (:rewrite :linear))

denominator-integerptheorem

(defthm denominator-integerp (integerp (denominator x)))

denominator-one-means-integertheorem

(defthm denominator-one-means-integer
  (implies (case-split (rationalp x))
    (equal (equal (denominator x) 1) (integerp x)))
  :hints (("goal" :in-theory (disable rational-implies2)
     :use (rational-implies2 (:instance lowest-terms (n (denominator x)) (r x) (q 1))))))

denominator-of-integer-is-onetheorem

(defthm denominator-of-integer-is-one
  (implies (integerp x) (equal (denominator x) 1)))

denominator-lower-boundencapsulate

(encapsulate nil
  (local (include-book "../../../arithmetic/mod-gcd"))
  (defthm denominator-lower-bound
    (implies (and (< 0 q) (integerp p) (integerp q))
      (<= (denominator (* p (/ q))) q))
    :hints (("goal" :use (:instance least-numerator-denominator-<= (n p) (d q))))))