# Theory More_Word

theory More_Word
imports Ancient_Numeral Misc_Auxiliary Misc_Arithmetic Misc_set_bit
```(*  Title:      HOL/Word/More_thy
*)

section ‹Ancient comprehensive Word Library›

theory More_Word
imports
Word
Ancient_Numeral
Reversed_Bit_Lists
Bits_Int
Misc_Auxiliary
Misc_Arithmetic
Misc_set_bit
Misc_lsb
begin

declare signed_take_bit_Suc [simp]

lemmas bshiftr1_def = bshiftr1_eq
lemmas is_down_def = is_down_eq
lemmas is_up_def = is_up_eq
lemmas scast_def = scast_eq
lemmas shiftl1_def = shiftl1_eq
lemmas shiftr1_def = shiftr1_eq
lemmas sshiftr1_def = sshiftr1_eq
lemmas sshiftr_def = sshiftr_eq
lemmas to_bl_def = to_bl_eq
lemmas ucast_def = ucast_eq
lemmas unat_def = unat_eq_nat_uint
lemmas word_cat_def = word_cat_eq
lemmas word_reverse_def = word_reverse_eq_of_bl_rev_to_bl
lemmas word_roti_def = word_roti_eq_word_rotr_word_rotl
lemmas word_rotl_def = word_rotl_eq
lemmas word_rotr_def = word_rotr_eq
lemmas word_sle_def = word_sle_eq
lemmas word_sless_def = word_sless_eq

lemma shiftl_transfer [transfer_rule]:
includes lifting_syntax
shows "(pcr_word ===> (=) ===> pcr_word) (<<) (<<)"
by (unfold shiftl_eq_push_bit) transfer_prover

end
```