		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Constraint-wfp

Check if a constraint is well-formed, with respect to a list of relation definitions.

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

An equality is always well-formed. An application of a named relation to some expressions is well-formed iff the relation is defined in the list of defined relations and the number of argument expressions is the same as the number of formal parameters.

Definitions and Theorems

Function: constraint-wfp

(defun constraint-wfp (constr defs)
 (declare (xargs :guard (and (constraintp constr)
                             (definition-listp defs))))
 (let ((__function__ 'constraint-wfp))
  (declare (ignorable __function__))
  (constraint-case constr :equal t :relation
                   (b* ((def? (lookup-definition constr.name defs)))
                     (and (definitionp def?)
                          (= (len constr.args)
                             (len (definition->para def?))))))))

Theorem: booleanp-of-constraint-wfp

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

Theorem: constraint-wfp-of-constraint-fix-constr

(defthm constraint-wfp-of-constraint-fix-constr
  (equal (constraint-wfp (constraint-fix constr)
                         defs)
         (constraint-wfp constr defs)))

Theorem: constraint-wfp-constraint-equiv-congruence-on-constr

(defthm constraint-wfp-constraint-equiv-congruence-on-constr
  (implies (constraint-equiv constr constr-equiv)
           (equal (constraint-wfp constr defs)
                  (constraint-wfp constr-equiv defs)))
  :rule-classes :congruence)

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

(defthm constraint-wfp-of-definition-list-fix-defs
  (equal (constraint-wfp constr (definition-list-fix defs))
         (constraint-wfp constr defs)))

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

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