diff -r 1d8e914e04d6 -r 572ab9e64e18 src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy	Wed Feb 05 20:16:59 2020 +0000
+++ b/src/HOL/ex/Bit_Lists.thy	Wed Feb 05 20:17:00 2020 +0000
@@ -5,9 +5,19 @@
 
 theory Bit_Lists
   imports
-    Word
+    Word "HOL-Library.More_List"
 begin
 
+lemma hd_zip:
+  \<open>hd (zip xs ys) = (hd xs, hd ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close>
+  using that by (cases xs; cases ys) simp_all
+
+lemma last_zip:
+  \<open>last (zip xs ys) = (last xs, last ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close>
+    and \<open>length xs = length ys\<close>
+  using that by (cases xs rule: rev_cases; cases ys rule: rev_cases) simp_all
+
+
 subsection \<open>Fragments of algebraic bit representations\<close>
 
 context comm_semiring_1
@@ -36,7 +46,7 @@
     simp_all add: algebra_simps)
 
 lemma unsigned_of_bits_take [simp]:
-  "unsigned_of_bits (take n bs) = Parity.take_bit n (unsigned_of_bits bs)"
+  "unsigned_of_bits (take n bs) = take_bit n (unsigned_of_bits bs)"
 proof (induction bs arbitrary: n)
   case Nil
   then show ?case
@@ -59,6 +69,18 @@
     by (cases n) simp_all
 qed
 
+lemma bit_unsigned_of_bits_iff:
+  \<open>bit (unsigned_of_bits bs) n \<longleftrightarrow> nth_default False bs n\<close>
+proof (induction bs arbitrary: n)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons b bs)
+  then show ?case
+    by (cases n) simp_all
+qed
+
 primrec n_bits_of :: "nat \<Rightarrow> 'a \<Rightarrow> bool list"
   where
     "n_bits_of 0 a = []"
@@ -125,6 +147,10 @@
 
 end
 
+lemma bit_of_bits_nat_iff:
+  \<open>bit (of_bits bs :: nat) n \<longleftrightarrow> nth_default False bs n\<close>
+  by (simp add: bit_unsigned_of_bits_iff)
+
 lemma bits_of_Suc_0 [simp]:
   "bits_of (Suc 0) = [True]"
   by simp
@@ -211,6 +237,18 @@
     by (simp_all add: *)
 qed
 
+lemma bit_of_bits_int_iff:
+  \<open>bit (of_bits bs :: int) n \<longleftrightarrow> nth_default (bs \<noteq> [] \<and> last bs) bs n\<close>
+proof (induction bs arbitrary: n)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons b bs)
+  then show ?case
+    by (cases n; cases b; cases bs) simp_all
+qed
+
 lemma of_bits_append [simp]:
   "of_bits (bs @ cs) = of_bits bs + push_bit (length bs) (of_bits cs :: int)"
     if "bs \<noteq> []" "\<not> last bs"
@@ -291,24 +329,14 @@
 class ring_bit_representation = ring_bit_operations + semiring_bit_representation +
   assumes not_eq: "not = of_bits \<circ> map Not \<circ> bits_of"
 
-
 context zip_nat
 begin
 
 lemma of_bits:
   "of_bits bs \<^bold>\<times> of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: nat)"
-    if "length bs = length cs" for bs cs
-using that proof (induction bs cs rule: list_induct2)
-  case Nil
-  then show ?case
-    by simp
-next
-  case (Cons b bs c cs)
-  then show ?case
-    by (cases "of_bits bs = (0::nat) \<or> of_bits cs = (0::nat)")
-      (auto simp add: ac_simps end_of_bits rec [of "Suc 0"])
-qed
-
+  if "length bs = length cs" for bs cs
+  by (simp add: Parity.bit_eq_iff bit_unsigned_of_bits_iff bit_eq_iff)
+    (simp add: that end_of_bits nth_default_map2 [of _ _ _ False False])
 end
 
 instance nat :: semiring_bit_representation
@@ -321,32 +349,22 @@
 begin
  
 lemma of_bits:
-  "of_bits bs \<^bold>\<times> of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: int)"
-    if "length bs = length cs" and "\<not> False \<^bold>* False" for bs cs
-using \<open>length bs = length cs\<close> proof (induction bs cs rule: list_induct2)
-  case Nil
-  then show ?case
-    using \<open>\<not> False \<^bold>* False\<close> by (auto simp add: False_False_imp_True_True split: bool.splits)
+  \<open>of_bits bs \<^bold>\<times> of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: int)\<close>
+  if \<open>length bs = length cs\<close> and \<open>\<not> False \<^bold>* False\<close> for bs cs
+proof (cases \<open>bs = []\<close>)
+  case True
+  moreover have \<open>cs = []\<close>
+    using True that by simp
+  ultimately show ?thesis
+    by (simp add: Parity.bit_eq_iff bit_eq_iff that)
 next
-  case (Cons b bs c cs)
-  show ?case
-  proof (cases "bs = []")
-    case True
-    with Cons show ?thesis
-      using \<open>\<not> False \<^bold>* False\<close> by (cases b; cases c)
-        (auto simp add: ac_simps split: bool.splits)
-  next
-    case False
-    with Cons.hyps have "cs \<noteq> []"
-      by auto
-    with \<open>bs \<noteq> []\<close> have "map2 (\<^bold>*) bs cs \<noteq> []"
-      by (simp add: zip_eq_Nil_iff)
-    from \<open>bs \<noteq> []\<close> \<open>cs \<noteq> []\<close> \<open>map2 (\<^bold>*) bs cs \<noteq> []\<close> Cons show ?thesis
-      by (cases b; cases c)
-        (auto simp add: \<open>\<not> False \<^bold>* False\<close> ac_simps
-          rec [of "of_bits bs * 2"] rec [of "of_bits cs * 2"]
-          rec [of "1 + of_bits bs * 2"])
-  qed
+  case False
+  moreover have \<open>cs \<noteq> []\<close>
+    using False that by auto
+  ultimately show ?thesis
+    apply (simp add: Parity.bit_eq_iff bit_of_bits_int_iff bit_eq_iff zip_eq_Nil_iff last_map last_zip that)
+    apply (simp add: that nth_default_map2 [of _ _ _ \<open>last bs\<close> \<open>last cs\<close>])
+    done
 qed
 
 end