		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Group-lendian

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

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

The larger base must be a positive power of the smaller base. The argument base is the smaller base; the argument exp is the positive power that yields the larger base, which is thus base^exp. The order of these two arguments is so that the base comes before the exponent.

The argument digits consists of digits in the smaller base. We first convert the digits to the natural number they represent, and then we convert that to digits in the larger base. This has the effect of grouping each contiguous sub-sequence of exp digits in the smaller base into a single digit in the larger base. The number of input digits must be a multiple of exp, so that they can be evenly grouped into digits in the larget base.

The grouping of digits is little-endian: each sub-sequence of exp digits in the smaller base is converted to a little-endian natural number that becomes a digit in the larger base.

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

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

Definitions and Theorems

Function: group-lendian

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

Theorem: return-type-of-group-lendian

(defthm return-type-of-group-lendian
  (implies (equal base^exp
                  (expt (dab-base-fix base)
                        (pos-fix exp)))
           (b* ((new-digits (group-lendian base exp digits)))
             (dab-digit-listp base^exp new-digits)))
  :rule-classes :rewrite)

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

(defthm group-lendian-of-dab-digit-list-fix-digits
  (equal (group-lendian base
                        exp (dab-digit-list-fix base digits))
         (group-lendian base exp digits)))

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

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

Theorem: len-of-group-lendian

(defthm len-of-group-lendian
  (equal (len (group-lendian base exp digits))
         (ceiling (len digits) (pos-fix exp))))

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

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

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

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

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

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

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

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

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

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