hons-alphorder-merge

(in-package "ACL2")

(defsection hons-alphorder-merge
  :parents (alphorder)
  :short "Merge two already-@(see alphorder)ed lists of atoms."
  :long "<p>This is just a completely standard ordered-union operation for
@(see atom-listp)s, except that:</p>

<ul>
 <li>The resulting set is constructed with @(see hons), and</li>
 <li>We @(see memoize) non-recursive calls</li>
</ul>

<p>This is used in @(see aig-vars) and @(see 4v-sexpr-vars).</p>

<p>When the inputs happen to be ordered sets, the result is also an ordered set
and @('hons-alphorder-merge') is nothing more than @(see set::union).</p>"
  (defun hons-alphorder-merge
    (a b)
    (declare (xargs :guard (and (atom-listp a) (atom-listp b))
        :guard-hints (("Goal" :in-theory (enable alphorder symbol<)))
        :measure (+ (len a) (len 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)))))
  (memoize 'hons-alphorder-merge
    :condition '(or (consp a) (consp b))
    :recursive nil)
  (defthm atom-listp-hons-alphorder-merge
    (implies (and (atom-listp a) (atom-listp b))
      (atom-listp (hons-alphorder-merge a b)))
    :hints (("Goal" :in-theory (enable hons-alphorder-merge atom-listp))))
  (defthm member-equal-hons-alphorder-merge
    (iff (member-equal k (hons-alphorder-merge a b))
      (or (member-equal k a) (member-equal k b))))
  (defthm hons-set-equiv-hons-alphorder-merge-append
    (set-equiv (hons-alphorder-merge a b) (append a b))
    :hints ((set-reasoning)))
  (local (in-theory (disable insert-under-set-equiv
        double-containment
        default-car
        default-cdr)))
  (local (defthm l0
      (implies (and (force (atom x)) (force (atom y)))
        (equal (alphorder x y) (or (<< x y) (equal x y))))
      :hints (("Goal" :in-theory (enable << lexorder)))))
  (local (defthm l1 (implies (atom-listp x) (atom (car x)))))
  (local (defthm l2 (implies (atom-listp x) (atom-listp (cdr x)))))
  (local (defthm l3
      (implies (and (setp x)
          (setp y)
          (atom-listp x)
          (atom-listp y))
        (equal (car (hons-alphorder-merge x y))
          (cond ((atom x) (car y))
            ((atom y) (car x))
            ((<< (car y) (car x)) (car y))
            (t (car x)))))
      :hints (("Goal" :induct (hons-alphorder-merge x y)
         :in-theory (e/d* (hons-alphorder-merge (:ruleset primitive-rules))
           (nonempty-means-set setp-of-cons
             <<-trichotomy
             <<-asymmetric
             <<-transitive))))))
  (defthm setp-of-hons-alphorder-merge
    (implies (and (setp x)
        (setp y)
        (atom-listp x)
        (atom-listp y))
      (setp (hons-alphorder-merge x y)))
    :hints (("Goal" :induct (hons-alphorder-merge x y)
       :in-theory (e/d* (hons-alphorder-merge (:ruleset low-level-rules))
         (nonempty-means-set setp-of-cons
           <<-asymmetric
           <<-transitive)))))
  (defthm in-of-hons-alphorder-merge
    (implies (and (setp x)
        (setp y)
        (atom-listp x)
        (atom-listp y))
      (equal (in a (hons-alphorder-merge x y))
        (or (in a x) (in a y))))
    :hints (("Goal" :induct (hons-alphorder-merge x y)
       :in-theory (e/d* (hons-alphorder-merge (:ruleset low-level-rules))
         (subset-in subsetp
           setp-of-cons
           nonempty-means-set
           in-tail
           head-minimal
           in-set
           <<-transitive
           <<-asymmetric)))))
  (defthm hons-alphorder-merge-is-union-for-sets-of-atoms
    (implies (and (setp x)
        (setp y)
        (atom-listp x)
        (atom-listp y))
      (equal (hons-alphorder-merge x y) (union x y)))
    :hints (("Goal" :in-theory (enable double-containment)))))