Abstract placeholders for the Java floating-point conversions [JLS14:5.1].
Theorem:
(defthm byte-to-float-abs-type (float-value-abs-p (byte-to-float-abs x)))
Theorem:
(defthm byte-to-double-abs-type (double-value-abs-p (byte-to-double-abs x)))
Theorem:
(defthm short-to-float-abs-type (float-value-abs-p (short-to-float-abs x)))
Theorem:
(defthm short-to-double-abs-type (double-value-abs-p (short-to-double-abs x)))
Theorem:
(defthm char-to-float-abs-type (float-value-abs-p (char-to-float-abs x)))
Theorem:
(defthm char-to-double-abs-type (double-value-abs-p (char-to-double-abs x)))
Theorem:
(defthm int-to-float-abs-type (float-value-abs-p (int-to-float-abs x)))
Theorem:
(defthm int-to-double-abs-type (double-value-abs-p (int-to-double-abs x)))
Theorem:
(defthm long-to-float-abs-type (float-value-abs-p (long-to-float-abs x)))
Theorem:
(defthm long-to-double-abs-type (double-value-abs-p (long-to-double-abs x)))
Theorem:
(defthm float-to-double-abs-type (double-value-abs-p (float-to-double-abs x)))
Theorem:
(defthm float-to-byte-abs-type (sbyte8p (float-to-byte-abs x)))
Theorem:
(defthm float-to-short-abs-type (sbyte16p (float-to-short-abs x)))
Theorem:
(defthm float-to-char-abs-type (ubyte16p (float-to-char-abs x)))
Theorem:
(defthm float-to-int-abs-type (sbyte32p (float-to-int-abs x)))
Theorem:
(defthm float-to-long-abs-type (sbyte64p (float-to-long-abs x)))
Theorem:
(defthm double-to-byte-abs-type (sbyte8p (double-to-byte-abs x)))
Theorem:
(defthm double-to-short-abs-type (sbyte16p (double-to-short-abs x)))
Theorem:
(defthm double-to-char-abs-type (ubyte16p (double-to-char-abs x)))
Theorem:
(defthm double-to-int-abs-type (sbyte32p (double-to-int-abs x)))
Theorem:
(defthm double-to-long-abs-type (sbyte64p (double-to-long-abs x)))
Theorem:
(defthm double-to-float-abs-type (float-value-abs-p (double-to-float-abs x)))