		Search-engine friendly clone of the ACL2 documentation.

Solve-event-generation

Solve-gen-axe-rewriter-theorem

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

Signature
(solve-gen-axe-rewriter-theorem matrix rewritten-term method-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).; method-rules — Guard (symbol-listp method-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-axe-rewriter succeeds, it should be the case that the matrix of old is equal to the rewritten term, but the Axe rewriter does not 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. Our proof strategy is fairly crude for now: we simply enable the rules passed to the Axe rewriter, hoping that ACL2 can perform the same rewritings. We add these to the current ACL2 theory, just in case we may need some other basic rules. Clearly, this strategy should be refined significantly.

Definitions and Theorems

Function: solve-gen-axe-rewriter-theorem

(defun solve-gen-axe-rewriter-theorem
       (matrix rewritten-term
               method-rules names-to-avoid wrld)
 (declare (xargs :guard (and (pseudo-termp matrix)
                             (pseudo-termp rewritten-term)
                             (symbol-listp method-rules)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'solve-gen-axe-rewriter-theorem))
  (declare (ignorable __function__))
  (b*
   (((mv name names-to-avoid)
     (fresh-logical-name-with-$s-suffix 'axe-rewriting
                                        nil names-to-avoid wrld))
    (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 'enable method-rules)
                                         'nil)))
                       'nil)
                 'nil)))))
       'nil))))
   (mv event name names-to-avoid))))