# HG changeset patch
# User paulson
# Date 1596646200 -3600
# Node ID 6a2f439013507cf9c6ee4aa6348b8aa0dc5ac0a1
# Parent  43a43b182a81f06f274c59b1157ffaeef20722e4# Parent  3f8e6c0166ac0d644640f76f6b9e3fa3b55e8be8
merged

diff -r 3f8e6c0166ac -r 6a2f43901350 NEWS
--- a/NEWS	Tue Aug 04 11:45:03 2020 +0100
+++ b/NEWS	Wed Aug 05 17:50:00 2020 +0100
@@ -83,6 +83,13 @@
 * Session HOL-Word: Compound operation "bin_split" simplifies by default
 into its components "drop_bit" and "take_bit".  INCOMPATIBILITY.
 
+* Session HOL-Word: Uniform polymorphic "mask" operation for both
+types int and word.  INCOMPATIBILITY
+
+* Session HOL-Word: Operations lsb, msb and set_bit are separated
+into theories Misc_lsb, Misc_msb and Misc_set_bit respectively.
+INCOMPATIBILITY.
+
 * Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth",
 "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and "max_word" are now
 mere input abbreviations.  Minor INCOMPATIBILITY.
@@ -90,10 +97,6 @@
 * Session HOL-Word: Theory HOL-Library.Z2 is not imported any longer.
 Minor INCOMPATIBILITY.
 
-* Session HOL-Word: Operations lsb, msb and set_bit are separated
-into theories Misc_lsb, Misc_msb and Misc_set_bit respectively.
-INCOMPATIBILITY.
-
 * Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands
 are in working order again, as opposed to outputting "GaveUp" on nearly
 all problems.
diff -r 3f8e6c0166ac -r 6a2f43901350 src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Tue Aug 04 11:45:03 2020 +0100
+++ b/src/HOL/Library/Bit_Operations.thy	Wed Aug 05 17:50:00 2020 +0100
@@ -15,9 +15,11 @@
   fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>AND\<close> 64)
     and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>OR\<close>  59)
     and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>XOR\<close> 59)
+    and mask :: \<open>nat \<Rightarrow> 'a\<close>
   assumes bit_and_iff: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
     and bit_or_iff: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
     and bit_xor_iff: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
+    and mask_eq_exp_minus_1: \<open>mask n = 2 ^ n - 1\<close>
 begin
 
 text \<open>
@@ -93,9 +95,6 @@
   \<open>take_bit n (a XOR b) = take_bit n a XOR take_bit n b\<close>
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff)
 
-definition mask :: \<open>nat \<Rightarrow> 'a\<close>
-  where mask_eq_exp_minus_1: \<open>mask n = 2 ^ n - 1\<close>
-
 lemma bit_mask_iff:
   \<open>bit (mask m) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
   by (simp add: mask_eq_exp_minus_1 bit_mask_iff)
@@ -104,25 +103,33 @@
   \<open>even (mask n) \<longleftrightarrow> n = 0\<close>
   using bit_mask_iff [of n 0] by auto
 
-lemma mask_0 [simp, code]:
+lemma mask_0 [simp]:
   \<open>mask 0 = 0\<close>
   by (simp add: mask_eq_exp_minus_1)
 
-lemma mask_Suc_exp [code]:
+lemma mask_Suc_0 [simp]:
+  \<open>mask (Suc 0) = 1\<close>
+  by (simp add: mask_eq_exp_minus_1 add_implies_diff sym)
+
+lemma mask_Suc_exp:
   \<open>mask (Suc n) = 2 ^ n OR mask n\<close>
   by (rule bit_eqI)
     (auto simp add: bit_or_iff bit_mask_iff bit_exp_iff not_less le_less_Suc_eq)
 
 lemma mask_Suc_double:
-  \<open>mask (Suc n) = 2 * mask n OR 1\<close>
+  \<open>mask (Suc n) = 1 OR 2 * mask n\<close>
 proof (rule bit_eqI)
   fix q
   assume \<open>2 ^ q \<noteq> 0\<close>
-  show \<open>bit (mask (Suc n)) q \<longleftrightarrow> bit (2 * mask n OR 1) q\<close>
+  show \<open>bit (mask (Suc n)) q \<longleftrightarrow> bit (1 OR 2 * mask n) q\<close>
     by (cases q)
       (simp_all add: even_mask_iff even_or_iff bit_or_iff bit_mask_iff bit_exp_iff bit_double_iff not_less le_less_Suc_eq bit_1_iff, auto simp add: mult_2)
 qed
 
+lemma mask_numeral:
+  \<open>mask (numeral n) = 1 + 2 * mask (pred_numeral n)\<close>
+  by (simp add: numeral_eq_Suc mask_Suc_double one_or_eq ac_simps)
+
 lemma take_bit_eq_mask:
   \<open>take_bit n a = a AND mask n\<close>
   by (rule bit_eqI)
@@ -495,6 +502,9 @@
   \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close> for k l :: int
   by (auto simp add: xor_int_def bit_or_int_iff bit_and_int_iff bit_not_int_iff)
 
+definition mask_int :: \<open>nat \<Rightarrow> int\<close>
+  where \<open>mask n = (2 :: int) ^ n - 1\<close>
+
 instance proof
   fix k l :: int and n :: nat
   show \<open>- k = NOT (k - 1)\<close>
@@ -505,7 +515,7 @@
     by (fact bit_or_int_iff)
   show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
     by (fact bit_xor_int_iff)
-qed (simp_all add: bit_not_int_iff)
+qed (simp_all add: bit_not_int_iff mask_int_def)
 
 end
 
@@ -948,17 +958,18 @@
 
 lemma signed_take_bit_code [code]:
   \<open>signed_take_bit n k =
