Sothm-inst-facts
Create list of facts for functional instantiation.
- Signature
(sothm-inst-facts fsbs wrld) → fact-names
- Arguments
- fsbs — Guard (fun-substp fsbs).
- wrld — Guard (plist-worldp wrld).
- Returns
- fact-names — A symbol-listp.
When a :functional-instance is used in a proof,
proof subgoals are created to ensure that the replacing functions
satisfy all the constraints of the replaced functions.
In a :functional-instance with a function substitution S
as calculated by ext-fun-subst-term/terms/function,
each function variable (which comes from the instantiation)
has no constraints and so no subgoals are generated for them.
Each second-order function sofun in S
has the following constraints:
- If sofun is a plain second-order function,
the constraint is that
the application of S to the definition of sofun is a theorem,
which follows by the construction of the instance fun of sofun,
i.e. it follows from the definition of fun.
- If sofun is a choice second-order function,
the constraint is that
the application of S to the choice axiom of sofun is a theorem,
which follows by the construction of the instance fun of sofun,
i.e. it follows from the choice axiom of fun.
- If sofun is a quantifier second-order function,
the constraints are that
(1) the application of S
to the rewrite rule generated by the defun-sk of sofun,
and (2) the application of S to the definition of sofun
(or to the defining theorem of sofun
if sofun was introduced with :constrain t),
are both theorems,
which both follow by the construction
of the instance fun of sofun,
i.e. they follow from
(1) the rewrite rule generated by the defun-sk of fun
and (2) the definition of fun
(or the defining theorem of fun
if fun was introduced with :constrain nil).
The list of facts needed to prove these constraints is determined
by the function substitution S.
For each pair (fun1 . fun2) of the function substitution:
- If fun1 is a plain second-order function,
the fact used in the proof is the definition of fun2,
whose name is the name of fun2.
(Note that by construction, since fun2 is an instance of fun1,
fun2 is introduced by a defun.)
- If fun1 is a choice second-order function,
the fact used in the proof is the defchoose axiom of fun2,
whose name is the name of fun2.
(Note that by construction, since fun2 is an instance of fun1,
fun2 is introduced by a defchoose.)
- If fun1 is a quantifier second-order function,
the facts used in the proof are
(1) the defun-sk rewrite rule of fun2
and (2)
either (i) the definition of fun2
(if fun2 was introduced with :constrain nil),
whose name is the name of fun2,
or (ii) the defining theorem of fun2
(if fun2 was introduced with :constrain t),
whose name is fun2 followed by -definition.
(Note that by construction, since fun2 is an instance of fun1,
fun2 is introduced by a defun-sk.)
- Otherwise, fun1 is a function variable, which has no constraints,
so no fact is used in the proof.
Definitions and Theorems
Function: sothm-inst-facts
(defun sothm-inst-facts (fsbs wrld)
(declare (xargs :guard (and (fun-substp fsbs)
(plist-worldp wrld))))
(let ((__function__ 'sothm-inst-facts))
(declare (ignorable __function__))
(if (endp fsbs)
nil
(let* ((pair (car fsbs))
(1st (car pair))
(2nd (cdr pair)))
(cond ((or (plain-sofunp 1st wrld)
(choice-sofunp 1st wrld))
(cons 2nd (sothm-inst-facts (cdr fsbs) wrld)))
((quant-sofunp 1st wrld)
(cons (defun-sk-rewrite-name 2nd wrld)
(cons (if (definedp 2nd wrld)
2nd
(defun-sk-definition-name 2nd wrld))
(sothm-inst-facts (cdr fsbs) wrld))))
(t (sothm-inst-facts (cdr fsbs) wrld)))))))
