		Search-engine friendly clone of the ACL2 documentation.

Keyword-uscores

Keyword-uscores-fix

Fixing function for keyword-uscores structures.

Signature
(keyword-uscores-fix x) → new-x
Arguments: x — Guard (keyword-uscores-p x).
Returns: new-x — Type (keyword-uscores-p new-x).

Definitions and Theorems

Function: keyword-uscores-fix$inline

(defun keyword-uscores-fix$inline (x)
  (declare (xargs :guard (keyword-uscores-p x)))
  (mbe :logic
       (case (keyword-uscores-kind x)
         (:none (cons :none nil))
         (:start (cons :start nil))
         (:both (cons :both nil)))
       :exec x))

Theorem: keyword-uscores-p-of-keyword-uscores-fix

(defthm keyword-uscores-p-of-keyword-uscores-fix
  (b* ((new-x (keyword-uscores-fix$inline x)))
    (keyword-uscores-p new-x))
  :rule-classes :rewrite)

Theorem: keyword-uscores-fix-when-keyword-uscores-p

(defthm keyword-uscores-fix-when-keyword-uscores-p
  (implies (keyword-uscores-p x)
           (equal (keyword-uscores-fix x) x)))

Function: keyword-uscores-equiv$inline

(defun keyword-uscores-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (keyword-uscores-p acl2::x)
                              (keyword-uscores-p acl2::y))))
  (equal (keyword-uscores-fix acl2::x)
         (keyword-uscores-fix acl2::y)))

Theorem: keyword-uscores-equiv-is-an-equivalence

(defthm keyword-uscores-equiv-is-an-equivalence
  (and (booleanp (keyword-uscores-equiv x y))
       (keyword-uscores-equiv x x)
       (implies (keyword-uscores-equiv x y)
                (keyword-uscores-equiv y x))
       (implies (and (keyword-uscores-equiv x y)
                     (keyword-uscores-equiv y z))
                (keyword-uscores-equiv x z)))
  :rule-classes (:equivalence))

Theorem: keyword-uscores-equiv-implies-equal-keyword-uscores-fix-1

(defthm keyword-uscores-equiv-implies-equal-keyword-uscores-fix-1
  (implies (keyword-uscores-equiv acl2::x x-equiv)
           (equal (keyword-uscores-fix acl2::x)
                  (keyword-uscores-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: keyword-uscores-fix-under-keyword-uscores-equiv

(defthm keyword-uscores-fix-under-keyword-uscores-equiv
  (keyword-uscores-equiv (keyword-uscores-fix acl2::x)
                         acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-keyword-uscores-fix-1-forward-to-keyword-uscores-equiv

(defthm
    equal-of-keyword-uscores-fix-1-forward-to-keyword-uscores-equiv
  (implies (equal (keyword-uscores-fix acl2::x)
                  acl2::y)
           (keyword-uscores-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-keyword-uscores-fix-2-forward-to-keyword-uscores-equiv

(defthm
    equal-of-keyword-uscores-fix-2-forward-to-keyword-uscores-equiv
  (implies (equal acl2::x (keyword-uscores-fix acl2::y))
           (keyword-uscores-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: keyword-uscores-equiv-of-keyword-uscores-fix-1-forward

(defthm keyword-uscores-equiv-of-keyword-uscores-fix-1-forward
  (implies (keyword-uscores-equiv (keyword-uscores-fix acl2::x)
                                  acl2::y)
           (keyword-uscores-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: keyword-uscores-equiv-of-keyword-uscores-fix-2-forward

(defthm keyword-uscores-equiv-of-keyword-uscores-fix-2-forward
  (implies
       (keyword-uscores-equiv acl2::x (keyword-uscores-fix acl2::y))
       (keyword-uscores-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: keyword-uscores-kind$inline-of-keyword-uscores-fix-x

(defthm keyword-uscores-kind$inline-of-keyword-uscores-fix-x
  (equal (keyword-uscores-kind$inline (keyword-uscores-fix x))
         (keyword-uscores-kind$inline x)))

Theorem: keyword-uscores-kind$inline-keyword-uscores-equiv-congruence-on-x

(defthm
  keyword-uscores-kind$inline-keyword-uscores-equiv-congruence-on-x
  (implies (keyword-uscores-equiv x x-equiv)
           (equal (keyword-uscores-kind$inline x)
                  (keyword-uscores-kind$inline x-equiv)))
  :rule-classes :congruence)

Theorem: consp-of-keyword-uscores-fix

(defthm consp-of-keyword-uscores-fix
  (consp (keyword-uscores-fix x))
  :rule-classes :type-prescription)

Theorem: keyword-uscores-fix$inline-of-keyword-uscores-fix-x

(defthm keyword-uscores-fix$inline-of-keyword-uscores-fix-x
  (equal (keyword-uscores-fix$inline (keyword-uscores-fix x))
         (keyword-uscores-fix$inline x)))

Theorem: keyword-uscores-fix$inline-keyword-uscores-equiv-congruence-on-x

(defthm
   keyword-uscores-fix$inline-keyword-uscores-equiv-congruence-on-x
  (implies (keyword-uscores-equiv x x-equiv)
           (equal (keyword-uscores-fix$inline x)
                  (keyword-uscores-fix$inline x-equiv)))
  :rule-classes :congruence)