-  (let l = k AND mask (Suc n)
+  (let l = take_bit (Suc n) k
    in if bit l n then l - (push_bit n 2) else l)\<close>
 proof -
-  have *: \<open>(k AND mask (Suc n)) - 2 * 2 ^ n = k AND mask (Suc n) OR NOT (mask (Suc n))\<close>
+  have *: \<open>(take_bit (Suc n) k) - 2 * 2 ^ n = take_bit (Suc n) k OR NOT (mask (Suc n))\<close>
     apply (subst disjunctive_add [symmetric])
-    apply (simp_all add: bit_and_iff bit_mask_iff bit_not_iff)
+    apply (simp_all add: bit_and_iff bit_mask_iff bit_not_iff bit_take_bit_iff)
     apply (simp flip: minus_exp_eq_not_mask)
     done
   show ?thesis
     by (rule bit_eqI)
-     (auto simp add: Let_def bit_and_iff bit_signed_take_bit_iff push_bit_eq_mult min_def not_le bit_mask_iff bit_exp_iff less_Suc_eq * bit_or_iff bit_not_iff)
+     (auto simp add: Let_def bit_and_iff bit_signed_take_bit_iff push_bit_eq_mult min_def not_le
+       bit_mask_iff bit_exp_iff less_Suc_eq * bit_or_iff bit_take_bit_iff bit_not_iff)
 qed
 
 
@@ -976,6 +987,9 @@
 definition xor_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
   where \<open>m XOR n = nat (int m XOR int n)\<close> for m n :: nat
 
+definition mask_nat :: \<open>nat \<Rightarrow> nat\<close>
+  where \<open>mask n = (2 :: nat) ^ n - 1\<close>
+
 instance proof
   fix m n q :: nat
   show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
@@ -984,7 +998,7 @@
     by (auto simp add: or_nat_def bit_or_iff less_le bit_eq_iff)
   show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
     by (auto simp add: xor_nat_def bit_xor_iff less_le bit_eq_iff)
-qed
+qed (simp add: mask_nat_def)
 
 end
 
@@ -1044,22 +1058,19 @@
 lift_definition xor_integer ::  \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
   is xor .
 
-instance proof
-  fix k l :: \<open>integer\<close> and n :: nat
-  show \<open>- k = NOT (k - 1)\<close>
-    by transfer (simp add: minus_eq_not_minus_1)
-  show \<open>bit (NOT k) n \<longleftrightarrow> (2 :: integer) ^ n \<noteq> 0 \<and> \<not> bit k n\<close>
-    by transfer (fact bit_not_iff)
-  show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
-    by transfer (fact bit_and_iff)
-  show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
-    by transfer (fact bit_or_iff)
-  show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
-    by transfer (fact bit_xor_iff)
-qed
+lift_definition mask_integer :: \<open>nat \<Rightarrow> integer\<close>
+  is mask .
+
+instance by (standard; transfer)
+  (simp_all add: minus_eq_not_minus_1 mask_eq_exp_minus_1
+    bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)
 
 end
 
+lemma [code]:
+  \<open>mask n = 2 ^ n - (1::integer)\<close>
+  by (simp add: mask_eq_exp_minus_1)
+
 instantiation natural :: semiring_bit_operations
 begin
 
@@ -1072,18 +1083,18 @@
 lift_definition xor_natural ::  \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
   is xor .
 
-instance proof
-  fix m n :: \<open>natural\<close> and q :: nat
-  show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
-    by transfer (fact bit_and_iff)
-  show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
-    by transfer (fact bit_or_iff)
-  show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
-    by transfer (fact bit_xor_iff)
-qed
+lift_definition mask_natural :: \<open>nat \<Rightarrow> natural\<close>
+  is mask .
+
+instance by (standard; transfer)
+  (simp_all add: mask_eq_exp_minus_1 bit_and_iff bit_or_iff bit_xor_iff)
 
 end
 
+lemma [code]:
+  \<open>integer_of_natural (mask n) = mask n\<close>
+  by transfer (simp add: mask_eq_exp_minus_1 of_nat_diff)
+
 lifting_update integer.lifting
 lifting_forget integer.lifting
 
diff -r 3f8e6c0166ac -r 6a2f43901350 src/HOL/Library/Z2.thy
--- a/src/HOL/Library/Z2.thy	Tue Aug 04 11:45:03 2020 +0100
+++ b/src/HOL/Library/Z2.thy	Wed Aug 05 17:50:00 2020 +0100
@@ -187,6 +187,9 @@
 definition xor_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
   where [simp]: \<open>b XOR c = of_bool (odd b \<noteq> odd c)\<close> for b c :: bit
 
+definition mask_bit :: \<open>nat \<Rightarrow> bit\<close>
+  where [simp]: \<open>mask_bit n = of_bool (n > 0)\<close>
+
 instance
   by standard auto
 
diff -r 3f8e6c0166ac -r 6a2f43901350 src/HOL/Word/Bit_Comprehension.thy
--- a/src/HOL/Word/Bit_Comprehension.thy	Tue Aug 04 11:45:03 2020 +0100
+++ b/src/HOL/Word/Bit_Comprehension.thy	Wed Aug 05 17:50:00 2020 +0100
@@ -32,6 +32,6 @@
   by (simp add: set_bits_int_def)
 
 lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)"
-  by (auto simp add: set_bits_int_def bl_to_bin_def)
+  by (auto simp add: set_bits_int_def)
 
-end
\ No newline at end of file
+end
diff -r 3f8e6c0166ac -r 6a2f43901350 src/HOL/Word/Bit_Lists.thy
--- a/src/HOL/Word/Bit_Lists.thy	Tue Aug 04 11:45:03 2020 +0100
+++ b/src/HOL/Word/Bit_Lists.thy	Wed Aug 05 17:50:00 2020 +0100
@@ -125,15 +125,6 @@
 lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) ((!) (rev xs)) = xs"
   by (simp add: bl_of_nth_nth_le)
 
-lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
-  apply (rule nth_equalityI)
-   apply simp
-  apply (clarsimp simp: nth_takefill rev_nth nth_bin_to_bl bin_nth_of_bl)
-  done
-
-lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
-  by (simp add: takefill_bintrunc)
-
 
 subsection \<open>More\<close>
 
@@ -296,4 +287,671 @@
     rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
   by (induct n) (auto intro!: lth)
 
