author | haftmann |
Mon, 10 Aug 2020 08:27:17 +0200 | |
changeset 72128 | 3707cf7b370b |
parent 72088 | a36db1c8238e |
child 72130 | 9e5862223442 |
permissions | -rw-r--r-- |
72079 | 1 |
(* Title: HOL/Word/More_thy |
70174 | 2 |
*) |
3 |
||
71985 | 4 |
section \<open>Ancient comprehensive Word Library\<close> |
70174 | 5 |
|
6 |
theory More_Word |
|
7 |
imports |
|
8 |
Word |
|
71986 | 9 |
Ancient_Numeral |
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72079
diff
changeset
|
10 |
Reversed_Bit_Lists |
72128 | 11 |
Bits_Int |
71997 | 12 |
Misc_Auxiliary |
13 |
Misc_Arithmetic |
|
72000 | 14 |
Misc_set_bit |
15 |
Misc_lsb |
|
70174 | 16 |
begin |
17 |
||
72010 | 18 |
declare signed_take_bit_Suc [simp] |
19 |
||
72079 | 20 |
lemmas bshiftr1_def = bshiftr1_eq |
21 |
lemmas is_down_def = is_down_eq |
|
22 |
lemmas is_up_def = is_up_eq |
|
23 |
lemmas mask_def = mask_eq_decr_exp |
|
24 |
lemmas scast_def = scast_eq |
|
25 |
lemmas shiftl1_def = shiftl1_eq |
|
26 |
lemmas shiftr1_def = shiftr1_eq |
|
27 |
lemmas sshiftr1_def = sshiftr1_eq |
|
28 |
lemmas sshiftr_def = sshiftr_eq |
|
29 |
lemmas to_bl_def = to_bl_eq |
|
30 |
lemmas ucast_def = ucast_eq |
|
31 |
lemmas unat_def = unat_eq_nat_uint |
|
32 |
lemmas word_cat_def = word_cat_eq |
|
33 |
lemmas word_reverse_def = word_reverse_eq_of_bl_rev_to_bl |
|
34 |
lemmas word_roti_def = word_roti_eq_word_rotr_word_rotl |
|
35 |
lemmas word_rotl_def = word_rotl_eq |
|
36 |
lemmas word_rotr_def = word_rotr_eq |
|
37 |
lemmas word_sle_def = word_sle_eq |
|
38 |
lemmas word_sless_def = word_sless_eq |
|
39 |
||
40 |
lemma shiftl_transfer [transfer_rule]: |
|
41 |
includes lifting_syntax |
|
42 |
shows "(pcr_word ===> (=) ===> pcr_word) (<<) (<<)" |
|
43 |
by (auto intro!: rel_funI word_eqI simp add: word.pcr_cr_eq cr_word_def word_size nth_shiftl) |
|
44 |
||
70174 | 45 |
end |