Bridge theorems between the deeply embedded integer values and the shallowly embedded integer values.
The deeply embedded integer values are a subset of the values of the fixtype value. The shallowly embedded ineger values are the values of the fixtypes uchar, schar, etc. These have the same representation, and thus their constructors and destructors are equivelent. Here we prove these equivalences, leaving them disabled by default; they can be used to prove theorems that involve relations between deep and shallow embedding.
Theorem:
(defthm value-schar-to-schar-from-integer (equal (value-schar x) (schar-from-integer x)))
Theorem:
(defthm value-uchar-to-uchar-from-integer (equal (value-uchar x) (uchar-from-integer x)))
Theorem:
(defthm value-sshort-to-sshort-from-integer (equal (value-sshort x) (sshort-from-integer x)))
Theorem:
(defthm value-ushort-to-ushort-from-integer (equal (value-ushort x) (ushort-from-integer x)))
Theorem:
(defthm value-sint-to-sint-from-integer (equal (value-sint x) (sint-from-integer x)))
Theorem:
(defthm value-uint-to-uint-from-integer (equal (value-uint x) (uint-from-integer x)))
Theorem:
(defthm value-slong-to-slong-from-integer (equal (value-slong x) (slong-from-integer x)))
Theorem:
(defthm value-ulong-to-ulong-from-integer (equal (value-ulong x) (ulong-from-integer x)))
Theorem:
(defthm value-sllong-to-sllong-from-integer (equal (value-sllong x) (sllong-from-integer x)))
Theorem:
(defthm value-ullong-to-ullong-from-integer (equal (value-ullong x) (ullong-from-integer x)))
Theorem:
(defthm value-schar->get-to-integer-from-schar (implies (value-case x :schar) (equal (value-schar->get x) (integer-from-schar x))))
Theorem:
(defthm value-uchar->get-to-integer-from-uchar (implies (value-case x :uchar) (equal (value-uchar->get x) (integer-from-uchar x))))
Theorem:
(defthm value-sshort->get-to-integer-from-sshort (implies (value-case x :sshort) (equal (value-sshort->get x) (integer-from-sshort x))))
Theorem:
(defthm value-ushort->get-to-integer-from-ushort (implies (value-case x :ushort) (equal (value-ushort->get x) (integer-from-ushort x))))
Theorem:
(defthm value-sint->get-to-integer-from-sint (implies (value-case x :sint) (equal (value-sint->get x) (integer-from-sint x))))
Theorem:
(defthm value-uint->get-to-integer-from-uint (implies (value-case x :uint) (equal (value-uint->get x) (integer-from-uint x))))
Theorem:
(defthm value-slong->get-to-integer-from-slong (implies (value-case x :slong) (equal (value-slong->get x) (integer-from-slong x))))
Theorem:
(defthm value-ulong->get-to-integer-from-ulong (implies (value-case x :ulong) (equal (value-ulong->get x) (integer-from-ulong x))))
Theorem:
(defthm value-sllong->get-to-integer-from-sllong (implies (value-case x :sllong) (equal (value-sllong->get x) (integer-from-sllong x))))
Theorem:
(defthm value-ullong->get-to-integer-from-ullong (implies (value-case x :ullong) (equal (value-ullong->get x) (integer-from-ullong x))))