Theorems saying that specific value-kinds imply corresponding value predicates.
Theorem:
(defthm scharp-when-valuep-and-kind-schar (implies (and (valuep val) (value-case val :schar)) (scharp val)))
Theorem:
(defthm ucharp-when-valuep-and-kind-uchar (implies (and (valuep val) (value-case val :uchar)) (ucharp val)))
Theorem:
(defthm sshortp-when-valuep-and-kind-sshort (implies (and (valuep val) (value-case val :sshort)) (sshortp val)))
Theorem:
(defthm ushortp-when-valuep-and-kind-ushort (implies (and (valuep val) (value-case val :ushort)) (ushortp val)))
Theorem:
(defthm sintp-when-valuep-and-kind-sint (implies (and (valuep val) (value-case val :sint)) (sintp val)))
Theorem:
(defthm uintp-when-valuep-and-kind-uint (implies (and (valuep val) (value-case val :uint)) (uintp val)))
Theorem:
(defthm slongp-when-valuep-and-kind-slong (implies (and (valuep val) (value-case val :slong)) (slongp val)))
Theorem:
(defthm ulongp-when-valuep-and-kind-ulong (implies (and (valuep val) (value-case val :ulong)) (ulongp val)))
Theorem:
(defthm sllongp-when-valuep-and-kind-sllong (implies (and (valuep val) (value-case val :sllong)) (sllongp val)))
Theorem:
(defthm ullongp-when-valuep-and-kind-ullong (implies (and (valuep val) (value-case val :ullong)) (ullongp val)))