		Search-engine friendly clone of the ACL2 documentation.

Defequal-event-generation

Defequal-gen-right-to-left

Generate the right-to-left rewrite rule.

Signature
(defequal-gen-right-to-left right-to-left right-to-left-enable name left right x1...xn left-to-right) → (mv local-event exported-event)
Arguments: right-to-left — Guard (symbolp right-to-left).; right-to-left-enable — Guard (booleanp right-to-left-enable).; name — Guard (symbolp name).; left — Guard (symbolp left).; right — Guard (symbolp right).; x1...xn — Guard (symbol-listp x1...xn).; left-to-right — Guard (symbolp left-to-right).
Returns: local-event — Type (pseudo-event-formp local-event).; exported-event — Type (pseudo-event-formp exported-event).

Definitions and Theorems

Function: defequal-gen-right-to-left

(defun defequal-gen-right-to-left
       (right-to-left right-to-left-enable
                      name left right x1...xn left-to-right)
 (declare (xargs :guard (and (symbolp right-to-left)
                             (booleanp right-to-left-enable)
                             (symbolp name)
                             (symbolp left)
                             (symbolp right)
                             (symbol-listp x1...xn)
                             (symbolp left-to-right))))
 (let ((__function__ 'defequal-gen-right-to-left))
  (declare (ignorable __function__))
  (b*
   ((macro (if right-to-left-enable 'defthm
             'defthmd))
    (body
     (cons 'implies
           (cons (cons name 'nil)
                 (cons (cons 'equal
                             (cons (cons right x1...xn)
                                   (cons (cons left x1...xn) 'nil)))
                       'nil))))
    (hints
     (cons
      ':hints
      (cons
       (cons
        (cons
            '"Goal"
            (cons ':in-theory
                  (cons (cons 'quote
                              (cons (cons left-to-right 'nil) 'nil))
                        'nil)))
        'nil)
       'nil)))
    (local-event
         (cons 'local
               (cons (cons macro
                           (cons right-to-left (cons body hints)))
                     'nil)))
    (exported-event (cons macro
                          (cons right-to-left (cons body 'nil)))))
   (mv local-event exported-event))))

Theorem: pseudo-event-formp-of-defequal-gen-right-to-left.local-event

(defthm pseudo-event-formp-of-defequal-gen-right-to-left.local-event
  (b* (((mv ?local-event ?exported-event)
        (defequal-gen-right-to-left
             right-to-left right-to-left-enable
             name left right x1...xn left-to-right)))
    (pseudo-event-formp local-event))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-defequal-gen-right-to-left.exported-event

(defthm
    pseudo-event-formp-of-defequal-gen-right-to-left.exported-event
  (b* (((mv ?local-event ?exported-event)
        (defequal-gen-right-to-left
             right-to-left right-to-left-enable
             name left right x1...xn left-to-right)))
    (pseudo-event-formp exported-event))
  :rule-classes :rewrite)