14516

1 
theory HOL4Word32 = HOL4Base:


2 


3 
;setup_theory bits


4 


5 
consts


6 
DIV2 :: "nat => nat"


7 


8 
defs


9 
DIV2_primdef: "DIV2 == %n. n div 2"


10 


11 
lemma DIV2_def: "ALL n. DIV2 n = n div 2"


12 
by (import bits DIV2_def)


13 


14 
consts


15 
TIMES_2EXP :: "nat => nat => nat"


16 


17 
defs


18 
TIMES_2EXP_primdef: "TIMES_2EXP == %x n. n * 2 ^ x"


19 


20 
lemma TIMES_2EXP_def: "ALL x n. TIMES_2EXP x n = n * 2 ^ x"


21 
by (import bits TIMES_2EXP_def)


22 


23 
consts


24 
DIV_2EXP :: "nat => nat => nat"


25 


26 
defs


27 
DIV_2EXP_primdef: "DIV_2EXP == %x n. n div 2 ^ x"


28 


29 
lemma DIV_2EXP_def: "ALL x n. DIV_2EXP x n = n div 2 ^ x"


30 
by (import bits DIV_2EXP_def)


31 


32 
consts


33 
MOD_2EXP :: "nat => nat => nat"


34 


35 
defs


36 
MOD_2EXP_primdef: "MOD_2EXP == %x n. n mod 2 ^ x"


37 


38 
lemma MOD_2EXP_def: "ALL x n. MOD_2EXP x n = n mod 2 ^ x"


39 
by (import bits MOD_2EXP_def)


40 


41 
consts


42 
DIVMOD_2EXP :: "nat => nat => nat * nat"


43 


44 
defs


45 
DIVMOD_2EXP_primdef: "DIVMOD_2EXP == %x n. (n div 2 ^ x, n mod 2 ^ x)"


46 


47 
lemma DIVMOD_2EXP_def: "ALL x n. DIVMOD_2EXP x n = (n div 2 ^ x, n mod 2 ^ x)"


48 
by (import bits DIVMOD_2EXP_def)


49 


50 
consts


51 
SBIT :: "bool => nat => nat"


52 


53 
defs


54 
SBIT_primdef: "SBIT == %b n. if b then 2 ^ n else 0"


55 


56 
lemma SBIT_def: "ALL b n. SBIT b n = (if b then 2 ^ n else 0)"


57 
by (import bits SBIT_def)


58 


59 
consts


60 
BITS :: "nat => nat => nat => nat"


61 


62 
defs


63 
BITS_primdef: "BITS == %h l n. MOD_2EXP (Suc h  l) (DIV_2EXP l n)"


64 


65 
lemma BITS_def: "ALL h l n. BITS h l n = MOD_2EXP (Suc h  l) (DIV_2EXP l n)"


66 
by (import bits BITS_def)


67 


68 
constdefs


69 
bit :: "nat => nat => bool"


70 
"bit == %b n. BITS b b n = 1"


71 


72 
lemma BIT_def: "ALL b n. bit b n = (BITS b b n = 1)"


73 
by (import bits BIT_def)


74 


75 
consts


76 
SLICE :: "nat => nat => nat => nat"


77 


78 
defs


79 
SLICE_primdef: "SLICE == %h l n. MOD_2EXP (Suc h) n  MOD_2EXP l n"


80 


81 
lemma SLICE_def: "ALL h l n. SLICE h l n = MOD_2EXP (Suc h) n  MOD_2EXP l n"


82 
by (import bits SLICE_def)


83 


84 
consts


85 
LSBn :: "nat => bool"


86 


87 
defs


88 
LSBn_primdef: "LSBn == bit 0"


89 


90 
lemma LSBn_def: "LSBn = bit 0"


91 
by (import bits LSBn_def)


92 


93 
consts


94 
BITWISE :: "nat => (bool => bool => bool) => nat => nat => nat"


95 


96 
specification (BITWISE_primdef: BITWISE) BITWISE_def: "(ALL oper x y. BITWISE 0 oper x y = 0) &


97 
(ALL n oper x y.


98 
BITWISE (Suc n) oper x y =


99 
BITWISE n oper x y + SBIT (oper (bit n x) (bit n y)) n)"


100 
by (import bits BITWISE_def)


101 


102 
lemma DIV1: "ALL x::nat. x div (1::nat) = x"


103 
by (import bits DIV1)


104 


105 
lemma SUC_SUB: "Suc a  a = 1"


106 
by (import bits SUC_SUB)


107 


108 
lemma DIV_MULT_1: "ALL (r::nat) n::nat. r < n > (n + r) div n = (1::nat)"


109 
by (import bits DIV_MULT_1)


110 


111 
lemma ZERO_LT_TWOEXP: "ALL n::nat. (0::nat) < (2::nat) ^ n"


112 
by (import bits ZERO_LT_TWOEXP)


113 


114 
lemma MOD_2EXP_LT: "ALL (n::nat) k::nat. k mod (2::nat) ^ n < (2::nat) ^ n"


115 
by (import bits MOD_2EXP_LT)


116 


117 
lemma TWOEXP_DIVISION: "ALL (n::nat) k::nat.


118 
k = k div (2::nat) ^ n * (2::nat) ^ n + k mod (2::nat) ^ n"


119 
by (import bits TWOEXP_DIVISION)


120 


121 
lemma TWOEXP_MONO: "ALL (a::nat) b::nat. a < b > (2::nat) ^ a < (2::nat) ^ b"


122 
by (import bits TWOEXP_MONO)


123 


124 
lemma TWOEXP_MONO2: "ALL (a::nat) b::nat. a <= b > (2::nat) ^ a <= (2::nat) ^ b"


125 
by (import bits TWOEXP_MONO2)


126 


127 
lemma EXP_SUB_LESS_EQ: "ALL (a::nat) b::nat. (2::nat) ^ (a  b) <= (2::nat) ^ a"


128 
by (import bits EXP_SUB_LESS_EQ)


129 


130 
lemma BITS_THM: "ALL x xa xb. BITS x xa xb = xb div 2 ^ xa mod 2 ^ (Suc x  xa)"


131 
by (import bits BITS_THM)


132 


133 
lemma BITSLT_THM: "ALL h l n. BITS h l n < 2 ^ (Suc h  l)"


134 
by (import bits BITSLT_THM)


135 


136 
lemma DIV_MULT_LEM: "ALL (m::nat) n::nat. (0::nat) < n > m div n * n <= m"


137 
by (import bits DIV_MULT_LEM)


138 


139 
lemma MOD_2EXP_LEM: "ALL (n::nat) x::nat.


140 
n mod (2::nat) ^ x = n  n div (2::nat) ^ x * (2::nat) ^ x"


141 
by (import bits MOD_2EXP_LEM)


142 


143 
lemma BITS2_THM: "ALL h l n. BITS h l n = n mod 2 ^ Suc h div 2 ^ l"


144 
by (import bits BITS2_THM)


145 


146 
lemma BITS_COMP_THM: "ALL h1 l1 h2 l2 n.


147 
h2 + l1 <= h1 > BITS h2 l2 (BITS h1 l1 n) = BITS (h2 + l1) (l2 + l1) n"


148 
by (import bits BITS_COMP_THM)


149 


150 
lemma BITS_DIV_THM: "ALL h l x n. BITS h l x div 2 ^ n = BITS h (l + n) x"


151 
by (import bits BITS_DIV_THM)


152 


153 
lemma BITS_LT_HIGH: "ALL h l n. n < 2 ^ Suc h > BITS h l n = n div 2 ^ l"


154 
by (import bits BITS_LT_HIGH)


155 


156 
lemma BITS_ZERO: "ALL h l n. h < l > BITS h l n = 0"


157 
by (import bits BITS_ZERO)


158 


159 
lemma BITS_ZERO2: "ALL h l. BITS h l 0 = 0"


160 
by (import bits BITS_ZERO2)


161 


162 
lemma BITS_ZERO3: "ALL h x. BITS h 0 x = x mod 2 ^ Suc h"


163 
by (import bits BITS_ZERO3)


164 


165 
lemma BITS_COMP_THM2: "ALL h1 l1 h2 l2 n.


166 
BITS h2 l2 (BITS h1 l1 n) = BITS (min h1 (h2 + l1)) (l2 + l1) n"


167 
by (import bits BITS_COMP_THM2)


168 


169 
lemma NOT_MOD2_LEM: "ALL n::nat. (n mod (2::nat) ~= (0::nat)) = (n mod (2::nat) = (1::nat))"


170 
by (import bits NOT_MOD2_LEM)


171 


172 
lemma NOT_MOD2_LEM2: "ALL (n::nat) a::'a.


173 
(n mod (2::nat) ~= (1::nat)) = (n mod (2::nat) = (0::nat))"


174 
by (import bits NOT_MOD2_LEM2)


175 


176 
lemma EVEN_MOD2_LEM: "ALL n. EVEN n = (n mod 2 = 0)"


177 
by (import bits EVEN_MOD2_LEM)


178 


179 
lemma ODD_MOD2_LEM: "ALL n. ODD n = (n mod 2 = 1)"


180 
by (import bits ODD_MOD2_LEM)


181 


182 
lemma LSB_ODD: "LSBn = ODD"


183 
by (import bits LSB_ODD)


184 


185 
lemma DIV_MULT_THM: "ALL (x::nat) n::nat.


