270 (uint :: 'a::len0 word \<Rightarrow> int)" |
270 (uint :: 'a::len0 word \<Rightarrow> int)" |
271 unfolding fun_rel_def cr_word_def by (simp add: word_ubin.eq_norm) |
271 unfolding fun_rel_def cr_word_def by (simp add: word_ubin.eq_norm) |
272 |
272 |
273 subsection "Arithmetic operations" |
273 subsection "Arithmetic operations" |
274 |
274 |
275 lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x::int. x + 1" |
275 lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x + 1" |
276 by (metis bintr_ariths(6)) |
276 by (metis bintr_ariths(6)) |
277 |
277 |
278 lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x::int. x - 1" |
278 lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x - 1" |
279 by (metis bintr_ariths(7)) |
279 by (metis bintr_ariths(7)) |
280 |
280 |
281 instantiation word :: (len0) "{neg_numeral, Divides.div, comm_monoid_mult, comm_ring}" |
281 instantiation word :: (len0) "{neg_numeral, Divides.div, comm_monoid_mult, comm_ring}" |
282 begin |
282 begin |
283 |
283 |
284 lift_definition zero_word :: "'a word" is "0::int" . |
284 lift_definition zero_word :: "'a word" is "0" . |
285 |
285 |
286 lift_definition one_word :: "'a word" is "1::int" . |
286 lift_definition one_word :: "'a word" is "1" . |
287 |
287 |
288 lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
288 lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op +" |
289 is "op + :: int \<Rightarrow> int \<Rightarrow> int" |
|
290 by (metis bintr_ariths(2)) |
289 by (metis bintr_ariths(2)) |
291 |
290 |
292 lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
291 lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op -" |
293 is "op - :: int \<Rightarrow> int \<Rightarrow> int" |
|
294 by (metis bintr_ariths(3)) |
292 by (metis bintr_ariths(3)) |
295 |
293 |
296 lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" |
294 lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" is uminus |
297 is "uminus :: int \<Rightarrow> int" |
|
298 by (metis bintr_ariths(5)) |
295 by (metis bintr_ariths(5)) |
299 |
296 |
300 lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
297 lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op *" |
301 is "op * :: int \<Rightarrow> int \<Rightarrow> int" |
|
302 by (metis bintr_ariths(4)) |
298 by (metis bintr_ariths(4)) |
303 |
299 |
304 definition |
300 definition |
305 word_div_def: "a div b = word_of_int (uint a div uint b)" |
301 word_div_def: "a div b = word_of_int (uint a div uint b)" |
306 |
302 |
392 subsection "Bit-wise operations" |
388 subsection "Bit-wise operations" |
393 |
389 |
394 instantiation word :: (len0) bits |
390 instantiation word :: (len0) bits |
395 begin |
391 begin |
396 |
392 |
397 lift_definition bitNOT_word :: "'a word \<Rightarrow> 'a word" |
393 lift_definition bitNOT_word :: "'a word \<Rightarrow> 'a word" is bitNOT |
398 is "bitNOT :: int \<Rightarrow> int" |
|
399 by (metis bin_trunc_not) |
394 by (metis bin_trunc_not) |
400 |
395 |
401 lift_definition bitAND_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
396 lift_definition bitAND_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitAND |
402 is "bitAND :: int \<Rightarrow> int \<Rightarrow> int" |
|
403 by (metis bin_trunc_and) |
397 by (metis bin_trunc_and) |
404 |
398 |
405 lift_definition bitOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
399 lift_definition bitOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitOR |
406 is "bitOR :: int \<Rightarrow> int \<Rightarrow> int" |
|
407 by (metis bin_trunc_or) |
400 by (metis bin_trunc_or) |
408 |
401 |
409 lift_definition bitXOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
402 lift_definition bitXOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitXOR |
410 is "bitXOR :: int \<Rightarrow> int \<Rightarrow> int" |
|
411 by (metis bin_trunc_xor) |
403 by (metis bin_trunc_xor) |
412 |
404 |
413 definition |
405 definition |
414 word_test_bit_def: "test_bit a = bin_nth (uint a)" |
406 word_test_bit_def: "test_bit a = bin_nth (uint a)" |
415 |
407 |