		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-modinst-fix

Signature
(elab-modinst-fix x) → xx
Arguments: x — Guard (elab-modinst$cp x).
Returns: xx — Type (elab-modinst$cp xx).

Definitions and Theorems

Function: elab-modinst-fix

(defun elab-modinst-fix (x)
  (declare (xargs :guard (elab-modinst$cp x)))
  (let ((__function__ 'elab-modinst-fix))
    (declare (ignorable __function__))
    (mbe :logic (list (name-fix (nth 0 x))
                      (nfix (nth 1 x))
                      (nfix (nth 2 x))
                      (nfix (nth 3 x)))
         :exec x)))

Theorem: elab-modinst$cp-of-elab-modinst-fix

(defthm elab-modinst$cp-of-elab-modinst-fix
  (b* ((xx (elab-modinst-fix x)))
    (elab-modinst$cp xx))
  :rule-classes :rewrite)

Theorem: elab-modinst-fix-when-elab-modinst$cp

(defthm elab-modinst-fix-when-elab-modinst$cp
  (implies (elab-modinst$cp x)
           (equal (elab-modinst-fix x) x)))

Function: elab-modinst$c-equiv$inline

(defun elab-modinst$c-equiv$inline (x y)
  (declare (xargs :guard (and (elab-modinst$cp x)
                              (elab-modinst$cp y))))
  (equal (elab-modinst-fix x)
         (elab-modinst-fix y)))

Theorem: elab-modinst$c-equiv-is-an-equivalence

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

Theorem: elab-modinst$c-equiv-implies-equal-elab-modinst-fix-1

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

Theorem: elab-modinst-fix-under-elab-modinst$c-equiv

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

Theorem: equal-of-elab-modinst-fix-1-forward-to-elab-modinst$c-equiv

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

Theorem: equal-of-elab-modinst-fix-2-forward-to-elab-modinst$c-equiv

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

Theorem: elab-modinst$c-equiv-of-elab-modinst-fix-1-forward

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

Theorem: elab-modinst$c-equiv-of-elab-modinst-fix-2-forward

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

Theorem: len-of-elab-modinst-fix

(defthm len-of-elab-modinst-fix
  (equal (len (elab-modinst-fix x)) 4))

Theorem: true-listp-of-elab-modinst-fix

(defthm true-listp-of-elab-modinst-fix
  (true-listp (elab-modinst-fix x))
  :rule-classes (:rewrite :type-prescription))

Theorem: nths-of-elab-modinst-fix

(defthm nths-of-elab-modinst-fix
  (and (equal (nth 0 (elab-modinst-fix x))
              (name-fix (nth 0 x)))
       (equal (nth 1 (elab-modinst-fix x))
              (nfix (nth 1 x)))
       (equal (nth 2 (elab-modinst-fix x))
              (nfix (nth 2 x)))
       (equal (nth 3 (elab-modinst-fix x))
              (nfix (nth 3 x)))))