		Search-engine friendly clone of the ACL2 documentation.

Create-nth-choice-count-alist

Create-count-alist

Given a choice list, maps each candidate ID to the number of votes they obtained

Signature
(create-count-alist cids choice-lst) → count-alst
Arguments: cids — All the candidates in the election, sorted.
Guard (nat-listp cids).; choice-lst — Guard (nat-listp choice-lst).
Returns: count-alst — Type (alistp count-alst).

Definitions and Theorems

Function: create-count-alist

(defun create-count-alist (cids choice-lst)
  (declare (xargs :guard (and (nat-listp cids)
                              (nat-listp choice-lst))))
  (let ((__function__ 'create-count-alist))
    (declare (ignorable __function__))
    (if (endp cids)
        nil
      (b* ((cid (car cids))
           (count (acl2::duplicity cid choice-lst)))
        (cons (cons cid count)
              (create-count-alist (cdr cids)
                                  choice-lst))))))

Theorem: alistp-of-create-count-alist

(defthm alistp-of-create-count-alist
  (b* ((count-alst (create-count-alist cids choice-lst)))
    (alistp count-alst))
  :rule-classes :rewrite)

Theorem: count-alistp-of-create-count-alist

(defthm count-alistp-of-create-count-alist
  (b* ((?count-alst (create-count-alist cids choice-lst)))
    (implies (nat-listp cids)
             (count-alistp count-alst))))

Theorem: create-count-alist-of-cids=nil

(defthm create-count-alist-of-cids=nil
  (equal (create-count-alist nil x) nil))

Theorem: consp-of-create-count-alist

(defthm consp-of-create-count-alist
  (equal (consp (create-count-alist cids choice-lst))
         (consp cids)))

Theorem: consp-of-strip-cars-of-create-count-alist

(defthm consp-of-strip-cars-of-create-count-alist
  (implies (consp x)
           (consp (strip-cars (create-count-alist x y)))))

Theorem: consp-of-strip-cdrs-of-create-count-alist

(defthm consp-of-strip-cdrs-of-create-count-alist
  (implies (consp x)
           (consp (strip-cdrs (create-count-alist x y)))))

Theorem: strip-cars-of-create-count-alist-x-y-=-x

(defthm strip-cars-of-create-count-alist-x-y-=-x
  (implies (nat-listp x)
           (equal (strip-cars (create-count-alist x y))
                  x)))

Theorem: strip-cars-of-create-count-alist-is-sorted-if-cids-is-sorted

(defthm strip-cars-of-create-count-alist-is-sorted-if-cids-is-sorted
  (implies (acl2::<-ordered-p cids)
           (acl2::<-ordered-p
                (strip-cars (create-count-alist cids choice-lst)))))

Theorem: strip-cars-of-create-count-alist-equal-under-set-equiv

(defthm strip-cars-of-create-count-alist-equal-under-set-equiv
  (acl2::set-equiv (strip-cars (create-count-alist cids choice-lst))
                   cids))

Theorem: no-duplicatesp-equal-of-strip-cars-of-create-count-alist

(defthm no-duplicatesp-equal-of-strip-cars-of-create-count-alist
  (implies (no-duplicatesp-equal cids)
           (no-duplicatesp-equal
                (strip-cars (create-count-alist cids lst)))))

Theorem: member-of-strip-cars-of-create-count-alist

(defthm member-of-strip-cars-of-create-count-alist
  (b* ((count-alst (create-count-alist cids xs)))
    (implies (member-equal id cids)
             (member-equal id (strip-cars count-alst)))))

Theorem: member-of-strip-cdrs-of-create-count-alist

(defthm member-of-strip-cdrs-of-create-count-alist
  (b* ((count-alst (create-count-alist cids xs)))
    (implies (member-equal id cids)
             (member-equal (cdr (assoc-equal id count-alst))
                           (strip-cdrs count-alst)))))

Theorem: upper-bound-of-duplicity

(defthm upper-bound-of-duplicity
  (<= (acl2::duplicity e x) (len x))
  :rule-classes (:linear :rewrite))

Theorem: len-of-create-count-alist

(defthm len-of-create-count-alist
  (equal (len (create-count-alist x y))
         (len x)))

Theorem: duplicity-is-a-member-of-strip-cdrs-count-alist

(defthm duplicity-is-a-member-of-strip-cdrs-count-alist
  (implies (member-equal e x)
           (member-equal (acl2::duplicity e y)
                         (strip-cdrs (create-count-alist x y)))))

Theorem: duplicity-e-y-is-the-val-of-e-in-count-alist

(defthm duplicity-e-y-is-the-val-of-e-in-count-alist
  (implies (member-equal e x)
           (equal (cdr (assoc-equal e (create-count-alist x y)))
                  (acl2::duplicity e y))))

Theorem: nat-listp-strip-cdrs-count-alist-of-choice-lst

(defthm nat-listp-strip-cdrs-count-alist-of-choice-lst
  (nat-listp (strip-cdrs (create-count-alist x y))))

Subtopics

Count-alistp: Recognizer for a count alist (see create-count-alist)