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