		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$c-add-inst

Signature
(elab-mod$c-add-inst elab-modinst$c elab-mod$c) → elab-mod$c

Definitions and Theorems

Function: elab-mod$c-add-inst

(defun elab-mod$c-add-inst (elab-modinst$c elab-mod$c)
 (declare (xargs :stobjs (elab-modinst$c elab-mod$c)))
 (declare (xargs :guard (elab-mod$c-modinsts-ok elab-mod$c)))
 (let ((__function__ 'elab-mod$c-add-inst))
  (declare (ignorable __function__))
  (b*
   ((idx (lnfix (elab-mod$c->ninsts elab-mod$c)))
    (iname (elab-modinst$c->instname elab-modinst$c))
    (iname (mbe :logic (name-fix iname)
                :exec iname))
    ((when (elab-mod$c->modinstname-idxes-boundp iname elab-mod$c))
     (raise "Inst already exists in ~s0: ~x1"
            (elab-mod$c->name elab-mod$c)
            iname)
     elab-mod$c)
    (elab-mod$c
         (if (<= (elab-mod$c->modinsttable-length elab-mod$c)
                 idx)
             (resize-elab-mod$c->modinsttable (max 16 (* 2 idx))
                                              elab-mod$c)
           elab-mod$c))
    (elab-mod$c (update-elab-mod$c->ninsts (1+ idx)
                                           elab-mod$c))
    (elab-mod$c
         (elab-mod$c->modinstname-idxes-put iname idx elab-mod$c)))
   (stobj-let
      ((elab-modinst$c2 (elab-mod$c->modinsttablei idx elab-mod$c)))
      (elab-modinst$c2)
      (elab-modinst$c-copy elab-modinst$c elab-modinst$c2)
      elab-mod$c))))

Theorem: elab-mod$c-modinsts-ok-of-elab-mod$c-add-inst

(defthm elab-mod$c-modinsts-ok-of-elab-mod$c-add-inst
 (implies
    (elab-mod$c-modinsts-ok elab-mod$c)
    (elab-mod$c-modinsts-ok (elab-mod$c-add-inst inst elab-mod$c))))

Theorem: elab-mod$c-add-inst-update

(defthm elab-mod$c-add-inst-update
 (implies
  (elab-mod$c-modinsts-ok elab-mod$c)
  (equal
      (elab-mod$c-inst-abstraction
           (elab-mod$c-add-inst inst elab-mod$c))
      (let ((orig-insts (elab-mod$c-inst-abstraction elab-mod$c)))
        (if (member (name-fix (nth *elab-modinst$c->instname* inst))
                    (elab-modinst-list-names orig-insts))
            orig-insts
          (append orig-insts
                  (list (elab-modinst$c-fix inst))))))))

Theorem: elab-mod$cp-of-add-inst

(defthm elab-mod$cp-of-add-inst
  (implies (elab-mod$cp elab-mod$c)
           (elab-mod$cp (elab-mod$c-add-inst name elab-mod$c))))

Theorem: elab-mod$cp-add-inst-frame

(defthm elab-mod$cp-add-inst-frame
  (implies (and (not (equal n *elab-mod$c->ninsts*))
                (not (equal n *elab-mod$c->modinsttablei*))
                (not (equal n *elab-mod$c->modinstname-idxes-get*)))
           (equal (nth n (elab-mod$c-add-inst inst elab-mod$c))
                  (nth n elab-mod$c))))

Theorem: elab-mod$cp-add-inst-irrel

(defthm elab-mod$cp-add-inst-irrel
  (implies
       (and (not (equal n *elab-mod$c->ninsts*))
            (not (equal n *elab-mod$c->modinsttablei*))
            (not (equal n *elab-mod$c->modinstname-idxes-get*)))
       (equal (elab-mod$c-add-inst inst (update-nth n v elab-mod$c))
              (update-nth n v
                          (elab-mod$c-add-inst inst elab-mod$c)))))

Theorem: elab-mod$c-add-inst-of-elab-modinst-fix-elab-modinst$c

(defthm elab-mod$c-add-inst-of-elab-modinst-fix-elab-modinst$c
  (equal (elab-mod$c-add-inst (elab-modinst-fix elab-modinst$c)
                              elab-mod$c)
         (elab-mod$c-add-inst elab-modinst$c elab-mod$c)))

Theorem: elab-mod$c-add-inst-elab-modinst$c-equiv-congruence-on-elab-modinst$c

(defthm
 elab-mod$c-add-inst-elab-modinst$c-equiv-congruence-on-elab-modinst$c
 (implies
      (elab-modinst$c-equiv elab-modinst$c elab-modinst$c-equiv)
      (equal (elab-mod$c-add-inst elab-modinst$c elab-mod$c)
             (elab-mod$c-add-inst elab-modinst$c-equiv elab-mod$c)))
 :rule-classes :congruence)