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