check-fn-inst - ACL2 Book

other

(in-package "ACL2")

subst-to-trivial-formulasfunction

(defun subst-to-trivial-formulas
  (subst wrld)
  (declare (xargs :guard (and (symbol-alistp subst) (plist-worldp wrld))))
  (cond ((endp subst) nil)
    (t (cons (let* ((fn (caar subst)) (formals (getprop fn 'formals t 'current-acl2-world wrld))
            (ap (cons fn formals))
            (term `(equal (hide ,AP) (hide ,AP))))
          (cond ((eq formals t) (er hard?
                'subst-to-trivial-formulas
                "The symbol ~x0 is not a function symbol in the ~
                               current ACL2 world."
                fn))
            (t term)))
        (subst-to-trivial-formulas (cdr subst) wrld)))))

check-fn-instmacro

(defmacro check-fn-inst
  (&rest subst)
  `(make-event (er-progn (let ((form (cons 'and (subst-to-trivial-formulas ',SUBST (w state)))))
        (thm-fn 't
          state
          nil
          (list (list "Goal"
              :use (list (list* :functional-instance (list :theorem form) ',SUBST))))
          'nil
          nil))
      (value '(value-triple nil)))))

local

(local (progn (encapsulate ((f (x) t))
      (local (defun f (x) x))
      (defthm f-preserves-len (equal (len (f x)) (len x))))
    (defun g (x) (reverse x))
    (defthm len-revappend
      (equal (len (revappend x y)) (+ (len x) (len y))))
    (encapsulate nil
      (local (defthm my-test
          t
          :hints (("Goal" :use ((:functional-instance (:theorem (equal (f x) (f x))) (f g)))))
          :rule-classes nil)))
    (check-fn-inst (f g))
    (defun h (x) (cdr x))))