fl-hacks - ACL2 Book

Included Books

ground-zero inverted-factor nniq numerator denominator fp2 predicate product unary-divide rationalp integerp fl mod even-odd meta-plus-equal arith

other

(in-package "ACL2")

include-book

(include-book "ground-zero")

flfunction

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

local

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

local

(local (include-book "nniq"))

local

(local (include-book "numerator"))

local

(local (include-book "denominator"))

local

(local (include-book "fp2"))

local

(local (include-book "predicate"))

local

(local (include-book "product"))

local

(local (include-book "unary-divide"))

local

(local (include-book "rationalp"))

local

(local (include-book "integerp"))

local

(local (include-book "fl"))

local

(local (include-book "mod"))

local

(local (include-book "even-odd"))

local

(local (include-book "../../../meta/meta-plus-equal"))

local

(local (include-book "arith"))

fl-m-1theorem

(defthm fl-m-1
  (implies (and (< 0 n) (integerp m) (integerp n))
    (= (fl (- (/ (1+ m) n))) (1- (- (fl (/ m n))))))
  :otf-flg t
  :rule-classes nil
  :hints (("goal" :in-theory (disable fl-def-linear-part-2
       less-than-multiply-through-by-inverted-factor-from-left-hand-side)
     :use ((:instance fl-of-fraction-min-change (p (+ 1 m)) (q n)) (:instance fl-unique
         (x (* m (/ n)))
         (n (+ -1 (+ (/ n) (* m (/ n))))))
       (:instance fl-unique
         (x (+ (/ n) (* m (/ n))))
         (n (fl (* m (/ n)))))))))

fl-m-ntheorem

(defthm fl-m-n
  (implies (and (< 0 n) (integerp m) (integerp n))
    (= (fl (- (/ m n))) (1- (- (fl (/ (1- m) n))))))
  :hints (("Goal" :use ((:instance fl-m-1 (m (1- m))))))
  :rule-classes nil)

fl-lemmatheorem

(defthm fl-lemma
  (implies (integerp m)
    (= (fl (- (/ (1+ m) 2))) (1- (- (fl (/ m 2))))))
  :rule-classes nil
  :hints (("goal" :use (:instance fl-m-1 (n 2)))))