		Search-engine friendly clone of the ACL2 documentation.

Floating-point-value-placeholders

Doublex-value-abs

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

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

Definition: doublex-value-abs-p

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

Definition: doublex-value-abs-pos-zero

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

Definitions and Theorems

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

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

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

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

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

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

Function: doublex-value-abs-fix

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

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

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

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

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