		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$c-inst-abstraction

Signature
(elab-mod$c-inst-abstraction elab-mod$c) → insts
Returns: insts — Type (elab-modinst-list-p insts).

Definitions and Theorems

Function: elab-mod$c-inst-abstraction

(defun elab-mod$c-inst-abstraction (elab-mod$c)
  (declare (xargs :stobjs (elab-mod$c)))
  (declare (xargs :non-executable t))
  (declare (xargs :guard t))
  (prog2$ (acl2::throw-nonexec-error 'elab-mod$c-inst-abstraction
                                     (list elab-mod$c))
          (let ((__function__ 'elab-mod$c-inst-abstraction))
            (declare (ignorable __function__))
            (elab-modinst-list-fix
                 (take (nth *elab-mod$c->ninsts* elab-mod$c)
                       (nth *elab-mod$c->modinsttablei*
                            elab-mod$c))))))

Theorem: elab-modinst-list-p-of-elab-mod$c-inst-abstraction

(defthm elab-modinst-list-p-of-elab-mod$c-inst-abstraction
  (b* ((insts (elab-mod$c-inst-abstraction elab-mod$c)))
    (elab-modinst-list-p insts))
  :rule-classes :rewrite)

Theorem: member-of-abstraction-when-modinsts-ok

(defthm member-of-abstraction-when-modinsts-ok
 (implies
     (and (elab-mod$c-modinsts-ok elab-mod$c)
          (name-p x))
     (iff (hons-assoc-equal x
                            (nth *elab-mod$c->modinstname-idxes-get*
                                 elab-mod$c))
          (member x
                  (elab-modinst-list-names
                       (elab-mod$c-inst-abstraction elab-mod$c))))))

Theorem: no-duplicatesp-of-abstraction-when-modinsts-ok

(defthm no-duplicatesp-of-abstraction-when-modinsts-ok
 (implies
   (elab-mod$c-modinsts-ok elab-mod$c)
   (no-duplicatesp (elab-modinst-list-names
                        (elab-mod$c-inst-abstraction elab-mod$c)))))

Theorem: elab-modinsts-nodups-p-of-abstraction-when-modinsts-ok

(defthm elab-modinsts-nodups-p-of-abstraction-when-modinsts-ok
  (implies (elab-mod$c-modinsts-ok elab-mod$c)
           (elab-modinsts-nodups-p
                (elab-mod$c-inst-abstraction elab-mod$c))))