concatentation of bit values

--- a/NEWS	Sun Jul 12 18:10:06 2020 +0000
+++ b/NEWS	Mon Jul 13 15:23:32 2020 +0000
@@ -75,8 +75,8 @@
 into its components "drop_bit" and "take_bit".  INCOMPATIBILITY.
 
 * Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth",
-"bintrunc", "sbintrunc" and "max_word" are now mere input abbreviations.
-Minor INCOMPATIBILITY.
+"bintrunc", "sbintrunc", "bin_cat" and "max_word" are now mere
+input abbreviations.  Minor INCOMPATIBILITY.
 
 * Session HOL-Word: Theory HOL-Library.Z2 is not imported any longer.
 Minor INCOMPATIBILITY.

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

--- a/src/HOL/Word/Ancient_Numeral.thy	Sun Jul 12 18:10:06 2020 +0000
+++ b/src/HOL/Word/Ancient_Numeral.thy	Mon Jul 13 15:23:32 2020 +0000
@@ -180,7 +180,7 @@
   by (cases n) (simp_all add: Bit_def signed_take_bit_Suc)
 
 lemma bin_cat_Suc_Bit: "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
-  by (auto simp add: Bit_def)
+  by (auto simp add: Bit_def concat_bit_Suc)
 
 lemma int_not_BIT [simp]: "NOT (w BIT b) = (NOT w) BIT (\<not> b)"
   by (simp add: not_int_def Bit_def)

--- a/src/HOL/Word/Bits_Int.thy	Sun Jul 12 18:10:06 2020 +0000
+++ b/src/HOL/Word/Bits_Int.thy	Mon Jul 13 15:23:32 2020 +0000
@@ -291,7 +291,7 @@
   by (simp_all add: signed_take_bit_Suc)
 
 lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = -1) = bit bin n"
-  using mask_nonnegative [of n] by (simp add: bin_sign_def not_le signed_take_bit_def)
+  by (simp add: bin_sign_def)
 
 lemma nth_bintr: "bin_nth (bintrunc m w) n \<longleftrightarrow> n < m \<and> bin_nth w n"
   by (fact bit_take_bit_iff)
@@ -553,16 +553,13 @@
   "bin_split 0 w = (w, 0)"
   by (simp_all add: drop_bit_Suc take_bit_Suc mod_2_eq_odd)
 
-primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int"
-  where
-    Z: "bin_cat w 0 v = w"
-  | Suc: "bin_cat w (Suc n) v = of_bool (odd v) + 2 * bin_cat w n (v div 2)"
+abbreviation (input) bin_cat :: \<open>int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>bin_cat k n l \<equiv> concat_bit n l k\<close>
 
 lemma bin_cat_eq_push_bit_add_take_bit:
   \<open>bin_cat k n l = push_bit n k + take_bit n l\<close>
-  by (induction n arbitrary: k l)
-    (simp_all add: take_bit_Suc push_bit_double mod_2_eq_odd)
-
+  by (simp add: concat_bit_eq)
+  
 lemma bin_sign_cat: "bin_sign (bin_cat x n y) = bin_sign x"
 proof -
   have \<open>0 \<le> x\<close> if \<open>0 \<le> x * 2 ^ n + y mod 2 ^ n\<close>
@@ -588,13 +585,10 @@
 qed
 
 lemma bin_cat_assoc: "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
-  by (induct n arbitrary: z) auto
+  by (fact concat_bit_assoc)
 
 lemma bin_cat_assoc_sym: "bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
-  apply (induct n arbitrary: z m)
-   apply clarsimp
-  apply (case_tac m, auto)
-  done
+  by (fact concat_bit_assoc_sym)
 
 definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
   where "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
@@ -625,11 +619,7 @@
 lemma bin_nth_cat:
   "bin_nth (bin_cat x k y) n =
     (if n < k then bin_nth y n else bin_nth x (n - k))"
-  apply (induct k arbitrary: n y)
-   apply simp
-  apply (case_tac n)
-   apply (simp_all add: bit_Suc)
-  done
+  by (simp add: bit_concat_bit_iff)
 
 lemma bin_nth_drop_bit_iff:
   \<open>bin_nth (drop_bit n c) k \<longleftrightarrow> bin_nth c (n + k)\<close>
@@ -653,6 +643,7 @@
 
 lemma bintr_cat: "bintrunc m (bin_cat a n b) =
     bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
+  
   by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
 
 lemma bintr_cat_same [simp]: "bintrunc n (bin_cat a n b) = bintrunc n b"
@@ -669,13 +660,11 @@
 
 lemma drop_bit_bin_cat_eq:
   \<open>drop_bit n (bin_cat v n w) = v\<close>
-  by (induct n arbitrary: w)
-    (simp_all add: drop_bit_Suc)
+  by (rule bit_eqI) (simp add: bit_drop_bit_eq bit_concat_bit_iff)
 
 lemma take_bit_bin_cat_eq:
   \<open>take_bit n (bin_cat v n w) = take_bit n w\<close>
-  by (induct n arbitrary: w)
-    (simp_all add: take_bit_Suc mod_2_eq_odd)
+  by (rule bit_eqI) (simp add: bit_concat_bit_iff)
 
 lemma bin_split_cat: "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
   by (simp add: drop_bit_bin_cat_eq take_bit_bin_cat_eq)
@@ -1913,9 +1902,9 @@
     (auto simp add: bin_nth_of_bl_aux bin_nth_cat algebra_simps)
 
 lemma bin_to_bl_aux_cat:
-  "\<And>w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
+  "bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
     bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
-  by (induct nw) auto
+  by (induction nw arbitrary: w bs) (simp_all add: concat_bit_Suc)
 
 lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
   using bl_to_bin_aux_cat [where nv = "0" and v = "0"]