		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Check-unary-lambda-call

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

Signature
(check-unary-lambda-call term) → (mv yes/no formal body arg)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; formal — Type (symbolp formal), given the guard.; body — Type (pseudo-termp body), given the guard.; arg — Type (pseudo-termp arg), given the guard.

This is a specialization of check-nary-lambda-call that returns a single formal and a single argument instead of two singleton lists.

Definitions and Theorems

Function: check-unary-lambda-call

(defun check-unary-lambda-call (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'check-unary-lambda-call))
    (declare (ignorable __function__))
    (b* (((mv yes/no formals body args)
          (check-nary-lambda-call term 1))
         ((unless yes/no) (mv nil nil nil nil)))
      (mv t (car formals) body (car args)))))

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

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

Theorem: symbolp-of-check-unary-lambda-call.formal

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

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

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

Theorem: pseudo-termp-of-check-unary-lambda-call.arg

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

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

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

Theorem: acl2-count-of-check-unary-lambda-call.arg

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