186 
n div (2::nat) ^ x * (2::nat) ^ x = n  n mod (2::nat) ^ x"


187 
by (import bits DIV_MULT_THM)


188 


189 
lemma DIV_MULT_THM2: "ALL x::nat. (2::nat) * (x div (2::nat)) = x  x mod (2::nat)"


190 
by (import bits DIV_MULT_THM2)


191 


192 
lemma LESS_EQ_EXP_MULT: "ALL (a::nat) b::nat. a <= b > (EX x::nat. (2::nat) ^ b = x * (2::nat) ^ a)"


193 
by (import bits LESS_EQ_EXP_MULT)


194 


195 
lemma SLICE_LEM1: "ALL (a::nat) (x::nat) y::nat.


196 
a div (2::nat) ^ (x + y) * (2::nat) ^ (x + y) =


197 
a div (2::nat) ^ x * (2::nat) ^ x 


198 
a div (2::nat) ^ x mod (2::nat) ^ y * (2::nat) ^ x"


199 
by (import bits SLICE_LEM1)


200 


201 
lemma SLICE_LEM2: "ALL (a::'a) (x::nat) y::nat.


202 
(n::nat) mod (2::nat) ^ (x + y) =


203 
n mod (2::nat) ^ x + n div (2::nat) ^ x mod (2::nat) ^ y * (2::nat) ^ x"


204 
by (import bits SLICE_LEM2)


205 


206 
lemma SLICE_LEM3: "ALL (n::nat) (h::nat) l::nat.


207 
l < h > n mod (2::nat) ^ Suc l <= n mod (2::nat) ^ h"


208 
by (import bits SLICE_LEM3)


209 


210 
lemma SLICE_THM: "ALL n h l. SLICE h l n = BITS h l n * 2 ^ l"


211 
by (import bits SLICE_THM)


212 


213 
lemma SLICELT_THM: "ALL h l n. SLICE h l n < 2 ^ Suc h"


214 
by (import bits SLICELT_THM)


215 


216 
lemma BITS_SLICE_THM: "ALL h l n. BITS h l (SLICE h l n) = BITS h l n"


217 
by (import bits BITS_SLICE_THM)


218 


219 
lemma BITS_SLICE_THM2: "ALL h l n. h <= h2 > BITS h2 l (SLICE h l n) = BITS h l n"


220 
by (import bits BITS_SLICE_THM2)


221 


222 
lemma MOD_2EXP_MONO: "ALL (n::nat) (h::nat) l::nat.


223 
l <= h > n mod (2::nat) ^ l <= n mod (2::nat) ^ Suc h"


224 
by (import bits MOD_2EXP_MONO)


225 


226 
lemma SLICE_COMP_THM: "ALL h m l n.


227 
Suc m <= h & l <= m > SLICE h (Suc m) n + SLICE m l n = SLICE h l n"


228 
by (import bits SLICE_COMP_THM)


229 


230 
lemma SLICE_ZERO: "ALL h l n. h < l > SLICE h l n = 0"


231 
by (import bits SLICE_ZERO)


232 


233 
lemma BIT_COMP_THM3: "ALL h m l n.


234 
Suc m <= h & l <= m >


235 
BITS h (Suc m) n * 2 ^ (Suc m  l) + BITS m l n = BITS h l n"


236 
by (import bits BIT_COMP_THM3)


237 


238 
lemma NOT_BIT: "ALL n a. (~ bit n a) = (BITS n n a = 0)"


239 
by (import bits NOT_BIT)


240 


241 
lemma NOT_BITS: "ALL n a. (BITS n n a ~= 0) = (BITS n n a = 1)"


242 
by (import bits NOT_BITS)


243 


244 
lemma NOT_BITS2: "ALL n a. (BITS n n a ~= 1) = (BITS n n a = 0)"


245 
by (import bits NOT_BITS2)


246 


247 
lemma BIT_SLICE: "ALL n a b. (bit n a = bit n b) = (SLICE n n a = SLICE n n b)"


248 
by (import bits BIT_SLICE)


249 


250 
lemma BIT_SLICE_LEM: "ALL y x n. SBIT (bit x n) (x + y) = SLICE x x n * 2 ^ y"


251 
by (import bits BIT_SLICE_LEM)


252 


253 
lemma BIT_SLICE_THM: "ALL x xa. SBIT (bit x xa) x = SLICE x x xa"


254 
by (import bits BIT_SLICE_THM)


255 


256 
lemma SBIT_DIV: "ALL b m n. n < m > SBIT b (m  n) = SBIT b m div 2 ^ n"


257 
by (import bits SBIT_DIV)


258 


259 
lemma BITS_SUC: "ALL h l n.


260 
l <= Suc h >


261 
SBIT (bit (Suc h) n) (Suc h  l) + BITS h l n = BITS (Suc h) l n"


262 
by (import bits BITS_SUC)


263 


264 
lemma BITS_SUC_THM: "ALL h l n.


265 
BITS (Suc h) l n =


266 
(if Suc h < l then 0 else SBIT (bit (Suc h) n) (Suc h  l) + BITS h l n)"


267 
by (import bits BITS_SUC_THM)


268 


269 
lemma BIT_BITS_THM: "ALL h l a b.


270 
(ALL x. l <= x & x <= h > bit x a = bit x b) =


271 
(BITS h l a = BITS h l b)"


272 
by (import bits BIT_BITS_THM)


273 


274 
lemma BITWISE_LT_2EXP: "ALL n oper a b. BITWISE n oper a b < 2 ^ n"


275 
by (import bits BITWISE_LT_2EXP)


276 


277 
lemma LESS_EXP_MULT2: "ALL (a::nat) b::nat.


278 
a < b >


279 
(EX x::nat. (2::nat) ^ b = (2::nat) ^ (x + (1::nat)) * (2::nat) ^ a)"


280 
by (import bits LESS_EXP_MULT2)


281 


282 
lemma BITWISE_THM: "ALL x n oper a b.


283 
x < n > bit x (BITWISE n oper a b) = oper (bit x a) (bit x b)"


284 
by (import bits BITWISE_THM)


285 


286 
lemma BITWISE_COR: "ALL x n oper a b.


287 
x < n >


288 
oper (bit x a) (bit x b) > BITWISE n oper a b div 2 ^ x mod 2 = 1"


289 
by (import bits BITWISE_COR)


290 


291 
lemma BITWISE_NOT_COR: "ALL x n oper a b.


292 
x < n >


293 
~ oper (bit x a) (bit x b) > BITWISE n oper a b div 2 ^ x mod 2 = 0"


294 
by (import bits BITWISE_NOT_COR)


295 


296 
lemma MOD_PLUS_RIGHT: "ALL n::nat.


297 
(0::nat) < n >


298 
(ALL (j::nat) k::nat. (j + k mod n) mod n = (j + k) mod n)"


299 
by (import bits MOD_PLUS_RIGHT)


300 


301 
lemma MOD_PLUS_1: "ALL n::nat.


302 
(0::nat) < n >


303 
(ALL x::nat.


304 
((x + (1::nat)) mod n = (0::nat)) = (x mod n + (1::nat) = n))"


305 
by (import bits MOD_PLUS_1)


306 


307 
lemma MOD_ADD_1: "ALL n::nat.


308 
(0::nat) < n >


309 
(ALL x::nat.


310 
(x + (1::nat)) mod n ~= (0::nat) >


311 
(x + (1::nat)) mod n = x mod n + (1::nat))"


312 
by (import bits MOD_ADD_1)


313 


314 
;end_setup


315 


316 
;setup_theory word32


317 


318 
consts


319 
HB :: "nat"


320 


321 
defs


322 
HB_primdef: "HB ==


323 
NUMERAL


324 
(NUMERAL_BIT1


325 
(NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))"


326 


327 
lemma HB_def: "HB =


328 
NUMERAL


329 
(NUMERAL_BIT1


330 
(NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))"


331 
by (import word32 HB_def)


332 


333 
consts


334 
WL :: "nat"


335 


336 
defs


337 
WL_primdef: "WL == Suc HB"


338 


339 
lemma WL_def: "WL = Suc HB"


340 
by (import word32 WL_def)


341 


342 
consts


343 
MODw :: "nat => nat"


344 


345 
defs


346 
MODw_primdef: "MODw == %n. n mod 2 ^ WL"


347 


348 
lemma MODw_def: "ALL n. MODw n = n mod 2 ^ WL"


349 
by (import word32 MODw_def)


350 


351 
consts


352 
INw :: "nat => bool"


353 


354 
defs


355 
INw_primdef: "INw == %n. n < 2 ^ WL"


356 


357 
lemma INw_def: "ALL n. INw n = (n < 2 ^ WL)"


358 
by (import word32 INw_def)


359 


360 
consts


361 
EQUIV :: "nat => nat => bool"


362 


363 
defs


364 
EQUIV_primdef: "EQUIV == %x y. MODw x = MODw y"


365 


366 
lemma EQUIV_def: "ALL x y. EQUIV x y = (MODw x = MODw y)"


367 
by (import word32 EQUIV_def)


368 


369 
lemma EQUIV_QT: "ALL x y. EQUIV x y = (EQUIV x = EQUIV y)"


370 
by (import word32 EQUIV_QT)


371 


372 
lemma FUNPOW_THM: "ALL f n x. (f ^ n) (f x) = f ((f ^ n) x)"


