		Search-engine friendly clone of the ACL2 documentation.

Comp-db-entry

Comp-db-entry-fix

Fixing function for comp-db-entry structures.

Signature
(comp-db-entry-fix x) → new-x
Arguments: x — Guard (comp-db-entryp x).
Returns: new-x — Type (comp-db-entryp new-x).

Definitions and Theorems

Function: comp-db-entry-fix$inline

(defun comp-db-entry-fix$inline (x)
 (declare (xargs :guard (comp-db-entryp x)))
 (mbe
    :logic
    (b* ((exec (str-fix (cdr (std::da-nth 0 x))))
         (directory (str-fix (cdr (std::da-nth 1 x))))
         (output (acl2::string-option-fix (cdr (std::da-nth 2 x))))
         (arguments (comp-db-arg-list-fix (cdr (std::da-nth 3 x)))))
      (list (cons 'exec exec)
            (cons 'directory directory)
            (cons 'output output)
            (cons 'arguments arguments)))
    :exec x))

Theorem: comp-db-entryp-of-comp-db-entry-fix

(defthm comp-db-entryp-of-comp-db-entry-fix
  (b* ((new-x (comp-db-entry-fix$inline x)))
    (comp-db-entryp new-x))
  :rule-classes :rewrite)

Theorem: comp-db-entry-fix-when-comp-db-entryp

(defthm comp-db-entry-fix-when-comp-db-entryp
  (implies (comp-db-entryp x)
           (equal (comp-db-entry-fix x) x)))

Function: comp-db-entry-equiv$inline

(defun comp-db-entry-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (comp-db-entryp acl2::x)
                              (comp-db-entryp acl2::y))))
  (equal (comp-db-entry-fix acl2::x)
         (comp-db-entry-fix acl2::y)))

Theorem: comp-db-entry-equiv-is-an-equivalence

(defthm comp-db-entry-equiv-is-an-equivalence
  (and (booleanp (comp-db-entry-equiv x y))
       (comp-db-entry-equiv x x)
       (implies (comp-db-entry-equiv x y)
                (comp-db-entry-equiv y x))
       (implies (and (comp-db-entry-equiv x y)
                     (comp-db-entry-equiv y z))
                (comp-db-entry-equiv x z)))
  :rule-classes (:equivalence))

Theorem: comp-db-entry-equiv-implies-equal-comp-db-entry-fix-1

(defthm comp-db-entry-equiv-implies-equal-comp-db-entry-fix-1
  (implies (comp-db-entry-equiv acl2::x x-equiv)
           (equal (comp-db-entry-fix acl2::x)
                  (comp-db-entry-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: comp-db-entry-fix-under-comp-db-entry-equiv

(defthm comp-db-entry-fix-under-comp-db-entry-equiv
  (comp-db-entry-equiv (comp-db-entry-fix acl2::x)
                       acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-comp-db-entry-fix-1-forward-to-comp-db-entry-equiv

(defthm equal-of-comp-db-entry-fix-1-forward-to-comp-db-entry-equiv
  (implies (equal (comp-db-entry-fix acl2::x)
                  acl2::y)
           (comp-db-entry-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-comp-db-entry-fix-2-forward-to-comp-db-entry-equiv

(defthm equal-of-comp-db-entry-fix-2-forward-to-comp-db-entry-equiv
  (implies (equal acl2::x (comp-db-entry-fix acl2::y))
           (comp-db-entry-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: comp-db-entry-equiv-of-comp-db-entry-fix-1-forward

(defthm comp-db-entry-equiv-of-comp-db-entry-fix-1-forward
  (implies (comp-db-entry-equiv (comp-db-entry-fix acl2::x)
                                acl2::y)
           (comp-db-entry-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: comp-db-entry-equiv-of-comp-db-entry-fix-2-forward

(defthm comp-db-entry-equiv-of-comp-db-entry-fix-2-forward
  (implies (comp-db-entry-equiv acl2::x (comp-db-entry-fix acl2::y))
           (comp-db-entry-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)