(in-package "ACL2")

;In real proofs I'd just use (not (consp x)) instead of defining this function.
;I define it here to let us experimenting with disabling it.
(defun non-consp (x)
  (not (consp x)))

(defun app (x y)
  (if (non-consp x) ;would normally use endp here
      y
    (cons (car x) (app (cdr x) y))))

(in-theory (disable app))

(defthm app-of-cons
  (equal (APP (CONS x y) Z)
         (cons x (APP y Z)))
  :hints (("Goal" :in-theory (enable app))))

(defthm app-of-non-consp
  (implies (not (consp x))
           (equal (app x y)
                  y))
  :hints (("Goal" :in-theory (enable app non-consp))))

(defthm app-associative
  (equal (app (app x y) z)
         (app x (app y z)))
  :hints (("Subgoal *1/2" :expand ((APP X Y) (APP X (APP Y Z))))
          ("Goal" 
           :in-theory (enable (:induction app)))))