Filtering...

equal-sets

books/centaur/misc/equal-sets

Included Books

top sets witness-cp
other
(in-package "ACL2")
include-book
(include-book "std/osets/top" :dir :system)
include-book
(include-book "std/lists/sets" :dir :system)
include-book
(include-book "witness-cp")
other
(defquantexpr subsetp
  :predicate (subsetp-equal x y)
  :quantifier :forall :witnesses ((k (subsetp-witness x y)))
  :expr (implies (member k x) (member k y))
  :witness-hints ('(:in-theory '(subsetp-witness-correct)))
  :instance-hints ('(:in-theory '(subsetp-member)))
  :in-package-of foo)
other
(defquantexpr intersectp
  :predicate (intersectp-equal x y)
  :quantifier :exists :witnesses ((k (intersectp-witness x y)))
  :expr (and (member k x) (member k y))
  :witness-hints ('(:in-theory '(intersectp-witness-correct)))
  :instance-hints ('(:in-theory '(intersectp-member)))
  :in-package-of foo)
other
(defquantexpr set-equiv
  :predicate (set-equiv x y)
  :quantifier :forall :witnesses ((k (set-unequal-witness x y)))
  :expr (iff (member k x) (member k y))
  :witness-hints ('(:in-theory '(set-unequal-witness-correct)))
  :instance-hints ('(:in-theory '(set-equiv-implies-iff-member-2))))
other
(defquantexpr set-consp
  :predicate (consp x)
  :quantifier :exists :witnesses ((k (car x)))
  :expr (member k x)
  :generalize nil
  :witness-hints ('(:in-theory nil
     :expand ((:with member-equal (:free (k) (member-equal k x))))))
  :instance-hints ('(:in-theory nil
     :expand ((:with member-equal (:free (k) (member-equal k x)))))))
other
(defexample set-reasoning-member-template
  :pattern (member-equal k y)
  :templates (k)
  :instance-rules (subsetp-instancing intersectp-instancing
    set-equiv-instancing
    set-consp-instancing))
other
(defexample set-reasoning-no-consp-member-template
  :pattern (member-equal k y)
  :templates (k)
  :instance-rules (subsetp-instancing intersectp-instancing
    set-equiv-instancing))
other
(def-witness-ruleset set-reasoning-rules
  '(subsetp-witnessing intersectp-witnessing
    set-equiv-witnessing
    set-consp-witnessing
    subsetp-instancing
    set-equiv-instancing
    intersectp-instancing
    set-consp-instancing
    set-reasoning-member-template))
other
(def-witness-ruleset set-reasoning-no-consp
  '(subsetp-witnessing intersectp-witnessing
    set-equiv-witnessing
    subsetp-instancing
    set-equiv-instancing
    intersectp-instancing
    intersectp-member-template
    subsetp-member-template
    set-equiv-member-template
    set-reasoning-no-consp-member-template))
other
(def-witness-ruleset set-reasoning-no-consp-manual-examples
  '(subsetp-witnessing intersectp-witnessing
    set-equiv-witnessing
    subsetp-instancing
    set-equiv-instancing
    intersectp-instancing
    intersectp-member-template
    subsetp-member-template
    set-equiv-member-template))
other
(def-witness-ruleset set-reasoning-manual-examples
  '(subsetp-witnessing intersectp-witnessing
    set-equiv-witnessing
    set-consp-witnessing
    subsetp-instancing
    set-equiv-instancing
    intersectp-instancing
    set-consp-instancing))
set-reasoningmacro
(defmacro set-reasoning
  nil
  '(witness :ruleset set-reasoning-rules))
intersectp-of-supersettheorem
(defthmd intersectp-of-superset
  (implies (and (intersectp a b) (subsetp a c))
    (intersectp c b))
  :hints ((set-reasoning))
  :rule-classes ((:rewrite :match-free :all)))
intersectp-of-superset2theorem
(defthmd intersectp-of-superset2
  (implies (and (subsetp a c) (intersectp b a))
    (intersectp b c))
  :hints ((set-reasoning))
  :rule-classes ((:rewrite :match-free :all)))
in-theory
(in-theory (disable set-difference-equal intersection-equal))