		Search-engine friendly clone of the ACL2 documentation.

Charlist-codelist-conversions

Chars=>nats

Convert a true list of characters to the corresponding true list of natural numbers below 256.

Signature
(chars=>nats chars) → nats
Arguments: chars — Guard (character-listp chars).
Returns: nats — Type (unsigned-byte-listp 8 nats).

This operation has a natural-recursive definition for logic reasoning and a tail-recursive executional for execution.

Definitions and Theorems

Function: chars=>nats-exec

(defun chars=>nats-exec (chars rev-nats)
  (declare (xargs :guard (and (character-listp chars)
                              (unsigned-byte-listp 8 rev-nats))))
  (let ((__function__ 'chars=>nats-exec))
    (declare (ignorable __function__))
    (cond ((endp chars) (rev rev-nats))
          (t (chars=>nats-exec (cdr chars)
                               (cons (char-code (car chars))
                                     rev-nats))))))

Function: chars=>nats

(defun chars=>nats (chars)
  (declare (xargs :guard (character-listp chars)))
  (let ((__function__ 'chars=>nats))
    (declare (ignorable __function__))
    (mbe :logic (cond ((endp chars) nil)
                      (t (cons (char-code (car chars))
                               (chars=>nats (cdr chars)))))
         :exec (chars=>nats-exec chars nil))))

Theorem: return-type-of-chars=>nats

(defthm return-type-of-chars=>nats
  (b* ((nats (chars=>nats chars)))
    (unsigned-byte-listp 8 nats))
  :rule-classes :rewrite)

Theorem: nat-listp-of-chars=>nats

(defthm nat-listp-of-chars=>nats
  (b* ((nats (chars=>nats chars)))
    (nat-listp nats))
  :rule-classes :rewrite)

Theorem: integer-listp-of-chars=>nats

(defthm integer-listp-of-chars=>nats
  (b* ((nats (chars=>nats chars)))
    (integer-listp nats))
  :rule-classes :rewrite)

Theorem: len-of-chars=>nats

(defthm len-of-chars=>nats
  (equal (len (chars=>nats chars))
         (len chars)))

Theorem: chars=>nats-of-cons

(defthm chars=>nats-of-cons
  (equal (chars=>nats (cons char chars))
         (cons (char-code char)
               (chars=>nats chars))))

Theorem: chars=>nats-of-append

(defthm chars=>nats-of-append
  (equal (chars=>nats (append chars1 chars2))
         (append (chars=>nats chars1)
                 (chars=>nats chars2))))

Theorem: chars=>nats-of-repeat

(defthm chars=>nats-of-repeat
  (equal (chars=>nats (repeat n char))
         (repeat n (char-code char))))

Theorem: car-of-chars=>nats

(defthm car-of-chars=>nats
  (equal (car (chars=>nats chars))
         (and (consp chars)
              (char-code (car chars)))))

Theorem: nth-of-chars=>nats

(defthm nth-of-chars=>nats
  (equal (nth i (chars=>nats chars))
         (if (< (nfix i) (len chars))
             (char-code (nth i chars))
           nil)))

Theorem: chars=>nats-of-make-character-list

(defthm chars=>nats-of-make-character-list
  (equal (chars=>nats (make-character-list x))
         (chars=>nats x)))

Theorem: consp-of-chars=>nats

(defthm consp-of-chars=>nats
  (iff (consp (chars=>nats chars))
       (consp chars)))

Theorem: chars=>nats-of-make-list-ac

(defthm chars=>nats-of-make-list-ac
  (equal (chars=>nats (make-list-ac n val ac))
         (make-list-ac n (char-code val)
                       (chars=>nats ac))))

Theorem: chars=>nats-of-take

(defthm chars=>nats-of-take
  (implies (<= (nfix n) (len chars))
           (equal (chars=>nats (take n chars))
                  (take n (chars=>nats chars)))))

Theorem: chars=>nats-of-nthcdr

(defthm chars=>nats-of-nthcdr
  (equal (chars=>nats (nthcdr n chars))
         (nthcdr n (chars=>nats chars))))

Theorem: chars=>nats-of-revappend

(defthm chars=>nats-of-revappend
  (equal (chars=>nats (revappend x y))
         (revappend (chars=>nats x)
                    (chars=>nats y))))

Theorem: chars=>nats-of-make-character-list-chars

(defthm chars=>nats-of-make-character-list-chars
  (equal (chars=>nats (make-character-list chars))
         (chars=>nats chars)))

Theorem: chars=>nats-charlisteqv-congruence-on-chars

(defthm chars=>nats-charlisteqv-congruence-on-chars
  (implies (str::charlisteqv chars chars-equiv)
           (equal (chars=>nats chars)
                  (chars=>nats chars-equiv)))
  :rule-classes :congruence)

Subtopics

Nats<=>chars-inverses-theorems: nats=>chars and chars=>nats are mutual inverses.