/usr/share/acl2-7.1/books/xdoc/book-thms-example.lisp is in acl2-books-source 7.1-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 | ; Copyright (C) 2014, Regents of the University of Texas
; Original author: Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
(in-package "ACL2")
; See book-thms.lisp. This is an example that tests the utilities contained in
; that book.
(include-book "book-thms")
; Example:
(logic)
(local (encapsulate-then-new-info
my-name
(defthm foo
(equal (car (cons x y)) x))
(defun f1 (x y) (<= x y))
(defthm bar
(< (acl2-count x) (acl2-count (cons x y))))
(defun-sk exists-x-f1 (y)
(exists x (f1 x y)))
(encapsulate ((f (x) t)
(h (x) t))
(local (defun f (x) x))
(defun g (x) (f x))
(local (defun h (x) x))
(defthm my-thm
(equal (f x) (h (g x)))))
(defchoose my-ch (x) (y)
(f1 x (cons 0 y)))
))
(local
(assert-event
(equal (my-name)
'((FOO :THEOREM (EQUAL (CAR (CONS X Y)) X))
(F1 :DEF (EQUAL (F1 X Y) (<= X Y)))
(BAR :THEOREM (< (ACL2-COUNT X)
(ACL2-COUNT (CONS X Y))))
(EXISTS-X-F1-SUFF :THEOREM (IMPLIES (F1 X Y) (EXISTS-X-F1 Y)))
((EXISTS-X-F1 EXISTS-X-F1-WITNESS)
:CONSTRAINT
(AND (EQUAL (EXISTS-X-F1 Y)
(LET ((X (EXISTS-X-F1-WITNESS Y)))
(F1 X Y)))
(IMPLIES (F1 X Y) (EXISTS-X-F1 Y))))
(MY-THM :THEOREM (EQUAL (F X) (H (G X))))
((G F H)
:CONSTRAINT
(AND (EQUAL (G X) (F X))
(EQUAL (F X) (H (G X)))))
(MY-CH :DEFCHOOSE (IMPLIES (F1 X (CONS 0 Y))
(LET ((X (MY-CH Y)))
(F1 X (CONS 0 Y)))))))))
|