Filtering...

duplicated-members

books/defsort/duplicated-members

Included Books

uniquep sets no-duplicatesp
other
(in-package "ACL2")
include-book
(include-book "uniquep")
local
(local (include-book "std/lists/sets" :dir :system))
local
(local (include-book "std/lists/no-duplicatesp" :dir :system))
collect-adjacent-duplicatesfunction
(defund collect-adjacent-duplicates
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) nil)
    ((atom (cdr x)) nil)
    ((equal (first x) (second x)) (if (atom (cddr x))
        (list (first x))
        (if (not (equal (first x) (third x)))
          (cons (first x) (collect-adjacent-duplicates (cddr x)))
          (collect-adjacent-duplicates (cdr x)))))
    (t (collect-adjacent-duplicates (cdr x)))))
collect-adjacent-duplicates-when-not-consptheorem
(defthm collect-adjacent-duplicates-when-not-consp
  (implies (not (consp x))
    (equal (collect-adjacent-duplicates x) nil))
  :hints (("Goal" :in-theory (enable collect-adjacent-duplicates))))
collect-adjacent-duplicates-when-not-consp-of-cdrtheorem
(defthm collect-adjacent-duplicates-when-not-consp-of-cdr
  (implies (not (consp (cdr x)))
    (equal (collect-adjacent-duplicates x) nil))
  :hints (("Goal" :in-theory (enable collect-adjacent-duplicates))))
collect-adjacent-duplicates-of-cons-and-constheorem
(defthm collect-adjacent-duplicates-of-cons-and-cons
  (equal (collect-adjacent-duplicates (cons a (cons b x)))
    (if (equal a b)
      (if (not (consp x))
        (list a)
        (if (equal a (car x))
          (collect-adjacent-duplicates (cons a x))
          (cons a (collect-adjacent-duplicates x))))
      (collect-adjacent-duplicates (cons b x))))
  :hints (("Goal" :in-theory (enable collect-adjacent-duplicates))))
member-equal-of-collect-adjacent-duplicates-when-<<-ordered-pencapsulate
(encapsulate nil
  (local (defthm lemma
      (implies (and (member-equal a (collect-adjacent-duplicates (cons x1 x4)))
          (not (<< b a))
          (<< b x1))
        (member-equal a (collect-adjacent-duplicates x4)))
      :hints (("Goal" :in-theory (enable collect-adjacent-duplicates)))))
  (local (defthm lemma2
      (implies (and (<<-ordered-p x)
          (equal (duplicity a x) 1)
          (not (<< b a))
          (<< b (car x)))
        (member-equal a (collect-adjacent-duplicates (cons b x))))
      :hints (("Goal" :in-theory (enable <<-ordered-p)))))
  (local (defthm lemma3
      (implies (and (<<-ordered-p x)
          (equal (duplicity a x) 1)
          (not (<< b a))
          (not (<< (car x) b)))
        (member-equal a (collect-adjacent-duplicates (cons b x))))
      :hints (("Goal" :in-theory (enable <<-ordered-p)))))
  (local (defthm lemma4
      (implies (and (<<-ordered-p x) (< 1 (duplicity a x)))
        (member-equal a (collect-adjacent-duplicates x)))
      :hints (("Goal" :in-theory (enable <<-ordered-p collect-adjacent-duplicates)))))
  (local (defthm lemma5
      (implies (and (<<-ordered-p x) (not (< 1 (duplicity a x))))
        (not (member-equal a (collect-adjacent-duplicates x))))
      :hints (("Goal" :in-theory (enable <<-ordered-p collect-adjacent-duplicates duplicity)))))
  (defthm member-equal-of-collect-adjacent-duplicates-when-<<-ordered-p
    (implies (<<-ordered-p x)
      (iff (member-equal a (collect-adjacent-duplicates x))
        (< 1 (duplicity a x))))))
no-duplicatesp-equal-of-collect-adjacent-duplicates-when-<<-ordered-pencapsulate
(encapsulate nil
  (local (defthm crock0
      (implies (<<-ordered-p x) (<<-ordered-p (cdr x)))
      :hints (("Goal" :in-theory (enable <<-ordered-p)))))
  (local (defthm crock1
      (implies (no-duplicatesp-equal x)
        (equal (duplicity a x)
          (if (member-equal a x)
            1
            0)))
      :hints (("Goal" :in-theory (enable duplicity)))))
  (local (defthm crock3
      (implies (and (no-duplicatesp-equal (collect-adjacent-duplicates (cons b x)))
          (<<-ordered-p x)
          (<< a b)
          (not (<< (car x) b)))
        (<= (duplicity a x) 1))
      :hints (("Goal" :in-theory (enable duplicity <<-ordered-p collect-adjacent-duplicates)))))
  (defthm no-duplicatesp-equal-of-collect-adjacent-duplicates-when-<<-ordered-p
    (implies (<<-ordered-p x)
      (no-duplicatesp-equal (collect-adjacent-duplicates x)))
    :hints (("Goal" :in-theory (enable collect-adjacent-duplicates <<-ordered-p)))))
