--- a/src/HOL/Library/Bit_Operations.thy Tue Aug 04 09:33:05 2020 +0000
+++ b/src/HOL/Library/Bit_Operations.thy Wed Aug 05 08:47:45 2020 +0000
@@ -958,17 +958,18 @@
lemma signed_take_bit_code [code]:
\<open>signed_take_bit n k =
- (let l = k AND mask (Suc n)
+ (let l = take_bit (Suc n) k
in if bit l n then l - (push_bit n 2) else l)\<close>
proof -
- have *: \<open>(k AND mask (Suc n)) - 2 * 2 ^ n = k AND mask (Suc n) OR NOT (mask (Suc n))\<close>
+ have *: \<open>(take_bit (Suc n) k) - 2 * 2 ^ n = take_bit (Suc n) k OR NOT (mask (Suc n))\<close>
apply (subst disjunctive_add [symmetric])
- apply (simp_all add: bit_and_iff bit_mask_iff bit_not_iff)
+ apply (simp_all add: bit_and_iff bit_mask_iff bit_not_iff bit_take_bit_iff)
apply (simp flip: minus_exp_eq_not_mask)
done
show ?thesis
by (rule bit_eqI)
- (auto simp add: Let_def bit_and_iff bit_signed_take_bit_iff push_bit_eq_mult min_def not_le bit_mask_iff bit_exp_iff less_Suc_eq * bit_or_iff bit_not_iff)
+ (auto simp add: Let_def bit_and_iff bit_signed_take_bit_iff push_bit_eq_mult min_def not_le
+ bit_mask_iff bit_exp_iff less_Suc_eq * bit_or_iff bit_take_bit_iff bit_not_iff)
qed
@@ -1066,6 +1067,10 @@
end
+lemma [code]:
+ \<open>mask n = 2 ^ n - (1::integer)\<close>
+ by (simp add: mask_eq_exp_minus_1)
+
instantiation natural :: semiring_bit_operations
begin
@@ -1086,6 +1091,10 @@
end
+lemma [code]:
+ \<open>integer_of_natural (mask n) = mask n\<close>
+ by transfer (simp add: mask_eq_exp_minus_1 of_nat_diff)
+
lifting_update integer.lifting
lifting_forget integer.lifting
--- a/src/HOL/Word/Word.thy Tue Aug 04 09:33:05 2020 +0000
+++ b/src/HOL/Word/Word.thy Wed Aug 05 08:47:45 2020 +0000
@@ -1164,13 +1164,13 @@
by (simp add: shiftr_word_eq)
lemma [code]:
- \<open>take_bit n a = a AND mask n\<close> for a :: \<open>'a::len word\<close>
- by (fact take_bit_eq_mask)
+ \<open>uint (take_bit n w) = (if n < LENGTH('a::len) then take_bit n (uint w) else uint w)\<close>
+ for w :: \<open>'a::len word\<close>
+ by transfer (simp add: min_def)
lemma [code]:
- \<open>mask (Suc n) = push_bit n (1 :: 'a word) OR mask n\<close>
- \<open>mask 0 = (0 :: 'a::len word)\<close>
- by (simp_all add: mask_Suc_exp push_bit_of_1)
+ \<open>uint (mask n :: 'a::len word) = mask (min LENGTH('a) n)\<close>
+ by transfer simp
lemma [code_abbrev]:
\<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>