		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certs-with-authors

Retrieve, from a set of certificates, the subset of certificates with author in a given set.

Signature
(certs-with-authors authors certs) → certs-with-authors
Arguments: authors — Guard (address-setp authors).; certs — Guard (certificate-setp certs).
Returns: certs-with-authors — Type (certificate-setp certs-with-authors).

Definitions and Theorems

Function: certs-with-authors

(defun certs-with-authors (authors certs)
  (declare (xargs :guard (and (address-setp authors)
                              (certificate-setp certs))))
  (let ((__function__ 'certs-with-authors))
    (declare (ignorable __function__))
    (b* (((when (emptyp certs)) nil)
         ((certificate cert) (head certs)))
      (if (in cert.author (address-set-fix authors))
          (insert (certificate-fix cert)
                  (certs-with-authors authors (tail certs)))
        (certs-with-authors authors (tail certs))))))

Theorem: certificate-setp-of-certs-with-authors

(defthm certificate-setp-of-certs-with-authors
  (b* ((certs-with-authors (certs-with-authors authors certs)))
    (certificate-setp certs-with-authors))
  :rule-classes :rewrite)

Theorem: certs-with-authors-of-address-set-fix-authors

(defthm certs-with-authors-of-address-set-fix-authors
  (equal (certs-with-authors (address-set-fix authors)
                             certs)
         (certs-with-authors authors certs)))

Theorem: certs-with-authors-address-set-equiv-congruence-on-authors

(defthm certs-with-authors-address-set-equiv-congruence-on-authors
  (implies (address-set-equiv authors authors-equiv)
           (equal (certs-with-authors authors certs)
                  (certs-with-authors authors-equiv certs)))
  :rule-classes :congruence)

Theorem: certs-with-authors-subset

(defthm certs-with-authors-subset
 (implies
      (certificate-setp certs)
      (b* ((?certs-with-authors (certs-with-authors authors certs)))
        (subset certs-with-authors certs))))

Theorem: certs-with-authors-of-nil

(defthm certs-with-authors-of-nil
  (equal (certs-with-author authors nil)
         nil))

Theorem: in-of-certs-with-authors

(defthm in-of-certs-with-authors
  (implies (certificate-setp certs)
           (equal (in cert (certs-with-authors authors certs))
                  (and (in cert certs)
                       (in (certificate->author cert)
                           (address-set-fix authors))))))

Theorem: cert-set->author-set-of-certs-with-authors

(defthm cert-set->author-set-of-certs-with-authors
 (implies
    (certificate-setp certs)
    (equal (cert-set->author-set (certs-with-authors authors certs))
           (intersect (address-set-fix authors)
                      (cert-set->author-set certs)))))