/usr/share/acl2-6.3/books/make-event/gen-defthm.lisp is in acl2-books-source 6.3-5.
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 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 | ; Copyright (C) 2013, Regents of the University of Texas
; Written by Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; This file shows how the expansion phase can modify state to generate events.
; The macro defthm! below is similar to the macro defthm? from the distributed
; book misc/expander. But defthm? modifies state in a way that cannot be done
; in a certifiable book, because it relies on other than embedded event forms.
; Defthm!, on the other hand, calls defthm? during expansion to generate an
; event as the expansion result, which is then evaluated. This is a bit
; inefficient since the same theorems are in essence proved twice, but it is
; sound: we revert the world and most of the state after expansion, record the
; expansion, and then treat the defthm! call as though it were the expansion --
; which is a legal embedded event form.
(in-package "ACL2")
(include-book "misc/expander" :dir :system)
(defmacro defthm! (&whole ev
&rest args)
`(make-event (defthm? ,@args)
:on-behalf-of ,ev))
(defthm! app-simplify
(implies (true-listp x)
(equal (append x y)
?))
:hints (("Goal" :expand ((true-listp x)
(true-listp (cdr x))
(append x y))))
; show some output
:print-flg t)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The rest of this file just checks that the defthm! above generated the ;
; expected events. ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(set-enforce-redundancy t)
(DEFTHM
APP-SIMPLIFY$0
(IMPLIES (AND (CONSP X) (NOT (CDR X)))
(EQUAL (APPEND X Y) (CONS (CAR X) Y)))
#|
:HINTS
(("Goal"
:EXPAND ((TRUE-LISTP X)
(TRUE-LISTP (CDR X))
(APPEND X Y))
:IN-THEORY
(UNION-THEORIES
(DEFINITION-RUNES
(UNION-EQ '(IFF)
*EXPANDABLE-BOOT-STRAP-NON-REC-FNS*)
T WORLD)
'((:DEFINITION TRUE-LISTP)
(:DEFINITION BINARY-APPEND)
(:EXECUTABLE-COUNTERPART CONSP)))))
|# ; |
)
(DEFTHM
APP-SIMPLIFY$1
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(TRUE-LISTP (CDDR X)))
(EQUAL (APPEND X Y)
(CONS (CAR X) (APPEND (CDR X) Y))))
#|
:HINTS
(("Goal"
:EXPAND ((TRUE-LISTP X)
(TRUE-LISTP (CDR X))
(APPEND X Y))
:IN-THEORY
(UNION-THEORIES
(DEFINITION-RUNES
(UNION-EQ '(IFF)
*EXPANDABLE-BOOT-STRAP-NON-REC-FNS*)
T WORLD)
'((:DEFINITION TRUE-LISTP)
(:EXECUTABLE-COUNTERPART CONSP)
(:DEFINITION BINARY-APPEND)))))
|# ; |
)
(DEFTHM
APP-SIMPLIFY$2
(IMPLIES (NOT X) (EQUAL (APPEND X Y) Y))
#|
:HINTS
(("Goal"
:EXPAND ((TRUE-LISTP X)
(TRUE-LISTP (CDR X))
(APPEND X Y))
:IN-THEORY
(UNION-THEORIES
(DEFINITION-RUNES
(UNION-EQ '(IFF)
*EXPANDABLE-BOOT-STRAP-NON-REC-FNS*)
T WORLD)
'((:DEFINITION TRUE-LISTP)
(:EXECUTABLE-COUNTERPART CONSP)
(:DEFINITION BINARY-APPEND)))))
|# ; |
)
|