		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$a-fix

Signature
(elab-mod$a-fix elab-mod$a) → em
Arguments: elab-mod$a — Guard (elab-mod$ap elab-mod$a).
Returns: em — Type (elab-mod$ap em).

Definitions and Theorems

Function: elab-mod$a-fix

(defun elab-mod$a-fix (elab-mod$a)
 (declare (xargs :guard (elab-mod$ap elab-mod$a)))
 (let ((__function__ 'elab-mod$a-fix))
  (declare (ignorable __function__))
  (mbe
    :logic
    (s :name (modname-fix (g :name elab-mod$a))
       (s :totalwires
          (nfix (g :totalwires elab-mod$a))
          (s :totalinsts
             (nfix (g :totalinsts elab-mod$a))
             (s :orig-mod
                (module-fix (g :orig-mod elab-mod$a))
                (s :wires
                   (wirelist-rem-dups (g :wires elab-mod$a))
                   (s :insts
                      (elab-modinsts-rem-dups (g :insts elab-mod$a))
                      nil))))))
    :exec elab-mod$a)))

Theorem: elab-mod$ap-of-elab-mod$a-fix

(defthm elab-mod$ap-of-elab-mod$a-fix
  (b* ((em (elab-mod$a-fix elab-mod$a)))
    (elab-mod$ap em))
  :rule-classes :rewrite)

Theorem: elab-mod$a-fix-when-elab-mod$ap

(defthm elab-mod$a-fix-when-elab-mod$ap
  (implies (elab-mod$ap x)
           (equal (elab-mod$a-fix x) x)))

Function: elab-mod$a-equiv$inline

(defun elab-mod$a-equiv$inline (x y)
  (declare (xargs :guard (and (elab-mod$ap x) (elab-mod$ap y))))
  (equal (elab-mod$a-fix x)
         (elab-mod$a-fix y)))

Theorem: elab-mod$a-equiv-is-an-equivalence

(defthm elab-mod$a-equiv-is-an-equivalence
  (and (booleanp (elab-mod$a-equiv x y))
       (elab-mod$a-equiv x x)
       (implies (elab-mod$a-equiv x y)
                (elab-mod$a-equiv y x))
       (implies (and (elab-mod$a-equiv x y)
                     (elab-mod$a-equiv y z))
                (elab-mod$a-equiv x z)))
  :rule-classes (:equivalence))

Theorem: elab-mod$a-equiv-implies-equal-elab-mod$a-fix-1

(defthm elab-mod$a-equiv-implies-equal-elab-mod$a-fix-1
  (implies (elab-mod$a-equiv x x-equiv)
           (equal (elab-mod$a-fix x)
                  (elab-mod$a-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: elab-mod$a-fix-under-elab-mod$a-equiv

(defthm elab-mod$a-fix-under-elab-mod$a-equiv
  (elab-mod$a-equiv (elab-mod$a-fix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-elab-mod$a-fix-1-forward-to-elab-mod$a-equiv

(defthm equal-of-elab-mod$a-fix-1-forward-to-elab-mod$a-equiv
  (implies (equal (elab-mod$a-fix x) y)
           (elab-mod$a-equiv x y))
  :rule-classes :forward-chaining)

Theorem: equal-of-elab-mod$a-fix-2-forward-to-elab-mod$a-equiv

(defthm equal-of-elab-mod$a-fix-2-forward-to-elab-mod$a-equiv
  (implies (equal x (elab-mod$a-fix y))
           (elab-mod$a-equiv x y))
  :rule-classes :forward-chaining)

Theorem: elab-mod$a-equiv-of-elab-mod$a-fix-1-forward

(defthm elab-mod$a-equiv-of-elab-mod$a-fix-1-forward
  (implies (elab-mod$a-equiv (elab-mod$a-fix x) y)
           (elab-mod$a-equiv x y))
  :rule-classes :forward-chaining)

Theorem: elab-mod$a-equiv-of-elab-mod$a-fix-2-forward

(defthm elab-mod$a-equiv-of-elab-mod$a-fix-2-forward
  (implies (elab-mod$a-equiv x (elab-mod$a-fix y))
           (elab-mod$a-equiv x y))
  :rule-classes :forward-chaining)

Theorem: s-of-elab-mod$a-fix-x-under-elab-mod$a-equiv

(defthm acl2::s-of-elab-mod$a-fix-x-under-elab-mod$a-equiv
  (elab-mod$a-equiv (s k v (elab-mod$a-fix x))
                    (s k v x)))

Theorem: s-elab-mod$a-equiv-congruence-on-x-under-elab-mod$a-equiv

(defthm
    acl2::s-elab-mod$a-equiv-congruence-on-x-under-elab-mod$a-equiv
  (implies (elab-mod$a-equiv x acl2::x-equiv)
           (elab-mod$a-equiv (s k v x)
                             (s k v acl2::x-equiv)))
  :rule-classes :congruence)

Theorem: g-of-elab-mod$a-fix

(defthm g-of-elab-mod$a-fix
  (and (equal (g :name (elab-mod$a-fix x))
              (modname-fix (g :name x)))
       (equal (g :totalinsts (elab-mod$a-fix x))
              (nfix (g :totalinsts x)))
       (equal (g :totalwires (elab-mod$a-fix x))
              (nfix (g :totalwires x)))
       (equal (g :orig-mod (elab-mod$a-fix x))
              (module-fix (g :orig-mod x)))))

Theorem: g-of-elab-mod$a-fix-wires

(defthm g-of-elab-mod$a-fix-wires
  (equal (g :wires (elab-mod$a-fix x))
         (wirelist-rem-dups (g :wires x))))

Theorem: g-of-elab-mod$a-fix-insts

(defthm g-of-elab-mod$a-fix-insts
  (equal (g :insts (elab-mod$a-fix x))
         (elab-modinsts-rem-dups (g :insts x))))