		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-find-bad-index

Signature
(moddb-find-bad-index idx moddb) → idx
Arguments: idx — Guard (natp idx).; moddb — Guard (moddbp moddb).
Returns: idx — Type (iff (natp idx) idx).

Definitions and Theorems

Function: moddb-find-bad-index

(defun moddb-find-bad-index (idx moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (natp idx) (moddbp moddb))))
 (declare (xargs :guard (and (<= (moddb->nmods moddb)
                                 (moddb->mods-length moddb))
                             (<= idx (moddb->nmods moddb)))))
 (let ((__function__ 'moddb-find-bad-index))
  (declare (ignorable __function__))
  (if (zp idx)
      nil
   (b* ((idx (1- idx))
        ((unless (mbt (< idx (lnfix (moddb->nmods moddb)))))
         (moddb-find-bad-index idx moddb))
        (name (stobj-let ((elab-mod (moddb->modsi idx moddb)))
                         (name)
                         (elab-mod->name elab-mod)
                         name))
        (name-idx (moddb->modname-idxes-get name moddb)))
    (if
     (mbe
      :logic
      (non-exec
       (equal
         (cons name idx)
         (hons-assoc-equal name
                           (nth *moddb->modname-idxes-get* moddb))))
      :exec (equal name-idx idx))
     (moddb-find-bad-index idx moddb)
     idx)))))

Theorem: return-type-of-moddb-find-bad-index

(defthm return-type-of-moddb-find-bad-index
  (b* ((idx (moddb-find-bad-index idx moddb)))
    (iff (natp idx) idx))
  :rule-classes :rewrite)

Theorem: moddb-find-bad-index-of-nfix-idx

(defthm moddb-find-bad-index-of-nfix-idx
  (equal (moddb-find-bad-index (nfix idx) moddb)
         (moddb-find-bad-index idx moddb)))

Theorem: moddb-find-bad-index-nat-equiv-congruence-on-idx

(defthm moddb-find-bad-index-nat-equiv-congruence-on-idx
  (implies (nat-equiv idx idx-equiv)
           (equal (moddb-find-bad-index idx moddb)
                  (moddb-find-bad-index idx-equiv moddb)))
  :rule-classes :congruence)

Theorem: moddb-find-bad-index-of-moddb-fix-moddb

(defthm moddb-find-bad-index-of-moddb-fix-moddb
  (equal (moddb-find-bad-index idx (moddb-fix moddb))
         (moddb-find-bad-index idx moddb)))

Theorem: moddb-find-bad-index-moddb-equiv-congruence-on-moddb

(defthm moddb-find-bad-index-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-find-bad-index idx moddb)
                  (moddb-find-bad-index idx moddb-equiv)))
  :rule-classes :congruence)

Theorem: moddb-find-bad-index-is-bad

(defthm moddb-find-bad-index-is-bad
  (implies
       (moddb-find-bad-index n moddb)
       (let* ((idx (moddb-find-bad-index n moddb))
              (names->idxes (nth *moddb->modname-idxes-get* moddb))
              (idxes->mods (nth *moddb->modsi* moddb))
              (mod (nth idx idxes->mods))
              (name (modname-fix (g :name mod))))
         (and (< (nfix idx) (nfix n))
              (< (nfix idx)
                 (nfix (nth *moddb->nmods* moddb)))
              (not (equal (hons-assoc-equal name names->idxes)
                          (cons name (nfix idx))))))))

Theorem: moddb-find-bad-index-finds-bad

(defthm moddb-find-bad-index-finds-bad
 (implies
   (and (< (nfix idx) (nfix n))
        (< (nfix idx)
           (nfix (nth *moddb->nmods* moddb)))
        (let* ((names->idxes (nth *moddb->modname-idxes-get* moddb))
               (idxes->mods (nth *moddb->modsi* moddb))
               (mod (nth idx idxes->mods))
               (name (modname-fix (g :name mod))))
          (not (equal (hons-assoc-equal name names->idxes)
                      (cons name (nfix idx))))))
   (and (moddb-find-bad-index n moddb)
        (let* ((idx (moddb-find-bad-index n moddb))
               (names->idxes (nth *moddb->modname-idxes-get* moddb))
               (idxes->mods (nth *moddb->modsi* moddb))
               (mod (nth idx idxes->mods))
               (name (modname-fix (g :name mod))))
          (not (equal (hons-assoc-equal name names->idxes)
                      (cons name (nfix idx))))))))