/usr/share/acl2-8.0dfsg/books/misc/eliminate-irrelevance-tests.lisp is in acl2-books-source 8.0dfsg-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 | ; Copyright (C) 2016, ForrestHunt, Inc.
; Matt Kaufmann, October, 2016
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
(in-package "ACL2")
; First example
(encapsulate
((p1 () t)
(my-app1 (x y) t))
(local (defun p1 () 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))))))
(defun rev1 (x)
(if (consp x)
(my-app1 (rev1 (cdr x))
(cons (car x) nil))
nil))
(defthm test1
(implies (and (p1)
(true-listp x))
(equal (rev1 (rev1 x)) x)))
; Second example
(encapsulate
((p2 () t)
(my-app2 (x y) t))
(local (defun p2 () 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))))))
(defun rev2 (x)
(if (consp x)
(my-app2 (rev2 (cdr x))
(cons (car x) nil))
nil))
(defthm test2
(implies (and (not (p2))
(true-listp x))
(equal (rev2 (rev2 x)) x)))
|