Fixtype of sizes in bits of the integer values.
These are all the integer multiples of 8 from 8 to 256.
This is a type defined by fty::deffixtype.
Function:
(defun bit-size-p (x) (declare (xargs :guard t)) (and (integerp x) (integerp (/ x 8)) (<= 8 x) (<= x 256)))
Theorem:
(defthm booleanp-of-bit-size-p (b* ((yes/no (bit-size-p x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm bit-size-p-alt-def (iff (bit-size-p x) (member x (list 8 16 24 32 40 48 56 64 72 80 88 96 104 112 120 128 136 144 152 160 168 176 184 192 200 208 216 224 232 240 248 256))))
Function:
(defun bit-size-fix (x) (declare (xargs :guard (bit-size-p x))) (mbe :logic (if (bit-size-p x) x 256) :exec x))
Theorem:
(defthm bit-size-p-of-bit-size-fix (b* ((fixed-x (bit-size-fix x))) (bit-size-p fixed-x)) :rule-classes :rewrite)
Theorem:
(defthm bit-size-fix-when-bit-size-p (implies (bit-size-p x) (equal (bit-size-fix x) x)))
Theorem:
(defthm posp-of-bit-size-fix (posp (bit-size-fix x)) :rule-classes :type-prescription)
Function:
(defun bit-size-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (bit-size-p acl2::x) (bit-size-p acl2::y)))) (equal (bit-size-fix acl2::x) (bit-size-fix acl2::y)))
Theorem:
(defthm bit-size-equiv-is-an-equivalence (and (booleanp (bit-size-equiv x y)) (bit-size-equiv x x) (implies (bit-size-equiv x y) (bit-size-equiv y x)) (implies (and (bit-size-equiv x y) (bit-size-equiv y z)) (bit-size-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm bit-size-equiv-implies-equal-bit-size-fix-1 (implies (bit-size-equiv acl2::x x-equiv) (equal (bit-size-fix acl2::x) (bit-size-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm bit-size-fix-under-bit-size-equiv (bit-size-equiv (bit-size-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-bit-size-fix-1-forward-to-bit-size-equiv (implies (equal (bit-size-fix acl2::x) acl2::y) (bit-size-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-bit-size-fix-2-forward-to-bit-size-equiv (implies (equal acl2::x (bit-size-fix acl2::y)) (bit-size-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm bit-size-equiv-of-bit-size-fix-1-forward (implies (bit-size-equiv (bit-size-fix acl2::x) acl2::y) (bit-size-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm bit-size-equiv-of-bit-size-fix-2-forward (implies (bit-size-equiv acl2::x (bit-size-fix acl2::y)) (bit-size-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)