float-a - ACL2 Book

other

(in-package "ACL2")

encapsulate

(encapsulate nil
  (logic)
  (partial-encapsulate (((constrained-to-df *) =>
       *
       :formals (x)
       :guard (rationalp x)))
    nil
    (local (defun constrained-to-df (x) (declare (ignore x)) 0))
    (defthm rationalp-constrained-to-df
      (rationalp (constrained-to-df x))
      :rule-classes :type-prescription)
    (defthm constrained-to-df-idempotent
      (equal (constrained-to-df (constrained-to-df x))
        (constrained-to-df x)))
    (defthm to-df-minus
      (implies (and (rationalp x) (equal (constrained-to-df x) x))
        (equal (constrained-to-df (- x)) (- x))))
    (defthm constrained-to-df-default
      (implies (not (rationalp x))
        (equal (constrained-to-df x) 0)))
    (defthm constrained-to-df-0 (equal (constrained-to-df 0) 0))
    (defthm constrained-to-df-monotonicity
      (implies (and (<= x y) (rationalp x) (rationalp y))
        (<= (constrained-to-df x) (constrained-to-df y)))
      :rule-classes (:linear :rewrite))))

to-dffunction

(defun to-df
  (x)
  (declare (xargs :guard (rationalp x) :mode :logic))
  (constrained-to-df x))

rationalp-to-dftheorem

(defthm rationalp-to-df
  (rationalp (to-df x))
  :rule-classes :type-prescription)

to-df-idempotenttheorem

(defthm to-df-idempotent
  (equal (to-df (to-df x)) (to-df x)))

to-df-defaulttheorem

(defthm to-df-default
  (implies (not (rationalp x)) (equal (to-df x) 0)))

to-df-monotonicitytheorem

(defthm to-df-monotonicity
  (implies (and (<= x y) (rationalp x) (rationalp y))
    (<= (to-df x) (to-df y)))
  :rule-classes (:linear :rewrite))

dfpfunction

(defun dfp
  (x)
  (declare (xargs :guard t :mode :logic))
  (and (rationalp x) (= (to-df x) x)))

from-dffunction

(defun from-df
  (x)
  (declare (xargs :guard (dfp x) :mode :logic))
  x)

to-dfpfunction

(defun to-dfp
  (x)
  (declare (xargs :guard (rationalp x) :mode :logic))
  (from-df (to-df x)))

dfp-to-dftheorem

(defthm dfp-to-df (dfp (to-df x)))

dfp-implies-rationalptheorem

(defthm dfp-implies-rationalp
  (implies (dfp x) (rationalp x))
  :rule-classes :compound-recognizer)

dfp-implies-to-df-is-identitytheorem

(defthm dfp-implies-to-df-is-identity
  (implies (dfp x) (equal (to-df x) x))
  :rule-classes (:forward-chaining :rewrite))

in-theory

(in-theory (disable dfp to-df))

encapsulate

(encapsulate nil
  (logic)
  (partial-encapsulate (((df-round *) => * :formals (x) :guard (rationalp x)))
    nil
    (local (defun df-round (x) (constrained-to-df x)))
    (defthm rationalp-df-round
      (rationalp (df-round x))
      :rule-classes :type-prescription)
    (defthm dfp-df-round (dfp (df-round r)))
    (defthm df-round-is-identity-for-dfp
      (implies (dfp r) (equal (df-round r) r)))
    (defthm df-round-monotonicity
      (implies (and (<= x y) (rationalp x) (rationalp y))
        (<= (df-round x) (df-round y)))
      :rule-classes (:linear :rewrite))))

df-round-idempotenttheorem

(defthm df-round-idempotent
  (equal (df-round (df-round x)) (df-round x)))

encapsulate

(encapsulate nil
  (logic)
  (partial-encapsulate (((constrained-df-rationalize *) =>
       *
       :formals (x)
       :guard (dfp x)))
    (constrained-to-df)
    (local (defun constrained-df-rationalize
        (x)
        (if (dfp x)
          x
          0)))
    (defthm rationalp-constrained-df-rationalize
      (rationalp (constrained-df-rationalize x))
      :rule-classes :type-prescription)
    (defthm to-df-of-constrained-df-rationalize
      (implies (dfp x)
        (equal (to-df (constrained-df-rationalize x)) x)))))

binary-df+function

(defun binary-df+
  (x y)
  (declare (xargs :mode :logic :guard (and (dfp x) (dfp y))))
  (df-round (+ x y)))

unary-df-function

(defun unary-df-
  (x)
  (declare (xargs :mode :logic :guard (dfp x)))
  (df-round (- x)))

dfp-minustheorem

(defthm dfp-minus
  (implies (dfp x) (dfp (- x)))
  :hints (("Goal" :in-theory (enable dfp to-df))))

unary-df/function

(defun unary-df/
  (x)
  (declare (xargs :mode :logic :guard (and (dfp x) (not (= x 0)))))
  (df-round (/ x)))

binary-df*function

(defun binary-df*
  (x y)
  (declare (xargs :mode :logic :guard (and (dfp x) (dfp y))))
  (df-round (* x y)))

binary-df/function

(defun binary-df/
  (x y)
  (declare (xargs :mode :logic :guard (and (dfp x) (dfp y) (not (= y 0)))))
  (df-round (/ x y)))

*df-basic-primitives*constant

(defconst *df-basic-primitives*
  '((from-df (:df) (nil)) (to-df (nil) (:df))
    (df-string (:df) (nil))
    (binary-df+ (:df :df) (:df))
    (binary-df* (:df :df) (:df))
    (binary-df/ (:df :df) (:df))
    (unary-df- (:df) (:df))
    (unary-df/ (:df) (:df))))

install-df-basic-primitives-1function

(defun install-df-basic-primitives-1
  (alist wrld)
  (declare (xargs :mode :program))
  (cond ((endp alist) wrld)
    (t (install-df-basic-primitives-1 (cdr alist)
        (let* ((tuple (car alist)) (fn (car tuple))
            (stobjs-in (cadr tuple))
            (stobjs-out (caddr tuple)))
          (putprop fn
            'stobjs-in
            stobjs-in
            (putprop fn 'stobjs-out stobjs-out wrld)))))))