• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
      • Soft-future-work
      • Soft-macros
        • Defun-inst
        • Defequal
          • Defequal-implementation
            • Defequal-fn
            • Defequal-event-generation
              • Defequal-gen-everything
              • Defequal-gen-equality
              • Defequal-gen-right-to-left
              • Defequal-gen-theory-invariant
            • Defequal-input-processing
            • Defequal-table
            • Defequal-macro-definition
        • Defsoft
        • Defthm-inst
        • Defun2
        • Defunvar
        • Defun-sk2
        • Defchoose2
        • Defthm-2nd-order
        • Define-sk2
        • Defund-sk2
        • Define2
        • Defund2
      • Updates-to-workshop-material
      • Soft-implementation
      • Soft-notions
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defequal-event-generation

Defequal-gen-equality

Generate the equality function.

Signature

(defequal-gen-equality name 
                       left right x1...xn enable verify-guards 
                       left-to-right left-to-right-enable) 
 
  → 
(mv local-event exported-event)

Arguments

name — Guard (symbolp name).

left — Guard (symbolp left).

right — Guard (symbolp right).

x1...xn — Guard (symbol-listp x1...xn).

enable — Guard (booleanp enable).

verify-guards — Guard (booleanp verify-guards).

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-equality

(defun defequal-gen-equality
       (name left right x1...xn enable verify-guards
             left-to-right left-to-right-enable)
 (declare (xargs :guard (and (symbolp name)
                             (symbolp left)
                             (symbolp right)
                             (symbol-listp x1...xn)
                             (booleanp enable)
                             (booleanp verify-guards)
                             (symbolp left-to-right))))
 (let ((__function__ 'defequal-gen-equality))
  (declare (ignorable __function__))
  (b*
   ((macro (if enable 'defun-sk2 'defund-sk2))
    (body
     (cons
          'forall
          (cons x1...xn
                (cons (cons 'equal
                            (cons (cons left x1...xn)
                                  (cons (cons right x1...xn) 'nil)))
                      'nil))))
    (declare
     (cons
         'declare
         (cons (cons 'xargs
                     (cons ':guard
                           (cons 't
                                 (cons ':verify-guards
                                       (cons verify-guards 'nil)))))
               'nil)))
    (options (cons ':rewrite
                   (cons ':direct
                         (cons ':thm-name
                               (cons left-to-right
                                     (and (not enable)
                                          left-to-right-enable
                                          (list :thm-enable t)))))))
    (local-event
     (cons
      'local
      (cons
       (cons
        macro
        (cons
         name
         (cons
          'nil
          (cons
           declare
           (append
            (and
             verify-guards
             '((declare
                   (xargs :guard-hints (("Goal" :in-theory nil))))))
            (cons body options))))))
       'nil)))
    (exported-event
         (cons macro
               (cons name
                     (cons 'nil
                           (cons declare (cons body options)))))))
   (mv local-event exported-event))))

Theorem: pseudo-event-formp-of-defequal-gen-equality.local-event

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

Theorem: pseudo-event-formp-of-defequal-gen-equality.exported-event

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