		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Nat=>lendian

Convert a natural number to its little-endian list of digits of specified length.

Signature
(nat=>lendian base width nat) → digits
Arguments: base — Guard (dab-basep base).; width — Guard (natp width).; nat — Guard (natp nat).
Returns: digits — Type (dab-digit-listp base digits).

The number must be representable in the specified number of digits. The resulting list starts with zero or more 0s.

See also nat=>lendian* and nat=>lendian+.

Definitions and Theorems

Function: nat=>lendian

(defun nat=>lendian (base width nat)
  (declare (xargs :guard (and (dab-basep base)
                              (natp width)
                              (natp nat))))
  (declare (xargs :guard (< nat (expt base width))))
  (let ((__function__ 'nat=>lendian))
    (declare (ignorable __function__))
    (b* ((width (mbe :logic (nfix width) :exec width))
         (nat (mbe :logic (mod (nfix nat)
                               (expt (dab-base-fix base) width))
                   :exec nat))
         (digits (nat=>lendian* base nat))
         (zeros (repeat (- width (len digits)) 0)))
      (append digits zeros))))

Theorem: return-type-of-nat=>lendian

(defthm return-type-of-nat=>lendian
  (b* ((digits (nat=>lendian base width nat)))
    (dab-digit-listp base digits))
  :rule-classes :rewrite)

Theorem: nat-listp-of-nat=>lendian

(defthm nat-listp-of-nat=>lendian
  (b* ((digits (nat=>lendian base width nat)))
    (nat-listp digits))
  :rule-classes :rewrite)

Theorem: consp-of-nat=>lendian

(defthm consp-of-nat=>lendian
  (implies (not (zp width))
           (b* ((digits (nat=>lendian base width nat)))
             (consp digits)))
  :rule-classes :type-prescription)

Theorem: nat=>lendian-of-mod

(defthm nat=>lendian-of-mod
 (implies (and (dab-basep base)
               (natp width)
               (natp nat)
               (equal expt-base-width (expt base width)))
          (equal (nat=>lendian base width (mod nat expt-base-width))
                 (nat=>lendian base width nat))))

Theorem: len-of-nat=>lendian

(defthm len-of-nat=>lendian
  (equal (len (nat=>lendian base width nat))
         (nfix width)))

Theorem: nat=>lendian-of-dab-base-fix-base

(defthm nat=>lendian-of-dab-base-fix-base
  (equal (nat=>lendian (dab-base-fix base)
                       width nat)
         (nat=>lendian base width nat)))

Theorem: nat=>lendian-dab-base-equiv-congruence-on-base

(defthm nat=>lendian-dab-base-equiv-congruence-on-base
  (implies (dab-base-equiv base base-equiv)
           (equal (nat=>lendian base width nat)
                  (nat=>lendian base-equiv width nat)))
  :rule-classes :congruence)

Theorem: nat=>lendian-of-nfix-width

(defthm nat=>lendian-of-nfix-width
  (equal (nat=>lendian base (nfix width) nat)
         (nat=>lendian base width nat)))

Theorem: nat=>lendian-nat-equiv-congruence-on-width

(defthm nat=>lendian-nat-equiv-congruence-on-width
  (implies (nat-equiv width width-equiv)
           (equal (nat=>lendian base width nat)
                  (nat=>lendian base width-equiv nat)))
  :rule-classes :congruence)

Theorem: nat=>lendian-of-nfix-nat

(defthm nat=>lendian-of-nfix-nat
  (equal (nat=>lendian base width (nfix nat))
         (nat=>lendian base width nat)))

Theorem: nat=>lendian-nat-equiv-congruence-on-nat

(defthm nat=>lendian-nat-equiv-congruence-on-nat
  (implies (nat-equiv nat nat-equiv)
           (equal (nat=>lendian base width nat)
                  (nat=>lendian base width nat-equiv)))
  :rule-classes :congruence)