+
+subsection \<open>Explicit bit representation of \<^typ>\<open>int\<close>\<close>
+
+primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
+  where
+    Nil: "bl_to_bin_aux [] w = w"
+  | Cons: "bl_to_bin_aux (b # bs) w = bl_to_bin_aux bs (of_bool b + 2 * w)"
+
+definition bl_to_bin :: "bool list \<Rightarrow> int"
+  where "bl_to_bin bs = bl_to_bin_aux bs 0"
+
+primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
+  where
+    Z: "bin_to_bl_aux 0 w bl = bl"
+  | Suc: "bin_to_bl_aux (Suc n) w bl = bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
+
+definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
+  where "bin_to_bl n w = bin_to_bl_aux n w []"
+
+lemma bin_to_bl_aux_zero_minus_simp [simp]:
+  "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)"
+  by (cases n) auto
+
+lemma bin_to_bl_aux_minus1_minus_simp [simp]:
+  "0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)"
+  by (cases n) auto
+
+lemma bin_to_bl_aux_one_minus_simp [simp]:
+  "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)"
+  by (cases n) auto
+
+lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
+  "0 < n \<Longrightarrow>
+    bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)"
+  by (cases n) simp_all
+
+lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
+  "0 < n \<Longrightarrow>
+    bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
+  by (cases n) simp_all
+
+lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
+  by (induct bs arbitrary: w) auto
+
+lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
+  by (induct n arbitrary: w bs) auto
+
+lemma bl_to_bin_append: "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
+  unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
+
+lemma bin_to_bl_aux_alt: "bin_to_bl_aux n w bs = bin_to_bl n w @ bs"
+  by (simp add: bin_to_bl_def bin_to_bl_aux_append)
+
+lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
+  by (auto simp: bin_to_bl_def)
+
+lemma size_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
+  by (induct n arbitrary: w bs) auto
+
+lemma size_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
+  by (simp add: bin_to_bl_def size_bin_to_bl_aux)
+
+lemma bl_bin_bl': "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs"
+  apply (induct bs arbitrary: w n)
+   apply auto
+    apply (simp_all only: add_Suc [symmetric])
+    apply (auto simp add: bin_to_bl_def)
+  done
+
+lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
+  unfolding bl_to_bin_def
+  apply (rule box_equals)
+    apply (rule bl_bin_bl')
+   prefer 2
+   apply (rule bin_to_bl_aux.Z)
+  apply simp
+  done
+
+lemma bl_to_bin_inj: "bl_to_bin bs = bl_to_bin cs \<Longrightarrow> length bs = length cs \<Longrightarrow> bs = cs"
+  apply (rule_tac box_equals)
+    defer
+    apply (rule bl_bin_bl)
+   apply (rule bl_bin_bl)
+  apply simp
+  done
+
+lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
+  by (auto simp: bl_to_bin_def)
+
+lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
+  by (auto simp: bl_to_bin_def)
+
+lemma bin_to_bl_zero_aux: "bin_to_bl_aux n 0 bl = replicate n False @ bl"
+  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
+
+lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False"
+  by (simp add: bin_to_bl_def bin_to_bl_zero_aux)
+
+lemma bin_to_bl_minus1_aux: "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
+  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
+
+lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
+  by (simp add: bin_to_bl_def bin_to_bl_minus1_aux)
+
+
+subsection \<open>Semantic interpretation of \<^typ>\<open>bool list\<close> as \<^typ>\<open>int\<close>\<close>
+
+lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (bintrunc n w)"
+  by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def take_bit_Suc ac_simps mod_2_eq_odd)
+
+lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
+  by (auto simp: bin_to_bl_def bin_bl_bin')
+
+lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
+  by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def)
+
+lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
+  by (auto intro: bl_to_bin_inj)
+
+lemma bin_to_bl_aux_bintr:
+  "bin_to_bl_aux n (bintrunc m bin) bl =
+    replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
+  apply (induct n arbitrary: m bin bl)
+   apply clarsimp
+  apply clarsimp
+  apply (case_tac "m")
+   apply (clarsimp simp: bin_to_bl_zero_aux)
+   apply (erule thin_rl)
+   apply (induct_tac n)
+    apply (auto simp add: take_bit_Suc)
+  done
+
+lemma bin_to_bl_bintr:
+  "bin_to_bl n (bintrunc m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin"
+  unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
+
+lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
+  by (induct n) auto
+
+lemma len_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
+  by (fact size_bin_to_bl_aux)
+
+lemma len_bin_to_bl: "length (bin_to_bl n w) = n"
+  by (fact size_bin_to_bl) (* FIXME: duplicate *)
+
+lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
+  by (induction bs arbitrary: w) (simp_all add: bin_sign_def)
+
+lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
+  by (simp add: bl_to_bin_def sign_bl_bin')
+
+lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (sbintrunc n w) = -1)"
+  by (induction n arbitrary: w bs) (auto simp add: bin_sign_def even_iff_mod_2_eq_zero bit_Suc)
+
+lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
+  unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
+
+lemma bin_nth_of_bl_aux:
+  "bin_nth (bl_to_bin_aux bl w) n =
+    (n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bin_nth w (n - size bl))"
+  apply (induction bl arbitrary: w)
+   apply simp_all
+  apply safe
+                      apply (simp_all add: not_le nth_append bit_double_iff even_bit_succ_iff split: if_splits)
+  done
+
+lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)"
+  by (simp add: bl_to_bin_def bin_nth_of_bl_aux)
+
+lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
+  apply (induct n arbitrary: m w)
+   apply clarsimp
+   apply (case_tac m, clarsimp)
+   apply (clarsimp simp: bin_to_bl_def)
+   apply (simp add: bin_to_bl_aux_alt)
+  apply (case_tac m, clarsimp)
+  apply (clarsimp simp: bin_to_bl_def)
+  apply (simp add: bin_to_bl_aux_alt bit_Suc)
+  done
+
+lemma nth_bin_to_bl_aux:
+  "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
+    (if n < m then bit w (m - 1 - n) else bl ! (n - m))"
+  apply (induction bl arbitrary: w)
+   apply simp_all
+   apply (simp add: bin_nth_bl [of \<open>m - Suc n\<close> m] rev_nth flip: bin_to_bl_def)
+   apply (metis One_nat_def Suc_pred add_diff_cancel_left'
+     add_diff_cancel_right' bin_to_bl_aux_alt bin_to_bl_def
+     diff_Suc_Suc diff_is_0_eq diff_zero less_Suc_eq_0_disj
+     less_antisym less_imp_Suc_add list.size(3) nat_less_le nth_append size_bin_to_bl_aux)
+  done
+
+lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
+  by (simp add: bin_to_bl_def nth_bin_to_bl_aux)
+
+lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
+  apply (rule nth_equalityI)
+   apply simp
+  apply (clarsimp simp: nth_takefill rev_nth nth_bin_to_bl bin_nth_of_bl)
+  done
+
+lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
+  by (simp add: takefill_bintrunc)
+
+lemma bl_to_bin_lt2p_aux: "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
+proof (induction bs arbitrary: w)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons b bs)
+  from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
+  show ?case
+    apply (auto simp add: algebra_simps)
+    apply (subst mult_2 [of \<open>2 ^ length bs\<close>])
+    apply (simp only: add.assoc)
+    apply (rule pos_add_strict)
+     apply simp_all
+    done
+qed
+
+lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
+proof (induct bs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons b bs)
+  with bl_to_bin_lt2p_aux[where w=1] show ?case
+    by (simp add: bl_to_bin_def)
+qed
+
+lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
+  by (metis bin_bl_bin bintr_lt2p bl_bin_bl)
+
+lemma bl_to_bin_ge2p_aux: "bl_to_bin_aux bs w \<ge> w * (2 ^ length bs)"
+proof (induction bs arbitrary: w)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons b bs)
+  from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
+  show ?case
+    apply (auto simp add: algebra_simps)
+    apply (rule add_le_imp_le_left [of \<open>2 ^ length bs\<close>])
+    apply (rule add_increasing)
+    apply simp_all
+    done
+qed
+
+lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0"
+  apply (unfold bl_to_bin_def)
+  apply (rule xtrans(4))
+   apply (rule bl_to_bin_ge2p_aux)
+  apply simp
+  done
+
+lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
+  apply (unfold bin_to_bl_def)
+  apply (cases n, clarsimp)
+  apply clarsimp
+  apply (auto simp add: bin_to_bl_aux_alt)
+  done
+
+lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
+  using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
+
+lemma butlast_rest_bl2bin_aux:
+  "bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
+  by (induct bl arbitrary: w) auto
+
+lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
+  by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux)
+
+lemma trunc_bl2bin_aux:
+  "bintrunc m (bl_to_bin_aux bl w) =
+    bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
+proof (induct bl arbitrary: w)
+  case Nil
+  show ?case by simp
+next
+  case (Cons b bl)
+  show ?case
+  proof (cases "m - length bl")
+    case 0
+    then have "Suc (length bl) - m = Suc (length bl - m)" by simp
+    with Cons show ?thesis by simp
+  next
+    case (Suc n)
+    then have "m - Suc (length bl) = n" by simp
+    with Cons Suc show ?thesis by (simp add: take_bit_Suc ac_simps)
+  qed
+qed
+
+lemma trunc_bl2bin: "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
+  by (simp add: bl_to_bin_def trunc_bl2bin_aux)
+
+lemma trunc_bl2bin_len [simp]: "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
+  by (simp add: trunc_bl2bin)
+
+lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
+  apply (rule trans)
+   prefer 2
+   apply (rule trunc_bl2bin [symmetric])
+  apply (cases "k \<le> length bl")
+   apply auto
+  done
+
+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)"
+  apply (rule nth_equalityI)
+   apply simp
+  apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
+  done
+
+lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)"
+  by (induct xs arbitrary: w) auto
+
+lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)"
+  unfolding bl_to_bin_def by (erule last_bin_last')
+
+lemma bin_last_last: "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)"
+  by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)
+
+lemma drop_bin2bl_aux:
+  "drop m (bin_to_bl_aux n bin bs) =
+    bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
+  apply (induction n arbitrary: m bin bs)
+   apply auto
+  apply (case_tac "m \<le> n")
+   apply (auto simp add: not_le Suc_diff_le)
+  apply (case_tac "m - n")
+   apply auto
+  apply (use Suc_diff_Suc in fastforce)
+  done
+
+lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
+  by (simp add: bin_to_bl_def drop_bin2bl_aux)
+
+lemma take_bin2bl_lem1: "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
+  apply (induct m arbitrary: w bs)
+   apply clarsimp
+  apply clarsimp
+  apply (simp add: bin_to_bl_aux_alt)
+  apply (simp add: bin_to_bl_def)
+  apply (simp add: bin_to_bl_aux_alt)
+  done
+
+lemma take_bin2bl_lem: "take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)"
+  by (induct n arbitrary: w bs) (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1, simp)
+
+lemma bin_split_take: "bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)"
+  apply (induct n arbitrary: b c)
+   apply clarsimp
+  apply (clarsimp simp: Let_def split: prod.split_asm)
+  apply (simp add: bin_to_bl_def)
+  apply (simp add: take_bin2bl_lem drop_bit_Suc)
+  done
+
+lemma bin_to_bl_drop_bit:
+  "k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c)"
+  using bin_split_take by simp
+
+lemma bin_split_take1:
+  "k = m + n \<Longrightarrow> bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)"
+  using bin_split_take by simp
+
+lemma bl_bin_bl_rep_drop:
+  "bin_to_bl n (bl_to_bin bl) =
+    replicate (n - length bl) False @ drop (length bl - n) bl"
+  by (simp add: bl_to_bin_inj bl_to_bin_rep_F trunc_bl2bin)
+
+lemma bl_to_bin_aux_cat:
+  "bl_to_bin_aux bs (bin_cat w nv v) =
+    bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
+  by (rule bit_eqI)
+    (auto simp add: bin_nth_of_bl_aux bin_nth_cat algebra_simps)
+
+lemma bin_to_bl_aux_cat:
+  "bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
+    bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
+  by (induction nw arbitrary: w bs) (simp_all add: concat_bit_Suc)
+
+lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
+  using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
+  by (simp add: bl_to_bin_def [symmetric])
+
+lemma bin_to_bl_cat:
+  "bin_to_bl (nv + nw) (bin_cat v nw w) =
+    bin_to_bl_aux nv v (bin_to_bl nw w)"
+  by (simp add: bin_to_bl_def bin_to_bl_aux_cat)
+
+lemmas bl_to_bin_aux_app_cat =
+  trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
+
+lemmas bin_to_bl_aux_cat_app =
+  trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
+
+lemma bl_to_bin_app_cat:
+  "bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)"
+  by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)
+
+lemma bin_to_bl_cat_app:
+  "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
+  by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
+
+text \<open>\<open>bl_to_bin_app_cat_alt\<close> and \<open>bl_to_bin_app_cat\<close> are easily interderivable.\<close>
+lemma bl_to_bin_app_cat_alt: "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
+  by (simp add: bl_to_bin_app_cat)
+
+lemma mask_lem: "(bl_to_bin (True # replicate n False)) = bl_to_bin (replicate n True) + 1"
+  apply (unfold bl_to_bin_def)
+  apply (induct n)
+   apply simp
+  apply (simp only: Suc_eq_plus1 replicate_add append_Cons [symmetric] bl_to_bin_aux_append)
+  apply simp
+  done
+
+lemma bin_exhaust:
+  "(\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q) \<Longrightarrow> Q" for bin :: int
+  apply (cases \<open>even bin\<close>)
+   apply (auto elim!: evenE oddE)
+   apply fastforce
+  apply fastforce
+  done
+
+primrec rbl_succ :: "bool list \<Rightarrow> bool list"
+  where
+    Nil: "rbl_succ Nil = Nil"
+  | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
+
+primrec rbl_pred :: "bool list \<Rightarrow> bool list"
+  where
+    Nil: "rbl_pred Nil = Nil"
+  | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
+
+primrec rbl_add :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
+  where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
+    Nil: "rbl_add Nil x = Nil"
+  | Cons: "rbl_add (y # ys) x =
+      (let ws = rbl_add ys (tl x)
+       in (y \<noteq> hd x) # (if hd x \<and> y then rbl_succ ws else ws))"
+
+primrec rbl_mult :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
+  where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
+    Nil: "rbl_mult Nil x = Nil"
+  | Cons: "rbl_mult (y # ys) x =
+      (let ws = False # rbl_mult ys x
+       in if y then rbl_add ws x else ws)"
+
+lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
+  by (induct bl) auto
+
+lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
+  by (induct bl) auto
+
+lemma size_rbl_add: "length (rbl_add bl cl) = length bl"
+  by (induct bl arbitrary: cl) (auto simp: Let_def size_rbl_succ)
+
+lemma size_rbl_mult: "length (rbl_mult bl cl) = length bl"
+  by (induct bl arbitrary: cl) (auto simp add: Let_def size_rbl_add)
+
+lemmas rbl_sizes [simp] =
+  size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
+
+lemmas rbl_Nils =
+  rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
+
+lemma rbl_add_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb"
+  apply (induct bla arbitrary: blb)
+   apply simp
+  apply clarsimp
+  apply (case_tac blb, clarsimp)
+  apply (clarsimp simp: Let_def)
+  done
+
+lemma rbl_add_take2:
+  "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
+  apply (induct bla arbitrary: blb)
+   apply simp
+  apply clarsimp
+  apply (case_tac blb, clarsimp)
+  apply (clarsimp simp: Let_def)
+  done
+
+lemma rbl_mult_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb"
+  apply (induct bla arbitrary: blb)
+   apply simp
+  apply clarsimp
+  apply (case_tac blb, clarsimp)
+  apply (clarsimp simp: Let_def rbl_add_app2)
+  done
+
+lemma rbl_mult_take2:
+  "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
+  apply (rule trans)
+   apply (rule rbl_mult_app2 [symmetric])
+   apply simp
+  apply (rule_tac f = "rbl_mult bla" in arg_cong)
+  apply (rule append_take_drop_id)
+  done
+
+lemma rbl_add_split:
+  "P (rbl_add (y # ys) (x # xs)) =
+    (\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow>
+      (y \<longrightarrow> ((x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws)))) \<and>
+      (\<not> y \<longrightarrow> P (x # ws)))"
+  by (cases y) (auto simp: Let_def)
+
+lemma rbl_mult_split:
+  "P (rbl_mult (y # ys) xs) =
+    (\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow>
+      (y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))"
+  by (auto simp: Let_def)
+
+lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
+proof (unfold bin_to_bl_def, induction n arbitrary: bin)
+  case 0
+  then show ?case
+    by simp
+next
+  case (Suc n)
+  obtain b k where \<open>bin = of_bool b + 2 * k\<close>
+    using bin_exhaust by blast
+  moreover have \<open>(2 * k - 1) div 2 = k - 1\<close>
+    using even_succ_div_2 [of \<open>2 * (k - 1)\<close>] 
+    by simp
+  ultimately show ?case
+    using Suc [of \<open>bin div 2\<close>]
+    by simp (simp add: bin_to_bl_aux_alt)
+qed
+
+lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
+  apply (unfold bin_to_bl_def)
+  apply (induction n arbitrary: bin)
+   apply simp_all
+  apply (case_tac bin rule: bin_exhaust)
+  apply simp
+  apply (simp add: bin_to_bl_aux_alt ac_simps)
+  done
+
+lemma rbl_add:
+  "\<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
+    rev (bin_to_bl n (bina + binb))"
+  apply (unfold bin_to_bl_def)
+  apply (induct n)
+   apply simp
+  apply clarsimp
+  apply (case_tac bina rule: bin_exhaust)
+  apply (case_tac binb rule: bin_exhaust)
+  apply (case_tac b)
+   apply (case_tac [!] "ba")
+     apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
+  done
+
+lemma rbl_add_long:
+  "m \<ge> n \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
+    rev (bin_to_bl n (bina + binb))"
+  apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
+   apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
+   apply (rule rev_swap [THEN iffD1])
+   apply (simp add: rev_take drop_bin2bl)
+  apply simp
+  done
+
+lemma rbl_mult_gt1:
+  "m \<ge> length bl \<Longrightarrow>
+    rbl_mult bl (rev (bin_to_bl m binb)) =
+    rbl_mult bl (rev (bin_to_bl (length bl) binb))"
+  apply (rule trans)
+   apply (rule rbl_mult_take2 [symmetric])
+   apply simp_all
+  apply (rule_tac f = "rbl_mult bl" in arg_cong)
+  apply (rule rev_swap [THEN iffD1])
+  apply (simp add: rev_take drop_bin2bl)
+  done
+
+lemma rbl_mult_gt:
+  "m > n \<Longrightarrow>
+    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
+    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
+  by (auto intro: trans [OF rbl_mult_gt1])
+
+lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
+
+lemma rbbl_Cons: "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (of_bool b + 2 * x))"
+  by (simp add: bin_to_bl_def) (simp add: bin_to_bl_aux_alt)
+
+lemma rbl_mult:
+  "rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
+    rev (bin_to_bl n (bina * binb))"
+  apply (induct n arbitrary: bina binb)
+   apply simp_all
+  apply (unfold bin_to_bl_def)
+  apply clarsimp
+  apply (case_tac bina rule: bin_exhaust)
+  apply (case_tac binb rule: bin_exhaust)
+  apply simp
+  apply (simp add: bin_to_bl_aux_alt)
+  apply (simp add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps)
+  done
+
+lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n"
+  by (induct xs) auto
+
+lemma bin_cat_foldl_lem:
+  "foldl (\<lambda>u. bin_cat u n) x xs =
+    bin_cat x (size xs * n) (foldl (\<lambda>u. bin_cat u n) y xs)"
+  apply (induct xs arbitrary: x)
+   apply simp
+  apply (simp (no_asm))
+  apply (frule asm_rl)
+  apply (drule meta_spec)
+  apply (erule trans)
+  apply (drule_tac x = "bin_cat y n a" in meta_spec)
+  apply (simp add: bin_cat_assoc_sym min.absorb2)
+  done
+
+lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))"
+  apply (unfold bin_rcat_def)
+  apply (rule sym)
+  apply (induct wl)
+   apply (auto simp add: bl_to_bin_append)
+  apply (simp add: bl_to_bin_aux_alt sclem)
+  apply (simp add: bin_cat_foldl_lem [symmetric])
+  done
+
+lemma bin_last_bl_to_bin: "bin_last (bl_to_bin bs) \<longleftrightarrow> bs \<noteq> [] \<and> last bs"
+by(cases "bs = []")(auto simp add: bl_to_bin_def last_bin_last'[where w=0])
+
+lemma bin_rest_bl_to_bin: "bin_rest (bl_to_bin bs) = bl_to_bin (butlast bs)"
+by(cases "bs = []")(simp_all add: bl_to_bin_def butlast_rest_bl2bin_aux)
+
+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 (induction n arbitrary: v w bs cs)
+   apply auto
+  apply (case_tac v rule: bin_exhaust)
+  apply (case_tac w rule: bin_exhaust)
+  apply clarsimp
+  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)"
+  by (induct n arbitrary: v w bs cs) simp_all
+
+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)"
+  by (induction n arbitrary: v w bs cs) simp_all
+
+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 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
+  using bl_xor_aux_bin by (simp add: bin_to_bl_def)
+
 end