duplicated-membersfunction
(defund duplicated-members
  (x)
  (declare (xargs :guard (true-listp x)))
  (collect-adjacent-duplicates (<<-sort x)))
member-equal-of-duplicated-memberstheorem
(defthm member-equal-of-duplicated-members
  (iff (member-equal a (duplicated-members x))
    (< 1 (duplicity a x)))
  :hints (("Goal" :in-theory (enable duplicated-members))))
no-duplicatesp-equal-of-duplicated-memberstheorem
(defthm no-duplicatesp-equal-of-duplicated-members
  (no-duplicatesp-equal (duplicated-members x))
  :hints (("Goal" :in-theory (enable duplicated-members))))
local
(local (defthm element-p-by-duplicity-in-element-list-p
    (implies (and (element-list-p x) (< 0 (duplicity a x)))
      (element-p a))))
local
(local (defthm element-list-p-when-subset-of-duplicated-members
    (implies (and (subsetp x (duplicated-members y)) (element-list-p y))
      (equal (element-list-p x)
        (or (element-list-final-cdr-p t) (true-listp x))))))
other
(def-listp-rule element-list-p-of-duplicated-members
  (implies (element-list-p x)
    (element-list-p (duplicated-members x)))
  :hints (("goal" :use ((:instance element-list-p-when-subset-of-duplicated-members
        (y x)
        (x (duplicated-members x))))
     :in-theory (disable element-list-p-when-subset-of-duplicated-members)))
  :tags (:duplicated-members))
duplicated-members-under-iffencapsulate
(encapsulate nil
  (local (defthm l0
      (implies (duplicated-members x)
        (not (no-duplicatesp-equal x)))
      :hints (("Goal" :in-theory (disable no-duplicatesp-equal-when-high-duplicity
           member-equal-of-duplicated-members)
         :use ((:instance no-duplicatesp-equal-when-high-duplicity
            (a (car (duplicated-members x)))) (:instance member-equal-of-duplicated-members
             (a (car (duplicated-members x)))))))))
  (local (defthm l1
      (implies (not (duplicated-members x))
        (no-duplicatesp-equal x))
      :hints (("Goal" :in-theory (disable member-equal-of-duplicated-members)
         :use ((:instance member-equal-of-duplicated-members
            (a (car (duplicity-badguy x)))
            (x x)))))))
  (defthm duplicated-members-under-iff
    (iff (duplicated-members x) (not (no-duplicatesp-equal x)))))
hons-duplicity-alist-pfunction
(defund hons-duplicity-alist-p
  (x)
  (declare (xargs :guard t))
  (if (consp x)
    (and (consp (car x))
      (natp (cdar x))
      (hons-duplicity-alist-p (cdr x)))
    (not x)))
hons-duplicity-alist-p-when-not-consptheorem
(defthm hons-duplicity-alist-p-when-not-consp
  (implies (not (consp x))
    (equal (hons-duplicity-alist-p x) (not x)))
  :hints (("Goal" :in-theory (enable hons-duplicity-alist-p))))
hons-duplicity-alist-p-of-constheorem
(defthm hons-duplicity-alist-p-of-cons
  (equal (hons-duplicity-alist-p (cons a x))
    (and (consp a) (natp (cdr a)) (hons-duplicity-alist-p x)))
  :hints (("Goal" :in-theory (enable hons-duplicity-alist-p))))
alistp-when-hons-duplicity-alist-ptheorem
(defthm alistp-when-hons-duplicity-alist-p
  (implies (hons-duplicity-alist-p x) (alistp x))
  :hints (("Goal" :induct (len x))))
hons-duplicity-alist-auxfunction
(defund hons-duplicity-alist-aux
  (x alist)
  (declare (xargs :guard (hons-duplicity-alist-p alist)))
  (if (atom x)
    alist
    (hons-duplicity-alist-aux (cdr x)
      (hons-acons (car x)
        (+ 1 (nfix (cdr (hons-get (car x) alist))))
        alist))))
hons-duplicity-alist-p-of-hons-duplicity-alist-auxtheorem
(defthm hons-duplicity-alist-p-of-hons-duplicity-alist-aux
  (implies (hons-duplicity-alist-p alist)
    (hons-duplicity-alist-p (hons-duplicity-alist-aux x alist)))
  :hints (("Goal" :in-theory (enable hons-duplicity-alist-aux))))
hons-assoc-equal-of-hons-duplicity-alist-auxtheorem
(defthm hons-assoc-equal-of-hons-duplicity-alist-aux
  (implies (hons-duplicity-alist-p alist)
    (equal (hons-assoc-equal a (hons-duplicity-alist-aux x alist))
      (if (or (member-equal a x) (hons-assoc-equal a alist))
        (cons a
          (+ (duplicity a x) (nfix (cdr (hons-assoc-equal a alist)))))
        nil)))
  :hints (("Goal" :in-theory (enable hons-duplicity-alist-aux duplicity)
     :do-not '(generalize fertilize)
     :induct (hons-duplicity-alist-aux x alist))))
