		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Definition-list-wfp

Check if a list of definitions is well-formed.

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

The empty list of definitions is well-formed, and every well-formed list of definitions can be extended by adding a definition that is well-formed with respect to that list. To iterate through the list more naturally, we use an auxiliary function that operates on the reversed list.

Definitions and Theorems

Function: definition-list-wfp-aux

(defun definition-list-wfp-aux (rev-defs)
  (declare (xargs :guard (definition-listp rev-defs)))
  (let ((__function__ 'definition-list-wfp-aux))
    (declare (ignorable __function__))
    (or (endp rev-defs)
        (and (definition-list-wfp-aux (cdr rev-defs))
             (definition-wfp (car rev-defs)
                             (cdr rev-defs))))))

Theorem: booleanp-of-definition-list-wfp-aux

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

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

(defthm definition-list-wfp-aux-of-definition-list-fix-rev-defs
  (equal (definition-list-wfp-aux (definition-list-fix rev-defs))
         (definition-list-wfp-aux rev-defs)))

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

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

Function: definition-list-wfp

(defun definition-list-wfp (defs)
  (declare (xargs :guard (definition-listp defs)))
  (let ((__function__ 'definition-list-wfp))
    (declare (ignorable __function__))
    (definition-list-wfp-aux (rev defs))))

Theorem: booleanp-of-definition-list-wfp

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

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

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

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

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