moved instance to appropriate place
authorhaftmann
Tue Apr 16 19:50:03 2019 +0000 (7 days ago)
changeset 701698bb835f10a39
parent 70168 e79bbf86a984
child 70170 56727602d0a5
moved instance to appropriate place
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Bits_Int.thy
src/HOL/Word/Bool_List_Representation.thy
src/HOL/Word/Word.thy
src/HOL/Word/Word_Miscellaneous.thy
     1.1 --- a/src/HOL/Word/Bit_Representation.thy	Tue Apr 16 20:00:14 2019 +0200
     1.2 +++ b/src/HOL/Word/Bit_Representation.thy	Tue Apr 16 19:50:03 2019 +0000
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Jeremy Dawson, NICTA
     1.5  *)
     1.6  
     1.7 -section \<open>Integers as implict bit strings\<close>
     1.8 +section \<open>Integers as implicit bit strings\<close>
     1.9  
    1.10  theory Bit_Representation
    1.11    imports Misc_Numeric
    1.12 @@ -25,6 +25,9 @@
    1.13  lemma Bit_B1_2t: "k BIT True = 2 * k + 1"
    1.14    by (rule trans, rule Bit_B1) simp
    1.15  
    1.16 +lemma power_BIT: "2 ^ Suc n - 1 = (2 ^ n - 1) BIT True"
    1.17 +  by (simp add: Bit_B1)
    1.18 +
    1.19  definition bin_last :: "int \<Rightarrow> bool"
    1.20    where "bin_last w \<longleftrightarrow> w mod 2 = 1"
    1.21  
    1.22 @@ -242,6 +245,14 @@
    1.23    bin_nth.Z bin_nth.Suc bin_nth_zero bin_nth_minus1
    1.24    bin_nth_numeral_simps
    1.25  
    1.26 +lemma nth_2p_bin: "bin_nth (2 ^ n) m = (m = n)" \<comment> \<open>for use when simplifying with \<open>bin_nth_Bit\<close>\<close>
    1.27 +  apply (induct n arbitrary: m)
    1.28 +   apply clarsimp
    1.29 +   apply safe
    1.30 +   apply (case_tac m)
    1.31 +    apply (auto simp: Bit_B0_2t [symmetric])
    1.32 +  done 
    1.33 +
    1.34  
    1.35  subsection \<open>Truncating binary integers\<close>
    1.36  
    1.37 @@ -682,4 +693,129 @@
    1.38      Z: "bin_cat w 0 v = w"
    1.39    | Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
    1.40  
    1.41 +lemma bin_sign_cat: "bin_sign (bin_cat x n y) = bin_sign x"
    1.42 +  by (induct n arbitrary: y) auto
    1.43 +
    1.44 +lemma bin_cat_Suc_Bit: "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
    1.45 +  by auto
    1.46 +
    1.47 +lemma bin_cat_assoc: "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
    1.48 +  by (induct n arbitrary: z) auto
    1.49 +
    1.50 +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"
    1.51 +  apply (induct n arbitrary: z m)
    1.52 +   apply clarsimp
    1.53 +  apply (case_tac m, auto)
    1.54 +  done
    1.55 +
    1.56 +definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
    1.57 +  where "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
    1.58 +
    1.59 +fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
    1.60 +  where "bin_rsplit_aux n m c bs =
    1.61 +    (if m = 0 \<or> n = 0 then bs
    1.62 +     else
    1.63 +      let (a, b) = bin_split n c
    1.64 +      in bin_rsplit_aux n (m - n) a (b # bs))"
    1.65 +
    1.66 +definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
    1.67 +  where "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
    1.68 +
    1.69 +fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
    1.70 +  where "bin_rsplitl_aux n m c bs =
    1.71 +    (if m = 0 \<or> n = 0 then bs
    1.72 +     else
    1.73 +      let (a, b) = bin_split (min m n) c
    1.74 +      in bin_rsplitl_aux n (m - n) a (b # bs))"
    1.75 +
    1.76 +definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
    1.77 +  where "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
    1.78 +
    1.79 +declare bin_rsplit_aux.simps [simp del]
    1.80 +declare bin_rsplitl_aux.simps [simp del]
    1.81 +
    1.82 +lemma bin_nth_cat:
    1.83 +  "bin_nth (bin_cat x k y) n =
    1.84 +    (if n < k then bin_nth y n else bin_nth x (n - k))"
    1.85 +  apply (induct k arbitrary: n y)
    1.86 +   apply clarsimp
    1.87 +  apply (case_tac n, auto)
    1.88 +  done
    1.89 +
    1.90 +lemma bin_nth_split:
    1.91 +  "bin_split n c = (a, b) \<Longrightarrow>
    1.92 +    (\<forall>k. bin_nth a k = bin_nth c (n + k)) \<and>
    1.93 +    (\<forall>k. bin_nth b k = (k < n \<and> bin_nth c k))"
    1.94 +  apply (induct n arbitrary: b c)
    1.95 +   apply clarsimp
    1.96 +  apply (clarsimp simp: Let_def split: prod.split_asm)
    1.97 +  apply (case_tac k)
    1.98 +  apply auto
    1.99 +  done
   1.100 +
   1.101 +lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
   1.102 +  by (induct n arbitrary: w) auto
   1.103 +
   1.104 +lemma bintr_cat1: "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
   1.105 +  by (induct n arbitrary: b) auto
   1.106 +
   1.107 +lemma bintr_cat: "bintrunc m (bin_cat a n b) =
   1.108 +    bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
   1.109 +  by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
   1.110 +
   1.111 +lemma bintr_cat_same [simp]: "bintrunc n (bin_cat a n b) = bintrunc n b"
   1.112 +  by (auto simp add : bintr_cat)
   1.113 +
   1.114 +lemma cat_bintr [simp]: "bin_cat a n (bintrunc n b) = bin_cat a n b"
   1.115 +  by (induct n arbitrary: b) auto
   1.116 +
   1.117 +lemma split_bintrunc: "bin_split n c = (a, b) \<Longrightarrow> b = bintrunc n c"
   1.118 +  by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm)
   1.119 +
   1.120 +lemma bin_cat_split: "bin_split n w = (u, v) \<Longrightarrow> w = bin_cat u n v"
   1.121 +  by (induct n arbitrary: v w) (auto simp: Let_def split: prod.split_asm)
   1.122 +
   1.123 +lemma bin_split_cat: "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
   1.124 +  by (induct n arbitrary: w) auto
   1.125 +
   1.126 +lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
   1.127 +  by (induct n) auto
   1.128 +
   1.129 +lemma bin_split_minus1 [simp]:
   1.130 +  "bin_split n (- 1) = (- 1, bintrunc n (- 1))"
   1.131 +  by (induct n) auto
   1.132 +
   1.133 +lemma bin_split_trunc:
   1.134 +  "bin_split (min m n) c = (a, b) \<Longrightarrow>
   1.135 +    bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
   1.136 +  apply (induct n arbitrary: m b c, clarsimp)
   1.137 +  apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
   1.138 +  apply (case_tac m)
   1.139 +   apply (auto simp: Let_def split: prod.split_asm)
   1.140 +  done
   1.141 +
   1.142 +lemma bin_split_trunc1:
   1.143 +  "bin_split n c = (a, b) \<Longrightarrow>
   1.144 +    bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
   1.145 +  apply (induct n arbitrary: m b c, clarsimp)
   1.146 +  apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
   1.147 +  apply (case_tac m)
   1.148 +   apply (auto simp: Let_def split: prod.split_asm)
   1.149 +  done
   1.150 +
   1.151 +lemma bin_cat_num: "bin_cat a n b = a * 2 ^ n + bintrunc n b"
   1.152 +  apply (induct n arbitrary: b)
   1.153 +   apply clarsimp
   1.154 +  apply (simp add: Bit_def)
   1.155 +  done
   1.156 +
   1.157 +lemma bin_split_num: "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
   1.158 +  apply (induct n arbitrary: b)
   1.159 +   apply simp
   1.160 +  apply (simp add: bin_rest_def zdiv_zmult2_eq)
   1.161 +  apply (case_tac b rule: bin_exhaust)
   1.162 +  apply simp
   1.163 +  apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
   1.164 +  done
   1.165 +
   1.166  end
     2.1 --- a/src/HOL/Word/Bits_Int.thy	Tue Apr 16 20:00:14 2019 +0200
     2.2 +++ b/src/HOL/Word/Bits_Int.thy	Tue Apr 16 19:50:03 2019 +0000
     2.3 @@ -9,7 +9,7 @@
     2.4  section \<open>Bitwise Operations on Binary Integers\<close>
     2.5  
     2.6  theory Bits_Int
     2.7 -  imports Bits Bit_Representation
     2.8 +  imports Bits Bit_Representation Bool_List_Representation
     2.9  begin
    2.10  
    2.11  subsection \<open>Logical operations\<close>
    2.12 @@ -365,6 +365,41 @@
    2.13    apply (case_tac bit, auto)
    2.14    done
    2.15  
    2.16 +lemma mod_BIT: "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
    2.17 +proof -
    2.18 +  have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
    2.19 +    by (simp add: mod_mult_mult1)
    2.20 +  also have "\<dots> = ((2 * bin mod 2 ^ Suc n) + 1) mod 2 ^ Suc n"
    2.21 +    by (simp add: ac_simps p1mod22k')
    2.22 +  also have "\<dots> = (2 * bin + 1) mod 2 ^ Suc n"
    2.23 +    by (simp only: mod_simps)
    2.24 +  finally show ?thesis
    2.25 +    by (auto simp add: Bit_def)
    2.26 +qed
    2.27 +
    2.28 +lemma AND_mod: "x AND 2 ^ n - 1 = x mod 2 ^ n"
    2.29 +  for x :: int
    2.30 +proof (induct x arbitrary: n rule: bin_induct)
    2.31 +  case 1
    2.32 +  then show ?case
    2.33 +    by simp
    2.34 +next
    2.35 +  case 2
    2.36 +  then show ?case
    2.37 +    by (simp, simp add: m1mod2k)
    2.38 +next
    2.39 +  case (3 bin bit)
    2.40 +  show ?case
    2.41 +  proof (cases n)
    2.42 +    case 0
    2.43 +    then show ?thesis by simp
    2.44 +  next
    2.45 +    case (Suc m)
    2.46 +    with 3 show ?thesis
    2.47 +      by (simp only: power_BIT mod_BIT int_and_Bits) simp
    2.48 +  qed
    2.49 +qed
    2.50 +
    2.51  
    2.52  subsubsection \<open>Truncating results of bit-wise operations\<close>
    2.53  
    2.54 @@ -386,6 +421,53 @@
    2.55  lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
    2.56  lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
    2.57  
    2.58 +lemma bl_xor_aux_bin:
    2.59 +  "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
    2.60 +    bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
    2.61 +  apply (induct n arbitrary: v w bs cs)
    2.62 +   apply simp
    2.63 +  apply (case_tac v rule: bin_exhaust)
    2.64 +  apply (case_tac w rule: bin_exhaust)
    2.65 +  apply clarsimp
    2.66 +  apply (case_tac b)
    2.67 +   apply auto
    2.68 +  done
    2.69 +
    2.70 +lemma bl_or_aux_bin:
    2.71 +  "map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
    2.72 +    bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)"
    2.73 +  apply (induct n arbitrary: v w bs cs)
    2.74 +   apply simp
    2.75 +  apply (case_tac v rule: bin_exhaust)
    2.76 +  apply (case_tac w rule: bin_exhaust)
    2.77 +  apply clarsimp
    2.78 +  done
    2.79 +
    2.80 +lemma bl_and_aux_bin:
    2.81 +  "map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
    2.82 +    bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)"
    2.83 +  apply (induct n arbitrary: v w bs cs)
    2.84 +   apply simp
    2.85 +  apply (case_tac v rule: bin_exhaust)
    2.86 +  apply (case_tac w rule: bin_exhaust)
    2.87 +  apply clarsimp
    2.88 +  done
    2.89 +
    2.90 +lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)"
    2.91 +  by (induct n arbitrary: w cs) auto
    2.92 +
    2.93 +lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
    2.94 +  by (simp add: bin_to_bl_def bl_not_aux_bin)
    2.95 +
    2.96 +lemma bl_and_bin: "map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
    2.97 +  by (simp add: bin_to_bl_def bl_and_aux_bin)
    2.98 +
    2.99 +lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
   2.100 +  by (simp add: bin_to_bl_def bl_or_aux_bin)
   2.101 +
   2.102 +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)"
   2.103 +  by (simp only: bin_to_bl_def bl_xor_aux_bin map2_Nil)
   2.104 +
   2.105  
   2.106  subsection \<open>Setting and clearing bits\<close>
   2.107  
   2.108 @@ -470,186 +552,33 @@
   2.109      bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
   2.110    by (simp add: numeral_eq_Suc)
   2.111  
   2.112 -
   2.113 -subsection \<open>Splitting and concatenation\<close>
   2.114 -
   2.115 -definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
   2.116 -  where "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
   2.117 -
   2.118 -fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
   2.119 -  where "bin_rsplit_aux n m c bs =
   2.120 -    (if m = 0 \<or> n = 0 then bs
   2.121 -     else
   2.122 -      let (a, b) = bin_split n c
   2.123 -      in bin_rsplit_aux n (m - n) a (b # bs))"
   2.124 -
   2.125 -definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
   2.126 -  where "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
   2.127 -
   2.128 -fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
   2.129 -  where "bin_rsplitl_aux n m c bs =
   2.130 -    (if m = 0 \<or> n = 0 then bs
   2.131 -     else
   2.132 -      let (a, b) = bin_split (min m n) c
   2.133 -      in bin_rsplitl_aux n (m - n) a (b # bs))"
   2.134 -
   2.135 -definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
   2.136 -  where "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
   2.137 -
   2.138 -declare bin_rsplit_aux.simps [simp del]
   2.139 -declare bin_rsplitl_aux.simps [simp del]
   2.140 -
   2.141 -lemma bin_sign_cat: "bin_sign (bin_cat x n y) = bin_sign x"
   2.142 -  by (induct n arbitrary: y) auto
   2.143 -
   2.144 -lemma bin_cat_Suc_Bit: "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
   2.145 -  by auto
   2.146 -
   2.147 -lemma bin_nth_cat:
   2.148 -  "bin_nth (bin_cat x k y) n =
   2.149 -    (if n < k then bin_nth y n else bin_nth x (n - k))"
   2.150 -  apply (induct k arbitrary: n y)
   2.151 -   apply clarsimp
   2.152 -  apply (case_tac n, auto)
   2.153 -  done
   2.154 +instantiation int :: bitss
   2.155 +begin
   2.156  
   2.157 -lemma bin_nth_split:
   2.158 -  "bin_split n c = (a, b) \<Longrightarrow>
   2.159 -    (\<forall>k. bin_nth a k = bin_nth c (n + k)) \<and>
   2.160 -    (\<forall>k. bin_nth b k = (k < n \<and> bin_nth c k))"
   2.161 -  apply (induct n arbitrary: b c)
   2.162 -   apply clarsimp
   2.163 -  apply (clarsimp simp: Let_def split: prod.split_asm)
   2.164 -  apply (case_tac k)
   2.165 -  apply auto
   2.166 -  done
   2.167 -
   2.168 -lemma bin_cat_assoc: "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
   2.169 -  by (induct n arbitrary: z) auto
   2.170 -
   2.171 -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"
   2.172 -  apply (induct n arbitrary: z m)
   2.173 -   apply clarsimp
   2.174 -  apply (case_tac m, auto)
   2.175 -  done
   2.176 +definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
   2.177  
   2.178 -lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
   2.179 -  by (induct n arbitrary: w) auto
   2.180 -
   2.181 -lemma bintr_cat1: "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
   2.182 -  by (induct n arbitrary: b) auto
   2.183 -
   2.184 -lemma bintr_cat: "bintrunc m (bin_cat a n b) =
   2.185 -    bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
   2.186 -  by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
   2.187 +definition "lsb i = i !! 0" for i :: int
   2.188  
   2.189 -lemma bintr_cat_same [simp]: "bintrunc n (bin_cat a n b) = bintrunc n b"
   2.190 -  by (auto simp add : bintr_cat)
   2.191 -
   2.192 -lemma cat_bintr [simp]: "bin_cat a n (bintrunc n b) = bin_cat a n b"
   2.193 -  by (induct n arbitrary: b) auto
   2.194 -
   2.195 -lemma split_bintrunc: "bin_split n c = (a, b) \<Longrightarrow> b = bintrunc n c"
   2.196 -  by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm)
   2.197 -
   2.198 -lemma bin_cat_split: "bin_split n w = (u, v) \<Longrightarrow> w = bin_cat u n v"
   2.199 -  by (induct n arbitrary: v w) (auto simp: Let_def split: prod.split_asm)
   2.200 -
   2.201 -lemma bin_split_cat: "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
   2.202 -  by (induct n arbitrary: w) auto
   2.203 +definition "set_bit i n b = bin_sc n b i"
   2.204  
   2.205 -lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
   2.206 -  by (induct n) auto
   2.207 -
   2.208 -lemma bin_split_minus1 [simp]:
   2.209 -  "bin_split n (- 1) = (- 1, bintrunc n (- 1))"
   2.210 -  by (induct n) auto
   2.211 -
   2.212 -lemma bin_split_trunc:
   2.213 -  "bin_split (min m n) c = (a, b) \<Longrightarrow>
   2.214 -    bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
   2.215 -  apply (induct n arbitrary: m b c, clarsimp)
   2.216 -  apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
   2.217 -  apply (case_tac m)
   2.218 -   apply (auto simp: Let_def split: prod.split_asm)
   2.219 -  done
   2.220 -
   2.221 -lemma bin_split_trunc1:
   2.222 -  "bin_split n c = (a, b) \<Longrightarrow>
   2.223 -    bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
   2.224 -  apply (induct n arbitrary: m b c, clarsimp)
   2.225 -  apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
   2.226 -  apply (case_tac m)
   2.227 -   apply (auto simp: Let_def split: prod.split_asm)
   2.228 -  done
   2.229 -
   2.230 -lemma bin_cat_num: "bin_cat a n b = a * 2 ^ n + bintrunc n b"
   2.231 -  apply (induct n arbitrary: b)
   2.232 -   apply clarsimp
   2.233 -  apply (simp add: Bit_def)
   2.234 -  done
   2.235 -
   2.236 -lemma bin_split_num: "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
   2.237 -  apply (induct n arbitrary: b)
   2.238 -   apply simp
   2.239 -  apply (simp add: bin_rest_def zdiv_zmult2_eq)
   2.240 -  apply (case_tac b rule: bin_exhaust)
   2.241 -  apply simp
   2.242 -  apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
   2.243 -  done
   2.244 -
   2.245 -
   2.246 -subsection \<open>Miscellaneous lemmas\<close>
   2.247 +definition
   2.248 +  "set_bits f =
   2.249 +    (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
   2.250 +      let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
   2.251 +      in bl_to_bin (rev (map f [0..<n]))
   2.252 +     else if \<exists>n. \<forall>n'\<ge>n. f n' then
   2.253 +      let n = LEAST n. \<forall>n'\<ge>n. f n'
   2.254 +      in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
   2.255 +     else 0 :: int)"
   2.256  
   2.257 -lemma nth_2p_bin: "bin_nth (2 ^ n) m = (m = n)"
   2.258 -  apply (induct n arbitrary: m)
   2.259 -   apply clarsimp
   2.260 -   apply safe
   2.261 -   apply (case_tac m)
   2.262 -    apply (auto simp: Bit_B0_2t [symmetric])
   2.263 -  done
   2.264 +definition "shiftl x n = x * 2 ^ n" for x :: int
   2.265  
   2.266 -\<comment> \<open>for use when simplifying with \<open>bin_nth_Bit\<close>\<close>
   2.267 -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)"
   2.268 -  by auto
   2.269 -
   2.270 -lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT True"
   2.271 -  by (induct n) (simp_all add: Bit_B1)
   2.272 +definition "shiftr x n = x div 2 ^ n" for x :: int
   2.273  
   2.274 -lemma mod_BIT: "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
   2.275 -proof -
   2.276 -  have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
   2.277 -    by (simp add: mod_mult_mult1)
   2.278 -  also have "\<dots> = ((2 * bin mod 2 ^ Suc n) + 1) mod 2 ^ Suc n"
   2.279 -    by (simp add: ac_simps p1mod22k')
   2.280 -  also have "\<dots> = (2 * bin + 1) mod 2 ^ Suc n"
   2.281 -    by (simp only: mod_simps)
   2.282 -  finally show ?thesis
   2.283 -    by (auto simp add: Bit_def)
   2.284 -qed
   2.285 +definition "msb x \<longleftrightarrow> x < 0" for x :: int
   2.286  
   2.287 -lemma AND_mod: "x AND 2 ^ n - 1 = x mod 2 ^ n"
   2.288 -  for x :: int
   2.289 -proof (induct x arbitrary: n rule: bin_induct)
   2.290 -  case 1
   2.291 -  then show ?case
   2.292 -    by simp
   2.293 -next
   2.294 -  case 2
   2.295 -  then show ?case
   2.296 -    by (simp, simp add: m1mod2k)
   2.297 -next
   2.298 -  case (3 bin bit)
   2.299 -  show ?case
   2.300 -  proof (cases n)
   2.301 -    case 0
   2.302 -    then show ?thesis by simp
   2.303 -  next
   2.304 -    case (Suc m)
   2.305 -    with 3 show ?thesis
   2.306 -      by (simp only: power_BIT mod_BIT int_and_Bits) simp
   2.307 -  qed
   2.308 -qed
   2.309 +instance ..
   2.310  
   2.311  end
   2.312  
   2.313 +end
     3.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Tue Apr 16 20:00:14 2019 +0200
     3.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Tue Apr 16 19:50:03 2019 +0000
     3.3 @@ -6,10 +6,10 @@
     3.4  and concatenation.
     3.5  *)
     3.6  
     3.7 -section "Bool lists and integers"
     3.8 +section \<open>Bool lists and integers\<close>
     3.9  
    3.10  theory Bool_List_Representation
    3.11 -  imports Bits_Int
    3.12 +  imports Bit_Representation
    3.13  begin
    3.14  
    3.15  definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
    3.16 @@ -400,55 +400,6 @@
    3.17    by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)
    3.18  
    3.19  
    3.20 -subsection \<open>Links between bit-wise operations and operations on bool lists\<close>
    3.21 -
    3.22 -lemma bl_xor_aux_bin:
    3.23 -  "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
    3.24 -    bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
    3.25 -  apply (induct n arbitrary: v w bs cs)
    3.26 -   apply simp
    3.27 -  apply (case_tac v rule: bin_exhaust)
    3.28 -  apply (case_tac w rule: bin_exhaust)
    3.29 -  apply clarsimp
    3.30 -  apply (case_tac b)
    3.31 -   apply auto
    3.32 -  done
    3.33 -
    3.34 -lemma bl_or_aux_bin:
    3.35 -  "map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
    3.36 -    bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)"
    3.37 -  apply (induct n arbitrary: v w bs cs)
    3.38 -   apply simp
    3.39 -  apply (case_tac v rule: bin_exhaust)
    3.40 -  apply (case_tac w rule: bin_exhaust)
    3.41 -  apply clarsimp
    3.42 -  done
    3.43 -
    3.44 -lemma bl_and_aux_bin:
    3.45 -  "map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
    3.46 -    bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)"
    3.47 -  apply (induct n arbitrary: v w bs cs)
    3.48 -   apply simp
    3.49 -  apply (case_tac v rule: bin_exhaust)
    3.50 -  apply (case_tac w rule: bin_exhaust)
    3.51 -  apply clarsimp
    3.52 -  done
    3.53 -
    3.54 -lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)"
    3.55 -  by (induct n arbitrary: w cs) auto
    3.56 -
    3.57 -lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
    3.58 -  by (simp add: bin_to_bl_def bl_not_aux_bin)
    3.59 -
    3.60 -lemma bl_and_bin: "map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
    3.61 -  by (simp add: bin_to_bl_def bl_and_aux_bin)
    3.62 -
    3.63 -lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
    3.64 -  by (simp add: bin_to_bl_def bl_or_aux_bin)
    3.65 -
    3.66 -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)"
    3.67 -  by (simp only: bin_to_bl_def bl_xor_aux_bin map2_Nil)
    3.68 -
    3.69  lemma drop_bin2bl_aux:
    3.70    "drop m (bin_to_bl_aux n bin bs) =
    3.71      bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
    3.72 @@ -1042,36 +993,4 @@
    3.73    apply (rule refl)
    3.74    done
    3.75  
    3.76 -
    3.77 -text \<open>Even more bit operations\<close>
    3.78 -
    3.79 -instantiation int :: bitss
    3.80 -begin
    3.81 -
    3.82 -definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
    3.83 -
    3.84 -definition "lsb i = i !! 0" for i :: int
    3.85 -
    3.86 -definition "set_bit i n b = bin_sc n b i"
    3.87 -
    3.88 -definition
    3.89 -  "set_bits f =
    3.90 -    (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
    3.91 -      let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
    3.92 -      in bl_to_bin (rev (map f [0..<n]))
    3.93 -     else if \<exists>n. \<forall>n'\<ge>n. f n' then
    3.94 -      let n = LEAST n. \<forall>n'\<ge>n. f n'
    3.95 -      in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
    3.96 -     else 0 :: int)"
    3.97 -
    3.98 -definition "shiftl x n = x * 2 ^ n" for x :: int
    3.99 -
   3.100 -definition "shiftr x n = x div 2 ^ n" for x :: int
   3.101 -
   3.102 -definition "msb x \<longleftrightarrow> x < 0" for x :: int
   3.103 -
   3.104 -instance ..
   3.105 -
   3.106  end
   3.107 -
   3.108 -end
     4.1 --- a/src/HOL/Word/Word.thy	Tue Apr 16 20:00:14 2019 +0200
     4.2 +++ b/src/HOL/Word/Word.thy	Tue Apr 16 19:50:03 2019 +0000
     4.3 @@ -9,7 +9,7 @@
     4.4    "HOL-Library.Type_Length"
     4.5    "HOL-Library.Boolean_Algebra"
     4.6    Bits_Bit
     4.7 -  Bool_List_Representation
     4.8 +  Bits_Int
     4.9    Misc_Typedef
    4.10    Word_Miscellaneous
    4.11  begin
     5.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Tue Apr 16 20:00:14 2019 +0200
     5.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Tue Apr 16 19:50:03 2019 +0000
     5.3 @@ -6,6 +6,9 @@
     5.4    imports "HOL-Library.Bit" Misc_Numeric
     5.5  begin
     5.6  
     5.7 +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)"
     5.8 +  by auto
     5.9 +
    5.10  lemma power_minus_simp: "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)"
    5.11    by (auto dest: gr0_implies_Suc)
    5.12