cg - ACL2 Book

other

(in-package "ACL2")

local

(local (include-book "fl"))

local

(local (include-book "fp2"))

local

(local (include-book "integerp"))

local

(local (include-book "integerp"))

local

(local (include-book "arith2"))

local

(local (include-book "common-factor"))

flfunction

(defund fl
  (x)
  (declare (xargs :guard (real/rationalp x)))
  (floor x 1))

cgfunction

(defund cg
  (x)
  (declare (xargs :guard (real/rationalp x)))
  (- (fl (- x))))

cg-def-lineartheorem

(defthm cg-def-linear
  (implies (case-split (rationalp x))
    (and (>= (cg x) x) (> (1+ x) (cg x))))
  :hints (("Goal" :in-theory (enable cg)))
  :rule-classes :linear)

cg-monotone-lineartheorem

(defthm cg-monotone-linear
  (implies (and (rationalp x) (rationalp y) (<= x y))
    (<= (cg x) (cg y)))
  :rule-classes :linear)

n>=cg-lineartheorem

(defthm n>=cg-linear
  (implies (and (>= n x) (rationalp x) (integerp n))
    (>= n (cg x)))
  :rule-classes :linear)

cg+int-rewritetheorem

(defthm cg+int-rewrite
  (implies (and (integerp n) (rationalp x))
    (equal (cg (+ x n)) (+ (cg x) n))))

local

(local (defthm cg/int-1
    (implies (and (rationalp x) (integerp n) (> n 0))
      (>= (cg (/ (cg x) n)) (cg (/ x n))))
    :rule-classes nil
    :hints (("Goal" :use ((:instance cg-def-linear) (:instance cg-monotone-linear (x (/ x n)) (y (/ (cg x) n))))))))

local

(local (defthm cg/int-2
    (implies (and (rationalp x) (integerp n) (> n 0))
      (<= (cg (/ (cg x) n)) (cg (/ x n))))
    :rule-classes nil
    :hints (("Goal" :use ((:instance n>=cg-linear (n (* n (cg (/ x n))))) (:instance n>=cg-linear (n (cg (/ x n))) (x (/ (cg x) n)))
         (:instance cg-def-linear (x (/ x n))))))))

cg/int-rewritetheorem

(defthm cg/int-rewrite
  (implies (and (integerp n) (> n 0) (rationalp x))
    (equal (cg (* (cg x) (/ n))) (cg (/ x n))))
  :hints (("Goal" :use ((:instance cg/int-1) (:instance cg/int-2)))))

cg/int-rewrite-alttheorem

(defthm cg/int-rewrite-alt
  (implies (and (integerp n) (> n 0) (rationalp x))
    (equal (cg (* (/ n) (cg x))) (cg (/ x n))))
  :hints (("Goal" :use ((:instance cg/int-1) (:instance cg/int-2)))))

int-cg-rulestheorem

(defthm int-cg-rules
  (implies (rationalp x) (integerp (cg x)))
  :rule-classes (:rewrite :type-prescription))

cg-inttheorem

(defthm cg-int (implies (integerp x) (equal (cg x) x)))

cg-integerptheorem

(defthm cg-integerp
  (implies (rationalp x)
    (equal (equal (cg x) x) (integerp x))))

cg-uniquetheorem

(defthm cg-unique
  (implies (and (rationalp x) (integerp n) (>= n x) (> (1+ x) n))
    (equal (cg x) n))
  :rule-classes nil)

fl-cgtheorem

(defthm fl-cg
  (implies (rationalp x)
    (equal (cg x)
      (if (integerp x)
        (fl x)
        (1+ (fl x)))))
  :rule-classes nil)

cg-integer-typetheorem

(defthm cg-integer-type
  (integerp (cg x))
  :rule-classes (:type-prescription))

cg-deftheorem

(defthmd cg-def
  (and (integerp (cg x))
    (implies (case-split (rationalp x))
      (and (>= (cg x) x) (> (1+ x) (cg x)))))
  :rule-classes ((:linear :corollary (implies (case-split (rationalp x))
       (and (>= (cg x) x) (> (1+ x) (cg x))))) (:type-prescription :corollary (integerp (cg x)))))

cg-positivetheorem

(defthm cg-positive
  (implies (case-split (not (complex-rationalp x)))
    (equal (< 0 (cg x)) (< 0 x)))
  :hints (("Goal" :in-theory (enable cg))))

cg

Included Books