		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certs-with-author

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

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

Definitions and Theorems

Function: certs-with-author

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

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

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

Theorem: certs-with-author-of-address-fix-author

(defthm certs-with-author-of-address-fix-author
  (equal (certs-with-author (address-fix author)
                            certs)
         (certs-with-author author certs)))

Theorem: certs-with-author-address-equiv-congruence-on-author

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

Theorem: certs-with-author-subset

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

Theorem: certs-with-author-of-nil

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

Theorem: emptyp-of-certs-with-author-to-no-author

(defthm emptyp-of-certs-with-author-to-no-author
  (implies (certificate-setp certs)
           (equal (emptyp (certs-with-author author certs))
                  (not (in (address-fix author)
                           (cert-set->author-set certs))))))

Theorem: in-of-certs-with-author

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

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

(defthm cert-set->author-set-of-certs-with-author
 (implies
      (certificate-setp certs)
      (equal (cert-set->author-set (certs-with-author author certs))
             (if (in (address-fix author)
                     (cert-set->author-set certs))
                 (insert (address-fix author) nil)
               nil))))

Theorem: certificate->author-of-head-of-certs-with-author

(defthm certificate->author-of-head-of-certs-with-author
 (implies
  (and (certificate-setp certs)
       (not (emptyp (certs-with-author author certs))))
  (equal
       (certificate->author (head (certs-with-author author certs)))
       (address-fix author))))

Theorem: in-cert-set->author-set-to-nonempty-certs-with-author

(defthm in-cert-set->author-set-to-nonempty-certs-with-author
 (implies
     (certificate-setp certs)
     (equal (in author (cert-set->author-set certs))
            (and (addressp author)
                 (not (emptyp (certs-with-author author certs)))))))

Theorem: certs-with-author-of-insert

(defthm certs-with-author-of-insert
  (implies (and (certificatep cert)
                (certificate-setp certs))
           (equal (certs-with-author author (insert cert certs))
                  (if (equal (certificate->author cert)
                             (address-fix author))
                      (insert cert (certs-with-author author certs))
                    (certs-with-author author certs)))))

Theorem: certs-with-author-of-delete

(defthm certs-with-author-of-delete
  (implies (certificate-setp certs)
           (equal (certs-with-author author (delete cert certs))
                  (delete cert
                          (certs-with-author author certs)))))

Theorem: cert-with-author+round-in-certs-with-author

(defthm cert-with-author+round-in-certs-with-author
  (implies (and (certificate-setp certs)
                (cert-with-author+round author round certs))
           (in (cert-with-author+round author round certs)
               (certs-with-author author certs))))

Theorem: no-cert-with-author+round-if-no-certs-with-author

(defthm no-cert-with-author+round-if-no-certs-with-author
  (implies (and (certificate-setp certs)
                (equal (certs-with-author author certs)
                       nil))
           (not (cert-with-author+round author round certs))))

Theorem: head-of-certs-with-author-in-certs-when-author-in-authors

(defthm head-of-certs-with-author-in-certs-when-author-in-authors
  (implies (certificate-setp certs)
           (implies (in author (cert-set->author-set certs))
                    (in (head (certs-with-author author certs))
                        certs))))