explode-nonnegative-integer

Included Books

decimal quotient-remainder-lemmas revappend append rev

other

(in-package "ACL2")

include-book

(include-book "decimal")

local

(local (include-book "ihs/quotient-remainder-lemmas" :dir :system))

local

(local (include-book "std/lists/revappend" :dir :system))

local

(local (include-book "std/lists/append" :dir :system))

local

(local (in-theory (e/d (print-base-p) (floor mod))))

local

(local (defun simpler-explode-nonnegative-integer
    (n base ans)
    (declare (xargs :guard (and (integerp n) (<= 0 n) (print-base-p base))))
    (if (or (zp n) (not (print-base-p base)))
      ans
      (simpler-explode-nonnegative-integer (floor n base)
        base
        (cons (digit-to-char (mod n base)) ans)))))

local

(local (defthm explode-nonnegative-integer-redefinition
    (equal (explode-nonnegative-integer n base ans)
      (or (simpler-explode-nonnegative-integer n base ans) '(#\0)))
    :rule-classes ((:definition :install-body nil))))

local

(local (in-theory (disable (:definition explode-nonnegative-integer))))

local

(local (defun basic-eni-core
    (n base)
    (declare (xargs :guard (and (natp n) (print-base-p base))))
    (if (or (zp n) (not (print-base-p base)))
      nil
      (cons (digit-to-char (mod n base))
        (basic-eni-core (floor n base) base)))))

local

(local (defun basic-eni-induction
    (n m base)
    (declare (xargs :guard (and (natp n) (natp m) (print-base-p base))))
    (cond ((zp n) nil)
      ((zp m) nil)
      ((not (print-base-p base)) nil)
      (t (basic-eni-induction (floor n base) (floor m base) base)))))

local

(local (defthm basic-eni-core-under-iff
    (iff (basic-eni-core n base)
      (and (not (zp n)) (print-base-p base)))))

local

(local (defthm consp-of-basic-eni-core
    (equal (consp (basic-eni-core n base))
      (and (not (zp n))
        (if (print-base-p base)
          t
          nil)))
    :hints (("Goal" :expand (basic-eni-core n base)))))

local

(local (defthm equal-of-basic-eni-cores
    (implies (force (print-base-p base))
      (equal (equal (basic-eni-core n base) (basic-eni-core m base))
        (equal (nfix n) (nfix m))))
    :hints (("Goal" :in-theory (disable basic-eni-core)
       :induct (basic-eni-induction n m base)
       :expand ((:free (base) (basic-eni-core n base)) (:free (base) (basic-eni-core m base)))
       :do-not '(generalize fertilize)))))

local

(local (defthm equal-of-basic-eni-core-with-list-zero
    (not (equal (basic-eni-core n base) '(#\0)))
    :hints (("Goal" :in-theory (enable digit-to-char)))))

local

(local (defthm basic/simpler-equivalence
    (equal (simpler-explode-nonnegative-integer n base acc)
      (revappend (basic-eni-core n base) acc))))

local

(local (defthm equal-of-simpler-explode-nonnegative-integers
    (implies (force (print-base-p base))
      (equal (equal (simpler-explode-nonnegative-integer n base acc)
          (simpler-explode-nonnegative-integer m base acc))
        (equal (nfix n) (nfix m))))))

local

(local (defthm simpler-eni-when-nonzero
    (implies (and (not (zp n)) (print-base-p base))
      (simpler-explode-nonnegative-integer n base acc))))

local

(local (defthm simpler-eni-degenerate-lemma
    (equal (equal (simpler-explode-nonnegative-integer n base acc)
        '(#\0))
      (and (equal acc '(#\0))
        (or (zp n) (not (print-base-p base)))))
    :hints (("Goal" :induct (simpler-explode-nonnegative-integer n base acc)
       :expand ((:free (base) (basic-eni-core n base)))
       :in-theory (e/d (digit-to-char) (basic-eni-core))))))

local

(local (defthm not-of-simpler-explode-nonnegative-integer
    (equal (not (simpler-explode-nonnegative-integer n base acc))
      (and (equal acc nil) (or (zp n) (not (print-base-p base)))))))

local

(local (defthm true-listp-of-simpler-explode-nonnegative-integer
    (equal (true-listp (simpler-explode-nonnegative-integer n base acc))
      (true-listp acc))))

local

(local (defthm equal-of-explode-nonnegative-integers-lemma
    (implies (and (natp n)
        (natp m)
        (not (equal n m))
        (not (simpler-explode-nonnegative-integer n base acc))
        (force (print-base-p base)))
      (simpler-explode-nonnegative-integer m base acc))))

equal-of-explode-nonnegative-integerstheorem

(defthm equal-of-explode-nonnegative-integers
  (implies (and (natp n) (natp m) (force (print-base-p base)))
    (equal (equal (explode-nonnegative-integer n base acc)
        (explode-nonnegative-integer m base acc))
      (equal n m)))
  :hints (("Goal" :in-theory (disable simpler-explode-nonnegative-integer
       basic/simpler-equivalence))))

true-listp-of-explode-nonnegative-integertheorem

(defthm true-listp-of-explode-nonnegative-integer
  (equal (true-listp (explode-nonnegative-integer n base acc))
    (true-listp acc)))

true-listp-of-explode-nonnegative-integer-typetheorem

(defthm true-listp-of-explode-nonnegative-integer-type
  (implies (true-listp acc)
    (true-listp (explode-nonnegative-integer n base acc)))
  :rule-classes :type-prescription)

character-listp-of-explode-nonnegative-integertheorem

(defthm character-listp-of-explode-nonnegative-integer
  (equal (character-listp (explode-nonnegative-integer n base acc))
    (character-listp acc)))

local

(local (defthm dec-digit-char-list*p-of-basic-eni-core
    (dec-digit-char-list*p (basic-eni-core n 10))))

local

(local (defthm dec-digit-char-list*p-of-simpler-eni
    (implies (dec-digit-char-list*p acc)
      (dec-digit-char-list*p (simpler-explode-nonnegative-integer n 10 acc)))))

dec-digit-char-list*p-of-explode-nonnegative-integertheorem

(defthm dec-digit-char-list*p-of-explode-nonnegative-integer
  (implies (dec-digit-char-list*p acc)
    (dec-digit-char-list*p (explode-nonnegative-integer n 10 acc))))

nonzeroness-of-explode-nonnegative-integer-when-nonzeroencapsulate

(encapsulate nil
  (local (in-theory (disable revappend-removal)))
  (local (defthm lemma
      (equal (equal (revappend x acc) '(#\0))
        (or (and (equal acc nil)
            (consp x)
            (equal (car x) #\0)
            (atom (cdr x)))
          (and (equal acc '(#\0)) (atom x))))))
  (local (defthm lemma2
      (implies (and (not (zp n)) (print-base-p base))
        (consp (basic-eni-core n base)))))
  (defthm nonzeroness-of-explode-nonnegative-integer-when-nonzero
    (implies (and (not (zp n)) (force (print-base-p base)))
      (not (equal (explode-nonnegative-integer n base nil) '(#\0))))
    :hints (("Goal" :in-theory (e/d (digit-to-char) (basic-eni-core))
       :expand ((:free (base) (basic-eni-core n base)))))))

dec-digit-char-value-of-digit-to-chartheorem

(defthm dec-digit-char-value-of-digit-to-char
  (implies (and (force (natp n)) (force (<= 0 n)) (force (<= n 9)))
    (equal (dec-digit-char-value (digit-to-char n)) n))
  :hints (("Goal" :in-theory (enable dec-digit-char-value digit-to-char))))

other

(defsection digit-to-char-of-dec-digit-char-value
  (local (defun test
      (n)
      (declare (xargs :ruler-extenders :all))
      (and (let ((char (code-char n)))
          (or (not (dec-digit-char-p char))
            (equal (digit-to-char (dec-digit-char-value char))
              char)))
        (if (zp n)
          t
          (test (- n 1))))))
  (local (defthm l0
      (implies (and (test n) (natp i) (natp n) (<= i n))
        (let ((char (code-char i)))
          (implies (dec-digit-char-p char)
            (equal (digit-to-char (dec-digit-char-value char))
              char))))))
  (local (defthm l1
      (implies (and (natp i) (<= i 255))
        (let ((char (code-char i)))
          (implies (dec-digit-char-p char)
            (equal (digit-to-char (dec-digit-char-value char))
              char))))
      :hints (("Goal" :use ((:instance l0 (n 255)))))))
  (defthm digit-to-char-of-dec-digit-char-value
    (implies (dec-digit-char-p char)
      (equal (digit-to-char (dec-digit-char-value char))
        char))
    :hints (("Goal" :use ((:instance l1 (i (char-code char))))))))

basic-unexplode-corefunction

(defund basic-unexplode-core
  (x)
  (declare (xargs :guard (and (character-listp x) (dec-digit-char-list*p x))))
  (if (consp x)
    (+ (dec-digit-char-value (car x))
      (* 10 (basic-unexplode-core (cdr x))))
    0))

local

(local (defthm basic-unexplode-core-of-basic-eni-core
    (implies (force (natp n))
      (equal (basic-unexplode-core (basic-eni-core n 10)) n))
    :hints (("Goal" :in-theory (enable basic-eni-core basic-unexplode-core)))))

unexplode-nonnegative-integerfunction

(defund unexplode-nonnegative-integer
  (x)
  (declare (xargs :guard (and (character-listp x) (dec-digit-char-list*p x))))
  (basic-unexplode-core (revappend x nil)))

unexplode-nonnegative-integer-of-explode-nonnegative-integerencapsulate

(encapsulate nil
  (local (include-book "std/lists/rev" :dir :system))
  (defthm unexplode-nonnegative-integer-of-explode-nonnegative-integer
    (implies (force (natp n))
      (equal (unexplode-nonnegative-integer (explode-nonnegative-integer n 10 nil))
        n))
    :hints (("Goal" :in-theory (e/d (unexplode-nonnegative-integer) (basic-eni-core))))))