		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-maybe-grow

Signature
(moddb-maybe-grow moddb) → moddb

Definitions and Theorems

Function: moddb-maybe-grow

(defun moddb-maybe-grow (moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard t))
  (let ((__function__ 'moddb-maybe-grow))
    (declare (ignorable __function__))
    (b* ((moddb (moddb-fix moddb))
         (idx (lnfix (moddb->nmods moddb))))
      (if (<= (moddb->mods-length moddb) idx)
          (resize-moddb->mods (max 16 (* 2 idx))
                              moddb)
        moddb))))

Theorem: moddb-maybe-grow-of-moddb-fix-moddb

(defthm moddb-maybe-grow-of-moddb-fix-moddb
  (equal (moddb-maybe-grow (moddb-fix moddb))
         (moddb-maybe-grow moddb)))

Theorem: moddb-maybe-grow-moddb-equiv-congruence-on-moddb

(defthm moddb-maybe-grow-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-maybe-grow moddb)
                  (moddb-maybe-grow moddb-equiv)))
  :rule-classes :congruence)

Theorem: elab-mods->names-of-replicate

(defthm elab-mods->names-of-replicate
  (equal (elab-mods->names (replicate n x))
         (replicate n (modname-fix (g :name x)))))

Theorem: elab-mods->names-of-resize-list

(defthm elab-mods->names-of-resize-list
  (equal (elab-mods->names (resize-list lst n d))
         (resize-list (elab-mods->names lst)
                      n (modname-fix (g :name d)))))

Theorem: take-of-resize-under-elab-modlist-equiv

(defthm take-of-resize-under-elab-modlist-equiv
  (implies (and (<= (nfix n) (nfix m))
                (elab-mod$a-equiv d nil))
           (elab-modlist-equiv (take n (resize-list lst m d))
                               (take n lst))))

Theorem: moddb-maybe-grow-under-moddb-norm-equiv

(defthm moddb-maybe-grow-under-moddb-norm-equiv
  (moddb-norm-equiv (moddb-maybe-grow moddb)
                    moddb))

Theorem: moddb-maybe-grow-of-moddb-norm-moddb-under-moddb-norm-equiv

(defthm moddb-maybe-grow-of-moddb-norm-moddb-under-moddb-norm-equiv
  (moddb-norm-equiv (moddb-maybe-grow (moddb-norm moddb))
                    (moddb-maybe-grow moddb)))

Theorem: moddb-maybe-grow-moddb-norm-equiv-congruence-on-moddb-under-moddb-norm-equiv

(defthm
 moddb-maybe-grow-moddb-norm-equiv-congruence-on-moddb-under-moddb-norm-equiv
 (implies (moddb-norm-equiv moddb moddb-equiv)
          (moddb-norm-equiv (moddb-maybe-grow moddb)
                            (moddb-maybe-grow moddb-equiv)))
 :rule-classes :congruence)

Theorem: moddb-basics-ok-of-moddb-maybe-grow

(defthm moddb-basics-ok-of-moddb-maybe-grow
  (implies (moddb-basics-ok moddb)
           (moddb-basics-ok (moddb-maybe-grow moddb))))

Theorem: moddb-maybe-grow-frame

(defthm moddb-maybe-grow-frame
  (implies (not (equal (nfix n) *moddb->modsi*))
           (equal (nth n (moddb-maybe-grow moddb))
                  (nth n (moddb-fix moddb)))))

Theorem: len-mods-of-moddb-maybe-grow

(defthm len-mods-of-moddb-maybe-grow
  (< (nfix (nth *moddb->nmods* moddb))
     (len (nth *moddb->modsi*
               (moddb-maybe-grow moddb))))
  :rule-classes :linear)