author | haftmann |
Thu, 08 Oct 2020 07:30:02 +0000 | |
changeset 72397 | 48013583e8e6 |
parent 72388 | 633d14bd1e59 |
child 72487 | ab32922f139b |
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 |
72397 | 12 |
Bit_Comprehension |
71997 | 13 |
Misc_Auxiliary |
14 |
Misc_Arithmetic |
|
72000 | 15 |
Misc_set_bit |
16 |
Misc_lsb |
|
72292 | 17 |
Misc_Typedef |
70174 | 18 |
begin |
19 |
||
72010 | 20 |
declare signed_take_bit_Suc [simp] |
21 |
||
72079 | 22 |
lemmas bshiftr1_def = bshiftr1_eq |
23 |
lemmas is_down_def = is_down_eq |
|
24 |
lemmas is_up_def = is_up_eq |
|
25 |
lemmas mask_def = mask_eq_decr_exp |
|
26 |
lemmas scast_def = scast_eq |
|
27 |
lemmas shiftl1_def = shiftl1_eq |
|
28 |
lemmas shiftr1_def = shiftr1_eq |
|
29 |
lemmas sshiftr1_def = sshiftr1_eq |
|
72388 | 30 |
lemmas sshiftr_def = sshiftr_eq_funpow_sshiftr1 |
72079 | 31 |
lemmas to_bl_def = to_bl_eq |
32 |
lemmas ucast_def = ucast_eq |
|
33 |
lemmas unat_def = unat_eq_nat_uint |
|
34 |
lemmas word_cat_def = word_cat_eq |
|
35 |
lemmas word_reverse_def = word_reverse_eq_of_bl_rev_to_bl |
|
36 |
lemmas word_roti_def = word_roti_eq_word_rotr_word_rotl |
|
37 |
lemmas word_rotl_def = word_rotl_eq |
|
38 |
lemmas word_rotr_def = word_rotr_eq |
|
39 |
lemmas word_sle_def = word_sle_eq |
|
40 |
lemmas word_sless_def = word_sless_eq |
|
41 |
||
72243 | 42 |
lemmas uint_0 = uint_nonnegative |
43 |
lemmas uint_lt = uint_bounded |
|
44 |
lemmas uint_mod_same = uint_idem |
|
45 |
lemmas of_nth_def = word_set_bits_def |
|
46 |
||
72262 | 47 |
lemmas of_nat_word_eq_iff = word_of_nat_eq_iff |
48 |
lemmas of_nat_word_eq_0_iff = word_of_nat_eq_0_iff |
|
49 |
lemmas of_int_word_eq_iff = word_of_int_eq_iff |
|
50 |
lemmas of_int_word_eq_0_iff = word_of_int_eq_0_iff |
|
51 |
||
72079 | 52 |
lemma shiftl_transfer [transfer_rule]: |
53 |
includes lifting_syntax |
|
54 |
shows "(pcr_word ===> (=) ===> pcr_word) (<<) (<<)" |
|
72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset
|
55 |
by (unfold shiftl_eq_push_bit) transfer_prover |
72079 | 56 |
|
70174 | 57 |
end |