37 reverse order to \<^const>\<open>to_bl\<close>.\<close> |
37 reverse order to \<^const>\<open>to_bl\<close>.\<close> |
38 |
38 |
39 lemma bl_word_sub: "to_bl (x - y) = to_bl (x + (- y))" |
39 lemma bl_word_sub: "to_bl (x - y) = to_bl (x + (- y))" |
40 by simp |
40 by simp |
41 |
41 |
42 lemma rbl_word_1: "rev (to_bl (1 :: 'a::len0 word)) = takefill False (LENGTH('a)) [True]" |
42 lemma rbl_word_1: "rev (to_bl (1 :: 'a::len word)) = takefill False (LENGTH('a)) [True]" |
43 apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans) |
43 apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans) |
44 apply simp |
44 apply simp |
45 apply (simp only: rtb_rbl_ariths(1)[OF refl]) |
45 apply (simp only: rtb_rbl_ariths(1)[OF refl]) |
46 apply simp |
46 apply simp |
47 apply (case_tac "LENGTH('a)") |
47 apply (case_tac "LENGTH('a)") |
102 |
102 |
103 lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))" |
103 lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))" |
104 by (simp add: twos_complement word_succ_rbl[OF refl] bl_word_not rev_map rbl_succ2_def) |
104 by (simp add: twos_complement word_succ_rbl[OF refl] bl_word_not rev_map rbl_succ2_def) |
105 |
105 |
106 lemma rbl_word_cat: |
106 lemma rbl_word_cat: |
107 "rev (to_bl (word_cat x y :: 'a::len0 word)) = |
107 "rev (to_bl (word_cat x y :: 'a::len word)) = |
108 takefill False (LENGTH('a)) (rev (to_bl y) @ rev (to_bl x))" |
108 takefill False (LENGTH('a)) (rev (to_bl y) @ rev (to_bl x))" |
109 by (simp add: word_cat_bl word_rev_tf) |
109 by (simp add: word_cat_bl word_rev_tf) |
110 |
110 |
111 lemma rbl_word_slice: |
111 lemma rbl_word_slice: |
112 "rev (to_bl (slice n w :: 'a::len0 word)) = |
112 "rev (to_bl (slice n w :: 'a::len word)) = |
113 takefill False (LENGTH('a)) (drop n (rev (to_bl w)))" |
113 takefill False (LENGTH('a)) (drop n (rev (to_bl w)))" |
114 apply (simp add: slice_take word_rev_tf rev_take) |
114 apply (simp add: slice_take word_rev_tf rev_take) |
115 apply (cases "n < LENGTH('b)", simp_all) |
115 apply (cases "n < LENGTH('b)", simp_all) |
116 done |
116 done |
117 |
117 |
118 lemma rbl_word_ucast: |
118 lemma rbl_word_ucast: |
119 "rev (to_bl (ucast x :: 'a::len0 word)) = takefill False (LENGTH('a)) (rev (to_bl x))" |
119 "rev (to_bl (ucast x :: 'a::len word)) = takefill False (LENGTH('a)) (rev (to_bl x))" |
120 apply (simp add: to_bl_ucast takefill_alt) |
120 apply (simp add: to_bl_ucast takefill_alt) |
121 apply (simp add: rev_drop) |
121 apply (simp add: rev_drop) |
122 apply (cases "LENGTH('a) < LENGTH('b)") |
122 apply (cases "LENGTH('a) < LENGTH('b)") |
123 apply simp_all |
123 apply simp_all |
124 done |
124 done |
162 apply (simp add: nth_sshiftr word_size test_bit_of_bl |
162 apply (simp add: nth_sshiftr word_size test_bit_of_bl |
163 msb_nth) |
163 msb_nth) |
164 done |
164 done |
165 |
165 |
166 lemma nth_word_of_int: |
166 lemma nth_word_of_int: |
167 "(word_of_int x :: 'a::len0 word) !! n = (n < LENGTH('a) \<and> bin_nth x n)" |
167 "(word_of_int x :: 'a::len word) !! n = (n < LENGTH('a) \<and> bin_nth x n)" |
168 apply (simp add: test_bit_bl word_size to_bl_of_bin) |
168 apply (simp add: test_bit_bl word_size to_bl_of_bin) |
169 apply (subst conj_cong[OF refl], erule bin_nth_bl) |
169 apply (subst conj_cong[OF refl], erule bin_nth_bl) |
170 apply auto |
170 apply auto |
171 done |
171 done |
172 |
172 |
282 apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat) |
282 apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat) |
283 apply (auto simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq Bit_def) |
283 apply (auto simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq Bit_def) |
284 done |
284 done |
285 |
285 |
286 lemma word_le_rbl: "x \<le> y \<longleftrightarrow> rev_bl_order True (rev (to_bl x)) (rev (to_bl y))" |
286 lemma word_le_rbl: "x \<le> y \<longleftrightarrow> rev_bl_order True (rev (to_bl x)) (rev (to_bl y))" |
287 for x y :: "'a::len0 word" |
287 for x y :: "'a::len word" |
288 by (simp add: rev_bl_order_bl_to_bin word_le_def) |
288 by (simp add: rev_bl_order_bl_to_bin word_le_def) |
289 |
289 |
290 lemma word_less_rbl: "x < y \<longleftrightarrow> rev_bl_order False (rev (to_bl x)) (rev (to_bl y))" |
290 lemma word_less_rbl: "x < y \<longleftrightarrow> rev_bl_order False (rev (to_bl x)) (rev (to_bl y))" |
291 for x y :: "'a::len0 word" |
291 for x y :: "'a::len word" |
292 by (simp add: word_less_alt rev_bl_order_bl_to_bin) |
292 by (simp add: word_less_alt rev_bl_order_bl_to_bin) |
293 |
293 |
294 lemma word_sint_msb_eq: "sint x = uint x - (if msb x then 2 ^ size x else 0)" |
294 lemma word_sint_msb_eq: "sint x = uint x - (if msb x then 2 ^ size x else 0)" |
295 apply (cases "msb x") |
295 apply (cases "msb x") |
296 apply (rule word_sint.Abs_eqD[where 'a='a], simp_all) |
296 apply (rule word_sint.Abs_eqD[where 'a='a], simp_all) |