Fixing function for asgop structures.
Function:
(defun asgop-fix$inline (x) (declare (xargs :guard (asgopp x))) (let ((__function__ 'asgop-fix)) (declare (ignorable __function__)) (mbe :logic (case (asgop-kind x) (:asg (cons :asg (list))) (:asg-add (cons :asg-add (list))) (:asg-sub (cons :asg-sub (list))) (:asg-mul (cons :asg-mul (list))) (:asg-div (cons :asg-div (list))) (:asg-rem (cons :asg-rem (list))) (:asg-pow (cons :asg-pow (list))) (:asg-shl (cons :asg-shl (list))) (:asg-shr (cons :asg-shr (list))) (:asg-bitand (cons :asg-bitand (list))) (:asg-bitior (cons :asg-bitior (list))) (:asg-bitxor (cons :asg-bitxor (list))) (:asg-and (cons :asg-and (list))) (:asg-or (cons :asg-or (list)))) :exec x)))
Theorem:
(defthm asgopp-of-asgop-fix (b* ((new-x (asgop-fix$inline x))) (asgopp new-x)) :rule-classes :rewrite)
Theorem:
(defthm asgop-fix-when-asgopp (implies (asgopp x) (equal (asgop-fix x) x)))
Function:
(defun asgop-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (asgopp acl2::x) (asgopp acl2::y)))) (equal (asgop-fix acl2::x) (asgop-fix acl2::y)))
Theorem:
(defthm asgop-equiv-is-an-equivalence (and (booleanp (asgop-equiv x y)) (asgop-equiv x x) (implies (asgop-equiv x y) (asgop-equiv y x)) (implies (and (asgop-equiv x y) (asgop-equiv y z)) (asgop-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm asgop-equiv-implies-equal-asgop-fix-1 (implies (asgop-equiv acl2::x x-equiv) (equal (asgop-fix acl2::x) (asgop-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm asgop-fix-under-asgop-equiv (asgop-equiv (asgop-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-asgop-fix-1-forward-to-asgop-equiv (implies (equal (asgop-fix acl2::x) acl2::y) (asgop-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-asgop-fix-2-forward-to-asgop-equiv (implies (equal acl2::x (asgop-fix acl2::y)) (asgop-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm asgop-equiv-of-asgop-fix-1-forward (implies (asgop-equiv (asgop-fix acl2::x) acl2::y) (asgop-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm asgop-equiv-of-asgop-fix-2-forward (implies (asgop-equiv acl2::x (asgop-fix acl2::y)) (asgop-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm asgop-kind$inline-of-asgop-fix-x (equal (asgop-kind$inline (asgop-fix x)) (asgop-kind$inline x)))
Theorem:
(defthm asgop-kind$inline-asgop-equiv-congruence-on-x (implies (asgop-equiv x x-equiv) (equal (asgop-kind$inline x) (asgop-kind$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm consp-of-asgop-fix (consp (asgop-fix x)) :rule-classes :type-prescription)