(encapsulate
 ((ac (x y) t))
 (local (defun ac (x y)
          (+ x y)))
 (defthm ac-comm
   (equal (ac x y)
          (ac y x)))
 (defthm ac-assoc
   (equal (ac (ac x y) z)
          (ac x (ac y z)))))

(defun fold-ac (lst root)
  (if (endp lst)
      root
    (ac (car lst)
        (fold-ac (cdr lst) root))))

(fold-ac '(2 3 4) 1) ; error

(defun times (x y)
  (* (fix x) (fix y)))

(defattach ac times) ; fails

(verify-guards times)

(defattach ac times) ; fails

(include-book "arithmetic/top" :dir :system)

(defattach ac times) ; succeeds

(fold-ac '(2 3 4) 1)

(fold-ac '(4 3 2) 1)

; So now we might think of proving that reverse preserves fold-ac.
; (That's a nice little proof, which I can show you offline.)

(trace$ ac times)
(fold-ac '(2 3 4) 1)
(untrace$)

(equal (fold-ac '(2 3 4) 1)
       24) ; returns T

(thm (equal (fold-ac '(2 3 4) 1)
            24)) ; Fails (holds for evaluation theory, not current theory)

(quote (return-to-slides))

; Acyclicity condition demo.

(encapsulate
 ((f (x) t))
 (local (defun f (x) x)))

(defun g (x)
  (declare (xargs :guard t))
  (not (f x)))

(defattach f g) ; fails, reporting a cycle

(quote (return-to-slides))

; See kaufmann-demo-book.lisp in this directory for a proof that reverse
; preserves fold-ac and fold-times.