		Search-engine friendly clone of the ACL2 documentation.

Remove-trivial-vars

Remove-equal-formals-actuals

Remove equal formals and actuals from two lists of the same length.

Signature
(remove-equal-formals-actuals formals actuals) → (mv new-formals new-actuals)
Arguments: formals — Guard (symbol-listp formals).; actuals — Guard (pseudo-term-listp actuals).
Returns: new-formals — Type (symbol-listp new-formals), given (symbol-listp formals).; new-actuals — Type (pseudo-term-listp new-actuals), given (pseudo-term-listp actuals).

This is used by remove-trivial-vars, but it may be more generally useful. In fact, it could be generalized to an operation on lists.

Definitions and Theorems

Function: remove-equal-formals-actuals

(defun remove-equal-formals-actuals (formals actuals)
  (declare (xargs :guard (and (symbol-listp formals)
                              (pseudo-term-listp actuals))))
  (declare (xargs :guard (= (len formals) (len actuals))))
  (let ((__function__ 'remove-equal-formals-actuals))
    (declare (ignorable __function__))
    (b* (((when (endp formals)) (mv nil nil))
         ((unless (mbt (consp actuals)))
          (mv nil nil))
         (formal (car formals))
         (actual (car actuals))
         ((when (eq formal actual))
          (remove-equal-formals-actuals (cdr formals)
                                        (cdr actuals)))
         ((mv rest-formals rest-actuals)
          (remove-equal-formals-actuals (cdr formals)
                                        (cdr actuals))))
      (mv (cons formal rest-formals)
          (cons actual rest-actuals)))))

Theorem: symbol-listp-of-remove-equal-formals-actuals.new-formals

(defthm symbol-listp-of-remove-equal-formals-actuals.new-formals
  (implies (symbol-listp formals)
           (b* (((mv ?new-formals ?new-actuals)
                 (remove-equal-formals-actuals formals actuals)))
             (symbol-listp new-formals)))
  :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-remove-equal-formals-actuals.new-actuals

(defthm
      pseudo-term-listp-of-remove-equal-formals-actuals.new-actuals
  (implies (pseudo-term-listp actuals)
           (b* (((mv ?new-formals ?new-actuals)
                 (remove-equal-formals-actuals formals actuals)))
             (pseudo-term-listp new-actuals)))
  :rule-classes :rewrite)

Theorem: remove-equal-formals-actuals-same-len

(defthm remove-equal-formals-actuals-same-len
 (equal
     (len (mv-nth 0
                  (remove-equal-formals-actuals formals actuals)))
     (len (mv-nth 1
                  (remove-equal-formals-actuals formals actuals)))))

Theorem: true-listp-of-remove-equal-formals-actuals.new-formals

(defthm true-listp-of-remove-equal-formals-actuals.new-formals
  (b* (((mv ?new-formals ?new-actuals)
        (remove-equal-formals-actuals formals actuals)))
    (true-listp new-formals))
  :rule-classes :type-prescription)

Theorem: true-listp-of-remove-equal-formals-actuals.new-actuals

(defthm true-listp-of-remove-equal-formals-actuals.new-actuals
  (b* (((mv ?new-formals ?new-actuals)
        (remove-equal-formals-actuals formals actuals)))
    (true-listp new-actuals))
  :rule-classes :type-prescription)

Theorem: acl2-count-of-remove-equal-formals-actuals.formals

(defthm acl2-count-of-remove-equal-formals-actuals.formals
  (b* (((mv ?new-formals ?new-actuals)
        (remove-equal-formals-actuals formals actuals)))
    (<= (acl2-count new-formals)
        (acl2-count formals)))
  :rule-classes :linear)

Theorem: acl2-count-of-remove-equal-formals-actuals.actuals

(defthm acl2-count-of-remove-equal-formals-actuals.actuals
  (b* (((mv ?new-formals ?new-actuals)
        (remove-equal-formals-actuals formals actuals)))
    (<= (acl2-count new-actuals)
        (acl2-count actuals)))
  :rule-classes :linear)