373 
by (import word32 FUNPOW_THM)


374 


375 
lemma FUNPOW_THM2: "ALL f n x. (f ^ Suc n) x = f ((f ^ n) x)"


376 
by (import word32 FUNPOW_THM2)


377 


378 
lemma FUNPOW_COMP: "ALL f m n a. (f ^ m) ((f ^ n) a) = (f ^ (m + n)) a"


379 
by (import word32 FUNPOW_COMP)


380 


381 
lemma INw_MODw: "ALL n. INw (MODw n)"


382 
by (import word32 INw_MODw)


383 


384 
lemma TOw_IDEM: "ALL a. INw a > MODw a = a"


385 
by (import word32 TOw_IDEM)


386 


387 
lemma MODw_IDEM2: "ALL a. MODw (MODw a) = MODw a"


388 
by (import word32 MODw_IDEM2)


389 


390 
lemma TOw_QT: "ALL a. EQUIV (MODw a) a"


391 
by (import word32 TOw_QT)


392 


393 
lemma MODw_THM: "MODw = BITS HB 0"


394 
by (import word32 MODw_THM)


395 


396 
lemma MOD_ADD: "ALL a b. MODw (a + b) = MODw (MODw a + MODw b)"


397 
by (import word32 MOD_ADD)


398 


399 
lemma MODw_MULT: "ALL a b. MODw (a * b) = MODw (MODw a * MODw b)"


400 
by (import word32 MODw_MULT)


401 


402 
consts


403 
AONE :: "nat"


404 


405 
defs


406 
AONE_primdef: "AONE == 1"


407 


408 
lemma AONE_def: "AONE = 1"


409 
by (import word32 AONE_def)


410 


411 
lemma ADD_QT: "(ALL n. EQUIV (0 + n) n) & (ALL m n. EQUIV (Suc m + n) (Suc (m + n)))"


412 
by (import word32 ADD_QT)


413 


414 
lemma ADD_0_QT: "ALL a. EQUIV (a + 0) a"


415 
by (import word32 ADD_0_QT)


416 


417 
lemma ADD_COMM_QT: "ALL a b. EQUIV (a + b) (b + a)"


418 
by (import word32 ADD_COMM_QT)


419 


420 
lemma ADD_ASSOC_QT: "ALL a b c. EQUIV (a + (b + c)) (a + b + c)"


421 
by (import word32 ADD_ASSOC_QT)


422 


423 
lemma MULT_QT: "(ALL n. EQUIV (0 * n) 0) & (ALL m n. EQUIV (Suc m * n) (m * n + n))"


424 
by (import word32 MULT_QT)


425 


426 
lemma ADD1_QT: "ALL m. EQUIV (Suc m) (m + AONE)"


427 
by (import word32 ADD1_QT)


428 


429 
lemma ADD_CLAUSES_QT: "(ALL m. EQUIV (0 + m) m) &


430 
(ALL m. EQUIV (m + 0) m) &


431 
(ALL m n. EQUIV (Suc m + n) (Suc (m + n))) &


432 
(ALL m n. EQUIV (m + Suc n) (Suc (m + n)))"


433 
by (import word32 ADD_CLAUSES_QT)


434 


435 
lemma SUC_EQUIV_COMP: "ALL a b. EQUIV (Suc a) b > EQUIV a (b + (2 ^ WL  1))"


436 
by (import word32 SUC_EQUIV_COMP)


437 


438 
lemma INV_SUC_EQ_QT: "ALL m n. EQUIV (Suc m) (Suc n) = EQUIV m n"


439 
by (import word32 INV_SUC_EQ_QT)


440 


441 
lemma ADD_INV_0_QT: "ALL m n. EQUIV (m + n) m > EQUIV n 0"


442 
by (import word32 ADD_INV_0_QT)


443 


444 
lemma ADD_INV_0_EQ_QT: "ALL m n. EQUIV (m + n) m = EQUIV n 0"


445 
by (import word32 ADD_INV_0_EQ_QT)


446 


447 
lemma EQ_ADD_LCANCEL_QT: "ALL m n p. EQUIV (m + n) (m + p) = EQUIV n p"


448 
by (import word32 EQ_ADD_LCANCEL_QT)


449 


450 
lemma EQ_ADD_RCANCEL_QT: "ALL x xa xb. EQUIV (x + xb) (xa + xb) = EQUIV x xa"


451 
by (import word32 EQ_ADD_RCANCEL_QT)


452 


453 
lemma LEFT_ADD_DISTRIB_QT: "ALL m n p. EQUIV (p * (m + n)) (p * m + p * n)"


454 
by (import word32 LEFT_ADD_DISTRIB_QT)


455 


456 
lemma MULT_ASSOC_QT: "ALL m n p. EQUIV (m * (n * p)) (m * n * p)"


457 
by (import word32 MULT_ASSOC_QT)


458 


459 
lemma MULT_COMM_QT: "ALL m n. EQUIV (m * n) (n * m)"


460 
by (import word32 MULT_COMM_QT)


461 


462 
lemma MULT_CLAUSES_QT: "ALL m n.


463 
EQUIV (0 * m) 0 &


464 
EQUIV (m * 0) 0 &


465 
EQUIV (AONE * m) m &


466 
EQUIV (m * AONE) m &


467 
EQUIV (Suc m * n) (m * n + n) & EQUIV (m * Suc n) (m + m * n)"


468 
by (import word32 MULT_CLAUSES_QT)


469 


470 
consts


471 
MSBn :: "nat => bool"


472 


473 
defs


474 
MSBn_primdef: "MSBn == bit HB"


475 


476 
lemma MSBn_def: "MSBn = bit HB"


477 
by (import word32 MSBn_def)


478 


479 
consts


480 
ONE_COMP :: "nat => nat"


481 


482 
defs


483 
ONE_COMP_primdef: "ONE_COMP == %x. 2 ^ WL  1  MODw x"


484 


485 
lemma ONE_COMP_def: "ALL x. ONE_COMP x = 2 ^ WL  1  MODw x"


486 
by (import word32 ONE_COMP_def)


487 


488 
consts


489 
TWO_COMP :: "nat => nat"


490 


491 
defs


492 
TWO_COMP_primdef: "TWO_COMP == %x. 2 ^ WL  MODw x"


493 


494 
lemma TWO_COMP_def: "ALL x. TWO_COMP x = 2 ^ WL  MODw x"


495 
by (import word32 TWO_COMP_def)


496 


497 
lemma ADD_TWO_COMP_QT: "ALL a. EQUIV (MODw a + TWO_COMP a) 0"


498 
by (import word32 ADD_TWO_COMP_QT)


499 


500 
lemma TWO_COMP_ONE_COMP_QT: "ALL a. EQUIV (TWO_COMP a) (ONE_COMP a + AONE)"


501 
by (import word32 TWO_COMP_ONE_COMP_QT)


502 

14847

503 
lemma BIT_EQUIV_THM: "(All::(nat => bool) => bool)


504 
(%x::nat.


505 
(All::(nat => bool) => bool)


506 
(%xa::nat.


507 
(op =::bool => bool => bool)


508 
((All::(nat => bool) => bool)


509 
(%xb::nat.


510 
(op >::bool => bool => bool)


511 
((op <::nat => nat => bool) xb (WL::nat))


512 
((op =::bool => bool => bool)


513 
((bit::nat => nat => bool) xb x)


514 
((bit::nat => nat => bool) xb xa))))


515 
((EQUIV::nat => nat => bool) x xa)))"

14516

516 
by (import word32 BIT_EQUIV_THM)


517 


518 
lemma BITS_SUC2: "ALL n a. BITS (Suc n) 0 a = SLICE (Suc n) (Suc n) a + BITS n 0 a"


519 
by (import word32 BITS_SUC2)


520 


521 
lemma BITWISE_ONE_COMP_THM: "ALL a b. BITWISE WL (%x y. ~ x) a b = ONE_COMP a"


522 
by (import word32 BITWISE_ONE_COMP_THM)


523 


524 
lemma ONE_COMP_THM: "ALL x xa. xa < WL > bit xa (ONE_COMP x) = (~ bit xa x)"


525 
by (import word32 ONE_COMP_THM)


526 


527 
consts


528 
OR :: "nat => nat => nat"


529 


530 
defs


531 
OR_primdef: "OR == BITWISE WL op "


532 


533 
lemma OR_def: "OR = BITWISE WL op "


534 
by (import word32 OR_def)


535 


536 
consts


537 
AND :: "nat => nat => nat"


538 


539 
defs


540 
AND_primdef: "AND == BITWISE WL op &"


541 


542 
lemma AND_def: "AND = BITWISE WL op &"


543 
by (import word32 AND_def)


544 


545 
consts


546 
EOR :: "nat => nat => nat"


547 


548 
defs


549 
EOR_primdef: "EOR == BITWISE WL (%x y. x ~= y)"


550 


551 
lemma EOR_def: "EOR = BITWISE WL (%x y. x ~= y)"


552 
by (import word32 EOR_def)


553 


554 
consts


555 
COMP0 :: "nat"


556 


557 
defs


558 
COMP0_primdef: "COMP0 == ONE_COMP 0"


559 


560 
lemma COMP0_def: "COMP0 = ONE_COMP 0"


561 
by (import word32 COMP0_def)


562 

14847

563 
lemma BITWISE_THM2: "(All::(nat => bool) => bool)


