		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Dumb-occur-var-open

Check if a variable occurs free in a term that may contain non-closed (i.e. open) lambda expressions.

Signature
(dumb-occur-var-open var term) → yes/no
Arguments: var — Guard (symbolp var).; term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).

When trivial lambda-bound variables are removed from a term via remove-trivial-vars, some lambda expressions may not be closed. For checking whether a variable occurs free in this kind of terms, the system utility dumb-occur-var is inadequate, because it skips over lambda expressions, assuming they are closed, as is the case in ACL2's internal translated form.

Thus, we define a utility similar to dumb-occur-var that does not just skip over lambda expressions. Instead, it skips over lambda expressions only if the variable is among the formal parameters of the lambda expression, because in that case the variable is bound in the lambda expression. Otherwise, it examines the body of the lambda expression. This is the standard treatment of lambda expressions in languages where lambda expressions are not necessarily closed.

Function: dumb-occur-var-open

(defun dumb-occur-var-open (var term)
  (declare (xargs :guard (and (symbolp var)
                              (pseudo-termp term))))
  (let ((__function__ 'dumb-occur-var-open))
    (declare (ignorable __function__))
    (b* (((when (eq var term)) t)
         ((when (variablep term)) nil)
         ((when (fquotep term)) nil)
         (fn (ffn-symb term)))
      (or (dumb-occur-var-open-lst var (fargs term))
          (and (flambdap fn)
               (not (member-eq var (lambda-formals fn)))
               (dumb-occur-var-open var (lambda-body fn)))))))

Function: dumb-occur-var-open-lst

(defun dumb-occur-var-open-lst (var terms)
  (declare (xargs :guard (and (symbolp var)
                              (pseudo-term-listp terms))))
  (let ((__function__ 'dumb-occur-var-open-lst))
    (declare (ignorable __function__))
    (cond ((endp terms) nil)
          (t (or (dumb-occur-var-open var (car terms))
                 (dumb-occur-var-open-lst var (cdr terms)))))))

Theorem: return-type-of-dumb-occur-var-open.yes/no

(defthm return-type-of-dumb-occur-var-open.yes/no
  (b* ((?yes/no (dumb-occur-var-open var term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-dumb-occur-var-open-lst.yes/no

(defthm return-type-of-dumb-occur-var-open-lst.yes/no
  (b* ((?yes/no (dumb-occur-var-open-lst var terms)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Subtopics

Dumb-occur-var-open-lst