--- a/src/HOL/Library/Bit_Operations.thy Sun Jul 12 18:10:06 2020 +0000
+++ b/src/HOL/Library/Bit_Operations.thy Mon Jul 13 15:23:32 2020 +0000
@@ -536,6 +536,14 @@
by (simp add: not_add_distrib)
qed
+lemma mask_nonnegative_int [simp]:
+ \<open>mask n \<ge> (0::int)\<close>
+ by (simp add: mask_eq_exp_minus_1)
+
+lemma not_mask_negative_int [simp]:
+ \<open>\<not> mask n < (0::int)\<close>
+ by (simp add: not_less)
+
lemma not_nonnegative_int_iff [simp]:
\<open>NOT k \<ge> 0 \<longleftrightarrow> k < 0\<close> for k :: int
by (simp add: not_int_def)
@@ -633,10 +641,6 @@
\<open>k XOR l < 0 \<longleftrightarrow> (k < 0) \<noteq> (l < 0)\<close> for k l :: int
by (subst Not_eq_iff [symmetric]) (auto simp add: not_less)
-lemma mask_nonnegative:
- \<open>(mask n :: int) \<ge> 0\<close>
- by (simp add: mask_eq_exp_minus_1)
-
lemma set_bit_nonnegative_int_iff [simp]:
\<open>set_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
by (simp add: set_bit_def)
@@ -716,10 +720,57 @@
qed
+subsection \<open>Bit concatenation\<close>
+
+definition concat_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int\<close>
+ where \<open>concat_bit n k l = (k AND mask n) OR push_bit n l\<close>
+
+lemma bit_concat_bit_iff:
+ \<open>bit (concat_bit m k l) n \<longleftrightarrow> n < m \<and> bit k n \<or> m \<le> n \<and> bit l (n - m)\<close>
+ by (simp add: concat_bit_def bit_or_iff bit_and_iff bit_mask_iff bit_push_bit_iff ac_simps)
+
+lemma concat_bit_eq:
+ \<open>concat_bit n k l = take_bit n k + push_bit n l\<close>
+ by (simp add: concat_bit_def take_bit_eq_mask
+ bit_and_iff bit_mask_iff bit_push_bit_iff disjunctive_add)
+
+lemma concat_bit_0 [simp]:
+ \<open>concat_bit 0 k l = l\<close>
+ by (simp add: concat_bit_def)
+
+lemma concat_bit_Suc:
+ \<open>concat_bit (Suc n) k l = k mod 2 + 2 * concat_bit n (k div 2) l\<close>
+ by (simp add: concat_bit_eq take_bit_Suc push_bit_double)
+
+lemma concat_bit_of_zero_1 [simp]:
+ \<open>concat_bit n 0 l = push_bit n l\<close>
+ by (simp add: concat_bit_def)
+
+lemma concat_bit_of_zero_2 [simp]:
+ \<open>concat_bit n k 0 = take_bit n k\<close>
+ by (simp add: concat_bit_def take_bit_eq_mask)
+
+lemma concat_bit_nonnegative_iff [simp]:
+ \<open>concat_bit n k l \<ge> 0 \<longleftrightarrow> l \<ge> 0\<close>
+ by (simp add: concat_bit_def)
+
+lemma concat_bit_negative_iff [simp]:
+ \<open>concat_bit n k l < 0 \<longleftrightarrow> l < 0\<close>
+ by (simp add: concat_bit_def)
+
+lemma concat_bit_assoc:
+ \<open>concat_bit n k (concat_bit m l r) = concat_bit (m + n) (concat_bit n k l) r\<close>
+ by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps)
+
+lemma concat_bit_assoc_sym:
+ \<open>concat_bit m (concat_bit n k l) r = concat_bit (min m n) k (concat_bit (m - n) l r)\<close>
+ by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps min_def)
+
+
subsection \<open>Taking bit with sign propagation\<close>
-definition signed_take_bit :: "nat \<Rightarrow> int \<Rightarrow> int"
- where \<open>signed_take_bit n k = take_bit n k OR (NOT (mask n) * of_bool (bit k n))\<close>
+definition signed_take_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+ where \<open>signed_take_bit n k = concat_bit n k (- of_bool (bit k n))\<close>
lemma signed_take_bit_eq:
\<open>signed_take_bit n k = take_bit n k\<close> if \<open>\<not> bit k n\<close>
@@ -727,7 +778,7 @@
lemma signed_take_bit_eq_or:
\<open>signed_take_bit n k = take_bit n k OR NOT (mask n)\<close> if \<open>bit k n\<close>
- using that by (simp add: signed_take_bit_def)
+ using that by (simp add: signed_take_bit_def concat_bit_def take_bit_eq_mask push_bit_minus_one_eq_not_mask)
lemma signed_take_bit_0 [simp]:
\<open>signed_take_bit 0 k = - (k mod 2)\<close>
@@ -740,7 +791,7 @@
lemma signed_take_bit_Suc:
\<open>signed_take_bit (Suc n) k = k mod 2 + 2 * signed_take_bit n (k div 2)\<close>
by (unfold signed_take_bit_def or_int_rec [of \<open>take_bit (Suc n) k\<close>])
- (simp add: bit_Suc take_bit_Suc even_or_iff even_mask_iff odd_iff_mod_2_eq_one not_int_div_2 mask_half_int)
+ (simp add: bit_Suc concat_bit_Suc even_or_iff even_mask_iff odd_iff_mod_2_eq_one not_int_div_2 mask_half_int)
lemma signed_take_bit_rec:
\<open>signed_take_bit n k = (if n = 0 then - (k mod 2) else k mod 2 + 2 * signed_take_bit (n - 1) (k div 2))\<close>
@@ -748,7 +799,7 @@
lemma bit_signed_take_bit_iff:
\<open>bit (signed_take_bit m k) n = bit k (min m n)\<close>
- by (simp add: signed_take_bit_def bit_or_iff bit_take_bit_iff bit_not_iff bit_mask_iff min_def)
+ by (simp add: signed_take_bit_def bit_or_iff bit_concat_bit_iff bit_not_iff bit_mask_iff min_def)
text \<open>Modulus centered around 0\<close>
@@ -790,7 +841,9 @@
by (rule disjunctive_add)
(auto simp add: disjunctive_add bit_take_bit_iff bit_double_iff bit_exp_iff)
finally show ?thesis
- using * ** by (simp add: signed_take_bit_def take_bit_Suc min_def ac_simps)
+ using * **
+ by (simp add: signed_take_bit_def concat_bit_Suc min_def ac_simps)
+ (simp add: concat_bit_def take_bit_eq_mask push_bit_minus_one_eq_not_mask ac_simps)
qed
lemma signed_take_bit_of_0 [simp]:
@@ -799,7 +852,7 @@
lemma signed_take_bit_of_minus_1 [simp]:
\<open>signed_take_bit n (- 1) = - 1\<close>
- by (simp add: signed_take_bit_def take_bit_minus_one_eq_mask)
+ by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask take_bit_minus_one_eq_mask)
lemma signed_take_bit_eq_iff_take_bit_eq:
\<open>signed_take_bit n k = signed_take_bit n l \<longleftrightarrow> take_bit (Suc n) k = take_bit (Suc n) l\<close>
@@ -809,7 +862,7 @@
for k :: int
by (auto simp add: disjunctive_add [symmetric] bit_not_iff bit_mask_iff bit_take_bit_iff minus_exp_eq_not_mask)
ultimately show ?thesis
- by (simp add: signed_take_bit_def take_bit_Suc_from_most)
+ by (simp add: signed_take_bit_def take_bit_Suc_from_most concat_bit_eq)
next
case False
then have \<open>signed_take_bit n k \<noteq> signed_take_bit n l\<close> and \<open>take_bit (Suc n) k \<noteq> take_bit (Suc n) l\<close>
@@ -836,11 +889,11 @@
lemma signed_take_bit_nonnegative_iff [simp]:
\<open>0 \<le> signed_take_bit n k \<longleftrightarrow> \<not> bit k n\<close>
- by (simp add: signed_take_bit_def not_less mask_nonnegative)
+ by (simp add: signed_take_bit_def not_less concat_bit_def)
lemma signed_take_bit_negative_iff [simp]:
\<open>signed_take_bit n k < 0 \<longleftrightarrow> bit k n\<close>
- by (simp add: signed_take_bit_def not_less mask_nonnegative)
+ by (simp add: signed_take_bit_def not_less concat_bit_def)
lemma signed_take_bit_greater_eq:
\<open>k + 2 ^ Suc n \<le> signed_take_bit n k\<close> if \<open>k < - (2 ^ n)\<close>
@@ -1096,6 +1149,12 @@
\<^item> Unset a single bit: @{thm unset_bit_def [where ?'a = int, no_vars]}
\<^item> Flip a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]}
+
+ \<^item> Bit concatenation: @{thm concat_bit_def [no_vars]}
+
+ \<^item> Truncation centered towards \<^term>\<open>0::int\<close>: @{thm signed_take_bit_def [no_vars]}
+
+ \<^item> (Bounded) conversion from and to a list of bits: @{thm horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
\<close>
end