		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Check-nary-lambda-call

Check if a term is a (translated) call of an n-ary lambda expression.

Signature
(check-nary-lambda-call term n) → (mv yes/no formals body args)
Arguments: term — Guard (pseudo-termp term).; n — Guard (natp n).
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.

This is like check-lambda-call but it additionally requires the lambda expression to have a specified arity. It is accompanied by theorems saying that the lengths of the formal and argument lists equal the specified arity.

Definitions and Theorems

Function: check-nary-lambda-call

(defun check-nary-lambda-call (term n)
  (declare (xargs :guard (and (pseudo-termp term) (natp n))))
  (let ((__function__ 'check-nary-lambda-call))
    (declare (ignorable __function__))
    (b* (((mv yes/no formals body args)
          (check-lambda-call term))
         ((unless yes/no) (mv nil nil nil nil))
         ((unless (equal (len formals) n))
          (mv nil nil nil nil)))
      (mv t formals body args))))

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: len-of-check-nary-lambda-call.formals

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

Theorem: len-of-check-nary-lambda-call.args

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

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

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

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

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