		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-indices-ok

Signature
(moddb-indices-ok moddb) → *

Definitions and Theorems

Function: moddb-indices-ok

(defun moddb-indices-ok (moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (<= (moddb->nmods moddb)
                             (moddb->mods-length moddb))))
  (let ((__function__ 'moddb-indices-ok))
    (declare (ignorable __function__))
    (not (moddb-find-bad-index (moddb->nmods moddb)
                               moddb))))

Theorem: moddb-indices-ok-of-moddb-fix-moddb

(defthm moddb-indices-ok-of-moddb-fix-moddb
  (equal (moddb-indices-ok (moddb-fix moddb))
         (moddb-indices-ok moddb)))

Theorem: moddb-indices-ok-moddb-equiv-congruence-on-moddb

(defthm moddb-indices-ok-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-indices-ok moddb)
                  (moddb-indices-ok moddb-equiv)))
  :rule-classes :congruence)

Theorem: moddb-indices-ok-implies

(defthm moddb-indices-ok-implies
  (implies
       (and (moddb-indices-ok moddb)
            (< (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))))
         (equal (hons-assoc-equal name names->idxes)
                (cons name (nfix idx))))))

Function: moddb-indices-badguy

(defun moddb-indices-badguy (moddb)
  (declare (xargs :non-executable t))
  (prog2$ (acl2::throw-nonexec-error 'moddb-indices-badguy
                                     (list moddb))
          (moddb-find-bad-index (moddb->nmods moddb)
                                moddb)))

Theorem: moddb-indices-not-ok

(defthm moddb-indices-not-ok
 (implies
   (acl2::rewriting-positive-literal (cons 'moddb-indices-ok
                                           (cons moddb 'nil)))
   (equal
        (moddb-indices-ok moddb)
        (let* ((idx (moddb-indices-badguy 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))))
          (or (>= (nfix idx)
                  (nfix (nth *moddb->nmods* moddb)))
              (equal (hons-assoc-equal name names->idxes)
                     (cons name (nfix idx))))))))

Theorem: moddb-indices-ok-implies-name-indices-in-bounds

(defthm moddb-indices-ok-implies-name-indices-in-bounds
 (implies
   (and (moddb-indices-ok moddb)
        (equal (nfix (nth *moddb->nmods* moddb))
               (count-keys (nth *moddb->modname-idxes-get* moddb))))
   (b* ((nametab (nth *moddb->modname-idxes-get* moddb))
        (look (hons-assoc-equal name nametab)))
     (implies look
              (< (nfix (cdr look))
                 (nfix (nth *moddb->nmods* moddb))))))
 :rule-classes :linear)

Theorem: moddb-indices-ok-implies-names-ok

(defthm moddb-indices-ok-implies-names-ok
 (implies
   (and (moddb-indices-ok moddb)
        (equal (nfix (nth *moddb->nmods* moddb))
               (count-keys (nth *moddb->modname-idxes-get* moddb))))
   (b*
    ((nametab (nth *moddb->modname-idxes-get* moddb))
     (look (hons-assoc-equal name nametab))
     (name-idx-name
          (modname-fix (g :name (nth (cdr look)
                                     (nth *moddb->modsi* moddb))))))
    (implies look (equal name-idx-name name)))))

Theorem: moddb-indices-ok-implies-no-duplicates-of-elab-mods->names

(defthm moddb-indices-ok-implies-no-duplicates-of-elab-mods->names
 (implies
   (and (moddb-indices-ok moddb)
        (<= (nfix (nth *moddb->nmods* moddb))
            (len (nth *moddb->modsi* moddb)))
        (equal (nfix (nth *moddb->nmods* moddb))
               (count-keys (nth *moddb->modname-idxes-get* moddb))))
   (no-duplicatesp
        (take (nth *moddb->nmods* moddb)
              (elab-mods->names (nth *moddb->modsi* moddb))))))

Theorem: moddb-indices-ok-of-norm

(defthm moddb-indices-ok-of-norm
 (implies
   (and (moddb-indices-ok moddb)
        (equal (nfix (nth *moddb->nmods* moddb))
               (count-keys (nth *moddb->modname-idxes-get* moddb))))
   (moddb-indices-ok (moddb-norm moddb))))