Filtering...

hons-sets

books/centaur/misc/hons-sets

Included Books

remove-duplicates hons-help2 equal-sets alist-defs
other
(in-package "ACL2")
include-book
(include-book "std/lists/remove-duplicates" :dir :system)
include-book
(include-book "misc/hons-help2" :dir :system)
include-book
(include-book "equal-sets")
is-prefixfunction
(defun is-prefix
  (x y)
  (or (atom x)
    (and (equal (car x) (car y)) (is-prefix (cdr x) (cdr y)))))
subgoal-offunction
(defun subgoal-of
  (goal id)
  (declare (xargs :mode :program))
  (let ((goal (parse-clause-id goal)))
    (and (is-prefix (car goal) (car id))
      (or (not (equal (car goal) (car id)))
        (and (is-prefix (cadr goal) (cadr id))
          (or (not (equal (cadr goal) (cadr id)))
            (< (cddr goal) (cddr id))))))))
hons-member-equal-member-equaltheorem
(defthm hons-member-equal-member-equal
  (equal (hons-member-equal a b) (member-equal a b)))
hons-assoc-equal-hons-put-list-ifftheorem
(defthm hons-assoc-equal-hons-put-list-iff
  (iff (hons-assoc-equal x (hons-put-list a b c))
    (or (member-equal x a) (hons-assoc-equal x c)))
  :hints (("goal" :induct (hons-put-list a b c))))
hons-union2-membertheorem
(defthm hons-union2-member
  (iff (member-equal x (hons-union2 a b c))
    (or (and (member-equal x a) (not (member-equal x b)))
      (member-equal x c))))
hons-union1-membertheorem
(defthm hons-union1-member
  (iff (member-equal x (hons-union1 a b c))
    (or (and (member-equal x a) (not (hons-get x b)))
      (member-equal x c))))
hons-union-membertheorem
(defthm hons-union-member
  (iff (member-equal x (hons-union a b))
    (or (member-equal x a) (member-equal x b))))
hons-int1-is-intersection-equaltheorem
(defthm hons-int1-is-intersection-equal
  (implies (atom atom)
    (equal (hons-int1 x (hons-put-list y t atom))
      (intersection-equal x y)))
  :hints (("Goal" :in-theory (enable intersection-equal))))
hons-intersection2-is-intersection-equaltheorem
(defthm hons-intersection2-is-intersection-equal
  (equal (hons-intersection2 x y) (intersection-equal x y))
  :hints (("Goal" :in-theory (enable intersection-equal))))
hons-set-diff2-membertheorem
(defthm hons-set-diff2-member
  (iff (member-equal x (hons-set-diff2 a b))
    (and (member-equal x a) (not (member-equal x b)))))
hons-sd1-membertheorem
(defthm hons-sd1-member
  (iff (member-equal x (hons-sd1 a b))
    (and (member-equal x a) (not (hons-assoc-equal x b)))))
hons-set-diff-membertheorem
(defthm hons-set-diff-member
  (iff (member-equal x (hons-set-diff a b))
    (and (member-equal x a) (not (member-equal x b)))))
