		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Modinstlist-add-modinsts

Signature
(modinstlist-add-modinsts modinsts modalist elab-mod moddb) → elab-mod1
Arguments: modinsts — Guard (modinstlist-p modinsts).; modalist — Guard (modalist-p modalist).; moddb — Guard (moddb-ok moddb).

Definitions and Theorems

Function: modinstlist-add-modinsts

(defun modinstlist-add-modinsts (modinsts modalist elab-mod moddb)
 (declare (xargs :stobjs (elab-mod moddb)))
 (declare (xargs :guard (and (modinstlist-p modinsts)
                             (modalist-p modalist)
                             (moddb-ok moddb))))
 (declare
  (xargs
    :guard (moddb-contains-modnames (modinstlist->modnames modinsts)
                                    moddb)))
 (let ((__function__ 'modinstlist-add-modinsts))
   (declare (ignorable __function__))
   (b*
     (((when (atom modinsts))
       (elab-mod-fix elab-mod))
      ((modinst inst) (car modinsts))
      (modidx (moddb-modname-get-index inst.modname moddb))
      ((unless (mbt (natp modidx)))
       (modinstlist-add-modinsts (cdr modinsts)
                                 modalist elab-mod moddb))
      ((when (elab-mod-instname->idx inst.instname elab-mod))
       (modinstlist-add-modinsts (cdr modinsts)
                                 modalist elab-mod moddb))
      (elab-mod
           (moddb-add-modinst inst.instname modidx elab-mod moddb)))
     (modinstlist-add-modinsts (cdr modinsts)
                               modalist elab-mod moddb))))

Theorem: modinstlist-add-modinsts-of-modinstlist-fix-modinsts

(defthm modinstlist-add-modinsts-of-modinstlist-fix-modinsts
  (equal
       (modinstlist-add-modinsts (modinstlist-fix modinsts)
                                 modalist elab-mod moddb)
       (modinstlist-add-modinsts modinsts modalist elab-mod moddb)))

Theorem: modinstlist-add-modinsts-modinstlist-equiv-congruence-on-modinsts

(defthm
  modinstlist-add-modinsts-modinstlist-equiv-congruence-on-modinsts
 (implies
  (modinstlist-equiv modinsts modinsts-equiv)
  (equal (modinstlist-add-modinsts modinsts modalist elab-mod moddb)
         (modinstlist-add-modinsts modinsts-equiv
                                   modalist elab-mod moddb)))
 :rule-classes :congruence)

Theorem: modinstlist-add-modinsts-of-modalist-fix-modalist

(defthm modinstlist-add-modinsts-of-modalist-fix-modalist
  (equal
       (modinstlist-add-modinsts modinsts (modalist-fix modalist)
                                 elab-mod moddb)
       (modinstlist-add-modinsts modinsts modalist elab-mod moddb)))

Theorem: modinstlist-add-modinsts-modalist-equiv-congruence-on-modalist

(defthm
     modinstlist-add-modinsts-modalist-equiv-congruence-on-modalist
 (implies
  (modalist-equiv modalist modalist-equiv)
  (equal (modinstlist-add-modinsts modinsts modalist elab-mod moddb)
         (modinstlist-add-modinsts modinsts
                                   modalist-equiv elab-mod moddb)))
 :rule-classes :congruence)

Theorem: modinstlist-add-modinsts-of-elab-mod$a-fix-elab-mod

(defthm modinstlist-add-modinsts-of-elab-mod$a-fix-elab-mod
  (equal
       (modinstlist-add-modinsts modinsts
                                 modalist (elab-mod$a-fix elab-mod)
                                 moddb)
       (modinstlist-add-modinsts modinsts modalist elab-mod moddb)))

Theorem: modinstlist-add-modinsts-elab-mod$a-equiv-congruence-on-elab-mod

(defthm
   modinstlist-add-modinsts-elab-mod$a-equiv-congruence-on-elab-mod
 (implies
  (elab-mod$a-equiv elab-mod elab-mod-equiv)
  (equal (modinstlist-add-modinsts modinsts modalist elab-mod moddb)
         (modinstlist-add-modinsts modinsts
                                   modalist elab-mod-equiv moddb)))
 :rule-classes :congruence)

Theorem: modinstlist-add-modinsts-of-moddb-fix-moddb

(defthm modinstlist-add-modinsts-of-moddb-fix-moddb
 (equal
      (modinstlist-add-modinsts modinsts
                                modalist elab-mod (moddb-fix moddb))
      (modinstlist-add-modinsts modinsts modalist elab-mod moddb)))

Theorem: modinstlist-add-modinsts-moddb-equiv-congruence-on-moddb

(defthm modinstlist-add-modinsts-moddb-equiv-congruence-on-moddb
 (implies
  (moddb-equiv moddb moddb-equiv)
  (equal (modinstlist-add-modinsts modinsts modalist elab-mod moddb)
         (modinstlist-add-modinsts modinsts
                                   modalist elab-mod moddb-equiv)))
 :rule-classes :congruence)

Theorem: modname-of-moddb-add-modinst

(defthm modname-of-moddb-add-modinst
 (equal (g :name (moddb-add-modinst instname modidx elab-mod moddb))
        (modname-fix (g :name elab-mod))))

Theorem: modname-of-modinstlist-add-modinsts

(defthm modname-of-modinstlist-add-modinsts
 (equal
     (g :name
        (modinstlist-add-modinsts modinsts modalist elab-mod moddb))
     (modname-fix (g :name elab-mod))))

Theorem: modinstlist-add-modinsts-preserves-moddb-mods-ok-of-add-module

(defthm
     modinstlist-add-modinsts-preserves-moddb-mods-ok-of-add-module
 (implies
  (and (moddb-mods-ok (mv-nth 1 (moddb-add-module1 elab-mod moddb)))
       (not (moddb-modname-get-index (g :name elab-mod)
                                     moddb)))
  (moddb-mods-ok
   (mv-nth
    1
    (moddb-add-module1
         (modinstlist-add-modinsts modinsts modalist elab-mod moddb)
         moddb)))))