# HG changeset patch
# User haftmann
# Date 1555444203 0
# Node ID 8bb835f10a393ae601a0bc75eaa7be5b9fa992e4
# Parent  e79bbf86a984b4e92cdaff572e4a05f4599793d0
moved instance to appropriate place

diff -r e79bbf86a984 -r 8bb835f10a39 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Apr 16 20:00:14 2019 +0200
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Apr 16 19:50:03 2019 +0000
@@ -2,7 +2,7 @@
     Author:     Jeremy Dawson, NICTA
 *)
 
-section \<open>Integers as implict bit strings\<close>
+section \<open>Integers as implicit bit strings\<close>
 
 theory Bit_Representation
   imports Misc_Numeric
@@ -25,6 +25,9 @@
 lemma Bit_B1_2t: "k BIT True = 2 * k + 1"
   by (rule trans, rule Bit_B1) simp
 
+lemma power_BIT: "2 ^ Suc n - 1 = (2 ^ n - 1) BIT True"
+  by (simp add: Bit_B1)
+
 definition bin_last :: "int \<Rightarrow> bool"
   where "bin_last w \<longleftrightarrow> w mod 2 = 1"
 
@@ -242,6 +245,14 @@
   bin_nth.Z bin_nth.Suc bin_nth_zero bin_nth_minus1
   bin_nth_numeral_simps
 
+lemma nth_2p_bin: "bin_nth (2 ^ n) m = (m = n)" \<comment> \<open>for use when simplifying with \<open>bin_nth_Bit\<close>\<close>
+  apply (induct n arbitrary: m)
+   apply clarsimp
+   apply safe
+   apply (case_tac m)
+    apply (auto simp: Bit_B0_2t [symmetric])
+  done 
+
 
 subsection \<open>Truncating binary integers\<close>
 
@@ -682,4 +693,129 @@
     Z: "bin_cat w 0 v = w"
   | Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
 
