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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
; (include-book "m1")
; (certify-book "defsys-utilities" 1)
(in-package "M1")
(defthm about-make-state
(and (true-listp (make-state pc locs stk prog))
(equal (len (make-state pc locs stk prog)) 4))
:hints (("Goal" :in-theory (enable make-state))))
(defun name-locals (names locals i)
(cond ((endp names) t)
((equal (car names) (nth i locals))
(name-locals (cdr names) locals (+ i 1)))
(t nil)))
(defthm name-locals-opener
(and (equal (name-locals nil locals i) t)
(equal (name-locals (cons name names) locals i)
(and (equal name (nth i locals))
(name-locals names locals (+ 1 i))))))
(defun name-locals-locals-gen-hint (names junk)
(if (endp names)
junk
(name-locals-locals-gen-hint (cdr names)
(append junk (list (car names))))))
(defthm append-assoc
(equal (append (append a b) c) (append a (append b c))))
(defthm len-append
(equal (len (append a b)) (+ (len a) (len b))))
(defthm nth-len-append
(equal (nth (len a) (append a b))
(car b)))
(defthm name-locals-locals-gen
(equal (name-locals names (append junk names) (len junk))
t)
:hints (("Goal" :induct (name-locals-locals-gen-hint names junk)))
:rule-classes nil)
(defthm name-locals-locals
(equal (name-locals names names 0) t)
:hints (("Goal" :use (:instance name-locals-locals-gen
(junk nil)))))
(defun update-nth* (i lst locals)
(cond ((endp lst) locals)
(t (update-nth i (car lst)
(update-nth* (+ i 1) (cdr lst) locals)))))
(defthm update-nth*-opener
(and (equal (update-nth* i nil locals) locals)
(equal (update-nth* i (cons x lst) locals)
(update-nth i x (update-nth* (+ i 1) lst locals)))))
(defthm len-update-nth-nil
(implies (natp i)
(equal (len (update-nth i v nil))
(+ 1 i))))
(defthm len-m1-update-nth
(equal (len (update-nth n val x))
(max (1+ (nfix n)) (len x))))
(defthm len-update-nth-inequality
(<= (len x) (len (update-nth i v x)))
:rule-classes :linear)
; The :rewrite rule above (len-update-nth) causes case splits that prevent us
; from establishing some of the READY-AT hypotheses. It seems to be sufficient
; to know just the weaker :linear result. So we disable the rewrite rule.
(in-theory (disable len-m1-update-nth))
(defthm update-nth-noop
(implies (and (natp i)
(< i (len x)))
(equal (update-nth i (nth i x) x) x)))
(defun number-of-explicit-elements (x)
(cond ((atom x) 0)
((quotep x)
(cond ((true-listp (car (cdr x)))
(len (car (cdr x))))
((consp (car (cdr x)))
(+ 1 (number-of-explicit-elements
(kwote (cdr (car (cdr x)))))))
(t 0)))
((eq (acl2::ffn-symb x) 'cons)
(+ 1 (number-of-explicit-elements (acl2::fargn x 2))))
(t 0)))
(defthm nth-cons
(and (equal (nth 0 (cons e x)) e)
(implies (and (natp n)
(syntaxp
(and (quotep n)
(natp (car (cdr n)))
(<= (car (cdr n))
(number-of-explicit-elements x)))))
(equal (nth (+ 1 n) (cons e x))
(nth n x)))))
(defthm true-listp-m1-update-nth-nil
(true-listp (update-nth i v nil)))
(defthm true-listp-m1-update-nth
(implies (true-listp x)
(true-listp (update-nth i v x))))
(in-theory (disable nth nth-add1! update-nth))
(defthm len-push
(equal (len (push x stack)) (+ 1 (len stack)))
:hints (("Goal" :in-theory (enable push))))
(defthm true-listp-locals-step
(implies (true-listp (locals s))
(true-listp (locals (step s))))
:hints (("Goal" :in-theory (enable step))))
(defthm true-listp-locals-m1
(implies (true-listp (locals s))
(true-listp (locals (m1 s n))))
:hints (("Goal" :in-theory (enable m1))))
(defthm len-locals-step
(<= (len (locals s))
(len (locals (step s))))
:hints (("Goal" :in-theory (enable step)))
:rule-classes :linear)
(defthm len-locals-m1
(<= (len (locals s))
(len (locals (m1 s n))))
:hints (("Goal" :in-theory (enable m1)))
:rule-classes :linear)
(defthm s-is-make-state-s
(implies (and (true-listp s)
(equal (len s) 4)
(equal (pc s) pc)
(equal (program s) program))
(equal (equal s (make-state pc (locals s) (stack s) program))
t))
:hints (("Goal" :in-theory (enable make-state))))
|
