|
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
|
|
71997
|
10 |
Misc_Auxiliary
|
|
|
11 |
Misc_Arithmetic
|
|
72000
|
12 |
Misc_set_bit
|
|
|
13 |
Misc_lsb
|
|
70174
|
14 |
begin
|
|
|
15 |
|
|
72010
|
16 |
declare signed_take_bit_Suc [simp]
|
|
|
17 |
|
|
72079
|
18 |
lemmas bshiftr1_def = bshiftr1_eq
|
|
|
19 |
lemmas is_down_def = is_down_eq
|
|
|
20 |
lemmas is_up_def = is_up_eq
|
|
|
21 |
lemmas mask_def = mask_eq_decr_exp
|
|
|
22 |
lemmas scast_def = scast_eq
|
|
|
23 |
lemmas shiftl1_def = shiftl1_eq
|
|
|
24 |
lemmas shiftr1_def = shiftr1_eq
|
|
|
25 |
lemmas sshiftr1_def = sshiftr1_eq
|
|
|
26 |
lemmas sshiftr_def = sshiftr_eq
|
|
|
27 |
lemmas to_bl_def = to_bl_eq
|
|
|
28 |
lemmas ucast_def = ucast_eq
|
|
|
29 |
lemmas unat_def = unat_eq_nat_uint
|
|
|
30 |
lemmas word_cat_def = word_cat_eq
|
|
|
31 |
lemmas word_reverse_def = word_reverse_eq_of_bl_rev_to_bl
|
|
|
32 |
lemmas word_roti_def = word_roti_eq_word_rotr_word_rotl
|
|
|
33 |
lemmas word_rotl_def = word_rotl_eq
|
|
|
34 |
lemmas word_rotr_def = word_rotr_eq
|
|
|
35 |
lemmas word_sle_def = word_sle_eq
|
|
|
36 |
lemmas word_sless_def = word_sless_eq
|
|
|
37 |
|
|
|
38 |
lemma shiftl_transfer [transfer_rule]:
|
|
|
39 |
includes lifting_syntax
|
|
|
40 |
shows "(pcr_word ===> (=) ===> pcr_word) (<<) (<<)"
|
|
|
41 |
by (auto intro!: rel_funI word_eqI simp add: word.pcr_cr_eq cr_word_def word_size nth_shiftl)
|
|
|
42 |
|
|
70174
|
43 |
end
|