		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Fsublis-var

Variant of sublis-var that performs no simplification.

Signature
(fsublis-var alist term) → new-term
Arguments: alist — Guard (and (symbol-alistp alist) (pseudo-term-listp (strip-cdrs alist))).; term — Guard (pseudo-termp term).
Returns: new-term — Type (pseudo-termp new-term), given the guard.

The meaning of the starting f in the name of this utility is analogous to fcons-term compared to cons-term.

Function: fsublis-var

(defun fsublis-var (alist term)
 (declare
     (xargs :guard (and (and (symbol-alistp alist)
                             (pseudo-term-listp (strip-cdrs alist)))
                        (pseudo-termp term))))
 (let ((__function__ 'fsublis-var))
   (declare (ignorable __function__))
   (cond ((variablep term)
          (b* ((pair (assoc-eq term alist)))
            (cond (pair (cdr pair)) (t term))))
         ((fquotep term) term)
         (t (b* ((fn (ffn-symb term))
                 (args (fsublis-var-lst alist (fargs term))))
              (fcons-term fn args))))))

Function: fsublis-var-lst

(defun fsublis-var-lst (alist terms)
 (declare
     (xargs :guard (and (and (symbol-alistp alist)
                             (pseudo-term-listp (strip-cdrs alist)))
                        (pseudo-term-listp terms))))
 (let ((__function__ 'fsublis-var-lst))
   (declare (ignorable __function__))
   (cond ((endp terms) nil)
         (t (cons (fsublis-var alist (car terms))
                  (fsublis-var-lst alist (cdr terms)))))))

The file fsublis-var-more-theorems.lisp contains theorems about these functions and symbol-pseudoterm-alistp. They are similar to the return type theorems, but involve that stronger alist recognizer; they are disabled by default.

Theorem: return-type-of-fsublis-var.new-term

(defthm return-type-of-fsublis-var.new-term
  (implies (and (if (symbol-alistp alist)
                    (pseudo-term-listp (strip-cdrs alist))
                  'nil)
                (pseudo-termp term))
           (b* ((?new-term (fsublis-var alist term)))
             (pseudo-termp new-term)))
  :rule-classes :rewrite)

Theorem: return-type-of-fsublis-var-lst.new-terms

(defthm return-type-of-fsublis-var-lst.new-terms
  (implies (and (if (symbol-alistp alist)
                    (pseudo-term-listp (strip-cdrs alist))
                  'nil)
                (pseudo-term-listp terms))
           (b* ((?new-terms (fsublis-var-lst alist terms)))
             (and (pseudo-term-listp new-terms)
                  (equal (len new-terms) (len terms)))))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-fsublis-var-when-symbol-pseudoterm-alistp

(defthm pseudo-termp-of-fsublis-var-when-symbol-pseudoterm-alistp
  (implies (and (symbol-pseudoterm-alistp alist)
                (pseudo-termp term))
           (pseudo-termp (fsublis-var alist term))))

Theorem: pseudo-term-listp-of-fsublis-var-lst-when-symbol-pseudoterm-alistp

(defthm
 pseudo-term-listp-of-fsublis-var-lst-when-symbol-pseudoterm-alistp
 (implies (and (symbol-pseudoterm-alistp alist)
               (pseudo-term-listp terms))
          (pseudo-term-listp (fsublis-var-lst alist terms))))

Subtopics

Fsublis-var-lst