		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Ext-fun-subst-term/terms/function

Extend function substitutions for functional instantiation.

An instance thm of a second-order theorem sothm is also a theorem, provable using a :functional-instance of sothm. The pairs of the :functional-instance are not only the pairs of the instantiation that creates thm from sothm, but also all the pairs whose first components are second-order functions that sothm depends on and whose second components are the corresponding instances.

For example, if sothm is (p (sofun x)), sofun is a second-order function, p is a first-order predicate, and applying an instantiation I to (p (sofun x)) yields (p (fun x)), then thm is proved using (:functional-instance sothm (... (sofun fun) ...)), where the first ... are the pairs of I and the second ... are further pairs of second-order functions and their instances, e.g. if sofun calls a second-order function sofun1, the pair (sofun1 fun1) must be in the second ..., where fun1 is the instance of sofun1 corresponding to I. All these pairs are needed to properly instantiate the constraints that arise from the :functional-instance, which involve the second-order functions that sothm depends on, directly or indirectly.

The following code extends a function substitution (initially an instantiation) to contain all those extra pairs. The starting point is a term; the bodies of second-order functions referenced in the term are recursively processed. The table of instances of second-order functions is searched, similarly to fun-subst-function.

Function: ext-fun-subst-term

(defun ext-fun-subst-term (term fsbs wrld)
  (declare (xargs :guard (and (pseudo-termp term)
                              (fun-substp fsbs)
                              (plist-worldp wrld))))
  (let ((__function__ 'ext-fun-subst-term))
    (declare (ignorable __function__))
    (if (or (variablep term) (quotep term))
        fsbs
      (let* ((fn (fn-symb term))
             (fsbs (if (symbolp fn)
                       (ext-fun-subst-function fn fsbs wrld)
                     (ext-fun-subst-term (lambda-body fn)
                                         fsbs wrld))))
        (ext-fun-subst-terms (fargs term)
                             fsbs wrld)))))

Function: ext-fun-subst-terms

(defun ext-fun-subst-terms (terms fsbs wrld)
  (declare (xargs :guard (and (pseudo-term-listp terms)
                              (fun-substp fsbs)
                              (plist-worldp wrld))))
  (let ((__function__ 'ext-fun-subst-terms))
    (declare (ignorable __function__))
    (if (endp terms)
        fsbs
      (let ((fsbs (ext-fun-subst-term (car terms)
                                      fsbs wrld)))
        (ext-fun-subst-terms (cdr terms)
                             fsbs wrld)))))

Function: ext-fun-subst-function

(defun ext-fun-subst-function (fun fsbs wrld)
  (declare (xargs :guard (and (symbolp fun)
                              (fun-substp fsbs)
                              (plist-worldp wrld))))
  (let ((__function__ 'ext-fun-subst-function))
    (declare (ignorable __function__))
    (cond ((assoc fun fsbs) fsbs)
          ((sofunp fun wrld)
           (b* ((funvars (sofun-funvars fun wrld))
                (subfsbs (restrict-alist funvars fsbs))
                ((if (null subfsbs)) fsbs)
                (instmap (sof-instances fun wrld))
                (funinst (get-sof-instance subfsbs instmap wrld))
                ((unless funinst)
                 (raise "~x0 has no instance for ~x1."
                        fun fsbs))
                (fsbs (acons fun funinst fsbs)))
             (case (sofun-kind fun wrld)
               ((plain quant)
                (ext-fun-subst-term (ubody fun wrld)
                                    fsbs wrld))
               (choice (ext-fun-subst-term (defchoose-body fun wrld)
                                           fsbs wrld)))))
          (t fsbs))))

Definitions and Theorems

Function: ext-fun-subst-term

(defun ext-fun-subst-term (term fsbs wrld)
  (declare (xargs :guard (and (pseudo-termp term)
                              (fun-substp fsbs)
                              (plist-worldp wrld))))
  (let ((__function__ 'ext-fun-subst-term))
    (declare (ignorable __function__))
    (if (or (variablep term) (quotep term))
        fsbs
      (let* ((fn (fn-symb term))
             (fsbs (if (symbolp fn)
                       (ext-fun-subst-function fn fsbs wrld)
                     (ext-fun-subst-term (lambda-body fn)
                                         fsbs wrld))))
        (ext-fun-subst-terms (fargs term)
                             fsbs wrld)))))

Function: ext-fun-subst-terms

(defun ext-fun-subst-terms (terms fsbs wrld)
  (declare (xargs :guard (and (pseudo-term-listp terms)
                              (fun-substp fsbs)
                              (plist-worldp wrld))))
  (let ((__function__ 'ext-fun-subst-terms))
    (declare (ignorable __function__))
    (if (endp terms)
        fsbs
      (let ((fsbs (ext-fun-subst-term (car terms)
                                      fsbs wrld)))
        (ext-fun-subst-terms (cdr terms)
                             fsbs wrld)))))

Function: ext-fun-subst-function

(defun ext-fun-subst-function (fun fsbs wrld)
  (declare (xargs :guard (and (symbolp fun)
                              (fun-substp fsbs)
                              (plist-worldp wrld))))
  (let ((__function__ 'ext-fun-subst-function))
    (declare (ignorable __function__))
    (cond ((assoc fun fsbs) fsbs)
          ((sofunp fun wrld)
           (b* ((funvars (sofun-funvars fun wrld))
                (subfsbs (restrict-alist funvars fsbs))
                ((if (null subfsbs)) fsbs)
                (instmap (sof-instances fun wrld))
                (funinst (get-sof-instance subfsbs instmap wrld))
                ((unless funinst)
                 (raise "~x0 has no instance for ~x1."
                        fun fsbs))
                (fsbs (acons fun funinst fsbs)))
             (case (sofun-kind fun wrld)
               ((plain quant)
                (ext-fun-subst-term (ubody fun wrld)
                                    fsbs wrld))
               (choice (ext-fun-subst-term (defchoose-body fun wrld)
                                           fsbs wrld)))))
          (t fsbs))))

Subtopics

Ext-fun-subst-terms
Ext-fun-subst-term
Ext-fun-subst-function