hons-duplicity-alistfunction
(defund hons-duplicity-alist
  (x)
  (declare (xargs :guard t))
  (hons-shrink-alist (hons-duplicity-alist-aux x nil) nil))
hons-duplicity-alist-p-of-hons-shrink-alisttheorem
(defthm hons-duplicity-alist-p-of-hons-shrink-alist
  (implies (and (hons-duplicity-alist-p alist)
      (hons-duplicity-alist-p ans))
    (hons-duplicity-alist-p (hons-shrink-alist alist ans)))
  :hints (("Goal" :in-theory (enable hons-shrink-alist))))
hons-duplicity-alist-p-of-hons-duplicity-alisttheorem
(defthm hons-duplicity-alist-p-of-hons-duplicity-alist
  (hons-duplicity-alist-p (hons-duplicity-alist x))
  :hints (("Goal" :in-theory (enable hons-duplicity-alist))))
local
(local (defthm iff-of-hons-assoc-equal
    (implies (alistp x)
      (iff (hons-assoc-equal a x) (member-equal a (strip-cars x))))))
no-duplicatesp-equal-of-strip-cars-of-hons-shrink-alisttheorem
(defthm no-duplicatesp-equal-of-strip-cars-of-hons-shrink-alist
  (implies (alistp y)
    (equal (no-duplicatesp-equal (strip-cars (hons-shrink-alist x y)))
      (no-duplicatesp-equal (strip-cars y))))
  :hints (("Goal" :in-theory (enable hons-shrink-alist))))
no-duplicatesp-equal-of-strip-cars-of-hons-duplicity-alisttheorem
(defthm no-duplicatesp-equal-of-strip-cars-of-hons-duplicity-alist
  (no-duplicatesp-equal (strip-cars (hons-duplicity-alist x)))
  :hints (("Goal" :in-theory (enable hons-duplicity-alist))))
hons-assoc-equal-of-hons-shrink-alisttheorem
(defthm hons-assoc-equal-of-hons-shrink-alist
  (equal (hons-assoc-equal a (hons-shrink-alist x y))
    (or (hons-assoc-equal a y) (hons-assoc-equal a x)))
  :hints (("Goal" :in-theory (enable hons-shrink-alist))))
hons-assoc-equal-of-hons-duplicity-alisttheorem
(defthm hons-assoc-equal-of-hons-duplicity-alist
  (equal (hons-assoc-equal a (hons-duplicity-alist x))
    (if (member-equal a x)
      (cons a (duplicity a x))
      nil))
  :hints (("Goal" :in-theory (enable hons-duplicity-alist))))
hons-duplicated-members-auxfunction
(defund hons-duplicated-members-aux
  (alist)
  (declare (xargs :guard (alistp alist)))
  (cond ((atom alist) nil)
    ((> (nfix (cdar alist)) 1) (cons (caar alist)
        (hons-duplicated-members-aux (cdr alist))))
    (t (hons-duplicated-members-aux (cdr alist)))))
member-equal-of-strip-cars-when-member-equal-of-hons-duplicated-members-auxtheorem
(defthm member-equal-of-strip-cars-when-member-equal-of-hons-duplicated-members-aux
  (implies (member-equal a (hons-duplicated-members-aux x))
    (member-equal a (strip-cars x)))
  :hints (("Goal" :in-theory (enable hons-duplicated-members-aux))))
member-equal-of-hons-duplicated-members-auxtheorem
(defthm member-equal-of-hons-duplicated-members-aux
  (implies (no-duplicatesp-equal (strip-cars x))
    (iff (member-equal a (hons-duplicated-members-aux x))
      (> (nfix (cdr (hons-assoc-equal a x))) 1)))
  :hints (("Goal" :in-theory (enable hons-duplicated-members-aux))))
no-duplicatesp-equal-of-hons-duplicated-members-auxtheorem
(defthm no-duplicatesp-equal-of-hons-duplicated-members-aux
  (implies (no-duplicatesp-equal (strip-cars alist))
    (no-duplicatesp-equal (hons-duplicated-members-aux alist)))
  :hints (("Goal" :in-theory (enable hons-duplicated-members-aux))))
hons-duplicated-membersfunction
(defund hons-duplicated-members
  (x)
  (declare (xargs :guard t))
  (let* ((dalist (hons-duplicity-alist x)) (result (hons-duplicated-members-aux dalist)))
    (prog2$ (flush-hons-get-hash-table-link dalist) result)))
member-equal-of-hons-duplicated-memberstheorem
(defthm member-equal-of-hons-duplicated-members
  (iff (member-equal a (hons-duplicated-members x))
    (< 1 (duplicity a x)))
  :hints (("Goal" :in-theory (enable hons-duplicated-members))))
no-duplicatesp-equal-of-hons-duplicated-memberstheorem
(defthm no-duplicatesp-equal-of-hons-duplicated-members
  (no-duplicatesp-equal (hons-duplicated-members x))
  :hints (("Goal" :in-theory (enable hons-duplicated-members))))