		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Sothm-inst-pairs

Create a list of doublets for functional instantiation.

Signature
(sothm-inst-pairs fsbs wrld) → pairs
Arguments: fsbs — Guard (fun-substp fsbs).; wrld — Guard (plist-worldp wrld).
Returns: pairs — A doublet-listp.

From a function substitution obtained by extending an instantiation via ext-fun-subst-term/terms/function, the list of pairs to supply to :functional-instance is obtained. Each dotted pair is turned into a doublet (a different representation of the pair).

In addition, when a dotted pair is encountered whose car is the name of a quantifier second-order function, an extra pair for instantiating the associated witness is inserted. The witnesses of quantifier second-order functions must also be part of the :functional-instance, because they are referenced by the quantifier second-order functions. However, these witnesses are not recorded as second-order functions in the table of second-order functions, and thus the code of ext-fun-subst-term/terms/function does not catch these witnesses.

Definitions and Theorems

Function: sothm-inst-pairs

(defun sothm-inst-pairs (fsbs wrld)
  (declare (xargs :guard (and (fun-substp fsbs)
                              (plist-worldp wrld))))
  (let ((__function__ 'sothm-inst-pairs))
    (declare (ignorable __function__))
    (if (endp fsbs)
        nil
      (let* ((pair (car fsbs))
             (1st (car pair))
             (2nd (cdr pair)))
        (if (quant-sofunp 1st wrld)
            (let ((1st-wit (defun-sk-witness 1st wrld))
                  (2nd-wit (defun-sk-witness 2nd wrld)))
              (cons (list 1st 2nd)
                    (cons (list 1st-wit 2nd-wit)
                          (sothm-inst-pairs (cdr fsbs) wrld))))
          (cons (list 1st 2nd)
                (sothm-inst-pairs (cdr fsbs) wrld)))))))