		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-eq 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)