# HG changeset patch
# User haftmann
# Date 1596617265 0
# Node ID 3ec8761815274858355fed8ff059ac6ef14de282
# Parent  41393ecb57ace7ccd69e36f6a377678f50d4512a
further refinement of code equations for mask operation

diff -r 41393ecb57ac -r 3ec876181527 src/HOL/Library/Bit_Operations.thy
--- 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
 
diff -r 41393ecb57ac -r 3ec876181527 src/HOL/Word/Word.thy
--- 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>