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
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
|
(in-package "BCV")
(include-book "typechecker")
(include-book "typechecker-ext")
(include-book "typechecker-simple")
(include-book "bcv-base")
;;(i-am-here) ;; Sat Dec 31 02:24:36 2005
(defthm is-suffix-facts
(implies (IS-SUFFIX (LIST* MERGEDCODE1 any) mergedcode)
(is-suffix any mergedcode))
:rule-classes :forward-chaining)
(defthm is-suffix-facts-member
(implies (IS-SUFFIX (LIST* MERGEDCODE1 any) mergedcode)
(member mergedcode1 mergedcode))
:rule-classes :forward-chaining)
;; (defthm is-suffix-implies-next-inst
;; (implies (IS-SUFFIX (LIST* frame inst rest) mergedcode)
;; (equal (next-inst frame mergedcode)
;; inst))
;; :hints (("Goal" :do-not '(generalize)
;; :expand (IS-SUFFIX (LIST* frame inst rest) mergedcode))))
;; ;; this is not true!!!
;----------------------------------------------------------------------
(local
(defthm next-inst-append
(implies (not (member inst prefix))
(equal (next-inst inst (append prefix suffix))
(next-inst inst suffix)))))
;;;
;;; list with duplicates!!
;;;
;----------------------------------------------------------------------
;; (i-am-here) ;; Sun Jan 1 19:21:02 2006
(defthm pc-wff-mergedcode1-equal-pc
(implies (and (pc-wff-mergedcode1 pc mergedcode)
(consp mergedcode)
(not (isEnd (car mergedcode))))
(equal (instrOffset (car (extract-code mergedcode))) pc))
:hints (("Goal" :do-not '(generalize fertilize)
:in-theory (disable instructionIsTypeSafe
instructionSatisfiesHandlers
instrOffset
sig-do-inst
allinstructions
isEnd
mapFrame
jvm::inst-size
getMap mapOffset
frameIsAssignable
isInstruction
isStackMap))))
(defthm is-suffix-pc-equal
(implies (and (IS-SUFFIX (LIST* MERGEDCODE1 mergedcode4) mergedcode)
(isStackMap mergedcode1)
(pc-wff-mergedcode1 pc mergedcode))
(equal (instrOffset (car (extract-code mergedcode4)))
(mapOffset (getMap mergedcode1))))
:hints (("Goal" :do-not '(generalize fertilize)
:in-theory (disable instructionIsTypeSafe
instructionSatisfiesHandlers
instrOffset
sig-do-inst
allinstructions
isEnd
mapFrame
jvm::inst-size
getMap mapOffset
frameIsAssignable
isInstruction
isStackMap))))
(defthm pc-wff-mergedcode1-implies-wff-merged-code-instr
(implies (pc-wff-mergedcode1 pc mergedcode)
(wff-mergedcode-instr mergedcode))
:hints (("Goal" :in-theory (disable isInstruction isStackMap
isEnd
jvm::inst-size)))
:rule-classes :forward-chaining)
(defthm is-suffix-extract-code-is-consp-lemma
(implies (and (wff-mergedcode-instr mergedcode)
(IS-SUFFIX (LIST* MERGEDCODE1 mergedcode4) mergedcode)
(isStackMap mergedcode1))
(consp (extract-code mergedcode4)))
:hints (("Goal" :do-not '(generalize fertilize)
:in-theory (disable instructionIsTypeSafe
instructionSatisfiesHandlers
instrOffset
sig-do-inst
allinstructions
isEnd
mapFrame
jvm::inst-size
getMap mapOffset
frameIsAssignable
isInstruction
isStackMap)))
:rule-classes :forward-chaining)
(defthm is-suffix-not-end
(implies (and (IS-SUFFIX (LIST* MERGEDCODE1 mergedcode4) mergedcode)
(wff-merged-code-weak mergedcode)
(isStackMap mergedcode1))
(not (isEnd (car mergedcode))))
:hints (("Goal" :in-theory (disable isInstruction isStackMap
isEnd
jvm::inst-size)))
:rule-classes :forward-chaining)
(defthm isInstruction-car-extract-code-x
(implies (consp (extract-code mergedcode))
(isInstruction (car (extract-code mergedcode))))
:hints (("Goal" :do-not '(generalize fertilize)
:in-theory (disable instructionIsTypeSafe
instructionSatisfiesHandlers
instrOffset
sig-do-inst
allinstructions
isEnd
mapFrame
jvm::inst-size
getMap mapOffset
frameIsAssignable
isInstruction
isStackMap)))
:rule-classes :forward-chaining)
(defthm is-suffix-extract-code-is-code
(implies (and (IS-SUFFIX (LIST* MERGEDCODE1 mergedcode4) mergedcode)
(isStackMap mergedcode1)
(pc-wff-mergedcode1 pc mergedcode))
(isInstruction (car (extract-code mergedcode4))))
:rule-classes :forward-chaining)
(defthm is-suffix-extract-code-is-consp
(implies (and (IS-SUFFIX (LIST* MERGEDCODE1 mergedcode4) mergedcode)
(isStackMap mergedcode1)
(pc-wff-mergedcode1 pc mergedcode))
(consp (extract-code mergedcode4)))
:rule-classes :forward-chaining)
;----------------------------------------------------------------------
|
