		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Check-lambda-call

Check if a term is a (translated) call of a lambda expression.

Signature
(check-lambda-call term) → (mv yes/no formals body args)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; formals — Type (symbol-listp formals), given the guard.; body — Type (pseudo-termp body), given the guard.; args — Type (pseudo-term-listp args), given the guard.

If it is, the first result is t and the other results are the formal parameters of the lambda expression, the body of the lambda expression, and the arguments on which the lambda expression is called. Otherwise, all the results are nil.

Definitions and Theorems

Function: check-lambda-call

(defun check-lambda-call (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'check-lambda-call))
    (declare (ignorable __function__))
    (b* (((when (variablep term))
          (mv nil nil nil nil))
         ((when (fquotep term))
          (mv nil nil nil nil))
         (fn (ffn-symb term))
         ((when (symbolp fn))
          (mv nil nil nil nil)))
      (mv t (lambda-formals fn)
          (lambda-body fn)
          (fargs term)))))

Theorem: booleanp-of-check-lambda-call.yes/no

(defthm booleanp-of-check-lambda-call.yes/no
  (b* (((mv ?yes/no ?formals ?body ?args)
        (check-lambda-call term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-check-lambda-call.formals

(defthm symbol-listp-of-check-lambda-call.formals
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?formals ?body ?args)
                 (check-lambda-call term)))
             (symbol-listp formals)))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-check-lambda-call.body

(defthm pseudo-termp-of-check-lambda-call.body
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?formals ?body ?args)
                 (check-lambda-call term)))
             (pseudo-termp body)))
  :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-check-lambda-call.args

(defthm pseudo-term-listp-of-check-lambda-call.args
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?formals ?body ?args)
                 (check-lambda-call term)))
             (pseudo-term-listp args)))
  :rule-classes :rewrite)

Theorem: len-of-check-lambda-calls.formals-is-args

(defthm len-of-check-lambda-calls.formals-is-args
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?formals ?body ?args)
                 (check-lambda-call term)))
             (equal (len formals) (len args)))))

Theorem: len-of-check-lambda-calls.args-is-formals

(defthm len-of-check-lambda-calls.args-is-formals
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?formals ?body ?args)
                 (check-lambda-call term)))
             (equal (len args) (len formals)))))

Theorem: true-listp-of-check-lambda-call.formals

(defthm true-listp-of-check-lambda-call.formals
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?formals ?body ?args)
                 (check-lambda-call term)))
             (true-listp formals)))
  :rule-classes :type-prescription)

Theorem: true-listp-of-check-lambda-call.args

(defthm true-listp-of-check-lambda-call.args
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?formals ?body ?args)
                 (check-lambda-call term)))
             (true-listp args)))
  :rule-classes :type-prescription)

Theorem: acl2-count-of-check-lambda-call.body

(defthm acl2-count-of-check-lambda-call.body
  (b* (((mv ?yes/no ?formals ?body ?args)
        (check-lambda-call term)))
    (implies yes/no
             (< (acl2-count body)
                (acl2-count term))))
  :rule-classes :linear)

Theorem: acl2-count-of-check-lambda-call.args

(defthm acl2-count-of-check-lambda-call.args
  (b* (((mv ?yes/no ?formals ?body ?args)
        (check-lambda-call term)))
    (implies yes/no
             (< (acl2-count args)
                (acl2-count term))))
  :rule-classes :linear)