building-blocks-helper

Included Books

top

other

(in-package "ACL2")

local

(local (include-book "../../support/top"))

local

(local (defun rationalp-guard-fn
    (args)
    (if (endp (cdr args))
      `((rationalp ,(CAR ARGS)))
      (cons `(rationalp ,(CAR ARGS))
        (rationalp-guard-fn (cdr args))))))

local

(local (defmacro rationalp-guard
    (&rest args)
    (if (endp (cdr args))
      `(rationalp ,(CAR ARGS))
      (cons 'and (rationalp-guard-fn args)))))

local

(local (defun real/rationalp-guard-fn
    (args)
    (if (endp (cdr args))
      `((real/rationalp ,(CAR ARGS)))
      (cons `(real/rationalp ,(CAR ARGS))
        (real/rationalp-guard-fn (cdr args))))))

local

(local (defmacro real/rationalp-guard
    (&rest args)
    (if (endp (cdr args))
      `(real/rationalp ,(CAR ARGS))
      (cons 'and (real/rationalp-guard-fn args)))))

local

(local (defthm niq-bounds
    (implies (and (integerp i) (<= 0 i) (integerp j) (< 0 j))
      (and (<= (nonnegative-integer-quotient i j) (/ i j))
        (< (+ (/ i j) -1) (nonnegative-integer-quotient i j))))
    :hints (("Subgoal *1/1''" :use (:instance normalize-<-/-to-*-3-3 (x 1) (z j) (y i))))
    :rule-classes ((:linear :trigger-terms ((nonnegative-integer-quotient i j))))))

local

(local (defthm floor-bounds-1
    (implies (real/rationalp-guard x y)
      (and (< (+ (/ x y) -1) (floor x y))
        (<= (floor x y) (/ x y))))
    :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y))))))

local

(local (defthm floor-bounds-2
    (implies (and (real/rationalp-guard x y) (integerp (/ x y)))
      (equal (floor x y) (/ x y)))
    :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y))))))

local

(local (defthm floor-bounds-3
    (implies (and (real/rationalp-guard x y) (not (integerp (/ x y))))
      (< (floor x y) (/ x y)))
    :rule-classes ((:generalize) (:linear :trigger-terms ((floor x y))))))

local

(local (in-theory (disable floor)))

onetheorem

(defthm one
  (implies (and (integerp x) (integerp y) (<= 0 y))
    (<= 0 (logand x y)))
  :rule-classes :linear)

twotheorem

(defthm two
  (implies (and (integerp x) (integerp y) (<= 0 y))
    (<= (logand x y) y))
  :rule-classes :linear)

rewrite-floor-x*y-z-lefttheorem

(defthm rewrite-floor-x*y-z-left
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (real/rationalp z)
      (not (equal z 0)))
    (equal (floor (* x y) z) (floor y (/ z x)))))

power-of-2-measurefunction

(defun power-of-2-measure
  (x)
  (declare (xargs :guard (and (real/rationalp x) (not (equal x 0)))))
  (cond ((or (not (real/rationalp x)) (<= x 0)) 0)
    ((< x 1) (cons (cons 1 1) (floor (/ x) 1)))
    (t (floor x 1))))

power-of-2-helperfunction

(defun power-of-2-helper
  (x)
  (declare (xargs :guard t
      :measure (power-of-2-measure x)
      :hints (("Subgoal 2.2'" :use (:instance (:theorem (implies (and (real/rationalp x) (< 2 x))
               (< (floor x 2) (floor x 1))))
           (x (/ x)))
         :in-theory (enable normalize-<-/-to-*-1)))))
  (cond ((or (not (real/rationalp x)) (<= x 0)) 0)
    ((< x 1) (+ -1 (power-of-2-helper (* 2 x))))
    ((<= 2 x) (+ 1 (power-of-2-helper (* 1/2 x))))
    ((equal x 1) 0)
    (t 0)))