		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Group-bendian

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

Signature
(group-bendian 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))).

This is analogous to group-lendian, but each sub-sequence of exp digits in the smaller base is converted to a big-endian number as a digit in the larger base.

Definitions and Theorems

Function: group-bendian

(defun group-bendian (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-bendian))
   (declare (ignorable __function__))
   (b*
     ((exp (pos-fix exp))
      (base^exp (expt (dab-base-fix base) exp))
      (nat (bendian=>nat base digits))
      (number-of-new-digits (ceiling (len digits) exp))
      (new-digits (nat=>bendian base^exp number-of-new-digits nat)))
     new-digits)))

Theorem: return-type-of-group-bendian

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

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

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

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

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

Theorem: len-of-group-bendian

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

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

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

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

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

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

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

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

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

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

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