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
|
; 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)))))
|# ; |
)
|
