		Search-engine friendly clone of the ACL2 documentation.

Floating-point-value-placeholders

Floatx-value-abs

Abstract recognizer and fixer for the float-extended-exponent value set [JLS14:4.2.3].

We introduce a constrained predicate for the underlying values of Java float values in the float-extended-exponent 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 empty if and only if floatx-param is nil, i.e. if there are no extended-exponent float values. Non-emptiness is expressed via a constrained nullary function that returns the positive 0 of the float-extended-exponent value set. Since the predicate may be empty, we cannot define a fixtype, but we define a conditional fixer.

Definition: floatx-value-abs-p

(encapsulate (((floatx-value-abs-p *) => *)
              ((floatx-value-abs-pos-zero) => *))
  (local (value-triple :elided))
  (local (value-triple :elided))
  (local (value-triple :elided))
  (defthm booleanp-of-floatx-value-abs-p
    (booleanp (floatx-value-abs-p x))
    :rule-classes (:rewrite :type-prescription))
  (defrule not-floatx-value-abs-p-when-not-floatx-param
    (implies (not (floatx-param))
             (not (floatx-value-abs-p x))))
  (defrule
   floatx-value-abs-p-of-floatx-value-abs-pos-zero-when-floatx-param
   (implies (floatx-param)
            (floatx-value-abs-p (floatx-value-abs-pos-zero)))))

Definition: floatx-value-abs-pos-zero

(encapsulate (((floatx-value-abs-p *) => *)
              ((floatx-value-abs-pos-zero) => *))
  (local (value-triple :elided))
  (local (value-triple :elided))
  (local (value-triple :elided))
  (defthm booleanp-of-floatx-value-abs-p
    (booleanp (floatx-value-abs-p x))
    :rule-classes (:rewrite :type-prescription))
  (defrule not-floatx-value-abs-p-when-not-floatx-param
    (implies (not (floatx-param))
             (not (floatx-value-abs-p x))))
  (defrule
   floatx-value-abs-p-of-floatx-value-abs-pos-zero-when-floatx-param
   (implies (floatx-param)
            (floatx-value-abs-p (floatx-value-abs-pos-zero)))))

Definitions and Theorems

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

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

Theorem: not-floatx-value-abs-p-when-not-floatx-param

(defthm not-floatx-value-abs-p-when-not-floatx-param
  (implies (not (floatx-param))
           (not (floatx-value-abs-p x))))

Theorem: floatx-value-abs-p-of-floatx-value-abs-pos-zero-when-floatx-param

(defthm
  floatx-value-abs-p-of-floatx-value-abs-pos-zero-when-floatx-param
  (implies (floatx-param)
           (floatx-value-abs-p (floatx-value-abs-pos-zero))))

Function: floatx-value-abs-fix

(defun floatx-value-abs-fix (x)
  (declare (xargs :guard (floatx-value-abs-p x)))
  (let ((__function__ 'floatx-value-abs-fix))
    (declare (ignorable __function__))
    (mbe :logic
         (if (floatx-value-abs-p x)
             x
           (floatx-value-abs-pos-zero))
         :exec x)))

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

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

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

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