		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Definition-wfp

Check if a definition is well-formed.

Signature
(definition-wfp def defs) → yes/no
Arguments: def — Guard (definitionp def).; defs — Guard (definition-listp defs).
Returns: yes/no — Type (booleanp yes/no).

This is checked with respect to definitions that precede the definition being checked in a larger list that includes the definition. That is, this predicate holds when the definition can be used to extend the list. See definition-list-wfp.

A definition is well-formed iff its constraints are all well-formed, its parameters are distinct, and the relation being defined is not already defined.

Definitions and Theorems

Function: definition-wfp

(defun definition-wfp (def defs)
  (declare (xargs :guard (and (definitionp def)
                              (definition-listp defs))))
  (let ((__function__ 'definition-wfp))
    (declare (ignorable __function__))
    (b* (((definition def) def))
      (and (not (lookup-definition def.name defs))
           (no-duplicatesp-equal def.para)
           (constraint-list-wfp def.body defs)))))

Theorem: booleanp-of-definition-wfp

(defthm booleanp-of-definition-wfp
  (b* ((yes/no (definition-wfp def defs)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: definition-wfp-of-definition-fix-def

(defthm definition-wfp-of-definition-fix-def
  (equal (definition-wfp (definition-fix def)
                         defs)
         (definition-wfp def defs)))

Theorem: definition-wfp-definition-equiv-congruence-on-def

(defthm definition-wfp-definition-equiv-congruence-on-def
  (implies (definition-equiv def def-equiv)
           (equal (definition-wfp def defs)
                  (definition-wfp def-equiv defs)))
  :rule-classes :congruence)

Theorem: definition-wfp-of-definition-list-fix-defs

(defthm definition-wfp-of-definition-list-fix-defs
  (equal (definition-wfp def (definition-list-fix defs))
         (definition-wfp def defs)))

Theorem: definition-wfp-definition-list-equiv-congruence-on-defs

(defthm definition-wfp-definition-list-equiv-congruence-on-defs
  (implies (definition-list-equiv defs defs-equiv)
           (equal (definition-wfp def defs)
                  (definition-wfp def defs-equiv)))
  :rule-classes :congruence)