+lemma bin_sign_cat: "bin_sign (bin_cat x n y) = bin_sign x"
+  by (induct n arbitrary: y) auto
+
+lemma bin_cat_Suc_Bit: "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
+  by auto
+
+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
+
+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
+
+definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
+  where "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
+
+fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
+  where "bin_rsplit_aux n m c bs =
+    (if m = 0 \<or> n = 0 then bs
+     else
+      let (a, b) = bin_split n c
+      in bin_rsplit_aux n (m - n) a (b # bs))"
+
+definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
+  where "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
+
+fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
+  where "bin_rsplitl_aux n m c bs =
+    (if m = 0 \<or> n = 0 then bs
+     else
+      let (a, b) = bin_split (min m n) c
+      in bin_rsplitl_aux n (m - n) a (b # bs))"
+
+definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
+  where "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
+
+declare bin_rsplit_aux.simps [simp del]
+declare bin_rsplitl_aux.simps [simp del]
+
+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 clarsimp
+  apply (case_tac n, auto)
+  done
+
+lemma bin_nth_split:
+  "bin_split n c = (a, b) \<Longrightarrow>
+    (\<forall>k. bin_nth a k = bin_nth c (n + k)) \<and>
+    (\<forall>k. bin_nth b k = (k < n \<and> bin_nth c k))"
+  apply (induct n arbitrary: b c)
+   apply clarsimp
+  apply (clarsimp simp: Let_def split: prod.split_asm)
+  apply (case_tac k)
+  apply auto
+  done
+
+lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
+  by (induct n arbitrary: w) auto
+
+lemma bintr_cat1: "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
+  by (induct n arbitrary: b) auto
+
+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"
+  by (auto simp add : bintr_cat)
+
+lemma cat_bintr [simp]: "bin_cat a n (bintrunc n b) = bin_cat a n b"
+  by (induct n arbitrary: b) auto
+
+lemma split_bintrunc: "bin_split n c = (a, b) \<Longrightarrow> b = bintrunc n c"
+  by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm)
+
+lemma bin_cat_split: "bin_split n w = (u, v) \<Longrightarrow> w = bin_cat u n v"
+  by (induct n arbitrary: v w) (auto simp: Let_def split: prod.split_asm)
+
+lemma bin_split_cat: "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
+  by (induct n arbitrary: w) auto
+
+lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
+  by (induct n) auto
+
+lemma bin_split_minus1 [simp]:
+  "bin_split n (- 1) = (- 1, bintrunc n (- 1))"
+  by (induct n) auto
+
+lemma bin_split_trunc:
+  "bin_split (min m n) c = (a, b) \<Longrightarrow>
+    bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
+  apply (induct n arbitrary: m b c, clarsimp)
+  apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
+  apply (case_tac m)
+   apply (auto simp: Let_def split: prod.split_asm)
+  done
+
+lemma bin_split_trunc1:
+  "bin_split n c = (a, b) \<Longrightarrow>
+    bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
+  apply (induct n arbitrary: m b c, clarsimp)
+  apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
+  apply (case_tac m)
+   apply (auto simp: Let_def split: prod.split_asm)
+  done
+
+lemma bin_cat_num: "bin_cat a n b = a * 2 ^ n + bintrunc n b"
+  apply (induct n arbitrary: b)
+   apply clarsimp
+  apply (simp add: Bit_def)
+  done
+
+lemma bin_split_num: "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
+  apply (induct n arbitrary: b)
+   apply simp
+  apply (simp add: bin_rest_def zdiv_zmult2_eq)
+  apply (case_tac b rule: bin_exhaust)
+  apply simp
+  apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
+  done
+
 end
diff -r e79bbf86a984 -r 8bb835f10a39 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Tue Apr 16 20:00:14 2019 +0200
+++ b/src/HOL/Word/Bits_Int.thy	Tue Apr 16 19:50:03 2019 +0000
@@ -9,7 +9,7 @@
 section \<open>Bitwise Operations on Binary Integers\<close>
 
 theory Bits_Int
-  imports Bits Bit_Representation
+  imports Bits Bit_Representation Bool_List_Representation
 begin
 
 subsection \<open>Logical operations\<close>
@@ -365,6 +365,41 @@
   apply (case_tac bit, auto)
   done
 
+lemma mod_BIT: "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
+proof -
+  have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
+    by (simp add: mod_mult_mult1)
+  also have "\<dots> = ((2 * bin mod 2 ^ Suc n) + 1) mod 2 ^ Suc n"
+    by (simp add: ac_simps p1mod22k')
+  also have "\<dots> = (2 * bin + 1) mod 2 ^ Suc n"
+    by (simp only: mod_simps)
+  finally show ?thesis
+    by (auto simp add: Bit_def)
+qed
+
+lemma AND_mod: "x AND 2 ^ n - 1 = x mod 2 ^ n"
+  for x :: int
+proof (induct x arbitrary: n rule: bin_induct)
+  case 1
+  then show ?case
+    by simp
+next
+  case 2
+  then show ?case
+    by (simp, simp add: m1mod2k)
+next
+  case (3 bin bit)
+  show ?case
+  proof (cases n)
+    case 0
+    then show ?thesis by simp
+  next
+    case (Suc m)
+    with 3 show ?thesis
+      by (simp only: power_BIT mod_BIT int_and_Bits) simp
+  qed
+qed
+
 
 subsubsection \<open>Truncating results of bit-wise operations\<close>
 
@@ -386,6 +421,53 @@
 lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
 lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
 
+lemma bl_xor_aux_bin:
+  "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+    bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
+  apply (induct n arbitrary: v w bs cs)
+   apply simp
+  apply (case_tac v rule: bin_exhaust)
+  apply (case_tac w rule: bin_exhaust)
+  apply clarsimp
+  apply (case_tac b)
+   apply auto
+  done
+
+lemma bl_or_aux_bin:
+  "map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+    bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)"
+  apply (induct n arbitrary: v w bs cs)
+   apply simp
+  apply (case_tac v rule: bin_exhaust)
+  apply (case_tac w rule: bin_exhaust)
+  apply clarsimp
+  done
+
+lemma bl_and_aux_bin:
+  "map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+    bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)"
+  apply (induct n arbitrary: v w bs cs)
+   apply simp
+  apply (case_tac v rule: bin_exhaust)
+  apply (case_tac w rule: bin_exhaust)
+  apply clarsimp
+  done
+
+lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)"
+  by (induct n arbitrary: w cs) auto
+
+lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
+  by (simp add: bin_to_bl_def bl_not_aux_bin)
+
+lemma bl_and_bin: "map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
+  by (simp add: bin_to_bl_def bl_and_aux_bin)
+
+lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
+  by (simp add: bin_to_bl_def bl_or_aux_bin)
+
+lemma bl_xor_bin: "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
+  by (simp only: bin_to_bl_def bl_xor_aux_bin map2_Nil)
+
 
 subsection \<open>Setting and clearing bits\<close>
 
@@ -470,186 +552,33 @@
     bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
   by (simp add: numeral_eq_Suc)
 
-
-subsection \<open>Splitting and concatenation\<close>
-
-definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
-  where "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
-
-fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
-  where "bin_rsplit_aux n m c bs =
-    (if m = 0 \<or> n = 0 then bs
-     else
-      let (a, b) = bin_split n c
-      in bin_rsplit_aux n (m - n) a (b # bs))"
-
-definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
-  where "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
-
-fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
-  where "bin_rsplitl_aux n m c bs =
-    (if m = 0 \<or> n = 0 then bs
-     else
-      let (a, b) = bin_split (min m n) c
-      in bin_rsplitl_aux n (m - n) a (b # bs))"
-
-definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
-  where "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
-
-declare bin_rsplit_aux.simps [simp del]
-declare bin_rsplitl_aux.simps [simp del]
-
-lemma bin_sign_cat: "bin_sign (bin_cat x n y) = bin_sign x"
-  by (induct n arbitrary: y) auto
-
-lemma bin_cat_Suc_Bit: "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
-  by auto
-
-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 clarsimp
-  apply (case_tac n, auto)
-  done
+instantiation int :: bitss
+begin
 
-lemma bin_nth_split:
-  "bin_split n c = (a, b) \<Longrightarrow>
-    (\<forall>k. bin_nth a k = bin_nth c (n + k)) \<and>
-    (\<forall>k. bin_nth b k = (k < n \<and> bin_nth c k))"
-  apply (induct n arbitrary: b c)
-   apply clarsimp
-  apply (clarsimp simp: Let_def split: prod.split_asm)
-  apply (case_tac k)
-  apply auto
-  done
-
-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
-
-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
+definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
 
-lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
-  by (induct n arbitrary: w) auto
-
-lemma bintr_cat1: "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
-  by (induct n arbitrary: b) auto
-
-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)
+definition "lsb i = i !! 0" for i :: int
 
-lemma bintr_cat_same [simp]: "bintrunc n (bin_cat a n b) = bintrunc n b"
-  by (auto simp add : bintr_cat)
-
-lemma cat_bintr [simp]: "bin_cat a n (bintrunc n b) = bin_cat a n b"
-  by (induct n arbitrary: b) auto
-
-lemma split_bintrunc: "bin_split n c = (a, b) \<Longrightarrow> b = bintrunc n c"
-  by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm)
-
-lemma bin_cat_split: "bin_split n w = (u, v) \<Longrightarrow> w = bin_cat u n v"
-  by (induct n arbitrary: v w) (auto simp: Let_def split: prod.split_asm)
-
-lemma bin_split_cat: "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
-  by (induct n arbitrary: w) auto
+definition "set_bit i n b = bin_sc n b i"
 
-lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
-  by (induct n) auto
-
-lemma bin_split_minus1 [simp]:
-  "bin_split n (- 1) = (- 1, bintrunc n (- 1))"
-  by (induct n) auto
-
-lemma bin_split_trunc:
-  "bin_split (min m n) c = (a, b) \<Longrightarrow>
-    bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
-  apply (induct n arbitrary: m b c, clarsimp)
-  apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
-  apply (case_tac m)
-   apply (auto simp: Let_def split: prod.split_asm)
-  done
-
-lemma bin_split_trunc1:
-  "bin_split n c = (a, b) \<Longrightarrow>
-    bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
-  apply (induct n arbitrary: m b c, clarsimp)
-  apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
-  apply (case_tac m)
-   apply (auto simp: Let_def split: prod.split_asm)
-  done
-
-lemma bin_cat_num: "bin_cat a n b = a * 2 ^ n + bintrunc n b"
-  apply (induct n arbitrary: b)
-   apply clarsimp
-  apply (simp add: Bit_def)
-  done
-
-lemma bin_split_num: "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
-  apply (induct n arbitrary: b)
-   apply simp
-  apply (simp add: bin_rest_def zdiv_zmult2_eq)
-  apply (case_tac b rule: bin_exhaust)
-  apply simp
-  apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
-  done
-
-
-subsection \<open>Miscellaneous lemmas\<close>
+definition
+  "set_bits f =
+    (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
+      let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
+      in bl_to_bin (rev (map f [0..<n]))
+     else if \<exists>n. \<forall>n'\<ge>n. f n' then
+      let n = LEAST n. \<forall>n'\<ge>n. f n'
+      in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
+     else 0 :: int)"
 
-lemma nth_2p_bin: "bin_nth (2 ^ n) m = (m = n)"
-  apply (induct n arbitrary: m)
-   apply clarsimp
-   apply safe
-   apply (case_tac m)
-    apply (auto simp: Bit_B0_2t [symmetric])
-  done
+definition "shiftl x n = x * 2 ^ n" for x :: int
 
-\<comment> \<open>for use when simplifying with \<open>bin_nth_Bit\<close>\<close>
-lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)"
-  by auto
-
-lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT True"
-  by (induct n) (simp_all add: Bit_B1)
+definition "shiftr x n = x div 2 ^ n" for x :: int
 
-lemma mod_BIT: "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
-proof -
-  have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
-    by (simp add: mod_mult_mult1)
-  also have "\<dots> = ((2 * bin mod 2 ^ Suc n) + 1) mod 2 ^ Suc n"
-    by (simp add: ac_simps p1mod22k')
-  also have "\<dots> = (2 * bin + 1) mod 2 ^ Suc n"
-    by (simp only: mod_simps)
-  finally show ?thesis
-    by (auto simp add: Bit_def)
-qed
+definition "msb x \<longleftrightarrow> x < 0" for x :: int
 
-lemma AND_mod: "x AND 2 ^ n - 1 = x mod 2 ^ n"
-  for x :: int
-proof (induct x arbitrary: n rule: bin_induct)
-  case 1
-  then show ?case
-    by simp
-next
-  case 2
-  then show ?case
-    by (simp, simp add: m1mod2k)
-next
-  case (3 bin bit)
-  show ?case
-  proof (cases n)
-    case 0
-    then show ?thesis by simp
-  next
-    case (Suc m)
-    with 3 show ?thesis
-      by (simp only: power_BIT mod_BIT int_and_Bits) simp
-  qed
-qed
+instance ..
 
 end
 
+end
diff -r e79bbf86a984 -r 8bb835f10a39 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Tue Apr 16 20:00:14 2019 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy	Tue Apr 16 19:50:03 2019 +0000
@@ -6,10 +6,10 @@
 and concatenation.
 *)
 
-section "Bool lists and integers"
+section \<open>Bool lists and integers\<close>
 
 theory Bool_List_Representation
-  imports Bits_Int
+  imports Bit_Representation
 begin
 
 definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
@@ -400,55 +400,6 @@
   by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)
 
 
-subsection \<open>Links between bit-wise operations and operations on bool lists\<close>
-
-lemma bl_xor_aux_bin:
-  "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
-    bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
-  apply (induct n arbitrary: v w bs cs)
-   apply simp
-  apply (case_tac v rule: bin_exhaust)
-  apply (case_tac w rule: bin_exhaust)
-  apply clarsimp
-  apply (case_tac b)
-   apply auto
-  done
-
-lemma bl_or_aux_bin:
-  "map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
-    bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)"
-  apply (induct n arbitrary: v w bs cs)
-   apply simp
-  apply (case_tac v rule: bin_exhaust)
-  apply (case_tac w rule: bin_exhaust)
-  apply clarsimp
-  done
-
-lemma bl_and_aux_bin:
-  "map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
-    bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)"
-  apply (induct n arbitrary: v w bs cs)
-   apply simp
-  apply (case_tac v rule: bin_exhaust)
-  apply (case_tac w rule: bin_exhaust)
-  apply clarsimp
-  done
-
-lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)"
-  by (induct n arbitrary: w cs) auto
-
-lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
-  by (simp add: bin_to_bl_def bl_not_aux_bin)
-
-lemma bl_and_bin: "map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
-  by (simp add: bin_to_bl_def bl_and_aux_bin)
-
-lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
-  by (simp add: bin_to_bl_def bl_or_aux_bin)
-
-lemma bl_xor_bin: "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
-  by (simp only: bin_to_bl_def bl_xor_aux_bin map2_Nil)
-
 lemma drop_bin2bl_aux:
   "drop m (bin_to_bl_aux n bin bs) =
     bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
