eliminate-irrelevance-tests

other

(in-package "ACL2")

my-app1-defencapsulate

(encapsulate ((p1 nil t) (my-app1 (x y) t))
  (local (defun p1 nil t))
  (local (defun my-app1 (x y) (append x y)))
  (defthm my-app1-def
    (implies (p1)
      (equal (my-app1 x y)
        (if (consp x)
          (cons (car x) (my-app1 (cdr x) y))
          y)))
    :rule-classes ((:definition :controller-alist ((my-app1 t nil))))))

rev1function

(defun rev1
  (x)
  (if (consp x)
    (my-app1 (rev1 (cdr x)) (cons (car x) nil))
    nil))

test1theorem

(defthm test1
  (implies (and (p1) (true-listp x))
    (equal (rev1 (rev1 x)) x)))

my-app2-defencapsulate

(encapsulate ((p2 nil t) (my-app2 (x y) t))
  (local (defun p2 nil nil))
  (local (defun my-app2 (x y) (append x y)))
  (defthm my-app2-def
    (implies (not (p2))
      (equal (my-app2 x y)
        (if (consp x)
          (cons (car x) (my-app2 (cdr x) y))
          y)))
    :rule-classes ((:definition :controller-alist ((my-app2 t nil))))))

rev2function

(defun rev2
  (x)
  (if (consp x)
    (my-app2 (rev2 (cdr x)) (cons (car x) nil))
    nil))

test2theorem

(defthm test2
  (implies (and (not (p2)) (true-listp x))
    (equal (rev2 (rev2 x)) x)))