# HG changeset patch
# User haftmann
# Date 1633933929 0
# Node ID 27475e64a8871389a4fe7d0bb304d8a616b67ef6
# Parent  9c04a82c312850bd2c9e23e9c061be090cbe1998
more complete simp rules

diff -r 9c04a82c3128 -r 27475e64a887 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Sun Oct 10 18:16:57 2021 +0000
+++ b/src/HOL/Bit_Operations.thy	Mon Oct 11 06:32:09 2021 +0000
@@ -1412,6 +1412,14 @@
   \<open>push_bit (numeral l) (- numeral k) = push_bit (pred_numeral l) (- numeral (Num.Bit0 k))\<close>
   by (simp only: numeral_eq_Suc push_bit_Suc_minus_numeral)
 
+lemma take_bit_Suc_1:
+  \<open>take_bit (Suc n) (- 1) = 2 ^ Suc n - 1\<close>
+  by (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1)
+
+lemma take_bit_numeral_1 [simp]:
+  \<open>take_bit (numeral k) (- 1) = 2 ^ numeral k - 1\<close>
+  by (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1)
+
 end
 
 
diff -r 9c04a82c3128 -r 27475e64a887 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sun Oct 10 18:16:57 2021 +0000
+++ b/src/HOL/Library/Word.thy	Mon Oct 11 06:32:09 2021 +0000
@@ -3508,18 +3508,86 @@
 
 subsubsection \<open>shift functions in terms of lists of bools\<close>
 
-text \<open>TODO: rules for \<^term>\<open>- (numeral n)\<close>\<close>
-
 lemma drop_bit_word_numeral [simp]:
   \<open>drop_bit (numeral n) (numeral k) =
     (word_of_int (drop_bit (numeral n) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)\<close>
   by transfer simp
 
+lemma drop_bit_word_Suc_numeral [simp]:
+  \<open>drop_bit (Suc n) (numeral k) =
+    (word_of_int (drop_bit (Suc n) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)\<close>
+  by transfer simp
+
+lemma drop_bit_word_minus_numeral [simp]:
+  \<open>drop_bit (numeral n) (- numeral k) =
+    (word_of_int (drop_bit (numeral n) (take_bit LENGTH('a) (- numeral k))) :: 'a::len word)\<close>
+  by transfer simp
+
+lemma drop_bit_word_Suc_minus_numeral [simp]:
+  \<open>drop_bit (Suc n) (- numeral k) =
+    (word_of_int (drop_bit (Suc n) (take_bit LENGTH('a) (- numeral k))) :: 'a::len word)\<close>
+  by transfer simp
+
 lemma signed_drop_bit_word_numeral [simp]:
   \<open>signed_drop_bit (numeral n) (numeral k) =
     (word_of_int (drop_bit (numeral n) (signed_take_bit (LENGTH('a) - 1) (numeral k))) :: 'a::len word)\<close>
   by transfer simp
 
+lemma signed_drop_bit_word_Suc_numeral [simp]:
+  \<open>signed_drop_bit (Suc n) (numeral k) =
+    (word_of_int (drop_bit (Suc n) (signed_take_bit (LENGTH('a) - 1) (numeral k))) :: 'a::len word)\<close>
+  by transfer simp
+
+lemma signed_drop_bit_word_minus_numeral [simp]:
+  \<open>signed_drop_bit (numeral n) (- numeral k) =
+    (word_of_int (drop_bit (numeral n) (signed_take_bit (LENGTH('a) - 1) (- numeral k))) :: 'a::len word)\<close>
+  by transfer simp
+
+lemma signed_drop_bit_word_Suc_minus_numeral [simp]:
+  \<open>signed_drop_bit (Suc n) (- numeral k) =
+    (word_of_int (drop_bit (Suc n) (signed_take_bit (LENGTH('a) - 1) (- numeral k))) :: 'a::len word)\<close>
+  by transfer simp
+
+lemma take_bit_word_numeral [simp]:
+  \<open>take_bit (numeral n) (numeral k) =
+    (word_of_int (take_bit (min LENGTH('a) (numeral n)) (numeral k)) :: 'a::len word)\<close>
+  by transfer rule
+
+lemma take_bit_word_Suc_numeral [simp]:
+  \<open>take_bit (Suc n) (numeral k) =
+    (word_of_int (take_bit (min LENGTH('a) (Suc n)) (numeral k)) :: 'a::len word)\<close>
+  by transfer rule
+
+lemma take_bit_word_minus_numeral [simp]:
+  \<open>take_bit (numeral n) (- numeral k) =
+    (word_of_int (take_bit (min LENGTH('a) (numeral n)) (- numeral k)) :: 'a::len word)\<close>
+  by transfer rule
+
+lemma take_bit_word_Suc_minus_numeral [simp]:
+  \<open>take_bit (Suc n) (- numeral k) =
+    (word_of_int (take_bit (min LENGTH('a) (Suc n)) (- numeral k)) :: 'a::len word)\<close>
+  by transfer rule
+
+lemma signed_take_bit_word_numeral [simp]:
+  \<open>signed_take_bit (numeral n) (numeral k) =
+    (word_of_int (signed_take_bit (numeral n) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)\<close>
+  by transfer rule
+
+lemma signed_take_bit_word_Suc_numeral [simp]:
+  \<open>signed_take_bit (Suc n) (numeral k) =
+    (word_of_int (signed_take_bit (Suc n) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)\<close>
+  by transfer rule
+
+lemma signed_take_bit_word_minus_numeral [simp]:
+  \<open>signed_take_bit (numeral n) (- numeral k) =
+    (word_of_int (signed_take_bit (numeral n) (take_bit LENGTH('a) (- numeral k))) :: 'a::len word)\<close>
+  by transfer rule
+
+lemma signed_take_bit_word_Suc_minus_numeral [simp]:
+  \<open>signed_take_bit (Suc n) (- numeral k) =
+    (word_of_int (signed_take_bit (Suc n) (take_bit LENGTH('a) (- numeral k))) :: 'a::len word)\<close>
+  by transfer rule
+
 lemma False_map2_or: "\<lbrakk>set xs \<subseteq> {False}; length ys = length xs\<rbrakk> \<Longrightarrow> map2 (\<or>) xs ys = ys"
   by (induction xs arbitrary: ys) (auto simp: length_Suc_conv)