apply-constraints

(in-package "ACL2")

(when-pass-2 (encapsulate ((badge-userfn (fn) t))
    (local (defun badge-userfn (fn) (declare (ignore fn)) nil))
    (defthm badge-userfn-type
      (implies (badge-userfn fn)
        (apply$-badgep (badge-userfn fn)))
      :rule-classes ((:forward-chaining))))
  (encapsulate ((apply$-userfn (fn args) t :guard (true-listp args)))
    (local (defun apply$-userfn
        (fn args)
        (declare (ignore fn args))
        nil))
    (defthm apply$-userfn-takes-arity-args
      (implies (badge-userfn fn)
        (equal (apply$-userfn fn args)
          (apply$-userfn fn
            (take (apply$-badge-arity (badge-userfn fn)) args))))
      :rule-classes nil))
  (encapsulate (((untame-apply$ * *) =>
       *
       :formals (fn args)
       :guard (true-listp args)))
    (local (defun untame-apply$
        (fn args)
        (declare (ignore fn args))
        nil))
    (defthm untame-apply$-takes-arity-args
      (implies (badge-userfn fn)
        (equal (untame-apply$ fn args)
          (untame-apply$ fn
            (take (apply$-badge-arity (badge-userfn fn)) args))))
      :rule-classes ((:rewrite :corollary (implies (and (syntaxp (and (quotep fn) (symbolp args)))
             (badge-userfn fn))
           (equal (untame-apply$ fn args)
             (untame-apply$ fn
               (take (apply$-badge-arity (badge-userfn fn)) args))))))))
  (defstub untame-ev$ (x a) t)
  (defconst *apply$-boot-fns-badge-alist*
    `((badge . ,*GENERIC-TAME-BADGE-1*) (tamep . ,*GENERIC-TAME-BADGE-1*)
      (tamep-functionp . ,*GENERIC-TAME-BADGE-1*)
      (suitably-tamep-listp . ,*GENERIC-TAME-BADGE-2*)
      (apply$ . ,*APPLY$-BADGE*)
      (ev$ . ,*EV$-BADGE*))))