• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
      • Defun
      • Declare
      • System-utilities
      • Stobj
      • State
      • Memoize
      • Mbe
      • Io
      • Apply$
      • Defpkg
      • Mutual-recursion
      • Loop$
      • Programming-with-state
      • Arrays
      • Characters
      • Time$
      • Loop$-primer
      • Fast-alists
      • Defmacro
      • Defconst
      • Guard
      • Evaluation
      • Equality-variants
      • Compilation
      • Hons
      • ACL2-built-ins
      • System-attachments
      • Advanced-features
      • Set-check-invariant-risk
      • Developers-guide
      • Numbers
      • Irrelevant-formals
      • Efficiency
      • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
      • Redefining-programs
      • Lists
      • Invariant-risk
      • Errors
      • Defabbrev
      • Conses
      • Alists
      • Set-register-invariant-risk
      • Strings
      • Program-wrapper
      • Get-internal-time
      • Basics
      • Packages
      • Defmacro-untouchable
      • Primitive
      • <<
        • Alphorder
          • Fast-alphorder
          • Hons-alphorder-merge
        • Lexorder
        • Fast-<<
      • Revert-world
      • Set-duplicate-keys-action
      • Unmemoize
      • Symbols
      • Def-list-constructor
      • Easy-simplify-term
      • Defiteration
      • Defopen
      • Sleep
    • Start-here
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Alphorder

Hons-alphorder-merge

Merge two already-alphordered lists of atoms.

This is just a completely standard ordered-union operation for atom-listps, except that:

• The resulting set is constructed with hons, and
• We memoize non-recursive calls

This is used in aig-vars and 4v-sexpr-vars.

When the inputs happen to be ordered sets, the result is also an ordered set and hons-alphorder-merge is nothing more than set::union.

Definitions and Theorems

Function: hons-alphorder-merge

(defun hons-alphorder-merge (a b)
       (declare (xargs :guard (and (atom-listp a) (atom-listp b))))
       (cond ((atom a) b)
             ((atom b) a)
             ((equal (car a) (car b))
              (hons-alphorder-merge (cdr a) b))
             ((fast-alphorder (car b) (car a))
              (hons (car b)
                    (hons-alphorder-merge a (cdr b))))
             (t (hons (car a)
                      (hons-alphorder-merge (cdr a) b)))))

Function: hons-alphorder-merge-memoize-condition

(defun hons-alphorder-merge-memoize-condition
       (a b)
       (declare (ignorable a b)
                (xargs :guard (if (atom-listp a)
                                  (atom-listp b)
                                  'nil)))
       (or (consp a) (consp b)))

Theorem: atom-listp-hons-alphorder-merge

(defthm atom-listp-hons-alphorder-merge
        (implies (and (atom-listp a) (atom-listp b))
                 (atom-listp (hons-alphorder-merge a b))))

Theorem: member-equal-hons-alphorder-merge

(defthm member-equal-hons-alphorder-merge
        (iff (member-equal k (hons-alphorder-merge a b))
             (or (member-equal k a)
                 (member-equal k b))))

Theorem: hons-set-equiv-hons-alphorder-merge-append

(defthm hons-set-equiv-hons-alphorder-merge-append
        (set-equiv (hons-alphorder-merge a b)
                   (append a b)))

Theorem: setp-of-hons-alphorder-merge

(defthm setp-of-hons-alphorder-merge
        (implies (and (set::setp x)
                      (set::setp y)
                      (atom-listp x)
                      (atom-listp y))
                 (set::setp (hons-alphorder-merge x y))))

Theorem: in-of-hons-alphorder-merge

(defthm in-of-hons-alphorder-merge
        (implies (and (set::setp x)
                      (set::setp y)
                      (atom-listp x)
                      (atom-listp y))
                 (equal (set::in a (hons-alphorder-merge x y))
                        (or (set::in a x) (set::in a y)))))

Theorem: hons-alphorder-merge-is-union-for-sets-of-atoms

(defthm hons-alphorder-merge-is-union-for-sets-of-atoms
        (implies (and (set::setp x)
                      (set::setp y)
                      (atom-listp x)
                      (atom-listp y))
                 (equal (hons-alphorder-merge x y)
                        (set::union x y))))