Turn an ACL2 boolean into an
This is essentially (but not exactly)
the inverse of boolean-from-sint.
Together with boolean-from-sint
and other
Function:
(defun sint-from-boolean (b) (declare (xargs :guard (booleanp b))) (if b (sint-from-integer 1) (sint-from-integer 0)))
Theorem:
(defthm sintp-of-sint-from-boolean (b* ((x (sint-from-boolean b))) (sintp x)) :rule-classes :rewrite)
Theorem:
(defthm sint-from-boolean-of-bool-fix-b (equal (sint-from-boolean (acl2::bool-fix b)) (sint-from-boolean b)))
Theorem:
(defthm sint-from-boolean-iff-congruence-on-b (implies (iff b b-equiv) (equal (sint-from-boolean b) (sint-from-boolean b-equiv))) :rule-classes :congruence)