		Search-engine friendly clone of the ACL2 documentation.

Evaluation

Put-leftmost-nonconst

Replace the leftmost term in a list that is not a quoted constant with a quoted constant with the given value.

Signature
(put-leftmost-nonconst terms value) → (mv foundp new-terms)
Arguments: terms — Guard (tterm-listp terms).; value — Guard (valuep value).
Returns: foundp — Type (booleanp foundp).; new-terms — Type (tterm-listp new-terms).

This is used as explained in step-from-trans.

If all the terms in the list are quoted constants, no replacement takes place, and the first result is nil. Otherwise, the first result is t, and the second result is the updated list of terms.

Definitions and Theorems

Function: put-leftmost-nonconst

(defun put-leftmost-nonconst (terms value)
       (declare (xargs :guard (and (tterm-listp terms)
                                   (valuep value))))
       (let ((__function__ 'put-leftmost-nonconst))
            (declare (ignorable __function__))
            (b* (((when (endp terms)) (mv nil nil))
                 (term (car terms))
                 ((when (tterm-case term :constant))
                  (b* (((mv foundp new-terms)
                        (put-leftmost-nonconst (cdr terms)
                                               value))
                       ((unless foundp) (mv nil nil)))
                      (mv t (cons (tterm-fix term) new-terms)))))
                (mv t
                    (cons (tterm-constant value)
                          (cdr (tterm-list-fix terms)))))))

Theorem: booleanp-of-put-leftmost-nonconst.foundp

(defthm booleanp-of-put-leftmost-nonconst.foundp
        (b* (((mv ?foundp ?new-terms)
              (put-leftmost-nonconst terms value)))
            (booleanp foundp))
        :rule-classes :rewrite)

Theorem: tterm-listp-of-put-leftmost-nonconst.new-terms

(defthm tterm-listp-of-put-leftmost-nonconst.new-terms
        (b* (((mv ?foundp ?new-terms)
              (put-leftmost-nonconst terms value)))
            (tterm-listp new-terms))
        :rule-classes :rewrite)

Theorem: put-leftmost-nonconst-of-tterm-list-fix-terms

(defthm put-leftmost-nonconst-of-tterm-list-fix-terms
        (equal (put-leftmost-nonconst (tterm-list-fix terms)
                                      value)
               (put-leftmost-nonconst terms value)))

Theorem: put-leftmost-nonconst-tterm-list-equiv-congruence-on-terms

(defthm put-leftmost-nonconst-tterm-list-equiv-congruence-on-terms
        (implies (tterm-list-equiv terms terms-equiv)
                 (equal (put-leftmost-nonconst terms value)
                        (put-leftmost-nonconst terms-equiv value)))
        :rule-classes :congruence)

Theorem: put-leftmost-nonconst-of-value-fix-value

(defthm put-leftmost-nonconst-of-value-fix-value
        (equal (put-leftmost-nonconst terms (value-fix value))
               (put-leftmost-nonconst terms value)))

Theorem: put-leftmost-nonconst-value-equiv-congruence-on-value

(defthm put-leftmost-nonconst-value-equiv-congruence-on-value
        (implies (value-equiv value value-equiv)
                 (equal (put-leftmost-nonconst terms value)
                        (put-leftmost-nonconst terms value-equiv)))
        :rule-classes :congruence)