in-theory
(in-theory (disable hons-union hons-intersection hons-set-diff))
local
(local (set-default-hints '((set-reasoning))))
hons-union-set-equiv-union-equaltheorem
(defthm hons-union-set-equiv-union-equal
  (set-equiv (hons-union x y) (union-equal x y)))
hons-set-diff-set-equiv-set-diff-equaltheorem
(defthm hons-set-diff-set-equiv-set-diff-equal
  (set-equiv (hons-set-diff x y) (set-difference-equal x y)))
other
(defcong set-equiv iff (hons-member-equal a b) 2)
other
(defcong set-equiv set-equiv (hons-union x y) 1)
other
(defcong set-equiv set-equiv (hons-union x y) 2)
other
(defcong set-equiv set-equiv (hons-intersection x y) 1)
other
(defcong set-equiv set-equiv (hons-intersection x y) 2)
other
(defcong set-equiv set-equiv (hons-set-diff x y) 1)
other
(defcong set-equiv set-equiv (hons-set-diff x y) 2)
hons-subset1-member-invtheorem
(defthmd hons-subset1-member-inv
  (implies (and (hons-subset1 l al) (not (hons-assoc-equal x al)))
    (not (member-equal x l))))
hons-subset2-membertheorem
(defthmd hons-subset2-member
  (implies (and (hons-subset2 l l2) (member-equal x l))
    (member-equal x l2)))
hons-subset-membertheorem
(defthmd hons-subset-member
  (implies (and (hons-subset l l2) (member-equal x l))
    (member-equal x l2))
  :hints (("goal" :in-theory (enable hons-subset1-member-inv hons-subset2-member))))
in-theory
(in-theory (disable hons-subset))
hons-subset-implies-subsettheorem
(defthmd hons-subset-implies-subset
  (implies (hons-subset x y) (subsetp-equal x y))
  :hints (("goal" :expand (subsetp-equal x y)
     :in-theory (enable hons-subset-member))))
subset-implies-hons-subset1theorem
(defthm subset-implies-hons-subset1
  (implies (subsetp-equal x y)
    (hons-subset1 x (hons-put-list y a z)))
  :hints (("Goal" :induct (len x))))
subset-implies-hons-subset2theorem
(defthm subset-implies-hons-subset2
  (implies (subsetp-equal x y) (hons-subset2 x y))
  :hints (("Goal" :induct (len x))))
hons-subset-is-subsettheorem
(defthm hons-subset-is-subset
  (equal (hons-subset x y) (subsetp-equal x y))
  :hints (("goal" :expand (hons-subset x y)
     :cases ((hons-subset x y))
     :use hons-subset-implies-subset)))
local
(local (defthm equal-of-booleans-rewrite
    (implies (and (booleanp x) (booleanp y))
      (equal (equal x y) (iff x y)))
    :rule-classes ((:rewrite :backchain-limit-lst 1))))
other
(defcong set-equiv equal (hons-subset x y) 1)
other
(defcong set-equiv equal (hons-subset x y) 2)
list-intersects-falfunction
(defun list-intersects-fal
  (x fal)
  (and (consp x)
    (or (hons-get (car x) fal)
      (list-intersects-fal (cdr x) fal))))
list-does-not-intersect-fal-atomtheorem
(defthm list-does-not-intersect-fal-atom
  (implies (atom fal) (not (list-intersects-fal x fal))))
list-intersects-fal-cons-faltheorem
(defthm list-intersects-fal-cons-fal
  (iff (list-intersects-fal x (cons (cons k v) fal))
    (or (member-equal k x) (list-intersects-fal x fal)))
  :hints (("Goal" :in-theory (enable hons-assoc-equal))))
hons-dups-p1-iff-no-dups-and-not-in-tabtheorem
(defthm hons-dups-p1-iff-no-dups-and-not-in-tab
  (iff (hons-dups-p1 l tab)
    (or (list-intersects-fal l tab)
      (not (no-duplicatesp-equal l))))
  :hints (("Goal" :in-theory (enable hons-dups-p1)
     :induct (hons-dups-p1 l tab))))
hons-dupsp-to-no-duplicatesp-equaltheorem
(defthm hons-dupsp-to-no-duplicatesp-equal
  (iff (hons-dups-p x) (not (no-duplicatesp-equal x))))
in-theory
(in-theory (disable hons-dups-p))
hons-intersect-p1-iff-intersecttheorem
(defthm hons-intersect-p1-iff-intersect
  (iff (hons-intersect-p1 l tab) (list-intersects-fal l tab)))
hons-intersect-p2-is-intersectp-equaltheorem
(defthm hons-intersect-p2-is-intersectp-equal
  (iff (hons-intersect-p2 x y) (intersectp-equal x y)))
list-intersects-fal-intersectp-equaltheorem
(defthm list-intersects-fal-intersectp-equal
  (iff (list-intersects-fal x (hons-put-list y z acc))
    (or (intersectp-equal x y) (list-intersects-fal x acc)))
  :hints (("goal" :induct (len x))))
hons-intersect-p-is-intersectp-equaltheorem
(defthm hons-intersect-p-is-intersectp-equal
  (iff (hons-intersect-p x y) (intersectp-equal x y)))
in-theory
(in-theory (disable hons-intersect-p))
hons-set-diff-removalencapsulate
(encapsulate nil
  (local (include-book "alist-defs"))
  (local (defthm l0
      (iff (hons-assoc-equal key alist)
        (member-equal key (alist-keys alist)))
      :hints (("Goal" :in-theory (enable alist-keys)))))
  (local (defthm l1
      (iff (member-equal a (alist-keys (hons-put-list x y z)))
        (member-equal a (append x (alist-keys z))))
      :hints (("Goal" :in-theory (enable hons-put-list alist-keys)))))
  (local (defthm l2
      (set-equiv (alist-keys (hons-put-list x y z))
        (append x (alist-keys z)))
      :hints ((witness))))
  (local (defthm l3
      (equal (hons-sd1 x (hons-put-list y t acc))
        (set-difference-equal x (append y (alist-keys acc))))
      :hints (("Goal" :induct (len x)
         :in-theory (enable hons-sd1 set-difference-equal)))))
  (local (defthm l4
      (equal (hons-set-diff2 x y) (set-difference-equal x y))
      :hints (("Goal" :in-theory (enable hons-set-diff2 set-difference-equal)))))
  (defthm hons-set-diff-removal
    (equal (hons-set-diff x y) (set-difference-equal x y))
    :hints (("Goal" :in-theory (enable hons-set-diff)))))