basic - ACL2 Book

Included Books

fp2 even-odd fl expt

other

(in-package "ACL2")

flfunction

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

include-book

(include-book "fp2")

local

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

natpfunction

(defun natp
  (x)
  (declare (xargs :guard t))
  (and (integerp x) (<= 0 x)))

natp-compound-recognizertheorem

(defthm natp-compound-recognizer
  (equal (natp x) (and (integerp x) (<= 0 x)))
  :rule-classes :compound-recognizer)

natp+theorem

(defthmd natp+
  (implies (and (natp x) (natp y)) (natp (+ x y))))

natp*theorem

(defthmd natp*
  (implies (and (natp x) (natp y)) (natp (* x y))))

abs-nonnegative-acl2-numberp-typetheorem

(defthm abs-nonnegative-acl2-numberp-type
  (implies (case-split (acl2-numberp x))
    (and (<= 0 (abs x)) (acl2-numberp (abs x))))
  :rule-classes (:type-prescription))

abs-nonnegative-rationalp-typetheorem

(defthm abs-nonnegative-rationalp-type
  (implies (case-split (rationalp x))
    (and (<= 0 (abs x)) (rationalp (abs x))))
  :rule-classes (:type-prescription))

abs-nonnegative-integerp-typetheorem

(defthm abs-nonnegative-integerp-type
  (implies (integerp x)
    (and (<= 0 (abs x)) (rationalp (abs x))))
  :rule-classes (:type-prescription))

abs-nonnegativetheorem

(defthm abs-nonnegative (<= 0 (abs x)))

local

(local (include-book "fl"))

fl-def-lineartheorem

(defthm fl-def-linear
  (implies (case-split (rationalp x))
    (and (<= (fl x) x) (< x (1+ (fl x)))))
  :rule-classes :linear)

fl-monotone-lineartheorem

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

n<=fl-lineartheorem

(defthm n<=fl-linear
  (implies (and (<= n x) (rationalp x) (integerp n))
    (<= n (fl x)))
  :rule-classes :linear)

fl+int-rewritetheorem

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

fl/int-rewritetheorem

(defthm fl/int-rewrite
  (implies (and (integerp n) (<= 0 n) (rationalp x))
    (equal (fl (/ (fl x) n)) (fl (/ x n))))
  :hints (("Goal" :use ((:instance fl/int-1) (:instance fl/int-2)))))

fl-integer-typetheorem

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

fl-deftheorem

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

in-theory

(in-theory (disable (:type-prescription fl)))

fl-inttheorem

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

fl-integerpencapsulate

(encapsulate nil
  (local (include-book "fl"))
  (defthm fl-integerp (equal (equal (fl x) x) (integerp x))))

fl-uniquetheorem

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

expt-2-positive-rational-typeencapsulate

(encapsulate nil
  (local (include-book "expt"))
  (defthm expt-2-positive-rational-type
    (and (rationalp (expt 2 i)) (< 0 (expt 2 i)))
    :rule-classes (:rewrite (:type-prescription :typed-term (expt 2 i))))
  (defthm expt-2-positive-integer-type
    (implies (<= 0 i)
      (and (integerp (expt 2 i)) (< 0 (expt 2 i))))
    :rule-classes (:type-prescription))
  (defthm expt-2-integerp
    (implies (<= 0 i) (integerp (expt 2 i))))
  (defthm expt-2-type-linear
    (implies (<= 0 i) (<= 1 (expt 2 i)))
    :rule-classes ((:linear :trigger-terms ((expt 2 i)))))
  (defthmd expt-split
    (implies (and (integerp i)
        (integerp j)
        (case-split (acl2-numberp r))
        (case-split (not (equal r 0))))
      (equal (expt r (+ i j)) (* (expt r i) (expt r j)))))
  (theory-invariant (incompatible (:rewrite expt-split) (:definition a15))
    :key expt-split-invariant)
  (defthmd expt-weak-monotone
    (implies (and (integerp n) (integerp m))
      (equal (<= (expt 2 n) (expt 2 m)) (<= n m))))
  (defthmd expt-weak-monotone-linear
    (implies (and (<= n m)
        (case-split (integerp n))
        (case-split (integerp m)))
      (<= (expt 2 n) (expt 2 m)))
    :rule-classes ((:linear :match-free :all)))
  (defthmd expt-strong-monotone
    (implies (and (integerp n) (integerp m))
      (equal (< (expt 2 n) (expt 2 m)) (< n m))))
  (defthmd expt-strong-monotone-linear
    (implies (and (< n m)
        (case-split (integerp n))
        (case-split (integerp m)))
      (< (expt 2 n) (expt 2 m)))
    :rule-classes ((:linear :match-free :all)))
  (defthmd a15
    (implies (and (rationalp i)
        (not (equal i 0))
        (integerp j1)
        (integerp j2))
      (and (equal (* (expt i j1) (expt i j2)) (expt i (+ j1 j2)))
        (equal (* (expt i j1) (* (expt i j2) x))
          (* (expt i (+ j1 j2)) x))))))

expt-execfunction

(defun expt-exec
  (r i)
  (declare (xargs :guard (and (acl2-numberp r)
        (integerp i)
        (not (and (eql r 0) (< i 0))))
      :guard-hints (("Goal" :expand (hide (expt r i))))))
  (mbe :logic (hide (expt r i)) :exec (expt r i)))

expt-2-evaluatortheorem

(defthm expt-2-evaluator
  (implies (syntaxp (and (quotep n) (natp (cadr n)) (< (cadr n) 130)))
    (equal (expt 2 n) (expt-exec 2 n)))
  :hints (("Goal" :expand ((hide (expt 2 n))))))

*-doubly-monotonictheorem

(defthm *-doubly-monotonic
  (implies (and (rationalp x)
      (rationalp y)
      (rationalp a)
      (rationalp b)
      (<= 0 x)
      (<= 0 y)
      (<= 0 a)
      (<= 0 b)
      (<= x y)
      (<= a b))
    (<= (* x a) (* y b)))
  :rule-classes nil)

fl-halffunction

(defund fl-half (x) (1- (fl (/ (1+ x) 2))))

fl-half-lemmatheorem

(defthm fl-half-lemma
  (implies (and (integerp x) (not (integerp (/ x 2))))
    (= x (1+ (* 2 (fl-half x)))))
  :rule-classes nil
  :hints (("goal" :in-theory (e/d (fl-half) (fl-int))
     :use ((:instance x-or-x/2) (:instance fl-int (x (/ (1+ x) 2)))))))