		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-modlist-normp

Signature
(elab-modlist-normp x) → *

Definitions and Theorems

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)