		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$c-modinsts-ok

Signature
(elab-mod$c-modinsts-ok elab-mod$c) → *

Definitions and Theorems

Function: elab-mod$c-modinsts-ok

(defun elab-mod$c-modinsts-ok (elab-mod$c)
  (declare (xargs :stobjs (elab-mod$c)))
  (declare (xargs :guard t))
  (let ((__function__ 'elab-mod$c-modinsts-ok))
    (declare (ignorable __function__))
    (and (<= (nfix (elab-mod$c->ninsts elab-mod$c))
             (elab-mod$c->modinsttable-length elab-mod$c))
         (ec-call (elab-mod$c-inst-indices-ok elab-mod$c))
         (ec-call (elab-mod$c-inst-names-ok elab-mod$c)))))

Theorem: elab-mod$c-modinsts-ok-when-empty

(defthm elab-mod$c-modinsts-ok-when-empty
  (implies (and (nat-equiv (nth *elab-mod$c->ninsts* elab-mod$c)
                           0)
                (not (consp (nth *elab-mod$c->modinstname-idxes-get*
                                 elab-mod$c))))
           (elab-mod$c-modinsts-ok elab-mod$c)))

Theorem: elab-mod$c-modinsts-ok-implies-lookup-name

(defthm elab-mod$c-modinsts-ok-implies-lookup-name
 (let
  ((look (hons-assoc-equal k
                           (nth *elab-mod$c->modinstname-idxes-get*
                                elab-mod$c)))
   (idx
      (index-of
           k
           (elab-modinst-list-names (nth *elab-mod$c->modinsttablei*
                                         elab-mod$c)))))
  (implies
       (and (elab-mod$c-modinsts-ok elab-mod$c)
            (name-p k))
       (equal look
              (and idx
                   (< idx
                      (nfix (nth *elab-mod$c->ninsts* elab-mod$c)))
                   (cons k idx))))))

Theorem: elab-mod$c-inst-indices-ok-in-terms-of-index-of

(defthm elab-mod$c-inst-indices-ok-in-terms-of-index-of
 (implies (and (elab-mod$c-modinsts-ok elab-mod$c)
               (< (nfix idx)
                  (nfix (nth *elab-mod$c->ninsts* elab-mod$c))))
          (let ((idxes->insts (nth *elab-mod$c->modinsttablei*
                                   elab-mod$c)))
            (equal (index-of (nth *elab-modinst$c->instname*
                                  (nth idx idxes->insts))
                             (elab-modinst-list-names idxes->insts))
                   (nfix idx)))))

Theorem: elab-mod$c-modinsts-ok-linear

(defthm elab-mod$c-modinsts-ok-linear
 (implies (elab-mod$c-modinsts-ok elab-mod$c)
          (and (<= (nfix (nth *elab-mod$c->ninsts* elab-mod$c))
                   (len (nth *elab-mod$c->modinsttablei*
                             elab-mod$c)))
               (implies (natp (nth *elab-mod$c->ninsts* elab-mod$c))
                        (<= (nth *elab-mod$c->ninsts* elab-mod$c)
                            (len (nth *elab-mod$c->modinsttablei*
                                      elab-mod$c))))))
 :rule-classes :linear)

Theorem: elab-mod$c-insts-ok-implies-no-duplicated-names

(defthm elab-mod$c-insts-ok-implies-no-duplicated-names
 (implies
  (and (elab-mod$c-modinsts-ok elab-mod$c)
       (< (nfix n)
          (nfix (nth *elab-mod$c->ninsts* elab-mod$c)))
       (< (nfix m)
          (nfix (nth *elab-mod$c->ninsts* elab-mod$c))))
  (and
    (equal
         (equal (name-fix (nth *elab-modinst$c->instname*
                               (nth n
                                    (nth *elab-mod$c->modinsttablei*
                                         elab-mod$c))))
                (name-fix (nth *elab-modinst$c->instname*
                               (nth m
                                    (nth *elab-mod$c->modinsttablei*
                                         elab-mod$c)))))
         (nat-equiv n m))
    (equal (equal (nth n
                       (nth *elab-mod$c->modinsttablei* elab-mod$c))
                  (nth m
                       (nth *elab-mod$c->modinsttablei*
                            elab-mod$c)))
           (nat-equiv n m)))))