		Search-engine friendly clone of the ACL2 documentation.

Floating-point-value-placeholders

Double-value-abs

Abstract fixtype for the double value set [JLS14:4.2.3].

We introduce a constrained predicate for the underlying values of Java double values in the double value set. The latter are defined by tagging the underlying values, in the same way that our model of the Java int values (for instance) is defined by tagging 32-bit signed integers as the underlying values.

The predicate is constrained to be non-empty: this is expressed via a constrained nullary function that returns the positive 0 of the double value set. These constraints enable the definition of a fixer and fixtype.

Definition: double-value-abs-p

(encapsulate (((double-value-abs-p *) acl2::=> *)
              ((double-value-abs-pos-zero)
               acl2::=> *))
  (local (value-triple :elided))
  (local (value-triple :elided))
  (defthm booleanp-of-double-value-abs-p
    (booleanp (double-value-abs-p x))
    :rule-classes (:rewrite :type-prescription))
  (defthm double-value-abs-p-of-double-value-abs-pos-zero
    (double-value-abs-p (double-value-abs-pos-zero))))

Definition: double-value-abs-pos-zero

(encapsulate (((double-value-abs-p *) acl2::=> *)
              ((double-value-abs-pos-zero)
               acl2::=> *))
  (local (value-triple :elided))
  (local (value-triple :elided))
  (defthm booleanp-of-double-value-abs-p
    (booleanp (double-value-abs-p x))
    :rule-classes (:rewrite :type-prescription))
  (defthm double-value-abs-p-of-double-value-abs-pos-zero
    (double-value-abs-p (double-value-abs-pos-zero))))

Definitions and Theorems

Theorem: booleanp-of-double-value-abs-p

(defthm booleanp-of-double-value-abs-p
  (booleanp (double-value-abs-p x))
  :rule-classes (:rewrite :type-prescription))

Theorem: double-value-abs-p-of-double-value-abs-pos-zero

(defthm double-value-abs-p-of-double-value-abs-pos-zero
  (double-value-abs-p (double-value-abs-pos-zero)))

Function: double-value-abs-fix

(defun double-value-abs-fix (x)
  (declare (xargs :guard (double-value-abs-p x)))
  (mbe :logic
       (if (double-value-abs-p x)
           x
         (double-value-abs-pos-zero))
       :exec x))

Theorem: double-value-abs-p-of-double-value-abs-fix

(defthm double-value-abs-p-of-double-value-abs-fix
  (b* ((fixed-x (double-value-abs-fix x)))
    (double-value-abs-p fixed-x))
  :rule-classes :rewrite)

Theorem: double-value-abs-fix-when-double-value-abs-p

(defthm double-value-abs-fix-when-double-value-abs-p
  (implies (double-value-abs-p x)
           (equal (double-value-abs-fix x) x)))

Function: double-value-abs-equiv$inline

(defun double-value-abs-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (double-value-abs-p acl2::x)
                              (double-value-abs-p acl2::y))))
  (equal (double-value-abs-fix acl2::x)
         (double-value-abs-fix acl2::y)))

Theorem: double-value-abs-equiv-is-an-equivalence

(defthm double-value-abs-equiv-is-an-equivalence
  (and (booleanp (double-value-abs-equiv x y))
       (double-value-abs-equiv x x)
       (implies (double-value-abs-equiv x y)
                (double-value-abs-equiv y x))
       (implies (and (double-value-abs-equiv x y)
                     (double-value-abs-equiv y z))
                (double-value-abs-equiv x z)))
  :rule-classes (:equivalence))

Theorem: double-value-abs-equiv-implies-equal-double-value-abs-fix-1

(defthm double-value-abs-equiv-implies-equal-double-value-abs-fix-1
  (implies (double-value-abs-equiv acl2::x x-equiv)
           (equal (double-value-abs-fix acl2::x)
                  (double-value-abs-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: double-value-abs-fix-under-double-value-abs-equiv

(defthm double-value-abs-fix-under-double-value-abs-equiv
  (double-value-abs-equiv (double-value-abs-fix acl2::x)
                          acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-double-value-abs-fix-1-forward-to-double-value-abs-equiv

(defthm
  equal-of-double-value-abs-fix-1-forward-to-double-value-abs-equiv
  (implies (equal (double-value-abs-fix acl2::x)
                  acl2::y)
           (double-value-abs-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-double-value-abs-fix-2-forward-to-double-value-abs-equiv

(defthm
  equal-of-double-value-abs-fix-2-forward-to-double-value-abs-equiv
  (implies (equal acl2::x (double-value-abs-fix acl2::y))
           (double-value-abs-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: double-value-abs-equiv-of-double-value-abs-fix-1-forward

(defthm double-value-abs-equiv-of-double-value-abs-fix-1-forward
  (implies (double-value-abs-equiv (double-value-abs-fix acl2::x)
                                   acl2::y)
           (double-value-abs-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: double-value-abs-equiv-of-double-value-abs-fix-2-forward

(defthm double-value-abs-equiv-of-double-value-abs-fix-2-forward
 (implies
     (double-value-abs-equiv acl2::x (double-value-abs-fix acl2::y))
     (double-value-abs-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Subtopics

Double-value-abs-fix: Fixer for double-value-abs.