Rules about value-integer->get assuming the various integer types.
Using these rules, instead of opening the definition of value-integer->get, avoids case splits in proofs.
Theorem:
(defthm value-integer->get-when-scharp (implies (scharp x) (equal (value-integer->get x) (integer-from-schar x))))
Theorem:
(defthm value-integer->get-when-ucharp (implies (ucharp x) (equal (value-integer->get x) (integer-from-uchar x))))
Theorem:
(defthm value-integer->get-when-sshortp (implies (sshortp x) (equal (value-integer->get x) (integer-from-sshort x))))
Theorem:
(defthm value-integer->get-when-ushortp (implies (ushortp x) (equal (value-integer->get x) (integer-from-ushort x))))
Theorem:
(defthm value-integer->get-when-sintp (implies (sintp x) (equal (value-integer->get x) (integer-from-sint x))))
Theorem:
(defthm value-integer->get-when-uintp (implies (uintp x) (equal (value-integer->get x) (integer-from-uint x))))
Theorem:
(defthm value-integer->get-when-slongp (implies (slongp x) (equal (value-integer->get x) (integer-from-slong x))))
Theorem:
(defthm value-integer->get-when-ulongp (implies (ulongp x) (equal (value-integer->get x) (integer-from-ulong x))))
Theorem:
(defthm value-integer->get-when-sllongp (implies (sllongp x) (equal (value-integer->get x) (integer-from-sllong x))))
Theorem:
(defthm value-integer->get-when-ullongp (implies (ullongp x) (equal (value-integer->get x) (integer-from-ullong x))))
Theorem:
(defthm value-integer->get-when-cintegerp (implies (cintegerp x) (equal (value-integer->get x) (integer-from-cinteger x))))