		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-fix

Signature
(moddb-fix moddb) → moddb

Definitions and Theorems

Function: moddb-fix

(defun moddb-fix (moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard t))
  (let ((__function__ 'moddb-fix))
    (declare (ignorable __function__))
    (mbe :logic (non-exec (list (nfix (nth 0 moddb))
                                (elab-modlist-fix (nth 1 moddb))
                                (nth 2 moddb)))
         :exec moddb)))

Theorem: moddb-fix-when-moddbp

(defthm moddb-fix-when-moddbp
  (implies (moddbp moddb)
           (equal (moddb-fix moddb) moddb)))

Function: moddb-equiv

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

Theorem: moddb-equiv-is-an-equivalence

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

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

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

Theorem: moddb-fix-under-moddb-equiv

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

Theorem: nth-of-moddb-fix

(defthm nth-of-moddb-fix
  (and (equal (nth 0 (moddb-fix moddb))
              (nfix (nth 0 moddb)))
       (equal (nth 1 (moddb-fix moddb))
              (elab-modlist-fix (nth 1 moddb)))
       (equal (nth 2 (moddb-fix moddb))
              (nth 2 moddb))))

Theorem: moddb-equiv-implies-moddb-equiv-update-nth-3

(defthm moddb-equiv-implies-moddb-equiv-update-nth-3
  (implies (moddb-equiv x x-equiv)
           (moddb-equiv (update-nth n v x)
                        (update-nth n v x-equiv)))
  :rule-classes (:congruence))

Theorem: update-nth-of-elab-modlist-fix-v-under-moddb-equiv

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

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

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