diff -r 3f8e6c0166ac -r 6a2f43901350 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Tue Aug 04 11:45:03 2020 +0100
+++ b/src/HOL/Word/Bits_Int.thy	Wed Aug 05 17:50:00 2020 +0100
@@ -63,110 +63,6 @@
   by auto
 
 
-subsection \<open>Explicit bit representation of \<^typ>\<open>int\<close>\<close>
-
-primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
-  where
-    Nil: "bl_to_bin_aux [] w = w"
-  | Cons: "bl_to_bin_aux (b # bs) w = bl_to_bin_aux bs (of_bool b + 2 * w)"
-
-definition bl_to_bin :: "bool list \<Rightarrow> int"
-  where "bl_to_bin bs = bl_to_bin_aux bs 0"
-
-primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
-  where
-    Z: "bin_to_bl_aux 0 w bl = bl"
-  | Suc: "bin_to_bl_aux (Suc n) w bl = bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
-
-definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
-  where "bin_to_bl n w = bin_to_bl_aux n w []"
-
-lemma bin_to_bl_aux_zero_minus_simp [simp]:
-  "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)"
-  by (cases n) auto
-
-lemma bin_to_bl_aux_minus1_minus_simp [simp]:
-  "0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)"
-  by (cases n) auto
-
-lemma bin_to_bl_aux_one_minus_simp [simp]:
-  "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)"
-  by (cases n) auto
-
-lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
-  "0 < n \<Longrightarrow>
-    bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)"
-  by (cases n) simp_all
-
-lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
-  "0 < n \<Longrightarrow>
-    bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
-  by (cases n) simp_all
-
-lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
-  by (induct bs arbitrary: w) auto
-
-lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
-  by (induct n arbitrary: w bs) auto
-
-lemma bl_to_bin_append: "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
-  unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
-
-lemma bin_to_bl_aux_alt: "bin_to_bl_aux n w bs = bin_to_bl n w @ bs"
-  by (simp add: bin_to_bl_def bin_to_bl_aux_append)
-
-lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
-  by (auto simp: bin_to_bl_def)
-
-lemma size_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
-  by (induct n arbitrary: w bs) auto
-
-lemma size_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
-  by (simp add: bin_to_bl_def size_bin_to_bl_aux)
-
-lemma bl_bin_bl': "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs"
-  apply (induct bs arbitrary: w n)
-   apply auto
-    apply (simp_all only: add_Suc [symmetric])
-    apply (auto simp add: bin_to_bl_def)
-  done
-
-lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
-  unfolding bl_to_bin_def
-  apply (rule box_equals)
-    apply (rule bl_bin_bl')
-   prefer 2
-   apply (rule bin_to_bl_aux.Z)
-  apply simp
-  done
-
-lemma bl_to_bin_inj: "bl_to_bin bs = bl_to_bin cs \<Longrightarrow> length bs = length cs \<Longrightarrow> bs = cs"
-  apply (rule_tac box_equals)
-    defer
-    apply (rule bl_bin_bl)
-   apply (rule bl_bin_bl)
-  apply simp
-  done
-
-lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
-  by (auto simp: bl_to_bin_def)
-
-lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
-  by (auto simp: bl_to_bin_def)
-
-lemma bin_to_bl_zero_aux: "bin_to_bl_aux n 0 bl = replicate n False @ bl"
-  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
-
-lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False"
-  by (simp add: bin_to_bl_def bin_to_bl_zero_aux)
-
-lemma bin_to_bl_minus1_aux: "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
-  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
-
-lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
-  by (simp add: bin_to_bl_def bin_to_bl_minus1_aux)
-
-
 subsection \<open>Bit projection\<close>
 
 abbreviation (input) bin_nth :: \<open>int \<Rightarrow> nat \<Rightarrow> bool\<close>
@@ -1640,558 +1536,4 @@
   "bin_sc n True i = i OR (1 << n)"
   by (induct n arbitrary: i) (rule bin_rl_eqI; simp)+
 
-
-subsection \<open>Semantic interpretation of \<^typ>\<open>bool list\<close> as \<^typ>\<open>int\<close>\<close>
-
-lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (bintrunc n w)"
-  by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def take_bit_Suc ac_simps mod_2_eq_odd)
-
-lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
-  by (auto simp: bin_to_bl_def bin_bl_bin')
-
-lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
-  by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def)
-
-lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
-  by (auto intro: bl_to_bin_inj)
-
-lemma bin_to_bl_aux_bintr:
-  "bin_to_bl_aux n (bintrunc m bin) bl =
-    replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
-  apply (induct n arbitrary: m bin bl)
-   apply clarsimp
-  apply clarsimp
-  apply (case_tac "m")
-   apply (clarsimp simp: bin_to_bl_zero_aux)
-   apply (erule thin_rl)
-   apply (induct_tac n)
-    apply (auto simp add: take_bit_Suc)
-  done
-
-lemma bin_to_bl_bintr:
-  "bin_to_bl n (bintrunc m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin"
-  unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
-
-lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
-  by (induct n) auto
-
-lemma len_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
-  by (fact size_bin_to_bl_aux)
-
-lemma len_bin_to_bl: "length (bin_to_bl n w) = n"
-  by (fact size_bin_to_bl) (* FIXME: duplicate *)
-
-lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
-  by (induction bs arbitrary: w) (simp_all add: bin_sign_def)
-
-lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
-  by (simp add: bl_to_bin_def sign_bl_bin')
-
-lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (sbintrunc n w) = -1)"
-  by (induction n arbitrary: w bs) (auto simp add: bin_sign_def even_iff_mod_2_eq_zero bit_Suc)
-
-lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
-  unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
-
-lemma bin_nth_of_bl_aux:
-  "bin_nth (bl_to_bin_aux bl w) n =
-    (n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bin_nth w (n - size bl))"
-  apply (induction bl arbitrary: w)
-   apply simp_all
-  apply safe
-                      apply (simp_all add: not_le nth_append bit_double_iff even_bit_succ_iff split: if_splits)
-  done
-
-lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)"
-  by (simp add: bl_to_bin_def bin_nth_of_bl_aux)
-
-lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
-  apply (induct n arbitrary: m w)
-   apply clarsimp
-   apply (case_tac m, clarsimp)
-   apply (clarsimp simp: bin_to_bl_def)
-   apply (simp add: bin_to_bl_aux_alt)
-  apply (case_tac m, clarsimp)
-  apply (clarsimp simp: bin_to_bl_def)
-  apply (simp add: bin_to_bl_aux_alt bit_Suc)
-  done
-
-lemma nth_bin_to_bl_aux:
-  "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
-    (if n < m then bit w (m - 1 - n) else bl ! (n - m))"
-  apply (induction bl arbitrary: w)
-   apply simp_all
-   apply (simp add: bin_nth_bl [of \<open>m - Suc n\<close> m] rev_nth flip: bin_to_bl_def)
-   apply (metis One_nat_def Suc_pred add_diff_cancel_left'
-     add_diff_cancel_right' bin_to_bl_aux_alt bin_to_bl_def
-     diff_Suc_Suc diff_is_0_eq diff_zero less_Suc_eq_0_disj
-     less_antisym less_imp_Suc_add list.size(3) nat_less_le nth_append size_bin_to_bl_aux)
-  done
-
-lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
-  by (simp add: bin_to_bl_def nth_bin_to_bl_aux)
-
-lemma bl_to_bin_lt2p_aux: "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
-proof (induction bs arbitrary: w)
-  case Nil
-  then show ?case
-    by simp
-next
-  case (Cons b bs)
-  from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
-  show ?case
-    apply (auto simp add: algebra_simps)
-    apply (subst mult_2 [of \<open>2 ^ length bs\<close>])
-    apply (simp only: add.assoc)
-    apply (rule pos_add_strict)
-     apply simp_all
-    done
-qed
-
-lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
-proof (induct bs)
-  case Nil
-  then show ?case by simp
-next
-  case (Cons b bs)
-  with bl_to_bin_lt2p_aux[where w=1] show ?case
-    by (simp add: bl_to_bin_def)
-qed
-
-lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
-  by (metis bin_bl_bin bintr_lt2p bl_bin_bl)
-
-lemma bl_to_bin_ge2p_aux: "bl_to_bin_aux bs w \<ge> w * (2 ^ length bs)"
-proof (induction bs arbitrary: w)
-  case Nil
-  then show ?case
-    by simp
-next
-  case (Cons b bs)
-  from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
-  show ?case
-    apply (auto simp add: algebra_simps)
-    apply (rule add_le_imp_le_left [of \<open>2 ^ length bs\<close>])
-    apply (rule add_increasing)
-    apply simp_all
-    done
-qed
-
-lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0"
-  apply (unfold bl_to_bin_def)
-  apply (rule xtrans(4))
-   apply (rule bl_to_bin_ge2p_aux)
-  apply simp
-  done
-
-lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
-  apply (unfold bin_to_bl_def)
-  apply (cases n, clarsimp)
-  apply clarsimp
-  apply (auto simp add: bin_to_bl_aux_alt)
-  done
-
-lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
-  using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
-
-lemma butlast_rest_bl2bin_aux:
-  "bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
-  by (induct bl arbitrary: w) auto
-
-lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
-  by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux)
-
-lemma trunc_bl2bin_aux:
-  "bintrunc m (bl_to_bin_aux bl w) =
-    bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
-proof (induct bl arbitrary: w)
-  case Nil
-  show ?case by simp
-next
-  case (Cons b bl)
-  show ?case
-  proof (cases "m - length bl")
-    case 0
-    then have "Suc (length bl) - m = Suc (length bl - m)" by simp
-    with Cons show ?thesis by simp
-  next
-    case (Suc n)
-    then have "m - Suc (length bl) = n" by simp
-    with Cons Suc show ?thesis by (simp add: take_bit_Suc ac_simps)
-  qed
-qed
-
-lemma trunc_bl2bin: "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
-  by (simp add: bl_to_bin_def trunc_bl2bin_aux)
-
-lemma trunc_bl2bin_len [simp]: "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
-  by (simp add: trunc_bl2bin)
-
-lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
-  apply (rule trans)
-   prefer 2
-   apply (rule trunc_bl2bin [symmetric])
-  apply (cases "k \<le> length bl")
-   apply auto
-  done
-
-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)"
-  apply (rule nth_equalityI)
-   apply simp
-  apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
-  done
-
-lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)"
-  by (induct xs arbitrary: w) auto
-
-lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)"
-  unfolding bl_to_bin_def by (erule last_bin_last')
-
-lemma bin_last_last: "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)"
-  by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)
-
-lemma drop_bin2bl_aux:
-  "drop m (bin_to_bl_aux n bin bs) =
-    bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
-  apply (induction n arbitrary: m bin bs)
-   apply auto
-  apply (case_tac "m \<le> n")
-   apply (auto simp add: not_le Suc_diff_le)
-  apply (case_tac "m - n")
-   apply auto
-  apply (use Suc_diff_Suc in fastforce)
-  done
-
-lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
-  by (simp add: bin_to_bl_def drop_bin2bl_aux)
-
-lemma take_bin2bl_lem1: "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
-  apply (induct m arbitrary: w bs)
-   apply clarsimp
-  apply clarsimp
-  apply (simp add: bin_to_bl_aux_alt)
-  apply (simp add: bin_to_bl_def)
-  apply (simp add: bin_to_bl_aux_alt)
-  done
-
-lemma take_bin2bl_lem: "take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)"
-  by (induct n arbitrary: w bs) (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1, simp)
-
-lemma bin_split_take: "bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)"
-  apply (induct n arbitrary: b c)
-   apply clarsimp
-  apply (clarsimp simp: Let_def split: prod.split_asm)
-  apply (simp add: bin_to_bl_def)
-  apply (simp add: take_bin2bl_lem drop_bit_Suc)
-  done
-
-lemma bin_to_bl_drop_bit:
-  "k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c)"
-  using bin_split_take by simp
-
-lemma bin_split_take1:
-  "k = m + n \<Longrightarrow> bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)"
-  using bin_split_take by simp
-
-lemma bl_bin_bl_rep_drop:
-  "bin_to_bl n (bl_to_bin bl) =
-    replicate (n - length bl) False @ drop (length bl - n) bl"
-  by (simp add: bl_to_bin_inj bl_to_bin_rep_F trunc_bl2bin)
-
-lemma bl_to_bin_aux_cat:
-  "bl_to_bin_aux bs (bin_cat w nv v) =
-    bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
-  by (rule bit_eqI)
-    (auto simp add: bin_nth_of_bl_aux bin_nth_cat algebra_simps)
-
-lemma bin_to_bl_aux_cat:
-  "bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
-    bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
-  by (induction nw arbitrary: w bs) (simp_all add: concat_bit_Suc)
-
-lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
-  using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
-  by (simp add: bl_to_bin_def [symmetric])
-
-lemma bin_to_bl_cat:
-  "bin_to_bl (nv + nw) (bin_cat v nw w) =
-    bin_to_bl_aux nv v (bin_to_bl nw w)"
-  by (simp add: bin_to_bl_def bin_to_bl_aux_cat)
-
-lemmas bl_to_bin_aux_app_cat =
-  trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
-
-lemmas bin_to_bl_aux_cat_app =
-  trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
-
-lemma bl_to_bin_app_cat:
-  "bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)"
-  by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)
-
-lemma bin_to_bl_cat_app:
-  "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
-  by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
-
-text \<open>\<open>bl_to_bin_app_cat_alt\<close> and \<open>bl_to_bin_app_cat\<close> are easily interderivable.\<close>
-lemma bl_to_bin_app_cat_alt: "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
-  by (simp add: bl_to_bin_app_cat)
-
-lemma mask_lem: "(bl_to_bin (True # replicate n False)) = bl_to_bin (replicate n True) + 1"
-  apply (unfold bl_to_bin_def)
-  apply (induct n)
-   apply simp
-  apply (simp only: Suc_eq_plus1 replicate_add append_Cons [symmetric] bl_to_bin_aux_append)
-  apply simp
-  done
-
-lemma bin_exhaust:
-  "(\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q) \<Longrightarrow> Q" for bin :: int
-  apply (cases \<open>even bin\<close>)
-   apply (auto elim!: evenE oddE)
-   apply fastforce
-  apply fastforce
-  done
-
-primrec rbl_succ :: "bool list \<Rightarrow> bool list"
-  where
-    Nil: "rbl_succ Nil = Nil"
-  | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
-
-primrec rbl_pred :: "bool list \<Rightarrow> bool list"
-  where
-    Nil: "rbl_pred Nil = Nil"
-  | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
-
-primrec rbl_add :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
-  where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
-    Nil: "rbl_add Nil x = Nil"
-  | Cons: "rbl_add (y # ys) x =
-      (let ws = rbl_add ys (tl x)
-       in (y \<noteq> hd x) # (if hd x \<and> y then rbl_succ ws else ws))"
-
-primrec rbl_mult :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
-  where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
-    Nil: "rbl_mult Nil x = Nil"
-  | Cons: "rbl_mult (y # ys) x =
-      (let ws = False # rbl_mult ys x
-       in if y then rbl_add ws x else ws)"
-
-lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
-  by (induct bl) auto
-
-lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
-  by (induct bl) auto
-
-lemma size_rbl_add: "length (rbl_add bl cl) = length bl"
-  by (induct bl arbitrary: cl) (auto simp: Let_def size_rbl_succ)
-
-lemma size_rbl_mult: "length (rbl_mult bl cl) = length bl"
-  by (induct bl arbitrary: cl) (auto simp add: Let_def size_rbl_add)
-
-lemmas rbl_sizes [simp] =
-  size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
-
-lemmas rbl_Nils =
-  rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
-
-lemma rbl_add_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb"
-  apply (induct bla arbitrary: blb)
-   apply simp
-  apply clarsimp
-  apply (case_tac blb, clarsimp)
-  apply (clarsimp simp: Let_def)
-  done
-
-lemma rbl_add_take2:
-  "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
-  apply (induct bla arbitrary: blb)
-   apply simp
-  apply clarsimp
-  apply (case_tac blb, clarsimp)
-  apply (clarsimp simp: Let_def)
-  done
-
-lemma rbl_mult_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb"
-  apply (induct bla arbitrary: blb)
-   apply simp
-  apply clarsimp
-  apply (case_tac blb, clarsimp)
-  apply (clarsimp simp: Let_def rbl_add_app2)
-  done
-
-lemma rbl_mult_take2:
-  "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
-  apply (rule trans)
-   apply (rule rbl_mult_app2 [symmetric])
-   apply simp
-  apply (rule_tac f = "rbl_mult bla" in arg_cong)
-  apply (rule append_take_drop_id)
-  done
-
-lemma rbl_add_split:
-  "P (rbl_add (y # ys) (x # xs)) =
-    (\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow>
-      (y \<longrightarrow> ((x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws)))) \<and>
-      (\<not> y \<longrightarrow> P (x # ws)))"
-  by (cases y) (auto simp: Let_def)
-
-lemma rbl_mult_split:
-  "P (rbl_mult (y # ys) xs) =
-    (\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow>
-      (y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))"
-  by (auto simp: Let_def)
-
-lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
-proof (unfold bin_to_bl_def, induction n arbitrary: bin)
-  case 0
-  then show ?case
-    by simp
-next
-  case (Suc n)
-  obtain b k where \<open>bin = of_bool b + 2 * k\<close>
-    using bin_exhaust by blast
-  moreover have \<open>(2 * k - 1) div 2 = k - 1\<close>
-    using even_succ_div_2 [of \<open>2 * (k - 1)\<close>] 
-    by simp
-  ultimately show ?case
-    using Suc [of \<open>bin div 2\<close>]
-    by simp (simp add: bin_to_bl_aux_alt)
-qed
-
-lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
-  apply (unfold bin_to_bl_def)
-  apply (induction n arbitrary: bin)
-   apply simp_all
-  apply (case_tac bin rule: bin_exhaust)
-  apply simp
-  apply (simp add: bin_to_bl_aux_alt ac_simps)
-  done
-
-lemma rbl_add:
-  "\<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
-    rev (bin_to_bl n (bina + binb))"
-  apply (unfold bin_to_bl_def)
-  apply (induct n)
-   apply simp
-  apply clarsimp
-  apply (case_tac bina rule: bin_exhaust)
-  apply (case_tac binb rule: bin_exhaust)
-  apply (case_tac b)
-   apply (case_tac [!] "ba")
-     apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
-  done
-
-lemma rbl_add_long:
-  "m \<ge> n \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
-    rev (bin_to_bl n (bina + binb))"
-  apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
-   apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
-   apply (rule rev_swap [THEN iffD1])
-   apply (simp add: rev_take drop_bin2bl)
-  apply simp
-  done
-
-lemma rbl_mult_gt1:
-  "m \<ge> length bl \<Longrightarrow>
-    rbl_mult bl (rev (bin_to_bl m binb)) =
-    rbl_mult bl (rev (bin_to_bl (length bl) binb))"
-  apply (rule trans)
-   apply (rule rbl_mult_take2 [symmetric])
-   apply simp_all
-  apply (rule_tac f = "rbl_mult bl" in arg_cong)
-  apply (rule rev_swap [THEN iffD1])
-  apply (simp add: rev_take drop_bin2bl)
-  done
-
-lemma rbl_mult_gt:
-  "m > n \<Longrightarrow>
-    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
-    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
-  by (auto intro: trans [OF rbl_mult_gt1])
-
-lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
-
-lemma rbbl_Cons: "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (of_bool b + 2 * x))"
-  by (simp add: bin_to_bl_def) (simp add: bin_to_bl_aux_alt)
-
-lemma rbl_mult:
-  "rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
-    rev (bin_to_bl n (bina * binb))"
-  apply (induct n arbitrary: bina binb)
-   apply simp_all
-  apply (unfold bin_to_bl_def)
-  apply clarsimp
-  apply (case_tac bina rule: bin_exhaust)
-  apply (case_tac binb rule: bin_exhaust)
-  apply simp
-  apply (simp add: bin_to_bl_aux_alt)
-  apply (simp add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps)
-  done
-
-lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n"
-  by (induct xs) auto
-
-lemma bin_cat_foldl_lem:
-  "foldl (\<lambda>u. bin_cat u n) x xs =
-    bin_cat x (size xs * n) (foldl (\<lambda>u. bin_cat u n) y xs)"
-  apply (induct xs arbitrary: x)
-   apply simp
-  apply (simp (no_asm))
-  apply (frule asm_rl)
-  apply (drule meta_spec)
-  apply (erule trans)
-  apply (drule_tac x = "bin_cat y n a" in meta_spec)
-  apply (simp add: bin_cat_assoc_sym min.absorb2)
-  done
-
-lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))"
-  apply (unfold bin_rcat_def)
-  apply (rule sym)
-  apply (induct wl)
-   apply (auto simp add: bl_to_bin_append)
-  apply (simp add: bl_to_bin_aux_alt sclem)
-  apply (simp add: bin_cat_foldl_lem [symmetric])
-  done
-
-lemma bin_last_bl_to_bin: "bin_last (bl_to_bin bs) \<longleftrightarrow> bs \<noteq> [] \<and> last bs"
-by(cases "bs = []")(auto simp add: bl_to_bin_def last_bin_last'[where w=0])
-
-lemma bin_rest_bl_to_bin: "bin_rest (bl_to_bin bs) = bl_to_bin (butlast bs)"
-by(cases "bs = []")(simp_all add: bl_to_bin_def butlast_rest_bl2bin_aux)
-
-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 (induction n arbitrary: v w bs cs)
-   apply auto
-  apply (case_tac v rule: bin_exhaust)
-  apply (case_tac w rule: bin_exhaust)
-  apply clarsimp
-  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)"
-  by (induct n arbitrary: v w bs cs) simp_all
-
-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)"
-  by (induction n arbitrary: v w bs cs) simp_all
-
-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 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
-  using bl_xor_aux_bin by (simp add: bin_to_bl_def)
-
 end
