		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-norm

Signature
(moddb-norm moddb) → moddb1
Returns: moddb1 — Type (moddbp moddb1).

Definitions and Theorems

Function: moddb-norm

(defun moddb-norm (moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :non-executable t))
 (declare (xargs :guard t))
 (prog2$
  (acl2::throw-nonexec-error 'moddb-norm
                             (list moddb))
  (let ((__function__ 'moddb-norm))
    (declare (ignorable __function__))
    (b* ((nmods (nfix (nth *moddb->nmods* moddb)))
         (mods (elab-modlist-fix (take (nth *moddb->nmods* moddb)
                                       (nth *moddb->modsi* moddb))))
         (names (elab-mods->names mods)))
      (list nmods mods
            (pairlis$ names (acl2::numlist 0 1 nmods)))))))

Theorem: moddbp-of-moddb-norm

(defthm moddbp-of-moddb-norm
  (b* ((moddb1 (moddb-norm moddb)))
    (moddbp moddb1))
  :rule-classes :rewrite)

Theorem: moddb-norm-of-moddb-fix-moddb

(defthm moddb-norm-of-moddb-fix-moddb
  (equal (moddb-norm (moddb-fix moddb))
         (moddb-norm moddb)))

Theorem: moddb-norm-moddb-equiv-congruence-on-moddb

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

Theorem: hons-assoc-equal-pairlis

(defthm hons-assoc-equal-pairlis
  (equal (hons-assoc-equal k (pairlis$ keys vals))
         (and (member k keys)
              (cons k (nth (index-of k keys) vals)))))

Theorem: nth-of-numlist

(defthm nth-of-numlist
  (implies (acl2-numberp start)
           (equal (nth n (acl2::numlist start by count))
                  (and (< (nfix n) (nfix count))
                       (+ start (* (nfix n) by))))))

Theorem: nmods-of-moddb-norm

(defthm nmods-of-moddb-norm
  (equal (nth *moddb->nmods* (moddb-norm moddb))
         (nfix (nth *moddb->nmods* moddb))))

Theorem: modidx-of-moddb-norm

(defthm modidx-of-moddb-norm
 (implies
  (< (nfix modidx)
     (nfix (nth *moddb->nmods* moddb)))
  (equal (nth modidx
              (nth *moddb->modsi* (moddb-norm moddb)))
         (elab-mod$a-fix (nth modidx (nth *moddb->modsi* moddb))))))

Theorem: moddb-norm-idempotent

(defthm moddb-norm-idempotent
  (equal (moddb-norm (moddb-norm moddb))
         (moddb-norm moddb)))

Function: moddb-norm-p

(defun moddb-norm-p (moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :non-executable t))
  (declare (xargs :guard t))
  (prog2$ (acl2::throw-nonexec-error 'moddb-norm-p
                                     (list moddb))
          (let ((__function__ 'moddb-norm-p))
            (declare (ignorable __function__))
            (equal (moddb-norm moddb) moddb))))

Function: moddb-norm-equiv

(defun moddb-norm-equiv (x y)
  (declare (xargs :non-executable t))
  (prog2$ (acl2::throw-nonexec-error 'moddb-norm-equiv
                                     (list x y))
          (equal (moddb-norm x) (moddb-norm y))))

Theorem: moddb-norm-equiv-is-an-equivalence

(defthm moddb-norm-equiv-is-an-equivalence
  (and (booleanp (moddb-norm-equiv x y))
       (moddb-norm-equiv x x)
       (implies (moddb-norm-equiv x y)
                (moddb-norm-equiv y x))
       (implies (and (moddb-norm-equiv x y)
                     (moddb-norm-equiv y z))
                (moddb-norm-equiv x z)))
  :rule-classes (:equivalence))

Theorem: moddb-norm-equiv-implies-equal-moddb-norm-1

(defthm moddb-norm-equiv-implies-equal-moddb-norm-1
  (implies (moddb-norm-equiv x x-equiv)
           (equal (moddb-norm x)
                  (moddb-norm x-equiv)))
  :rule-classes (:congruence))

Theorem: moddb-norm-under-moddb-norm-equiv

(defthm moddb-norm-under-moddb-norm-equiv
  (moddb-norm-equiv (moddb-norm x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-moddb-norm-1-forward-to-moddb-norm-equiv

(defthm equal-of-moddb-norm-1-forward-to-moddb-norm-equiv
  (implies (equal (moddb-norm x) y)
           (moddb-norm-equiv x y))
  :rule-classes :forward-chaining)

Theorem: equal-of-moddb-norm-2-forward-to-moddb-norm-equiv

(defthm equal-of-moddb-norm-2-forward-to-moddb-norm-equiv
  (implies (equal x (moddb-norm y))
           (moddb-norm-equiv x y))
  :rule-classes :forward-chaining)

Theorem: moddb-norm-equiv-of-moddb-norm-1-forward

(defthm moddb-norm-equiv-of-moddb-norm-1-forward
  (implies (moddb-norm-equiv (moddb-norm x) y)
           (moddb-norm-equiv x y))
  :rule-classes :forward-chaining)

Theorem: moddb-norm-equiv-of-moddb-norm-2-forward

(defthm moddb-norm-equiv-of-moddb-norm-2-forward
  (implies (moddb-norm-equiv x (moddb-norm y))
           (moddb-norm-equiv x y))
  :rule-classes :forward-chaining)

Theorem: nth-of-moddb-norm-moddb-under-nat-equiv

(defthm acl2::nth-of-moddb-norm-moddb-under-nat-equiv
  (nat-equiv (nth *moddb->nmods* (moddb-norm moddb))
             (nth *moddb->nmods* moddb)))

Theorem: nth-moddb-norm-equiv-congruence-on-moddb-under-nat-equiv

(defthm
     acl2::nth-moddb-norm-equiv-congruence-on-moddb-under-nat-equiv
  (implies (moddb-norm-equiv moddb acl2::moddb-equiv)
           (nat-equiv (nth *moddb->nmods* moddb)
                      (nth *moddb->nmods* acl2::moddb-equiv)))
  :rule-classes :congruence)

Theorem: take-of-elab-modlist-norm-mods-under-elab-modlist-equiv

(defthm
      acl2::take-of-elab-modlist-norm-mods-under-elab-modlist-equiv
  (elab-modlist-equiv (take n (elab-modlist-norm mods))
                      (take n mods)))

Theorem: take-elab-modlist-norm-equiv-congruence-on-mods-under-elab-modlist-equiv

(defthm
 acl2::take-elab-modlist-norm-equiv-congruence-on-mods-under-elab-modlist-equiv
 (implies (elab-modlist-norm-equiv mods acl2::mods-equiv)
          (elab-modlist-equiv (take n mods)
                              (take n acl2::mods-equiv)))
 :rule-classes :congruence)

Theorem: update-nth-of-elab-modlist-norm-mods-under-moddb-norm-equiv

(defthm
  acl2::update-nth-of-elab-modlist-norm-mods-under-moddb-norm-equiv
  (moddb-norm-equiv
       (update-nth *moddb->modsi* (elab-modlist-norm mods)
                   moddb)
       (update-nth *moddb->modsi* mods moddb)))

Theorem: update-nth-elab-modlist-norm-equiv-congruence-on-mods-under-moddb-norm-equiv

(defthm
 acl2::update-nth-elab-modlist-norm-equiv-congruence-on-mods-under-moddb-norm-equiv
 (implies (elab-modlist-norm-equiv mods acl2::mods-equiv)
          (moddb-norm-equiv
               (update-nth *moddb->modsi* mods moddb)
               (update-nth *moddb->modsi* acl2::mods-equiv moddb)))
 :rule-classes :congruence)

Theorem: moddb-norm-equiv-nth-module-congruence

(defthm moddb-norm-equiv-nth-module-congruence
  (implies
       (and (< (nfix n)
               (nfix (nth *moddb->nmods* moddb)))
            (moddb-norm-equiv moddb moddb1))
       (equal (elab-mod$a-equiv (nth n (nth *moddb->modsi* moddb))
                                (nth n (nth *moddb->modsi* moddb1)))
              t)))

Theorem: moddb-fix-under-moddb-norm-equiv

(defthm moddb-fix-under-moddb-norm-equiv
  (moddb-norm-equiv (moddb-fix x) x))