• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
    • Real
    • Debugging
    • Miscellaneous
      • Term
        • Lambda
        • Pseudo-termp
          • Pseudo-term-fty
            • Pseudo-term-lambda
            • Pseudo-term-call
              • Pseudo-term-call->fn
              • Pseudo-term-call->args
            • Pseudo-term-fncall
            • Pseudo-lambda
            • Pseudo-term-var
            • Pseudo-term-quote
            • Pseudo-term-kind
            • Pseudo-term-null
            • Pseudo-fnsym
            • Pseudo-term-case
            • Pseudo-term-count
            • Def-ev-pseudo-term-fty-support
            • Def-ev-pseudo-term-congruence
            • Pseudo-term-fix
            • Pseudo-var
            • Pseudo-term-list-fix
            • Pseudo-fn
          • Std/typed-lists/pseudo-term-listp
        • Term-order
        • Pseudo-term-listp
        • Guard-holders
        • Termp
        • L<
        • Kwote
        • Kwote-lst
      • Ld
      • Hints
      • Type-set
      • Ordinals
      • ACL2-customization
      • With-prover-step-limit
      • With-prover-time-limit
      • Set-prover-step-limit
      • Set-case-split-limitations
      • Subversive-recursions
      • Local-incompatibility
      • Specious-simplification
      • Defsum
      • Oracle-timelimit
      • Thm
      • Defopener
      • Gcl
      • Case-split-limitations
      • Set-gc-strategy
      • Default-defun-mode
      • Top-level
      • Reader
      • Ttags-seen
      • Adviser
      • Ttree
      • Abort-soft
      • Defsums
      • Gc$
      • With-timeout
      • Coi-debug::fail
      • Expander
      • Gc-strategy
      • Coi-debug::assert
      • Sin-cos
      • Def::doc
      • Syntax
      • Subversive-inductions
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Pseudo-term-fty

Pseudo-term-call

Constructor that produces either a function call or lambda call pseudo-term, depending whether the given function is a function symbol or lambda.

Signature

(pseudo-term-call fn args) → term

Arguments

fn — Guard (pseudo-fn-p fn).

args — Guard (pseudo-term-listp args).

Returns

term — Type (pseudo-termp term).

Definitions and Theorems

Function: pseudo-term-call

(defun
 pseudo-term-call (fn args)
 (declare (xargs :guard (and (pseudo-fn-p fn)
                             (pseudo-term-listp args))))
 (declare (xargs :guard (pseudo-fn-args-p fn args)))
 (let
     ((__function__ 'pseudo-term-call))
     (declare (ignorable __function__))
     (mbe :logic (if (consp fn)
                     (pseudo-term-lambda (pseudo-lambda->formals fn)
                                         (pseudo-lambda->body fn)
                                         args)
                     (pseudo-term-fncall fn args))
          :exec (cons fn args))))

Theorem: pseudo-termp-of-pseudo-term-call

(defthm pseudo-termp-of-pseudo-term-call
        (b* ((term (pseudo-term-call fn args)))
            (pseudo-termp term))
        :rule-classes :rewrite)

Theorem: kind-of-pseudo-term-call

(defthm
 kind-of-pseudo-term-call
 (or (equal (pseudo-term-kind (pseudo-term-call fn args))
            :fncall)
     (equal (pseudo-term-kind (pseudo-term-call fn args))
            :lambda))
 :rule-classes
 ((:forward-chaining
   :trigger-terms ((pseudo-term-kind (pseudo-term-call fn args))))))

Theorem: pseudo-term-call->fn-of-pseudo-term-call

(defthm pseudo-term-call->fn-of-pseudo-term-call
        (equal (pseudo-term-call->fn (pseudo-term-call fn args))
               (pseudo-fn-fix fn)))

Theorem: pseudo-term-call->args-of-pseudo-term-call

(defthm pseudo-term-call->args-of-pseudo-term-call
        (equal (pseudo-term-call->args (pseudo-term-call fn args))
               (pseudo-fn-args-fix fn args)))

Theorem: pseudo-term-call-when-function

(defthm pseudo-term-call-when-function
        (implies (not (consp fn))
                 (equal (pseudo-term-call fn args)
                        (pseudo-term-fncall fn args))))

Theorem: pseudo-term-call-when-lambda

(defthm
     pseudo-term-call-when-lambda
     (implies (consp fn)
              (equal (pseudo-term-call fn args)
                     (pseudo-term-lambda (pseudo-lambda->formals fn)
                                         (pseudo-lambda->body fn)
                                         args))))

Theorem: pseudo-term-call-of-accessors

(defthm
     pseudo-term-call-of-accessors
     (implies (or (equal (pseudo-term-kind x) :lambda)
                  (equal (pseudo-term-kind x) :fncall))
              (equal (pseudo-term-call (pseudo-term-call->fn x)
                                       (pseudo-term-call->args x))
                     (pseudo-term-fix x))))

Theorem: base-ev-of-pseudo-term-call

(defthm
 base-ev-of-pseudo-term-call
 (implies
  (syntaxp (not (equal a ''nil)))
  (equal
    (base-ev (pseudo-term-call fn args) a)
    (base-ev (pseudo-term-call fn (kwote-lst (base-ev-list args a)))
             nil))))

Theorem: base-ev-when-pseudo-term-call

(defthm
 base-ev-when-pseudo-term-call
 (implies
  (and (or (equal (pseudo-term-kind x) :lambda)
           (equal (pseudo-term-kind x) :fncall))
       (syntaxp (not (and (consp x)
                          (eq (car x) 'pseudo-term-call)))))
  (equal
   (base-ev x a)
   (base-ev (pseudo-term-call
                 (pseudo-term-call->fn x)
                 (kwote-lst (base-ev-list (pseudo-term-call->args x)
                                          a)))
            nil))))

Theorem: pseudo-term-call-of-pseudo-fn-fix-fn

(defthm pseudo-term-call-of-pseudo-fn-fix-fn
        (equal (pseudo-term-call (pseudo-fn-fix fn)
                                 args)
               (pseudo-term-call fn args)))

Theorem: pseudo-term-call-pseudo-fn-equiv-congruence-on-fn

(defthm pseudo-term-call-pseudo-fn-equiv-congruence-on-fn
        (implies (pseudo-fn-equiv fn fn-equiv)
                 (equal (pseudo-term-call fn args)
                        (pseudo-term-call fn-equiv args)))
        :rule-classes :congruence)

Theorem: pseudo-term-call-of-pseudo-term-list-fix-args

(defthm pseudo-term-call-of-pseudo-term-list-fix-args
        (equal (pseudo-term-call fn (pseudo-term-list-fix args))
               (pseudo-term-call fn args)))

Theorem: pseudo-term-call-pseudo-term-list-equiv-congruence-on-args

(defthm pseudo-term-call-pseudo-term-list-equiv-congruence-on-args
        (implies (pseudo-term-list-equiv args args-equiv)
                 (equal (pseudo-term-call fn args)
                        (pseudo-term-call fn args-equiv)))
        :rule-classes :congruence)

Subtopics

Pseudo-term-call->fn

Accessor for the function of a function call or lambda call pseduo-term.

Pseudo-term-call->args

Accessor for the arguments of a lambda or function call pseudo-term.