564 
(%y::nat.


565 
(All::((bool => bool => bool) => bool) => bool)


566 
(%oper::bool => bool => bool.


567 
(All::(nat => bool) => bool)


568 
(%a::nat.


569 
(All::(nat => bool) => bool)


570 
(%b::nat.


571 
(op =::bool => bool => bool)


572 
((All::(nat => bool) => bool)


573 
(%x::nat.


574 
(op >::bool => bool => bool)


575 
((op <::nat => nat => bool) x (WL::nat))


576 
((op =::bool => bool => bool)


577 
(oper ((bit::nat => nat => bool) x a)


578 
((bit::nat => nat => bool) x b))


579 
((bit::nat => nat => bool) x y))))


580 
((EQUIV::nat => nat => bool)


581 
((BITWISE::nat


582 
=> (bool => bool => bool)


583 
=> nat => nat => nat)


584 
(WL::nat) oper a b)


585 
y)))))"

14516

586 
by (import word32 BITWISE_THM2)


587 


588 
lemma OR_ASSOC_QT: "ALL a b c. EQUIV (OR a (OR b c)) (OR (OR a b) c)"


589 
by (import word32 OR_ASSOC_QT)


590 


591 
lemma OR_COMM_QT: "ALL a b. EQUIV (OR a b) (OR b a)"


592 
by (import word32 OR_COMM_QT)


593 


594 
lemma OR_ABSORB_QT: "ALL a b. EQUIV (AND a (OR a b)) a"


595 
by (import word32 OR_ABSORB_QT)


596 


597 
lemma OR_IDEM_QT: "ALL a. EQUIV (OR a a) a"


598 
by (import word32 OR_IDEM_QT)


599 


600 
lemma AND_ASSOC_QT: "ALL a b c. EQUIV (AND a (AND b c)) (AND (AND a b) c)"


601 
by (import word32 AND_ASSOC_QT)


602 


603 
lemma AND_COMM_QT: "ALL a b. EQUIV (AND a b) (AND b a)"


604 
by (import word32 AND_COMM_QT)


605 


606 
lemma AND_ABSORB_QT: "ALL a b. EQUIV (OR a (AND a b)) a"


607 
by (import word32 AND_ABSORB_QT)


608 


609 
lemma AND_IDEM_QT: "ALL a. EQUIV (AND a a) a"


610 
by (import word32 AND_IDEM_QT)


611 


612 
lemma OR_COMP_QT: "ALL a. EQUIV (OR a (ONE_COMP a)) COMP0"


613 
by (import word32 OR_COMP_QT)


614 


615 
lemma AND_COMP_QT: "ALL a. EQUIV (AND a (ONE_COMP a)) 0"


616 
by (import word32 AND_COMP_QT)


617 


618 
lemma ONE_COMP_QT: "ALL a. EQUIV (ONE_COMP (ONE_COMP a)) a"


619 
by (import word32 ONE_COMP_QT)


620 


621 
lemma RIGHT_AND_OVER_OR_QT: "ALL a b c. EQUIV (AND (OR a b) c) (OR (AND a c) (AND b c))"


622 
by (import word32 RIGHT_AND_OVER_OR_QT)


623 


624 
lemma RIGHT_OR_OVER_AND_QT: "ALL a b c. EQUIV (OR (AND a b) c) (AND (OR a c) (OR b c))"


625 
by (import word32 RIGHT_OR_OVER_AND_QT)


626 


627 
lemma DE_MORGAN_THM_QT: "ALL a b.


628 
EQUIV (ONE_COMP (AND a b)) (OR (ONE_COMP a) (ONE_COMP b)) &


629 
EQUIV (ONE_COMP (OR a b)) (AND (ONE_COMP a) (ONE_COMP b))"


630 
by (import word32 DE_MORGAN_THM_QT)


631 


632 
lemma BIT_EQUIV: "ALL n a b. n < WL > EQUIV a b > bit n a = bit n b"


633 
by (import word32 BIT_EQUIV)


634 


635 
lemma LSB_WELLDEF: "ALL a b. EQUIV a b > LSBn a = LSBn b"


636 
by (import word32 LSB_WELLDEF)


637 


638 
lemma MSB_WELLDEF: "ALL a b. EQUIV a b > MSBn a = MSBn b"


639 
by (import word32 MSB_WELLDEF)


640 


641 
lemma BITWISE_ISTEP: "ALL n oper a b.


642 
0 < n >


643 
BITWISE n oper (a div 2) (b div 2) =


644 
BITWISE n oper a b div 2 + SBIT (oper (bit n a) (bit n b)) (n  1)"


645 
by (import word32 BITWISE_ISTEP)


646 


647 
lemma BITWISE_EVAL: "ALL n oper a b.


648 
BITWISE (Suc n) oper a b =


649 
2 * BITWISE n oper (a div 2) (b div 2) + SBIT (oper (LSBn a) (LSBn b)) 0"


650 
by (import word32 BITWISE_EVAL)


651 


652 
lemma BITWISE_WELLDEF: "ALL n oper a b c d.


653 
EQUIV a b & EQUIV c d > EQUIV (BITWISE n oper a c) (BITWISE n oper b d)"


654 
by (import word32 BITWISE_WELLDEF)


655 


656 
lemma BITWISEw_WELLDEF: "ALL oper a b c d.


657 
EQUIV a b & EQUIV c d >


658 
EQUIV (BITWISE WL oper a c) (BITWISE WL oper b d)"


659 
by (import word32 BITWISEw_WELLDEF)


660 


661 
lemma SUC_WELLDEF: "ALL a b. EQUIV a b > EQUIV (Suc a) (Suc b)"


662 
by (import word32 SUC_WELLDEF)


663 


664 
lemma ADD_WELLDEF: "ALL a b c d. EQUIV a b & EQUIV c d > EQUIV (a + c) (b + d)"


665 
by (import word32 ADD_WELLDEF)


666 


667 
lemma MUL_WELLDEF: "ALL a b c d. EQUIV a b & EQUIV c d > EQUIV (a * c) (b * d)"


668 
by (import word32 MUL_WELLDEF)


669 


670 
lemma ONE_COMP_WELLDEF: "ALL a b. EQUIV a b > EQUIV (ONE_COMP a) (ONE_COMP b)"


671 
by (import word32 ONE_COMP_WELLDEF)


672 


673 
lemma TWO_COMP_WELLDEF: "ALL a b. EQUIV a b > EQUIV (TWO_COMP a) (TWO_COMP b)"


674 
by (import word32 TWO_COMP_WELLDEF)


675 


676 
lemma TOw_WELLDEF: "ALL a b. EQUIV a b > EQUIV (MODw a) (MODw b)"


677 
by (import word32 TOw_WELLDEF)


678 


679 
consts


680 
LSR_ONE :: "nat => nat"


681 


682 
defs


683 
LSR_ONE_primdef: "LSR_ONE == %a. MODw a div 2"


684 


685 
lemma LSR_ONE_def: "ALL a. LSR_ONE a = MODw a div 2"


686 
by (import word32 LSR_ONE_def)


687 


688 
consts


689 
ASR_ONE :: "nat => nat"


690 


691 
defs


692 
ASR_ONE_primdef: "ASR_ONE == %a. LSR_ONE a + SBIT (MSBn a) HB"


693 


694 
lemma ASR_ONE_def: "ALL a. ASR_ONE a = LSR_ONE a + SBIT (MSBn a) HB"


695 
by (import word32 ASR_ONE_def)


696 


697 
consts


698 
ROR_ONE :: "nat => nat"


699 


700 
defs


701 
ROR_ONE_primdef: "ROR_ONE == %a. LSR_ONE a + SBIT (LSBn a) HB"


702 


703 
lemma ROR_ONE_def: "ALL a. ROR_ONE a = LSR_ONE a + SBIT (LSBn a) HB"


704 
by (import word32 ROR_ONE_def)


705 


706 
consts


707 
RRXn :: "bool => nat => nat"


708 


709 
defs


710 
RRXn_primdef: "RRXn == %c a. LSR_ONE a + SBIT c HB"


711 


712 
lemma RRXn_def: "ALL c a. RRXn c a = LSR_ONE a + SBIT c HB"


713 
by (import word32 RRXn_def)


714 


715 
lemma LSR_ONE_WELLDEF: "ALL a b. EQUIV a b > EQUIV (LSR_ONE a) (LSR_ONE b)"


716 
by (import word32 LSR_ONE_WELLDEF)


717 


718 
lemma ASR_ONE_WELLDEF: "ALL a b. EQUIV a b > EQUIV (ASR_ONE a) (ASR_ONE b)"


719 
by (import word32 ASR_ONE_WELLDEF)


720 


721 
lemma ROR_ONE_WELLDEF: "ALL a b. EQUIV a b > EQUIV (ROR_ONE a) (ROR_ONE b)"


722 
by (import word32 ROR_ONE_WELLDEF)


723 


724 
lemma RRX_WELLDEF: "ALL a b c. EQUIV a b > EQUIV (RRXn c a) (RRXn c b)"


725 
by (import word32 RRX_WELLDEF)


726 


727 
lemma LSR_ONE: "LSR_ONE = BITS HB 1"


728 
by (import word32 LSR_ONE)


729 


730 
typedef (open) word32 = "{x. EX xa. x = EQUIV xa}"


731 
by (rule typedef_helper,import word32 word32_TY_DEF)


732 


