• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
      • Defun
      • Declare
      • System-utilities
      • Stobj
      • State
      • Mutual-recursion
      • Memoize
      • Mbe
      • Io
      • Defpkg
      • Apply$
      • Loop$
      • Programming-with-state
      • Arrays
      • Characters
      • Time$
      • Defmacro
      • Loop$-primer
      • Fast-alists
      • Defconst
      • Evaluation
      • Guard
      • Equality-variants
      • Compilation
      • Hons
      • ACL2-built-ins
      • Developers-guide
      • System-attachments
      • Advanced-features
      • Set-check-invariant-risk
      • Numbers
      • Efficiency
      • Irrelevant-formals
      • 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
      • Oracle-eval
      • Defmacro-untouchable
      • <<
        • Alphorder
          • Fast-alphorder
          • Hons-alphorder-merge
        • Lexorder
        • Fast-<<
      • Primitive
      • Revert-world
      • Unmemoize
      • Set-duplicate-keys-action
      • Symbols
      • Def-list-constructor
      • Easy-simplify-term
      • Defiteration
      • Fake-oracle-eval
      • Defopen
      • Sleep
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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))))