power2p

other

(in-package "ACL2")

flfunction

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

local

(local (include-book "fl"))

local

(local (include-book "fp2"))

local

(local (include-book "predicate"))

local

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

include-book

(include-book "../../../ordinals/e0-ordinal")

other

(set-well-founded-relation e0-ord-<)

power2p-measurefunction

(defund power2p-measure
  (x)
  (declare (xargs :guard (and (rationalp x) (not (equal x 0)))))
  (cond ((or (not (rationalp x)) (<= x 0)) 0)
    ((< x 1) (cons 1 (fl (/ x))))
    (t (fl x))))

power2pfunction

(defund power2p
  (x)
  (declare (xargs :guard t
      :measure (power2p-measure x)
      :hints (("goal" :in-theory (enable power2p-measure)))))
  (cond ((or (not (rationalp x)) (<= x 0)) nil)
    ((< x 1) (power2p (* 2 x)))
    ((<= 2 x) (power2p (* 1/2 x)))
    ((equal x 1) t)
    (t nil)))

power2-syntaxpfunction

(defund power2-syntaxp
  (term)
  (if (not (consp term))
    nil
    (case (car term)
      '(and (rationalp (cadr term)) (power2p (cadr term)))
      (expt (equal (cadr term) ''2))
      (binary-* (and (power2-syntaxp (cadr term))
          (power2-syntaxp (caddr term))))
      (unary-/ (power2-syntaxp (cadr term)))
      (otherwise nil))))

power2p-with-arg-between-one-and-twotheorem

(defthmd power2p-with-arg-between-one-and-two
  (implies (and (< 1/2 x) (< x 1)) (not (power2p x)))
  :hints (("goal" :in-theory (enable power2p))))

power2p-of-non-rationaltheorem

(defthm power2p-of-non-rational
  (implies (not (rationalp x)) (equal (power2p x) nil))
  :hints (("goal" :in-theory (enable power2p))))

power2p-of-non-positivetheorem

(defthm power2p-of-non-positive
  (implies (not (< 0 x)) (equal (power2p x) nil))
  :hints (("goal" :in-theory (enable power2p))))

power2p-inversetheorem

(defthm power2p-inverse
  (and (equal (power2p (/ x)) (power2p x))
    (equal (power2p (/ 1 x)) (power2p x)))
  :otf-flg t
  :hints (("goal" :in-theory (enable power2p power2p-with-arg-between-one-and-two))))

power2p-doubletheorem

(defthmd power2p-double
  (equal (power2p (* 2 x)) (power2p x))
  :hints (("goal" :in-theory (enable power2p power2p-with-arg-between-one-and-two))))

power2p-halftheorem

(defthmd power2p-half
  (equal (power2p (* 1/2 x)) (power2p x))
  :hints (("goal" :in-theory (enable power2p power2p-with-arg-between-one-and-two))))

power2p-prodtheorem

(defthmd power2p-prod
  (implies (and (power2p x) (power2p y)) (power2p (* x y)))
  :hints (("goal" :in-theory (enable power2p
       power2p-double
       power2p-half
       power2p-with-arg-between-one-and-two))))

power2p-prod-nottheorem

(defthmd power2p-prod-not
  (implies (and (not (power2p x)) (power2p y))
    (not (power2p (* x y))))
  :hints (("goal" :in-theory (disable power2p-prod)
     :use (:instance power2p-prod (x (* x y)) (y (/ y))))))

power2p-shifttheorem

(defthm power2p-shift
  (implies (and (syntaxp (power2-syntaxp x)) (force (power2p x)))
    (equal (power2p (* x y)) (power2p y)))
  :hints (("goal" :use ((:instance power2p-prod-not (y x) (x y)) (:instance power2p-prod (y x) (x y))))))

power2p-shift-2theorem

(defthm power2p-shift-2
  (implies (and (syntaxp (power2-syntaxp y)) (force (power2p y)))
    (equal (power2p (* x y)) (power2p x)))
  :hints (("goal" :in-theory (disable power2p)
     :use (power2p-prod-not power2p-prod))))

power2p-means-positive-rationalptheorem

(defthm power2p-means-positive-rationalp
  (implies (power2p x) (and (< 0 x) (rationalp x)))
  :rule-classes ((:forward-chaining :trigger-terms ((power2p x)))))

Included Books