# HG changeset patch # User haftmann # Date 1592471250 0 # Node ID 2efc5b8c7456cbcfe71e8f6434f3b473ec93a2d0 # Parent ac6f9738c20099bd969d325cfc05fe5a2fb40a82 canonical bit shifts for word type, leaving duplicates as they are at the moment diff -r ac6f9738c200 -r 2efc5b8c7456 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Jun 18 09:07:30 2020 +0000 +++ b/src/HOL/Word/Word.thy Thu Jun 18 09:07:30 2020 +0000 @@ -735,13 +735,62 @@ end +instantiation word :: (len) semiring_bit_shifts +begin + +lift_definition push_bit_word :: \nat \ 'a word \ 'a word\ + is push_bit +proof - + show \take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\ + if \take_bit LENGTH('a) k = take_bit LENGTH('a) l\ for k l :: int and n :: nat + proof - + from that + have \take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k) + = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)\ + by simp + moreover have \min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\ + by simp + ultimately show ?thesis + by (simp add: take_bit_push_bit) + qed +qed + +lift_definition drop_bit_word :: \nat \ 'a word \ 'a word\ + is \\n. drop_bit n \ take_bit LENGTH('a)\ + by (simp add: take_bit_eq_mod) + +instance proof + show \push_bit n a = a * 2 ^ n\ for n :: nat and a :: "'a word" + by transfer (simp add: push_bit_eq_mult) + show \drop_bit n a = a div 2 ^ n\ for n :: nat and a :: "'a word" + by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit) +qed + +end + definition shiftl1 :: "'a::len0 word \ 'a word" where "shiftl1 w = word_of_int (uint w BIT False)" +lemma shiftl1_eq_mult_2: + \shiftl1 = (*) 2\ + apply (simp add: fun_eq_iff shiftl1_def Bit_def) + apply (simp only: mult_2) + apply transfer + apply (simp only: take_bit_add) + apply simp + done + definition shiftr1 :: "'a::len0 word \ 'a word" \ \shift right as unsigned or as signed, ie logical or arithmetic\ where "shiftr1 w = word_of_int (bin_rest (uint w))" +lemma shiftr1_eq_div_2: + \shiftr1 w = w div 2\ + apply (simp add: fun_eq_iff shiftr1_def) + apply transfer + apply (auto simp add: not_le dest: less_2_cases) + done + instantiation word :: (len0) bit_operations begin @@ -773,6 +822,35 @@ end +lemma test_bit_word_eq: + \test_bit w = bit w\ for w :: \'a::len word\ + apply (simp add: word_test_bit_def fun_eq_iff) + apply transfer + apply (simp add: bit_take_bit_iff) + done + +lemma lsb_word_eq: + \lsb = (odd :: 'a word \ bool)\ for w :: \'a::len word\ + apply (simp add: word_lsb_def fun_eq_iff) + apply transfer + apply simp + done + +lemma msb_word_eq: + \msb w \ bit w (LENGTH('a) - 1)\ for w :: \'a::len word\ + apply (simp add: msb_word_def bin_sign_lem) + apply transfer + apply (simp add: bit_take_bit_iff) + done + +lemma shiftl_word_eq: + \w << n = push_bit n w\ for w :: \'a::len word\ + by (induction n) (simp_all add: shiftl_def shiftl1_eq_mult_2 push_bit_double) + +lemma shiftr_word_eq: + \w >> n = drop_bit n w\ for w :: \'a::len word\ + by (induction n) (simp_all add: shiftr_def shiftr1_eq_div_2 drop_bit_Suc drop_bit_half) + lemma word_msb_def: "msb a \ bin_sign (sint a) = - 1" by (simp add: msb_word_def sint_uint)