author | ballarin |
Fri, 19 Dec 2008 16:39:23 +0100 | |
changeset 29249 | 4dc278c8dc59 |
parent 29235 | 2d62b637fa80 |
child 29631 | 3aa049e5f156 |
permissions | -rw-r--r-- |
24333 | 1 |
(* |
2 |
ID: $Id$ |
|
3 |
Author: Jeremy Dawson and Gerwin Klein, NICTA |
|
4 |
||
5 |
contains theorems to do with bit-wise (logical) operations on words |
|
6 |
*) |
|
24350 | 7 |
|
8 |
header {* Bitwise Operations on Words *} |
|
9 |
||
26558 | 10 |
theory WordBitwise |
11 |
imports WordArith |
|
12 |
begin |
|
24333 | 13 |
|
14 |
lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or |
|
15 |
||
16 |
(* following definitions require both arithmetic and bit-wise word operations *) |
|
17 |
||
18 |
(* to get word_no_log_defs from word_log_defs, using bin_log_bintrs *) |
|
19 |
lemmas wils1 = bin_log_bintrs [THEN word_ubin.norm_eq_iff [THEN iffD1], |
|
20 |
folded word_ubin.eq_norm, THEN eq_reflection, standard] |
|
21 |
||
22 |
(* the binary operations only *) |
|
23 |
lemmas word_log_binary_defs = |
|
24 |
word_and_def word_or_def word_xor_def |
|
25 |
||
26 |
lemmas word_no_log_defs [simp] = |
|
25350
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset
|
27 |
word_not_def [where a="number_of a", |
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset
|
28 |
unfolded word_no_wi wils1, folded word_no_wi, standard] |
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset
|
29 |
word_log_binary_defs [where a="number_of a" and b="number_of b", |
a5fcf6d12a53
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset
|
30 |
unfolded word_no_wi wils1, folded word_no_wi, standard] |
24333 | 31 |
|
32 |
lemmas word_wi_log_defs = word_no_log_defs [unfolded word_no_wi] |
|
33 |
||
24353 | 34 |
lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)" |
24368 | 35 |
by (simp add: word_or_def word_no_wi [symmetric] number_of_is_id |
24333 | 36 |
bin_trunc_ao(2) [symmetric]) |
37 |
||
24353 | 38 |
lemma uint_and: "uint (x AND y) = (uint x) AND (uint y)" |
24368 | 39 |
by (simp add: word_and_def number_of_is_id word_no_wi [symmetric] |
24333 | 40 |
bin_trunc_ao(1) [symmetric]) |
41 |
||
42 |
lemma word_ops_nth_size: |
|
24465 | 43 |
"n < size (x::'a::len0 word) ==> |
24333 | 44 |
(x OR y) !! n = (x !! n | y !! n) & |
45 |
(x AND y) !! n = (x !! n & y !! n) & |
|
46 |
(x XOR y) !! n = (x !! n ~= y !! n) & |
|
47 |
(NOT x) !! n = (~ x !! n)" |
|
48 |
unfolding word_size word_no_wi word_test_bit_def word_log_defs |
|
49 |
by (clarsimp simp add : word_ubin.eq_norm nth_bintr bin_nth_ops) |
|
50 |
||
51 |
lemma word_ao_nth: |
|
24465 | 52 |
fixes x :: "'a::len0 word" |
24333 | 53 |
shows "(x OR y) !! n = (x !! n | y !! n) & |
54 |
(x AND y) !! n = (x !! n & y !! n)" |
|
55 |
apply (cases "n < size x") |
|
56 |
apply (drule_tac y = "y" in word_ops_nth_size) |
|
57 |
apply simp |
|
58 |
apply (simp add : test_bit_bin word_size) |
|
59 |
done |
|
60 |
||
61 |
(* get from commutativity, associativity etc of int_and etc |
|
62 |
to same for word_and etc *) |
|
63 |
||
64 |
lemmas bwsimps = |
|
65 |
word_of_int_homs(2) |
|
66 |
word_0_wi_Pls |
|
67 |
word_m1_wi_Min |
|
68 |
word_wi_log_defs |
|
69 |
||
70 |
lemma word_bw_assocs: |
|
24465 | 71 |
fixes x :: "'a::len0 word" |
24333 | 72 |
shows |
73 |
"(x AND y) AND z = x AND y AND z" |
|
74 |
"(x OR y) OR z = x OR y OR z" |
|
75 |
"(x XOR y) XOR z = x XOR y XOR z" |
|
76 |
using word_of_int_Ex [where x=x] |
|
77 |
word_of_int_Ex [where x=y] |
|
78 |
word_of_int_Ex [where x=z] |
|
24367
3e29eafabe16
AC rules for bitwise logical operators no longer declared simp
huffman
parents:
24353
diff
changeset
|
79 |
by (auto simp: bwsimps bbw_assocs) |
24333 | 80 |
|
81 |
lemma word_bw_comms: |
|
24465 | 82 |
fixes x :: "'a::len0 word" |
24333 | 83 |
shows |
84 |
"x AND y = y AND x" |
|
85 |
"x OR y = y OR x" |
|
86 |
"x XOR y = y XOR x" |
|
87 |
using word_of_int_Ex [where x=x] |
|
88 |
word_of_int_Ex [where x=y] |
|
24367
3e29eafabe16
AC rules for bitwise logical operators no longer declared simp
huffman
parents:
24353
diff
changeset
|
89 |
by (auto simp: bwsimps bin_ops_comm) |
24333 | 90 |
|
91 |
lemma word_bw_lcs: |
|
24465 | 92 |
fixes x :: "'a::len0 word" |
24333 | 93 |
shows |
94 |
"y AND x AND z = x AND y AND z" |
|
95 |
"y OR x OR z = x OR y OR z" |
|
96 |
"y XOR x XOR z = x XOR y XOR z" |
|
97 |
using word_of_int_Ex [where x=x] |
|
98 |
word_of_int_Ex [where x=y] |
|
99 |
word_of_int_Ex [where x=z] |
|
100 |
by (auto simp: bwsimps) |
|
101 |
||
102 |
lemma word_log_esimps [simp]: |
|
24465 | 103 |
fixes x :: "'a::len0 word" |
24333 | 104 |
shows |
105 |
"x AND 0 = 0" |
|
106 |
"x AND -1 = x" |
|
107 |
"x OR 0 = x" |
|
108 |
"x OR -1 = -1" |
|
109 |
"x XOR 0 = x" |
|
110 |
"x XOR -1 = NOT x" |
|
111 |
"0 AND x = 0" |
|
112 |
"-1 AND x = x" |
|
113 |
"0 OR x = x" |
|
114 |
"-1 OR x = -1" |
|
115 |
"0 XOR x = x" |
|
116 |
"-1 XOR x = NOT x" |
|
117 |
using word_of_int_Ex [where x=x] |
|
118 |
by (auto simp: bwsimps) |
|
119 |
||
120 |
lemma word_not_dist: |
|
24465 | 121 |
fixes x :: "'a::len0 word" |
24333 | 122 |
shows |
123 |
"NOT (x OR y) = NOT x AND NOT y" |
|
124 |
"NOT (x AND y) = NOT x OR NOT y" |
|
125 |
using word_of_int_Ex [where x=x] |
|
126 |
word_of_int_Ex [where x=y] |
|
127 |
by (auto simp: bwsimps bbw_not_dist) |
|
128 |
||
129 |
lemma word_bw_same: |
|
24465 | 130 |
fixes x :: "'a::len0 word" |
24333 | 131 |
shows |
132 |
"x AND x = x" |
|
133 |
"x OR x = x" |
|
134 |
"x XOR x = 0" |
|
135 |
using word_of_int_Ex [where x=x] |
|
136 |
by (auto simp: bwsimps) |
|
137 |
||
138 |
lemma word_ao_absorbs [simp]: |
|
24465 | 139 |
fixes x :: "'a::len0 word" |
24333 | 140 |
shows |
141 |
"x AND (y OR x) = x" |
|
142 |
"x OR y AND x = x" |
|
143 |
"x AND (x OR y) = x" |
|
144 |
"y AND x OR x = x" |
|
145 |
"(y OR x) AND x = x" |
|
146 |
"x OR x AND y = x" |
|
147 |
"(x OR y) AND x = x" |
|
148 |
"x AND y OR x = x" |
|
149 |
using word_of_int_Ex [where x=x] |
|
150 |
word_of_int_Ex [where x=y] |
|
151 |
by (auto simp: bwsimps) |
|
152 |
||
153 |
lemma word_not_not [simp]: |
|
24465 | 154 |
"NOT NOT (x::'a::len0 word) = x" |
24333 | 155 |
using word_of_int_Ex [where x=x] |
156 |
by (auto simp: bwsimps) |
|
157 |
||
158 |
lemma word_ao_dist: |
|
24465 | 159 |
fixes x :: "'a::len0 word" |
24333 | 160 |
shows "(x OR y) AND z = x AND z OR y AND z" |
161 |
using word_of_int_Ex [where x=x] |
|
162 |
word_of_int_Ex [where x=y] |
|
163 |
word_of_int_Ex [where x=z] |
|
164 |
by (auto simp: bwsimps bbw_ao_dist simp del: bin_ops_comm) |
|
165 |
||
166 |
lemma word_oa_dist: |
|
24465 | 167 |
fixes x :: "'a::len0 word" |
24333 | 168 |
shows "x AND y OR z = (x OR z) AND (y OR z)" |
169 |
using word_of_int_Ex [where x=x] |
|
170 |
word_of_int_Ex [where x=y] |
|
171 |
word_of_int_Ex [where x=z] |
|
172 |
by (auto simp: bwsimps bbw_oa_dist simp del: bin_ops_comm) |
|
173 |
||
174 |
lemma word_add_not [simp]: |
|
24465 | 175 |
fixes x :: "'a::len0 word" |
24333 | 176 |
shows "x + NOT x = -1" |
177 |
using word_of_int_Ex [where x=x] |
|
178 |
by (auto simp: bwsimps bin_add_not) |
|
179 |
||
180 |
lemma word_plus_and_or [simp]: |
|
24465 | 181 |
fixes x :: "'a::len0 word" |
24333 | 182 |
shows "(x AND y) + (x OR y) = x + y" |
183 |
using word_of_int_Ex [where x=x] |
|
184 |
word_of_int_Ex [where x=y] |
|
185 |
by (auto simp: bwsimps plus_and_or) |
|
186 |
||
187 |
lemma leoa: |
|
24465 | 188 |
fixes x :: "'a::len0 word" |
24333 | 189 |
shows "(w = (x OR y)) ==> (y = (w AND y))" by auto |
190 |
lemma leao: |
|
24465 | 191 |
fixes x' :: "'a::len0 word" |
24333 | 192 |
shows "(w' = (x' AND y')) ==> (x' = (x' OR w'))" by auto |
193 |
||
194 |
lemmas word_ao_equiv = leao [COMP leoa [COMP iffI]] |
|
195 |
||
24465 | 196 |
lemma le_word_or2: "x <= x OR (y::'a::len0 word)" |
24333 | 197 |
unfolding word_le_def uint_or |
198 |
by (auto intro: le_int_or) |
|
199 |
||
200 |
lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2, standard] |
|
201 |
lemmas word_and_le1 = |
|
202 |
xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2, standard] |
|
203 |
lemmas word_and_le2 = |
|
204 |
xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2, standard] |
|
205 |
||
24465 | 206 |
lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" |
207 |
unfolding to_bl_def word_log_defs |
|
208 |
by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric]) |
|
209 |
||
26558 | 210 |
lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)" |
24465 | 211 |
unfolding to_bl_def word_log_defs bl_xor_bin |
212 |
by (simp add: number_of_is_id word_no_wi [symmetric]) |
|
213 |
||
26558 | 214 |
lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)" |
24465 | 215 |
unfolding to_bl_def word_log_defs |
216 |
by (simp add: bl_or_bin number_of_is_id word_no_wi [symmetric]) |
|
217 |
||
26558 | 218 |
lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)" |
24465 | 219 |
unfolding to_bl_def word_log_defs |
220 |
by (simp add: bl_and_bin number_of_is_id word_no_wi [symmetric]) |
|
221 |
||
222 |
lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0" |
|
24333 | 223 |
by (auto simp: word_test_bit_def word_lsb_def) |
224 |
||
24465 | 225 |
lemma word_lsb_1_0: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)" |
24333 | 226 |
unfolding word_lsb_def word_1_no word_0_no by auto |
227 |
||
24465 | 228 |
lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)" |
229 |
apply (unfold word_lsb_def uint_bl bin_to_bl_def) |
|
230 |
apply (rule_tac bin="uint w" in bin_exhaust) |
|
231 |
apply (cases "size w") |
|
232 |
apply auto |
|
233 |
apply (auto simp add: bin_to_bl_aux_alt) |
|
234 |
done |
|
235 |
||
24333 | 236 |
lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)" |
237 |
unfolding word_lsb_def bin_last_mod by auto |
|
238 |
||
239 |
lemma word_msb_sint: "msb w = (sint w < 0)" |
|
240 |
unfolding word_msb_def |
|
24368 | 241 |
by (simp add : sign_Min_lt_0 number_of_is_id) |
24333 | 242 |
|
243 |
lemma word_msb_no': |
|
24465 | 244 |
"w = number_of bin ==> msb (w::'a::len word) = bin_nth bin (size w - 1)" |
24333 | 245 |
unfolding word_msb_def word_number_of_def |
246 |
by (clarsimp simp add: word_sbin.eq_norm word_size bin_sign_lem) |
|
247 |
||
248 |
lemmas word_msb_no = refl [THEN word_msb_no', unfolded word_size] |
|
249 |
||
24465 | 250 |
lemma word_msb_nth': "msb (w::'a::len word) = bin_nth (uint w) (size w - 1)" |
24333 | 251 |
apply (unfold word_size) |
252 |
apply (rule trans [OF _ word_msb_no]) |
|
253 |
apply (simp add : word_number_of_def) |
|
254 |
done |
|
255 |
||
256 |
lemmas word_msb_nth = word_msb_nth' [unfolded word_size] |
|
257 |
||
24465 | 258 |
lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)" |
259 |
apply (unfold word_msb_nth uint_bl) |
|
260 |
apply (subst hd_conv_nth) |
|
261 |
apply (rule length_greater_0_conv [THEN iffD1]) |
|
262 |
apply simp |
|
263 |
apply (simp add : nth_bin_to_bl word_size) |
|
264 |
done |
|
265 |
||
24333 | 266 |
lemma word_set_nth: |
24465 | 267 |
"set_bit w n (test_bit w n) = (w::'a::len0 word)" |
24333 | 268 |
unfolding word_test_bit_def word_set_bit_def by auto |
269 |
||
24465 | 270 |
lemma bin_nth_uint': |
271 |
"bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)" |
|
272 |
apply (unfold word_size) |
|
273 |
apply (safe elim!: bin_nth_uint_imp) |
|
274 |
apply (frule bin_nth_uint_imp) |
|
275 |
apply (fast dest!: bin_nth_bl)+ |
|
276 |
done |
|
277 |
||
278 |
lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size] |
|
279 |
||
280 |
lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)" |
|
281 |
unfolding to_bl_def word_test_bit_def word_size |
|
282 |
by (rule bin_nth_uint) |
|
283 |
||
284 |
lemma to_bl_nth: "n < size w ==> to_bl w ! n = w !! (size w - Suc n)" |
|
285 |
apply (unfold test_bit_bl) |
|
286 |
apply clarsimp |
|
287 |
apply (rule trans) |
|
288 |
apply (rule nth_rev_alt) |
|
289 |
apply (auto simp add: word_size) |
|
290 |
done |
|
291 |
||
24333 | 292 |
lemma test_bit_set: |
24465 | 293 |
fixes w :: "'a::len0 word" |
24333 | 294 |
shows "(set_bit w n x) !! n = (n < size w & x)" |
295 |
unfolding word_size word_test_bit_def word_set_bit_def |
|
296 |
by (clarsimp simp add : word_ubin.eq_norm nth_bintr) |
|
297 |
||
298 |
lemma test_bit_set_gen: |
|
24465 | 299 |
fixes w :: "'a::len0 word" |
24333 | 300 |
shows "test_bit (set_bit w n x) m = |
301 |
(if m = n then n < size w & x else test_bit w m)" |
|
302 |
apply (unfold word_size word_test_bit_def word_set_bit_def) |
|
303 |
apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen) |
|
304 |
apply (auto elim!: test_bit_size [unfolded word_size] |
|
305 |
simp add: word_test_bit_def [symmetric]) |
|
306 |
done |
|
307 |
||
24465 | 308 |
lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs" |
309 |
unfolding of_bl_def bl_to_bin_rep_F by auto |
|
310 |
||
24333 | 311 |
lemma msb_nth': |
24465 | 312 |
fixes w :: "'a::len word" |
24333 | 313 |
shows "msb w = w !! (size w - 1)" |
314 |
unfolding word_msb_nth' word_test_bit_def by simp |
|
315 |
||
316 |
lemmas msb_nth = msb_nth' [unfolded word_size] |
|
317 |
||
24465 | 318 |
lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN |
24333 | 319 |
word_ops_nth_size [unfolded word_size], standard] |
320 |
lemmas msb1 = msb0 [where i = 0] |
|
321 |
lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]] |
|
322 |
||
24465 | 323 |
lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size], standard] |
24333 | 324 |
lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt] |
325 |
||
24465 | 326 |
lemma td_ext_nth': |
327 |
"n = size (w::'a::len0 word) ==> ofn = set_bits ==> [w, ofn g] = l ==> |
|
328 |
td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)" |
|
329 |
apply (unfold word_size td_ext_def') |
|
26827
a62f8db42f4a
Deleted subset_antisym in a few proofs, because it is
berghofe
parents:
26558
diff
changeset
|
330 |
apply (safe del: subset_antisym) |
24465 | 331 |
apply (rule_tac [3] ext) |
332 |
apply (rule_tac [4] ext) |
|
333 |
apply (unfold word_size of_nth_def test_bit_bl) |
|
334 |
apply safe |
|
335 |
defer |
|
336 |
apply (clarsimp simp: word_bl.Abs_inverse)+ |
|
337 |
apply (rule word_bl.Rep_inverse') |
|
338 |
apply (rule sym [THEN trans]) |
|
339 |
apply (rule bl_of_nth_nth) |
|
340 |
apply simp |
|
341 |
apply (rule bl_of_nth_inj) |
|
342 |
apply (clarsimp simp add : test_bit_bl word_size) |
|
343 |
done |
|
344 |
||
345 |
lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size] |
|
346 |
||
29235 | 347 |
interpretation test_bit!: |
348 |
td_ext "op !! :: 'a::len0 word => nat => bool" |
|
349 |
set_bits |
|
350 |
"{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}" |
|
351 |
"(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))" |
|
24465 | 352 |
by (rule td_ext_nth) |
353 |
||
354 |
declare test_bit.Rep' [simp del] |
|
355 |
declare test_bit.Rep' [rule del] |
|
356 |
||
357 |
lemmas td_nth = test_bit.td_thm |
|
358 |
||
24333 | 359 |
lemma word_set_set_same: |
24465 | 360 |
fixes w :: "'a::len0 word" |
24333 | 361 |
shows "set_bit (set_bit w n x) n y = set_bit w n y" |
362 |
by (rule word_eqI) (simp add : test_bit_set_gen word_size) |
|
363 |
||
364 |
lemma word_set_set_diff: |
|
24465 | 365 |
fixes w :: "'a::len0 word" |
24333 | 366 |
assumes "m ~= n" |
367 |
shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" |
|
368 |
by (rule word_eqI) (clarsimp simp add : test_bit_set_gen word_size prems) |
|
369 |
||
370 |
lemma test_bit_no': |
|
24465 | 371 |
fixes w :: "'a::len0 word" |
24333 | 372 |
shows "w = number_of bin ==> test_bit w n = (n < size w & bin_nth bin n)" |
373 |
unfolding word_test_bit_def word_number_of_def word_size |
|
374 |
by (simp add : nth_bintr [symmetric] word_ubin.eq_norm) |
|
375 |
||
376 |
lemmas test_bit_no = |
|
377 |
refl [THEN test_bit_no', unfolded word_size, THEN eq_reflection, standard] |
|
378 |
||
24465 | 379 |
lemma nth_0: "~ (0::'a::len0 word) !! n" |
24333 | 380 |
unfolding test_bit_no word_0_no by auto |
381 |
||
382 |
lemma nth_sint: |
|
24465 | 383 |
fixes w :: "'a::len word" |
384 |
defines "l \<equiv> len_of TYPE ('a)" |
|
24333 | 385 |
shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))" |
386 |
unfolding sint_uint l_def |
|
387 |
by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric]) |
|
388 |
||
389 |
lemma word_lsb_no: |
|
24465 | 390 |
"lsb (number_of bin :: 'a :: len word) = (bin_last bin = bit.B1)" |
24333 | 391 |
unfolding word_lsb_alt test_bit_no by auto |
392 |
||
393 |
lemma word_set_no: |
|
24465 | 394 |
"set_bit (number_of bin::'a::len0 word) n b = |
24333 | 395 |
number_of (bin_sc n (if b then bit.B1 else bit.B0) bin)" |
396 |
apply (unfold word_set_bit_def word_number_of_def [symmetric]) |
|
397 |
apply (rule word_eqI) |
|
24368 | 398 |
apply (clarsimp simp: word_size bin_nth_sc_gen number_of_is_id |
24333 | 399 |
test_bit_no nth_bintr) |
400 |
done |
|
401 |
||
402 |
lemmas setBit_no = setBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no], |
|
403 |
simplified if_simps, THEN eq_reflection, standard] |
|
404 |
lemmas clearBit_no = clearBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no], |
|
405 |
simplified if_simps, THEN eq_reflection, standard] |
|
406 |
||
24465 | 407 |
lemma to_bl_n1: |
408 |
"to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True" |
|
409 |
apply (rule word_bl.Abs_inverse') |
|
410 |
apply simp |
|
411 |
apply (rule word_eqI) |
|
412 |
apply (clarsimp simp add: word_size test_bit_no) |
|
413 |
apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size) |
|
414 |
done |
|
415 |
||
416 |
lemma word_msb_n1: "msb (-1::'a::len word)" |
|
417 |
unfolding word_msb_alt word_msb_alt to_bl_n1 by simp |
|
24333 | 418 |
|
419 |
declare word_set_set_same [simp] word_set_nth [simp] |
|
420 |
test_bit_no [simp] word_set_no [simp] nth_0 [simp] |
|
421 |
setBit_no [simp] clearBit_no [simp] |
|
422 |
word_lsb_no [simp] word_msb_no [simp] word_msb_n1 [simp] word_lsb_1_0 [simp] |
|
423 |
||
424 |
lemma word_set_nth_iff: |
|
24465 | 425 |
"(set_bit w n b = w) = (w !! n = b | n >= size (w::'a::len0 word))" |
24333 | 426 |
apply (rule iffI) |
427 |
apply (rule disjCI) |
|
428 |
apply (drule word_eqD) |
|
429 |
apply (erule sym [THEN trans]) |
|
430 |
apply (simp add: test_bit_set) |
|
431 |
apply (erule disjE) |
|
432 |
apply clarsimp |
|
433 |
apply (rule word_eqI) |
|
434 |
apply (clarsimp simp add : test_bit_set_gen) |
|
435 |
apply (drule test_bit_size) |
|
436 |
apply force |
|
437 |
done |
|
438 |
||
439 |
lemma test_bit_2p': |
|
440 |
"w = word_of_int (2 ^ n) ==> |
|
24465 | 441 |
w !! m = (m = n & m < size (w :: 'a :: len word))" |
24333 | 442 |
unfolding word_test_bit_def word_size |
443 |
by (auto simp add: word_ubin.eq_norm nth_bintr nth_2p_bin) |
|
444 |
||
445 |
lemmas test_bit_2p = refl [THEN test_bit_2p', unfolded word_size] |
|
446 |
||
447 |
lemmas nth_w2p = test_bit_2p [unfolded of_int_number_of_eq |
|
26289 | 448 |
word_of_int [symmetric] Int.of_int_power] |
24333 | 449 |
|
450 |
lemma uint_2p: |
|
24465 | 451 |
"(0::'a::len word) < 2 ^ n ==> uint (2 ^ n::'a::len word) = 2 ^ n" |
24333 | 452 |
apply (unfold word_arith_power_alt) |
24465 | 453 |
apply (case_tac "len_of TYPE ('a)") |
24333 | 454 |
apply clarsimp |
455 |
apply (case_tac "nat") |
|
456 |
apply clarsimp |
|
457 |
apply (case_tac "n") |
|
458 |
apply (clarsimp simp add : word_1_wi [symmetric]) |
|
459 |
apply (clarsimp simp add : word_0_wi [symmetric]) |
|
460 |
apply (drule word_gt_0 [THEN iffD1]) |
|
461 |
apply (safe intro!: word_eqI bin_nth_lem ext) |
|
462 |
apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric]) |
|
463 |
done |
|
464 |
||
24465 | 465 |
lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n" |
24333 | 466 |
apply (unfold word_arith_power_alt) |
24465 | 467 |
apply (case_tac "len_of TYPE ('a)") |
24333 | 468 |
apply clarsimp |
469 |
apply (case_tac "nat") |
|
470 |
apply (rule word_ubin.norm_eq_iff [THEN iffD1]) |
|
471 |
apply (rule box_equals) |
|
472 |
apply (rule_tac [2] bintr_ariths (1))+ |
|
24368 | 473 |
apply (clarsimp simp add : number_of_is_id) |
24333 | 474 |
apply simp |
475 |
done |
|
476 |
||
24465 | 477 |
lemma bang_is_le: "x !! m ==> 2 ^ m <= (x :: 'a :: len word)" |
24333 | 478 |
apply (rule xtr3) |
479 |
apply (rule_tac [2] y = "x" in le_word_or2) |
|
480 |
apply (rule word_eqI) |
|
481 |
apply (auto simp add: word_ao_nth nth_w2p word_size) |
|
482 |
done |
|
483 |
||
484 |
lemma word_clr_le: |
|
24465 | 485 |
fixes w :: "'a::len0 word" |
24333 | 486 |
shows "w >= set_bit w n False" |
487 |
apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm) |
|
488 |
apply simp |
|
489 |
apply (rule order_trans) |
|
490 |
apply (rule bintr_bin_clr_le) |
|
491 |
apply simp |
|
492 |
done |
|
493 |
||
494 |
lemma word_set_ge: |
|
24465 | 495 |
fixes w :: "'a::len word" |
24333 | 496 |
shows "w <= set_bit w n True" |
497 |
apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm) |
|
498 |
apply simp |
|
499 |
apply (rule order_trans [OF _ bintr_bin_set_ge]) |
|
500 |
apply simp |
|
501 |
done |
|
502 |
||
503 |
end |
|
504 |