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