		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Sothm-inst-proof

Proof builder instructions to prove instances of second-order theorems.

Signature
(sothm-inst-proof sothm fsbs wrld) → instructions
Arguments: sothm — Guard (symbolp sothm).; fsbs — Guard (fun-substp fsbs).; wrld — Guard (plist-worldp wrld).
Returns: instructions — A true-listp.

Instances of second-order theorems are proved using the ACL2 proof builder. Each such instance is proved by first using the :functional-instance determined by sothm-inst-pairs, then using the facts computed by sothm-inst-facts on the subgoals. Each sugoal only needs a subset of those facts, but for simplicity all the facts are used for each subgoal, using the proof builder :repeat command. Since sometimes the facts are not quite identical to the subgoals, the proof builder :prove command is used to iron out any such differences.

Definitions and Theorems

Function: sothm-inst-proof

(defun sothm-inst-proof (sothm fsbs wrld)
 (declare (xargs :guard (and (symbolp sothm)
                             (fun-substp fsbs)
                             (plist-worldp wrld))))
 (let ((__function__ 'sothm-inst-proof))
  (declare (ignorable __function__))
  (cons
   ':instructions
   (cons
    (cons
     (cons ':use
           (cons (cons ':functional-instance
                       (cons sothm (sothm-inst-pairs fsbs wrld)))
                 'nil))
     (cons
         (cons ':repeat
               (cons (cons ':then
                           (cons (cons ':use
                                       (sothm-inst-facts fsbs wrld))
                                 '(:prove)))
                     'nil))
         'nil))
    'nil))))