diff -r 3f8e6c0166ac -r 6a2f43901350 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Aug 04 11:45:03 2020 +0100
+++ b/src/HOL/Word/Word.thy	Wed Aug 05 17:50:00 2020 +0100
@@ -1000,19 +1000,13 @@
   is xor
   by simp
 
-instance proof
-  fix a b :: \<open>'a word\<close> and n :: nat
-  show \<open>- a = NOT (a - 1)\<close>
-    by transfer (simp add: minus_eq_not_minus_1)
-  show \<open>bit (NOT a) n \<longleftrightarrow> (2 :: 'a word) ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
-    by transfer (simp add: bit_not_iff)
-  show \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
-    by transfer (auto simp add: bit_and_iff)
-  show \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
-    by transfer (auto simp add: bit_or_iff)
-  show \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
-    by transfer (auto simp add: bit_xor_iff)
-qed
+lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close>
+  is mask
+  .
+
+instance by (standard; transfer)
+  (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
+    bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)
 
 end
 
@@ -1170,8 +1164,13 @@
   by (simp add: shiftr_word_eq)
 
 lemma [code]:
-  \<open>take_bit n a = a AND mask n\<close> for a :: \<open>'a::len word\<close>
-  by (fact take_bit_eq_mask)
+  \<open>uint (take_bit n w) = (if n < LENGTH('a::len) then take_bit n (uint w) else uint w)\<close>
+  for w :: \<open>'a::len word\<close>
+  by transfer (simp add: min_def)
+
+lemma [code]:
+  \<open>uint (mask n :: 'a::len word) = mask (min LENGTH('a) n)\<close>
+  by transfer simp
 
 lemma [code_abbrev]:
   \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>
@@ -1289,9 +1288,6 @@
   is \<open>\<lambda>b k. take_bit LENGTH('a) k div 2 + of_bool b * 2 ^ (LENGTH('a) - Suc 0)\<close>
   by (fact arg_cong)
 
-lift_definition mask :: \<open>nat \<Rightarrow> 'a::len word\<close>
-  is \<open>take_bit LENGTH('a) \<circ> Bit_Operations.mask\<close> .
-
 lemma sshiftr1_eq:
   \<open>sshiftr1 w = word_of_int (bin_rest (sint w))\<close>
   by transfer simp
@@ -1328,7 +1324,7 @@
 qed
 
 lemma mask_eq:
-  \<open>mask n = (1 << n) - 1\<close>
+  \<open>mask n = (1 << n) - (1 :: 'a::len word)\<close>
   by transfer (simp add: mask_eq_exp_minus_1 push_bit_of_1) 
 
 lemma uint_sshiftr_eq [code]:
@@ -1977,18 +1973,8 @@
 lemma nth_ucast: "(ucast w::'a::len word) !! n = (w !! n \<and> n < LENGTH('a))"
   by transfer (simp add: bit_take_bit_iff ac_simps)
 
-context
-  includes lifting_syntax
-begin
-
-lemma transfer_rule_mask_word [transfer_rule]:
-  \<open>((=) ===> pcr_word) Bit_Operations.mask Bit_Operations.mask\<close>
-  by (simp only: mask_eq_exp_minus_1 [abs_def]) transfer_prover
-
-end
-
 lemma ucast_mask_eq:
-  \<open>ucast (Bit_Operations.mask n :: 'b word) = Bit_Operations.mask (min LENGTH('b::len) n)\<close>
+  \<open>ucast (mask n :: 'b word) = mask (min LENGTH('b::len) n)\<close>
   by (simp add: bit_eq_iff) (auto simp add: bit_mask_iff bit_ucast_iff exp_eq_zero_iff)
 
 \<comment> \<open>literal u(s)cast\<close>
@@ -4075,27 +4061,23 @@
 subsubsection \<open>Mask\<close>
 
 lemma minus_1_eq_mask:
-  \<open>- 1 = (Bit_Operations.mask LENGTH('a) :: 'a::len word)\<close>
+  \<open>- 1 = (mask LENGTH('a) :: 'a::len word)\<close>
   by (rule bit_eqI) (simp add: bit_exp_iff bit_mask_iff exp_eq_zero_iff)
-  
-lemma mask_eq_mask [code]:
-  \<open>mask = Bit_Operations.mask\<close>
-  by (rule ext, transfer) simp
 
 lemma mask_eq_decr_exp:
-  \<open>mask n = 2 ^ n - 1\<close>
-  by (simp add: mask_eq_mask mask_eq_exp_minus_1)
+  \<open>mask n = 2 ^ n - (1 :: 'a::len word)\<close>
+  by (fact mask_eq_exp_minus_1)
 
 lemma mask_Suc_rec:
-  \<open>mask (Suc n) = 2 * mask n + 1\<close>
-  by (simp add: mask_eq_mask mask_eq_exp_minus_1)
+  \<open>mask (Suc n) = 2 * mask n + (1 :: 'a::len word)\<close>
+  by (simp add: mask_eq_exp_minus_1)
 
 context
 begin
 
 qualified lemma bit_mask_iff:
   \<open>bit (mask m :: 'a::len word) n \<longleftrightarrow> n < min LENGTH('a) m\<close>
-  by (simp add: mask_eq_mask bit_mask_iff exp_eq_zero_iff not_le)
+  by (simp add: bit_mask_iff exp_eq_zero_iff not_le)
 
 end
 
@@ -4188,7 +4170,8 @@
 
 lemmas and_mask_less' = iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size]
 
-lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
+lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2 ^ n"
+  for x :: \<open>'a::len word\<close>
   unfolding word_size by (erule and_mask_less')
 
 lemma word_mod_2p_is_mask [OF refl]: "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = x AND mask n"
@@ -4212,6 +4195,7 @@
   by (auto simp: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps)
 
 lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
+  for x :: \<open>'a::len word\<close>
   using word_of_int_Ex [where x=x]
   by (auto simp: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps)
 
@@ -5365,10 +5349,6 @@
   "(1 :: 'a :: len word) !! n \<longleftrightarrow> 0 < LENGTH('a) \<and> n = 0"
   by simp
 
-lemma mask_0 [simp]:
-  "mask 0 = 0"
-  by (simp add: Word.mask_def)
-
 lemma shiftl0:
   "x << 0 = (x :: 'a :: len word)"
   by (fact shiftl_x_0)
@@ -5379,7 +5359,7 @@
 lemma mask_Suc_0: "mask (Suc 0) = 1"
   using mask_1 by simp
 
-lemma mask_numeral: "mask (numeral n) = 2 * mask (pred_numeral n) + 1"
+lemma mask_numeral: "mask (numeral n) = 2 * mask (pred_numeral n) + (1 :: 'a::len word)"
   by (simp add: mask_Suc_rec numeral_eq_Suc)
 
 lemma bin_last_bintrunc: "bin_last (bintrunc l n) = (l > 0 \<and> bin_last n)"
diff -r 3f8e6c0166ac -r 6a2f43901350 src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Tue Aug 04 11:45:03 2020 +0100
+++ b/src/HOL/ex/Word.thy	Wed Aug 05 17:50:00 2020 +0100
@@ -644,19 +644,12 @@
   is xor
   by simp
 
-instance proof
-  fix a b :: \<open>'a word\<close> and n :: nat
-  show \<open>- a = NOT (a - 1)\<close>
-    by transfer (simp add: minus_eq_not_minus_1)
-  show \<open>bit (NOT a) n \<longleftrightarrow> (2 :: 'a word) ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
-    by transfer (simp add: bit_not_iff)
-  show \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
-    by transfer (auto simp add: bit_and_iff)
-  show \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
-    by transfer (auto simp add: bit_or_iff)
-  show \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
-    by transfer (auto simp add: bit_xor_iff)
-qed
+lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close>
+  is mask .
+
+instance by (standard; transfer)
+  (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
+    bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)
 
 end
 
diff -r 3f8e6c0166ac -r 6a2f43901350 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Aug 04 11:45:03 2020 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Aug 05 17:50:00 2020 +0100
@@ -27,7 +27,7 @@
   val default_params: params
   val forks: params -> (unit -> 'a) list -> 'a future list
   val fork: (unit -> 'a) -> 'a future
-  val get_finished: 'a future -> 'a
+  val get_result: 'a future -> 'a Exn.result
   val join_results: 'a future list -> 'a Exn.result list
   val join_result: 'a future -> 'a Exn.result
   val joins: 'a future list -> 'a list
@@ -320,11 +320,14 @@
     val max_active0 = ! max_active;
     val max_workers0 = ! max_workers;
 
+    val workers_waiting = count_workers Waiting;
+
     val m =
       if ! do_shutdown andalso Task_Queue.all_passive (! queue) then 0
       else Multithreading.max_threads ();
     val _ = max_active := m;
-    val _ = max_workers := 2 * m;
+    val _ = max_workers :=
+      Int.max (2 * m, if workers_waiting > 0 then workers_waiting + 1 else 0);
 
     val missing = ! max_workers - length (! workers);
     val _ =
@@ -508,8 +511,6 @@
         | exns => Exn.Exn (Par_Exn.make exns))
       else res);
 
-fun get_finished x = Exn.release (get_result x);
-
 local
 
 fun join_next atts deps = (*requires SYNCHRONIZED*)
diff -r 3f8e6c0166ac -r 6a2f43901350 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Tue Aug 04 11:45:03 2020 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Wed Aug 05 17:50:00 2020 +0100
@@ -103,7 +103,7 @@
                   let
                     val res0 = Exn.capture (restore_attributes e) ();
                     val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
-                    val res = Future.join_result x;
+                    val res = Future.get_result x;
                     val _ =
                       if not (Exn.is_interrupt_exn res) then
                         Synchronized.assign var (Result (Future.value_result res))