|
1 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *) |
|
2 |
|
3 theory HOL4Word32 imports HOL4Base begin |
|
4 |
|
5 setup_theory "~~/src/HOL/Import/HOL4/Generated" bits |
|
6 |
|
7 consts |
|
8 DIV2 :: "nat => nat" |
|
9 |
|
10 defs |
|
11 DIV2_primdef: "DIV2 == %n. n div 2" |
|
12 |
|
13 lemma DIV2_def: "DIV2 n = n div 2" |
|
14 by (import bits DIV2_def) |
|
15 |
|
16 consts |
|
17 TIMES_2EXP :: "nat => nat => nat" |
|
18 |
|
19 defs |
|
20 TIMES_2EXP_primdef: "TIMES_2EXP == %x n. n * 2 ^ x" |
|
21 |
|
22 lemma TIMES_2EXP_def: "TIMES_2EXP x n = n * 2 ^ x" |
|
23 by (import bits TIMES_2EXP_def) |
|
24 |
|
25 consts |
|
26 DIV_2EXP :: "nat => nat => nat" |
|
27 |
|
28 defs |
|
29 DIV_2EXP_primdef: "DIV_2EXP == %x n. n div 2 ^ x" |
|
30 |
|
31 lemma DIV_2EXP_def: "DIV_2EXP x n = n div 2 ^ x" |
|
32 by (import bits DIV_2EXP_def) |
|
33 |
|
34 consts |
|
35 MOD_2EXP :: "nat => nat => nat" |
|
36 |
|
37 defs |
|
38 MOD_2EXP_primdef: "MOD_2EXP == %x n. n mod 2 ^ x" |
|
39 |
|
40 lemma MOD_2EXP_def: "MOD_2EXP x n = n mod 2 ^ x" |
|
41 by (import bits MOD_2EXP_def) |
|
42 |
|
43 consts |
|
44 DIVMOD_2EXP :: "nat => nat => nat * nat" |
|
45 |
|
46 defs |
|
47 DIVMOD_2EXP_primdef: "DIVMOD_2EXP == %x n. (n div 2 ^ x, n mod 2 ^ x)" |
|
48 |
|
49 lemma DIVMOD_2EXP_def: "DIVMOD_2EXP x n = (n div 2 ^ x, n mod 2 ^ x)" |
|
50 by (import bits DIVMOD_2EXP_def) |
|
51 |
|
52 consts |
|
53 SBIT :: "bool => nat => nat" |
|
54 |
|
55 defs |
|
56 SBIT_primdef: "SBIT == %b n. if b then 2 ^ n else 0" |
|
57 |
|
58 lemma SBIT_def: "SBIT b n = (if b then 2 ^ n else 0)" |
|
59 by (import bits SBIT_def) |
|
60 |
|
61 consts |
|
62 BITS :: "nat => nat => nat => nat" |
|
63 |
|
64 defs |
|
65 BITS_primdef: "BITS == %h l n. MOD_2EXP (Suc h - l) (DIV_2EXP l n)" |
|
66 |
|
67 lemma BITS_def: "BITS h l n = MOD_2EXP (Suc h - l) (DIV_2EXP l n)" |
|
68 by (import bits BITS_def) |
|
69 |
|
70 definition |
|
71 bit :: "nat => nat => bool" where |
|
72 "bit == %b n. BITS b b n = 1" |
|
73 |
|
74 lemma BIT_def: "bit b n = (BITS b b n = 1)" |
|
75 by (import bits BIT_def) |
|
76 |
|
77 consts |
|
78 SLICE :: "nat => nat => nat => nat" |
|
79 |
|
80 defs |
|
81 SLICE_primdef: "SLICE == %h l n. MOD_2EXP (Suc h) n - MOD_2EXP l n" |
|
82 |
|
83 lemma SLICE_def: "SLICE h l n = MOD_2EXP (Suc h) n - MOD_2EXP l n" |
|
84 by (import bits SLICE_def) |
|
85 |
|
86 consts |
|
87 LSBn :: "nat => bool" |
|
88 |
|
89 defs |
|
90 LSBn_primdef: "LSBn == bit 0" |
|
91 |
|
92 lemma LSBn_def: "LSBn = bit 0" |
|
93 by (import bits LSBn_def) |
|
94 |
|
95 consts |
|
96 BITWISE :: "nat => (bool => bool => bool) => nat => nat => nat" |
|
97 |
|
98 specification (BITWISE_primdef: BITWISE) BITWISE_def: "(ALL oper x y. BITWISE 0 oper x y = 0) & |
|
99 (ALL n oper x y. |
|
100 BITWISE (Suc n) oper x y = |
|
101 BITWISE n oper x y + SBIT (oper (bit n x) (bit n y)) n)" |
|
102 by (import bits BITWISE_def) |
|
103 |
|
104 lemma SUC_SUB: "Suc a - a = 1" |
|
105 by (import bits SUC_SUB) |
|
106 |
|
107 lemma DIV_MULT_1: "(r::nat) < (n::nat) ==> (n + r) div n = (1::nat)" |
|
108 by (import bits DIV_MULT_1) |
|
109 |
|
110 lemma ZERO_LT_TWOEXP: "(0::nat) < (2::nat) ^ (n::nat)" |
|
111 by (import bits ZERO_LT_TWOEXP) |
|
112 |
|
113 lemma MOD_2EXP_LT: "(k::nat) mod (2::nat) ^ (n::nat) < (2::nat) ^ n" |
|
114 by (import bits MOD_2EXP_LT) |
|
115 |
|
116 lemma TWOEXP_DIVISION: "(k::nat) = k div (2::nat) ^ (n::nat) * (2::nat) ^ n + k mod (2::nat) ^ n" |
|
117 by (import bits TWOEXP_DIVISION) |
|
118 |
|
119 lemma TWOEXP_MONO: "(a::nat) < (b::nat) ==> (2::nat) ^ a < (2::nat) ^ b" |
|
120 by (import bits TWOEXP_MONO) |
|
121 |
|
122 lemma TWOEXP_MONO2: "(a::nat) <= (b::nat) ==> (2::nat) ^ a <= (2::nat) ^ b" |
|
123 by (import bits TWOEXP_MONO2) |
|
124 |
|
125 lemma EXP_SUB_LESS_EQ: "(2::nat) ^ ((a::nat) - (b::nat)) <= (2::nat) ^ a" |
|
126 by (import bits EXP_SUB_LESS_EQ) |
|
127 |
|
128 lemma BITS_THM: "BITS x xa xb = xb div 2 ^ xa mod 2 ^ (Suc x - xa)" |
|
129 by (import bits BITS_THM) |
|
130 |
|
131 lemma BITSLT_THM: "BITS h l n < 2 ^ (Suc h - l)" |
|
132 by (import bits BITSLT_THM) |
|
133 |
|
134 lemma DIV_MULT_LEM: "(0::nat) < (n::nat) ==> (m::nat) div n * n <= m" |
|
135 by (import bits DIV_MULT_LEM) |
|
136 |
|
137 lemma MOD_2EXP_LEM: "(n::nat) mod (2::nat) ^ (x::nat) = n - n div (2::nat) ^ x * (2::nat) ^ x" |
|
138 by (import bits MOD_2EXP_LEM) |
|
139 |
|
140 lemma BITS2_THM: "BITS h l n = n mod 2 ^ Suc h div 2 ^ l" |
|
141 by (import bits BITS2_THM) |
|
142 |
|
143 lemma BITS_COMP_THM: "h2 + l1 <= h1 ==> BITS h2 l2 (BITS h1 l1 n) = BITS (h2 + l1) (l2 + l1) n" |
|
144 by (import bits BITS_COMP_THM) |
|
145 |
|
146 lemma BITS_DIV_THM: "BITS h l x div 2 ^ n = BITS h (l + n) x" |
|
147 by (import bits BITS_DIV_THM) |
|
148 |
|
149 lemma BITS_LT_HIGH: "n < 2 ^ Suc h ==> BITS h l n = n div 2 ^ l" |
|
150 by (import bits BITS_LT_HIGH) |
|
151 |
|
152 lemma BITS_ZERO: "h < l ==> BITS h l n = 0" |
|
153 by (import bits BITS_ZERO) |
|
154 |
|
155 lemma BITS_ZERO2: "BITS h l 0 = 0" |
|
156 by (import bits BITS_ZERO2) |
|
157 |
|
158 lemma BITS_ZERO3: "BITS h 0 x = x mod 2 ^ Suc h" |
|
159 by (import bits BITS_ZERO3) |
|
160 |
|
161 lemma BITS_COMP_THM2: "BITS h2 l2 (BITS h1 l1 n) = BITS (min h1 (h2 + l1)) (l2 + l1) n" |
|
162 by (import bits BITS_COMP_THM2) |
|
163 |
|
164 lemma NOT_MOD2_LEM: "((n::nat) mod (2::nat) ~= (0::nat)) = (n mod (2::nat) = (1::nat))" |
|
165 by (import bits NOT_MOD2_LEM) |
|
166 |
|
167 lemma NOT_MOD2_LEM2: "((n::nat) mod (2::nat) ~= (1::nat)) = (n mod (2::nat) = (0::nat))" |
|
168 by (import bits NOT_MOD2_LEM2) |
|
169 |
|
170 lemma EVEN_MOD2_LEM: "EVEN n = (n mod 2 = 0)" |
|
171 by (import bits EVEN_MOD2_LEM) |
|
172 |
|
173 lemma ODD_MOD2_LEM: "ODD n = (n mod 2 = 1)" |
|
174 by (import bits ODD_MOD2_LEM) |
|
175 |
|
176 lemma LSB_ODD: "LSBn = ODD" |
|
177 by (import bits LSB_ODD) |
|
178 |
|
179 lemma DIV_MULT_THM: "(n::nat) div (2::nat) ^ (x::nat) * (2::nat) ^ x = n - n mod (2::nat) ^ x" |
|
180 by (import bits DIV_MULT_THM) |
|
181 |
|
182 lemma DIV_MULT_THM2: "(2::nat) * ((x::nat) div (2::nat)) = x - x mod (2::nat)" |
|
183 by (import bits DIV_MULT_THM2) |
|
184 |
|
185 lemma LESS_EQ_EXP_MULT: "(a::nat) <= (b::nat) ==> EX x::nat. (2::nat) ^ b = x * (2::nat) ^ a" |
|
186 by (import bits LESS_EQ_EXP_MULT) |
|
187 |
|
188 lemma SLICE_LEM1: "(a::nat) div (2::nat) ^ ((x::nat) + (y::nat)) * (2::nat) ^ (x + y) = |
|
189 a div (2::nat) ^ x * (2::nat) ^ x - |
|
190 a div (2::nat) ^ x mod (2::nat) ^ y * (2::nat) ^ x" |
|
191 by (import bits SLICE_LEM1) |
|
192 |
|
193 lemma SLICE_LEM2: "(n::nat) mod (2::nat) ^ ((x::nat) + (y::nat)) = |
|
194 n mod (2::nat) ^ x + n div (2::nat) ^ x mod (2::nat) ^ y * (2::nat) ^ x" |
|
195 by (import bits SLICE_LEM2) |
|
196 |
|
197 lemma SLICE_LEM3: "(l::nat) < (h::nat) ==> (n::nat) mod (2::nat) ^ Suc l <= n mod (2::nat) ^ h" |
|
198 by (import bits SLICE_LEM3) |
|
199 |
|
200 lemma SLICE_THM: "SLICE h l n = BITS h l n * 2 ^ l" |
|
201 by (import bits SLICE_THM) |
|
202 |
|
203 lemma SLICELT_THM: "SLICE h l n < 2 ^ Suc h" |
|
204 by (import bits SLICELT_THM) |
|
205 |
|
206 lemma BITS_SLICE_THM: "BITS h l (SLICE h l n) = BITS h l n" |
|
207 by (import bits BITS_SLICE_THM) |
|
208 |
|
209 lemma BITS_SLICE_THM2: "h <= h2 ==> BITS h2 l (SLICE h l n) = BITS h l n" |
|
210 by (import bits BITS_SLICE_THM2) |
|
211 |
|
212 lemma MOD_2EXP_MONO: "(l::nat) <= (h::nat) ==> (n::nat) mod (2::nat) ^ l <= n mod (2::nat) ^ Suc h" |
|
213 by (import bits MOD_2EXP_MONO) |
|
214 |
|
215 lemma SLICE_COMP_THM: "Suc m <= h & l <= m ==> SLICE h (Suc m) n + SLICE m l n = SLICE h l n" |
|
216 by (import bits SLICE_COMP_THM) |
|
217 |
|
218 lemma SLICE_ZERO: "h < l ==> SLICE h l n = 0" |
|
219 by (import bits SLICE_ZERO) |
|
220 |
|
221 lemma BIT_COMP_THM3: "Suc m <= h & l <= m |
|
222 ==> BITS h (Suc m) n * 2 ^ (Suc m - l) + BITS m l n = BITS h l n" |
|
223 by (import bits BIT_COMP_THM3) |
|
224 |
|
225 lemma NOT_BIT: "(~ bit n a) = (BITS n n a = 0)" |
|
226 by (import bits NOT_BIT) |
|
227 |
|
228 lemma NOT_BITS: "(BITS n n a ~= 0) = (BITS n n a = 1)" |
|
229 by (import bits NOT_BITS) |
|
230 |
|
231 lemma NOT_BITS2: "(BITS n n a ~= 1) = (BITS n n a = 0)" |
|
232 by (import bits NOT_BITS2) |
|
233 |
|
234 lemma BIT_SLICE: "(bit n a = bit n b) = (SLICE n n a = SLICE n n b)" |
|
235 by (import bits BIT_SLICE) |
|
236 |
|
237 lemma BIT_SLICE_LEM: "SBIT (bit x n) (x + y) = SLICE x x n * 2 ^ y" |
|
238 by (import bits BIT_SLICE_LEM) |
|
239 |
|
240 lemma BIT_SLICE_THM: "SBIT (bit x xa) x = SLICE x x xa" |
|
241 by (import bits BIT_SLICE_THM) |
|
242 |
|
243 lemma SBIT_DIV: "n < m ==> SBIT b (m - n) = SBIT b m div 2 ^ n" |
|
244 by (import bits SBIT_DIV) |
|
245 |
|
246 lemma BITS_SUC: "l <= Suc h |
|
247 ==> SBIT (bit (Suc h) n) (Suc h - l) + BITS h l n = BITS (Suc h) l n" |
|
248 by (import bits BITS_SUC) |
|
249 |
|
250 lemma BITS_SUC_THM: "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)" |
|
252 by (import bits BITS_SUC_THM) |
|
253 |
|
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)" |
|
255 by (import bits BIT_BITS_THM) |
|
256 |
|
257 lemma BITWISE_LT_2EXP: "BITWISE n oper a b < 2 ^ n" |
|
258 by (import bits BITWISE_LT_2EXP) |
|
259 |
|
260 lemma LESS_EXP_MULT2: "(a::nat) < (b::nat) |
|
261 ==> EX x::nat. (2::nat) ^ b = (2::nat) ^ (x + (1::nat)) * (2::nat) ^ a" |
|
262 by (import bits LESS_EXP_MULT2) |
|
263 |
|
264 lemma BITWISE_THM: "x < n ==> bit x (BITWISE n oper a b) = oper (bit x a) (bit x b)" |
|
265 by (import bits BITWISE_THM) |
|
266 |
|
267 lemma BITWISE_COR: "[| x < n; oper (bit x a) (bit x b) |] |
|
268 ==> BITWISE n oper a b div 2 ^ x mod 2 = 1" |
|
269 by (import bits BITWISE_COR) |
|
270 |
|
271 lemma BITWISE_NOT_COR: "[| x < n; ~ oper (bit x a) (bit x b) |] |
|
272 ==> BITWISE n oper a b div 2 ^ x mod 2 = 0" |
|
273 by (import bits BITWISE_NOT_COR) |
|
274 |
|
275 lemma MOD_PLUS_RIGHT: "(0::nat) < (n::nat) ==> ((j::nat) + (k::nat) mod n) mod n = (j + k) mod n" |
|
276 by (import bits MOD_PLUS_RIGHT) |
|
277 |
|
278 lemma MOD_PLUS_1: "(0::nat) < (n::nat) |
|
279 ==> (((x::nat) + (1::nat)) mod n = (0::nat)) = (x mod n + (1::nat) = n)" |
|
280 by (import bits MOD_PLUS_1) |
|
281 |
|
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)" |
|
284 by (import bits MOD_ADD_1) |
|
285 |
|
286 ;end_setup |
|
287 |
|
288 setup_theory "~~/src/HOL/Import/HOL4/Generated" word32 |
|
289 |
|
290 consts |
|
291 HB :: "nat" |
|
292 |
|
293 defs |
|
294 HB_primdef: "HB == |
|
295 NUMERAL |
|
296 (NUMERAL_BIT1 |
|
297 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))" |
|
298 |
|
299 lemma HB_def: "HB = |
|
300 NUMERAL |
|
301 (NUMERAL_BIT1 |
|
302 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))" |
|
303 by (import word32 HB_def) |
|
304 |
|
305 consts |
|
306 WL :: "nat" |
|
307 |
|
308 defs |
|
309 WL_primdef: "WL == Suc HB" |
|
310 |
|
311 lemma WL_def: "WL = Suc HB" |
|
312 by (import word32 WL_def) |
|
313 |
|
314 consts |
|
315 MODw :: "nat => nat" |
|
316 |
|
317 defs |
|
318 MODw_primdef: "MODw == %n. n mod 2 ^ WL" |
|
319 |
|
320 lemma MODw_def: "MODw n = n mod 2 ^ WL" |
|
321 by (import word32 MODw_def) |
|
322 |
|
323 consts |
|
324 INw :: "nat => bool" |
|
325 |
|
326 defs |
|
327 INw_primdef: "INw == %n. n < 2 ^ WL" |
|
328 |
|
329 lemma INw_def: "INw n = (n < 2 ^ WL)" |
|
330 by (import word32 INw_def) |
|
331 |
|
332 consts |
|
333 EQUIV :: "nat => nat => bool" |
|
334 |
|
335 defs |
|
336 EQUIV_primdef: "EQUIV == %x y. MODw x = MODw y" |
|
337 |
|
338 lemma EQUIV_def: "EQUIV x y = (MODw x = MODw y)" |
|
339 by (import word32 EQUIV_def) |
|
340 |
|
341 lemma EQUIV_QT: "EQUIV x y = (EQUIV x = EQUIV y)" |
|
342 by (import word32 EQUIV_QT) |
|
343 |
|
344 lemma FUNPOW_THM2: "(f ^^ Suc n) x = f ((f ^^ n) x)" |
|
345 by (import word32 FUNPOW_THM2) |
|
346 |
|
347 lemma FUNPOW_COMP: "(f ^^ m) ((f ^^ n) a) = (f ^^ (m + n)) a" |
|
348 by (import word32 FUNPOW_COMP) |
|
349 |
|
350 lemma INw_MODw: "INw (MODw n)" |
|
351 by (import word32 INw_MODw) |
|
352 |
|
353 lemma TOw_IDEM: "INw a ==> MODw a = a" |
|
354 by (import word32 TOw_IDEM) |
|
355 |
|
356 lemma MODw_IDEM2: "MODw (MODw a) = MODw a" |
|
357 by (import word32 MODw_IDEM2) |
|
358 |
|
359 lemma TOw_QT: "EQUIV (MODw a) a" |
|
360 by (import word32 TOw_QT) |
|
361 |
|
362 lemma MODw_THM: "MODw = BITS HB 0" |
|
363 by (import word32 MODw_THM) |
|
364 |
|
365 lemma MOD_ADD: "MODw (a + b) = MODw (MODw a + MODw b)" |
|
366 by (import word32 MOD_ADD) |
|
367 |
|
368 lemma MODw_MULT: "MODw (a * b) = MODw (MODw a * MODw b)" |
|
369 by (import word32 MODw_MULT) |
|
370 |
|
371 consts |
|
372 AONE :: "nat" |
|
373 |
|
374 defs |
|
375 AONE_primdef: "AONE == 1" |
|
376 |
|
377 lemma AONE_def: "AONE = 1" |
|
378 by (import word32 AONE_def) |
|
379 |
|
380 lemma ADD_QT: "(ALL n. EQUIV (0 + n) n) & (ALL m n. EQUIV (Suc m + n) (Suc (m + n)))" |
|
381 by (import word32 ADD_QT) |
|
382 |
|
383 lemma ADD_0_QT: "EQUIV (a + 0) a" |
|
384 by (import word32 ADD_0_QT) |
|
385 |
|
386 lemma ADD_COMM_QT: "EQUIV (a + b) (b + a)" |
|
387 by (import word32 ADD_COMM_QT) |
|
388 |
|
389 lemma ADD_ASSOC_QT: "EQUIV (a + (b + c)) (a + b + c)" |
|
390 by (import word32 ADD_ASSOC_QT) |
|
391 |
|
392 lemma MULT_QT: "(ALL n. EQUIV (0 * n) 0) & (ALL m n. EQUIV (Suc m * n) (m * n + n))" |
|
393 by (import word32 MULT_QT) |
|
394 |
|
395 lemma ADD1_QT: "EQUIV (Suc m) (m + AONE)" |
|
396 by (import word32 ADD1_QT) |
|
397 |
|
398 lemma ADD_CLAUSES_QT: "(ALL m. EQUIV (0 + m) m) & |
|
399 (ALL m. EQUIV (m + 0) m) & |
|
400 (ALL m n. EQUIV (Suc m + n) (Suc (m + n))) & |
|
401 (ALL m n. EQUIV (m + Suc n) (Suc (m + n)))" |
|
402 by (import word32 ADD_CLAUSES_QT) |
|
403 |
|
404 lemma SUC_EQUIV_COMP: "EQUIV (Suc a) b ==> EQUIV a (b + (2 ^ WL - 1))" |
|
405 by (import word32 SUC_EQUIV_COMP) |
|
406 |
|
407 lemma INV_SUC_EQ_QT: "EQUIV (Suc m) (Suc n) = EQUIV m n" |
|
408 by (import word32 INV_SUC_EQ_QT) |
|
409 |
|
410 lemma ADD_INV_0_QT: "EQUIV (m + n) m ==> EQUIV n 0" |
|
411 by (import word32 ADD_INV_0_QT) |
|
412 |
|
413 lemma ADD_INV_0_EQ_QT: "EQUIV (m + n) m = EQUIV n 0" |
|
414 by (import word32 ADD_INV_0_EQ_QT) |
|
415 |
|
416 lemma EQ_ADD_LCANCEL_QT: "EQUIV (m + n) (m + p) = EQUIV n p" |
|
417 by (import word32 EQ_ADD_LCANCEL_QT) |
|
418 |
|
419 lemma EQ_ADD_RCANCEL_QT: "EQUIV (x + xb) (xa + xb) = EQUIV x xa" |
|
420 by (import word32 EQ_ADD_RCANCEL_QT) |
|
421 |
|
422 lemma LEFT_ADD_DISTRIB_QT: "EQUIV (p * (m + n)) (p * m + p * n)" |
|
423 by (import word32 LEFT_ADD_DISTRIB_QT) |
|
424 |
|
425 lemma MULT_ASSOC_QT: "EQUIV (m * (n * p)) (m * n * p)" |
|
426 by (import word32 MULT_ASSOC_QT) |
|
427 |
|
428 lemma MULT_COMM_QT: "EQUIV (m * n) (n * m)" |
|
429 by (import word32 MULT_COMM_QT) |
|
430 |
|
431 lemma MULT_CLAUSES_QT: "EQUIV (0 * m) 0 & |
|
432 EQUIV (m * 0) 0 & |
|
433 EQUIV (AONE * m) m & |
|
434 EQUIV (m * AONE) m & |
|
435 EQUIV (Suc m * n) (m * n + n) & EQUIV (m * Suc n) (m + m * n)" |
|
436 by (import word32 MULT_CLAUSES_QT) |
|
437 |
|
438 consts |
|
439 MSBn :: "nat => bool" |
|
440 |
|
441 defs |
|
442 MSBn_primdef: "MSBn == bit HB" |
|
443 |
|
444 lemma MSBn_def: "MSBn = bit HB" |
|
445 by (import word32 MSBn_def) |
|
446 |
|
447 consts |
|
448 ONE_COMP :: "nat => nat" |
|
449 |
|
450 defs |
|
451 ONE_COMP_primdef: "ONE_COMP == %x. 2 ^ WL - 1 - MODw x" |
|
452 |
|
453 lemma ONE_COMP_def: "ONE_COMP x = 2 ^ WL - 1 - MODw x" |
|
454 by (import word32 ONE_COMP_def) |
|
455 |
|
456 consts |
|
457 TWO_COMP :: "nat => nat" |
|
458 |
|
459 defs |
|
460 TWO_COMP_primdef: "TWO_COMP == %x. 2 ^ WL - MODw x" |
|
461 |
|
462 lemma TWO_COMP_def: "TWO_COMP x = 2 ^ WL - MODw x" |
|
463 by (import word32 TWO_COMP_def) |
|
464 |
|
465 lemma ADD_TWO_COMP_QT: "EQUIV (MODw a + TWO_COMP a) 0" |
|
466 by (import word32 ADD_TWO_COMP_QT) |
|
467 |
|
468 lemma TWO_COMP_ONE_COMP_QT: "EQUIV (TWO_COMP a) (ONE_COMP a + AONE)" |
|
469 by (import word32 TWO_COMP_ONE_COMP_QT) |
|
470 |
|
471 lemma BIT_EQUIV_THM: "(ALL xb<WL. bit xb x = bit xb xa) = EQUIV x xa" |
|
472 by (import word32 BIT_EQUIV_THM) |
|
473 |
|
474 lemma BITS_SUC2: "BITS (Suc n) 0 a = SLICE (Suc n) (Suc n) a + BITS n 0 a" |
|
475 by (import word32 BITS_SUC2) |
|
476 |
|
477 lemma BITWISE_ONE_COMP_THM: "BITWISE WL (%x y. ~ x) a b = ONE_COMP a" |
|
478 by (import word32 BITWISE_ONE_COMP_THM) |
|
479 |
|
480 lemma ONE_COMP_THM: "xa < WL ==> bit xa (ONE_COMP x) = (~ bit xa x)" |
|
481 by (import word32 ONE_COMP_THM) |
|
482 |
|
483 consts |
|
484 OR :: "nat => nat => nat" |
|
485 |
|
486 defs |
|
487 OR_primdef: "OR == BITWISE WL op |" |
|
488 |
|
489 lemma OR_def: "OR = BITWISE WL op |" |
|
490 by (import word32 OR_def) |
|
491 |
|
492 consts |
|
493 AND :: "nat => nat => nat" |
|
494 |
|
495 defs |
|
496 AND_primdef: "AND == BITWISE WL op &" |
|
497 |
|
498 lemma AND_def: "AND = BITWISE WL op &" |
|
499 by (import word32 AND_def) |
|
500 |
|
501 consts |
|
502 EOR :: "nat => nat => nat" |
|
503 |
|
504 defs |
|
505 EOR_primdef: "EOR == BITWISE WL op ~=" |
|
506 |
|
507 lemma EOR_def: "EOR = BITWISE WL op ~=" |
|
508 by (import word32 EOR_def) |
|
509 |
|
510 consts |
|
511 COMP0 :: "nat" |
|
512 |
|
513 defs |
|
514 COMP0_primdef: "COMP0 == ONE_COMP 0" |
|
515 |
|
516 lemma COMP0_def: "COMP0 = ONE_COMP 0" |
|
517 by (import word32 COMP0_def) |
|
518 |
|
519 lemma BITWISE_THM2: "(ALL x<WL. oper (bit x a) (bit x b) = bit x y) = |
|
520 EQUIV (BITWISE WL oper a b) y" |
|
521 by (import word32 BITWISE_THM2) |
|
522 |
|
523 lemma OR_ASSOC_QT: "EQUIV (OR a (OR b c)) (OR (OR a b) c)" |
|
524 by (import word32 OR_ASSOC_QT) |
|
525 |
|
526 lemma OR_COMM_QT: "EQUIV (OR a b) (OR b a)" |
|
527 by (import word32 OR_COMM_QT) |
|
528 |
|
529 lemma OR_ABSORB_QT: "EQUIV (AND a (OR a b)) a" |
|
530 by (import word32 OR_ABSORB_QT) |
|
531 |
|
532 lemma OR_IDEM_QT: "EQUIV (OR a a) a" |
|
533 by (import word32 OR_IDEM_QT) |
|
534 |
|
535 lemma AND_ASSOC_QT: "EQUIV (AND a (AND b c)) (AND (AND a b) c)" |
|
536 by (import word32 AND_ASSOC_QT) |
|
537 |
|
538 lemma AND_COMM_QT: "EQUIV (AND a b) (AND b a)" |
|
539 by (import word32 AND_COMM_QT) |
|
540 |
|
541 lemma AND_ABSORB_QT: "EQUIV (OR a (AND a b)) a" |
|
542 by (import word32 AND_ABSORB_QT) |
|
543 |
|
544 lemma AND_IDEM_QT: "EQUIV (AND a a) a" |
|
545 by (import word32 AND_IDEM_QT) |
|
546 |
|
547 lemma OR_COMP_QT: "EQUIV (OR a (ONE_COMP a)) COMP0" |
|
548 by (import word32 OR_COMP_QT) |
|
549 |
|
550 lemma AND_COMP_QT: "EQUIV (AND a (ONE_COMP a)) 0" |
|
551 by (import word32 AND_COMP_QT) |
|
552 |
|
553 lemma ONE_COMP_QT: "EQUIV (ONE_COMP (ONE_COMP a)) a" |
|
554 by (import word32 ONE_COMP_QT) |
|
555 |
|
556 lemma RIGHT_AND_OVER_OR_QT: "EQUIV (AND (OR a b) c) (OR (AND a c) (AND b c))" |
|
557 by (import word32 RIGHT_AND_OVER_OR_QT) |
|
558 |
|
559 lemma RIGHT_OR_OVER_AND_QT: "EQUIV (OR (AND a b) c) (AND (OR a c) (OR b c))" |
|
560 by (import word32 RIGHT_OR_OVER_AND_QT) |
|
561 |
|
562 lemma DE_MORGAN_THM_QT: "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))" |
|
564 by (import word32 DE_MORGAN_THM_QT) |
|
565 |
|
566 lemma BIT_EQUIV: "[| n < WL; EQUIV a b |] ==> bit n a = bit n b" |
|
567 by (import word32 BIT_EQUIV) |
|
568 |
|
569 lemma LSB_WELLDEF: "EQUIV a b ==> LSBn a = LSBn b" |
|
570 by (import word32 LSB_WELLDEF) |
|
571 |
|
572 lemma MSB_WELLDEF: "EQUIV a b ==> MSBn a = MSBn b" |
|
573 by (import word32 MSB_WELLDEF) |
|
574 |
|
575 lemma BITWISE_ISTEP: "0 < n |
|
576 ==> 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)" |
|
578 by (import word32 BITWISE_ISTEP) |
|
579 |
|
580 lemma BITWISE_EVAL: "BITWISE (Suc n) oper a b = |
|
581 2 * BITWISE n oper (a div 2) (b div 2) + SBIT (oper (LSBn a) (LSBn b)) 0" |
|
582 by (import word32 BITWISE_EVAL) |
|
583 |
|
584 lemma BITWISE_WELLDEF: "EQUIV a b & EQUIV c d ==> EQUIV (BITWISE n oper a c) (BITWISE n oper b d)" |
|
585 by (import word32 BITWISE_WELLDEF) |
|
586 |
|
587 lemma BITWISEw_WELLDEF: "EQUIV a b & EQUIV c d ==> EQUIV (BITWISE WL oper a c) (BITWISE WL oper b d)" |
|
588 by (import word32 BITWISEw_WELLDEF) |
|
589 |
|
590 lemma SUC_WELLDEF: "EQUIV a b ==> EQUIV (Suc a) (Suc b)" |
|
591 by (import word32 SUC_WELLDEF) |
|
592 |
|
593 lemma ADD_WELLDEF: "EQUIV a b & EQUIV c d ==> EQUIV (a + c) (b + d)" |
|
594 by (import word32 ADD_WELLDEF) |
|
595 |
|
596 lemma MUL_WELLDEF: "EQUIV a b & EQUIV c d ==> EQUIV (a * c) (b * d)" |
|
597 by (import word32 MUL_WELLDEF) |
|
598 |
|
599 lemma ONE_COMP_WELLDEF: "EQUIV a b ==> EQUIV (ONE_COMP a) (ONE_COMP b)" |
|
600 by (import word32 ONE_COMP_WELLDEF) |
|
601 |
|
602 lemma TWO_COMP_WELLDEF: "EQUIV a b ==> EQUIV (TWO_COMP a) (TWO_COMP b)" |
|
603 by (import word32 TWO_COMP_WELLDEF) |
|
604 |
|
605 lemma TOw_WELLDEF: "EQUIV a b ==> EQUIV (MODw a) (MODw b)" |
|
606 by (import word32 TOw_WELLDEF) |
|
607 |
|
608 consts |
|
609 LSR_ONE :: "nat => nat" |
|
610 |
|
611 defs |
|
612 LSR_ONE_primdef: "LSR_ONE == %a. MODw a div 2" |
|
613 |
|
614 lemma LSR_ONE_def: "LSR_ONE a = MODw a div 2" |
|
615 by (import word32 LSR_ONE_def) |
|
616 |
|
617 consts |
|
618 ASR_ONE :: "nat => nat" |
|
619 |
|
620 defs |
|
621 ASR_ONE_primdef: "ASR_ONE == %a. LSR_ONE a + SBIT (MSBn a) HB" |
|
622 |
|
623 lemma ASR_ONE_def: "ASR_ONE a = LSR_ONE a + SBIT (MSBn a) HB" |
|
624 by (import word32 ASR_ONE_def) |
|
625 |
|
626 consts |
|
627 ROR_ONE :: "nat => nat" |
|
628 |
|
629 defs |
|
630 ROR_ONE_primdef: "ROR_ONE == %a. LSR_ONE a + SBIT (LSBn a) HB" |
|
631 |
|
632 lemma ROR_ONE_def: "ROR_ONE a = LSR_ONE a + SBIT (LSBn a) HB" |
|
633 by (import word32 ROR_ONE_def) |
|
634 |
|
635 consts |
|
636 RRXn :: "bool => nat => nat" |
|
637 |
|
638 defs |
|
639 RRXn_primdef: "RRXn == %c a. LSR_ONE a + SBIT c HB" |
|
640 |
|
641 lemma RRXn_def: "RRXn c a = LSR_ONE a + SBIT c HB" |
|
642 by (import word32 RRXn_def) |
|
643 |
|
644 lemma LSR_ONE_WELLDEF: "EQUIV a b ==> EQUIV (LSR_ONE a) (LSR_ONE b)" |
|
645 by (import word32 LSR_ONE_WELLDEF) |
|
646 |
|
647 lemma ASR_ONE_WELLDEF: "EQUIV a b ==> EQUIV (ASR_ONE a) (ASR_ONE b)" |
|
648 by (import word32 ASR_ONE_WELLDEF) |
|
649 |
|
650 lemma ROR_ONE_WELLDEF: "EQUIV a b ==> EQUIV (ROR_ONE a) (ROR_ONE b)" |
|
651 by (import word32 ROR_ONE_WELLDEF) |
|
652 |
|
653 lemma RRX_WELLDEF: "EQUIV a b ==> EQUIV (RRXn c a) (RRXn c b)" |
|
654 by (import word32 RRX_WELLDEF) |
|
655 |
|
656 lemma LSR_ONE: "LSR_ONE = BITS HB 1" |
|
657 by (import word32 LSR_ONE) |
|
658 |
|
659 typedef (open) word32 = "{x::nat => bool. EX xa. x = EQUIV xa}" |
|
660 by (rule typedef_helper,import word32 word32_TY_DEF) |
|
661 |
|
662 lemmas word32_TY_DEF = typedef_hol2hol4 [OF type_definition_word32] |
|
663 |
|
664 consts |
|
665 mk_word32 :: "(nat => bool) => word32" |
|
666 dest_word32 :: "word32 => nat => bool" |
|
667 |
|
668 specification (dest_word32 mk_word32) word32_tybij: "(ALL a. mk_word32 (dest_word32 a) = a) & |
|
669 (ALL r. (EX x. r = EQUIV x) = (dest_word32 (mk_word32 r) = r))" |
|
670 by (import word32 word32_tybij) |
|
671 |
|
672 consts |
|
673 w_0 :: "word32" |
|
674 |
|
675 defs |
|
676 w_0_primdef: "w_0 == mk_word32 (EQUIV 0)" |
|
677 |
|
678 lemma w_0_def: "w_0 = mk_word32 (EQUIV 0)" |
|
679 by (import word32 w_0_def) |
|
680 |
|
681 consts |
|
682 w_1 :: "word32" |
|
683 |
|
684 defs |
|
685 w_1_primdef: "w_1 == mk_word32 (EQUIV AONE)" |
|
686 |
|
687 lemma w_1_def: "w_1 = mk_word32 (EQUIV AONE)" |
|
688 by (import word32 w_1_def) |
|
689 |
|
690 consts |
|
691 w_T :: "word32" |
|
692 |
|
693 defs |
|
694 w_T_primdef: "w_T == mk_word32 (EQUIV COMP0)" |
|
695 |
|
696 lemma w_T_def: "w_T = mk_word32 (EQUIV COMP0)" |
|
697 by (import word32 w_T_def) |
|
698 |
|
699 definition |
|
700 word_suc :: "word32 => word32" where |
|
701 "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))))" |
|
704 by (import word32 word_suc) |
|
705 |
|
706 definition |
|
707 word_add :: "word32 => word32 => word32" where |
|
708 "word_add == |
|
709 %T1 T2. mk_word32 (EQUIV (Eps (dest_word32 T1) + Eps (dest_word32 T2)))" |
|
710 |
|
711 lemma word_add: "word_add T1 T2 = |
|
712 mk_word32 (EQUIV (Eps (dest_word32 T1) + Eps (dest_word32 T2)))" |
|
713 by (import word32 word_add) |
|
714 |
|
715 definition |
|
716 word_mul :: "word32 => word32 => word32" where |
|
717 "word_mul == |
|
718 %T1 T2. mk_word32 (EQUIV (Eps (dest_word32 T1) * Eps (dest_word32 T2)))" |
|
719 |
|
720 lemma word_mul: "word_mul T1 T2 = |
|
721 mk_word32 (EQUIV (Eps (dest_word32 T1) * Eps (dest_word32 T2)))" |
|
722 by (import word32 word_mul) |
|
723 |
|
724 definition |
|
725 word_1comp :: "word32 => word32" where |
|
726 "word_1comp == %T1. mk_word32 (EQUIV (ONE_COMP (Eps (dest_word32 T1))))" |
|
727 |
|
728 lemma word_1comp: "word_1comp T1 = mk_word32 (EQUIV (ONE_COMP (Eps (dest_word32 T1))))" |
|
729 by (import word32 word_1comp) |
|
730 |
|
731 definition |
|
732 word_2comp :: "word32 => word32" where |
|
733 "word_2comp == %T1. mk_word32 (EQUIV (TWO_COMP (Eps (dest_word32 T1))))" |
|
734 |
|
735 lemma word_2comp: "word_2comp T1 = mk_word32 (EQUIV (TWO_COMP (Eps (dest_word32 T1))))" |
|
736 by (import word32 word_2comp) |
|
737 |
|
738 definition |
|
739 word_lsr1 :: "word32 => word32" where |
|
740 "word_lsr1 == %T1. mk_word32 (EQUIV (LSR_ONE (Eps (dest_word32 T1))))" |
|
741 |
|
742 lemma word_lsr1: "word_lsr1 T1 = mk_word32 (EQUIV (LSR_ONE (Eps (dest_word32 T1))))" |
|
743 by (import word32 word_lsr1) |
|
744 |
|
745 definition |
|
746 word_asr1 :: "word32 => word32" where |
|
747 "word_asr1 == %T1. mk_word32 (EQUIV (ASR_ONE (Eps (dest_word32 T1))))" |
|
748 |
|
749 lemma word_asr1: "word_asr1 T1 = mk_word32 (EQUIV (ASR_ONE (Eps (dest_word32 T1))))" |
|
750 by (import word32 word_asr1) |
|
751 |
|
752 definition |
|
753 word_ror1 :: "word32 => word32" where |
|
754 "word_ror1 == %T1. mk_word32 (EQUIV (ROR_ONE (Eps (dest_word32 T1))))" |
|
755 |
|
756 lemma word_ror1: "word_ror1 T1 = mk_word32 (EQUIV (ROR_ONE (Eps (dest_word32 T1))))" |
|
757 by (import word32 word_ror1) |
|
758 |
|
759 consts |
|
760 RRX :: "bool => word32 => word32" |
|
761 |
|
762 defs |
|
763 RRX_primdef: "RRX == %T1 T2. mk_word32 (EQUIV (RRXn T1 (Eps (dest_word32 T2))))" |
|
764 |
|
765 lemma RRX_def: "RRX T1 T2 = mk_word32 (EQUIV (RRXn T1 (Eps (dest_word32 T2))))" |
|
766 by (import word32 RRX_def) |
|
767 |
|
768 consts |
|
769 LSB :: "word32 => bool" |
|
770 |
|
771 defs |
|
772 LSB_primdef: "LSB == %T1. LSBn (Eps (dest_word32 T1))" |
|
773 |
|
774 lemma LSB_def: "LSB T1 = LSBn (Eps (dest_word32 T1))" |
|
775 by (import word32 LSB_def) |
|
776 |
|
777 consts |
|
778 MSB :: "word32 => bool" |
|
779 |
|
780 defs |
|
781 MSB_primdef: "MSB == %T1. MSBn (Eps (dest_word32 T1))" |
|
782 |
|
783 lemma MSB_def: "MSB T1 = MSBn (Eps (dest_word32 T1))" |
|
784 by (import word32 MSB_def) |
|
785 |
|
786 definition |
|
787 bitwise_or :: "word32 => word32 => word32" where |
|
788 "bitwise_or == |
|
789 %T1 T2. mk_word32 (EQUIV (OR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
|
790 |
|
791 lemma bitwise_or: "bitwise_or T1 T2 = |
|
792 mk_word32 (EQUIV (OR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
|
793 by (import word32 bitwise_or) |
|
794 |
|
795 definition |
|
796 bitwise_eor :: "word32 => word32 => word32" where |
|
797 "bitwise_eor == |
|
798 %T1 T2. |
|
799 mk_word32 (EQUIV (EOR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
|
800 |
|
801 lemma bitwise_eor: "bitwise_eor T1 T2 = |
|
802 mk_word32 (EQUIV (EOR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
|
803 by (import word32 bitwise_eor) |
|
804 |
|
805 definition |
|
806 bitwise_and :: "word32 => word32 => word32" where |
|
807 "bitwise_and == |
|
808 %T1 T2. |
|
809 mk_word32 (EQUIV (AND (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
|
810 |
|
811 lemma bitwise_and: "bitwise_and T1 T2 = |
|
812 mk_word32 (EQUIV (AND (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))" |
|
813 by (import word32 bitwise_and) |
|
814 |
|
815 consts |
|
816 TOw :: "word32 => word32" |
|
817 |
|
818 defs |
|
819 TOw_primdef: "TOw == %T1. mk_word32 (EQUIV (MODw (Eps (dest_word32 T1))))" |
|
820 |
|
821 lemma TOw_def: "TOw T1 = mk_word32 (EQUIV (MODw (Eps (dest_word32 T1))))" |
|
822 by (import word32 TOw_def) |
|
823 |
|
824 consts |
|
825 n2w :: "nat => word32" |
|
826 |
|
827 defs |
|
828 n2w_primdef: "n2w == %n. mk_word32 (EQUIV n)" |
|
829 |
|
830 lemma n2w_def: "n2w n = mk_word32 (EQUIV n)" |
|
831 by (import word32 n2w_def) |
|
832 |
|
833 consts |
|
834 w2n :: "word32 => nat" |
|
835 |
|
836 defs |
|
837 w2n_primdef: "w2n == %w. MODw (Eps (dest_word32 w))" |
|
838 |
|
839 lemma w2n_def: "w2n w = MODw (Eps (dest_word32 w))" |
|
840 by (import word32 w2n_def) |
|
841 |
|
842 lemma ADDw: "(ALL x. word_add w_0 x = x) & |
|
843 (ALL x xa. word_add (word_suc x) xa = word_suc (word_add x xa))" |
|
844 by (import word32 ADDw) |
|
845 |
|
846 lemma ADD_0w: "word_add x w_0 = x" |
|
847 by (import word32 ADD_0w) |
|
848 |
|
849 lemma ADD1w: "word_suc x = word_add x w_1" |
|
850 by (import word32 ADD1w) |
|
851 |
|
852 lemma ADD_ASSOCw: "word_add x (word_add xa xb) = word_add (word_add x xa) xb" |
|
853 by (import word32 ADD_ASSOCw) |
|
854 |
|
855 lemma ADD_CLAUSESw: "(ALL x. word_add w_0 x = x) & |
|
856 (ALL x. word_add x w_0 = x) & |
|
857 (ALL x xa. 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))" |
|
859 by (import word32 ADD_CLAUSESw) |
|
860 |
|
861 lemma ADD_COMMw: "word_add x xa = word_add xa x" |
|
862 by (import word32 ADD_COMMw) |
|
863 |
|
864 lemma ADD_INV_0_EQw: "(word_add x xa = x) = (xa = w_0)" |
|
865 by (import word32 ADD_INV_0_EQw) |
|
866 |
|
867 lemma EQ_ADD_LCANCELw: "(word_add x xa = word_add x xb) = (xa = xb)" |
|
868 by (import word32 EQ_ADD_LCANCELw) |
|
869 |
|
870 lemma EQ_ADD_RCANCELw: "(word_add x xb = word_add xa xb) = (x = xa)" |
|
871 by (import word32 EQ_ADD_RCANCELw) |
|
872 |
|
873 lemma LEFT_ADD_DISTRIBw: "word_mul xb (word_add x xa) = word_add (word_mul xb x) (word_mul xb xa)" |
|
874 by (import word32 LEFT_ADD_DISTRIBw) |
|
875 |
|
876 lemma MULT_ASSOCw: "word_mul x (word_mul xa xb) = word_mul (word_mul x xa) xb" |
|
877 by (import word32 MULT_ASSOCw) |
|
878 |
|
879 lemma MULT_COMMw: "word_mul x xa = word_mul xa x" |
|
880 by (import word32 MULT_COMMw) |
|
881 |
|
882 lemma MULT_CLAUSESw: "word_mul w_0 x = w_0 & |
|
883 word_mul x w_0 = w_0 & |
|
884 word_mul w_1 x = x & |
|
885 word_mul x w_1 = x & |
|
886 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)" |
|
888 by (import word32 MULT_CLAUSESw) |
|
889 |
|
890 lemma TWO_COMP_ONE_COMP: "word_2comp x = word_add (word_1comp x) w_1" |
|
891 by (import word32 TWO_COMP_ONE_COMP) |
|
892 |
|
893 lemma OR_ASSOCw: "bitwise_or x (bitwise_or xa xb) = bitwise_or (bitwise_or x xa) xb" |
|
894 by (import word32 OR_ASSOCw) |
|
895 |
|
896 lemma OR_COMMw: "bitwise_or x xa = bitwise_or xa x" |
|
897 by (import word32 OR_COMMw) |
|
898 |
|
899 lemma OR_IDEMw: "bitwise_or x x = x" |
|
900 by (import word32 OR_IDEMw) |
|
901 |
|
902 lemma OR_ABSORBw: "bitwise_and x (bitwise_or x xa) = x" |
|
903 by (import word32 OR_ABSORBw) |
|
904 |
|
905 lemma AND_ASSOCw: "bitwise_and x (bitwise_and xa xb) = bitwise_and (bitwise_and x xa) xb" |
|
906 by (import word32 AND_ASSOCw) |
|
907 |
|
908 lemma AND_COMMw: "bitwise_and x xa = bitwise_and xa x" |
|
909 by (import word32 AND_COMMw) |
|
910 |
|
911 lemma AND_IDEMw: "bitwise_and x x = x" |
|
912 by (import word32 AND_IDEMw) |
|
913 |
|
914 lemma AND_ABSORBw: "bitwise_or x (bitwise_and x xa) = x" |
|
915 by (import word32 AND_ABSORBw) |
|
916 |
|
917 lemma ONE_COMPw: "word_1comp (word_1comp x) = x" |
|
918 by (import word32 ONE_COMPw) |
|
919 |
|
920 lemma RIGHT_AND_OVER_ORw: "bitwise_and (bitwise_or x xa) xb = |
|
921 bitwise_or (bitwise_and x xb) (bitwise_and xa xb)" |
|
922 by (import word32 RIGHT_AND_OVER_ORw) |
|
923 |
|
924 lemma RIGHT_OR_OVER_ANDw: "bitwise_or (bitwise_and x xa) xb = |
|
925 bitwise_and (bitwise_or x xb) (bitwise_or xa xb)" |
|
926 by (import word32 RIGHT_OR_OVER_ANDw) |
|
927 |
|
928 lemma DE_MORGAN_THMw: "word_1comp (bitwise_and x xa) = bitwise_or (word_1comp x) (word_1comp xa) & |
|
929 word_1comp (bitwise_or x xa) = bitwise_and (word_1comp x) (word_1comp xa)" |
|
930 by (import word32 DE_MORGAN_THMw) |
|
931 |
|
932 lemma w_0: "w_0 = n2w 0" |
|
933 by (import word32 w_0) |
|
934 |
|
935 lemma w_1: "w_1 = n2w 1" |
|
936 by (import word32 w_1) |
|
937 |
|
938 lemma w_T: "w_T = |
|
939 n2w (NUMERAL |
|
940 (NUMERAL_BIT1 |
|
941 (NUMERAL_BIT1 |
|
942 (NUMERAL_BIT1 |
|
943 (NUMERAL_BIT1 |
|
944 (NUMERAL_BIT1 |
|
945 (NUMERAL_BIT1 |
|
946 (NUMERAL_BIT1 |
|
947 (NUMERAL_BIT1 |
|
948 (NUMERAL_BIT1 |
|
949 (NUMERAL_BIT1 |
|
950 (NUMERAL_BIT1 |
|
951 (NUMERAL_BIT1 |
|
952 (NUMERAL_BIT1 |
|
953 (NUMERAL_BIT1 |
|
954 (NUMERAL_BIT1 |
|
955 (NUMERAL_BIT1 |
|
956 (NUMERAL_BIT1 |
|
957 (NUMERAL_BIT1 |
|
958 (NUMERAL_BIT1 |
|
959 (NUMERAL_BIT1 |
|
960 (NUMERAL_BIT1 |
|
961 (NUMERAL_BIT1 |
|
962 (NUMERAL_BIT1 |
|
963 (NUMERAL_BIT1 |
|
964 (NUMERAL_BIT1 |
|
965 (NUMERAL_BIT1 |
|
966 (NUMERAL_BIT1 |
|
967 (NUMERAL_BIT1 |
|
968 (NUMERAL_BIT1 |
|
969 (NUMERAL_BIT1 |
|
970 (NUMERAL_BIT1 |
|
971 (NUMERAL_BIT1 |
|
972 ALT_ZERO)))))))))))))))))))))))))))))))))" |
|
973 by (import word32 w_T) |
|
974 |
|
975 lemma ADD_TWO_COMP: "word_add x (word_2comp x) = w_0" |
|
976 by (import word32 ADD_TWO_COMP) |
|
977 |
|
978 lemma ADD_TWO_COMP2: "word_add (word_2comp x) x = w_0" |
|
979 by (import word32 ADD_TWO_COMP2) |
|
980 |
|
981 definition |
|
982 word_sub :: "word32 => word32 => word32" where |
|
983 "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)" |
|
986 by (import word32 word_sub) |
|
987 |
|
988 definition |
|
989 word_lsl :: "word32 => nat => word32" where |
|
990 "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))" |
|
993 by (import word32 word_lsl) |
|
994 |
|
995 definition |
|
996 word_lsr :: "word32 => nat => word32" where |
|
997 "word_lsr == %a n. (word_lsr1 ^^ n) a" |
|
998 |
|
999 lemma word_lsr: "word_lsr a n = (word_lsr1 ^^ n) a" |
|
1000 by (import word32 word_lsr) |
|
1001 |
|
1002 definition |
|
1003 word_asr :: "word32 => nat => word32" where |
|
1004 "word_asr == %a n. (word_asr1 ^^ n) a" |
|
1005 |
|
1006 lemma word_asr: "word_asr a n = (word_asr1 ^^ n) a" |
|
1007 by (import word32 word_asr) |
|
1008 |
|
1009 definition |
|
1010 word_ror :: "word32 => nat => word32" where |
|
1011 "word_ror == %a n. (word_ror1 ^^ n) a" |
|
1012 |
|
1013 lemma word_ror: "word_ror a n = (word_ror1 ^^ n) a" |
|
1014 by (import word32 word_ror) |
|
1015 |
|
1016 consts |
|
1017 BITw :: "nat => word32 => bool" |
|
1018 |
|
1019 defs |
|
1020 BITw_primdef: "BITw == %b n. bit b (w2n n)" |
|
1021 |
|
1022 lemma BITw_def: "BITw b n = bit b (w2n n)" |
|
1023 by (import word32 BITw_def) |
|
1024 |
|
1025 consts |
|
1026 BITSw :: "nat => nat => word32 => nat" |
|
1027 |
|
1028 defs |
|
1029 BITSw_primdef: "BITSw == %h l n. BITS h l (w2n n)" |
|
1030 |
|
1031 lemma BITSw_def: "BITSw h l n = BITS h l (w2n n)" |
|
1032 by (import word32 BITSw_def) |
|
1033 |
|
1034 consts |
|
1035 SLICEw :: "nat => nat => word32 => nat" |
|
1036 |
|
1037 defs |
|
1038 SLICEw_primdef: "SLICEw == %h l n. SLICE h l (w2n n)" |
|
1039 |
|
1040 lemma SLICEw_def: "SLICEw h l n = SLICE h l (w2n n)" |
|
1041 by (import word32 SLICEw_def) |
|
1042 |
|
1043 lemma TWO_COMP_ADD: "word_2comp (word_add a b) = word_add (word_2comp a) (word_2comp b)" |
|
1044 by (import word32 TWO_COMP_ADD) |
|
1045 |
|
1046 lemma TWO_COMP_ELIM: "word_2comp (word_2comp a) = a" |
|
1047 by (import word32 TWO_COMP_ELIM) |
|
1048 |
|
1049 lemma ADD_SUB_ASSOC: "word_sub (word_add a b) c = word_add a (word_sub b c)" |
|
1050 by (import word32 ADD_SUB_ASSOC) |
|
1051 |
|
1052 lemma ADD_SUB_SYM: "word_sub (word_add a b) c = word_add (word_sub a c) b" |
|
1053 by (import word32 ADD_SUB_SYM) |
|
1054 |
|
1055 lemma SUB_EQUALw: "word_sub a a = w_0" |
|
1056 by (import word32 SUB_EQUALw) |
|
1057 |
|
1058 lemma ADD_SUBw: "word_sub (word_add a b) b = a" |
|
1059 by (import word32 ADD_SUBw) |
|
1060 |
|
1061 lemma SUB_SUBw: "word_sub a (word_sub b c) = word_sub (word_add a c) b" |
|
1062 by (import word32 SUB_SUBw) |
|
1063 |
|
1064 lemma ONE_COMP_TWO_COMP: "word_1comp a = word_sub (word_2comp a) w_1" |
|
1065 by (import word32 ONE_COMP_TWO_COMP) |
|
1066 |
|
1067 lemma SUBw: "word_sub (word_suc m) n = word_suc (word_sub m n)" |
|
1068 by (import word32 SUBw) |
|
1069 |
|
1070 lemma ADD_EQ_SUBw: "(word_add m n = p) = (m = word_sub p n)" |
|
1071 by (import word32 ADD_EQ_SUBw) |
|
1072 |
|
1073 lemma CANCEL_SUBw: "(word_sub n p = word_sub m p) = (n = m)" |
|
1074 by (import word32 CANCEL_SUBw) |
|
1075 |
|
1076 lemma SUB_PLUSw: "word_sub a (word_add b c) = word_sub (word_sub a b) c" |
|
1077 by (import word32 SUB_PLUSw) |
|
1078 |
|
1079 lemma word_nchotomy: "EX n. w = n2w n" |
|
1080 by (import word32 word_nchotomy) |
|
1081 |
|
1082 lemma dest_word_mk_word_eq3: "dest_word32 (mk_word32 (EQUIV a)) = EQUIV a" |
|
1083 by (import word32 dest_word_mk_word_eq3) |
|
1084 |
|
1085 lemma MODw_ELIM: "n2w (MODw n) = n2w n" |
|
1086 by (import word32 MODw_ELIM) |
|
1087 |
|
1088 lemma w2n_EVAL: "w2n (n2w n) = MODw n" |
|
1089 by (import word32 w2n_EVAL) |
|
1090 |
|
1091 lemma w2n_ELIM: "n2w (w2n a) = a" |
|
1092 by (import word32 w2n_ELIM) |
|
1093 |
|
1094 lemma n2w_11: "(n2w a = n2w b) = (MODw a = MODw b)" |
|
1095 by (import word32 n2w_11) |
|
1096 |
|
1097 lemma ADD_EVAL: "word_add (n2w a) (n2w b) = n2w (a + b)" |
|
1098 by (import word32 ADD_EVAL) |
|
1099 |
|
1100 lemma MUL_EVAL: "word_mul (n2w a) (n2w b) = n2w (a * b)" |
|
1101 by (import word32 MUL_EVAL) |
|
1102 |
|
1103 lemma ONE_COMP_EVAL: "word_1comp (n2w a) = n2w (ONE_COMP a)" |
|
1104 by (import word32 ONE_COMP_EVAL) |
|
1105 |
|
1106 lemma TWO_COMP_EVAL: "word_2comp (n2w a) = n2w (TWO_COMP a)" |
|
1107 by (import word32 TWO_COMP_EVAL) |
|
1108 |
|
1109 lemma LSR_ONE_EVAL: "word_lsr1 (n2w a) = n2w (LSR_ONE a)" |
|
1110 by (import word32 LSR_ONE_EVAL) |
|
1111 |
|
1112 lemma ASR_ONE_EVAL: "word_asr1 (n2w a) = n2w (ASR_ONE a)" |
|
1113 by (import word32 ASR_ONE_EVAL) |
|
1114 |
|
1115 lemma ROR_ONE_EVAL: "word_ror1 (n2w a) = n2w (ROR_ONE a)" |
|
1116 by (import word32 ROR_ONE_EVAL) |
|
1117 |
|
1118 lemma RRX_EVAL: "RRX c (n2w a) = n2w (RRXn c a)" |
|
1119 by (import word32 RRX_EVAL) |
|
1120 |
|
1121 lemma LSB_EVAL: "LSB (n2w a) = LSBn a" |
|
1122 by (import word32 LSB_EVAL) |
|
1123 |
|
1124 lemma MSB_EVAL: "MSB (n2w a) = MSBn a" |
|
1125 by (import word32 MSB_EVAL) |
|
1126 |
|
1127 lemma OR_EVAL: "bitwise_or (n2w a) (n2w b) = n2w (OR a b)" |
|
1128 by (import word32 OR_EVAL) |
|
1129 |
|
1130 lemma EOR_EVAL: "bitwise_eor (n2w a) (n2w b) = n2w (EOR a b)" |
|
1131 by (import word32 EOR_EVAL) |
|
1132 |
|
1133 lemma AND_EVAL: "bitwise_and (n2w a) (n2w b) = n2w (AND a b)" |
|
1134 by (import word32 AND_EVAL) |
|
1135 |
|
1136 lemma BITS_EVAL: "BITSw h l (n2w a) = BITS h l (MODw a)" |
|
1137 by (import word32 BITS_EVAL) |
|
1138 |
|
1139 lemma BIT_EVAL: "BITw b (n2w a) = bit b (MODw a)" |
|
1140 by (import word32 BIT_EVAL) |
|
1141 |
|
1142 lemma SLICE_EVAL: "SLICEw h l (n2w a) = SLICE h l (MODw a)" |
|
1143 by (import word32 SLICE_EVAL) |
|
1144 |
|
1145 lemma LSL_ADD: "word_lsl (word_lsl a m) n = word_lsl a (m + n)" |
|
1146 by (import word32 LSL_ADD) |
|
1147 |
|
1148 lemma LSR_ADD: "word_lsr (word_lsr x xa) xb = word_lsr x (xa + xb)" |
|
1149 by (import word32 LSR_ADD) |
|
1150 |
|
1151 lemma ASR_ADD: "word_asr (word_asr x xa) xb = word_asr x (xa + xb)" |
|
1152 by (import word32 ASR_ADD) |
|
1153 |
|
1154 lemma ROR_ADD: "word_ror (word_ror x xa) xb = word_ror x (xa + xb)" |
|
1155 by (import word32 ROR_ADD) |
|
1156 |
|
1157 lemma LSL_LIMIT: "HB < n ==> word_lsl w n = w_0" |
|
1158 by (import word32 LSL_LIMIT) |
|
1159 |
|
1160 lemma MOD_MOD_DIV: "INw (MODw a div 2 ^ b)" |
|
1161 by (import word32 MOD_MOD_DIV) |
|
1162 |
|
1163 lemma MOD_MOD_DIV_2EXP: "MODw (MODw a div 2 ^ n) div 2 = MODw a div 2 ^ Suc n" |
|
1164 by (import word32 MOD_MOD_DIV_2EXP) |
|
1165 |
|
1166 lemma LSR_EVAL: "word_lsr (n2w a) n = n2w (MODw a div 2 ^ n)" |
|
1167 by (import word32 LSR_EVAL) |
|
1168 |
|
1169 lemma LSR_THM: "word_lsr (n2w n) x = n2w (BITS HB (min WL x) n)" |
|
1170 by (import word32 LSR_THM) |
|
1171 |
|
1172 lemma LSR_LIMIT: "HB < x ==> word_lsr w x = w_0" |
|
1173 by (import word32 LSR_LIMIT) |
|
1174 |
|
1175 lemma LEFT_SHIFT_LESS: "(a::nat) < (2::nat) ^ (m::nat) |
|
1176 ==> (2::nat) ^ (n::nat) + a * (2::nat) ^ n <= (2::nat) ^ (m + n)" |
|
1177 by (import word32 LEFT_SHIFT_LESS) |
|
1178 |
|
1179 lemma ROR_THM: "word_ror (n2w n) x = |
|
1180 (let x' = x mod WL |
|
1181 in n2w (BITS HB x' n + BITS (x' - 1) 0 n * 2 ^ (WL - x')))" |
|
1182 by (import word32 ROR_THM) |
|
1183 |
|
1184 lemma ROR_CYCLE: "word_ror w (x * WL) = w" |
|
1185 by (import word32 ROR_CYCLE) |
|
1186 |
|
1187 lemma ASR_THM: "word_asr (n2w n) x = |
|
1188 (let x' = min HB x; s = BITS HB x' n |
|
1189 in n2w (if MSBn n then 2 ^ WL - 2 ^ (WL - x') + s else s))" |
|
1190 by (import word32 ASR_THM) |
|
1191 |
|
1192 lemma ASR_LIMIT: "HB <= x ==> word_asr w x = (if MSB w then w_T else w_0)" |
|
1193 by (import word32 ASR_LIMIT) |
|
1194 |
|
1195 lemma ZERO_SHIFT: "(ALL n. word_lsl w_0 n = w_0) & |
|
1196 (ALL n. word_asr w_0 n = w_0) & |
|
1197 (ALL n. word_lsr w_0 n = w_0) & (ALL n. word_ror w_0 n = w_0)" |
|
1198 by (import word32 ZERO_SHIFT) |
|
1199 |
|
1200 lemma ZERO_SHIFT2: "(ALL a. word_lsl a 0 = a) & |
|
1201 (ALL a. word_asr a 0 = a) & |
|
1202 (ALL a. word_lsr a 0 = a) & (ALL a. word_ror a 0 = a)" |
|
1203 by (import word32 ZERO_SHIFT2) |
|
1204 |
|
1205 lemma ASR_w_T: "word_asr w_T n = w_T" |
|
1206 by (import word32 ASR_w_T) |
|
1207 |
|
1208 lemma ROR_w_T: "word_ror w_T n = w_T" |
|
1209 by (import word32 ROR_w_T) |
|
1210 |
|
1211 lemma MODw_EVAL: "MODw x = |
|
1212 x mod |
|
1213 NUMERAL |
|
1214 (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 |
|
1310 (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 |
|
1320 (NUMERAL_BIT1 |
|
1321 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))) |
|
1322 op | a b)" |
|
1323 by (import word32 OR_EVAL2) |
|
1324 |
|
1325 lemma AND_EVAL2: "bitwise_and (n2w a) (n2w b) = |
|
1326 n2w (BITWISE |
|
1327 (NUMERAL |
|
1328 (NUMERAL_BIT2 |
|
1329 (NUMERAL_BIT1 |
|
1330 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))) |
|
1331 op & a b)" |
|
1332 by (import word32 AND_EVAL2) |
|
1333 |
|
1334 lemma EOR_EVAL2: "bitwise_eor (n2w a) (n2w b) = |
|
1335 n2w (BITWISE |
|
1336 (NUMERAL |
|
1337 (NUMERAL_BIT2 |
|
1338 (NUMERAL_BIT1 |
|
1339 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))) |
|
1340 op ~= a b)" |
|
1341 by (import word32 EOR_EVAL2) |
|
1342 |
|
1343 lemma BITWISE_EVAL2: "BITWISE n oper x y = |
|
1344 (if n = 0 then 0 |
|
1345 else 2 * BITWISE (n - 1) oper (x div 2) (y div 2) + |
|
1346 (if oper (ODD x) (ODD y) then 1 else 0))" |
|
1347 by (import word32 BITWISE_EVAL2) |
|
1348 |
|
1349 lemma BITSwLT_THM: "BITSw h l n < 2 ^ (Suc h - l)" |
|
1350 by (import word32 BITSwLT_THM) |
|
1351 |
|
1352 lemma BITSw_COMP_THM: "h2 + l1 <= h1 ==> BITS h2 l2 (BITSw h1 l1 n) = BITSw (h2 + l1) (l2 + l1) n" |
|
1353 by (import word32 BITSw_COMP_THM) |
|
1354 |
|
1355 lemma BITSw_DIV_THM: "BITSw h l x div 2 ^ n = BITSw h (l + n) x" |
|
1356 by (import word32 BITSw_DIV_THM) |
|
1357 |
|
1358 lemma BITw_THM: "BITw b n = (BITSw b b n = 1)" |
|
1359 by (import word32 BITw_THM) |
|
1360 |
|
1361 lemma SLICEw_THM: "SLICEw h l n = BITSw h l n * 2 ^ l" |
|
1362 by (import word32 SLICEw_THM) |
|
1363 |
|
1364 lemma BITS_SLICEw_THM: "BITS h l (SLICEw h l n) = BITSw h l n" |
|
1365 by (import word32 BITS_SLICEw_THM) |
|
1366 |
|
1367 lemma SLICEw_ZERO_THM: "SLICEw h 0 n = BITSw h 0 n" |
|
1368 by (import word32 SLICEw_ZERO_THM) |
|
1369 |
|
1370 lemma SLICEw_COMP_THM: "Suc m <= h & l <= m ==> SLICEw h (Suc m) a + SLICEw m l a = SLICEw h l a" |
|
1371 by (import word32 SLICEw_COMP_THM) |
|
1372 |
|
1373 lemma BITSw_ZERO: "h < l ==> BITSw h l n = 0" |
|
1374 by (import word32 BITSw_ZERO) |
|
1375 |
|
1376 lemma SLICEw_ZERO: "h < l ==> SLICEw h l n = 0" |
|
1377 by (import word32 SLICEw_ZERO) |
|
1378 |
|
1379 ;end_setup |
|
1380 |
|
1381 end |
|
1382 |