/usr/share/acl2-4.3/books/make-event/gen-defthm-check.lisp is in acl2-books-source 4.3-3.
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 | ; Same as gen-defthm.lisp, except for :check-expansion t.
(in-package "ACL2")
(include-book "misc/expander" :dir :system)
(defmacro defthm! (&whole ev
&rest args)
`(make-event (defthm? ,@args)
:on-behalf-of ,ev
:check-expansion t))
(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)))))
|# ; |
)
|