		Search-engine friendly clone of the ACL2 documentation.

Floating-point-value-placeholders

Float-value-abs

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

We introduce a constrained predicate for the underlying values of Java float values in the float 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 float value set. These constraints enable the definition of a fixer and fixtype.

Definition: float-value-abs-p

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

Definition: float-value-abs-pos-zero

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

Definitions and Theorems

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

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

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

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

Function: float-value-abs-fix

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

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

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

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

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

Function: float-value-abs-equiv$inline

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Subtopics

Float-value-abs-fix: Fixer for float-value-abs.