src/HOL/Import/HOL/HOL4Word32.thy
author wenzelm
Sat May 29 16:50:53 2004 +0200 (2004-05-29)
changeset 14847 44d92c12b255
parent 14516 a183dec876ab
child 15647 b1f486a9c56b
permissions -rw-r--r--
updated;
     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 
   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)))"
   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 
   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)))))"
   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