Filtering...

defattach-example

books/misc/defattach-example

Included Books

top
other
(in-package "ACL2")
abst-commencapsulate
(encapsulate ((abst (x y) t))
  (local (defun abst (x y) (+ x y)))
  (defthm abst-comm (equal (abst x y) (abst y x)))
  (defthm abst-assoc
    (equal (abst (abst x y) z) (abst x (abst y z)))))
fold-abstfunction
(defun fold-abst
  (x root)
  (if (consp x)
    (abst (car x) (fold-abst (cdr x) root))
    root))
fold-abst-reverseencapsulate
(encapsulate nil
  (local (defthm abst-comm2
      (equal (abst x (abst y z)) (abst y (abst x z)))
      :hints (("Goal" :use ((:instance abst-assoc (x x) (y y)) (:instance abst-assoc (x y) (y x)))
         :in-theory (disable abst-assoc)))))
  (local (defthm fold-abst-abst
      (equal (fold-abst x (abst a b)) (abst a (fold-abst x b)))))
  (local (defthm fold-abst-revappend
      (equal (fold-abst (revappend x y) root)
        (fold-abst x (fold-abst y root)))))
  (defthm fold-abst-reverse
    (equal (fold-abst (reverse x) root) (fold-abst x root))))
multfunction
(defun mult (x y) (* (fix x) (fix y)))
fold-multfunction
(defun fold-mult
  (x root)
  (if (consp x)
    (mult (car x) (fold-mult (cdr x) root))
    root))
local
(local (include-book "arithmetic/top" :dir :system))
fold-mult-reversetheorem
(defthm fold-mult-reverse
  (equal (fold-mult (reverse x) root) (fold-mult x root))
  :hints (("Goal" :by (:functional-instance fold-abst-reverse
       (abst mult)
       (fold-abst fold-mult)))))
other
(verify-guards mult)
other
(defattach abst mult)
other
(assert-event (equal (fold-abst '(3 4 5) 100) 6000))
addfunction
(defun add (x y) (+ (fix x) (fix y)))
other
(verify-guards add)
other
(defattach abst add)
other
(assert-event (equal (fold-abst '(3 4 5) 100) 112))