733 
lemmas word32_TY_DEF = typedef_hol2hol4 [OF type_definition_word32]


734 


735 
consts


736 
mk_word32 :: "(nat => bool) => word32"


737 
dest_word32 :: "word32 => nat => bool"


738 


739 
specification (dest_word32 mk_word32) word32_tybij: "(ALL a. mk_word32 (dest_word32 a) = a) &


740 
(ALL r. (EX x. r = EQUIV x) = (dest_word32 (mk_word32 r) = r))"


741 
by (import word32 word32_tybij)


742 


743 
consts


744 
w_0 :: "word32"


745 


746 
defs


747 
w_0_primdef: "w_0 == mk_word32 (EQUIV 0)"


748 


749 
lemma w_0_def: "w_0 = mk_word32 (EQUIV 0)"


750 
by (import word32 w_0_def)


751 


752 
consts


753 
w_1 :: "word32"


754 


755 
defs


756 
w_1_primdef: "w_1 == mk_word32 (EQUIV AONE)"


757 


758 
lemma w_1_def: "w_1 = mk_word32 (EQUIV AONE)"


759 
by (import word32 w_1_def)


760 


761 
consts


762 
w_T :: "word32"


763 


764 
defs


765 
w_T_primdef: "w_T == mk_word32 (EQUIV COMP0)"


766 


767 
lemma w_T_def: "w_T = mk_word32 (EQUIV COMP0)"


768 
by (import word32 w_T_def)


769 


770 
constdefs


771 
word_suc :: "word32 => word32"


772 
"word_suc == %T1. mk_word32 (EQUIV (Suc (Eps (dest_word32 T1))))"


773 


774 
lemma word_suc: "ALL T1. word_suc T1 = mk_word32 (EQUIV (Suc (Eps (dest_word32 T1))))"


775 
by (import word32 word_suc)


776 


777 
constdefs


778 
word_add :: "word32 => word32 => word32"


779 
"word_add ==


780 
%T1 T2. mk_word32 (EQUIV (Eps (dest_word32 T1) + Eps (dest_word32 T2)))"


781 


782 
lemma word_add: "ALL T1 T2.


783 
word_add T1 T2 =


784 
mk_word32 (EQUIV (Eps (dest_word32 T1) + Eps (dest_word32 T2)))"


785 
by (import word32 word_add)


786 


787 
constdefs


788 
word_mul :: "word32 => word32 => word32"


789 
"word_mul ==


790 
%T1 T2. mk_word32 (EQUIV (Eps (dest_word32 T1) * Eps (dest_word32 T2)))"


791 


792 
lemma word_mul: "ALL T1 T2.


793 
word_mul T1 T2 =


794 
mk_word32 (EQUIV (Eps (dest_word32 T1) * Eps (dest_word32 T2)))"


795 
by (import word32 word_mul)


796 


797 
constdefs


798 
word_1comp :: "word32 => word32"


799 
"word_1comp == %T1. mk_word32 (EQUIV (ONE_COMP (Eps (dest_word32 T1))))"


800 


801 
lemma word_1comp: "ALL T1. word_1comp T1 = mk_word32 (EQUIV (ONE_COMP (Eps (dest_word32 T1))))"


802 
by (import word32 word_1comp)


803 


804 
constdefs


805 
word_2comp :: "word32 => word32"


806 
"word_2comp == %T1. mk_word32 (EQUIV (TWO_COMP (Eps (dest_word32 T1))))"


807 


808 
lemma word_2comp: "ALL T1. word_2comp T1 = mk_word32 (EQUIV (TWO_COMP (Eps (dest_word32 T1))))"


809 
by (import word32 word_2comp)


810 


811 
constdefs


812 
word_lsr1 :: "word32 => word32"


813 
"word_lsr1 == %T1. mk_word32 (EQUIV (LSR_ONE (Eps (dest_word32 T1))))"


814 


815 
lemma word_lsr1: "ALL T1. word_lsr1 T1 = mk_word32 (EQUIV (LSR_ONE (Eps (dest_word32 T1))))"


816 
by (import word32 word_lsr1)


817 


818 
constdefs


819 
word_asr1 :: "word32 => word32"


820 
"word_asr1 == %T1. mk_word32 (EQUIV (ASR_ONE (Eps (dest_word32 T1))))"


821 


822 
lemma word_asr1: "ALL T1. word_asr1 T1 = mk_word32 (EQUIV (ASR_ONE (Eps (dest_word32 T1))))"


823 
by (import word32 word_asr1)


824 


825 
constdefs


826 
word_ror1 :: "word32 => word32"


827 
"word_ror1 == %T1. mk_word32 (EQUIV (ROR_ONE (Eps (dest_word32 T1))))"


828 


829 
lemma word_ror1: "ALL T1. word_ror1 T1 = mk_word32 (EQUIV (ROR_ONE (Eps (dest_word32 T1))))"


830 
by (import word32 word_ror1)


831 


832 
consts


833 
RRX :: "bool => word32 => word32"


834 


835 
defs


836 
RRX_primdef: "RRX == %T1 T2. mk_word32 (EQUIV (RRXn T1 (Eps (dest_word32 T2))))"


837 


838 
lemma RRX_def: "ALL T1 T2. RRX T1 T2 = mk_word32 (EQUIV (RRXn T1 (Eps (dest_word32 T2))))"


839 
by (import word32 RRX_def)


840 


841 
consts


842 
LSB :: "word32 => bool"


843 


844 
defs


845 
LSB_primdef: "LSB == %T1. LSBn (Eps (dest_word32 T1))"


846 


847 
lemma LSB_def: "ALL T1. LSB T1 = LSBn (Eps (dest_word32 T1))"


848 
by (import word32 LSB_def)


849 


850 
consts


851 
MSB :: "word32 => bool"


852 


853 
defs


854 
MSB_primdef: "MSB == %T1. MSBn (Eps (dest_word32 T1))"


855 


856 
lemma MSB_def: "ALL T1. MSB T1 = MSBn (Eps (dest_word32 T1))"


857 
by (import word32 MSB_def)


858 


859 
constdefs


860 
bitwise_or :: "word32 => word32 => word32"


861 
"bitwise_or ==


862 
%T1 T2. mk_word32 (EQUIV (OR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))"


863 


864 
lemma bitwise_or: "ALL T1 T2.


865 
bitwise_or T1 T2 =


866 
mk_word32 (EQUIV (OR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))"


867 
by (import word32 bitwise_or)


868 


869 
constdefs


870 
bitwise_eor :: "word32 => word32 => word32"


871 
"bitwise_eor ==


872 
%T1 T2.


873 
mk_word32 (EQUIV (EOR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))"


874 


875 
lemma bitwise_eor: "ALL T1 T2.


876 
bitwise_eor T1 T2 =