@@ -1042,36 +993,4 @@
   apply (rule refl)
   done
 
-
-text \<open>Even more bit operations\<close>
-
-instantiation int :: bitss
-begin
-
-definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
-
-definition "lsb i = i !! 0" for i :: int
-
-definition "set_bit i n b = bin_sc n b i"
-
-definition
-  "set_bits f =
-    (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
-      let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
-      in bl_to_bin (rev (map f [0..<n]))
-     else if \<exists>n. \<forall>n'\<ge>n. f n' then
-      let n = LEAST n. \<forall>n'\<ge>n. f n'
-      in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
-     else 0 :: int)"
-
-definition "shiftl x n = x * 2 ^ n" for x :: int
-
-definition "shiftr x n = x div 2 ^ n" for x :: int
-
-definition "msb x \<longleftrightarrow> x < 0" for x :: int
-
-instance ..
-
 end
-
-end
diff -r e79bbf86a984 -r 8bb835f10a39 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Apr 16 20:00:14 2019 +0200
+++ b/src/HOL/Word/Word.thy	Tue Apr 16 19:50:03 2019 +0000
@@ -9,7 +9,7 @@
   "HOL-Library.Type_Length"
   "HOL-Library.Boolean_Algebra"
   Bits_Bit
-  Bool_List_Representation
+  Bits_Int
   Misc_Typedef
   Word_Miscellaneous
 begin
diff -r e79bbf86a984 -r 8bb835f10a39 src/HOL/Word/Word_Miscellaneous.thy
--- a/src/HOL/Word/Word_Miscellaneous.thy	Tue Apr 16 20:00:14 2019 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Tue Apr 16 19:50:03 2019 +0000
@@ -6,6 +6,9 @@
   imports "HOL-Library.Bit" Misc_Numeric
 begin
 
+lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)"
+  by auto
+
 lemma power_minus_simp: "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)"
   by (auto dest: gr0_implies_Suc)