deflist-aux

(in-package "STD")

(include-book "std/osets/top" :dir :system)

(encapsulate (((predicate *) => *))
  (local (defun predicate (x) x)))

(defund all
  (x)
  (declare (xargs :guard t))
  (if (consp x)
    (and (predicate (car x)) (all (cdr x)))
    t))

(encapsulate (((all-hyps) => *) ((all-list) => *))
  (local (defun all-hyps nil nil))
  (local (defun all-list nil nil))
  (defthmd all-by-membership-constraint
    (implies (all-hyps)
      (implies (member-equal arbitrary-element (all-list))
        (predicate arbitrary-element)))))

(encapsulate nil
  (local (defun all-badguy
      (x)
      (if (consp x)
        (if (predicate (car x))
          (all-badguy (cdr x))
          (list (car x)))
        nil)))
  (local (defthmd all-badguy-membership-property
      (implies (all-badguy x)
        (and (member-equal (car (all-badguy x)) x)
          (not (predicate (car (all-badguy x))))))
      :hints (("Goal" :induct (all-badguy x)))))
  (local (defthm all-badguy-under-iff
      (iff (all-badguy x) (not (all x)))
      :hints (("Goal" :in-theory (enable all)))))
  (defthmd all-by-membership
    (implies (all-hyps) (all (all-list)))
    :hints (("Goal" :in-theory (enable all-by-membership-constraint)
       :use ((:instance all-badguy-membership-property
          (x (all-list))))))))

(defund subsetp-equal-trigger
  (x y)
  (declare (xargs :guard (and (true-listp x) (true-listp y))))
  (subsetp-equal x y))

(defthm pick-a-point-subsetp-equal-strategy
  (implies (and (syntaxp (rewriting-goal-lit mfc state))
      (syntaxp (rewriting-conc-lit `(subsetp-equal ,STD::X ,STD::Y)
          mfc
          state)))
    (equal (subsetp-equal x y)
      (subsetp-equal-trigger x y)))
  :hints (("Goal" :in-theory (enable subsetp-equal-trigger))))

(automate-instantiation :new-hint-name pick-a-point-subsetp-equal-hint
  :generic-theorem all-by-membership
  :generic-predicate predicate
  :generic-hyps all-hyps
  :generic-collection all-list
  :generic-collection-predicate all
  :actual-collection-predicate subsetp-equal
  :actual-trigger subsetp-equal-trigger
  :predicate-rewrite (((predicate ?x ?y) (member-equal ?x ?y)))
  :tagging-theorem pick-a-point-subsetp-equal-strategy)