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