		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-modname-get-index

Signature
(moddb-modname-get-index name moddb) → idx
Arguments: name — Guard (modname-p name).
Returns: idx — Type (iff (natp idx) idx).

Definitions and Theorems

Function: moddb-modname-get-index

(defun moddb-modname-get-index (name moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (modname-p name)))
 (declare (xargs :guard (moddb-basics-ok moddb)))
 (let ((__function__ 'moddb-modname-get-index))
  (declare (ignorable __function__))
  (mbe
     :logic (non-exec (moddb->modname-idxes-get (modname-fix name)
                                                (moddb-norm moddb)))
     :exec (moddb->modname-idxes-get name moddb))))

Theorem: return-type-of-moddb-modname-get-index

(defthm return-type-of-moddb-modname-get-index
 (b* ((idx (moddb-modname-get-index name moddb)))
   (iff (natp idx) idx))
 :rule-classes
 (:rewrite
  (:type-prescription
     :corollary (maybe-natp (moddb-modname-get-index name moddb)))))

Theorem: moddb-modname-get-index-of-modname-fix-name

(defthm moddb-modname-get-index-of-modname-fix-name
  (equal (moddb-modname-get-index (modname-fix name)
                                  moddb)
         (moddb-modname-get-index name moddb)))

Theorem: moddb-modname-get-index-modname-equiv-congruence-on-name

(defthm moddb-modname-get-index-modname-equiv-congruence-on-name
  (implies (modname-equiv name name-equiv)
           (equal (moddb-modname-get-index name moddb)
                  (moddb-modname-get-index name-equiv moddb)))
  :rule-classes :congruence)

Theorem: moddb-modname-get-index-of-moddb-fix-moddb

(defthm moddb-modname-get-index-of-moddb-fix-moddb
  (equal (moddb-modname-get-index name (moddb-fix moddb))
         (moddb-modname-get-index name moddb)))

Theorem: moddb-modname-get-index-moddb-equiv-congruence-on-moddb

(defthm moddb-modname-get-index-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-modname-get-index name moddb)
                  (moddb-modname-get-index name moddb-equiv)))
  :rule-classes :congruence)

Theorem: moddb-modname-get-index-of-moddb-norm-moddb

(defthm moddb-modname-get-index-of-moddb-norm-moddb
  (equal (moddb-modname-get-index name (moddb-norm moddb))
         (moddb-modname-get-index name moddb)))

Theorem: moddb-modname-get-index-moddb-norm-equiv-congruence-on-moddb

(defthm moddb-modname-get-index-moddb-norm-equiv-congruence-on-moddb
  (implies (moddb-norm-equiv moddb moddb-equiv)
           (equal (moddb-modname-get-index name moddb)
                  (moddb-modname-get-index name moddb-equiv)))
  :rule-classes :congruence)

Theorem: modbb-modname-get-index-type

(defthm modbb-modname-get-index-type
  (or (natp (moddb-modname-get-index name moddb))
      (not (moddb-modname-get-index name moddb)))
  :rule-classes :type-prescription)

Theorem: moddb-modname-get-index-bound

(defthm moddb-modname-get-index-bound
  (implies (moddb-modname-get-index name moddb)
           (< (moddb-modname-get-index name moddb)
              (nfix (nth *moddb->nmods* moddb))))
  :rule-classes :linear)