		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-algo-correct

Generate a local theorem asserting the correctness of algo[?f1]...[?fp].

Signature
(schemalg-gen-algo-correct schema x-x1...xn x-a1...am x y iorel algo spec-0 spec-1 spec-2 names-to-avoid wrld) → (mv event name updated-names-to-avoid)
Arguments: schema — Guard (keywordp schema).; x-x1...xn — Guard (symbol-listp x-x1...xn).; x-a1...am — Guard (symbol-listp x-a1...am).; x — Guard (symbolp x).; y — Guard (symbolp y).; iorel — Guard (pseudo-lambdap iorel).; algo — Guard (symbolp algo).; spec-0 — Guard (symbolp spec-0).; spec-1 — Guard (symbolp spec-1).; spec-2 — Guard (symbolp spec-2).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: event — A pseudo-event-formp.; name — A symbolp.; updated-names-to-avoid — A symbol-listp.

This is the theorem \mathit{COR} in the design notes. It is not described in the user documentation, because it is generated only locally.

Definitions and Theorems

Function: schemalg-gen-algo-correct

(defun schemalg-gen-algo-correct
       (schema x-x1...xn
               x-a1...am x y iorel algo spec-0
               spec-1 spec-2 names-to-avoid wrld)
 (declare (xargs :guard (and (keywordp schema)
                             (symbol-listp x-x1...xn)
                             (symbol-listp x-a1...am)
                             (symbolp x)
                             (symbolp y)
                             (pseudo-lambdap iorel)
                             (symbolp algo)
                             (symbolp spec-0)
                             (symbolp spec-1)
                             (symbolp spec-2)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'schemalg-gen-algo-correct))
  (declare (ignorable __function__))
  (case schema
    (:divconq-list-0-1 (schemalg-gen-algo-correct-divconq-list-0-1
                            x-x1...xn x-a1...am x y iorel
                            algo spec-0 spec-1 names-to-avoid wrld))
    (:divconq-list-0-1-2 (schemalg-gen-algo-correct-divconq-list-0-1-2
                              x-x1...xn
                              x-a1...am x y iorel algo spec-0
                              spec-1 spec-2 names-to-avoid wrld))
    (:divconq-oset-0-1 (schemalg-gen-algo-correct-divconq-oset-0-1
                            x-x1...xn x-a1...am x y iorel
                            algo spec-0 spec-1 names-to-avoid wrld))
    (t (prog2$ (raise "Internal error: unknown schema ~x0."
                      schema)
               (mv '(irrelevant)
                   nil names-to-avoid))))))