--- 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
--- 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)