877 
mk_word32 (EQUIV (EOR (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))"


878 
by (import word32 bitwise_eor)


879 


880 
constdefs


881 
bitwise_and :: "word32 => word32 => word32"


882 
"bitwise_and ==


883 
%T1 T2.


884 
mk_word32 (EQUIV (AND (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))"


885 


886 
lemma bitwise_and: "ALL T1 T2.


887 
bitwise_and T1 T2 =


888 
mk_word32 (EQUIV (AND (Eps (dest_word32 T1)) (Eps (dest_word32 T2))))"


889 
by (import word32 bitwise_and)


890 


891 
consts


892 
TOw :: "word32 => word32"


893 


894 
defs


895 
TOw_primdef: "TOw == %T1. mk_word32 (EQUIV (MODw (Eps (dest_word32 T1))))"


896 


897 
lemma TOw_def: "ALL T1. TOw T1 = mk_word32 (EQUIV (MODw (Eps (dest_word32 T1))))"


898 
by (import word32 TOw_def)


899 


900 
consts


901 
n2w :: "nat => word32"


902 


903 
defs


904 
n2w_primdef: "n2w == %n. mk_word32 (EQUIV n)"


905 


906 
lemma n2w_def: "ALL n. n2w n = mk_word32 (EQUIV n)"


907 
by (import word32 n2w_def)


908 


909 
consts


910 
w2n :: "word32 => nat"


911 


912 
defs


913 
w2n_primdef: "w2n == %w. MODw (Eps (dest_word32 w))"


914 


915 
lemma w2n_def: "ALL w. w2n w = MODw (Eps (dest_word32 w))"


916 
by (import word32 w2n_def)


917 


918 
lemma ADDw: "(ALL x. word_add w_0 x = x) &


919 
(ALL x xa. word_add (word_suc x) xa = word_suc (word_add x xa))"


920 
by (import word32 ADDw)


921 


922 
lemma ADD_0w: "ALL x. word_add x w_0 = x"


923 
by (import word32 ADD_0w)


924 


925 
lemma ADD1w: "ALL x. word_suc x = word_add x w_1"


926 
by (import word32 ADD1w)


927 


928 
lemma ADD_ASSOCw: "ALL x xa xb. word_add x (word_add xa xb) = word_add (word_add x xa) xb"


929 
by (import word32 ADD_ASSOCw)


930 


931 
lemma ADD_CLAUSESw: "(ALL x. word_add w_0 x = x) &


932 
(ALL x. word_add x w_0 = x) &


933 
(ALL x xa. word_add (word_suc x) xa = word_suc (word_add x xa)) &


934 
(ALL x xa. word_add x (word_suc xa) = word_suc (word_add x xa))"


935 
by (import word32 ADD_CLAUSESw)


936 


937 
lemma ADD_COMMw: "ALL x xa. word_add x xa = word_add xa x"


938 
by (import word32 ADD_COMMw)


939 


940 
lemma ADD_INV_0_EQw: "ALL x xa. (word_add x xa = x) = (xa = w_0)"


941 
by (import word32 ADD_INV_0_EQw)


942 


943 
lemma EQ_ADD_LCANCELw: "ALL x xa xb. (word_add x xa = word_add x xb) = (xa = xb)"


944 
by (import word32 EQ_ADD_LCANCELw)


945 


946 
lemma EQ_ADD_RCANCELw: "ALL x xa xb. (word_add x xb = word_add xa xb) = (x = xa)"


947 
by (import word32 EQ_ADD_RCANCELw)


948 


949 
lemma LEFT_ADD_DISTRIBw: "ALL x xa xb.


950 
word_mul xb (word_add x xa) = word_add (word_mul xb x) (word_mul xb xa)"


951 
by (import word32 LEFT_ADD_DISTRIBw)


952 


953 
lemma MULT_ASSOCw: "ALL x xa xb. word_mul x (word_mul xa xb) = word_mul (word_mul x xa) xb"


954 
by (import word32 MULT_ASSOCw)


955 


956 
lemma MULT_COMMw: "ALL x xa. word_mul x xa = word_mul xa x"


957 
by (import word32 MULT_COMMw)


958 


959 
lemma MULT_CLAUSESw: "ALL x xa.


960 
word_mul w_0 x = w_0 &


961 
word_mul x w_0 = w_0 &


962 
word_mul w_1 x = x &


963 
word_mul x w_1 = x &


964 
word_mul (word_suc x) xa = word_add (word_mul x xa) xa &


965 
word_mul x (word_suc xa) = word_add x (word_mul x xa)"


966 
by (import word32 MULT_CLAUSESw)


967 


968 
lemma TWO_COMP_ONE_COMP: "ALL x. word_2comp x = word_add (word_1comp x) w_1"


969 
by (import word32 TWO_COMP_ONE_COMP)


970 


971 
lemma OR_ASSOCw: "ALL x xa xb.


972 
bitwise_or x (bitwise_or xa xb) = bitwise_or (bitwise_or x xa) xb"


973 
by (import word32 OR_ASSOCw)


974 


975 
lemma OR_COMMw: "ALL x xa. bitwise_or x xa = bitwise_or xa x"


976 
by (import word32 OR_COMMw)


977 


978 
lemma OR_IDEMw: "ALL x. bitwise_or x x = x"


979 
by (import word32 OR_IDEMw)


980 


981 
lemma OR_ABSORBw: "ALL x xa. bitwise_and x (bitwise_or x xa) = x"


982 
by (import word32 OR_ABSORBw)


983 


984 
lemma AND_ASSOCw: "ALL x xa xb.


985 
bitwise_and x (bitwise_and xa xb) = bitwise_and (bitwise_and x xa) xb"


986 
by (import word32 AND_ASSOCw)


987 


988 
lemma AND_COMMw: "ALL x xa. bitwise_and x xa = bitwise_and xa x"


989 
by (import word32 AND_COMMw)


990 


991 
lemma AND_IDEMw: "ALL x. bitwise_and x x = x"


992 
by (import word32 AND_IDEMw)


993 


994 
lemma AND_ABSORBw: "ALL x xa. bitwise_or x (bitwise_and x xa) = x"


995 
by (import word32 AND_ABSORBw)


996 


997 
lemma ONE_COMPw: "ALL x. word_1comp (word_1comp x) = x"


998 
by (import word32 ONE_COMPw)


999 


1000 
lemma RIGHT_AND_OVER_ORw: "ALL x xa xb.


1001 
bitwise_and (bitwise_or x xa) xb =


1002 
bitwise_or (bitwise_and x xb) (bitwise_and xa xb)"


1003 
by (import word32 RIGHT_AND_OVER_ORw)


1004 


1005 
lemma RIGHT_OR_OVER_ANDw: "ALL x xa xb.


1006 
bitwise_or (bitwise_and x xa) xb =


1007 
bitwise_and (bitwise_or x xb) (bitwise_or xa xb)"


1008 
by (import word32 RIGHT_OR_OVER_ANDw)


1009 


1010 
lemma DE_MORGAN_THMw: "ALL x xa.


1011 
word_1comp (bitwise_and x xa) =


1012 
bitwise_or (word_1comp x) (word_1comp xa) &


1013 
word_1comp (bitwise_or x xa) = bitwise_and (word_1comp x) (word_1comp xa)"


1014 
by (import word32 DE_MORGAN_THMw)


1015 


1016 
lemma w_0: "w_0 = n2w 0"


1017 
by (import word32 w_0)


1018 


1019 
lemma w_1: "w_1 = n2w 1"


1020 
by (import word32 w_1)


1021 


1022 
lemma w_T: "w_T =


1023 
n2w (NUMERAL


1024 
(NUMERAL_BIT1


1025 
(NUMERAL_BIT1


1026 
(NUMERAL_BIT1


1027 
(NUMERAL_BIT1


1028 
(NUMERAL_BIT1


1029 
(NUMERAL_BIT1


1030 
(NUMERAL_BIT1


1031 
(NUMERAL_BIT1


1032 
(NUMERAL_BIT1


1033 
(NUMERAL_BIT1


1034 
(NUMERAL_BIT1


1035 
(NUMERAL_BIT1


1036 
(NUMERAL_BIT1


1037 
(NUMERAL_BIT1


1038 
(NUMERAL_BIT1


1039 
(NUMERAL_BIT1


1040 
(NUMERAL_BIT1


1041 
(NUMERAL_BIT1


1042 
(NUMERAL_BIT1


1043 
(NUMERAL_BIT1


1044 
(NUMERAL_BIT1


1045 
(NUMERAL_BIT1


1046 
(NUMERAL_BIT1


1047 
(NUMERAL_BIT1


1048 
(NUMERAL_BIT1


1049 
(NUMERAL_BIT1


1050 
(NUMERAL_BIT1


1051 
(NUMERAL_BIT1


1052 
(NUMERAL_BIT1


1053 
(NUMERAL_BIT1


1054 
(NUMERAL_BIT1


1055 
(NUMERAL_BIT1


1056 
ALT_ZERO)))))))))))))))))))))))))))))))))"


1057 
by (import word32 w_T)


1058 


1059 
lemma ADD_TWO_COMP: "ALL x. word_add x (word_2comp x) = w_0"


1060 
by (import word32 ADD_TWO_COMP)


1061 


1062 
lemma ADD_TWO_COMP2: "ALL x. word_add (word_2comp x) x = w_0"


1063 
by (import word32 ADD_TWO_COMP2)


1064 


1065 
constdefs


1066 
word_sub :: "word32 => word32 => word32"


1067 
"word_sub == %a b. word_add a (word_2comp b)"


1068 


1069 
lemma word_sub: "ALL a b. word_sub a b = word_add a (word_2comp b)"


1070 
by (import word32 word_sub)


1071 


1072 
constdefs


1073 
word_lsl :: "word32 => nat => word32"


1074 
"word_lsl == %a n. word_mul a (n2w (2 ^ n))"


1075 


1076 
lemma word_lsl: "ALL a n. word_lsl a n = word_mul a (n2w (2 ^ n))"


1077 
by (import word32 word_lsl)


1078 


1079 
constdefs


1080 
word_lsr :: "word32 => nat => word32"


1081 
"word_lsr == %a n. (word_lsr1 ^ n) a"


1082 


1083 
lemma word_lsr: "ALL a n. word_lsr a n = (word_lsr1 ^ n) a"


1084 
by (import word32 word_lsr)


1085 


1086 
constdefs


1087 
word_asr :: "word32 => nat => word32"


1088 
"word_asr == %a n. (word_asr1 ^ n) a"


1089 


1090 
lemma word_asr: "ALL a n. word_asr a n = (word_asr1 ^ n) a"


1091 
by (import word32 word_asr)


1092 


1093 
constdefs


1094 
word_ror :: "word32 => nat => word32"


1095 
"word_ror == %a n. (word_ror1 ^ n) a"


1096 


1097 
lemma word_ror: "ALL a n. word_ror a n = (word_ror1 ^ n) a"


1098 
by (import word32 word_ror)


1099 


1100 
consts


1101 
BITw :: "nat => word32 => bool"


1102 


1103 
defs


1104 
BITw_primdef: "BITw == %b n. bit b (w2n n)"


1105 


1106 
lemma BITw_def: "ALL b n. BITw b n = bit b (w2n n)"


1107 
by (import word32 BITw_def)


1108 


1109 
consts


1110 
BITSw :: "nat => nat => word32 => nat"


1111 


1112 
defs


1113 
BITSw_primdef: "BITSw == %h l n. BITS h l (w2n n)"


1114 


1115 
lemma BITSw_def: "ALL h l n. BITSw h l n = BITS h l (w2n n)"


1116 
by (import word32 BITSw_def)


1117 


1118 
consts


1119 
SLICEw :: "nat => nat => word32 => nat"


1120 


1121 
defs


1122 
SLICEw_primdef: "SLICEw == %h l n. SLICE h l (w2n n)"


1123 


1124 
lemma SLICEw_def: "ALL h l n. SLICEw h l n = SLICE h l (w2n n)"


1125 
by (import word32 SLICEw_def)


1126 


1127 
lemma TWO_COMP_ADD: "ALL a b. word_2comp (word_add a b) = word_add (word_2comp a) (word_2comp b)"


1128 
by (import word32 TWO_COMP_ADD)


1129 


1130 
lemma TWO_COMP_ELIM: "ALL a. word_2comp (word_2comp a) = a"


1131 
by (import word32 TWO_COMP_ELIM)


1132 


1133 
lemma ADD_SUB_ASSOC: "ALL a b c. word_sub (word_add a b) c = word_add a (word_sub b c)"


1134 
by (import word32 ADD_SUB_ASSOC)


1135 


1136 
lemma ADD_SUB_SYM: "ALL a b c. word_sub (word_add a b) c = word_add (word_sub a c) b"


1137 
by (import word32 ADD_SUB_SYM)


1138 


1139 
lemma SUB_EQUALw: "ALL a. word_sub a a = w_0"


1140 
by (import word32 SUB_EQUALw)


1141 


1142 
lemma ADD_SUBw: "ALL a b. word_sub (word_add a b) b = a"


1143 
by (import word32 ADD_SUBw)


1144 


1145 
lemma SUB_SUBw: "ALL a b c. word_sub a (word_sub b c) = word_sub (word_add a c) b"


1146 
by (import word32 SUB_SUBw)


1147 


1148 
lemma ONE_COMP_TWO_COMP: "ALL a. word_1comp a = word_sub (word_2comp a) w_1"


1149 
by (import word32 ONE_COMP_TWO_COMP)


1150 


1151 
lemma SUBw: "ALL m n. word_sub (word_suc m) n = word_suc (word_sub m n)"


1152 
by (import word32 SUBw)


1153 


1154 
lemma ADD_EQ_SUBw: "ALL m n p. (word_add m n = p) = (m = word_sub p n)"


1155 
by (import word32 ADD_EQ_SUBw)


1156 


1157 
lemma CANCEL_SUBw: "ALL m n p. (word_sub n p = word_sub m p) = (n = m)"


1158 
by (import word32 CANCEL_SUBw)


1159 


1160 
lemma SUB_PLUSw: "ALL a b c. word_sub a (word_add b c) = word_sub (word_sub a b) c"


1161 
by (import word32 SUB_PLUSw)


1162 


1163 
lemma word_nchotomy: "ALL w. EX n. w = n2w n"


1164 
by (import word32 word_nchotomy)


1165 


1166 
lemma dest_word_mk_word_eq3: "ALL a. dest_word32 (mk_word32 (EQUIV a)) = EQUIV a"


1167 
by (import word32 dest_word_mk_word_eq3)


1168 


1169 
lemma MODw_ELIM: "ALL n. n2w (MODw n) = n2w n"


1170 
by (import word32 MODw_ELIM)


1171 


1172 
lemma w2n_EVAL: "ALL n. w2n (n2w n) = MODw n"


1173 
by (import word32 w2n_EVAL)


1174 


1175 
lemma w2n_ELIM: "ALL a. n2w (w2n a) = a"


1176 
by (import word32 w2n_ELIM)


1177 


1178 
lemma n2w_11: "ALL a b. (n2w a = n2w b) = (MODw a = MODw b)"


1179 
by (import word32 n2w_11)


1180 


1181 
lemma ADD_EVAL: "word_add (n2w a) (n2w b) = n2w (a + b)"


1182 
by (import word32 ADD_EVAL)


1183 


1184 
lemma MUL_EVAL: "word_mul (n2w a) (n2w b) = n2w (a * b)"


1185 
by (import word32 MUL_EVAL)


1186 


1187 
lemma ONE_COMP_EVAL: "word_1comp (n2w a) = n2w (ONE_COMP a)"


1188 
by (import word32 ONE_COMP_EVAL)


1189 


1190 
lemma TWO_COMP_EVAL: "word_2comp (n2w a) = n2w (TWO_COMP a)"


1191 
by (import word32 TWO_COMP_EVAL)


1192 


1193 
lemma LSR_ONE_EVAL: "word_lsr1 (n2w a) = n2w (LSR_ONE a)"


1194 
by (import word32 LSR_ONE_EVAL)


1195 


1196 
lemma ASR_ONE_EVAL: "word_asr1 (n2w a) = n2w (ASR_ONE a)"


1197 
by (import word32 ASR_ONE_EVAL)


1198 


1199 
lemma ROR_ONE_EVAL: "word_ror1 (n2w a) = n2w (ROR_ONE a)"


1200 
by (import word32 ROR_ONE_EVAL)


1201 


1202 
lemma RRX_EVAL: "RRX c (n2w a) = n2w (RRXn c a)"


1203 
by (import word32 RRX_EVAL)


1204 


1205 
lemma LSB_EVAL: "LSB (n2w a) = LSBn a"


1206 
by (import word32 LSB_EVAL)


1207 


1208 
lemma MSB_EVAL: "MSB (n2w a) = MSBn a"


1209 
by (import word32 MSB_EVAL)


1210 


1211 
lemma OR_EVAL: "bitwise_or (n2w a) (n2w b) = n2w (OR a b)"


1212 
by (import word32 OR_EVAL)


1213 


1214 
lemma EOR_EVAL: "bitwise_eor (n2w a) (n2w b) = n2w (EOR a b)"


1215 
by (import word32 EOR_EVAL)


1216 


1217 
lemma AND_EVAL: "bitwise_and (n2w a) (n2w b) = n2w (AND a b)"


1218 
by (import word32 AND_EVAL)


1219 


1220 
lemma BITS_EVAL: "ALL h l a. BITSw h l (n2w a) = BITS h l (MODw a)"


1221 
by (import word32 BITS_EVAL)


1222 


1223 
lemma BIT_EVAL: "ALL b a. BITw b (n2w a) = bit b (MODw a)"


1224 
by (import word32 BIT_EVAL)


1225 


1226 
lemma SLICE_EVAL: "ALL h l a. SLICEw h l (n2w a) = SLICE h l (MODw a)"


1227 
by (import word32 SLICE_EVAL)


1228 


1229 
lemma LSL_ADD: "ALL a m n. word_lsl (word_lsl a m) n = word_lsl a (m + n)"


1230 
by (import word32 LSL_ADD)


1231 


1232 
lemma LSR_ADD: "ALL x xa xb. word_lsr (word_lsr x xa) xb = word_lsr x (xa + xb)"


1233 
by (import word32 LSR_ADD)


1234 


1235 
lemma ASR_ADD: "ALL x xa xb. word_asr (word_asr x xa) xb = word_asr x (xa + xb)"


1236 
by (import word32 ASR_ADD)


1237 


1238 
lemma ROR_ADD: "ALL x xa xb. word_ror (word_ror x xa) xb = word_ror x (xa + xb)"


1239 
by (import word32 ROR_ADD)


1240 


1241 
lemma LSL_LIMIT: "ALL w n. HB < n > word_lsl w n = w_0"


1242 
by (import word32 LSL_LIMIT)


1243 


1244 
lemma MOD_MOD_DIV: "ALL a b. INw (MODw a div 2 ^ b)"


1245 
by (import word32 MOD_MOD_DIV)


1246 


1247 
lemma MOD_MOD_DIV_2EXP: "ALL a n. MODw (MODw a div 2 ^ n) div 2 = MODw a div 2 ^ Suc n"


1248 
by (import word32 MOD_MOD_DIV_2EXP)


1249 


1250 
lemma LSR_EVAL: "ALL n. word_lsr (n2w a) n = n2w (MODw a div 2 ^ n)"


1251 
by (import word32 LSR_EVAL)


1252 


1253 
lemma LSR_THM: "ALL x n. word_lsr (n2w n) x = n2w (BITS HB (min WL x) n)"


1254 
by (import word32 LSR_THM)


1255 


1256 
lemma LSR_LIMIT: "ALL x w. HB < x > word_lsr w x = w_0"


1257 
by (import word32 LSR_LIMIT)


1258 


1259 
lemma LEFT_SHIFT_LESS: "ALL (n::nat) (m::nat) a::nat.


1260 
a < (2::nat) ^ m >


1261 
(2::nat) ^ n + a * (2::nat) ^ n <= (2::nat) ^ (m + n)"


1262 
by (import word32 LEFT_SHIFT_LESS)


1263 


1264 
lemma ROR_THM: "ALL x n.


1265 
word_ror (n2w n) x =


1266 
(let x' = x mod WL


1267 
in n2w (BITS HB x' n + BITS (x'  1) 0 n * 2 ^ (WL  x')))"


1268 
by (import word32 ROR_THM)


1269 


1270 
lemma ROR_CYCLE: "ALL x w. word_ror w (x * WL) = w"


1271 
by (import word32 ROR_CYCLE)


1272 


1273 
lemma ASR_THM: "ALL x n.


1274 
word_asr (n2w n) x =


1275 
(let x' = min HB x; s = BITS HB x' n


1276 
in n2w (if MSBn n then 2 ^ WL  2 ^ (WL  x') + s else s))"


1277 
by (import word32 ASR_THM)


1278 


1279 
lemma ASR_LIMIT: "ALL x w. HB <= x > word_asr w x = (if MSB w then w_T else w_0)"


1280 
by (import word32 ASR_LIMIT)


1281 


1282 
lemma ZERO_SHIFT: "(ALL n. word_lsl w_0 n = w_0) &


1283 
(ALL n. word_asr w_0 n = w_0) &


1284 
(ALL n. word_lsr w_0 n = w_0) & (ALL n. word_ror w_0 n = w_0)"


1285 
by (import word32 ZERO_SHIFT)


1286 


1287 
lemma ZERO_SHIFT2: "(ALL a. word_lsl a 0 = a) &


1288 
(ALL a. word_asr a 0 = a) &


1289 
(ALL a. word_lsr a 0 = a) & (ALL a. word_ror a 0 = a)"


1290 
by (import word32 ZERO_SHIFT2)


1291 


1292 
lemma ASR_w_T: "ALL n. word_asr w_T n = w_T"


1293 
by (import word32 ASR_w_T)


1294 


1295 
lemma ROR_w_T: "ALL n. word_ror w_T n = w_T"


1296 
by (import word32 ROR_w_T)


1297 


1298 
lemma MODw_EVAL: "ALL x.


1299 
MODw x =


1300 
x mod


1301 
NUMERAL


1302 
(NUMERAL_BIT2


1303 
(NUMERAL_BIT1


1304 
(NUMERAL_BIT1


1305 
(NUMERAL_BIT1


1306 
(NUMERAL_BIT1


1307 
(NUMERAL_BIT1


1308 
(NUMERAL_BIT1


1309 
(NUMERAL_BIT1


1310 
(NUMERAL_BIT1


1311 
(NUMERAL_BIT1


1312 
(NUMERAL_BIT1


1313 
(NUMERAL_BIT1


1314 
(NUMERAL_BIT1


1315 
(NUMERAL_BIT1


1316 
(NUMERAL_BIT1


1317 
(NUMERAL_BIT1


1318 
(NUMERAL_BIT1


1319 
(NUMERAL_BIT1


1320 
(NUMERAL_BIT1


1321 
(NUMERAL_BIT1


1322 
(NUMERAL_BIT1


1323 
(NUMERAL_BIT1


1324 
(NUMERAL_BIT1


1325 
(NUMERAL_BIT1


1326 
(NUMERAL_BIT1


1327 
(NUMERAL_BIT1


1328 
(NUMERAL_BIT1


1329 
(NUMERAL_BIT1


1330 
(NUMERAL_BIT1


1331 
(NUMERAL_BIT1


1332 
(NUMERAL_BIT1


1333 
(NUMERAL_BIT1


1334 
ALT_ZERO))))))))))))))))))))))))))))))))"


1335 
by (import word32 MODw_EVAL)


1336 


1337 
lemma ADD_EVAL2: "ALL b a. word_add (n2w a) (n2w b) = n2w (MODw (a + b))"


1338 
by (import word32 ADD_EVAL2)


1339 


1340 
lemma MUL_EVAL2: "ALL b a. word_mul (n2w a) (n2w b) = n2w (MODw (a * b))"


1341 
by (import word32 MUL_EVAL2)


1342 


1343 
lemma ONE_COMP_EVAL2: "ALL a.


1344 
word_1comp (n2w a) =


1345 
n2w (2 ^


1346 
NUMERAL


1347 
(NUMERAL_BIT2


1348 
(NUMERAL_BIT1


1349 
(NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO))))) 


1350 
1 


1351 
MODw a)"


1352 
by (import word32 ONE_COMP_EVAL2)


1353 


1354 
lemma TWO_COMP_EVAL2: "ALL a.


1355 
word_2comp (n2w a) =


1356 
n2w (MODw


1357 
(2 ^


1358 
NUMERAL


1359 
(NUMERAL_BIT2


1360 
(NUMERAL_BIT1


1361 
(NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO))))) 


1362 
MODw a))"


1363 
by (import word32 TWO_COMP_EVAL2)


1364 


1365 
lemma LSR_ONE_EVAL2: "ALL a. word_lsr1 (n2w a) = n2w (MODw a div 2)"


1366 
by (import word32 LSR_ONE_EVAL2)


1367 


1368 
lemma ASR_ONE_EVAL2: "ALL a.


1369 
word_asr1 (n2w a) =


1370 
n2w (MODw a div 2 +


1371 
SBIT (MSBn a)


1372 
(NUMERAL


1373 
(NUMERAL_BIT1


1374 
(NUMERAL_BIT1


1375 
(NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))))"


1376 
by (import word32 ASR_ONE_EVAL2)


1377 


1378 
lemma ROR_ONE_EVAL2: "ALL a.


1379 
word_ror1 (n2w a) =


1380 
n2w (MODw a div 2 +


1381 
SBIT (LSBn a)


1382 
(NUMERAL


1383 
(NUMERAL_BIT1


1384 
(NUMERAL_BIT1


1385 
(NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))))"


1386 
by (import word32 ROR_ONE_EVAL2)


1387 


1388 
lemma RRX_EVAL2: "ALL c a.


1389 
RRX c (n2w a) =


1390 
n2w (MODw a div 2 +


1391 
SBIT c


1392 
(NUMERAL


1393 
(NUMERAL_BIT1


1394 
(NUMERAL_BIT1


1395 
(NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO)))))))"


1396 
by (import word32 RRX_EVAL2)


1397 


1398 
lemma LSB_EVAL2: "ALL a. LSB (n2w a) = ODD a"


1399 
by (import word32 LSB_EVAL2)


1400 


1401 
lemma MSB_EVAL2: "ALL a.


1402 
MSB (n2w a) =


1403 
bit (NUMERAL


1404 
(NUMERAL_BIT1


1405 
(NUMERAL_BIT1


1406 
(NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO))))))


1407 
a"


1408 
by (import word32 MSB_EVAL2)


1409 


1410 
lemma OR_EVAL2: "ALL b a.


1411 
bitwise_or (n2w a) (n2w b) =


1412 
n2w (BITWISE


1413 
(NUMERAL


1414 
(NUMERAL_BIT2


1415 
(NUMERAL_BIT1


1416 
(NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO))))))


