Theorems about Java binary digits and functions in Std/strings.
Theorem:
(defthm bin-digitp-of-char-code (equal (bin-digitp (char-code char)) (str::bin-digit-char-p char)))
Theorem:
(defthm bin-digit-listp-of-chars=>nats (equal (bin-digit-listp (chars=>nats chars)) (str::bin-digit-char-list*p chars)))