		Search-engine friendly clone of the ACL2 documentation.

Semantics-deeply-embedded

Assignment-wfp

Check if an assignment is well-formed.

Signature
(assignment-wfp asg p) → yes/no
Arguments: asg — Guard (assignmentp asg).; p — Guard (primep p).
Returns: yes/no — Type (booleanp yes/no).

As explained in assignment, that fixtype is defined with natural numbers as range type. However, those natural numbers are meant to be prime field elements. This predicate says whether all the natural numbers in an assignment are in fact elements of the prime field specified by the given prime.

Definitions and Theorems

Function: assignment-wfp

(defun assignment-wfp (asg p)
  (declare (xargs :guard (and (assignmentp asg) (primep p))))
  (let ((__function__ 'assignment-wfp))
    (declare (ignorable __function__))
    (b* ((asg (assignment-fix asg)))
      (or (omap::emptyp asg)
          (b* (((mv & nat) (omap::head asg)))
            (and (fep nat p)
                 (assignment-wfp (omap::tail asg)
                                 p)))))))

Theorem: booleanp-of-assignment-wfp

(defthm booleanp-of-assignment-wfp
  (b* ((yes/no (assignment-wfp asg p)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: fep-of-cdr-of-in-when-assignment-wfp

(defthm fep-of-cdr-of-in-when-assignment-wfp
  (implies (and (assignmentp asg)
                (assignment-wfp asg p)
                (consp (omap::assoc var asg)))
           (fep (cdr (omap::assoc var asg)) p)))

Theorem: assignment-wfp-of-tail

(defthm assignment-wfp-of-tail
  (implies (and (assignmentp asg)
                (assignment-wfp asg p))
           (assignment-wfp (omap::tail asg) p)))

Theorem: assignment-wfp-of-nil

(defthm assignment-wfp-of-nil
  (assignment-wfp nil p))

Theorem: assignment-wfp-of-update

(defthm assignment-wfp-of-update
  (implies (and (assignmentp asg)
                (assignment-wfp asg p)
                (fep nat p))
           (assignment-wfp (omap::update var nat asg)
                           p)))

Theorem: assignment-wfp-of-update*

(defthm assignment-wfp-of-update*
  (implies (and (assignmentp asg-new)
                (assignmentp asg-old)
                (assignment-wfp asg-new p)
                (assignment-wfp asg-old p))
           (assignment-wfp (omap::update* asg-new asg-old)
                           p)))

Theorem: assignment-wfp-of-delete

(defthm assignment-wfp-of-delete
  (implies (and (assignmentp asg)
                (assignment-wfp asg p))
           (assignment-wfp (omap::delete var asg)
                           p)))

Theorem: assignment-wfp-of-delete*

(defthm assignment-wfp-of-delete*
  (implies (and (assignmentp asg)
                (assignment-wfp asg p))
           (assignment-wfp (omap::delete* vars asg)
                           p)))

Theorem: assignment-wfp-of-from-lists

(defthm assignment-wfp-of-from-lists
  (implies (and (string-listp keys)
                (fe-listp vals p)
                (equal (len keys) (len vals)))
           (assignment-wfp (omap::from-lists keys vals)
                           p)))

Theorem: assignment-wfp-of-assignment-fix-asg

(defthm assignment-wfp-of-assignment-fix-asg
  (equal (assignment-wfp (assignment-fix asg) p)
         (assignment-wfp asg p)))

Theorem: assignment-wfp-assignment-equiv-congruence-on-asg

(defthm assignment-wfp-assignment-equiv-congruence-on-asg
  (implies (assignment-equiv asg asg-equiv)
           (equal (assignment-wfp asg p)
                  (assignment-wfp asg-equiv p)))
  :rule-classes :congruence)