• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
      • Soft-future-work
      • Soft-macros
      • Updates-to-workshop-material
      • Soft-implementation
        • Soft-implementation-core
          • Sothm-inst-facts
          • Ext-fun-subst-term/terms/function
          • Fun-subst-function
          • Sothm-inst-pairs
          • Funvars-of-term/terms
          • Funvars-of-plain-fn
          • Sothm-inst-proof
          • Fun-subst-term/terms
          • Get-sof-instance
          • Sof-instancesp
          • Put-sof-instance
          • Fun-substp
          • Sofun-kindp
          • Funvar-listp
          • *-listp
          • Funvars-of-quantifier-fn
          • No-trivial-pairsp
          • Funvars-of-choice-fn
          • Funvar-instp
          • Funvars-of-thm
          • Sofunp
          • Funvarp
          • Sof-instances
          • Sothmp
          • Quant-sofunp
          • Plain-sofunp
          • Funvar-inst-listp
          • Choice-sofunp
          • Sofun-funvars
          • Sofun-kind
          • Function-variables-table
          • Sof-instances-table
          • Second-order-functions-table
        • Gen-macro2-of-macro
        • Defun-inst-implementation
        • Defthm-inst-implementation
        • Defsoft-implementation
        • Defunvar-implementation
        • Defund-sk2-implementation
        • Defun-sk2-implementation
        • Define-sk2-implementation
        • Defchoose2-implementation
        • Defund2-implementation
        • Defun2-implementation
        • Define2-implementation
      • Soft-notions
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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)))))))