1417 
op  a b)"


1418 
by (import word32 OR_EVAL2)


1419 


1420 
lemma AND_EVAL2: "ALL b a.


1421 
bitwise_and (n2w a) (n2w b) =


1422 
n2w (BITWISE


1423 
(NUMERAL


1424 
(NUMERAL_BIT2


1425 
(NUMERAL_BIT1


1426 
(NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO))))))


1427 
op & a b)"


1428 
by (import word32 AND_EVAL2)


1429 


1430 
lemma EOR_EVAL2: "ALL b a.


1431 
bitwise_eor (n2w a) (n2w b) =


1432 
n2w (BITWISE


1433 
(NUMERAL


1434 
(NUMERAL_BIT2


1435 
(NUMERAL_BIT1


1436 
(NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT1 ALT_ZERO))))))


1437 
(%x y. x ~= y) a b)"


1438 
by (import word32 EOR_EVAL2)


1439 


1440 
lemma BITWISE_EVAL2: "ALL n oper x y.


1441 
BITWISE n oper x y =


1442 
(if n = 0 then 0


1443 
else 2 * BITWISE (n  1) oper (x div 2) (y div 2) +


1444 
(if oper (ODD x) (ODD y) then 1 else 0))"


1445 
by (import word32 BITWISE_EVAL2)


