		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-modlist-norm

Signature
(elab-modlist-norm x) → *
Arguments: x — Guard (elab-modlist-p x).

Definitions and Theorems

Function: elab-modlist-norm

(defun elab-modlist-norm (x)
  (declare (xargs :guard (elab-modlist-p x)))
  (let ((__function__ 'elab-modlist-norm))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (let ((rest (elab-modlist-norm (cdr x))))
        (if (and (not rest)
                 (elab-mod$a-equiv (car x) nil))
            nil
          (cons (elab-mod$a-fix (car x))
                rest))))))

Theorem: elab-modlist-norm-of-elab-modlist-fix-x

(defthm elab-modlist-norm-of-elab-modlist-fix-x
  (equal (elab-modlist-norm (elab-modlist-fix x))
         (elab-modlist-norm x)))

Theorem: elab-modlist-norm-elab-modlist-equiv-congruence-on-x

(defthm elab-modlist-norm-elab-modlist-equiv-congruence-on-x
  (implies (elab-modlist-equiv x x-equiv)
           (equal (elab-modlist-norm x)
                  (elab-modlist-norm x-equiv)))
  :rule-classes :congruence)

Theorem: elab-modlist-norm-idempotent

(defthm elab-modlist-norm-idempotent
  (equal (elab-modlist-norm (elab-modlist-norm x))
         (elab-modlist-norm x)))

Function: elab-modlist-normp

(defun elab-modlist-normp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'elab-modlist-normp))
    (declare (ignorable __function__))
    (equal (elab-modlist-norm x) x)))

Function: elab-modlist-norm-equiv

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

Theorem: elab-modlist-norm-equiv-is-an-equivalence

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

Theorem: elab-modlist-norm-equiv-implies-equal-elab-modlist-norm-1

(defthm elab-modlist-norm-equiv-implies-equal-elab-modlist-norm-1
  (implies (elab-modlist-norm-equiv x x-equiv)
           (equal (elab-modlist-norm x)
                  (elab-modlist-norm x-equiv)))
  :rule-classes (:congruence))

Theorem: elab-modlist-norm-under-elab-modlist-norm-equiv

(defthm elab-modlist-norm-under-elab-modlist-norm-equiv
  (elab-modlist-norm-equiv (elab-modlist-norm x)
                           x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-elab-modlist-norm-1-forward-to-elab-modlist-norm-equiv

(defthm
    equal-of-elab-modlist-norm-1-forward-to-elab-modlist-norm-equiv
  (implies (equal (elab-modlist-norm x) y)
           (elab-modlist-norm-equiv x y))
  :rule-classes :forward-chaining)

Theorem: equal-of-elab-modlist-norm-2-forward-to-elab-modlist-norm-equiv

(defthm
    equal-of-elab-modlist-norm-2-forward-to-elab-modlist-norm-equiv
  (implies (equal x (elab-modlist-norm y))
           (elab-modlist-norm-equiv x y))
  :rule-classes :forward-chaining)

Theorem: elab-modlist-norm-equiv-of-elab-modlist-norm-1-forward

(defthm elab-modlist-norm-equiv-of-elab-modlist-norm-1-forward
  (implies (elab-modlist-norm-equiv (elab-modlist-norm x)
                                    y)
           (elab-modlist-norm-equiv x y))
  :rule-classes :forward-chaining)

Theorem: elab-modlist-norm-equiv-of-elab-modlist-norm-2-forward

(defthm elab-modlist-norm-equiv-of-elab-modlist-norm-2-forward
  (implies (elab-modlist-norm-equiv x (elab-modlist-norm y))
           (elab-modlist-norm-equiv x y))
  :rule-classes :forward-chaining)

Theorem: elab-modlist-fix-of-elab-modlist-norm

(defthm elab-modlist-fix-of-elab-modlist-norm
  (equal (elab-modlist-fix (elab-modlist-norm x))
         (elab-modlist-norm x)))

Theorem: elab-modlist-equiv-refines-elab-modlist-norm-equiv

(defthm elab-modlist-equiv-refines-elab-modlist-norm-equiv
  (implies (elab-modlist-equiv x y)
           (elab-modlist-norm-equiv x y))
  :rule-classes (:refinement))

Theorem: nth-of-elab-modlist-norm-x-under-elab-mod$a-equiv

(defthm acl2::nth-of-elab-modlist-norm-x-under-elab-mod$a-equiv
  (elab-mod$a-equiv (nth n (elab-modlist-norm x))
                    (nth n x)))

Theorem: nth-elab-modlist-norm-equiv-congruence-on-x-under-elab-mod$a-equiv

(defthm
 acl2::nth-elab-modlist-norm-equiv-congruence-on-x-under-elab-mod$a-equiv
 (implies (elab-modlist-norm-equiv x acl2::x-equiv)
          (elab-mod$a-equiv (nth n x)
                            (nth n acl2::x-equiv)))
 :rule-classes :congruence)

Theorem: update-nth-of-elab-modlist-norm-x-under-elab-modlist-norm-equiv

(defthm
 acl2::update-nth-of-elab-modlist-norm-x-under-elab-modlist-norm-equiv
 (elab-modlist-norm-equiv (update-nth n v (elab-modlist-norm x))
                          (update-nth n v x)))

Theorem: update-nth-elab-modlist-norm-equiv-congruence-on-x-under-elab-modlist-norm-equiv

(defthm
 acl2::update-nth-elab-modlist-norm-equiv-congruence-on-x-under-elab-modlist-norm-equiv
 (implies (elab-modlist-norm-equiv x acl2::x-equiv)
          (elab-modlist-norm-equiv (update-nth n v x)
                                   (update-nth n v acl2::x-equiv)))
 :rule-classes :congruence)

Theorem: update-nth-of-elab-mod$a-fix-v-under-elab-modlist-norm-equiv

(defthm
 acl2::update-nth-of-elab-mod$a-fix-v-under-elab-modlist-norm-equiv
 (elab-modlist-norm-equiv (update-nth n (elab-mod$a-fix v) x)
                          (update-nth n v x)))

Theorem: update-nth-elab-mod$a-equiv-congruence-on-v-under-elab-modlist-norm-equiv

(defthm
 acl2::update-nth-elab-mod$a-equiv-congruence-on-v-under-elab-modlist-norm-equiv
 (implies (elab-mod$a-equiv v acl2::v-equiv)
          (elab-modlist-norm-equiv (update-nth n v x)
                                   (update-nth n acl2::v-equiv x)))
 :rule-classes :congruence)