• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
      • Esim-primitives
      • E-conversion
      • Esim-steps
      • Patterns
        • Pat->al
        • Pat-flatten1
        • Member-of-pat-flatten
        • Similar-patternsp
        • Pat-flatten
        • Al->pat
        • Assoc-pat->al
        • Subsetp-of-pat-flatten
        • Pat->fal
        • Data-for-patternp
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Patterns

Member-of-pat-flatten

(member-of-pat-flatten a pat) is an optimized way to ask if a is a member of (pat-flatten1 pat).

This just avoids actually flattening the pattern, and picks a function with optimized EQ/EQL/EQUAL testing.

Definitions and Theorems

Function: member-eq-of-pat-flatten

(defun
     member-eq-of-pat-flatten (a pat)
     (declare (xargs :guard (symbolp a)))
     (mbe :logic (if (member-equal a (pat-flatten1 pat))
                     t nil)
          :exec (if pat
                    (if (atom pat)
                        (eq a pat)
                        (or (member-eq-of-pat-flatten a (car pat))
                            (member-eq-of-pat-flatten a (cdr pat))))
                    nil)))

Function: member-eql-of-pat-flatten

(defun
    member-eql-of-pat-flatten (a pat)
    (declare (xargs :guard (eqlablep a)))
    (mbe :logic (if (member-equal a (pat-flatten1 pat))
                    t nil)
         :exec (if pat
                   (if (atom pat)
                       (eql a pat)
                       (or (member-eql-of-pat-flatten a (car pat))
                           (member-eql-of-pat-flatten a (cdr pat))))
                   nil)))

Function: member-equal-of-pat-flatten-aux

(defun
 member-equal-of-pat-flatten-aux (a pat)
 (declare (xargs :guard t))
 (mbe
   :logic (if (member-equal a (pat-flatten1 pat))
              t nil)
   :exec (if pat
             (if (atom pat)
                 (equal a pat)
                 (or (member-equal-of-pat-flatten-aux a (car pat))
                     (member-equal-of-pat-flatten-aux a (cdr pat))))
             nil)))

Function: member-of-pat-flatten

(defun
     member-of-pat-flatten (a pat)
     (declare (xargs :guard t))
     (mbe :logic (if (member-equal a (pat-flatten1 pat))
                     t nil)
          :exec (cond ((symbolp a)
                       (member-eq-of-pat-flatten a pat))
                      ((or (acl2-numberp a) (characterp a))
                       (member-eql-of-pat-flatten a pat))
                      (t (member-equal-of-pat-flatten-aux a pat)))))