clearer separation of pre-word bit list material
authorhaftmann
Tue Aug 04 09:24:00 2020 +0000 (6 weeks ago)
changeset 72081e4d42f5766dc
parent 72080 2030eacf3a72
child 72082 41393ecb57ac
clearer separation of pre-word bit list material
src/HOL/Word/Bit_Comprehension.thy
src/HOL/Word/Bit_Lists.thy
src/HOL/Word/Bits_Int.thy
     1.1 --- a/src/HOL/Word/Bit_Comprehension.thy	Mon Aug 03 16:21:33 2020 +0200
     1.2 +++ b/src/HOL/Word/Bit_Comprehension.thy	Tue Aug 04 09:24:00 2020 +0000
     1.3 @@ -32,6 +32,6 @@
     1.4    by (simp add: set_bits_int_def)
     1.5  
     1.6  lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)"
     1.7 -  by (auto simp add: set_bits_int_def bl_to_bin_def)
     1.8 +  by (auto simp add: set_bits_int_def)
     1.9  
    1.10 -end
    1.11 \ No newline at end of file
    1.12 +end
     2.1 --- a/src/HOL/Word/Bit_Lists.thy	Mon Aug 03 16:21:33 2020 +0200
     2.2 +++ b/src/HOL/Word/Bit_Lists.thy	Tue Aug 04 09:24:00 2020 +0000
     2.3 @@ -125,15 +125,6 @@
     2.4  lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) ((!) (rev xs)) = xs"
     2.5    by (simp add: bl_of_nth_nth_le)
     2.6  
     2.7 -lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
     2.8 -  apply (rule nth_equalityI)
     2.9 -   apply simp
    2.10 -  apply (clarsimp simp: nth_takefill rev_nth nth_bin_to_bl bin_nth_of_bl)
    2.11 -  done
    2.12 -
    2.13 -lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
    2.14 -  by (simp add: takefill_bintrunc)
    2.15 -
    2.16  
    2.17  subsection \<open>More\<close>
    2.18  
    2.19 @@ -296,4 +287,671 @@
    2.20      rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
    2.21    by (induct n) (auto intro!: lth)
    2.22  
    2.23 +
    2.24 +subsection \<open>Explicit bit representation of \<^typ>\<open>int\<close>\<close>
    2.25 +
    2.26 +primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
    2.27 +  where
    2.28 +    Nil: "bl_to_bin_aux [] w = w"
    2.29 +  | Cons: "bl_to_bin_aux (b # bs) w = bl_to_bin_aux bs (of_bool b + 2 * w)"
    2.30 +
    2.31 +definition bl_to_bin :: "bool list \<Rightarrow> int"
    2.32 +  where "bl_to_bin bs = bl_to_bin_aux bs 0"
    2.33 +
    2.34 +primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
    2.35 +  where
    2.36 +    Z: "bin_to_bl_aux 0 w bl = bl"
    2.37 +  | Suc: "bin_to_bl_aux (Suc n) w bl = bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
    2.38 +
    2.39 +definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
    2.40 +  where "bin_to_bl n w = bin_to_bl_aux n w []"
    2.41 +
    2.42 +lemma bin_to_bl_aux_zero_minus_simp [simp]:
    2.43 +  "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)"
    2.44 +  by (cases n) auto
    2.45 +
    2.46 +lemma bin_to_bl_aux_minus1_minus_simp [simp]:
    2.47 +  "0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)"
    2.48 +  by (cases n) auto
    2.49 +
    2.50 +lemma bin_to_bl_aux_one_minus_simp [simp]:
    2.51 +  "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)"
    2.52 +  by (cases n) auto
    2.53 +
    2.54 +lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
    2.55 +  "0 < n \<Longrightarrow>
    2.56 +    bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)"
    2.57 +  by (cases n) simp_all
    2.58 +
    2.59 +lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
    2.60 +  "0 < n \<Longrightarrow>
    2.61 +    bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
    2.62 +  by (cases n) simp_all
    2.63 +
    2.64 +lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
    2.65 +  by (induct bs arbitrary: w) auto
    2.66 +
    2.67 +lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
    2.68 +  by (induct n arbitrary: w bs) auto
    2.69 +
    2.70 +lemma bl_to_bin_append: "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
    2.71 +  unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
    2.72 +
    2.73 +lemma bin_to_bl_aux_alt: "bin_to_bl_aux n w bs = bin_to_bl n w @ bs"
    2.74 +  by (simp add: bin_to_bl_def bin_to_bl_aux_append)
    2.75 +
    2.76 +lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
    2.77 +  by (auto simp: bin_to_bl_def)
    2.78 +
    2.79 +lemma size_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
    2.80 +  by (induct n arbitrary: w bs) auto
    2.81 +
    2.82 +lemma size_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
    2.83 +  by (simp add: bin_to_bl_def size_bin_to_bl_aux)
    2.84 +
    2.85 +lemma bl_bin_bl': "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs"
    2.86 +  apply (induct bs arbitrary: w n)
    2.87 +   apply auto
    2.88 +    apply (simp_all only: add_Suc [symmetric])
    2.89 +    apply (auto simp add: bin_to_bl_def)
    2.90 +  done
    2.91 +
    2.92 +lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
    2.93 +  unfolding bl_to_bin_def
    2.94 +  apply (rule box_equals)
    2.95 +    apply (rule bl_bin_bl')
    2.96 +   prefer 2
    2.97 +   apply (rule bin_to_bl_aux.Z)
    2.98 +  apply simp
    2.99 +  done
   2.100 +
   2.101 +lemma bl_to_bin_inj: "bl_to_bin bs = bl_to_bin cs \<Longrightarrow> length bs = length cs \<Longrightarrow> bs = cs"
   2.102 +  apply (rule_tac box_equals)
   2.103 +    defer
   2.104 +    apply (rule bl_bin_bl)
   2.105 +   apply (rule bl_bin_bl)
   2.106 +  apply simp
   2.107 +  done
   2.108 +
   2.109 +lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
   2.110 +  by (auto simp: bl_to_bin_def)
   2.111 +
   2.112 +lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
   2.113 +  by (auto simp: bl_to_bin_def)
   2.114 +
   2.115 +lemma bin_to_bl_zero_aux: "bin_to_bl_aux n 0 bl = replicate n False @ bl"
   2.116 +  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
   2.117 +
   2.118 +lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False"
   2.119 +  by (simp add: bin_to_bl_def bin_to_bl_zero_aux)
   2.120 +
   2.121 +lemma bin_to_bl_minus1_aux: "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
   2.122 +  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
   2.123 +
   2.124 +lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
   2.125 +  by (simp add: bin_to_bl_def bin_to_bl_minus1_aux)
   2.126 +
   2.127 +
   2.128 +subsection \<open>Semantic interpretation of \<^typ>\<open>bool list\<close> as \<^typ>\<open>int\<close>\<close>
   2.129 +
   2.130 +lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (bintrunc n w)"
   2.131 +  by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def take_bit_Suc ac_simps mod_2_eq_odd)
   2.132 +
   2.133 +lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
   2.134 +  by (auto simp: bin_to_bl_def bin_bl_bin')
   2.135 +
   2.136 +lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
   2.137 +  by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def)
   2.138 +
   2.139 +lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
   2.140 +  by (auto intro: bl_to_bin_inj)
   2.141 +
   2.142 +lemma bin_to_bl_aux_bintr:
   2.143 +  "bin_to_bl_aux n (bintrunc m bin) bl =
   2.144 +    replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
   2.145 +  apply (induct n arbitrary: m bin bl)
   2.146 +   apply clarsimp
   2.147 +  apply clarsimp
   2.148 +  apply (case_tac "m")
   2.149 +   apply (clarsimp simp: bin_to_bl_zero_aux)
   2.150 +   apply (erule thin_rl)
   2.151 +   apply (induct_tac n)
   2.152 +    apply (auto simp add: take_bit_Suc)
   2.153 +  done
   2.154 +
   2.155 +lemma bin_to_bl_bintr:
   2.156 +  "bin_to_bl n (bintrunc m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin"
   2.157 +  unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
   2.158 +
   2.159 +lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
   2.160 +  by (induct n) auto
   2.161 +
   2.162 +lemma len_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
   2.163 +  by (fact size_bin_to_bl_aux)
   2.164 +
   2.165 +lemma len_bin_to_bl: "length (bin_to_bl n w) = n"
   2.166 +  by (fact size_bin_to_bl) (* FIXME: duplicate *)
   2.167 +
   2.168 +lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
   2.169 +  by (induction bs arbitrary: w) (simp_all add: bin_sign_def)
   2.170 +
   2.171 +lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
   2.172 +  by (simp add: bl_to_bin_def sign_bl_bin')
   2.173 +
   2.174 +lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (sbintrunc n w) = -1)"
   2.175 +  by (induction n arbitrary: w bs) (auto simp add: bin_sign_def even_iff_mod_2_eq_zero bit_Suc)
   2.176 +
   2.177 +lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
   2.178 +  unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
   2.179 +
   2.180 +lemma bin_nth_of_bl_aux:
   2.181 +  "bin_nth (bl_to_bin_aux bl w) n =
   2.182 +    (n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bin_nth w (n - size bl))"
   2.183 +  apply (induction bl arbitrary: w)
   2.184 +   apply simp_all
   2.185 +  apply safe
   2.186 +                      apply (simp_all add: not_le nth_append bit_double_iff even_bit_succ_iff split: if_splits)
   2.187 +  done
   2.188 +
   2.189 +lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)"
   2.190 +  by (simp add: bl_to_bin_def bin_nth_of_bl_aux)
   2.191 +
   2.192 +lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
   2.193 +  apply (induct n arbitrary: m w)
   2.194 +   apply clarsimp
   2.195 +   apply (case_tac m, clarsimp)
   2.196 +   apply (clarsimp simp: bin_to_bl_def)
   2.197 +   apply (simp add: bin_to_bl_aux_alt)
   2.198 +  apply (case_tac m, clarsimp)
   2.199 +  apply (clarsimp simp: bin_to_bl_def)
   2.200 +  apply (simp add: bin_to_bl_aux_alt bit_Suc)
   2.201 +  done
   2.202 +
   2.203 +lemma nth_bin_to_bl_aux:
   2.204 +  "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
   2.205 +    (if n < m then bit w (m - 1 - n) else bl ! (n - m))"
   2.206 +  apply (induction bl arbitrary: w)
   2.207 +   apply simp_all
   2.208 +   apply (simp add: bin_nth_bl [of \<open>m - Suc n\<close> m] rev_nth flip: bin_to_bl_def)
   2.209 +   apply (metis One_nat_def Suc_pred add_diff_cancel_left'
   2.210 +     add_diff_cancel_right' bin_to_bl_aux_alt bin_to_bl_def
   2.211 +     diff_Suc_Suc diff_is_0_eq diff_zero less_Suc_eq_0_disj
   2.212 +     less_antisym less_imp_Suc_add list.size(3) nat_less_le nth_append size_bin_to_bl_aux)
   2.213 +  done
   2.214 +
   2.215 +lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
   2.216 +  by (simp add: bin_to_bl_def nth_bin_to_bl_aux)
   2.217 +
   2.218 +lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
   2.219 +  apply (rule nth_equalityI)
   2.220 +   apply simp
   2.221 +  apply (clarsimp simp: nth_takefill rev_nth nth_bin_to_bl bin_nth_of_bl)
   2.222 +  done
   2.223 +
   2.224 +lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
   2.225 +  by (simp add: takefill_bintrunc)
   2.226 +
   2.227 +lemma bl_to_bin_lt2p_aux: "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
   2.228 +proof (induction bs arbitrary: w)
   2.229 +  case Nil
   2.230 +  then show ?case
   2.231 +    by simp
   2.232 +next
   2.233 +  case (Cons b bs)
   2.234 +  from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
   2.235 +  show ?case
   2.236 +    apply (auto simp add: algebra_simps)
   2.237 +    apply (subst mult_2 [of \<open>2 ^ length bs\<close>])
   2.238 +    apply (simp only: add.assoc)
   2.239 +    apply (rule pos_add_strict)
   2.240 +     apply simp_all
   2.241 +    done
   2.242 +qed
   2.243 +
   2.244 +lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
   2.245 +proof (induct bs)
   2.246 +  case Nil
   2.247 +  then show ?case by simp
   2.248 +next
   2.249 +  case (Cons b bs)
   2.250 +  with bl_to_bin_lt2p_aux[where w=1] show ?case
   2.251 +    by (simp add: bl_to_bin_def)
   2.252 +qed
   2.253 +
   2.254 +lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
   2.255 +  by (metis bin_bl_bin bintr_lt2p bl_bin_bl)
   2.256 +
   2.257 +lemma bl_to_bin_ge2p_aux: "bl_to_bin_aux bs w \<ge> w * (2 ^ length bs)"
   2.258 +proof (induction bs arbitrary: w)
   2.259 +  case Nil
   2.260 +  then show ?case
   2.261 +    by simp
   2.262 +next
   2.263 +  case (Cons b bs)
   2.264 +  from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
   2.265 +  show ?case
   2.266 +    apply (auto simp add: algebra_simps)
   2.267 +    apply (rule add_le_imp_le_left [of \<open>2 ^ length bs\<close>])
   2.268 +    apply (rule add_increasing)
   2.269 +    apply simp_all
   2.270 +    done
   2.271 +qed
   2.272 +
   2.273 +lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0"
   2.274 +  apply (unfold bl_to_bin_def)
   2.275 +  apply (rule xtrans(4))
   2.276 +   apply (rule bl_to_bin_ge2p_aux)
   2.277 +  apply simp
   2.278 +  done
   2.279 +
   2.280 +lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
   2.281 +  apply (unfold bin_to_bl_def)
   2.282 +  apply (cases n, clarsimp)
   2.283 +  apply clarsimp
   2.284 +  apply (auto simp add: bin_to_bl_aux_alt)
   2.285 +  done
   2.286 +
   2.287 +lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
   2.288 +  using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
   2.289 +
   2.290 +lemma butlast_rest_bl2bin_aux:
   2.291 +  "bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
   2.292 +  by (induct bl arbitrary: w) auto
   2.293 +
   2.294 +lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
   2.295 +  by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux)
   2.296 +
   2.297 +lemma trunc_bl2bin_aux:
   2.298 +  "bintrunc m (bl_to_bin_aux bl w) =
   2.299 +    bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
   2.300 +proof (induct bl arbitrary: w)
   2.301 +  case Nil
   2.302 +  show ?case by simp
   2.303 +next
   2.304 +  case (Cons b bl)
   2.305 +  show ?case
   2.306 +  proof (cases "m - length bl")
   2.307 +    case 0
   2.308 +    then have "Suc (length bl) - m = Suc (length bl - m)" by simp
   2.309 +    with Cons show ?thesis by simp
   2.310 +  next
   2.311 +    case (Suc n)
   2.312 +    then have "m - Suc (length bl) = n" by simp
   2.313 +    with Cons Suc show ?thesis by (simp add: take_bit_Suc ac_simps)
   2.314 +  qed
   2.315 +qed
   2.316 +
   2.317 +lemma trunc_bl2bin: "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
   2.318 +  by (simp add: bl_to_bin_def trunc_bl2bin_aux)
   2.319 +
   2.320 +lemma trunc_bl2bin_len [simp]: "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
   2.321 +  by (simp add: trunc_bl2bin)
   2.322 +
   2.323 +lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
   2.324 +  apply (rule trans)
   2.325 +   prefer 2
   2.326 +   apply (rule trunc_bl2bin [symmetric])
   2.327 +  apply (cases "k \<le> length bl")
   2.328 +   apply auto
   2.329 +  done
   2.330 +
   2.331 +lemma take_rest_power_bin: "m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)"
   2.332 +  apply (rule nth_equalityI)
   2.333 +   apply simp
   2.334 +  apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
   2.335 +  done
   2.336 +
   2.337 +lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)"
   2.338 +  by (induct xs arbitrary: w) auto
   2.339 +
   2.340 +lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)"
   2.341 +  unfolding bl_to_bin_def by (erule last_bin_last')
   2.342 +
   2.343 +lemma bin_last_last: "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)"
   2.344 +  by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)
   2.345 +
   2.346 +lemma drop_bin2bl_aux:
   2.347 +  "drop m (bin_to_bl_aux n bin bs) =
   2.348 +    bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
   2.349 +  apply (induction n arbitrary: m bin bs)
   2.350 +   apply auto
   2.351 +  apply (case_tac "m \<le> n")
   2.352 +   apply (auto simp add: not_le Suc_diff_le)
   2.353 +  apply (case_tac "m - n")
   2.354 +   apply auto
   2.355 +  apply (use Suc_diff_Suc in fastforce)
   2.356 +  done
   2.357 +
   2.358 +lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
   2.359 +  by (simp add: bin_to_bl_def drop_bin2bl_aux)
   2.360 +
   2.361 +lemma take_bin2bl_lem1: "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
   2.362 +  apply (induct m arbitrary: w bs)
   2.363 +   apply clarsimp
   2.364 +  apply clarsimp
   2.365 +  apply (simp add: bin_to_bl_aux_alt)
   2.366 +  apply (simp add: bin_to_bl_def)
   2.367 +  apply (simp add: bin_to_bl_aux_alt)
   2.368 +  done
   2.369 +
   2.370 +lemma take_bin2bl_lem: "take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)"
   2.371 +  by (induct n arbitrary: w bs) (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1, simp)
   2.372 +
   2.373 +lemma bin_split_take: "bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)"
   2.374 +  apply (induct n arbitrary: b c)
   2.375 +   apply clarsimp
   2.376 +  apply (clarsimp simp: Let_def split: prod.split_asm)
   2.377 +  apply (simp add: bin_to_bl_def)
   2.378 +  apply (simp add: take_bin2bl_lem drop_bit_Suc)
   2.379 +  done
   2.380 +
   2.381 +lemma bin_to_bl_drop_bit:
   2.382 +  "k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c)"
   2.383 +  using bin_split_take by simp
   2.384 +
   2.385 +lemma bin_split_take1:
   2.386 +  "k = m + n \<Longrightarrow> bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)"
   2.387 +  using bin_split_take by simp
   2.388 +
   2.389 +lemma bl_bin_bl_rep_drop:
   2.390 +  "bin_to_bl n (bl_to_bin bl) =
   2.391 +    replicate (n - length bl) False @ drop (length bl - n) bl"
   2.392 +  by (simp add: bl_to_bin_inj bl_to_bin_rep_F trunc_bl2bin)
   2.393 +
   2.394 +lemma bl_to_bin_aux_cat:
   2.395 +  "bl_to_bin_aux bs (bin_cat w nv v) =
   2.396 +    bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
   2.397 +  by (rule bit_eqI)
   2.398 +    (auto simp add: bin_nth_of_bl_aux bin_nth_cat algebra_simps)
   2.399 +
   2.400 +lemma bin_to_bl_aux_cat:
   2.401 +  "bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
   2.402 +    bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
   2.403 +  by (induction nw arbitrary: w bs) (simp_all add: concat_bit_Suc)
   2.404 +
   2.405 +lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
   2.406 +  using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
   2.407 +  by (simp add: bl_to_bin_def [symmetric])
   2.408 +
   2.409 +lemma bin_to_bl_cat:
   2.410 +  "bin_to_bl (nv + nw) (bin_cat v nw w) =
   2.411 +    bin_to_bl_aux nv v (bin_to_bl nw w)"
   2.412 +  by (simp add: bin_to_bl_def bin_to_bl_aux_cat)
   2.413 +
   2.414 +lemmas bl_to_bin_aux_app_cat =
   2.415 +  trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
   2.416 +
   2.417 +lemmas bin_to_bl_aux_cat_app =
   2.418 +  trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
   2.419 +
   2.420 +lemma bl_to_bin_app_cat:
   2.421 +  "bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)"
   2.422 +  by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)
   2.423 +
   2.424 +lemma bin_to_bl_cat_app:
   2.425 +  "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
   2.426 +  by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
   2.427 +
   2.428 +text \<open>\<open>bl_to_bin_app_cat_alt\<close> and \<open>bl_to_bin_app_cat\<close> are easily interderivable.\<close>
   2.429 +lemma bl_to_bin_app_cat_alt: "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
   2.430 +  by (simp add: bl_to_bin_app_cat)
   2.431 +
   2.432 +lemma mask_lem: "(bl_to_bin (True # replicate n False)) = bl_to_bin (replicate n True) + 1"
   2.433 +  apply (unfold bl_to_bin_def)
   2.434 +  apply (induct n)
   2.435 +   apply simp
   2.436 +  apply (simp only: Suc_eq_plus1 replicate_add append_Cons [symmetric] bl_to_bin_aux_append)
   2.437 +  apply simp
   2.438 +  done
   2.439 +
   2.440 +lemma bin_exhaust:
   2.441 +  "(\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q) \<Longrightarrow> Q" for bin :: int
   2.442 +  apply (cases \<open>even bin\<close>)
   2.443 +   apply (auto elim!: evenE oddE)
   2.444 +   apply fastforce
   2.445 +  apply fastforce
   2.446 +  done
   2.447 +
   2.448 +primrec rbl_succ :: "bool list \<Rightarrow> bool list"
   2.449 +  where
   2.450 +    Nil: "rbl_succ Nil = Nil"
   2.451 +  | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
   2.452 +
   2.453 +primrec rbl_pred :: "bool list \<Rightarrow> bool list"
   2.454 +  where
   2.455 +    Nil: "rbl_pred Nil = Nil"
   2.456 +  | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
   2.457 +
   2.458 +primrec rbl_add :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
   2.459 +  where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
   2.460 +    Nil: "rbl_add Nil x = Nil"
   2.461 +  | Cons: "rbl_add (y # ys) x =
   2.462 +      (let ws = rbl_add ys (tl x)
   2.463 +       in (y \<noteq> hd x) # (if hd x \<and> y then rbl_succ ws else ws))"
   2.464 +
   2.465 +primrec rbl_mult :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
   2.466 +  where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
   2.467 +    Nil: "rbl_mult Nil x = Nil"
   2.468 +  | Cons: "rbl_mult (y # ys) x =
   2.469 +      (let ws = False # rbl_mult ys x
   2.470 +       in if y then rbl_add ws x else ws)"
   2.471 +
   2.472 +lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
   2.473 +  by (induct bl) auto
   2.474 +
   2.475 +lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
   2.476 +  by (induct bl) auto
   2.477 +
   2.478 +lemma size_rbl_add: "length (rbl_add bl cl) = length bl"
   2.479 +  by (induct bl arbitrary: cl) (auto simp: Let_def size_rbl_succ)
   2.480 +
   2.481 +lemma size_rbl_mult: "length (rbl_mult bl cl) = length bl"
   2.482 +  by (induct bl arbitrary: cl) (auto simp add: Let_def size_rbl_add)
   2.483 +
   2.484 +lemmas rbl_sizes [simp] =
   2.485 +  size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
   2.486 +
   2.487 +lemmas rbl_Nils =
   2.488 +  rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
   2.489 +
   2.490 +lemma rbl_add_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb"
   2.491 +  apply (induct bla arbitrary: blb)
   2.492 +   apply simp
   2.493 +  apply clarsimp
   2.494 +  apply (case_tac blb, clarsimp)
   2.495 +  apply (clarsimp simp: Let_def)
   2.496 +  done
   2.497 +
   2.498 +lemma rbl_add_take2:
   2.499 +  "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
   2.500 +  apply (induct bla arbitrary: blb)
   2.501 +   apply simp
   2.502 +  apply clarsimp
   2.503 +  apply (case_tac blb, clarsimp)
   2.504 +  apply (clarsimp simp: Let_def)
   2.505 +  done
   2.506 +
   2.507 +lemma rbl_mult_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb"
   2.508 +  apply (induct bla arbitrary: blb)
   2.509 +   apply simp
   2.510 +  apply clarsimp
   2.511 +  apply (case_tac blb, clarsimp)
   2.512 +  apply (clarsimp simp: Let_def rbl_add_app2)
   2.513 +  done
   2.514 +
   2.515 +lemma rbl_mult_take2:
   2.516 +  "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
   2.517 +  apply (rule trans)
   2.518 +   apply (rule rbl_mult_app2 [symmetric])
   2.519 +   apply simp
   2.520 +  apply (rule_tac f = "rbl_mult bla" in arg_cong)
   2.521 +  apply (rule append_take_drop_id)
   2.522 +  done
   2.523 +
   2.524 +lemma rbl_add_split:
   2.525 +  "P (rbl_add (y # ys) (x # xs)) =
   2.526 +    (\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow>
   2.527 +      (y \<longrightarrow> ((x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws)))) \<and>
   2.528 +      (\<not> y \<longrightarrow> P (x # ws)))"
   2.529 +  by (cases y) (auto simp: Let_def)
   2.530 +
   2.531 +lemma rbl_mult_split:
   2.532 +  "P (rbl_mult (y # ys) xs) =
   2.533 +    (\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow>
   2.534 +      (y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))"
   2.535 +  by (auto simp: Let_def)
   2.536 +
   2.537 +lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
   2.538 +proof (unfold bin_to_bl_def, induction n arbitrary: bin)
   2.539 +  case 0
   2.540 +  then show ?case
   2.541 +    by simp
   2.542 +next
   2.543 +  case (Suc n)
   2.544 +  obtain b k where \<open>bin = of_bool b + 2 * k\<close>
   2.545 +    using bin_exhaust by blast
   2.546 +  moreover have \<open>(2 * k - 1) div 2 = k - 1\<close>
   2.547 +    using even_succ_div_2 [of \<open>2 * (k - 1)\<close>] 
   2.548 +    by simp
   2.549 +  ultimately show ?case
   2.550 +    using Suc [of \<open>bin div 2\<close>]
   2.551 +    by simp (simp add: bin_to_bl_aux_alt)
   2.552 +qed
   2.553 +
   2.554 +lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
   2.555 +  apply (unfold bin_to_bl_def)
   2.556 +  apply (induction n arbitrary: bin)
   2.557 +   apply simp_all
   2.558 +  apply (case_tac bin rule: bin_exhaust)
   2.559 +  apply simp
   2.560 +  apply (simp add: bin_to_bl_aux_alt ac_simps)
   2.561 +  done
   2.562 +
   2.563 +lemma rbl_add:
   2.564 +  "\<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
   2.565 +    rev (bin_to_bl n (bina + binb))"
   2.566 +  apply (unfold bin_to_bl_def)
   2.567 +  apply (induct n)
   2.568 +   apply simp
   2.569 +  apply clarsimp
   2.570 +  apply (case_tac bina rule: bin_exhaust)
   2.571 +  apply (case_tac binb rule: bin_exhaust)
   2.572 +  apply (case_tac b)
   2.573 +   apply (case_tac [!] "ba")
   2.574 +     apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
   2.575 +  done
   2.576 +
   2.577 +lemma rbl_add_long:
   2.578 +  "m \<ge> n \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
   2.579 +    rev (bin_to_bl n (bina + binb))"
   2.580 +  apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
   2.581 +   apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
   2.582 +   apply (rule rev_swap [THEN iffD1])
   2.583 +   apply (simp add: rev_take drop_bin2bl)
   2.584 +  apply simp
   2.585 +  done
   2.586 +
   2.587 +lemma rbl_mult_gt1:
   2.588 +  "m \<ge> length bl \<Longrightarrow>
   2.589 +    rbl_mult bl (rev (bin_to_bl m binb)) =
   2.590 +    rbl_mult bl (rev (bin_to_bl (length bl) binb))"
   2.591 +  apply (rule trans)
   2.592 +   apply (rule rbl_mult_take2 [symmetric])
   2.593 +   apply simp_all
   2.594 +  apply (rule_tac f = "rbl_mult bl" in arg_cong)
   2.595 +  apply (rule rev_swap [THEN iffD1])
   2.596 +  apply (simp add: rev_take drop_bin2bl)
   2.597 +  done
   2.598 +
   2.599 +lemma rbl_mult_gt:
   2.600 +  "m > n \<Longrightarrow>
   2.601 +    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
   2.602 +    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
   2.603 +  by (auto intro: trans [OF rbl_mult_gt1])
   2.604 +
   2.605 +lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
   2.606 +
   2.607 +lemma rbbl_Cons: "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (of_bool b + 2 * x))"
   2.608 +  by (simp add: bin_to_bl_def) (simp add: bin_to_bl_aux_alt)
   2.609 +
   2.610 +lemma rbl_mult:
   2.611 +  "rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
   2.612 +    rev (bin_to_bl n (bina * binb))"
   2.613 +  apply (induct n arbitrary: bina binb)
   2.614 +   apply simp_all
   2.615 +  apply (unfold bin_to_bl_def)
   2.616 +  apply clarsimp
   2.617 +  apply (case_tac bina rule: bin_exhaust)
   2.618 +  apply (case_tac binb rule: bin_exhaust)
   2.619 +  apply simp
   2.620 +  apply (simp add: bin_to_bl_aux_alt)
   2.621 +  apply (simp add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps)
   2.622 +  done
   2.623 +
   2.624 +lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n"
   2.625 +  by (induct xs) auto
   2.626 +
   2.627 +lemma bin_cat_foldl_lem:
   2.628 +  "foldl (\<lambda>u. bin_cat u n) x xs =
   2.629 +    bin_cat x (size xs * n) (foldl (\<lambda>u. bin_cat u n) y xs)"
   2.630 +  apply (induct xs arbitrary: x)
   2.631 +   apply simp
   2.632 +  apply (simp (no_asm))
   2.633 +  apply (frule asm_rl)
   2.634 +  apply (drule meta_spec)
   2.635 +  apply (erule trans)
   2.636 +  apply (drule_tac x = "bin_cat y n a" in meta_spec)
   2.637 +  apply (simp add: bin_cat_assoc_sym min.absorb2)
   2.638 +  done
   2.639 +
   2.640 +lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))"
   2.641 +  apply (unfold bin_rcat_def)
   2.642 +  apply (rule sym)
   2.643 +  apply (induct wl)
   2.644 +   apply (auto simp add: bl_to_bin_append)
   2.645 +  apply (simp add: bl_to_bin_aux_alt sclem)
   2.646 +  apply (simp add: bin_cat_foldl_lem [symmetric])
   2.647 +  done
   2.648 +
   2.649 +lemma bin_last_bl_to_bin: "bin_last (bl_to_bin bs) \<longleftrightarrow> bs \<noteq> [] \<and> last bs"
   2.650 +by(cases "bs = []")(auto simp add: bl_to_bin_def last_bin_last'[where w=0])
   2.651 +
   2.652 +lemma bin_rest_bl_to_bin: "bin_rest (bl_to_bin bs) = bl_to_bin (butlast bs)"
   2.653 +by(cases "bs = []")(simp_all add: bl_to_bin_def butlast_rest_bl2bin_aux)
   2.654 +
   2.655 +lemma bl_xor_aux_bin:
   2.656 +  "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
   2.657 +    bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
   2.658 +  apply (induction n arbitrary: v w bs cs)
   2.659 +   apply auto
   2.660 +  apply (case_tac v rule: bin_exhaust)
   2.661 +  apply (case_tac w rule: bin_exhaust)
   2.662 +  apply clarsimp
   2.663 +  done
   2.664 +
   2.665 +lemma bl_or_aux_bin:
   2.666 +  "map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
   2.667 +    bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)"
   2.668 +  by (induct n arbitrary: v w bs cs) simp_all
   2.669 +
   2.670 +lemma bl_and_aux_bin:
   2.671 +  "map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
   2.672 +    bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)"
   2.673 +  by (induction n arbitrary: v w bs cs) simp_all
   2.674 +
   2.675 +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.676 +  by (induct n arbitrary: w cs) auto
   2.677 +
   2.678 +lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
   2.679 +  by (simp add: bin_to_bl_def bl_not_aux_bin)
   2.680 +
   2.681 +lemma bl_and_bin: "map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
   2.682 +  by (simp add: bin_to_bl_def bl_and_aux_bin)
   2.683 +
   2.684 +lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
   2.685 +  by (simp add: bin_to_bl_def bl_or_aux_bin)
   2.686 +
   2.687 +lemma bl_xor_bin: "map2 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
   2.688 +  using bl_xor_aux_bin by (simp add: bin_to_bl_def)
   2.689 +
   2.690  end
     3.1 --- a/src/HOL/Word/Bits_Int.thy	Mon Aug 03 16:21:33 2020 +0200
     3.2 +++ b/src/HOL/Word/Bits_Int.thy	Tue Aug 04 09:24:00 2020 +0000
     3.3 @@ -63,110 +63,6 @@
     3.4    by auto
     3.5  
     3.6  
     3.7 -subsection \<open>Explicit bit representation of \<^typ>\<open>int\<close>\<close>
     3.8 -
     3.9 -primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
    3.10 -  where
    3.11 -    Nil: "bl_to_bin_aux [] w = w"
    3.12 -  | Cons: "bl_to_bin_aux (b # bs) w = bl_to_bin_aux bs (of_bool b + 2 * w)"
    3.13 -
    3.14 -definition bl_to_bin :: "bool list \<Rightarrow> int"
    3.15 -  where "bl_to_bin bs = bl_to_bin_aux bs 0"
    3.16 -
    3.17 -primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
    3.18 -  where
    3.19 -    Z: "bin_to_bl_aux 0 w bl = bl"
    3.20 -  | Suc: "bin_to_bl_aux (Suc n) w bl = bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
    3.21 -
    3.22 -definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
    3.23 -  where "bin_to_bl n w = bin_to_bl_aux n w []"
    3.24 -
    3.25 -lemma bin_to_bl_aux_zero_minus_simp [simp]:
    3.26 -  "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)"
    3.27 -  by (cases n) auto
    3.28 -
    3.29 -lemma bin_to_bl_aux_minus1_minus_simp [simp]:
    3.30 -  "0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)"
    3.31 -  by (cases n) auto
    3.32 -
    3.33 -lemma bin_to_bl_aux_one_minus_simp [simp]:
    3.34 -  "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)"
    3.35 -  by (cases n) auto
    3.36 -
    3.37 -lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
    3.38 -  "0 < n \<Longrightarrow>
    3.39 -    bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)"
    3.40 -  by (cases n) simp_all
    3.41 -
    3.42 -lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
    3.43 -  "0 < n \<Longrightarrow>
    3.44 -    bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
    3.45 -  by (cases n) simp_all
    3.46 -
    3.47 -lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
    3.48 -  by (induct bs arbitrary: w) auto
    3.49 -
    3.50 -lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
    3.51 -  by (induct n arbitrary: w bs) auto
    3.52 -
    3.53 -lemma bl_to_bin_append: "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
    3.54 -  unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
    3.55 -
    3.56 -lemma bin_to_bl_aux_alt: "bin_to_bl_aux n w bs = bin_to_bl n w @ bs"
    3.57 -  by (simp add: bin_to_bl_def bin_to_bl_aux_append)
    3.58 -
    3.59 -lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
    3.60 -  by (auto simp: bin_to_bl_def)
    3.61 -
    3.62 -lemma size_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
    3.63 -  by (induct n arbitrary: w bs) auto
    3.64 -
    3.65 -lemma size_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
    3.66 -  by (simp add: bin_to_bl_def size_bin_to_bl_aux)
    3.67 -
    3.68 -lemma bl_bin_bl': "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs"
    3.69 -  apply (induct bs arbitrary: w n)
    3.70 -   apply auto
    3.71 -    apply (simp_all only: add_Suc [symmetric])
    3.72 -    apply (auto simp add: bin_to_bl_def)
    3.73 -  done
    3.74 -
    3.75 -lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
    3.76 -  unfolding bl_to_bin_def
    3.77 -  apply (rule box_equals)
    3.78 -    apply (rule bl_bin_bl')
    3.79 -   prefer 2
    3.80 -   apply (rule bin_to_bl_aux.Z)
    3.81 -  apply simp
    3.82 -  done
    3.83 -
    3.84 -lemma bl_to_bin_inj: "bl_to_bin bs = bl_to_bin cs \<Longrightarrow> length bs = length cs \<Longrightarrow> bs = cs"
    3.85 -  apply (rule_tac box_equals)
    3.86 -    defer
    3.87 -    apply (rule bl_bin_bl)
    3.88 -   apply (rule bl_bin_bl)
    3.89 -  apply simp
    3.90 -  done
    3.91 -
    3.92 -lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
    3.93 -  by (auto simp: bl_to_bin_def)
    3.94 -
    3.95 -lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
    3.96 -  by (auto simp: bl_to_bin_def)
    3.97 -
    3.98 -lemma bin_to_bl_zero_aux: "bin_to_bl_aux n 0 bl = replicate n False @ bl"
    3.99 -  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
   3.100 -
   3.101 -lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False"
   3.102 -  by (simp add: bin_to_bl_def bin_to_bl_zero_aux)
   3.103 -
   3.104 -lemma bin_to_bl_minus1_aux: "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
   3.105 -  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
   3.106 -
   3.107 -lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
   3.108 -  by (simp add: bin_to_bl_def bin_to_bl_minus1_aux)
   3.109 -
   3.110 -
   3.111  subsection \<open>Bit projection\<close>
   3.112  
   3.113  abbreviation (input) bin_nth :: \<open>int \<Rightarrow> nat \<Rightarrow> bool\<close>
   3.114 @@ -1640,558 +1536,4 @@
   3.115    "bin_sc n True i = i OR (1 << n)"
   3.116    by (induct n arbitrary: i) (rule bin_rl_eqI; simp)+
   3.117  
   3.118 -
   3.119 -subsection \<open>Semantic interpretation of \<^typ>\<open>bool list\<close> as \<^typ>\<open>int\<close>\<close>
   3.120 -
   3.121 -lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (bintrunc n w)"
   3.122 -  by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def take_bit_Suc ac_simps mod_2_eq_odd)
   3.123 -
   3.124 -lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
   3.125 -  by (auto simp: bin_to_bl_def bin_bl_bin')
   3.126 -
   3.127 -lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
   3.128 -  by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def)
   3.129 -
   3.130 -lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
   3.131 -  by (auto intro: bl_to_bin_inj)
   3.132 -
   3.133 -lemma bin_to_bl_aux_bintr:
   3.134 -  "bin_to_bl_aux n (bintrunc m bin) bl =
   3.135 -    replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
   3.136 -  apply (induct n arbitrary: m bin bl)
   3.137 -   apply clarsimp
   3.138 -  apply clarsimp
   3.139 -  apply (case_tac "m")
   3.140 -   apply (clarsimp simp: bin_to_bl_zero_aux)
   3.141 -   apply (erule thin_rl)
   3.142 -   apply (induct_tac n)
   3.143 -    apply (auto simp add: take_bit_Suc)
   3.144 -  done
   3.145 -
   3.146 -lemma bin_to_bl_bintr:
   3.147 -  "bin_to_bl n (bintrunc m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin"
   3.148 -  unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
   3.149 -
   3.150 -lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
   3.151 -  by (induct n) auto
   3.152 -
   3.153 -lemma len_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
   3.154 -  by (fact size_bin_to_bl_aux)
   3.155 -
   3.156 -lemma len_bin_to_bl: "length (bin_to_bl n w) = n"
   3.157 -  by (fact size_bin_to_bl) (* FIXME: duplicate *)
   3.158 -
   3.159 -lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
   3.160 -  by (induction bs arbitrary: w) (simp_all add: bin_sign_def)
   3.161 -
   3.162 -lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
   3.163 -  by (simp add: bl_to_bin_def sign_bl_bin')
   3.164 -
   3.165 -lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (sbintrunc n w) = -1)"
   3.166 -  by (induction n arbitrary: w bs) (auto simp add: bin_sign_def even_iff_mod_2_eq_zero bit_Suc)
   3.167 -
   3.168 -lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
   3.169 -  unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
   3.170 -
   3.171 -lemma bin_nth_of_bl_aux:
   3.172 -  "bin_nth (bl_to_bin_aux bl w) n =
   3.173 -    (n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bin_nth w (n - size bl))"
   3.174 -  apply (induction bl arbitrary: w)
   3.175 -   apply simp_all
   3.176 -  apply safe
   3.177 -                      apply (simp_all add: not_le nth_append bit_double_iff even_bit_succ_iff split: if_splits)
   3.178 -  done
   3.179 -
   3.180 -lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)"
   3.181 -  by (simp add: bl_to_bin_def bin_nth_of_bl_aux)
   3.182 -
   3.183 -lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
   3.184 -  apply (induct n arbitrary: m w)
   3.185 -   apply clarsimp
   3.186 -   apply (case_tac m, clarsimp)
   3.187 -   apply (clarsimp simp: bin_to_bl_def)
   3.188 -   apply (simp add: bin_to_bl_aux_alt)
   3.189 -  apply (case_tac m, clarsimp)
   3.190 -  apply (clarsimp simp: bin_to_bl_def)
   3.191 -  apply (simp add: bin_to_bl_aux_alt bit_Suc)
   3.192 -  done
   3.193 -
   3.194 -lemma nth_bin_to_bl_aux:
   3.195 -  "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
   3.196 -    (if n < m then bit w (m - 1 - n) else bl ! (n - m))"
   3.197 -  apply (induction bl arbitrary: w)
   3.198 -   apply simp_all
   3.199 -   apply (simp add: bin_nth_bl [of \<open>m - Suc n\<close> m] rev_nth flip: bin_to_bl_def)
   3.200 -   apply (metis One_nat_def Suc_pred add_diff_cancel_left'
   3.201 -     add_diff_cancel_right' bin_to_bl_aux_alt bin_to_bl_def
   3.202 -     diff_Suc_Suc diff_is_0_eq diff_zero less_Suc_eq_0_disj
   3.203 -     less_antisym less_imp_Suc_add list.size(3) nat_less_le nth_append size_bin_to_bl_aux)
   3.204 -  done
   3.205 -
   3.206 -lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
   3.207 -  by (simp add: bin_to_bl_def nth_bin_to_bl_aux)
   3.208 -
   3.209 -lemma bl_to_bin_lt2p_aux: "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
   3.210 -proof (induction bs arbitrary: w)
   3.211 -  case Nil
   3.212 -  then show ?case
   3.213 -    by simp
   3.214 -next
   3.215 -  case (Cons b bs)
   3.216 -  from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
   3.217 -  show ?case
   3.218 -    apply (auto simp add: algebra_simps)
   3.219 -    apply (subst mult_2 [of \<open>2 ^ length bs\<close>])
   3.220 -    apply (simp only: add.assoc)
   3.221 -    apply (rule pos_add_strict)
   3.222 -     apply simp_all
   3.223 -    done
   3.224 -qed
   3.225 -
   3.226 -lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
   3.227 -proof (induct bs)
   3.228 -  case Nil
   3.229 -  then show ?case by simp
   3.230 -next
   3.231 -  case (Cons b bs)
   3.232 -  with bl_to_bin_lt2p_aux[where w=1] show ?case
   3.233 -    by (simp add: bl_to_bin_def)
   3.234 -qed
   3.235 -
   3.236 -lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
   3.237 -  by (metis bin_bl_bin bintr_lt2p bl_bin_bl)
   3.238 -
   3.239 -lemma bl_to_bin_ge2p_aux: "bl_to_bin_aux bs w \<ge> w * (2 ^ length bs)"
   3.240 -proof (induction bs arbitrary: w)
   3.241 -  case Nil
   3.242 -  then show ?case
   3.243 -    by simp
   3.244 -next
   3.245 -  case (Cons b bs)
   3.246 -  from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
   3.247 -  show ?case
   3.248 -    apply (auto simp add: algebra_simps)
   3.249 -    apply (rule add_le_imp_le_left [of \<open>2 ^ length bs\<close>])
   3.250 -    apply (rule add_increasing)
   3.251 -    apply simp_all
   3.252 -    done
   3.253 -qed
   3.254 -
   3.255 -lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0"
   3.256 -  apply (unfold bl_to_bin_def)
   3.257 -  apply (rule xtrans(4))
   3.258 -   apply (rule bl_to_bin_ge2p_aux)
   3.259 -  apply simp
   3.260 -  done
   3.261 -
   3.262 -lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
   3.263 -  apply (unfold bin_to_bl_def)
   3.264 -  apply (cases n, clarsimp)
   3.265 -  apply clarsimp
   3.266 -  apply (auto simp add: bin_to_bl_aux_alt)
   3.267 -  done
   3.268 -
   3.269 -lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
   3.270 -  using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
   3.271 -
   3.272 -lemma butlast_rest_bl2bin_aux:
   3.273 -  "bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
   3.274 -  by (induct bl arbitrary: w) auto
   3.275 -
   3.276 -lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
   3.277 -  by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux)
   3.278 -
   3.279 -lemma trunc_bl2bin_aux:
   3.280 -  "bintrunc m (bl_to_bin_aux bl w) =
   3.281 -    bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
   3.282 -proof (induct bl arbitrary: w)
   3.283 -  case Nil
   3.284 -  show ?case by simp
   3.285 -next
   3.286 -  case (Cons b bl)
   3.287 -  show ?case
   3.288 -  proof (cases "m - length bl")
   3.289 -    case 0
   3.290 -    then have "Suc (length bl) - m = Suc (length bl - m)" by simp
   3.291 -    with Cons show ?thesis by simp
   3.292 -  next
   3.293 -    case (Suc n)
   3.294 -    then have "m - Suc (length bl) = n" by simp
   3.295 -    with Cons Suc show ?thesis by (simp add: take_bit_Suc ac_simps)
   3.296 -  qed
   3.297 -qed
   3.298 -
   3.299 -lemma trunc_bl2bin: "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
   3.300 -  by (simp add: bl_to_bin_def trunc_bl2bin_aux)
   3.301 -
   3.302 -lemma trunc_bl2bin_len [simp]: "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
   3.303 -  by (simp add: trunc_bl2bin)
   3.304 -
   3.305 -lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
   3.306 -  apply (rule trans)
   3.307 -   prefer 2
   3.308 -   apply (rule trunc_bl2bin [symmetric])
   3.309 -  apply (cases "k \<le> length bl")
   3.310 -   apply auto
   3.311 -  done
   3.312 -
   3.313 -lemma take_rest_power_bin: "m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)"
   3.314 -  apply (rule nth_equalityI)
   3.315 -   apply simp
   3.316 -  apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
   3.317 -  done
   3.318 -
   3.319 -lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)"
   3.320 -  by (induct xs arbitrary: w) auto
   3.321 -
   3.322 -lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)"
   3.323 -  unfolding bl_to_bin_def by (erule last_bin_last')
   3.324 -
   3.325 -lemma bin_last_last: "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)"
   3.326 -  by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)
   3.327 -
   3.328 -lemma drop_bin2bl_aux:
   3.329 -  "drop m (bin_to_bl_aux n bin bs) =
   3.330 -    bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
   3.331 -  apply (induction n arbitrary: m bin bs)
   3.332 -   apply auto
   3.333 -  apply (case_tac "m \<le> n")
   3.334 -   apply (auto simp add: not_le Suc_diff_le)
   3.335 -  apply (case_tac "m - n")
   3.336 -   apply auto
   3.337 -  apply (use Suc_diff_Suc in fastforce)
   3.338 -  done
   3.339 -
   3.340 -lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
   3.341 -  by (simp add: bin_to_bl_def drop_bin2bl_aux)
   3.342 -
   3.343 -lemma take_bin2bl_lem1: "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
   3.344 -  apply (induct m arbitrary: w bs)
   3.345 -   apply clarsimp
   3.346 -  apply clarsimp
   3.347 -  apply (simp add: bin_to_bl_aux_alt)
   3.348 -  apply (simp add: bin_to_bl_def)
   3.349 -  apply (simp add: bin_to_bl_aux_alt)
   3.350 -  done
   3.351 -
   3.352 -lemma take_bin2bl_lem: "take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)"
   3.353 -  by (induct n arbitrary: w bs) (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1, simp)
   3.354 -
   3.355 -lemma bin_split_take: "bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)"
   3.356 -  apply (induct n arbitrary: b c)
   3.357 -   apply clarsimp
   3.358 -  apply (clarsimp simp: Let_def split: prod.split_asm)
   3.359 -  apply (simp add: bin_to_bl_def)
   3.360 -  apply (simp add: take_bin2bl_lem drop_bit_Suc)
   3.361 -  done
   3.362 -
   3.363 -lemma bin_to_bl_drop_bit:
   3.364 -  "k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c)"
   3.365 -  using bin_split_take by simp
   3.366 -
   3.367 -lemma bin_split_take1:
   3.368 -  "k = m + n \<Longrightarrow> bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)"
   3.369 -  using bin_split_take by simp
   3.370 -
   3.371 -lemma bl_bin_bl_rep_drop:
   3.372 -  "bin_to_bl n (bl_to_bin bl) =
   3.373 -    replicate (n - length bl) False @ drop (length bl - n) bl"
   3.374 -  by (simp add: bl_to_bin_inj bl_to_bin_rep_F trunc_bl2bin)
   3.375 -
   3.376 -lemma bl_to_bin_aux_cat:
   3.377 -  "bl_to_bin_aux bs (bin_cat w nv v) =
   3.378 -    bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
   3.379 -  by (rule bit_eqI)
   3.380 -    (auto simp add: bin_nth_of_bl_aux bin_nth_cat algebra_simps)
   3.381 -
   3.382 -lemma bin_to_bl_aux_cat:
   3.383 -  "bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
   3.384 -    bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
   3.385 -  by (induction nw arbitrary: w bs) (simp_all add: concat_bit_Suc)
   3.386 -
   3.387 -lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
   3.388 -  using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
   3.389 -  by (simp add: bl_to_bin_def [symmetric])
   3.390 -
   3.391 -lemma bin_to_bl_cat:
   3.392 -  "bin_to_bl (nv + nw) (bin_cat v nw w) =
   3.393 -    bin_to_bl_aux nv v (bin_to_bl nw w)"
   3.394 -  by (simp add: bin_to_bl_def bin_to_bl_aux_cat)
   3.395 -
   3.396 -lemmas bl_to_bin_aux_app_cat =
   3.397 -  trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
   3.398 -
   3.399 -lemmas bin_to_bl_aux_cat_app =
   3.400 -  trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
   3.401 -
   3.402 -lemma bl_to_bin_app_cat:
   3.403 -  "bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)"
   3.404 -  by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)
   3.405 -
   3.406 -lemma bin_to_bl_cat_app:
   3.407 -  "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
   3.408 -  by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
   3.409 -
   3.410 -text \<open>\<open>bl_to_bin_app_cat_alt\<close> and \<open>bl_to_bin_app_cat\<close> are easily interderivable.\<close>
   3.411 -lemma bl_to_bin_app_cat_alt: "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
   3.412 -  by (simp add: bl_to_bin_app_cat)
   3.413 -
   3.414 -lemma mask_lem: "(bl_to_bin (True # replicate n False)) = bl_to_bin (replicate n True) + 1"
   3.415 -  apply (unfold bl_to_bin_def)
   3.416 -  apply (induct n)
   3.417 -   apply simp
   3.418 -  apply (simp only: Suc_eq_plus1 replicate_add append_Cons [symmetric] bl_to_bin_aux_append)
   3.419 -  apply simp
   3.420 -  done
   3.421 -
   3.422 -lemma bin_exhaust:
   3.423 -  "(\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q) \<Longrightarrow> Q" for bin :: int
   3.424 -  apply (cases \<open>even bin\<close>)
   3.425 -   apply (auto elim!: evenE oddE)
   3.426 -   apply fastforce
   3.427 -  apply fastforce
   3.428 -  done
   3.429 -
   3.430 -primrec rbl_succ :: "bool list \<Rightarrow> bool list"
   3.431 -  where
   3.432 -    Nil: "rbl_succ Nil = Nil"
   3.433 -  | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
   3.434 -
   3.435 -primrec rbl_pred :: "bool list \<Rightarrow> bool list"
   3.436 -  where
   3.437 -    Nil: "rbl_pred Nil = Nil"
   3.438 -  | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
   3.439 -
   3.440 -primrec rbl_add :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
   3.441 -  where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
   3.442 -    Nil: "rbl_add Nil x = Nil"
   3.443 -  | Cons: "rbl_add (y # ys) x =
   3.444 -      (let ws = rbl_add ys (tl x)
   3.445 -       in (y \<noteq> hd x) # (if hd x \<and> y then rbl_succ ws else ws))"
   3.446 -
   3.447 -primrec rbl_mult :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
   3.448 -  where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
   3.449 -    Nil: "rbl_mult Nil x = Nil"
   3.450 -  | Cons: "rbl_mult (y # ys) x =
   3.451 -      (let ws = False # rbl_mult ys x
   3.452 -       in if y then rbl_add ws x else ws)"
   3.453 -
   3.454 -lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
   3.455 -  by (induct bl) auto
   3.456 -
   3.457 -lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
   3.458 -  by (induct bl) auto
   3.459 -
   3.460 -lemma size_rbl_add: "length (rbl_add bl cl) = length bl"
   3.461 -  by (induct bl arbitrary: cl) (auto simp: Let_def size_rbl_succ)
   3.462 -
   3.463 -lemma size_rbl_mult: "length (rbl_mult bl cl) = length bl"
   3.464 -  by (induct bl arbitrary: cl) (auto simp add: Let_def size_rbl_add)
   3.465 -
   3.466 -lemmas rbl_sizes [simp] =
   3.467 -  size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
   3.468 -
   3.469 -lemmas rbl_Nils =
   3.470 -  rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
   3.471 -
   3.472 -lemma rbl_add_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb"
   3.473 -  apply (induct bla arbitrary: blb)
   3.474 -   apply simp
   3.475 -  apply clarsimp
   3.476 -  apply (case_tac blb, clarsimp)
   3.477 -  apply (clarsimp simp: Let_def)
   3.478 -  done
   3.479 -
   3.480 -lemma rbl_add_take2:
   3.481 -  "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
   3.482 -  apply (induct bla arbitrary: blb)
   3.483 -   apply simp
   3.484 -  apply clarsimp
   3.485 -  apply (case_tac blb, clarsimp)
   3.486 -  apply (clarsimp simp: Let_def)
   3.487 -  done
   3.488 -
   3.489 -lemma rbl_mult_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb"
   3.490 -  apply (induct bla arbitrary: blb)
   3.491 -   apply simp
   3.492 -  apply clarsimp
   3.493 -  apply (case_tac blb, clarsimp)
   3.494 -  apply (clarsimp simp: Let_def rbl_add_app2)
   3.495 -  done
   3.496 -
   3.497 -lemma rbl_mult_take2:
   3.498 -  "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
   3.499 -  apply (rule trans)
   3.500 -   apply (rule rbl_mult_app2 [symmetric])
   3.501 -   apply simp
   3.502 -  apply (rule_tac f = "rbl_mult bla" in arg_cong)
   3.503 -  apply (rule append_take_drop_id)
   3.504 -  done
   3.505 -
   3.506 -lemma rbl_add_split:
   3.507 -  "P (rbl_add (y # ys) (x # xs)) =
   3.508 -    (\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow>
   3.509 -      (y \<longrightarrow> ((x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws)))) \<and>
   3.510 -      (\<not> y \<longrightarrow> P (x # ws)))"
   3.511 -  by (cases y) (auto simp: Let_def)
   3.512 -
   3.513 -lemma rbl_mult_split:
   3.514 -  "P (rbl_mult (y # ys) xs) =
   3.515 -    (\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow>
   3.516 -      (y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))"
   3.517 -  by (auto simp: Let_def)
   3.518 -
   3.519 -lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
   3.520 -proof (unfold bin_to_bl_def, induction n arbitrary: bin)
   3.521 -  case 0
   3.522 -  then show ?case
   3.523 -    by simp
   3.524 -next
   3.525 -  case (Suc n)
   3.526 -  obtain b k where \<open>bin = of_bool b + 2 * k\<close>
   3.527 -    using bin_exhaust by blast
   3.528 -  moreover have \<open>(2 * k - 1) div 2 = k - 1\<close>
   3.529 -    using even_succ_div_2 [of \<open>2 * (k - 1)\<close>] 
   3.530 -    by simp
   3.531 -  ultimately show ?case
   3.532 -    using Suc [of \<open>bin div 2\<close>]
   3.533 -    by simp (simp add: bin_to_bl_aux_alt)
   3.534 -qed
   3.535 -
   3.536 -lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
   3.537 -  apply (unfold bin_to_bl_def)
   3.538 -  apply (induction n arbitrary: bin)
   3.539 -   apply simp_all
   3.540 -  apply (case_tac bin rule: bin_exhaust)
   3.541 -  apply simp
   3.542 -  apply (simp add: bin_to_bl_aux_alt ac_simps)
   3.543 -  done
   3.544 -
   3.545 -lemma rbl_add:
   3.546 -  "\<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
   3.547 -    rev (bin_to_bl n (bina + binb))"
   3.548 -  apply (unfold bin_to_bl_def)
   3.549 -  apply (induct n)
   3.550 -   apply simp
   3.551 -  apply clarsimp
   3.552 -  apply (case_tac bina rule: bin_exhaust)
   3.553 -  apply (case_tac binb rule: bin_exhaust)
   3.554 -  apply (case_tac b)
   3.555 -   apply (case_tac [!] "ba")
   3.556 -     apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
   3.557 -  done
   3.558 -
   3.559 -lemma rbl_add_long:
   3.560 -  "m \<ge> n \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
   3.561 -    rev (bin_to_bl n (bina + binb))"
   3.562 -  apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
   3.563 -   apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
   3.564 -   apply (rule rev_swap [THEN iffD1])
   3.565 -   apply (simp add: rev_take drop_bin2bl)
   3.566 -  apply simp
   3.567 -  done
   3.568 -
   3.569 -lemma rbl_mult_gt1:
   3.570 -  "m \<ge> length bl \<Longrightarrow>
   3.571 -    rbl_mult bl (rev (bin_to_bl m binb)) =
   3.572 -    rbl_mult bl (rev (bin_to_bl (length bl) binb))"
   3.573 -  apply (rule trans)
   3.574 -   apply (rule rbl_mult_take2 [symmetric])
   3.575 -   apply simp_all
   3.576 -  apply (rule_tac f = "rbl_mult bl" in arg_cong)
   3.577 -  apply (rule rev_swap [THEN iffD1])
   3.578 -  apply (simp add: rev_take drop_bin2bl)
   3.579 -  done
   3.580 -
   3.581 -lemma rbl_mult_gt:
   3.582 -  "m > n \<Longrightarrow>
   3.583 -    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
   3.584 -    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
   3.585 -  by (auto intro: trans [OF rbl_mult_gt1])
   3.586 -
   3.587 -lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
   3.588 -
   3.589 -lemma rbbl_Cons: "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (of_bool b + 2 * x))"
   3.590 -  by (simp add: bin_to_bl_def) (simp add: bin_to_bl_aux_alt)
   3.591 -
   3.592 -lemma rbl_mult:
   3.593 -  "rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
   3.594 -    rev (bin_to_bl n (bina * binb))"
   3.595 -  apply (induct n arbitrary: bina binb)
   3.596 -   apply simp_all
   3.597 -  apply (unfold bin_to_bl_def)
   3.598 -  apply clarsimp
   3.599 -  apply (case_tac bina rule: bin_exhaust)
   3.600 -  apply (case_tac binb rule: bin_exhaust)
   3.601 -  apply simp
   3.602 -  apply (simp add: bin_to_bl_aux_alt)
   3.603 -  apply (simp add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps)
   3.604 -  done
   3.605 -
   3.606 -lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n"
   3.607 -  by (induct xs) auto
   3.608 -
   3.609 -lemma bin_cat_foldl_lem:
   3.610 -  "foldl (\<lambda>u. bin_cat u n) x xs =
   3.611 -    bin_cat x (size xs * n) (foldl (\<lambda>u. bin_cat u n) y xs)"
   3.612 -  apply (induct xs arbitrary: x)
   3.613 -   apply simp
   3.614 -  apply (simp (no_asm))
   3.615 -  apply (frule asm_rl)
   3.616 -  apply (drule meta_spec)
   3.617 -  apply (erule trans)
   3.618 -  apply (drule_tac x = "bin_cat y n a" in meta_spec)
   3.619 -  apply (simp add: bin_cat_assoc_sym min.absorb2)
   3.620 -  done
   3.621 -
   3.622 -lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))"
   3.623 -  apply (unfold bin_rcat_def)
   3.624 -  apply (rule sym)
   3.625 -  apply (induct wl)
   3.626 -   apply (auto simp add: bl_to_bin_append)
   3.627 -  apply (simp add: bl_to_bin_aux_alt sclem)
   3.628 -  apply (simp add: bin_cat_foldl_lem [symmetric])
   3.629 -  done
   3.630 -
   3.631 -lemma bin_last_bl_to_bin: "bin_last (bl_to_bin bs) \<longleftrightarrow> bs \<noteq> [] \<and> last bs"
   3.632 -by(cases "bs = []")(auto simp add: bl_to_bin_def last_bin_last'[where w=0])
   3.633 -
   3.634 -lemma bin_rest_bl_to_bin: "bin_rest (bl_to_bin bs) = bl_to_bin (butlast bs)"
   3.635 -by(cases "bs = []")(simp_all add: bl_to_bin_def butlast_rest_bl2bin_aux)
   3.636 -
   3.637 -lemma bl_xor_aux_bin:
   3.638 -  "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
   3.639 -    bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
   3.640 -  apply (induction n arbitrary: v w bs cs)
   3.641 -   apply auto
   3.642 -  apply (case_tac v rule: bin_exhaust)
   3.643 -  apply (case_tac w rule: bin_exhaust)
   3.644 -  apply clarsimp
   3.645 -  done
   3.646 -
   3.647 -lemma bl_or_aux_bin:
   3.648 -  "map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
   3.649 -    bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)"
   3.650 -  by (induct n arbitrary: v w bs cs) simp_all
   3.651 -
   3.652 -lemma bl_and_aux_bin:
   3.653 -  "map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
   3.654 -    bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)"
   3.655 -  by (induction n arbitrary: v w bs cs) simp_all
   3.656 -
   3.657 -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.658 -  by (induct n arbitrary: w cs) auto
   3.659 -
   3.660 -lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
   3.661 -  by (simp add: bin_to_bl_def bl_not_aux_bin)
   3.662 -
   3.663 -lemma bl_and_bin: "map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
   3.664 -  by (simp add: bin_to_bl_def bl_and_aux_bin)
   3.665 -
   3.666 -lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
   3.667 -  by (simp add: bin_to_bl_def bl_or_aux_bin)
   3.668 -
   3.669 -lemma bl_xor_bin: "map2 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
   3.670 -  using bl_xor_aux_bin by (simp add: bin_to_bl_def)
   3.671 -
   3.672  end