		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-modinst-order-ok

Signature
(moddb-modinst-order-ok instidx modidx moddb) → *
Arguments: instidx — Guard (natp instidx).; modidx — Guard (natp modidx).

Definitions and Theorems

Function: moddb-modinst-order-ok

(defun moddb-modinst-order-ok (instidx modidx moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (natp instidx) (natp modidx))))
 (declare
  (xargs
     :guard (and (< modidx (moddb->nmods moddb))
                 (<= (moddb->nmods moddb)
                     (moddb->mods-length moddb))
                 (stobj-let ((elab-mod (moddb->modsi modidx moddb)))
                            (ok)
                            (< instidx (elab-mod-ninsts elab-mod))
                            ok))))
 (let ((__function__ 'moddb-modinst-order-ok))
  (declare (ignorable __function__))
  (b*
   (((unless
       (mbt (and (< (lnfix modidx)
                    (lnfix (moddb->nmods moddb)))
                 (stobj-let ((elab-mod (moddb->modsi modidx moddb)))
                            (ok)
                            (< (lnfix instidx)
                               (elab-mod-ninsts elab-mod))
                            ok))))
     t)
    ((stobj-get instname submodidx)
     ((elab-mod (moddb->modsi modidx moddb)))
     (mv (elab-mod->instname instidx elab-mod)
         (elab-mod->inst-modidx instidx elab-mod)))
    ((unless (< submodidx (lnfix modidx)))
     (cw "Mod index out of order: ~s0~%"
         instname)))
   t)))

Theorem: moddb-modinst-order-ok-of-nfix-instidx

(defthm moddb-modinst-order-ok-of-nfix-instidx
  (equal (moddb-modinst-order-ok (nfix instidx)
                                 modidx moddb)
         (moddb-modinst-order-ok instidx modidx moddb)))

Theorem: moddb-modinst-order-ok-nat-equiv-congruence-on-instidx

(defthm moddb-modinst-order-ok-nat-equiv-congruence-on-instidx
  (implies
       (nat-equiv instidx instidx-equiv)
       (equal (moddb-modinst-order-ok instidx modidx moddb)
              (moddb-modinst-order-ok instidx-equiv modidx moddb)))
  :rule-classes :congruence)

Theorem: moddb-modinst-order-ok-of-nfix-modidx

(defthm moddb-modinst-order-ok-of-nfix-modidx
  (equal (moddb-modinst-order-ok instidx (nfix modidx)
                                 moddb)
         (moddb-modinst-order-ok instidx modidx moddb)))

Theorem: moddb-modinst-order-ok-nat-equiv-congruence-on-modidx

(defthm moddb-modinst-order-ok-nat-equiv-congruence-on-modidx
  (implies
       (nat-equiv modidx modidx-equiv)
       (equal (moddb-modinst-order-ok instidx modidx moddb)
              (moddb-modinst-order-ok instidx modidx-equiv moddb)))
  :rule-classes :congruence)

Theorem: moddb-modinst-order-ok-of-moddb-fix-moddb

(defthm moddb-modinst-order-ok-of-moddb-fix-moddb
  (equal (moddb-modinst-order-ok instidx modidx (moddb-fix moddb))
         (moddb-modinst-order-ok instidx modidx moddb)))

Theorem: moddb-modinst-order-ok-moddb-equiv-congruence-on-moddb

(defthm moddb-modinst-order-ok-moddb-equiv-congruence-on-moddb
  (implies
       (moddb-equiv moddb moddb-equiv)
       (equal (moddb-modinst-order-ok instidx modidx moddb)
              (moddb-modinst-order-ok instidx modidx moddb-equiv)))
  :rule-classes :congruence)

Theorem: moddb-modinst-order-ok-implies-modidx-less

(defthm moddb-modinst-order-ok-implies-modidx-less
 (implies
  (and
    (moddb-modinst-order-ok instidx modidx moddb)
    (< (nfix modidx)
       (nfix (nth *moddb->nmods* moddb)))
    (< (nfix instidx)
       (elab-mod$a-ninsts (nth modidx (nth *moddb->modsi* moddb)))))
  (<
   (elab-mod$a->inst-modidx instidx
                            (nth modidx (nth *moddb->modsi* moddb)))
   (nfix modidx)))
 :rule-classes (:rewrite :linear))

Theorem: moddb-modinst-order-ok-of-moddb-norm-moddb

(defthm moddb-modinst-order-ok-of-moddb-norm-moddb
  (equal (moddb-modinst-order-ok idx modidx (moddb-norm moddb))
         (moddb-modinst-order-ok idx modidx moddb)))

Theorem: moddb-modinst-order-ok-moddb-norm-equiv-congruence-on-moddb

(defthm moddb-modinst-order-ok-moddb-norm-equiv-congruence-on-moddb
  (implies (moddb-norm-equiv moddb moddb-equiv)
           (equal (moddb-modinst-order-ok idx modidx moddb)
                  (moddb-modinst-order-ok idx modidx moddb-equiv)))
  :rule-classes :congruence)