Abstract placeholders for the Java floating-point operations [JLS14:4.2.4].
Theorem:
(defthm float-plus-abs-type (float-value-abs-p (float-plus-abs x)))
Theorem:
(defthm double-plus-abs-type (double-value-abs-p (double-plus-abs x)))
Theorem:
(defthm float-minus-abs-type (float-value-abs-p (float-minus-abs x)))
Theorem:
(defthm double-minus-abs-type (double-value-abs-p (double-minus-abs x)))
Theorem:
(defthm float-add-abs-type (float-value-abs-p (float-add-abs x y)))
Theorem:
(defthm double-add-abs-type (double-value-abs-p (double-add-abs x y)))
Theorem:
(defthm float-sub-abs-type (float-value-abs-p (float-sub-abs x y)))
Theorem:
(defthm double-sub-abs-type (double-value-abs-p (double-sub-abs x y)))
Theorem:
(defthm float-mul-abs-type (float-value-abs-p (float-mul-abs x y)))
Theorem:
(defthm double-mul-abs-type (double-value-abs-p (double-mul-abs x y)))
Theorem:
(defthm float-div-abs-type (float-value-abs-p (float-div-abs x y)))
Theorem:
(defthm double-div-abs-type (double-value-abs-p (double-div-abs x y)))
Theorem:
(defthm float-rem-abs-type (float-value-abs-p (float-rem-abs x y)))
Theorem:
(defthm double-rem-abs-type (double-value-abs-p (double-rem-abs x y)))
Theorem:
(defthm float-eq-abs-type (booleanp (float-eq-abs x y)))
Theorem:
(defthm double-eq-abs-type (booleanp (double-eq-abs x y)))
Theorem:
(defthm float-neq-abs-type (booleanp (float-neq-abs x y)))
Theorem:
(defthm double-neq-abs-type (booleanp (double-neq-abs x y)))
Theorem:
(defthm float-less-abs-type (booleanp (float-less-abs x y)))
Theorem:
(defthm double-less-abs-type (booleanp (double-less-abs x y)))
Theorem:
(defthm float-lesseq-abs-type (booleanp (float-lesseq-abs x y)))
Theorem:
(defthm double-lesseq-abs-type (booleanp (double-lesseq-abs x y)))
Theorem:
(defthm float-great-abs-type (booleanp (float-great-abs x y)))
Theorem:
(defthm double-great-abs-type (booleanp (double-great-abs x y)))
Theorem:
(defthm float-greateq-abs-type (booleanp (float-greateq-abs x y)))
Theorem:
(defthm double-greateq-abs-type (booleanp (double-greateq-abs x y)))