		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-modinsts-rem-dups

Signature
(elab-modinsts-rem-dups x) → xx
Arguments: x — Guard (elab-modinst-list-p x).
Returns: xx — Type (elab-modinsts-nodups-p xx).

Definitions and Theorems

Function: elab-modinsts-rem-dups

(defun elab-modinsts-rem-dups (x)
  (declare (xargs :guard (elab-modinst-list-p x)))
  (let ((__function__ 'elab-modinsts-rem-dups))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (elab-modinst-fix (car x))
            (elab-modinst-remove-name
                 (nth *elab-modinst$c->instname* (car x))
                 (elab-modinsts-rem-dups (cdr x)))))))

Theorem: elab-modinsts-nodups-p-of-elab-modinsts-rem-dups

(defthm elab-modinsts-nodups-p-of-elab-modinsts-rem-dups
  (b* ((xx (elab-modinsts-rem-dups x)))
    (elab-modinsts-nodups-p xx))
  :rule-classes :rewrite)

Theorem: elab-modinst-list-names-of-remove-duplicate-names

(defthm elab-modinst-list-names-of-remove-duplicate-names
  (equal
       (elab-modinst-list-names (elab-modinsts-rem-dups x))
       (acl2::remove-later-duplicates (elab-modinst-list-names x))))

Theorem: elab-modinsts-rem-dups-when-no-duplicates

(defthm elab-modinsts-rem-dups-when-no-duplicates
  (implies (no-duplicatesp (elab-modinst-list-names x))
           (equal (elab-modinsts-rem-dups x)
                  (elab-modinst-list-fix x))))

Theorem: elab-modinsts-rem-dups-when-elab-modinsts-nodups-p

(defthm elab-modinsts-rem-dups-when-elab-modinsts-nodups-p
  (implies (elab-modinsts-nodups-p x)
           (equal (elab-modinsts-rem-dups x) x)))

Theorem: no-duplicate-names-of-elab-modinsts-rem-dups

(defthm no-duplicate-names-of-elab-modinsts-rem-dups
  (no-duplicatesp
       (elab-modinst-list-names (elab-modinsts-rem-dups x))))

Theorem: elab-modinsts-rem-dups-of-elab-modinst-list-fix-x

(defthm elab-modinsts-rem-dups-of-elab-modinst-list-fix-x
  (equal (elab-modinsts-rem-dups (elab-modinst-list-fix x))
         (elab-modinsts-rem-dups x)))

Theorem: elab-modinsts-rem-dups-elab-modinst-list-equiv-congruence-on-x

(defthm
     elab-modinsts-rem-dups-elab-modinst-list-equiv-congruence-on-x
  (implies (elab-modinst-list-equiv x x-equiv)
           (equal (elab-modinsts-rem-dups x)
                  (elab-modinsts-rem-dups x-equiv)))
  :rule-classes :congruence)

Function: elab-modinsts-nodups-equiv$inline

(defun elab-modinsts-nodups-equiv$inline (x y)
  (declare (xargs :guard (and (elab-modinsts-nodups-p x)
                              (elab-modinsts-nodups-p y))))
  (equal (elab-modinsts-rem-dups x)
         (elab-modinsts-rem-dups y)))

Theorem: elab-modinsts-nodups-equiv-is-an-equivalence

(defthm elab-modinsts-nodups-equiv-is-an-equivalence
  (and (booleanp (elab-modinsts-nodups-equiv x y))
       (elab-modinsts-nodups-equiv x x)
       (implies (elab-modinsts-nodups-equiv x y)
                (elab-modinsts-nodups-equiv y x))
       (implies (and (elab-modinsts-nodups-equiv x y)
                     (elab-modinsts-nodups-equiv y z))
                (elab-modinsts-nodups-equiv x z)))
  :rule-classes (:equivalence))

Theorem: elab-modinsts-nodups-equiv-implies-equal-elab-modinsts-rem-dups-1

(defthm
  elab-modinsts-nodups-equiv-implies-equal-elab-modinsts-rem-dups-1
  (implies (elab-modinsts-nodups-equiv x x-equiv)
           (equal (elab-modinsts-rem-dups x)
                  (elab-modinsts-rem-dups x-equiv)))
  :rule-classes (:congruence))

Theorem: elab-modinsts-rem-dups-under-elab-modinsts-nodups-equiv

(defthm elab-modinsts-rem-dups-under-elab-modinsts-nodups-equiv
  (elab-modinsts-nodups-equiv (elab-modinsts-rem-dups x)
                              x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-elab-modinsts-rem-dups-1-forward-to-elab-modinsts-nodups-equiv

(defthm
 equal-of-elab-modinsts-rem-dups-1-forward-to-elab-modinsts-nodups-equiv
 (implies (equal (elab-modinsts-rem-dups x) y)
          (elab-modinsts-nodups-equiv x y))
 :rule-classes :forward-chaining)

Theorem: equal-of-elab-modinsts-rem-dups-2-forward-to-elab-modinsts-nodups-equiv

(defthm
 equal-of-elab-modinsts-rem-dups-2-forward-to-elab-modinsts-nodups-equiv
 (implies (equal x (elab-modinsts-rem-dups y))
          (elab-modinsts-nodups-equiv x y))
 :rule-classes :forward-chaining)

Theorem: elab-modinsts-nodups-equiv-of-elab-modinsts-rem-dups-1-forward

(defthm
     elab-modinsts-nodups-equiv-of-elab-modinsts-rem-dups-1-forward
  (implies (elab-modinsts-nodups-equiv (elab-modinsts-rem-dups x)
                                       y)
           (elab-modinsts-nodups-equiv x y))
  :rule-classes :forward-chaining)

Theorem: elab-modinsts-nodups-equiv-of-elab-modinsts-rem-dups-2-forward

(defthm
     elab-modinsts-nodups-equiv-of-elab-modinsts-rem-dups-2-forward
  (implies (elab-modinsts-nodups-equiv x (elab-modinsts-rem-dups y))
           (elab-modinsts-nodups-equiv x y))
  :rule-classes :forward-chaining)

Theorem: elab-modinsts-rem-dups-of-append

(defthm elab-modinsts-rem-dups-of-append
 (equal
   (elab-modinsts-rem-dups (append a b))
   (append (elab-modinsts-rem-dups a)
           (elab-modinst-remove-names (elab-modinst-list-names a)
                                      (elab-modinsts-rem-dups b)))))