digit-to-char

(in-package "ACL2")

(in-theory (disable digit-to-char))

(defthm our-digit-char-p-of-digit-to-char
  (implies (and (natp n) (< n radix))
    (our-digit-char-p (digit-to-char n) radix))
  :hints (("Goal" :in-theory (enable our-digit-char-p digit-to-char))))

(defthm our-digit-char-p-of-digit-to-char-gen
  (implies (< 0 radix)
    (iff (our-digit-char-p (digit-to-char n) radix)
      (if (and (< n 16) (natp n))
        (< n radix)
        t)))
  :hints (("Goal" :in-theory (enable our-digit-char-p digit-to-char))))

(defthm equal-of-0-and-digit-to-char
  (equal (equal #\0 (digit-to-char n))
    (or (equal n 0) (not (natp n)) (< 15 n)))
  :hints (("Goal" :in-theory (enable digit-to-char))))

(defthm equal-of-digit-to-char-and-digit-to-char
  (equal (equal (digit-to-char n1) (digit-to-char n2))
    (if (or (zp n1) (< 15 n1))
      (or (zp n2) (< 15 n2))
      (equal n1 n2)))
  :hints (("Goal" :in-theory (enable digit-to-char))))