Fixing function for topdecl structures.
Function:
(defun topdecl-fix$inline (x) (declare (xargs :guard (topdeclp x))) (let ((__function__ 'topdecl-fix)) (declare (ignorable __function__)) (mbe :logic (case (topdecl-kind x) (:function (b* ((get (fundecl-fix (std::da-nth 0 (cdr x))))) (cons :function (list get)))) (:struct (b* ((get (structdecl-fix (std::da-nth 0 (cdr x))))) (cons :struct (list get)))) (:mapping (b* ((get (mappingdecl-fix (std::da-nth 0 (cdr x))))) (cons :mapping (list get))))) :exec x)))
Theorem:
(defthm topdeclp-of-topdecl-fix (b* ((new-x (topdecl-fix$inline x))) (topdeclp new-x)) :rule-classes :rewrite)
Theorem:
(defthm topdecl-fix-when-topdeclp (implies (topdeclp x) (equal (topdecl-fix x) x)))
Function:
(defun topdecl-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (topdeclp acl2::x) (topdeclp acl2::y)))) (equal (topdecl-fix acl2::x) (topdecl-fix acl2::y)))
Theorem:
(defthm topdecl-equiv-is-an-equivalence (and (booleanp (topdecl-equiv x y)) (topdecl-equiv x x) (implies (topdecl-equiv x y) (topdecl-equiv y x)) (implies (and (topdecl-equiv x y) (topdecl-equiv y z)) (topdecl-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm topdecl-equiv-implies-equal-topdecl-fix-1 (implies (topdecl-equiv acl2::x x-equiv) (equal (topdecl-fix acl2::x) (topdecl-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm topdecl-fix-under-topdecl-equiv (topdecl-equiv (topdecl-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-topdecl-fix-1-forward-to-topdecl-equiv (implies (equal (topdecl-fix acl2::x) acl2::y) (topdecl-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-topdecl-fix-2-forward-to-topdecl-equiv (implies (equal acl2::x (topdecl-fix acl2::y)) (topdecl-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm topdecl-equiv-of-topdecl-fix-1-forward (implies (topdecl-equiv (topdecl-fix acl2::x) acl2::y) (topdecl-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm topdecl-equiv-of-topdecl-fix-2-forward (implies (topdecl-equiv acl2::x (topdecl-fix acl2::y)) (topdecl-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm topdecl-kind$inline-of-topdecl-fix-x (equal (topdecl-kind$inline (topdecl-fix x)) (topdecl-kind$inline x)))
Theorem:
(defthm topdecl-kind$inline-topdecl-equiv-congruence-on-x (implies (topdecl-equiv x x-equiv) (equal (topdecl-kind$inline x) (topdecl-kind$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm consp-of-topdecl-fix (consp (topdecl-fix x)) :rule-classes :type-prescription)