		Search-engine friendly clone of the ACL2 documentation.

Solve-event-generation

Solve-gen-ACL2-rewriter-theorem

Generate a local theorem for the rewriting performed by the ACL2 rewriter.

Signature
(solve-gen-acl2-rewriter-theorem matrix rewritten-term used-rules names-to-avoid wrld) → (mv event name updated-names-to-avoid)
Arguments: matrix — Guard (pseudo-termp matrix).; rewritten-term — Guard (pseudo-termp rewritten-term).; used-rules — Guard (symbol-listp used-rules).; 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.

If solve-gen-solution-ACL2-rewriter succeeds, it should be the case that the matrix of old is equal to the rewritten term, but the ACL2 rewriter does not quite produce a replayable ACL2 proof of that. However, in order to prove the refinement theorem, we need an ACL2 theorem asserting that the matrix is equal to the rewritten term.

So here we attempt to generate a local theorem asserting that. The programmatic interface to the ACL2 rewriter returns the rules used by the rewriting. Thus, we attempt to prove the theorem in the theory consisting of these rules, assuming that ACL2 will perform the same rewrites in the theorem. Note, however, that the returned list of rules may include the ``fake'' rules for linear arithmetic and other proof methods. Thus, we use a utility to drop all of those.

Definitions and Theorems

Function: solve-gen-acl2-rewriter-theorem

(defun solve-gen-acl2-rewriter-theorem
       (matrix rewritten-term
               used-rules names-to-avoid wrld)
 (declare (xargs :guard (and (pseudo-termp matrix)
                             (pseudo-termp rewritten-term)
                             (symbol-listp used-rules)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'solve-gen-acl2-rewriter-theorem))
  (declare (ignorable __function__))
  (b*
   (((mv name names-to-avoid)
     (fresh-logical-name-with-$s-suffix 'acl2-rewriting
                                        nil names-to-avoid wrld))
    (used-rules (drop-fake-runes used-rules))
    (event
     (cons
      'local
      (cons
       (cons
        'defthmd
        (cons
         name
         (cons
          (cons 'equal
                (cons matrix (cons rewritten-term 'nil)))
          (cons
           ':hints
           (cons
            (cons
              (cons '"Goal"
                    (cons ':in-theory
                          (cons (cons 'quote (cons used-rules 'nil))
                                'nil)))
              'nil)
            'nil)))))
       'nil))))
   (mv event name names-to-avoid))))