rewrite-with-equality

other

(in-package "ACL2")

other

(table rewrite-with-equality :preferences nil)

preferred-terms-for-rewrite-with-equalpfunction

(defun preferred-terms-for-rewrite-with-equalp
  (preferences fn gn)
  (cond ((endp preferences) nil)
    ((and (member-eq fn (car (car preferences)))
       (member-eq gn (cadr (car preferences)))) t)
    (t (preferred-terms-for-rewrite-with-equalp (cdr preferences)
        fn
        gn))))

triggering-lit-for-rewrite-with-equalpfunction

(defun triggering-lit-for-rewrite-with-equalp
  (preferences lit)
  (case-match lit
    (('not ('equal (fn . &) (gn . &))) (cond ((preferred-terms-for-rewrite-with-equalp preferences fn gn) (mv lit (fargn (fargn lit 1) 1) (fargn (fargn lit 1) 2)))
        ((preferred-terms-for-rewrite-with-equalp preferences gn fn) (mv lit (fargn (fargn lit 1) 2) (fargn (fargn lit 1) 1)))
        (t (mv nil nil nil))))
    (& (mv nil nil nil))))

find-triggering-lit-for-rewrite-with-equalpfunction

(defun find-triggering-lit-for-rewrite-with-equalp
  (preferences cl)
  (cond ((endp cl) (mv nil nil nil))
    (t (mv-let (lit lhs rhs)
        (triggering-lit-for-rewrite-with-equalp preferences
          (car cl))
        (cond (lit (mv lit lhs rhs))
          (t (find-triggering-lit-for-rewrite-with-equalp preferences
              (cdr cl))))))))

my-subst-expr1function

(defun my-subst-expr1
  (flg new old x)
  (declare (xargs :measure (acl2-count x)))
  (if flg
    (cond ((equal x old) new)
      ((variablep x) x)
      ((fquotep x) x)
      (t (cons (ffn-symb x) (my-subst-expr1 nil new old (fargs x)))))
    (cond ((endp x) nil)
      (t (cons (my-subst-expr1 t new old (car x))
          (my-subst-expr1 nil new old (cdr x)))))))

rewrite-clause-with-equalfunction

(defun rewrite-clause-with-equal
  (cl preferences)
  (mv-let (lit bad good)
    (find-triggering-lit-for-rewrite-with-equalp preferences cl)
    (cond (lit (prog2$ (cw "~%~%HIT!  Replaced ~x0 by ~x1.~%~%" bad good)
          (list (my-subst-expr1 nil good bad cl))))
      (t (list cl)))))

other

(defevaluator eqev
  eqev-lst
  ((not x) (equal x y)
    (if x
      y
      z)))

my-subst-expr1-correcttheorem

(defthm my-subst-expr1-correct
  (and (implies (and (pseudo-termp term)
        flg
        (equal (eqev new alist) (eqev old alist)))
      (equal (eqev (my-subst-expr1 flg new old term) alist)
        (eqev term alist)))
    (implies (and (pseudo-term-listp term)
        (not flg)
        (equal (eqev new alist) (eqev old alist)))
      (equal (eqev-lst (my-subst-expr1 flg new old term) alist)
        (eqev-lst term alist))))
  :hints (("Goal" :induct (my-subst-expr1 flg new old term)
     :in-theory (enable eqev-constraint-0))))

correctness-of-rewrite-clause-with-equal-gentheorem

(defthm correctness-of-rewrite-clause-with-equal-gen
  (implies (and (pseudo-term-listp cl)
      (alistp a)
      (equal (eqev good a) (eqev bad a))
      (eqev (disjoin (my-subst-expr1 nil good bad cl)) a))
    (eqev (disjoin cl) a))
  :rule-classes nil)

find-triggering-lit-for-rewrite-with-equalp-finds-membertheorem

(defthm find-triggering-lit-for-rewrite-with-equalp-finds-member
  (implies (and (pseudo-term-listp cl)
      (car (find-triggering-lit-for-rewrite-with-equalp hints cl)))
    (member-equal (car (find-triggering-lit-for-rewrite-with-equalp hints cl))
      cl)))

member-of-false-clause-is-falsetheorem

(defthm member-of-false-clause-is-false
  (implies (and (pseudo-term-listp cl)
      (not (eqev (disjoin cl) a))
      (member-equal lit cl))
    (not (eqev lit a)))
  :rule-classes nil)

terms-found-by-find-triggering-lit-for-rewrite-with-equalp-are-equaltheorem

(defthm terms-found-by-find-triggering-lit-for-rewrite-with-equalp-are-equal
  (implies (and (pseudo-term-listp cl)
      (car (find-triggering-lit-for-rewrite-with-equalp hints cl))
      (not (eqev (disjoin cl) a)))
    (equal (eqev (mv-nth 1
          (find-triggering-lit-for-rewrite-with-equalp hints cl))
        a)
      (eqev (mv-nth 2
          (find-triggering-lit-for-rewrite-with-equalp hints cl))
        a)))
  :hints (("Goal" :use (:instance member-of-false-clause-is-false
       (cl cl)
       (a a)
       (lit (car (find-triggering-lit-for-rewrite-with-equalp hints cl))))))
  :rule-classes nil)

correctness-of-rewrite-clause-with-equaltheorem

(defthm correctness-of-rewrite-clause-with-equal
  (implies (and (pseudo-term-listp cl)
      (alistp a)
      (eqev (conjoin-clauses (rewrite-clause-with-equal cl hints))
        a))
    (eqev (disjoin cl) a))
  :hints (("Goal" :do-not-induct t
     :use ((:instance terms-found-by-find-triggering-lit-for-rewrite-with-equalp-are-equal) (:instance correctness-of-rewrite-clause-with-equal-gen
         (cl cl)
         (a a)
         (good (mv-nth 2
             (find-triggering-lit-for-rewrite-with-equalp hints cl)))
         (bad (mv-nth 1
             (find-triggering-lit-for-rewrite-with-equalp hints cl)))))))
  :rule-classes :clause-processor)

rewrite-with-equality-when-stablefunction

(defun rewrite-with-equality-when-stable
  (id clause world stable-under-simplificationp)
  (declare (ignore id))
  (cond ((and stable-under-simplificationp
       (mv-let (lit bad good)
         (find-triggering-lit-for-rewrite-with-equalp (cdr (assoc-eq :preferences (table-alist 'rewrite-with-equality world)))
           clause)
         (declare (ignore bad good))
         lit)) `(:computed-hint-replacement t
        :clause-processor (rewrite-clause-with-equal clause
          ',(CDR (ASSOC-EQ :PREFERENCES (TABLE-ALIST 'REWRITE-WITH-EQUALITY WORLD))))))
    (t nil)))