		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-norm-p

Signature
(moddb-norm-p moddb) → *

Definitions and Theorems

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))