remove-hyp

(in-package "ACL2")

(defun remove-first-hyp-cp
  (clause)
  (if (consp clause)
    (list (cdr clause))
    (list clause)))

(defevaluator remove-hyp-ev
  remove-hyp-ev-lst
  ((if a
     b
     c)))

(defthm remove-first-hyp-cp-correct
  (implies (and (pseudo-term-listp x)
      (alistp a)
      (remove-hyp-ev (conjoin-clauses (remove-first-hyp-cp x)) a))
    (remove-hyp-ev (disjoin x) a))
  :rule-classes :clause-processor)

(defun remove-hyp-cp
  (clause hyp)
  (list (remove-equal hyp clause)))

(defthm disjoin-of-remove-equal
  (implies (not (remove-hyp-ev (disjoin x) a))
    (not (remove-hyp-ev (disjoin (remove hyp x)) a)))
  :hints (("Goal" :in-theory (enable remove))))

(defthm remove-hyp-cp-correct
  (implies (and (pseudo-term-listp x)
      (alistp a)
      (remove-hyp-ev (conjoin-clauses (remove-hyp-cp x hyp)) a))
    (remove-hyp-ev (disjoin x) a))
  :rule-classes :clause-processor)