		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-mod-order-ok

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

Definitions and Theorems

Function: moddb-mod-order-ok

(defun moddb-mod-order-ok (modidx moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (natp modidx)))
  (declare (xargs :guard (and (< modidx (moddb->nmods moddb))
                              (<= (moddb->nmods moddb)
                                  (moddb->mods-length moddb)))))
  (let ((__function__ 'moddb-mod-order-ok))
    (declare (ignorable __function__))
    (b* (((unless (mbt (< (lnfix modidx)
                          (lnfix (moddb->nmods moddb)))))
          t)
         ((stobj-get ninsts)
          ((elab-mod (moddb->modsi modidx moddb)))
          (elab-mod-ninsts elab-mod)))
      (not (moddb-find-bad-modinst-order ninsts modidx moddb)))))

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

(defthm moddb-mod-order-ok-of-nfix-modidx
  (equal (moddb-mod-order-ok (nfix modidx) moddb)
         (moddb-mod-order-ok modidx moddb)))

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

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

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

(defthm moddb-mod-order-ok-of-moddb-fix-moddb
  (equal (moddb-mod-order-ok modidx (moddb-fix moddb))
         (moddb-mod-order-ok modidx moddb)))

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

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

Theorem: moddb-mod-order-ok-implies

(defthm moddb-mod-order-ok-implies
 (implies
  (and
    (moddb-mod-order-ok modidx moddb)
    (< (nfix modidx)
       (nfix (nth *moddb->nmods* moddb)))
    (< (nfix idx)
       (elab-mod$a-ninsts (nth modidx (nth *moddb->modsi* moddb)))))
  (moddb-modinst-order-ok idx modidx moddb)))

Function: moddb-modinst-order-badguy

(defun moddb-modinst-order-badguy (modidx moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (natp modidx)))
  (declare (xargs :non-executable t))
  (prog2$ (acl2::throw-nonexec-error 'moddb-modinst-order-badguy
                                     (list modidx moddb))
          (let ((__function__ 'moddb-modinst-order-badguy))
            (declare (ignorable __function__))
            (let ((moddb (moddb-fix moddb)))
              (moddb-find-bad-modinst-order
                   (elab-mod-ninsts (moddb->modsi modidx moddb))
                   modidx moddb)))))

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

(defthm moddb-modinst-order-badguy-of-nfix-modidx
  (equal (moddb-modinst-order-badguy (nfix modidx)
                                     moddb)
         (moddb-modinst-order-badguy modidx moddb)))

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

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

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

(defthm moddb-modinst-order-badguy-of-moddb-fix-moddb
  (equal (moddb-modinst-order-badguy modidx (moddb-fix moddb))
         (moddb-modinst-order-badguy modidx moddb)))

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

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

Theorem: moddb-mod-order-not-ok

(defthm moddb-mod-order-not-ok
 (implies
  (acl2::rewriting-positive-literal
       (cons 'moddb-mod-order-ok
             (cons modidx (cons moddb 'nil))))
  (equal
   (moddb-mod-order-ok modidx moddb)
   (let ((idx (moddb-modinst-order-badguy modidx moddb)))
    (or
     (>=
        (nfix idx)
        (elab-mod$a-ninsts (nth modidx (nth *moddb->modsi* moddb))))
     (>= (nfix modidx)
         (nfix (nth *moddb->nmods* moddb)))
     (moddb-modinst-order-ok idx modidx moddb))))))

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

(defthm moddb-mod-order-ok-of-moddb-norm-moddb
  (equal (moddb-mod-order-ok modidx (moddb-norm moddb))
         (moddb-mod-order-ok modidx moddb)))

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

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