|
|
|---|
|
|
|
|---|
Theorems about certain conversions from unsigned to signed being always allowed for certain integer type sizes.
We prove these theorems in a general way, with hypotheses on the integer type sizes, disabling the rules that may otherwise obviate the hypotheses.
Theorem:
(defthm sint-from-uchar-okp-when-uchar-max-<=-sint-max (implies (<= (uchar-max) (sint-max)) (sint-from-uchar-okp x)))
Theorem:
(defthm sint-from-ushort-okp-when-ushort-max-<=-sint-max (implies (<= (ushort-max) (sint-max)) (sint-from-ushort-okp x)))
Theorem:
(defthm slong-from-uchar-okp-when-uchar-max-<=slong-max (implies (<= (uchar-max) (slong-max)) (slong-from-uchar-okp x)))
Theorem:
(defthm slong-from-ushort-okp-when-ushort-max-<=slong-max (implies (<= (ushort-max) (slong-max)) (slong-from-ushort-okp x)))
Theorem:
(defthm slong-from-uint-okp-when-uint-max-<=slong-max (implies (<= (uint-max) (slong-max)) (slong-from-uint-okp x)))
Theorem:
(defthm sllong-from-uchar-okp-when-uchar-max-<=sllong-max (implies (<= (uchar-max) (sllong-max)) (sllong-from-uchar-okp x)))
Theorem:
(defthm sllong-from-ushort-okp-when-ushort-max-<=sllong-max (implies (<= (ushort-max) (sllong-max)) (sllong-from-ushort-okp x)))
Theorem:
(defthm sllong-from-uint-okp-when-uint-max-<=sllong-max (implies (<= (uint-max) (sllong-max)) (sllong-from-uint-okp x)))
Theorem:
(defthm sllong-from-ulong-okp-when-ulong-max-<=sllong-max (implies (<= (ulong-max) (sllong-max)) (sllong-from-ulong-okp x)))