Generate the theorem asserting the correctness of the solution, from the rewriting theorem.
(solve-gen-solution-theorem-from-rewriting-theorem old x1...xn ?f f rewriting-theorem print names-to-avoid wrld) → (mv events name old-instance updated-names-to-avoid)
This is used when using a rewriting solution method.
This is the theorem
Since the theorem is about the instance of
The proof follows the design notes,
but those use a second-order notation and explicit quantification,
so here we need to do things a little differently.
We generate the instance of the rewriting theorem
that instantiates
We return a list of events, along with the name of the final theorem.
Function:
(defun solve-gen-solution-theorem-from-rewriting-theorem (old x1...xn ?f f rewriting-theorem print names-to-avoid wrld) (declare (xargs :guard (and (symbolp old) (symbol-listp x1...xn) (symbolp ?f) (symbolp f) (symbolp rewriting-theorem) (evmac-input-print-p print) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'solve-gen-solution-theorem-from-rewriting-theorem)) (declare (ignorable __function__)) (b* (((mv old-instance names-to-avoid) (fresh-logical-name-with-$s-suffix 'old-instance 'function names-to-avoid wrld)) ((mv rewriting-theorem-instance names-to-avoid) (fresh-logical-name-with-$s-suffix 'rewriting-theorem-instance nil names-to-avoid wrld)) ((mv solution-theorem names-to-avoid) (fresh-logical-name-with-$s-suffix 'solution-theorem nil names-to-avoid wrld)) (old-instance-event (cons 'local (cons (cons 'soft::defun-inst (cons old-instance (cons (cons old (cons (cons ?f f) 'nil)) (cons ':print (cons (and (eq print :all) :all) 'nil))))) 'nil))) (rewriting-theorem-instance-event (cons 'local (cons (cons 'soft::defthm-inst (cons rewriting-theorem-instance (cons (cons rewriting-theorem (cons (cons ?f f) 'nil)) (cons ':print (cons (and (eq print :all) :all) 'nil))))) 'nil))) (old-instance-witness (add-suffix-to-fn old-instance "-WITNESS")) (instantiation (if (>= (len x1...xn) 2) (loop$ for xi in x1...xn as i from 0 to (1- (len x1...xn)) collect (cons xi (cons (cons 'mv-nth (cons i (cons (cons old-instance-witness 'nil) 'nil))) 'nil))) (list (list (car x1...xn) (cons old-instance-witness 'nil))))) (solution-theorem-event (cons 'local (cons (cons 'defthm (cons solution-theorem (cons (cons old-instance 'nil) (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons old-instance (cons f 'nil)) 'nil)) (cons ':use (cons (cons ':instance (cons rewriting-theorem-instance instantiation)) 'nil))))) 'nil) 'nil))))) 'nil)))) (mv (list old-instance-event rewriting-theorem-instance-event solution-theorem-event) solution-theorem old-instance names-to-avoid))))