		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Ungroup-lendian

Ungroup digits from a larger base to a smaller base, little-endian.

Signature
(ungroup-lendian base exp digits) → new-digits
Arguments: base — Guard (dab-basep base).; exp — Guard (posp exp).; digits — Guard (dab-digit-listp (expt (dab-base-fix base) (pos-fix exp)) digits).
Returns: new-digits — Type (dab-digit-listp base new-digits).

This is the inverse of group-lendian. As in that function, the argument base is the smaller base, and the argument exp is such that base^exp is the larger base. The digits argument consists of the digits in the larger base. Each input digit in the larger base is converted to exp digits in the smaller base, little-endian.

This operation is useful, for example, to turn a sequence of bytes into one of nibbles, or a sequence of bytes into one of bits, or a sequence of numbers below 100 into one of numbers below 10.

As a degenerate case, if exp is 1, this operation leaves the digits unchanged.

Definitions and Theorems

Function: ungroup-lendian

(defun ungroup-lendian (base exp digits)
 (declare
  (xargs
      :guard
      (and (dab-basep base)
           (posp exp)
           (dab-digit-listp (expt (dab-base-fix base) (pos-fix exp))
                            digits))))
 (let ((__function__ 'ungroup-lendian))
   (declare (ignorable __function__))
   (b* ((exp (pos-fix exp))
        (base^exp (expt (dab-base-fix base) exp))
        (nat (lendian=>nat base^exp digits))
        (number-of-new-digits (* (len digits) exp))
        (new-digits (nat=>lendian base number-of-new-digits nat)))
     new-digits)))

Theorem: return-type-of-ungroup-lendian

(defthm return-type-of-ungroup-lendian
  (b* ((new-digits (ungroup-lendian base exp digits)))
    (dab-digit-listp base new-digits))
  :rule-classes :rewrite)

Theorem: ungroup-lendian-of-dab-digit-list-fix-digits

(defthm ungroup-lendian-of-dab-digit-list-fix-digits
  (implies
       (equal base^exp
              (expt (dab-base-fix base)
                    (pos-fix exp)))
       (equal (ungroup-lendian base exp
                               (dab-digit-list-fix base^exp digits))
              (ungroup-lendian base exp digits))))

Theorem: ungroup-lendian-of-dab-digit-list-fix-digits-normalize-const

(defthm ungroup-lendian-of-dab-digit-list-fix-digits-normalize-const
 (implies
  (syntaxp (and (quotep digits)
                (not (dab-digit-listp base (cadr digits)))))
  (equal
   (ungroup-lendian base exp digits)
   (ungroup-lendian
        base exp
        (dab-digit-list-fix (expt (dab-base-fix base) (pos-fix exp))
                            digits)))))

Theorem: len-of-ungroup-lendian

(defthm len-of-ungroup-lendian
  (equal (len (ungroup-lendian base exp digits))
         (* (len digits) (pos-fix exp))))

Theorem: ungroup-lendian-when-exp-is-1

(defthm ungroup-lendian-when-exp-is-1
  (equal (ungroup-lendian base 1 digits)
         (dab-digit-list-fix base digits)))

Theorem: ungroup-lendian-of-dab-base-fix-base

(defthm ungroup-lendian-of-dab-base-fix-base
  (equal (ungroup-lendian (dab-base-fix base)
                          exp digits)
         (ungroup-lendian base exp digits)))

Theorem: ungroup-lendian-dab-base-equiv-congruence-on-base

(defthm ungroup-lendian-dab-base-equiv-congruence-on-base
  (implies (dab-base-equiv base base-equiv)
           (equal (ungroup-lendian base exp digits)
                  (ungroup-lendian base-equiv exp digits)))
  :rule-classes :congruence)

Theorem: ungroup-lendian-of-pos-fix-exp

(defthm ungroup-lendian-of-pos-fix-exp
  (equal (ungroup-lendian base (pos-fix exp)
                          digits)
         (ungroup-lendian base exp digits)))

Theorem: ungroup-lendian-pos-equiv-congruence-on-exp

(defthm ungroup-lendian-pos-equiv-congruence-on-exp
  (implies (pos-equiv exp exp-equiv)
           (equal (ungroup-lendian base exp digits)
                  (ungroup-lendian base exp-equiv digits)))
  :rule-classes :congruence)