94 by (import bits LSBn_def) |
93 by (import bits LSBn_def) |
95 |
94 |
96 consts |
95 consts |
97 BITWISE :: "nat => (bool => bool => bool) => nat => nat => nat" |
96 BITWISE :: "nat => (bool => bool => bool) => nat => nat => nat" |
98 |
97 |
99 specification (BITWISE_primdef: BITWISE) BITWISE_def: "(ALL (oper::bool => bool => bool) (x::nat) y::nat. BITWISE 0 oper x y = 0) & |
98 specification (BITWISE_primdef: BITWISE) BITWISE_def: "(ALL oper x y. BITWISE 0 oper x y = 0) & |
100 (ALL (n::nat) (oper::bool => bool => bool) (x::nat) y::nat. |
99 (ALL n oper x y. |
101 BITWISE (Suc n) oper x y = |
100 BITWISE (Suc n) oper x y = |
102 BITWISE n oper x y + SBIT (oper (bit n x) (bit n y)) n)" |
101 BITWISE n oper x y + SBIT (oper (bit n x) (bit n y)) n)" |
103 by (import bits BITWISE_def) |
102 by (import bits BITWISE_def) |
104 |
103 |
105 lemma DIV1: "ALL x::nat. x div 1 = x" |
104 lemma SUC_SUB: "Suc a - a = 1" |
106 by (import bits DIV1) |
|
107 |
|
108 lemma SUC_SUB: "Suc (a::nat) - a = 1" |
|
109 by (import bits SUC_SUB) |
105 by (import bits SUC_SUB) |
110 |
106 |
111 lemma DIV_MULT_1: "ALL (r::nat) n::nat. r < n --> (n + r) div n = 1" |
107 lemma DIV_MULT_1: "(r::nat) < (n::nat) ==> (n + r) div n = (1::nat)" |
112 by (import bits DIV_MULT_1) |
108 by (import bits DIV_MULT_1) |
113 |
109 |
114 lemma ZERO_LT_TWOEXP: "(All::(nat => bool) => bool) |
110 lemma ZERO_LT_TWOEXP: "(0::nat) < (2::nat) ^ (n::nat)" |
115 (%n::nat. |
|
116 (op <::nat => nat => bool) (0::nat) |
|
117 ((op ^::nat => nat => nat) |
|
118 ((number_of \<Colon> int => nat) |
|
119 ((Int.Bit0 \<Colon> int => int) |
|
120 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))) |
|
121 n))" |
|
122 by (import bits ZERO_LT_TWOEXP) |
111 by (import bits ZERO_LT_TWOEXP) |
123 |
112 |
124 lemma MOD_2EXP_LT: "ALL (n::nat) k::nat. k mod 2 ^ n < 2 ^ n" |
113 lemma MOD_2EXP_LT: "(k::nat) mod (2::nat) ^ (n::nat) < (2::nat) ^ n" |
125 by (import bits MOD_2EXP_LT) |
114 by (import bits MOD_2EXP_LT) |
126 |
115 |
127 lemma TWOEXP_DIVISION: "ALL (n::nat) k::nat. k = k div 2 ^ n * 2 ^ n + k mod 2 ^ n" |
116 lemma TWOEXP_DIVISION: "(k::nat) = k div (2::nat) ^ (n::nat) * (2::nat) ^ n + k mod (2::nat) ^ n" |
128 by (import bits TWOEXP_DIVISION) |
117 by (import bits TWOEXP_DIVISION) |
129 |
118 |
130 lemma TWOEXP_MONO: "(All::(nat => bool) => bool) |
119 lemma TWOEXP_MONO: "(a::nat) < (b::nat) ==> (2::nat) ^ a < (2::nat) ^ b" |
131 (%a::nat. |
|
132 (All::(nat => bool) => bool) |
|
133 (%b::nat. |
|
134 (op -->::bool => bool => bool) ((op <::nat => nat => bool) a b) |
|
135 ((op <::nat => nat => bool) |
|
136 ((op ^::nat => nat => nat) |
|
137 ((number_of \<Colon> int => nat) |
|
138 ((Int.Bit0 \<Colon> int => int) |
|
139 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))) |
|
140 a) |
|
141 ((op ^::nat => nat => nat) |
|
142 ((number_of \<Colon> int => nat) |
|
143 ((Int.Bit0 \<Colon> int => int) |
|
144 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))) |
|
145 b))))" |
|
146 by (import bits TWOEXP_MONO) |
120 by (import bits TWOEXP_MONO) |
147 |
121 |
148 lemma TWOEXP_MONO2: "(All::(nat => bool) => bool) |
122 lemma TWOEXP_MONO2: "(a::nat) <= (b::nat) ==> (2::nat) ^ a <= (2::nat) ^ b" |
149 (%a::nat. |
|
150 (All::(nat => bool) => bool) |
|
151 (%b::nat. |
|
152 (op -->::bool => bool => bool) ((op <=::nat => nat => bool) a b) |
|
153 ((op <=::nat => nat => bool) |
|
154 ((op ^::nat => nat => nat) |
|
155 ((number_of \<Colon> int => nat) |
|
156 ((Int.Bit0 \<Colon> int => int) |
|
157 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))) |
|
158 a) |
|
159 ((op ^::nat => nat => nat) |
|
160 ((number_of \<Colon> int => nat) |
|
161 ((Int.Bit0 \<Colon> int => int) |
|
162 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))) |
|
163 b))))" |
|
164 by (import bits TWOEXP_MONO2) |
123 by (import bits TWOEXP_MONO2) |
165 |
124 |
166 lemma EXP_SUB_LESS_EQ: "(All::(nat => bool) => bool) |
125 lemma EXP_SUB_LESS_EQ: "(2::nat) ^ ((a::nat) - (b::nat)) <= (2::nat) ^ a" |
167 (%a::nat. |
|
168 (All::(nat => bool) => bool) |
|
169 (%b::nat. |
|
170 (op <=::nat => nat => bool) |
|
171 ((op ^::nat => nat => nat) |
|
172 ((number_of \<Colon> int => nat) |
|
173 ((Int.Bit0 \<Colon> int => int) |
|
174 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))) |
|
175 ((op -::nat => nat => nat) a b)) |
|
176 ((op ^::nat => nat => nat) |
|
177 ((number_of \<Colon> int => nat) |
|
178 ((Int.Bit0 \<Colon> int => int) |
|
179 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))) |
|
180 a)))" |
|
181 by (import bits EXP_SUB_LESS_EQ) |
126 by (import bits EXP_SUB_LESS_EQ) |
182 |
127 |
183 lemma BITS_THM: "ALL (x::nat) (xa::nat) xb::nat. |
128 lemma BITS_THM: "BITS x xa xb = xb div 2 ^ xa mod 2 ^ (Suc x - xa)" |
184 BITS x xa xb = xb div 2 ^ xa mod 2 ^ (Suc x - xa)" |
|
185 by (import bits BITS_THM) |
129 by (import bits BITS_THM) |
186 |
130 |
187 lemma BITSLT_THM: "ALL (h::nat) (l::nat) n::nat. BITS h l n < 2 ^ (Suc h - l)" |
131 lemma BITSLT_THM: "BITS h l n < 2 ^ (Suc h - l)" |
188 by (import bits BITSLT_THM) |
132 by (import bits BITSLT_THM) |
189 |
133 |
190 lemma DIV_MULT_LEM: "ALL (m::nat) n::nat. 0 < n --> m div n * n <= m" |
134 lemma DIV_MULT_LEM: "(0::nat) < (n::nat) ==> (m::nat) div n * n <= m" |
191 by (import bits DIV_MULT_LEM) |
135 by (import bits DIV_MULT_LEM) |
192 |
136 |
193 lemma MOD_2EXP_LEM: "ALL (n::nat) x::nat. n mod 2 ^ x = n - n div 2 ^ x * 2 ^ x" |
137 lemma MOD_2EXP_LEM: "(n::nat) mod (2::nat) ^ (x::nat) = n - n div (2::nat) ^ x * (2::nat) ^ x" |
194 by (import bits MOD_2EXP_LEM) |
138 by (import bits MOD_2EXP_LEM) |
195 |
139 |
196 lemma BITS2_THM: "ALL (h::nat) (l::nat) n::nat. BITS h l n = n mod 2 ^ Suc h div 2 ^ l" |
140 lemma BITS2_THM: "BITS h l n = n mod 2 ^ Suc h div 2 ^ l" |
197 by (import bits BITS2_THM) |
141 by (import bits BITS2_THM) |
198 |
142 |
199 lemma BITS_COMP_THM: "ALL (h1::nat) (l1::nat) (h2::nat) (l2::nat) n::nat. |
143 lemma BITS_COMP_THM: "h2 + l1 <= h1 ==> BITS h2 l2 (BITS h1 l1 n) = BITS (h2 + l1) (l2 + l1) n" |
200 h2 + l1 <= h1 --> BITS h2 l2 (BITS h1 l1 n) = BITS (h2 + l1) (l2 + l1) n" |
|
201 by (import bits BITS_COMP_THM) |
144 by (import bits BITS_COMP_THM) |
202 |
145 |
203 lemma BITS_DIV_THM: "ALL (h::nat) (l::nat) (x::nat) n::nat. |
146 lemma BITS_DIV_THM: "BITS h l x div 2 ^ n = BITS h (l + n) x" |
204 BITS h l x div 2 ^ n = BITS h (l + n) x" |
|
205 by (import bits BITS_DIV_THM) |
147 by (import bits BITS_DIV_THM) |
206 |
148 |
207 lemma BITS_LT_HIGH: "ALL (h::nat) (l::nat) n::nat. n < 2 ^ Suc h --> BITS h l n = n div 2 ^ l" |
149 lemma BITS_LT_HIGH: "n < 2 ^ Suc h ==> BITS h l n = n div 2 ^ l" |
208 by (import bits BITS_LT_HIGH) |
150 by (import bits BITS_LT_HIGH) |
209 |
151 |
210 lemma BITS_ZERO: "ALL (h::nat) (l::nat) n::nat. h < l --> BITS h l n = 0" |
152 lemma BITS_ZERO: "h < l ==> BITS h l n = 0" |
211 by (import bits BITS_ZERO) |
153 by (import bits BITS_ZERO) |
212 |
154 |
213 lemma BITS_ZERO2: "ALL (h::nat) l::nat. BITS h l 0 = 0" |
155 lemma BITS_ZERO2: "BITS h l 0 = 0" |
214 by (import bits BITS_ZERO2) |
156 by (import bits BITS_ZERO2) |
215 |
157 |
216 lemma BITS_ZERO3: "ALL (h::nat) x::nat. BITS h 0 x = x mod 2 ^ Suc h" |
158 lemma BITS_ZERO3: "BITS h 0 x = x mod 2 ^ Suc h" |
217 by (import bits BITS_ZERO3) |
159 by (import bits BITS_ZERO3) |
218 |
160 |
219 lemma BITS_COMP_THM2: "ALL (h1::nat) (l1::nat) (h2::nat) (l2::nat) n::nat. |
161 lemma BITS_COMP_THM2: "BITS h2 l2 (BITS h1 l1 n) = BITS (min h1 (h2 + l1)) (l2 + l1) n" |
220 BITS h2 l2 (BITS h1 l1 n) = BITS (min h1 (h2 + l1)) (l2 + l1) n" |
|
221 by (import bits BITS_COMP_THM2) |
162 by (import bits BITS_COMP_THM2) |
222 |
163 |
223 lemma NOT_MOD2_LEM: "ALL n::nat. (n mod 2 ~= 0) = (n mod 2 = 1)" |
164 lemma NOT_MOD2_LEM: "((n::nat) mod (2::nat) ~= (0::nat)) = (n mod (2::nat) = (1::nat))" |
224 by (import bits NOT_MOD2_LEM) |
165 by (import bits NOT_MOD2_LEM) |
225 |
166 |
226 lemma NOT_MOD2_LEM2: "ALL (n::nat) a::'a::type. (n mod 2 ~= 1) = (n mod 2 = 0)" |
167 lemma NOT_MOD2_LEM2: "((n::nat) mod (2::nat) ~= (1::nat)) = (n mod (2::nat) = (0::nat))" |
227 by (import bits NOT_MOD2_LEM2) |
168 by (import bits NOT_MOD2_LEM2) |
228 |
169 |
229 lemma EVEN_MOD2_LEM: "ALL n::nat. EVEN n = (n mod 2 = 0)" |
170 lemma EVEN_MOD2_LEM: "EVEN n = (n mod 2 = 0)" |
230 by (import bits EVEN_MOD2_LEM) |
171 by (import bits EVEN_MOD2_LEM) |
231 |
172 |
232 lemma ODD_MOD2_LEM: "ALL n::nat. ODD n = (n mod 2 = 1)" |
173 lemma ODD_MOD2_LEM: "ODD n = (n mod 2 = 1)" |
233 by (import bits ODD_MOD2_LEM) |
174 by (import bits ODD_MOD2_LEM) |
234 |
175 |
235 lemma LSB_ODD: "LSBn = ODD" |
176 lemma LSB_ODD: "LSBn = ODD" |
236 by (import bits LSB_ODD) |
177 by (import bits LSB_ODD) |
237 |
178 |
238 lemma DIV_MULT_THM: "ALL (x::nat) n::nat. n div 2 ^ x * 2 ^ x = n - n mod 2 ^ x" |
179 lemma DIV_MULT_THM: "(n::nat) div (2::nat) ^ (x::nat) * (2::nat) ^ x = n - n mod (2::nat) ^ x" |
239 by (import bits DIV_MULT_THM) |
180 by (import bits DIV_MULT_THM) |
240 |
181 |
241 lemma DIV_MULT_THM2: "ALL x::nat. 2 * (x div 2) = x - x mod 2" |
182 lemma DIV_MULT_THM2: "(2::nat) * ((x::nat) div (2::nat)) = x - x mod (2::nat)" |
242 by (import bits DIV_MULT_THM2) |
183 by (import bits DIV_MULT_THM2) |
243 |
184 |
244 lemma LESS_EQ_EXP_MULT: "ALL (a::nat) b::nat. a <= b --> (EX x::nat. 2 ^ b = x * 2 ^ a)" |
185 lemma LESS_EQ_EXP_MULT: "(a::nat) <= (b::nat) ==> EX x::nat. (2::nat) ^ b = x * (2::nat) ^ a" |
245 by (import bits LESS_EQ_EXP_MULT) |
186 by (import bits LESS_EQ_EXP_MULT) |
246 |
187 |
247 lemma SLICE_LEM1: "ALL (a::nat) (x::nat) y::nat. |
188 lemma SLICE_LEM1: "(a::nat) div (2::nat) ^ ((x::nat) + (y::nat)) * (2::nat) ^ (x + y) = |
248 a div 2 ^ (x + y) * 2 ^ (x + y) = |
189 a div (2::nat) ^ x * (2::nat) ^ x - |
249 a div 2 ^ x * 2 ^ x - a div 2 ^ x mod 2 ^ y * 2 ^ x" |
190 a div (2::nat) ^ x mod (2::nat) ^ y * (2::nat) ^ x" |
250 by (import bits SLICE_LEM1) |
191 by (import bits SLICE_LEM1) |
251 |
192 |
252 lemma SLICE_LEM2: "ALL (a::'a::type) (x::nat) y::nat. |
193 lemma SLICE_LEM2: "(n::nat) mod (2::nat) ^ ((x::nat) + (y::nat)) = |
253 (n::nat) mod 2 ^ (x + y) = n mod 2 ^ x + n div 2 ^ x mod 2 ^ y * 2 ^ x" |
194 n mod (2::nat) ^ x + n div (2::nat) ^ x mod (2::nat) ^ y * (2::nat) ^ x" |
254 by (import bits SLICE_LEM2) |
195 by (import bits SLICE_LEM2) |
255 |
196 |
256 lemma SLICE_LEM3: "ALL (n::nat) (h::nat) l::nat. l < h --> n mod 2 ^ Suc l <= n mod 2 ^ h" |
197 lemma SLICE_LEM3: "(l::nat) < (h::nat) ==> (n::nat) mod (2::nat) ^ Suc l <= n mod (2::nat) ^ h" |
257 by (import bits SLICE_LEM3) |
198 by (import bits SLICE_LEM3) |
258 |
199 |
259 lemma SLICE_THM: "ALL (n::nat) (h::nat) l::nat. SLICE h l n = BITS h l n * 2 ^ l" |
200 lemma SLICE_THM: "SLICE h l n = BITS h l n * 2 ^ l" |
260 by (import bits SLICE_THM) |
201 by (import bits SLICE_THM) |
261 |
202 |
262 lemma SLICELT_THM: "ALL (h::nat) (l::nat) n::nat. SLICE h l n < 2 ^ Suc h" |
203 lemma SLICELT_THM: "SLICE h l n < 2 ^ Suc h" |
263 by (import bits SLICELT_THM) |
204 by (import bits SLICELT_THM) |
264 |
205 |
265 lemma BITS_SLICE_THM: "ALL (h::nat) (l::nat) n::nat. BITS h l (SLICE h l n) = BITS h l n" |
206 lemma BITS_SLICE_THM: "BITS h l (SLICE h l n) = BITS h l n" |
266 by (import bits BITS_SLICE_THM) |
207 by (import bits BITS_SLICE_THM) |
267 |
208 |
268 lemma BITS_SLICE_THM2: "ALL (h::nat) (l::nat) n::nat. |
209 lemma BITS_SLICE_THM2: "h <= h2 ==> BITS h2 l (SLICE h l n) = BITS h l n" |
269 h <= (h2::nat) --> BITS h2 l (SLICE h l n) = BITS h l n" |
|
270 by (import bits BITS_SLICE_THM2) |
210 by (import bits BITS_SLICE_THM2) |
271 |
211 |
272 lemma MOD_2EXP_MONO: "ALL (n::nat) (h::nat) l::nat. l <= h --> n mod 2 ^ l <= n mod 2 ^ Suc h" |
212 lemma MOD_2EXP_MONO: "(l::nat) <= (h::nat) ==> (n::nat) mod (2::nat) ^ l <= n mod (2::nat) ^ Suc h" |
273 by (import bits MOD_2EXP_MONO) |
213 by (import bits MOD_2EXP_MONO) |
274 |
214 |
275 lemma SLICE_COMP_THM: "ALL (h::nat) (m::nat) (l::nat) n::nat. |
215 lemma SLICE_COMP_THM: "Suc m <= h & l <= m ==> SLICE h (Suc m) n + SLICE m l n = SLICE h l n" |
276 Suc m <= h & l <= m --> SLICE h (Suc m) n + SLICE m l n = SLICE h l n" |
|
277 by (import bits SLICE_COMP_THM) |
216 by (import bits SLICE_COMP_THM) |
278 |
217 |
279 lemma SLICE_ZERO: "ALL (h::nat) (l::nat) n::nat. h < l --> SLICE h l n = 0" |
218 lemma SLICE_ZERO: "h < l ==> SLICE h l n = 0" |
280 by (import bits SLICE_ZERO) |
219 by (import bits SLICE_ZERO) |
281 |
220 |
282 lemma BIT_COMP_THM3: "ALL (h::nat) (m::nat) (l::nat) n::nat. |
221 lemma BIT_COMP_THM3: "Suc m <= h & l <= m |
283 Suc m <= h & l <= m --> |
222 ==> BITS h (Suc m) n * 2 ^ (Suc m - l) + BITS m l n = BITS h l n" |
284 BITS h (Suc m) n * 2 ^ (Suc m - l) + BITS m l n = BITS h l n" |
|
285 by (import bits BIT_COMP_THM3) |
223 by (import bits BIT_COMP_THM3) |
286 |
224 |
287 lemma NOT_BIT: "ALL (n::nat) a::nat. (~ bit n a) = (BITS n n a = 0)" |
225 lemma NOT_BIT: "(~ bit n a) = (BITS n n a = 0)" |
288 by (import bits NOT_BIT) |
226 by (import bits NOT_BIT) |
289 |
227 |
290 lemma NOT_BITS: "ALL (n::nat) a::nat. (BITS n n a ~= 0) = (BITS n n a = 1)" |
228 lemma NOT_BITS: "(BITS n n a ~= 0) = (BITS n n a = 1)" |
291 by (import bits NOT_BITS) |
229 by (import bits NOT_BITS) |
292 |
230 |
293 lemma NOT_BITS2: "ALL (n::nat) a::nat. (BITS n n a ~= 1) = (BITS n n a = 0)" |
231 lemma NOT_BITS2: "(BITS n n a ~= 1) = (BITS n n a = 0)" |
294 by (import bits NOT_BITS2) |
232 by (import bits NOT_BITS2) |
295 |
233 |
296 lemma BIT_SLICE: "ALL (n::nat) (a::nat) b::nat. |
234 lemma BIT_SLICE: "(bit n a = bit n b) = (SLICE n n a = SLICE n n b)" |
297 (bit n a = bit n b) = (SLICE n n a = SLICE n n b)" |
|
298 by (import bits BIT_SLICE) |
235 by (import bits BIT_SLICE) |
299 |
236 |
300 lemma BIT_SLICE_LEM: "ALL (y::nat) (x::nat) n::nat. SBIT (bit x n) (x + y) = SLICE x x n * 2 ^ y" |
237 lemma BIT_SLICE_LEM: "SBIT (bit x n) (x + y) = SLICE x x n * 2 ^ y" |
301 by (import bits BIT_SLICE_LEM) |
238 by (import bits BIT_SLICE_LEM) |
302 |
239 |
303 lemma BIT_SLICE_THM: "ALL (x::nat) xa::nat. SBIT (bit x xa) x = SLICE x x xa" |
240 lemma BIT_SLICE_THM: "SBIT (bit x xa) x = SLICE x x xa" |
304 by (import bits BIT_SLICE_THM) |
241 by (import bits BIT_SLICE_THM) |
305 |
242 |
306 lemma SBIT_DIV: "ALL (b::bool) (m::nat) n::nat. n < m --> SBIT b (m - n) = SBIT b m div 2 ^ n" |
243 lemma SBIT_DIV: "n < m ==> SBIT b (m - n) = SBIT b m div 2 ^ n" |
307 by (import bits SBIT_DIV) |
244 by (import bits SBIT_DIV) |
308 |
245 |
309 lemma BITS_SUC: "ALL (h::nat) (l::nat) n::nat. |
246 lemma BITS_SUC: "l <= Suc h |
310 l <= Suc h --> |
247 ==> SBIT (bit (Suc h) n) (Suc h - l) + BITS h l n = BITS (Suc h) l n" |
311 SBIT (bit (Suc h) n) (Suc h - l) + BITS h l n = BITS (Suc h) l n" |
|
312 by (import bits BITS_SUC) |
248 by (import bits BITS_SUC) |
313 |
249 |
314 lemma BITS_SUC_THM: "ALL (h::nat) (l::nat) n::nat. |
250 lemma BITS_SUC_THM: "BITS (Suc h) l n = |
315 BITS (Suc h) l n = |
251 (if Suc h < l then 0 else SBIT (bit (Suc h) n) (Suc h - l) + BITS h l n)" |
316 (if Suc h < l then 0 else SBIT (bit (Suc h) n) (Suc h - l) + BITS h l n)" |
|
317 by (import bits BITS_SUC_THM) |
252 by (import bits BITS_SUC_THM) |
318 |
253 |
319 lemma BIT_BITS_THM: "ALL (h::nat) (l::nat) (a::nat) b::nat. |
254 lemma BIT_BITS_THM: "(ALL x. l <= x & x <= h --> bit x a = bit x b) = (BITS h l a = BITS h l b)" |
320 (ALL x::nat. l <= x & x <= h --> bit x a = bit x b) = |
|
321 (BITS h l a = BITS h l b)" |
|
322 by (import bits BIT_BITS_THM) |
255 by (import bits BIT_BITS_THM) |
323 |
256 |
324 lemma BITWISE_LT_2EXP: "ALL (n::nat) (oper::bool => bool => bool) (a::nat) b::nat. |
257 lemma BITWISE_LT_2EXP: "BITWISE n oper a b < 2 ^ n" |
325 BITWISE n oper a b < 2 ^ n" |
|
326 by (import bits BITWISE_LT_2EXP) |
258 by (import bits BITWISE_LT_2EXP) |
327 |
259 |
328 lemma LESS_EXP_MULT2: "(All::(nat => bool) => bool) |
260 lemma LESS_EXP_MULT2: "(a::nat) < (b::nat) |
329 (%a::nat. |
261 ==> EX x::nat. (2::nat) ^ b = (2::nat) ^ (x + (1::nat)) * (2::nat) ^ a" |
330 (All::(nat => bool) => bool) |
|
331 (%b::nat. |
|
332 (op -->::bool => bool => bool) ((op <::nat => nat => bool) a b) |
|
333 ((Ex::(nat => bool) => bool) |
|
334 (%x::nat. |
|
335 (op =::nat => nat => bool) |
|
336 ((op ^::nat => nat => nat) |
|
337 ((number_of \<Colon> int => nat) |
|
338 ((Int.Bit0 \<Colon> int => int) |
|
339 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))) |
|
340 b) |
|
341 ((op *::nat => nat => nat) |
|
342 ((op ^::nat => nat => nat) |
|
343 ((number_of \<Colon> int => nat) |
|
344 ((Int.Bit0 \<Colon> int => int) |
|
345 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))) |
|
346 ((op +::nat => nat => nat) x (1::nat))) |
|
347 ((op ^::nat => nat => nat) |
|
348 ((number_of \<Colon> int => nat) |
|
349 ((Int.Bit0 \<Colon> int => int) |
|
350 ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))) |
|
351 a))))))" |
|
352 by (import bits LESS_EXP_MULT2) |
262 by (import bits LESS_EXP_MULT2) |
353 |
263 |
354 lemma BITWISE_THM: "ALL (x::nat) (n::nat) (oper::bool => bool => bool) (a::nat) b::nat. |
264 lemma BITWISE_THM: "x < n ==> bit x (BITWISE n oper a b) = oper (bit x a) (bit x b)" |
355 x < n --> bit x (BITWISE n oper a b) = oper (bit x a) (bit x b)" |
|
356 by (import bits BITWISE_THM) |
265 by (import bits BITWISE_THM) |
357 |
266 |
358 lemma BITWISE_COR: "ALL (x::nat) (n::nat) (oper::bool => bool => bool) (a::nat) b::nat. |
267 lemma BITWISE_COR: "[| x < n; oper (bit x a) (bit x b) |] |
359 x < n --> |
268 ==> BITWISE n oper a b div 2 ^ x mod 2 = 1" |
360 oper (bit x a) (bit x b) --> BITWISE n oper a b div 2 ^ x mod 2 = 1" |
|
361 by (import bits BITWISE_COR) |
269 by (import bits BITWISE_COR) |
362 |
270 |
363 lemma BITWISE_NOT_COR: "ALL (x::nat) (n::nat) (oper::bool => bool => bool) (a::nat) b::nat. |
271 lemma BITWISE_NOT_COR: "[| x < n; ~ oper (bit x a) (bit x b) |] |
364 x < n --> |
272 ==> BITWISE n oper a b div 2 ^ x mod 2 = 0" |
365 ~ oper (bit x a) (bit x b) --> BITWISE n oper a b div 2 ^ x mod 2 = 0" |
|
366 by (import bits BITWISE_NOT_COR) |
273 by (import bits BITWISE_NOT_COR) |
367 |
274 |
368 lemma MOD_PLUS_RIGHT: "ALL n>0. ALL (j::nat) k::nat. (j + k mod n) mod n = (j + k) mod n" |
275 lemma MOD_PLUS_RIGHT: "(0::nat) < (n::nat) ==> ((j::nat) + (k::nat) mod n) mod n = (j + k) mod n" |
369 by (import bits MOD_PLUS_RIGHT) |
276 by (import bits MOD_PLUS_RIGHT) |
370 |
277 |
371 lemma MOD_PLUS_1: "ALL n>0. ALL x::nat. ((x + 1) mod n = 0) = (x mod n + 1 = n)" |
278 lemma MOD_PLUS_1: "(0::nat) < (n::nat) |
|
279 ==> (((x::nat) + (1::nat)) mod n = (0::nat)) = (x mod n + (1::nat) = n)" |
372 by (import bits MOD_PLUS_1) |
280 by (import bits MOD_PLUS_1) |
373 |
281 |
374 lemma MOD_ADD_1: "ALL n>0. ALL x::nat. (x + 1) mod n ~= 0 --> (x + 1) mod n = x mod n + 1" |
282 lemma MOD_ADD_1: "[| (0::nat) < (n::nat); ((x::nat) + (1::nat)) mod n ~= (0::nat) |] |
|
283 ==> (x + (1::nat)) mod n = x mod n + (1::nat)" |
375 by (import bits MOD_ADD_1) |
284 by (import bits MOD_ADD_1) |
376 |
285 |
377 ;end_setup |
286 ;end_setup |
378 |
287 |
379 ;setup_theory word32 |
288 ;setup_theory word32 |
626 COMP0_primdef: "COMP0 == ONE_COMP 0" |
514 COMP0_primdef: "COMP0 == ONE_COMP 0" |
627 |
515 |
628 lemma COMP0_def: "COMP0 = ONE_COMP 0" |
516 lemma COMP0_def: "COMP0 = ONE_COMP 0" |
629 by (import word32 COMP0_def) |
517 by (import word32 COMP0_def) |
630 |
518 |
631 lemma BITWISE_THM2: "(All::(nat => bool) => bool) |
519 lemma BITWISE_THM2: "(ALL x<WL. oper (bit x a) (bit x b) = bit x y) = |
632 (%y::nat. |
520 EQUIV (BITWISE WL oper a b) y" |
633 (All::((bool => bool => bool) => bool) => bool) |
|
634 (%oper::bool => bool => bool. |
|
635 (All::(nat => bool) => bool) |
|
636 (%a::nat. |
|
637 (All::(nat => bool) => bool) |
|
638 (%b::nat. |
|
639 (op =::bool => bool => bool) |
|
640 ((All::(nat => bool) => bool) |
|
641 (%x::nat. |
|
642 (op -->::bool => bool => bool) |
|
643 ((op <::nat => nat => bool) x (WL::nat)) |
|
644 ((op =::bool => bool => bool) |
|
645 (oper ((bit::nat => nat => bool) x a) |
|
646 ((bit::nat => nat => bool) x b)) |
|
647 ((bit::nat => nat => bool) x y)))) |
|
648 ((EQUIV::nat => nat => bool) |
|
649 ((BITWISE::nat |
|
650 => (bool => bool => bool) |
|
651 => nat => nat => nat) |
|
652 (WL::nat) oper a b) |
|
653 y)))))" |
|
654 by (import word32 BITWISE_THM2) |
521 by (import word32 BITWISE_THM2) |
655 |
522 |
656 lemma OR_ASSOC_QT: "ALL (a::nat) (b::nat) c::nat. EQUIV (OR a (OR b c)) (OR (OR a b) c)" |
523 lemma OR_ASSOC_QT: "EQUIV (OR a (OR b c)) (OR (OR a b) c)" |
657 by (import word32 OR_ASSOC_QT) |
524 by (import word32 OR_ASSOC_QT) |
658 |
525 |
659 lemma OR_COMM_QT: "ALL (a::nat) b::nat. EQUIV (OR a b) (OR b a)" |
526 lemma OR_COMM_QT: "EQUIV (OR a b) (OR b a)" |
660 by (import word32 OR_COMM_QT) |
527 by (import word32 OR_COMM_QT) |
661 |
528 |
662 lemma OR_ABSORB_QT: "ALL (a::nat) b::nat. EQUIV (AND a (OR a b)) a" |
529 lemma OR_ABSORB_QT: "EQUIV (AND a (OR a b)) a" |
663 by (import word32 OR_ABSORB_QT) |
530 by (import word32 OR_ABSORB_QT) |
664 |
531 |
665 lemma OR_IDEM_QT: "ALL a::nat. EQUIV (OR a a) a" |
532 lemma OR_IDEM_QT: "EQUIV (OR a a) a" |
666 by (import word32 OR_IDEM_QT) |
533 by (import word32 OR_IDEM_QT) |
667 |
534 |
668 lemma AND_ASSOC_QT: "ALL (a::nat) (b::nat) c::nat. EQUIV (AND a (AND b c)) (AND (AND a b) c)" |
535 lemma AND_ASSOC_QT: "EQUIV (AND a (AND b c)) (AND (AND a b) c)" |
669 by (import word32 AND_ASSOC_QT) |
536 by (import word32 AND_ASSOC_QT) |
670 |
537 |
671 lemma AND_COMM_QT: "ALL (a::nat) b::nat. EQUIV (AND a b) (AND b a)" |
538 lemma AND_COMM_QT: "EQUIV (AND a b) (AND b a)" |
672 by (import word32 AND_COMM_QT) |
539 by (import word32 AND_COMM_QT) |
673 |
540 |
674 lemma AND_ABSORB_QT: "ALL (a::nat) b::nat. EQUIV (OR a (AND a b)) a" |
541 lemma AND_ABSORB_QT: "EQUIV (OR a (AND a b)) a" |
675 by (import word32 AND_ABSORB_QT) |
542 by (import word32 AND_ABSORB_QT) |
676 |
543 |
677 lemma AND_IDEM_QT: "ALL a::nat. EQUIV (AND a a) a" |
544 lemma AND_IDEM_QT: "EQUIV (AND a a) a" |
678 by (import word32 AND_IDEM_QT) |
545 by (import word32 AND_IDEM_QT) |
679 |
546 |
680 lemma OR_COMP_QT: "ALL a::nat. EQUIV (OR a (ONE_COMP a)) COMP0" |
547 lemma OR_COMP_QT: "EQUIV (OR a (ONE_COMP a)) COMP0" |
681 by (import word32 OR_COMP_QT) |
548 by (import word32 OR_COMP_QT) |
682 |
549 |
683 lemma AND_COMP_QT: "ALL a::nat. EQUIV (AND a (ONE_COMP a)) 0" |
550 lemma AND_COMP_QT: "EQUIV (AND a (ONE_COMP a)) 0" |
684 by (import word32 AND_COMP_QT) |
551 by (import word32 AND_COMP_QT) |
685 |
552 |
686 lemma ONE_COMP_QT: "ALL a::nat. EQUIV (ONE_COMP (ONE_COMP a)) a" |
553 lemma ONE_COMP_QT: "EQUIV (ONE_COMP (ONE_COMP a)) a" |
687 by (import word32 ONE_COMP_QT) |
554 by (import word32 ONE_COMP_QT) |
688 |
555 |
689 lemma RIGHT_AND_OVER_OR_QT: "ALL (a::nat) (b::nat) c::nat. |
556 lemma RIGHT_AND_OVER_OR_QT: "EQUIV (AND (OR a b) c) (OR (AND a c) (AND b c))" |
690 EQUIV (AND (OR a b) c) (OR (AND a c) (AND b c))" |
|
691 by (import word32 RIGHT_AND_OVER_OR_QT) |
557 by (import word32 RIGHT_AND_OVER_OR_QT) |
692 |
558 |
693 lemma RIGHT_OR_OVER_AND_QT: "ALL (a::nat) (b::nat) c::nat. EQUIV (OR (AND a b) c) (AND (OR a c) (OR b c))" |
559 lemma RIGHT_OR_OVER_AND_QT: "EQUIV (OR (AND a b) c) (AND (OR a c) (OR b c))" |
694 by (import word32 RIGHT_OR_OVER_AND_QT) |
560 by (import word32 RIGHT_OR_OVER_AND_QT) |
695 |
561 |
696 lemma DE_MORGAN_THM_QT: "ALL (a::nat) b::nat. |
562 lemma DE_MORGAN_THM_QT: "EQUIV (ONE_COMP (AND a b)) (OR (ONE_COMP a) (ONE_COMP b)) & |
697 EQUIV (ONE_COMP (AND a b)) (OR (ONE_COMP a) (ONE_COMP b)) & |
563 EQUIV (ONE_COMP (OR a b)) (AND (ONE_COMP a) (ONE_COMP b))" |
698 EQUIV (ONE_COMP (OR a b)) (AND (ONE_COMP a) (ONE_COMP b))" |
|
699 by (import word32 DE_MORGAN_THM_QT) |
564 by (import word32 DE_MORGAN_THM_QT) |
700 |
565 |
701 lemma BIT_EQUIV: "ALL (n::nat) (a::nat) b::nat. n < WL --> EQUIV a b --> bit n a = bit n b" |
566 lemma BIT_EQUIV: "[| n < WL; EQUIV a b |] ==> bit n a = bit n b" |
702 by (import word32 BIT_EQUIV) |
567 by (import word32 BIT_EQUIV) |
703 |
568 |
704 lemma LSB_WELLDEF: "ALL (a::nat) b::nat. EQUIV a b --> LSBn a = LSBn b" |
569 lemma LSB_WELLDEF: "EQUIV a b ==> LSBn a = LSBn b" |
705 by (import word32 LSB_WELLDEF) |
570 by (import word32 LSB_WELLDEF) |
706 |
571 |
707 lemma MSB_WELLDEF: "ALL (a::nat) b::nat. EQUIV a b --> MSBn a = MSBn b" |
572 lemma MSB_WELLDEF: "EQUIV a b ==> MSBn a = MSBn b" |
708 by (import word32 MSB_WELLDEF) |
573 by (import word32 MSB_WELLDEF) |
709 |
574 |
710 lemma BITWISE_ISTEP: "ALL (n::nat) (oper::bool => bool => bool) (a::nat) b::nat. |
575 lemma BITWISE_ISTEP: "0 < n |
711 0 < n --> |
576 ==> BITWISE n oper (a div 2) (b div 2) = |
712 BITWISE n oper (a div 2) (b div 2) = |
577 BITWISE n oper a b div 2 + SBIT (oper (bit n a) (bit n b)) (n - 1)" |
713 BITWISE n oper a b div 2 + SBIT (oper (bit n a) (bit n b)) (n - 1)" |
|
714 by (import word32 BITWISE_ISTEP) |
578 by (import word32 BITWISE_ISTEP) |
715 |
579 |
716 lemma BITWISE_EVAL: "ALL (n::nat) (oper::bool => bool => bool) (a::nat) b::nat. |
580 lemma BITWISE_EVAL: "BITWISE (Suc n) oper a b = |
717 BITWISE (Suc n) oper a b = |
581 2 * BITWISE n oper (a div 2) (b div 2) + SBIT (oper (LSBn a) (LSBn b)) 0" |
718 2 * BITWISE n oper (a div 2) (b div 2) + SBIT (oper (LSBn a) (LSBn b)) 0" |
|
719 by (import word32 BITWISE_EVAL) |
582 by (import word32 BITWISE_EVAL) |
720 |
583 |
721 lemma BITWISE_WELLDEF: "ALL (n::nat) (oper::bool => bool => bool) (a::nat) (b::nat) (c::nat) d::nat. |
584 lemma BITWISE_WELLDEF: "EQUIV a b & EQUIV c d ==> EQUIV (BITWISE n oper a c) (BITWISE n oper b d)" |
722 EQUIV a b & EQUIV c d --> EQUIV (BITWISE n oper a c) (BITWISE n oper b d)" |
|
723 by (import word32 BITWISE_WELLDEF) |
585 by (import word32 BITWISE_WELLDEF) |
724 |
586 |
725 lemma BITWISEw_WELLDEF: "ALL (oper::bool => bool => bool) (a::nat) (b::nat) (c::nat) d::nat. |
587 lemma BITWISEw_WELLDEF: "EQUIV a b & EQUIV c d ==> EQUIV (BITWISE WL oper a c) (BITWISE WL oper b d)" |
726 EQUIV a b & EQUIV c d --> |
|
727 EQUIV (BITWISE WL oper a c) (BITWISE WL oper b d)" |
|
728 by (import word32 BITWISEw_WELLDEF) |
588 by (import word32 BITWISEw_WELLDEF) |
729 |
589 |
730 lemma SUC_WELLDEF: "ALL (a::nat) b::nat. EQUIV a b --> EQUIV (Suc a) (Suc b)" |
590 lemma SUC_WELLDEF: "EQUIV a b ==> EQUIV (Suc a) (Suc b)" |
731 by (import word32 SUC_WELLDEF) |
591 by (import word32 SUC_WELLDEF) |
732 |
592 |
733 lemma ADD_WELLDEF: "ALL (a::nat) (b::nat) (c::nat) d::nat. |
593 lemma ADD_WELLDEF: "EQUIV a b & EQUIV c d ==> EQUIV (a + c) (b + d)" |
734 EQUIV a b & EQUIV c d --> EQUIV (a + c) (b + d)" |
|
735 by (import word32 ADD_WELLDEF) |
594 by (import word32 ADD_WELLDEF) |
736 |
595 |
737 lemma MUL_WELLDEF: "ALL (a::nat) (b::nat) (c::nat) d::nat. |
596 lemma MUL_WELLDEF: "EQUIV a b & EQUIV c d ==> EQUIV (a * c) (b * d)" |
738 EQUIV a b & EQUIV c d --> EQUIV (a * c) (b * d)" |
|
739 by (import word32 MUL_WELLDEF) |
597 by (import word32 MUL_WELLDEF) |
740 |
598 |
741 lemma ONE_COMP_WELLDEF: "ALL (a::nat) b::nat. EQUIV a b --> EQUIV (ONE_COMP a) (ONE_COMP b)" |
599 lemma ONE_COMP_WELLDEF: "EQUIV a b ==> EQUIV (ONE_COMP a) (ONE_COMP b)" |
742 by (import word32 ONE_COMP_WELLDEF) |
600 by (import word32 ONE_COMP_WELLDEF) |
743 |
601 |
744 lemma TWO_COMP_WELLDEF: "ALL (a::nat) b::nat. EQUIV a b --> EQUIV (TWO_COMP a) (TWO_COMP b)" |
602 lemma TWO_COMP_WELLDEF: "EQUIV a b ==> EQUIV (TWO_COMP a) (TWO_COMP b)" |
745 by (import word32 TWO_COMP_WELLDEF) |
603 by (import word32 TWO_COMP_WELLDEF) |
746 |
604 |
747 lemma TOw_WELLDEF: "ALL (a::nat) b::nat. EQUIV a b --> EQUIV (MODw a) (MODw b)" |
605 lemma TOw_WELLDEF: "EQUIV a b ==> EQUIV (MODw a) (MODw b)" |
748 by (import word32 TOw_WELLDEF) |
606 by (import word32 TOw_WELLDEF) |
749 |
607 |
750 consts |
608 consts |
751 LSR_ONE :: "nat => nat" |
609 LSR_ONE :: "nat => nat" |
752 |
610 |
753 defs |
611 defs |
754 LSR_ONE_primdef: "LSR_ONE == %a::nat. MODw a div 2" |
612 LSR_ONE_primdef: "LSR_ONE == %a. MODw a div 2" |
755 |
613 |
756 lemma LSR_ONE_def: "ALL a::nat. LSR_ONE a = MODw a div 2" |
614 lemma LSR_ONE_def: "LSR_ONE a = MODw a div 2" |
757 by (import word32 LSR_ONE_def) |
615 by (import word32 LSR_ONE_def) |
758 |
616 |
759 consts |
617 consts |
760 ASR_ONE :: "nat => nat" |
618 ASR_ONE :: "nat => nat" |
761 |
619 |
762 defs |
620 defs |
763 ASR_ONE_primdef: "ASR_ONE == %a::nat. LSR_ONE a + SBIT (MSBn a) HB" |
621 ASR_ONE_primdef: "ASR_ONE == %a. LSR_ONE a + SBIT (MSBn a) HB" |
764 |
622 |
765 lemma ASR_ONE_def: "ALL a::nat. ASR_ONE a = LSR_ONE a + SBIT (MSBn a) HB" |
623 lemma ASR_ONE_def: "ASR_ONE a = LSR_ONE a + SBIT (MSBn a) HB" |
766 by (import word32 ASR_ONE_def) |
624 by (import word32 ASR_ONE_def) |
767 |
625 |
768 consts |
626 consts |
769 ROR_ONE :: "nat => nat" |
627 ROR_ONE :: "nat => nat" |
770 |
628 |
771 defs |
629 defs |
772 ROR_ONE_primdef: "ROR_ONE == %a::nat. LSR_ONE a + SBIT (LSBn a) HB" |
630 ROR_ONE_primdef: "ROR_ONE == %a. LSR_ONE a + SBIT (LSBn a) HB" |
773 |
631 |
774 lemma ROR_ONE_def: "ALL a::nat. ROR_ONE a = LSR_ONE a + SBIT (LSBn a) HB" |
632 lemma ROR_ONE_def: "ROR_ONE a = LSR_ONE a + SBIT (LSBn a) HB" |
775 by (import word32 ROR_ONE_def) |
633 by (import word32 ROR_ONE_def) |
776 |
634 |
777 consts |
635 consts |
778 RRXn :: "bool => nat => nat" |
636 RRXn :: "bool => nat => nat" |
779 |
637 |
780 defs |
638 defs |
781 RRXn_primdef: "RRXn == %(c::bool) a::nat. LSR_ONE a + SBIT c HB" |
639 RRXn_primdef: "RRXn == %c a. LSR_ONE a + SBIT c HB" |
782 |
640 |
783 lemma RRXn_def: "ALL (c::bool) a::nat. RRXn c a = LSR_ONE a + SBIT c HB" |
641 lemma RRXn_def: "RRXn c a = LSR_ONE a + SBIT c HB" |
784 by (import word32 RRXn_def) |
642 by (import word32 RRXn_def) |
785 |
643 |
786 lemma LSR_ONE_WELLDEF: "ALL (a::nat) b::nat. EQUIV a b --> EQUIV (LSR_ONE a) (LSR_ONE b)" |
644 lemma LSR_ONE_WELLDEF: "EQUIV a b ==> EQUIV (LSR_ONE a) (LSR_ONE b)" |
787 by (import word32 LSR_ONE_WELLDEF) |
645 by (import word32 LSR_ONE_WELLDEF) |
788 |
646 |
789 lemma ASR_ONE_WELLDEF: "ALL (a::nat) b::nat. EQUIV a b --> EQUIV (ASR_ONE a) (ASR_ONE b)" |
647 lemma ASR_ONE_WELLDEF: "EQUIV a b ==> EQUIV (ASR_ONE a) (ASR_ONE b)" |
790 by (import word32 ASR_ONE_WELLDEF) |
648 by (import word32 ASR_ONE_WELLDEF) |
791 |
649 |
792 lemma ROR_ONE_WELLDEF: "ALL (a::nat) b::nat. EQUIV a b --> EQUIV (ROR_ONE a) (ROR_ONE b)" |
650 lemma ROR_ONE_WELLDEF: "EQUIV a b ==> EQUIV (ROR_ONE a) (ROR_ONE b)" |
793 by (import word32 ROR_ONE_WELLDEF) |
651 by (import word32 ROR_ONE_WELLDEF) |
794 |
652 |
795 lemma RRX_WELLDEF: "ALL (a::nat) (b::nat) c::bool. EQUIV a b --> EQUIV (RRXn c a) (RRXn c b)" |
653 lemma RRX_WELLDEF: "EQUIV a b ==> EQUIV (RRXn c a) (RRXn c b)" |
796 by (import word32 RRX_WELLDEF) |
654 by (import word32 RRX_WELLDEF) |
797 |
655 |
798 lemma LSR_ONE: "LSR_ONE = BITS HB 1" |
656 lemma LSR_ONE: "LSR_ONE = BITS HB 1" |
799 by (import word32 LSR_ONE) |
657 by (import word32 LSR_ONE) |
800 |
658 |
801 typedef (open) word32 = "{x::nat => bool. EX xa::nat. x = EQUIV xa}" |
659 typedef (open) word32 = "{x::nat => bool. EX xa. x = EQUIV xa}" |
802 by (rule typedef_helper,import word32 word32_TY_DEF) |
660 by (rule typedef_helper,import word32 word32_TY_DEF) |
803 |
661 |
804 lemmas word32_TY_DEF = typedef_hol2hol4 [OF type_definition_word32] |
662 lemmas word32_TY_DEF = typedef_hol2hol4 [OF type_definition_word32] |
805 |
663 |
806 consts |
664 consts |
807 mk_word32 :: "(nat => bool) => word32" |
665 mk_word32 :: "(nat => bool) => word32" |
808 dest_word32 :: "word32 => nat => bool" |
666 dest_word32 :: "word32 => nat => bool" |
809 |
667 |
810 specification (dest_word32 mk_word32) word32_tybij: "(ALL a::word32. mk_word32 (dest_word32 a) = a) & |
668 specification (dest_word32 mk_word32) word32_tybij: "(ALL a. mk_word32 (dest_word32 a) = a) & |
811 (ALL r::nat => bool. |
669 (ALL r. (EX x. r = EQUIV x) = (dest_word32 (mk_word32 r) = r))" |
812 (EX x::nat. r = EQUIV x) = (dest_word32 (mk_word32 r) = r))" |
|
813 by (import word32 word32_tybij) |
670 by (import word32 word32_tybij) |
814 |
671 |
815 consts |
672 consts |
816 w_0 :: "word32" |
673 w_0 :: "word32" |
817 |
674 |
837 w_T_primdef: "w_T == mk_word32 (EQUIV COMP0)" |
694 w_T_primdef: "w_T == mk_word32 (EQUIV COMP0)" |
838 |
695 |
839 lemma w_T_def: "w_T = mk_word32 (EQUIV COMP0)" |
696 lemma w_T_def: "w_T = mk_word32 (EQUIV COMP0)" |
840 by (import word32 w_T_def) |
697 by (import word32 w_T_def) |
841 |
698 |
842 definition word_suc :: "word32 => word32" where |
699 definition |
843 "word_suc == %T1::word32. mk_word32 (EQUIV (Suc (Eps (dest_word32 T1))))" |
700 word_suc :: "word32 => word32" where |
844 |
701 "word_suc == %T1. mk_word32 (EQUIV (Suc (Eps (dest_word32 T1))))" |
845 lemma word_suc: "ALL T1::word32. word_suc T1 = mk_word32 (EQUIV (Suc (Eps (dest_word32 T1))))" |
702 |
|
703 lemma word_suc: "word_suc T1 = mk_word32 (EQUIV (Suc (Eps (dest_word32 T1))))" |
846 by (import word32 word_suc) |
704 by (import word32 word_suc) |
847 |
705 |
848 definition word_add :: "word32 => word32 => word32" where |
706 definition |
|
707 word_add :: "word32 => word32 => word32" where |
849 "word_add == |
708 "word_add == |
850 %(T1::word32) T2::word32. |
709 %T1 T2. mk_word32 (EQUIV (Eps (dest_word32 T1) + Eps (dest_word32 T2)))" |
851 mk_word32 (EQUIV (Eps (dest_word32 T1) + Eps (dest_word32 T2)))" |
710 |
852 |
711 lemma word_add: "word_add T1 T2 = |
853 lemma word_add: "ALL (T1::word32) T2::word32. |
712 mk_word32 (EQUIV (Eps (dest_word32 T1) + Eps (dest_word32 T2)))" |
854 word_add T1 T2 = |
|
855 mk_word32 (EQUIV (Eps (dest_word32 T1) + Eps (dest_word32 T2)))" |
|
856 by (import word32 word_add) |
713 by (import word32 word_add) |
857 |
714 |
858 definition word_mul :: "word32 => word32 => word32" where |
715 definition |
|
716 word_mul :: "word32 => word32 => word32" where |
859 "word_mul == |
717 "word_mul == |
860 %(T1::word32) T2::word32. |
718 %T1 T2. mk_word32 (EQUIV (Eps (dest_word32 T1) * Eps (dest_word32 T2)))" |
861 mk_word32 (EQUIV (Eps (dest_word32 T1) * Eps (dest_word32 T2)))" |
719 |
862 |
720 lemma word_mul: "word_mul T1 T2 = |
863 lemma word_mul: "ALL (T1::word32) T2::word32. |
721 mk_word32 (EQUIV (Eps (dest_word32 T1) * Eps (dest_word32 T2)))" |
864 word_mul T1 T2 = |
|
865 mk_word32 (EQUIV (Eps (dest_word32 T1) * Eps (dest_word32 T2)))" |
|
866 by (import word32 word_mul) |
722 by (import word32 word_mul) |
867 |
723 |
868 definition word_1comp :: "word32 => word32" where |
724 definition |
869 "word_1comp == |
725 word_1comp :: "word32 => word32" where |
870 %T1::word32. mk_word32 (EQUIV (ONE_COMP (Eps (dest_word32 T1))))" |
726 "word_1comp == %T1. mk_word32 (EQUIV (ONE_COMP (Eps (dest_word32 T1))))" |
871 |
727 |
872 lemma word_1comp: "ALL T1::word32. |
728 lemma word_1comp: "word_1comp T1 = mk_word32 (EQUIV (ONE_COMP (Eps (dest_word32 T1))))" |
873 word_1comp T1 = mk_word32 (EQUIV (ONE_COMP (Eps (dest_word32 T1))))" |
|
874 by (import word32 word_1comp) |
729 by (import word32 word_1comp) |
875 |
730 |
876 definition word_2comp :: "word32 => word32" where |
731 definition |
877 "word_2comp == |
732 word_2comp :: "word32 => word32" where |
878 %T1::word32. mk_word32 (EQUIV (TWO_COMP (Eps (dest_word32 T1))))" |
733 "word_2comp == %T1. mk_word32 (EQUIV (TWO_COMP (Eps (dest_word32 T1))))" |
879 |
734 |
880 lemma word_2comp: "ALL T1::word32. |
735 lemma word_2comp: "word_2comp T1 = mk_word32 (EQUIV (TWO_COMP (Eps (dest_word32 T1))))" |
881 word_2comp T1 = mk_word32 (EQUIV (TWO_COMP (Eps (dest_word32 T1))))" |
|
882 by (import word32 word_2comp) |
736 by (import word32 word_2comp) |
883 |
737 |
884 definition word_lsr1 :: "word32 => word32" where |
738 definition |
885 "word_lsr1 == %T1::word32. mk_word32 (EQUIV (LSR_ONE (Eps (dest_word32 T1))))" |
739 word_lsr1 :: "word32 => word32" where |
886 |
740 "word_lsr1 == %T1. mk_word32 (EQUIV (LSR_ONE (Eps (dest_word32 T1))))" |
887 lemma word_lsr1: "ALL T1::word32. |
741 |
888 word_lsr1 T1 = mk_word32 (EQUIV (LSR_ONE (Eps (dest_word32 T1))))" |
742 lemma word_lsr1: "word_lsr1 T1 = mk_word32 (EQUIV (LSR_ONE (Eps (dest_word32 T1))))" |
889 by (import word32 word_lsr1) |
743 by (import word32 word_lsr1) |
890 |
744 |
891 definition word_asr1 :: "word32 => word32" where |
745 definition |
892 "word_asr1 == %T1::word32. mk_word32 (EQUIV (ASR_ONE (Eps (dest_word32 T1))))" |
746 word_asr1 :: "word32 => word32" where |
893 |
747 "word_asr1 == %T1. mk_word32 (EQUIV (ASR_ONE (Eps (dest_word32 T1))))" |
894 lemma word_asr1: "ALL T1::word32. |
748 |
895 word_asr1 T1 = mk_word32 (EQUIV (ASR_ONE (Eps (dest_word32 T1))))" |
749 lemma word_asr1: "word_asr1 T1 = mk_word32 (EQUIV (ASR_ONE (Eps (dest_word32 T1))))" |
896 by (import word32 word_asr1) |
750 by (import word32 word_asr1) |
897 |
751 |
898 definition word_ror1 :: "word32 => word32" where |
752 definition |
899 "word_ror1 == %T1::word32. mk_word32 (EQUIV (ROR_ONE (Eps (dest_word32 T1))))" |
753 word_ror1 :: "word32 => word32" where |
900 |
754 "word_ror1 == %T1. mk_word32 (EQUIV (ROR_ONE (Eps (dest_word32 T1))))" |
901 lemma word_ror1: "ALL T1::word32. |
755 |
902 word_ror1 T1 = mk_word32 (EQUIV (ROR_ONE (Eps (dest_word32 T1))))" |
756 lemma word_ror1: "word_ror1 T1 = mk_word32 (EQUIV (ROR_ONE (Eps (dest_word32 T1))))" |
903 by (import word32 word_ror1) |
757 by (import word32 word_ror1) |
904 |
758 |
905 consts |
759 consts |
906 RRX :: "bool => word32 => word32" |
760 RRX :: "bool => word32 => word32" |
907 |
761 |
908 defs |
762 defs |
909 RRX_primdef: "RRX == |
763 RRX_primdef: "RRX == %T1 T2. mk_word32 (EQUIV (RRXn T1 (Eps (dest_word32 T2))))" |
910 %(T1::bool) T2::word32. mk_word32 (EQUIV (RRXn T1 (Eps (dest_word32 T2))))" |
764 |
911 |
765 lemma RRX_def: "RRX T1 T2 = mk_word32 (EQUIV (RRXn T1 (Eps (dest_word32 T2))))" |
912 lemma RRX_def: "ALL (T1::bool) T2::word32. |
|
913 RRX T1 T2 = mk_word32 (EQUIV (RRXn T1 (Eps (dest_word32 T2))))" |
|
914 by (import word32 RRX_def) |
766 by (import word32 RRX_def) |
915 |
767 |
916 consts |
768 consts |
917 LSB :: "word32 => bool" |
769 LSB :: "word32 => bool" |
918 |
770 |
919 defs |
771 defs |
920 LSB_primdef: "LSB == %T1::word32. LSBn (Eps (dest_word32 T1))" |
772 LSB_primdef: "LSB == %T1. LSBn (Eps (dest_word32 T1))" |
921 |
773 |
922 lemma LSB_def: "ALL T1::word32. LSB T1 = LSBn (Eps (dest_word32 T1))" |
774 lemma LSB_def: "LSB T1 = LSBn (Eps (dest_word32 T1))" |
923 by (import word32 LSB_def) |
775 by (import word32 LSB_def) |
924 |
776 |
925 consts |
777 consts |
926 MSB :: "word32 => bool" |
778 MSB :: "word32 => bool" |
927 |
779 |
928 defs |
780 defs |
929 MSB_primdef: "MSB == %T1::word32. MSBn (Eps (dest_word32 T1))" |
781 MSB_primdef: "MSB == %T1. MSBn (Eps (dest_word32 T1))" |
930 |
782 |
931 lemma MSB_def: "ALL T1::word32. MSB T1 = MSBn (Eps (dest_word32 T1))" |
783 lemma MSB_def: "MSB T1 = MSBn (Eps (dest_word32 T1))" |
932 by (import word32 MSB_def) |
784 by (import word32 MSB_def) |
933 |
785 |
934 definition bitwise_or :: "word32 => word32 => word32" where |
786 definition |
|
787 bitwise_or :: "word32 => word32 => word32" where |
935 "bitwise_or == |
788 "bitwise_or == |
936 %(T1::word32) T2::word32. |
789 %T1 T2. mk_word32 (EQUIV (OR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
937 mk_word32 (EQUIV (OR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
790 |
938 |
791 lemma bitwise_or: "bitwise_or T1 T2 = |
939 lemma bitwise_or: "ALL (T1::word32) T2::word32. |
792 mk_word32 (EQUIV (OR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
940 bitwise_or T1 T2 = |
|
941 mk_word32 (EQUIV (OR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
|
942 by (import word32 bitwise_or) |
793 by (import word32 bitwise_or) |
943 |
794 |
944 definition bitwise_eor :: "word32 => word32 => word32" where |
795 definition |
|
796 bitwise_eor :: "word32 => word32 => word32" where |
945 "bitwise_eor == |
797 "bitwise_eor == |
946 %(T1::word32) T2::word32. |
798 %T1 T2. |
947 mk_word32 (EQUIV (EOR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
799 mk_word32 (EQUIV (EOR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
948 |
800 |
949 lemma bitwise_eor: "ALL (T1::word32) T2::word32. |
801 lemma bitwise_eor: "bitwise_eor T1 T2 = |
950 bitwise_eor T1 T2 = |
802 mk_word32 (EQUIV (EOR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
951 mk_word32 (EQUIV (EOR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
|
952 by (import word32 bitwise_eor) |
803 by (import word32 bitwise_eor) |
953 |
804 |
954 definition bitwise_and :: "word32 => word32 => word32" where |
805 definition |
|
806 bitwise_and :: "word32 => word32 => word32" where |
955 "bitwise_and == |
807 "bitwise_and == |
956 %(T1::word32) T2::word32. |
808 %T1 T2. |
957 mk_word32 (EQUIV (AND (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
809 mk_word32 (EQUIV (AND (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
958 |
810 |
959 lemma bitwise_and: "ALL (T1::word32) T2::word32. |
811 lemma bitwise_and: "bitwise_and T1 T2 = |
960 bitwise_and T1 T2 = |
812 mk_word32 (EQUIV (AND (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
961 mk_word32 (EQUIV (AND (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
|
962 by (import word32 bitwise_and) |
813 by (import word32 bitwise_and) |
963 |
814 |
964 consts |
815 consts |
965 TOw :: "word32 => word32" |
816 TOw :: "word32 => word32" |
966 |
817 |
967 defs |
818 defs |
968 TOw_primdef: "TOw == %T1::word32. mk_word32 (EQUIV (MODw (Eps (dest_word32 T1))))" |
819 TOw_primdef: "TOw == %T1. mk_word32 (EQUIV (MODw (Eps (dest_word32 T1))))" |
969 |
820 |
970 lemma TOw_def: "ALL T1::word32. TOw T1 = mk_word32 (EQUIV (MODw (Eps (dest_word32 T1))))" |
821 lemma TOw_def: "TOw T1 = mk_word32 (EQUIV (MODw (Eps (dest_word32 T1))))" |
971 by (import word32 TOw_def) |
822 by (import word32 TOw_def) |
972 |
823 |
973 consts |
824 consts |
974 n2w :: "nat => word32" |
825 n2w :: "nat => word32" |
975 |
826 |
976 defs |
827 defs |
977 n2w_primdef: "n2w == %n::nat. mk_word32 (EQUIV n)" |
828 n2w_primdef: "n2w == %n. mk_word32 (EQUIV n)" |
978 |
829 |
979 lemma n2w_def: "ALL n::nat. n2w n = mk_word32 (EQUIV n)" |
830 lemma n2w_def: "n2w n = mk_word32 (EQUIV n)" |
980 by (import word32 n2w_def) |
831 by (import word32 n2w_def) |
981 |
832 |
982 consts |
833 consts |
983 w2n :: "word32 => nat" |
834 w2n :: "word32 => nat" |
984 |
835 |
985 defs |
836 defs |
986 w2n_primdef: "w2n == %w::word32. MODw (Eps (dest_word32 w))" |
837 w2n_primdef: "w2n == %w. MODw (Eps (dest_word32 w))" |
987 |
838 |
988 lemma w2n_def: "ALL w::word32. w2n w = MODw (Eps (dest_word32 w))" |
839 lemma w2n_def: "w2n w = MODw (Eps (dest_word32 w))" |
989 by (import word32 w2n_def) |
840 by (import word32 w2n_def) |
990 |
841 |
991 lemma ADDw: "(ALL x::word32. word_add w_0 x = x) & |
842 lemma ADDw: "(ALL x. word_add w_0 x = x) & |
992 (ALL (x::word32) xa::word32. |
843 (ALL x xa. word_add (word_suc x) xa = word_suc (word_add x xa))" |
993 word_add (word_suc x) xa = word_suc (word_add x xa))" |
|
994 by (import word32 ADDw) |
844 by (import word32 ADDw) |
995 |
845 |
996 lemma ADD_0w: "ALL x::word32. word_add x w_0 = x" |
846 lemma ADD_0w: "word_add x w_0 = x" |
997 by (import word32 ADD_0w) |
847 by (import word32 ADD_0w) |
998 |
848 |
999 lemma ADD1w: "ALL x::word32. word_suc x = word_add x w_1" |
849 lemma ADD1w: "word_suc x = word_add x w_1" |
1000 by (import word32 ADD1w) |
850 by (import word32 ADD1w) |
1001 |
851 |
1002 lemma ADD_ASSOCw: "ALL (x::word32) (xa::word32) xb::word32. |
852 lemma ADD_ASSOCw: "word_add x (word_add xa xb) = word_add (word_add x xa) xb" |
1003 word_add x (word_add xa xb) = word_add (word_add x xa) xb" |
|
1004 by (import word32 ADD_ASSOCw) |
853 by (import word32 ADD_ASSOCw) |
1005 |
854 |
1006 lemma ADD_CLAUSESw: "(ALL x::word32. word_add w_0 x = x) & |
855 lemma ADD_CLAUSESw: "(ALL x. word_add w_0 x = x) & |
1007 (ALL x::word32. word_add x w_0 = x) & |
856 (ALL x. word_add x w_0 = x) & |
1008 (ALL (x::word32) xa::word32. |
857 (ALL x xa. word_add (word_suc x) xa = word_suc (word_add x xa)) & |
1009 word_add (word_suc x) xa = word_suc (word_add x xa)) & |
858 (ALL x xa. word_add x (word_suc xa) = word_suc (word_add x xa))" |
1010 (ALL (x::word32) xa::word32. |
|
1011 word_add x (word_suc xa) = word_suc (word_add x xa))" |
|
1012 by (import word32 ADD_CLAUSESw) |
859 by (import word32 ADD_CLAUSESw) |
1013 |
860 |
1014 lemma ADD_COMMw: "ALL (x::word32) xa::word32. word_add x xa = word_add xa x" |
861 lemma ADD_COMMw: "word_add x xa = word_add xa x" |
1015 by (import word32 ADD_COMMw) |
862 by (import word32 ADD_COMMw) |
1016 |
863 |
1017 lemma ADD_INV_0_EQw: "ALL (x::word32) xa::word32. (word_add x xa = x) = (xa = w_0)" |
864 lemma ADD_INV_0_EQw: "(word_add x xa = x) = (xa = w_0)" |
1018 by (import word32 ADD_INV_0_EQw) |
865 by (import word32 ADD_INV_0_EQw) |
1019 |
866 |
1020 lemma EQ_ADD_LCANCELw: "ALL (x::word32) (xa::word32) xb::word32. |
867 lemma EQ_ADD_LCANCELw: "(word_add x xa = word_add x xb) = (xa = xb)" |
1021 (word_add x xa = word_add x xb) = (xa = xb)" |
|
1022 by (import word32 EQ_ADD_LCANCELw) |
868 by (import word32 EQ_ADD_LCANCELw) |
1023 |
869 |
1024 lemma EQ_ADD_RCANCELw: "ALL (x::word32) (xa::word32) xb::word32. |
870 lemma EQ_ADD_RCANCELw: "(word_add x xb = word_add xa xb) = (x = xa)" |
1025 (word_add x xb = word_add xa xb) = (x = xa)" |
|
1026 by (import word32 EQ_ADD_RCANCELw) |
871 by (import word32 EQ_ADD_RCANCELw) |
1027 |
872 |
1028 lemma LEFT_ADD_DISTRIBw: "ALL (x::word32) (xa::word32) xb::word32. |
873 lemma LEFT_ADD_DISTRIBw: "word_mul xb (word_add x xa) = word_add (word_mul xb x) (word_mul xb xa)" |
1029 word_mul xb (word_add x xa) = word_add (word_mul xb x) (word_mul xb xa)" |
|
1030 by (import word32 LEFT_ADD_DISTRIBw) |
874 by (import word32 LEFT_ADD_DISTRIBw) |
1031 |
875 |
1032 lemma MULT_ASSOCw: "ALL (x::word32) (xa::word32) xb::word32. |
876 lemma MULT_ASSOCw: "word_mul x (word_mul xa xb) = word_mul (word_mul x xa) xb" |
1033 word_mul x (word_mul xa xb) = word_mul (word_mul x xa) xb" |
|
1034 by (import word32 MULT_ASSOCw) |
877 by (import word32 MULT_ASSOCw) |
1035 |
878 |
1036 lemma MULT_COMMw: "ALL (x::word32) xa::word32. word_mul x xa = word_mul xa x" |
879 lemma MULT_COMMw: "word_mul x xa = word_mul xa x" |
1037 by (import word32 MULT_COMMw) |
880 by (import word32 MULT_COMMw) |
1038 |
881 |
1039 lemma MULT_CLAUSESw: "ALL (x::word32) xa::word32. |
882 lemma MULT_CLAUSESw: "word_mul w_0 x = w_0 & |
1040 word_mul w_0 x = w_0 & |
883 word_mul x w_0 = w_0 & |
1041 word_mul x w_0 = w_0 & |
884 word_mul w_1 x = x & |
1042 word_mul w_1 x = x & |
885 word_mul x w_1 = x & |
1043 word_mul x w_1 = x & |
886 word_mul (word_suc x) xa = word_add (word_mul x xa) xa & |
1044 word_mul (word_suc x) xa = word_add (word_mul x xa) xa & |
887 word_mul x (word_suc xa) = word_add x (word_mul x xa)" |
1045 word_mul x (word_suc xa) = word_add x (word_mul x xa)" |
|
1046 by (import word32 MULT_CLAUSESw) |
888 by (import word32 MULT_CLAUSESw) |
1047 |
889 |
1048 lemma TWO_COMP_ONE_COMP: "ALL x::word32. word_2comp x = word_add (word_1comp x) w_1" |
890 lemma TWO_COMP_ONE_COMP: "word_2comp x = word_add (word_1comp x) w_1" |
1049 by (import word32 TWO_COMP_ONE_COMP) |
891 by (import word32 TWO_COMP_ONE_COMP) |
1050 |
892 |
1051 lemma OR_ASSOCw: "ALL (x::word32) (xa::word32) xb::word32. |
893 lemma OR_ASSOCw: "bitwise_or x (bitwise_or xa xb) = bitwise_or (bitwise_or x xa) xb" |
1052 bitwise_or x (bitwise_or xa xb) = bitwise_or (bitwise_or x xa) xb" |
|
1053 by (import word32 OR_ASSOCw) |
894 by (import word32 OR_ASSOCw) |
1054 |
895 |
1055 lemma OR_COMMw: "ALL (x::word32) xa::word32. bitwise_or x xa = bitwise_or xa x" |
896 lemma OR_COMMw: "bitwise_or x xa = bitwise_or xa x" |
1056 by (import word32 OR_COMMw) |
897 by (import word32 OR_COMMw) |
1057 |
898 |
1058 lemma OR_IDEMw: "ALL x::word32. bitwise_or x x = x" |
899 lemma OR_IDEMw: "bitwise_or x x = x" |
1059 by (import word32 OR_IDEMw) |
900 by (import word32 OR_IDEMw) |
1060 |
901 |
1061 lemma OR_ABSORBw: "ALL (x::word32) xa::word32. bitwise_and x (bitwise_or x xa) = x" |
902 lemma OR_ABSORBw: "bitwise_and x (bitwise_or x xa) = x" |
1062 by (import word32 OR_ABSORBw) |
903 by (import word32 OR_ABSORBw) |
1063 |
904 |
1064 lemma AND_ASSOCw: "ALL (x::word32) (xa::word32) xb::word32. |
905 lemma AND_ASSOCw: "bitwise_and x (bitwise_and xa xb) = bitwise_and (bitwise_and x xa) xb" |
1065 bitwise_and x (bitwise_and xa xb) = bitwise_and (bitwise_and x xa) xb" |
|
1066 by (import word32 AND_ASSOCw) |
906 by (import word32 AND_ASSOCw) |
1067 |
907 |
1068 lemma AND_COMMw: "ALL (x::word32) xa::word32. bitwise_and x xa = bitwise_and xa x" |
908 lemma AND_COMMw: "bitwise_and x xa = bitwise_and xa x" |
1069 by (import word32 AND_COMMw) |
909 by (import word32 AND_COMMw) |
1070 |
910 |
1071 lemma AND_IDEMw: "ALL x::word32. bitwise_and x x = x" |
911 lemma AND_IDEMw: "bitwise_and x x = x" |
1072 by (import word32 AND_IDEMw) |
912 by (import word32 AND_IDEMw) |
1073 |
913 |
1074 lemma AND_ABSORBw: "ALL (x::word32) xa::word32. bitwise_or x (bitwise_and x xa) = x" |
914 lemma AND_ABSORBw: "bitwise_or x (bitwise_and x xa) = x" |
1075 by (import word32 AND_ABSORBw) |
915 by (import word32 AND_ABSORBw) |
1076 |
916 |
1077 lemma ONE_COMPw: "ALL x::word32. word_1comp (word_1comp x) = x" |
917 lemma ONE_COMPw: "word_1comp (word_1comp x) = x" |
1078 by (import word32 ONE_COMPw) |
918 by (import word32 ONE_COMPw) |
1079 |
919 |
1080 lemma RIGHT_AND_OVER_ORw: "ALL (x::word32) (xa::word32) xb::word32. |
920 lemma RIGHT_AND_OVER_ORw: "bitwise_and (bitwise_or x xa) xb = |
1081 bitwise_and (bitwise_or x xa) xb = |
921 bitwise_or (bitwise_and x xb) (bitwise_and xa xb)" |
1082 bitwise_or (bitwise_and x xb) (bitwise_and xa xb)" |
|
1083 by (import word32 RIGHT_AND_OVER_ORw) |
922 by (import word32 RIGHT_AND_OVER_ORw) |
1084 |
923 |
1085 lemma RIGHT_OR_OVER_ANDw: "ALL (x::word32) (xa::word32) xb::word32. |
924 lemma RIGHT_OR_OVER_ANDw: "bitwise_or (bitwise_and x xa) xb = |
1086 bitwise_or (bitwise_and x xa) xb = |
925 bitwise_and (bitwise_or x xb) (bitwise_or xa xb)" |
1087 bitwise_and (bitwise_or x xb) (bitwise_or xa xb)" |
|
1088 by (import word32 RIGHT_OR_OVER_ANDw) |
926 by (import word32 RIGHT_OR_OVER_ANDw) |
1089 |
927 |
1090 lemma DE_MORGAN_THMw: "ALL (x::word32) xa::word32. |
928 lemma DE_MORGAN_THMw: "word_1comp (bitwise_and x xa) = bitwise_or (word_1comp x) (word_1comp xa) & |
1091 word_1comp (bitwise_and x xa) = |
929 word_1comp (bitwise_or x xa) = bitwise_and (word_1comp x) (word_1comp xa)" |
1092 bitwise_or (word_1comp x) (word_1comp xa) & |
|
1093 word_1comp (bitwise_or x xa) = bitwise_and (word_1comp x) (word_1comp xa)" |
|
1094 by (import word32 DE_MORGAN_THMw) |
930 by (import word32 DE_MORGAN_THMw) |
1095 |
931 |
1096 lemma w_0: "w_0 = n2w 0" |
932 lemma w_0: "w_0 = n2w 0" |
1097 by (import word32 w_0) |
933 by (import word32 w_0) |
1098 |
934 |
1134 (NUMERAL_BIT1 |
970 (NUMERAL_BIT1 |
1135 (NUMERAL_BIT1 |
971 (NUMERAL_BIT1 |
1136 ALT_ZERO)))))))))))))))))))))))))))))))))" |
972 ALT_ZERO)))))))))))))))))))))))))))))))))" |
1137 by (import word32 w_T) |
973 by (import word32 w_T) |
1138 |
974 |
1139 lemma ADD_TWO_COMP: "ALL x::word32. word_add x (word_2comp x) = w_0" |
975 lemma ADD_TWO_COMP: "word_add x (word_2comp x) = w_0" |
1140 by (import word32 ADD_TWO_COMP) |
976 by (import word32 ADD_TWO_COMP) |
1141 |
977 |
1142 lemma ADD_TWO_COMP2: "ALL x::word32. word_add (word_2comp x) x = w_0" |
978 lemma ADD_TWO_COMP2: "word_add (word_2comp x) x = w_0" |
1143 by (import word32 ADD_TWO_COMP2) |
979 by (import word32 ADD_TWO_COMP2) |
1144 |
980 |
1145 definition word_sub :: "word32 => word32 => word32" where |
981 definition |
1146 "word_sub == %(a::word32) b::word32. word_add a (word_2comp b)" |
982 word_sub :: "word32 => word32 => word32" where |
1147 |
983 "word_sub == %a b. word_add a (word_2comp b)" |
1148 lemma word_sub: "ALL (a::word32) b::word32. word_sub a b = word_add a (word_2comp b)" |
984 |
|
985 lemma word_sub: "word_sub a b = word_add a (word_2comp b)" |
1149 by (import word32 word_sub) |
986 by (import word32 word_sub) |
1150 |
987 |
1151 definition word_lsl :: "word32 => nat => word32" where |
988 definition |
1152 "word_lsl == %(a::word32) n::nat. word_mul a (n2w (2 ^ n))" |
989 word_lsl :: "word32 => nat => word32" where |
1153 |
990 "word_lsl == %a n. word_mul a (n2w (2 ^ n))" |
1154 lemma word_lsl: "ALL (a::word32) n::nat. word_lsl a n = word_mul a (n2w (2 ^ n))" |
991 |
|
992 lemma word_lsl: "word_lsl a n = word_mul a (n2w (2 ^ n))" |
1155 by (import word32 word_lsl) |
993 by (import word32 word_lsl) |
1156 |
994 |
1157 definition word_lsr :: "word32 => nat => word32" where |
995 definition |
1158 "word_lsr == %(a::word32) n::nat. (word_lsr1 ^^ n) a" |
996 word_lsr :: "word32 => nat => word32" where |
1159 |
997 "word_lsr == %a n. (word_lsr1 ^^ n) a" |
1160 lemma word_lsr: "ALL (a::word32) n::nat. word_lsr a n = (word_lsr1 ^^ n) a" |
998 |
|
999 lemma word_lsr: "word_lsr a n = (word_lsr1 ^^ n) a" |
1161 by (import word32 word_lsr) |
1000 by (import word32 word_lsr) |
1162 |
1001 |
1163 definition word_asr :: "word32 => nat => word32" where |
1002 definition |
1164 "word_asr == %(a::word32) n::nat. (word_asr1 ^^ n) a" |
1003 word_asr :: "word32 => nat => word32" where |
1165 |
1004 "word_asr == %a n. (word_asr1 ^^ n) a" |
1166 lemma word_asr: "ALL (a::word32) n::nat. word_asr a n = (word_asr1 ^^ n) a" |
1005 |
|
1006 lemma word_asr: "word_asr a n = (word_asr1 ^^ n) a" |
1167 by (import word32 word_asr) |
1007 by (import word32 word_asr) |
1168 |
1008 |
1169 definition word_ror :: "word32 => nat => word32" where |
1009 definition |
1170 "word_ror == %(a::word32) n::nat. (word_ror1 ^^ n) a" |
1010 word_ror :: "word32 => nat => word32" where |
1171 |
1011 "word_ror == %a n. (word_ror1 ^^ n) a" |
1172 lemma word_ror: "ALL (a::word32) n::nat. word_ror a n = (word_ror1 ^^ n) a" |
1012 |
|
1013 lemma word_ror: "word_ror a n = (word_ror1 ^^ n) a" |
1173 by (import word32 word_ror) |
1014 by (import word32 word_ror) |
1174 |
1015 |
1175 consts |
1016 consts |
1176 BITw :: "nat => word32 => bool" |
1017 BITw :: "nat => word32 => bool" |
1177 |
1018 |
1178 defs |
1019 defs |
1179 BITw_primdef: "BITw == %(b::nat) n::word32. bit b (w2n n)" |
1020 BITw_primdef: "BITw == %b n. bit b (w2n n)" |
1180 |
1021 |
1181 lemma BITw_def: "ALL (b::nat) n::word32. BITw b n = bit b (w2n n)" |
1022 lemma BITw_def: "BITw b n = bit b (w2n n)" |
1182 by (import word32 BITw_def) |
1023 by (import word32 BITw_def) |
1183 |
1024 |
1184 consts |
1025 consts |
1185 BITSw :: "nat => nat => word32 => nat" |
1026 BITSw :: "nat => nat => word32 => nat" |
1186 |
1027 |
1187 defs |
1028 defs |
1188 BITSw_primdef: "BITSw == %(h::nat) (l::nat) n::word32. BITS h l (w2n n)" |
1029 BITSw_primdef: "BITSw == %h l n. BITS h l (w2n n)" |
1189 |
1030 |
1190 lemma BITSw_def: "ALL (h::nat) (l::nat) n::word32. BITSw h l n = BITS h l (w2n n)" |
1031 lemma BITSw_def: "BITSw h l n = BITS h l (w2n n)" |
1191 by (import word32 BITSw_def) |
1032 by (import word32 BITSw_def) |
1192 |
1033 |
1193 consts |
1034 consts |
1194 SLICEw :: "nat => nat => word32 => nat" |
1035 SLICEw :: "nat => nat => word32 => nat" |
1195 |
1036 |
1196 defs |
1037 defs |
1197 SLICEw_primdef: "SLICEw == %(h::nat) (l::nat) n::word32. SLICE h l (w2n n)" |
1038 SLICEw_primdef: "SLICEw == %h l n. SLICE h l (w2n n)" |
1198 |
1039 |
1199 lemma SLICEw_def: "ALL (h::nat) (l::nat) n::word32. SLICEw h l n = SLICE h l (w2n n)" |
1040 lemma SLICEw_def: "SLICEw h l n = SLICE h l (w2n n)" |
1200 by (import word32 SLICEw_def) |
1041 by (import word32 SLICEw_def) |
1201 |
1042 |
1202 lemma TWO_COMP_ADD: "ALL (a::word32) b::word32. |
1043 lemma TWO_COMP_ADD: "word_2comp (word_add a b) = word_add (word_2comp a) (word_2comp b)" |
1203 word_2comp (word_add a b) = word_add (word_2comp a) (word_2comp b)" |
|
1204 by (import word32 TWO_COMP_ADD) |
1044 by (import word32 TWO_COMP_ADD) |
1205 |
1045 |
1206 lemma TWO_COMP_ELIM: "ALL a::word32. word_2comp (word_2comp a) = a" |
1046 lemma TWO_COMP_ELIM: "word_2comp (word_2comp a) = a" |
1207 by (import word32 TWO_COMP_ELIM) |
1047 by (import word32 TWO_COMP_ELIM) |
1208 |
1048 |
1209 lemma ADD_SUB_ASSOC: "ALL (a::word32) (b::word32) c::word32. |
1049 lemma ADD_SUB_ASSOC: "word_sub (word_add a b) c = word_add a (word_sub b c)" |
1210 word_sub (word_add a b) c = word_add a (word_sub b c)" |
|
1211 by (import word32 ADD_SUB_ASSOC) |
1050 by (import word32 ADD_SUB_ASSOC) |
1212 |
1051 |
1213 lemma ADD_SUB_SYM: "ALL (a::word32) (b::word32) c::word32. |
1052 lemma ADD_SUB_SYM: "word_sub (word_add a b) c = word_add (word_sub a c) b" |
1214 word_sub (word_add a b) c = word_add (word_sub a c) b" |
|
1215 by (import word32 ADD_SUB_SYM) |
1053 by (import word32 ADD_SUB_SYM) |
1216 |
1054 |
1217 lemma SUB_EQUALw: "ALL a::word32. word_sub a a = w_0" |
1055 lemma SUB_EQUALw: "word_sub a a = w_0" |
1218 by (import word32 SUB_EQUALw) |
1056 by (import word32 SUB_EQUALw) |
1219 |
1057 |
1220 lemma ADD_SUBw: "ALL (a::word32) b::word32. word_sub (word_add a b) b = a" |
1058 lemma ADD_SUBw: "word_sub (word_add a b) b = a" |
1221 by (import word32 ADD_SUBw) |
1059 by (import word32 ADD_SUBw) |
1222 |
1060 |
1223 lemma SUB_SUBw: "ALL (a::word32) (b::word32) c::word32. |
1061 lemma SUB_SUBw: "word_sub a (word_sub b c) = word_sub (word_add a c) b" |
1224 word_sub a (word_sub b c) = word_sub (word_add a c) b" |
|
1225 by (import word32 SUB_SUBw) |
1062 by (import word32 SUB_SUBw) |
1226 |
1063 |
1227 lemma ONE_COMP_TWO_COMP: "ALL a::word32. word_1comp a = word_sub (word_2comp a) w_1" |
1064 lemma ONE_COMP_TWO_COMP: "word_1comp a = word_sub (word_2comp a) w_1" |
1228 by (import word32 ONE_COMP_TWO_COMP) |
1065 by (import word32 ONE_COMP_TWO_COMP) |
1229 |
1066 |
1230 lemma SUBw: "ALL (m::word32) n::word32. word_sub (word_suc m) n = word_suc (word_sub m n)" |
1067 lemma SUBw: "word_sub (word_suc m) n = word_suc (word_sub m n)" |
1231 by (import word32 SUBw) |
1068 by (import word32 SUBw) |
1232 |
1069 |
1233 lemma ADD_EQ_SUBw: "ALL (m::word32) (n::word32) p::word32. |
1070 lemma ADD_EQ_SUBw: "(word_add m n = p) = (m = word_sub p n)" |
1234 (word_add m n = p) = (m = word_sub p n)" |
|
1235 by (import word32 ADD_EQ_SUBw) |
1071 by (import word32 ADD_EQ_SUBw) |
1236 |
1072 |
1237 lemma CANCEL_SUBw: "ALL (m::word32) (n::word32) p::word32. |
1073 lemma CANCEL_SUBw: "(word_sub n p = word_sub m p) = (n = m)" |
1238 (word_sub n p = word_sub m p) = (n = m)" |
|
1239 by (import word32 CANCEL_SUBw) |
1074 by (import word32 CANCEL_SUBw) |
1240 |
1075 |
1241 lemma SUB_PLUSw: "ALL (a::word32) (b::word32) c::word32. |
1076 lemma SUB_PLUSw: "word_sub a (word_add b c) = word_sub (word_sub a b) c" |
1242 word_sub a (word_add b c) = word_sub (word_sub a b) c" |
|
1243 by (import word32 SUB_PLUSw) |
1077 by (import word32 SUB_PLUSw) |
1244 |
1078 |
1245 lemma word_nchotomy: "ALL w::word32. EX n::nat. w = n2w n" |
1079 lemma word_nchotomy: "EX n. w = n2w n" |
1246 by (import word32 word_nchotomy) |
1080 by (import word32 word_nchotomy) |
1247 |
1081 |
1248 lemma dest_word_mk_word_eq3: "ALL a::nat. dest_word32 (mk_word32 (EQUIV a)) = EQUIV a" |
1082 lemma dest_word_mk_word_eq3: "dest_word32 (mk_word32 (EQUIV a)) = EQUIV a" |
1249 by (import word32 dest_word_mk_word_eq3) |
1083 by (import word32 dest_word_mk_word_eq3) |
1250 |
1084 |
1251 lemma MODw_ELIM: "ALL n::nat. n2w (MODw n) = n2w n" |
1085 lemma MODw_ELIM: "n2w (MODw n) = n2w n" |
1252 by (import word32 MODw_ELIM) |
1086 by (import word32 MODw_ELIM) |
1253 |
1087 |
1254 lemma w2n_EVAL: "ALL n::nat. w2n (n2w n) = MODw n" |
1088 lemma w2n_EVAL: "w2n (n2w n) = MODw n" |
1255 by (import word32 w2n_EVAL) |
1089 by (import word32 w2n_EVAL) |
1256 |
1090 |
1257 lemma w2n_ELIM: "ALL a::word32. n2w (w2n a) = a" |
1091 lemma w2n_ELIM: "n2w (w2n a) = a" |
1258 by (import word32 w2n_ELIM) |
1092 by (import word32 w2n_ELIM) |
1259 |
1093 |
1260 lemma n2w_11: "ALL (a::nat) b::nat. (n2w a = n2w b) = (MODw a = MODw b)" |
1094 lemma n2w_11: "(n2w a = n2w b) = (MODw a = MODw b)" |
1261 by (import word32 n2w_11) |
1095 by (import word32 n2w_11) |
1262 |
1096 |
1263 lemma ADD_EVAL: "word_add (n2w (a::nat)) (n2w (b::nat)) = n2w (a + b)" |
1097 lemma ADD_EVAL: "word_add (n2w a) (n2w b) = n2w (a + b)" |
1264 by (import word32 ADD_EVAL) |
1098 by (import word32 ADD_EVAL) |
1265 |
1099 |
1266 lemma MUL_EVAL: "word_mul (n2w (a::nat)) (n2w (b::nat)) = n2w (a * b)" |
1100 lemma MUL_EVAL: "word_mul (n2w a) (n2w b) = n2w (a * b)" |
1267 by (import word32 MUL_EVAL) |
1101 by (import word32 MUL_EVAL) |
1268 |
1102 |
1269 lemma ONE_COMP_EVAL: "word_1comp (n2w (a::nat)) = n2w (ONE_COMP a)" |
1103 lemma ONE_COMP_EVAL: "word_1comp (n2w a) = n2w (ONE_COMP a)" |
1270 by (import word32 ONE_COMP_EVAL) |
1104 by (import word32 ONE_COMP_EVAL) |
1271 |
1105 |
1272 lemma TWO_COMP_EVAL: "word_2comp (n2w (a::nat)) = n2w (TWO_COMP a)" |
1106 lemma TWO_COMP_EVAL: "word_2comp (n2w a) = n2w (TWO_COMP a)" |
1273 by (import word32 TWO_COMP_EVAL) |
1107 by (import word32 TWO_COMP_EVAL) |
1274 |
1108 |
1275 lemma LSR_ONE_EVAL: "word_lsr1 (n2w (a::nat)) = n2w (LSR_ONE a)" |
1109 lemma LSR_ONE_EVAL: "word_lsr1 (n2w a) = n2w (LSR_ONE a)" |
1276 by (import word32 LSR_ONE_EVAL) |
1110 by (import word32 LSR_ONE_EVAL) |
1277 |
1111 |
1278 lemma ASR_ONE_EVAL: "word_asr1 (n2w (a::nat)) = n2w (ASR_ONE a)" |
1112 lemma ASR_ONE_EVAL: "word_asr1 (n2w a) = n2w (ASR_ONE a)" |
1279 by (import word32 ASR_ONE_EVAL) |
1113 by (import word32 ASR_ONE_EVAL) |
1280 |
1114 |
1281 lemma ROR_ONE_EVAL: "word_ror1 (n2w (a::nat)) = n2w (ROR_ONE a)" |
1115 lemma ROR_ONE_EVAL: "word_ror1 (n2w a) = n2w (ROR_ONE a)" |
1282 by (import word32 ROR_ONE_EVAL) |
1116 by (import word32 ROR_ONE_EVAL) |
1283 |
1117 |
1284 lemma RRX_EVAL: "RRX (c::bool) (n2w (a::nat)) = n2w (RRXn c a)" |
1118 lemma RRX_EVAL: "RRX c (n2w a) = n2w (RRXn c a)" |
1285 by (import word32 RRX_EVAL) |
1119 by (import word32 RRX_EVAL) |
1286 |
1120 |
1287 lemma LSB_EVAL: "LSB (n2w (a::nat)) = LSBn a" |
1121 lemma LSB_EVAL: "LSB (n2w a) = LSBn a" |
1288 by (import word32 LSB_EVAL) |
1122 by (import word32 LSB_EVAL) |
1289 |
1123 |
1290 lemma MSB_EVAL: "MSB (n2w (a::nat)) = MSBn a" |
1124 lemma MSB_EVAL: "MSB (n2w a) = MSBn a" |
1291 by (import word32 MSB_EVAL) |
1125 by (import word32 MSB_EVAL) |
1292 |
1126 |
1293 lemma OR_EVAL: "bitwise_or (n2w (a::nat)) (n2w (b::nat)) = n2w (OR a b)" |
1127 lemma OR_EVAL: "bitwise_or (n2w a) (n2w b) = n2w (OR a b)" |
1294 by (import word32 OR_EVAL) |
1128 by (import word32 OR_EVAL) |
1295 |
1129 |
1296 lemma EOR_EVAL: "bitwise_eor (n2w (a::nat)) (n2w (b::nat)) = n2w (EOR a b)" |
1130 lemma EOR_EVAL: "bitwise_eor (n2w a) (n2w b) = n2w (EOR a b)" |
1297 by (import word32 EOR_EVAL) |
1131 by (import word32 EOR_EVAL) |
1298 |
1132 |
1299 lemma AND_EVAL: "bitwise_and (n2w (a::nat)) (n2w (b::nat)) = n2w (AND a b)" |
1133 lemma AND_EVAL: "bitwise_and (n2w a) (n2w b) = n2w (AND a b)" |
1300 by (import word32 AND_EVAL) |
1134 by (import word32 AND_EVAL) |
1301 |
1135 |
1302 lemma BITS_EVAL: "ALL (h::nat) (l::nat) a::nat. BITSw h l (n2w a) = BITS h l (MODw a)" |
1136 lemma BITS_EVAL: "BITSw h l (n2w a) = BITS h l (MODw a)" |
1303 by (import word32 BITS_EVAL) |
1137 by (import word32 BITS_EVAL) |
1304 |
1138 |
1305 lemma BIT_EVAL: "ALL (b::nat) a::nat. BITw b (n2w a) = bit b (MODw a)" |
1139 lemma BIT_EVAL: "BITw b (n2w a) = bit b (MODw a)" |
1306 by (import word32 BIT_EVAL) |
1140 by (import word32 BIT_EVAL) |
1307 |
1141 |
1308 lemma SLICE_EVAL: "ALL (h::nat) (l::nat) a::nat. SLICEw h l (n2w a) = SLICE h l (MODw a)" |
1142 lemma SLICE_EVAL: "SLICEw h l (n2w a) = SLICE h l (MODw a)" |
1309 by (import word32 SLICE_EVAL) |
1143 by (import word32 SLICE_EVAL) |
1310 |
1144 |
1311 lemma LSL_ADD: "ALL (a::word32) (m::nat) n::nat. |
1145 lemma LSL_ADD: "word_lsl (word_lsl a m) n = word_lsl a (m + n)" |
1312 word_lsl (word_lsl a m) n = word_lsl a (m + n)" |
|
1313 by (import word32 LSL_ADD) |
1146 by (import word32 LSL_ADD) |
1314 |
1147 |
1315 lemma LSR_ADD: "ALL (x::word32) (xa::nat) xb::nat. |
1148 lemma LSR_ADD: "word_lsr (word_lsr x xa) xb = word_lsr x (xa + xb)" |
1316 word_lsr (word_lsr x xa) xb = word_lsr x (xa + xb)" |
|
1317 by (import word32 LSR_ADD) |
1149 by (import word32 LSR_ADD) |
1318 |
1150 |
1319 lemma ASR_ADD: "ALL (x::word32) (xa::nat) xb::nat. |
1151 lemma ASR_ADD: "word_asr (word_asr x xa) xb = word_asr x (xa + xb)" |
1320 word_asr (word_asr x xa) xb = word_asr x (xa + xb)" |
|
1321 by (import word32 ASR_ADD) |
1152 by (import word32 ASR_ADD) |
1322 |
1153 |
1323 lemma ROR_ADD: "ALL (x::word32) (xa::nat) xb::nat. |
1154 lemma ROR_ADD: "word_ror (word_ror x xa) xb = word_ror x (xa + xb)" |
1324 word_ror (word_ror x xa) xb = word_ror x (xa + xb)" |
|
1325 by (import word32 ROR_ADD) |
1155 by (import word32 ROR_ADD) |
1326 |
1156 |
1327 lemma LSL_LIMIT: "ALL (w::word32) n::nat. HB < n --> word_lsl w n = w_0" |
1157 lemma LSL_LIMIT: "HB < n ==> word_lsl w n = w_0" |
1328 by (import word32 LSL_LIMIT) |
1158 by (import word32 LSL_LIMIT) |
1329 |
1159 |
1330 lemma MOD_MOD_DIV: "ALL (a::nat) b::nat. INw (MODw a div 2 ^ b)" |
1160 lemma MOD_MOD_DIV: "INw (MODw a div 2 ^ b)" |
1331 by (import word32 MOD_MOD_DIV) |
1161 by (import word32 MOD_MOD_DIV) |
1332 |
1162 |
1333 lemma MOD_MOD_DIV_2EXP: "ALL (a::nat) n::nat. MODw (MODw a div 2 ^ n) div 2 = MODw a div 2 ^ Suc n" |
1163 lemma MOD_MOD_DIV_2EXP: "MODw (MODw a div 2 ^ n) div 2 = MODw a div 2 ^ Suc n" |
1334 by (import word32 MOD_MOD_DIV_2EXP) |
1164 by (import word32 MOD_MOD_DIV_2EXP) |
1335 |
1165 |
1336 lemma LSR_EVAL: "ALL n::nat. word_lsr (n2w (a::nat)) n = n2w (MODw a div 2 ^ n)" |
1166 lemma LSR_EVAL: "word_lsr (n2w a) n = n2w (MODw a div 2 ^ n)" |
1337 by (import word32 LSR_EVAL) |
1167 by (import word32 LSR_EVAL) |
1338 |
1168 |
1339 lemma LSR_THM: "ALL (x::nat) n::nat. word_lsr (n2w n) x = n2w (BITS HB (min WL x) n)" |
1169 lemma LSR_THM: "word_lsr (n2w n) x = n2w (BITS HB (min WL x) n)" |
1340 by (import word32 LSR_THM) |
1170 by (import word32 LSR_THM) |
1341 |
1171 |
1342 lemma LSR_LIMIT: "ALL (x::nat) w::word32. HB < x --> word_lsr w x = w_0" |
1172 lemma LSR_LIMIT: "HB < x ==> word_lsr w x = w_0" |
1343 by (import word32 LSR_LIMIT) |
1173 by (import word32 LSR_LIMIT) |
1344 |
1174 |
1345 lemma LEFT_SHIFT_LESS: "ALL (n::nat) (m::nat) a::nat. a < 2 ^ m --> 2 ^ n + a * 2 ^ n <= 2 ^ (m + n)" |
1175 lemma LEFT_SHIFT_LESS: "(a::nat) < (2::nat) ^ (m::nat) |
|
1176 ==> (2::nat) ^ (n::nat) + a * (2::nat) ^ n <= (2::nat) ^ (m + n)" |
1346 by (import word32 LEFT_SHIFT_LESS) |
1177 by (import word32 LEFT_SHIFT_LESS) |
1347 |
1178 |
1348 lemma ROR_THM: "ALL (x::nat) n::nat. |
1179 lemma ROR_THM: "word_ror (n2w n) x = |
1349 word_ror (n2w n) x = |
1180 (let x' = x mod WL |
1350 (let x'::nat = x mod WL |
1181 in n2w (BITS HB x' n + BITS (x' - 1) 0 n * 2 ^ (WL - x')))" |
1351 in n2w (BITS HB x' n + BITS (x' - 1) 0 n * 2 ^ (WL - x')))" |
|
1352 by (import word32 ROR_THM) |
1182 by (import word32 ROR_THM) |
1353 |
1183 |
1354 lemma ROR_CYCLE: "ALL (x::nat) w::word32. word_ror w (x * WL) = w" |
1184 lemma ROR_CYCLE: "word_ror w (x * WL) = w" |
1355 by (import word32 ROR_CYCLE) |
1185 by (import word32 ROR_CYCLE) |
1356 |
1186 |
1357 lemma ASR_THM: "ALL (x::nat) n::nat. |
1187 lemma ASR_THM: "word_asr (n2w n) x = |
1358 word_asr (n2w n) x = |
1188 (let x' = min HB x; s = BITS HB x' n |
1359 (let x'::nat = min HB x; s::nat = BITS HB x' n |
1189 in n2w (if MSBn n then 2 ^ WL - 2 ^ (WL - x') + s else s))" |
1360 in n2w (if MSBn n then 2 ^ WL - 2 ^ (WL - x') + s else s))" |
|
1361 by (import word32 ASR_THM) |
1190 by (import word32 ASR_THM) |
1362 |
1191 |
1363 lemma ASR_LIMIT: "ALL (x::nat) w::word32. |
1192 lemma ASR_LIMIT: "HB <= x ==> word_asr w x = (if MSB w then w_T else w_0)" |
1364 HB <= x --> word_asr w x = (if MSB w then w_T else w_0)" |
|
1365 by (import word32 ASR_LIMIT) |
1193 by (import word32 ASR_LIMIT) |
1366 |
1194 |
1367 lemma ZERO_SHIFT: "(ALL n::nat. word_lsl w_0 n = w_0) & |
1195 lemma ZERO_SHIFT: "(ALL n. word_lsl w_0 n = w_0) & |
1368 (ALL n::nat. word_asr w_0 n = w_0) & |
1196 (ALL n. word_asr w_0 n = w_0) & |
1369 (ALL n::nat. word_lsr w_0 n = w_0) & (ALL n::nat. word_ror w_0 n = w_0)" |
1197 (ALL n. word_lsr w_0 n = w_0) & (ALL n. word_ror w_0 n = w_0)" |
1370 by (import word32 ZERO_SHIFT) |
1198 by (import word32 ZERO_SHIFT) |
1371 |
1199 |
1372 lemma ZERO_SHIFT2: "(ALL a::word32. word_lsl a 0 = a) & |
1200 lemma ZERO_SHIFT2: "(ALL a. word_lsl a 0 = a) & |
1373 (ALL a::word32. word_asr a 0 = a) & |
1201 (ALL a. word_asr a 0 = a) & |
1374 (ALL a::word32. word_lsr a 0 = a) & (ALL a::word32. word_ror a 0 = a)" |
1202 (ALL a. word_lsr a 0 = a) & (ALL a. word_ror a 0 = a)" |
1375 by (import word32 ZERO_SHIFT2) |
1203 by (import word32 ZERO_SHIFT2) |
1376 |
1204 |
1377 lemma ASR_w_T: "ALL n::nat. word_asr w_T n = w_T" |
1205 lemma ASR_w_T: "word_asr w_T n = w_T" |
1378 by (import word32 ASR_w_T) |
1206 by (import word32 ASR_w_T) |
1379 |
1207 |
1380 lemma ROR_w_T: "ALL n::nat. word_ror w_T n = w_T" |
1208 lemma ROR_w_T: "word_ror w_T n = w_T" |
1381 by (import word32 ROR_w_T) |
1209 by (import word32 ROR_w_T) |
1382 |
1210 |
1383 lemma MODw_EVAL: "ALL x::nat. |
1211 lemma MODw_EVAL: "MODw x = |
1384 MODw x = |
1212 x mod |
1385 x mod |
1213 NUMERAL |
1386 NUMERAL |
1214 (NUMERAL_BIT2 |
1387 (NUMERAL_BIT2 |
1215 (NUMERAL_BIT1 |
|
1216 (NUMERAL_BIT1 |
|
1217 (NUMERAL_BIT1 |
|
1218 (NUMERAL_BIT1 |
|
1219 (NUMERAL_BIT1 |
|
1220 (NUMERAL_BIT1 |
|
1221 (NUMERAL_BIT1 |
|
1222 (NUMERAL_BIT1 |
|
1223 (NUMERAL_BIT1 |
|
1224 (NUMERAL_BIT1 |
|
1225 (NUMERAL_BIT1 |
|
1226 (NUMERAL_BIT1 |
|
1227 (NUMERAL_BIT1 |
|
1228 (NUMERAL_BIT1 |
|
1229 (NUMERAL_BIT1 |
|
1230 (NUMERAL_BIT1 |
|
1231 (NUMERAL_BIT1 |
|
1232 (NUMERAL_BIT1 |
|
1233 (NUMERAL_BIT1 |
|
1234 (NUMERAL_BIT1 |
|
1235 (NUMERAL_BIT1 |
|
1236 (NUMERAL_BIT1 |
|
1237 (NUMERAL_BIT1 |
|
1238 (NUMERAL_BIT1 |
|
1239 (NUMERAL_BIT1 |
|
1240 (NUMERAL_BIT1 |
|
1241 (NUMERAL_BIT1 |
|
1242 (NUMERAL_BIT1 |
|
1243 (NUMERAL_BIT1 |
|
1244 (NUMERAL_BIT1 |
|
1245 (NUMERAL_BIT1 |
|
1246 ALT_ZERO))))))))))))))))))))))))))))))))" |
|
1247 by (import word32 MODw_EVAL) |
|
1248 |
|
1249 lemma ADD_EVAL2: "word_add (n2w a) (n2w b) = n2w (MODw (a + b))" |
|
1250 by (import word32 ADD_EVAL2) |
|
1251 |
|
1252 lemma MUL_EVAL2: "word_mul (n2w a) (n2w b) = n2w (MODw (a * b))" |
|
1253 by (import word32 MUL_EVAL2) |
|
1254 |
|
1255 lemma ONE_COMP_EVAL2: "word_1comp (n2w a) = |
|
1256 n2w (2 ^ |
|
1257 NUMERAL |
|
1258 (NUMERAL_BIT2 |
|
1259 (NUMERAL_BIT1 |
|
1260 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO))))) - |
|
1261 1 - |
|
1262 MODw a)" |
|
1263 by (import word32 ONE_COMP_EVAL2) |
|
1264 |
|
1265 lemma TWO_COMP_EVAL2: "word_2comp (n2w a) = |
|
1266 n2w (MODw |
|
1267 (2 ^ |
|
1268 NUMERAL |
|
1269 (NUMERAL_BIT2 |
|
1270 (NUMERAL_BIT1 |
|
1271 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO))))) - |
|
1272 MODw a))" |
|
1273 by (import word32 TWO_COMP_EVAL2) |
|
1274 |
|
1275 lemma LSR_ONE_EVAL2: "word_lsr1 (n2w a) = n2w (MODw a div 2)" |
|
1276 by (import word32 LSR_ONE_EVAL2) |
|
1277 |
|
1278 lemma ASR_ONE_EVAL2: "word_asr1 (n2w a) = |
|
1279 n2w (MODw a div 2 + |
|
1280 SBIT (MSBn a) |
|
1281 (NUMERAL |
|
1282 (NUMERAL_BIT1 |
|
1283 (NUMERAL_BIT1 |
|
1284 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))))" |
|
1285 by (import word32 ASR_ONE_EVAL2) |
|
1286 |
|
1287 lemma ROR_ONE_EVAL2: "word_ror1 (n2w a) = |
|
1288 n2w (MODw a div 2 + |
|
1289 SBIT (LSBn a) |
|
1290 (NUMERAL |
|
1291 (NUMERAL_BIT1 |
|
1292 (NUMERAL_BIT1 |
|
1293 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))))" |
|
1294 by (import word32 ROR_ONE_EVAL2) |
|
1295 |
|
1296 lemma RRX_EVAL2: "RRX c (n2w a) = |
|
1297 n2w (MODw a div 2 + |
|
1298 SBIT c |
|
1299 (NUMERAL |
|
1300 (NUMERAL_BIT1 |
|
1301 (NUMERAL_BIT1 |
|
1302 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))))" |
|
1303 by (import word32 RRX_EVAL2) |
|
1304 |
|
1305 lemma LSB_EVAL2: "LSB (n2w a) = ODD a" |
|
1306 by (import word32 LSB_EVAL2) |
|
1307 |
|
1308 lemma MSB_EVAL2: "MSB (n2w a) = |
|
1309 bit (NUMERAL |
1388 (NUMERAL_BIT1 |
1310 (NUMERAL_BIT1 |
1389 (NUMERAL_BIT1 |
1311 (NUMERAL_BIT1 |
|
1312 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))) |
|
1313 a" |
|
1314 by (import word32 MSB_EVAL2) |
|
1315 |
|
1316 lemma OR_EVAL2: "bitwise_or (n2w a) (n2w b) = |
|
1317 n2w (BITWISE |
|
1318 (NUMERAL |
|
1319 (NUMERAL_BIT2 |
1390 (NUMERAL_BIT1 |
1320 (NUMERAL_BIT1 |
1391 (NUMERAL_BIT1 |
1321 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))) |
1392 (NUMERAL_BIT1 |
1322 op | a b)" |
1393 (NUMERAL_BIT1 |
1323 by (import word32 OR_EVAL2) |
1394 (NUMERAL_BIT1 |
1324 |
1395 (NUMERAL_BIT1 |
1325 lemma AND_EVAL2: "bitwise_and (n2w a) (n2w b) = |
1396 (NUMERAL_BIT1 |
1326 n2w (BITWISE |
1397 (NUMERAL_BIT1 |
1327 (NUMERAL |
1398 (NUMERAL_BIT1 |
1328 (NUMERAL_BIT2 |
1399 (NUMERAL_BIT1 |
|
1400 (NUMERAL_BIT1 |
|
1401 (NUMERAL_BIT1 |
|
1402 (NUMERAL_BIT1 |
|
1403 (NUMERAL_BIT1 |
|
1404 (NUMERAL_BIT1 |
|
1405 (NUMERAL_BIT1 |
|
1406 (NUMERAL_BIT1 |
|
1407 (NUMERAL_BIT1 |
|
1408 (NUMERAL_BIT1 |
|
1409 (NUMERAL_BIT1 |
1329 (NUMERAL_BIT1 |
1410 (NUMERAL_BIT1 |
1330 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))) |
1411 (NUMERAL_BIT1 |
1331 op & a b)" |
1412 (NUMERAL_BIT1 |
|
1413 (NUMERAL_BIT1 |
|
1414 (NUMERAL_BIT1 |
|
1415 (NUMERAL_BIT1 |
|
1416 (NUMERAL_BIT1 |
|
1417 (NUMERAL_BIT1 |
|
1418 (NUMERAL_BIT1 |
|
1419 ALT_ZERO))))))))))))))))))))))))))))))))" |
|
1420 by (import word32 MODw_EVAL) |
|
1421 |
|
1422 lemma ADD_EVAL2: "ALL (b::nat) a::nat. word_add (n2w a) (n2w b) = n2w (MODw (a + b))" |
|
1423 by (import word32 ADD_EVAL2) |
|
1424 |
|
1425 lemma MUL_EVAL2: "ALL (b::nat) a::nat. word_mul (n2w a) (n2w b) = n2w (MODw (a * b))" |
|
1426 by (import word32 MUL_EVAL2) |
|
1427 |
|
1428 lemma ONE_COMP_EVAL2: "ALL a::nat. |
|
1429 word_1comp (n2w a) = |
|
1430 n2w (2 ^ |
|
1431 NUMERAL |
|
1432 (NUMERAL_BIT2 |
|
1433 (NUMERAL_BIT1 |
|
1434 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO))))) - |
|
1435 1 - |
|
1436 MODw a)" |
|
1437 by (import word32 ONE_COMP_EVAL2) |
|
1438 |
|
1439 lemma TWO_COMP_EVAL2: "ALL a::nat. |
|
1440 word_2comp (n2w a) = |
|
1441 n2w (MODw |
|
1442 (2 ^ |
|
1443 NUMERAL |
|
1444 (NUMERAL_BIT2 |
|
1445 (NUMERAL_BIT1 |
|
1446 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO))))) - |
|
1447 MODw a))" |
|
1448 by (import word32 TWO_COMP_EVAL2) |
|
1449 |
|
1450 lemma LSR_ONE_EVAL2: "ALL a::nat. word_lsr1 (n2w a) = n2w (MODw a div 2)" |
|
1451 by (import word32 LSR_ONE_EVAL2) |
|
1452 |
|
1453 lemma ASR_ONE_EVAL2: "ALL a::nat. |
|
1454 word_asr1 (n2w a) = |
|
1455 n2w (MODw a div 2 + |
|
1456 SBIT (MSBn a) |
|
1457 (NUMERAL |
|
1458 (NUMERAL_BIT1 |
|
1459 (NUMERAL_BIT1 |
|
1460 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))))" |
|
1461 by (import word32 ASR_ONE_EVAL2) |
|
1462 |
|
1463 lemma ROR_ONE_EVAL2: "ALL a::nat. |
|
1464 word_ror1 (n2w a) = |
|
1465 n2w (MODw a div 2 + |
|
1466 SBIT (LSBn a) |
|
1467 (NUMERAL |
|
1468 (NUMERAL_BIT1 |
|
1469 (NUMERAL_BIT1 |
|
1470 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))))" |
|
1471 by (import word32 ROR_ONE_EVAL2) |
|
1472 |
|
1473 lemma RRX_EVAL2: "ALL (c::bool) a::nat. |
|
1474 RRX c (n2w a) = |
|
1475 n2w (MODw a div 2 + |
|
1476 SBIT c |
|
1477 (NUMERAL |
|
1478 (NUMERAL_BIT1 |
|
1479 (NUMERAL_BIT1 |
|
1480 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))))" |
|
1481 by (import word32 RRX_EVAL2) |
|
1482 |
|
1483 lemma LSB_EVAL2: "ALL a::nat. LSB (n2w a) = ODD a" |
|
1484 by (import word32 LSB_EVAL2) |
|
1485 |
|
1486 lemma MSB_EVAL2: "ALL a::nat. |
|
1487 MSB (n2w a) = |
|
1488 bit (NUMERAL |
|
1489 (NUMERAL_BIT1 |
|
1490 (NUMERAL_BIT1 |
|
1491 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))) |
|
1492 a" |
|
1493 by (import word32 MSB_EVAL2) |
|
1494 |
|
1495 lemma OR_EVAL2: "ALL (b::nat) a::nat. |
|
1496 bitwise_or (n2w a) (n2w b) = |
|
1497 n2w (BITWISE |
|
1498 (NUMERAL |
|
1499 (NUMERAL_BIT2 |
|
1500 (NUMERAL_BIT1 |
|
1501 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))) |
|
1502 op | a b)" |
|
1503 by (import word32 OR_EVAL2) |
|
1504 |
|
1505 lemma AND_EVAL2: "ALL (b::nat) a::nat. |
|
1506 bitwise_and (n2w a) (n2w b) = |
|
1507 n2w (BITWISE |
|
1508 (NUMERAL |
|
1509 (NUMERAL_BIT2 |
|
1510 (NUMERAL_BIT1 |
|
1511 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))) |
|
1512 op & a b)" |
|
1513 by (import word32 AND_EVAL2) |
1332 by (import word32 AND_EVAL2) |
1514 |
1333 |
1515 lemma EOR_EVAL2: "ALL (b::nat) a::nat. |
1334 lemma EOR_EVAL2: "bitwise_eor (n2w a) (n2w b) = |
1516 bitwise_eor (n2w a) (n2w b) = |
1335 n2w (BITWISE |
1517 n2w (BITWISE |
1336 (NUMERAL |
1518 (NUMERAL |
1337 (NUMERAL_BIT2 |
1519 (NUMERAL_BIT2 |
1338 (NUMERAL_BIT1 |
1520 (NUMERAL_BIT1 |
1339 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))) |
1521 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))) |
1340 op ~= a b)" |
1522 (%(x::bool) y::bool. x ~= y) a b)" |
|
1523 by (import word32 EOR_EVAL2) |
1341 by (import word32 EOR_EVAL2) |
1524 |
1342 |
1525 lemma BITWISE_EVAL2: "ALL (n::nat) (oper::bool => bool => bool) (x::nat) y::nat. |
1343 lemma BITWISE_EVAL2: "BITWISE n oper x y = |
1526 BITWISE n oper x y = |
1344 (if n = 0 then 0 |
1527 (if n = 0 then 0 |
1345 else 2 * BITWISE (n - 1) oper (x div 2) (y div 2) + |
1528 else 2 * BITWISE (n - 1) oper (x div 2) (y div 2) + |
1346 (if oper (ODD x) (ODD y) then 1 else 0))" |
1529 (if oper (ODD x) (ODD y) then 1 else 0))" |
|
1530 by (import word32 BITWISE_EVAL2) |
1347 by (import word32 BITWISE_EVAL2) |
1531 |
1348 |
1532 lemma BITSwLT_THM: "ALL (h::nat) (l::nat) n::word32. BITSw h l n < 2 ^ (Suc h - l)" |
1349 lemma BITSwLT_THM: "BITSw h l n < 2 ^ (Suc h - l)" |
1533 by (import word32 BITSwLT_THM) |
1350 by (import word32 BITSwLT_THM) |
1534 |
1351 |
1535 lemma BITSw_COMP_THM: "ALL (h1::nat) (l1::nat) (h2::nat) (l2::nat) n::word32. |
1352 lemma BITSw_COMP_THM: "h2 + l1 <= h1 ==> BITS h2 l2 (BITSw h1 l1 n) = BITSw (h2 + l1) (l2 + l1) n" |
1536 h2 + l1 <= h1 --> |
|
1537 BITS h2 l2 (BITSw h1 l1 n) = BITSw (h2 + l1) (l2 + l1) n" |
|
1538 by (import word32 BITSw_COMP_THM) |
1353 by (import word32 BITSw_COMP_THM) |
1539 |
1354 |
1540 lemma BITSw_DIV_THM: "ALL (h::nat) (l::nat) (n::nat) x::word32. |
1355 lemma BITSw_DIV_THM: "BITSw h l x div 2 ^ n = BITSw h (l + n) x" |
1541 BITSw h l x div 2 ^ n = BITSw h (l + n) x" |
|
1542 by (import word32 BITSw_DIV_THM) |
1356 by (import word32 BITSw_DIV_THM) |
1543 |
1357 |
1544 lemma BITw_THM: "ALL (b::nat) n::word32. BITw b n = (BITSw b b n = 1)" |
1358 lemma BITw_THM: "BITw b n = (BITSw b b n = 1)" |
1545 by (import word32 BITw_THM) |
1359 by (import word32 BITw_THM) |
1546 |
1360 |
1547 lemma SLICEw_THM: "ALL (n::word32) (h::nat) l::nat. SLICEw h l n = BITSw h l n * 2 ^ l" |
1361 lemma SLICEw_THM: "SLICEw h l n = BITSw h l n * 2 ^ l" |
1548 by (import word32 SLICEw_THM) |
1362 by (import word32 SLICEw_THM) |
1549 |
1363 |
1550 lemma BITS_SLICEw_THM: "ALL (h::nat) (l::nat) n::word32. BITS h l (SLICEw h l n) = BITSw h l n" |
1364 lemma BITS_SLICEw_THM: "BITS h l (SLICEw h l n) = BITSw h l n" |
1551 by (import word32 BITS_SLICEw_THM) |
1365 by (import word32 BITS_SLICEw_THM) |
1552 |
1366 |
1553 lemma SLICEw_ZERO_THM: "ALL (n::word32) h::nat. SLICEw h 0 n = BITSw h 0 n" |
1367 lemma SLICEw_ZERO_THM: "SLICEw h 0 n = BITSw h 0 n" |
1554 by (import word32 SLICEw_ZERO_THM) |
1368 by (import word32 SLICEw_ZERO_THM) |
1555 |
1369 |
1556 lemma SLICEw_COMP_THM: "ALL (h::nat) (m::nat) (l::nat) a::word32. |
1370 lemma SLICEw_COMP_THM: "Suc m <= h & l <= m ==> SLICEw h (Suc m) a + SLICEw m l a = SLICEw h l a" |
1557 Suc m <= h & l <= m --> SLICEw h (Suc m) a + SLICEw m l a = SLICEw h l a" |
|
1558 by (import word32 SLICEw_COMP_THM) |
1371 by (import word32 SLICEw_COMP_THM) |
1559 |
1372 |
1560 lemma BITSw_ZERO: "ALL (h::nat) (l::nat) n::word32. h < l --> BITSw h l n = 0" |
1373 lemma BITSw_ZERO: "h < l ==> BITSw h l n = 0" |
1561 by (import word32 BITSw_ZERO) |
1374 by (import word32 BITSw_ZERO) |
1562 |
1375 |
1563 lemma SLICEw_ZERO: "ALL (h::nat) (l::nat) n::word32. h < l --> SLICEw h l n = 0" |
1376 lemma SLICEw_ZERO: "h < l ==> SLICEw h l n = 0" |
1564 by (import word32 SLICEw_ZERO) |
1377 by (import word32 SLICEw_ZERO) |
1565 |
1378 |
1566 ;end_setup |
1379 ;end_setup |
1567 |
1380 |
1568 end |
1381 end |
|
1382 |