nat-to-string - ACL2 Book

Included Books

all-digit-charsp coerce our-digit-char-p explode-nonnegative-integer

other

(in-package "ACL2")

include-book

(include-book "kestrel/typed-lists-light/all-digit-charsp" :dir :system)

local

(local (include-book "coerce"))

local

(local (include-book "our-digit-char-p"))

local

(local (include-book "explode-nonnegative-integer"))

nat-to-charsfunction

(defund nat-to-chars
  (n)
  (declare (xargs :guard (natp n) :split-types t)
    (type (integer 0 *) n))
  (explode-nonnegative-integer n 10 nil))

character-listp-of-nat-to-charstheorem

(defthm character-listp-of-nat-to-chars
  (character-listp (nat-to-chars n))
  :hints (("Goal" :in-theory (enable nat-to-chars))))

equal-of-nat-to-chars-and-nat-to-charstheorem

(defthm equal-of-nat-to-chars-and-nat-to-chars
  (equal (equal (nat-to-chars n1) (nat-to-chars n2))
    (equal (nfix n1) (nfix n2)))
  :hints (("Goal" :in-theory (enable nat-to-chars))))

all-digit-charsp-of-nat-to-chars-and-10theorem

(defthm all-digit-charsp-of-nat-to-chars-and-10
  (all-digit-charsp (nat-to-chars n) 10)
  :hints (("Goal" :in-theory (enable nat-to-chars))))

nat-to-stringfunction

(defund nat-to-string
  (n)
  (declare (xargs :guard (natp n) :split-types t)
    (type (integer 0 *) n))
  (coerce (nat-to-chars n) 'string))

equal-of-nat-to-string-and-nat-to-stringtheorem

(defthm equal-of-nat-to-string-and-nat-to-string
  (equal (equal (nat-to-string n1) (nat-to-string n2))
    (equal (nfix n1) (nfix n2)))
  :hints (("Goal" :in-theory (enable nat-to-string))))

not-equal-of-nat-to-string-and-empty-stringtheorem

(defthm not-equal-of-nat-to-string-and-empty-string
  (not (equal (nat-to-string n) ""))
  :hints (("Goal" :in-theory (enable nat-to-string))))