1446 


1447 
lemma BITSwLT_THM: "ALL h l n. BITSw h l n < 2 ^ (Suc h  l)"


1448 
by (import word32 BITSwLT_THM)


1449 


1450 
lemma BITSw_COMP_THM: "ALL h1 l1 h2 l2 n.


1451 
h2 + l1 <= h1 >


1452 
BITS h2 l2 (BITSw h1 l1 n) = BITSw (h2 + l1) (l2 + l1) n"


1453 
by (import word32 BITSw_COMP_THM)


1454 


1455 
lemma BITSw_DIV_THM: "ALL h l n x. BITSw h l x div 2 ^ n = BITSw h (l + n) x"


1456 
by (import word32 BITSw_DIV_THM)


1457 


1458 
lemma BITw_THM: "ALL b n. BITw b n = (BITSw b b n = 1)"


1459 
by (import word32 BITw_THM)


1460 


1461 
lemma SLICEw_THM: "ALL n h l. SLICEw h l n = BITSw h l n * 2 ^ l"


1462 
by (import word32 SLICEw_THM)


1463 


1464 
lemma BITS_SLICEw_THM: "ALL h l n. BITS h l (SLICEw h l n) = BITSw h l n"


1465 
by (import word32 BITS_SLICEw_THM)


1466 


1467 
lemma SLICEw_ZERO_THM: "ALL n h. SLICEw h 0 n = BITSw h 0 n"


1468 
by (import word32 SLICEw_ZERO_THM)


1469 


1470 
lemma SLICEw_COMP_THM: "ALL h m l a.


1471 
Suc m <= h & l <= m > SLICEw h (Suc m) a + SLICEw m l a = SLICEw h l a"


1472 
by (import word32 SLICEw_COMP_THM)


1473 


1474 
lemma BITSw_ZERO: "ALL h l n. h < l > BITSw h l n = 0"


1475 
by (import word32 BITSw_ZERO)


1476 


1477 
lemma SLICEw_ZERO: "ALL h l n. h < l > SLICEw h l n = 0"


1478 
by (import word32 SLICEw_ZERO)


1479 


1480 
;end_setup


1481 


1482 
end


1483 
