diff --git a/src/HOL/Library/More_List.thy b/src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy
+++ b/src/HOL/Library/More_List.thy
@@ -1,382 +1,395 @@
 (* Author: Andreas Lochbihler, ETH Zürich
    Author: Florian Haftmann, TU Muenchen  *)
 
 section \<open>Less common functions on lists\<close>
 
 theory More_List
 imports Main
 begin
 
 definition strip_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "strip_while P = rev \<circ> dropWhile P \<circ> rev"
 
 lemma strip_while_rev [simp]:
   "strip_while P (rev xs) = rev (dropWhile P xs)"
   by (simp add: strip_while_def)
   
 lemma strip_while_Nil [simp]:
   "strip_while P [] = []"
   by (simp add: strip_while_def)
 
 lemma strip_while_append [simp]:
   "\<not> P x \<Longrightarrow> strip_while P (xs @ [x]) = xs @ [x]"
   by (simp add: strip_while_def)
 
 lemma strip_while_append_rec [simp]:
   "P x \<Longrightarrow> strip_while P (xs @ [x]) = strip_while P xs"
   by (simp add: strip_while_def)
 
 lemma strip_while_Cons [simp]:
   "\<not> P x \<Longrightarrow> strip_while P (x # xs) = x # strip_while P xs"
   by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
 
 lemma strip_while_eq_Nil [simp]:
   "strip_while P xs = [] \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
   by (simp add: strip_while_def)
 
 lemma strip_while_eq_Cons_rec:
   "strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))"
   by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
 
 lemma split_strip_while_append:
   fixes xs :: "'a list"
   obtains ys zs :: "'a list"
   where "strip_while P xs = ys" and "\<forall>x\<in>set zs. P x" and "xs = ys @ zs"
 proof (rule that)
   show "strip_while P xs = strip_while P xs" ..
   show "\<forall>x\<in>set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
   have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
     by (simp add: strip_while_def)
   then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
     by (simp only: rev_is_rev_conv)
 qed
 
 lemma strip_while_snoc [simp]:
   "strip_while P (xs @ [x]) = (if P x then strip_while P xs else xs @ [x])"
   by (simp add: strip_while_def)
 
 lemma strip_while_map:
   "strip_while P (map f xs) = map f (strip_while (P \<circ> f) xs)"
   by (simp add: strip_while_def rev_map dropWhile_map)
 
 lemma strip_while_dropWhile_commute:
   "strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)"
 proof (induct xs)
   case Nil
   then show ?case
     by simp
 next
   case (Cons x xs)
   show ?case
   proof (cases "\<forall>y\<in>set xs. P y")
     case True
     with dropWhile_append2 [of "rev xs"] show ?thesis
       by (auto simp add: strip_while_def dest: set_dropWhileD)
   next
     case False
     then obtain y where "y \<in> set xs" and "\<not> P y"
       by blast
     with Cons dropWhile_append3 [of P y "rev xs"] show ?thesis
       by (simp add: strip_while_def)
   qed
 qed
 
 lemma dropWhile_strip_while_commute:
   "dropWhile P (strip_while Q xs) = strip_while Q (dropWhile P xs)"
   by (simp add: strip_while_dropWhile_commute)
 
 
 definition no_leading :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
 where
   "no_leading P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (hd xs))"
 
 lemma no_leading_Nil [simp, intro!]:
   "no_leading P []"
   by (simp add: no_leading_def)
 
 lemma no_leading_Cons [simp, intro!]:
   "no_leading P (x # xs) \<longleftrightarrow> \<not> P x"
   by (simp add: no_leading_def)
 
 lemma no_leading_append [simp]:
   "no_leading P (xs @ ys) \<longleftrightarrow> no_leading P xs \<and> (xs = [] \<longrightarrow> no_leading P ys)"
   by (induct xs) simp_all
 
 lemma no_leading_dropWhile [simp]:
   "no_leading P (dropWhile P xs)"
   by (induct xs) simp_all
 
 lemma dropWhile_eq_obtain_leading:
   assumes "dropWhile P xs = ys"
   obtains zs where "xs = zs @ ys" and "\<And>z. z \<in> set zs \<Longrightarrow> P z" and "no_leading P ys"
 proof -
   from assms have "\<exists>zs. xs = zs @ ys \<and> (\<forall>z \<in> set zs. P z) \<and> no_leading P ys"
   proof (induct xs arbitrary: ys)
     case Nil then show ?case by simp
   next
     case (Cons x xs ys)
     show ?case proof (cases "P x")
       case True with Cons.hyps [of ys] Cons.prems
       have "\<exists>zs. xs = zs @ ys \<and> (\<forall>a\<in>set zs. P a) \<and> no_leading P ys"
         by simp
       then obtain zs where "xs = zs @ ys" and "\<And>z. z \<in> set zs \<Longrightarrow> P z"
         and *: "no_leading P ys"
         by blast
       with True have "x # xs = (x # zs) @ ys" and "\<And>z. z \<in> set (x # zs) \<Longrightarrow> P z"
         by auto
       with * show ?thesis
         by blast    next
       case False
       with Cons show ?thesis by (cases ys) simp_all
     qed
   qed
   with that show thesis
     by blast
 qed
 
 lemma dropWhile_idem_iff:
   "dropWhile P xs = xs \<longleftrightarrow> no_leading P xs"
   by (cases xs) (auto elim: dropWhile_eq_obtain_leading)
 
 
 abbreviation no_trailing :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
 where
   "no_trailing P xs \<equiv> no_leading P (rev xs)"
 
 lemma no_trailing_unfold:
   "no_trailing P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (last xs))"
   by (induct xs) simp_all
 
 lemma no_trailing_Nil [simp, intro!]:
   "no_trailing P []"
   by simp
 
 lemma no_trailing_Cons [simp]:
   "no_trailing P (x # xs) \<longleftrightarrow> no_trailing P xs \<and> (xs = [] \<longrightarrow> \<not> P x)"
   by simp
 
 lemma no_trailing_append:
   "no_trailing P (xs @ ys) \<longleftrightarrow> no_trailing P ys \<and> (ys = [] \<longrightarrow> no_trailing P xs)"
   by (induct xs) simp_all
 
 lemma no_trailing_append_Cons [simp]:
   "no_trailing P (xs @ y # ys) \<longleftrightarrow> no_trailing P (y # ys)"
   by simp
 
 lemma no_trailing_strip_while [simp]:
   "no_trailing P (strip_while P xs)"
   by (induct xs rule: rev_induct) simp_all
 
 lemma strip_while_idem [simp]:
   "no_trailing P xs \<Longrightarrow> strip_while P xs = xs"
   by (cases xs rule: rev_cases) simp_all
 
 lemma strip_while_eq_obtain_trailing:
   assumes "strip_while P xs = ys"
   obtains zs where "xs = ys @ zs" and "\<And>z. z \<in> set zs \<Longrightarrow> P z" and "no_trailing P ys"
 proof -
   from assms have "rev (rev (dropWhile P (rev xs))) = rev ys"
     by (simp add: strip_while_def)
   then have "dropWhile P (rev xs) = rev ys"
     by simp
   then obtain zs where A: "rev xs = zs @ rev ys" and B: "\<And>z. z \<in> set zs \<Longrightarrow> P z"
     and C: "no_trailing P ys"
     using dropWhile_eq_obtain_leading by blast
   from A have "rev (rev xs) = rev (zs @ rev ys)"
     by simp
   then have "xs = ys @ rev zs"
     by simp
   moreover from B have "\<And>z. z \<in> set (rev zs) \<Longrightarrow> P z"
     by simp
   ultimately show thesis using that C by blast
 qed
 
 lemma strip_while_idem_iff:
   "strip_while P xs = xs \<longleftrightarrow> no_trailing P xs"
 proof -
   define ys where "ys = rev xs"
   moreover have "strip_while P (rev ys) = rev ys \<longleftrightarrow> no_trailing P (rev ys)"
     by (simp add: dropWhile_idem_iff)
   ultimately show ?thesis by simp
 qed
 
 lemma no_trailing_map:
   "no_trailing P (map f xs) \<longleftrightarrow> no_trailing (P \<circ> f) xs"
   by (simp add: last_map no_trailing_unfold)
 
 lemma no_trailing_drop [simp]:
   "no_trailing P (drop n xs)" if "no_trailing P xs"
 proof -
   from that have "no_trailing P (take n xs @ drop n xs)"
     by simp
   then show ?thesis
     by (simp only: no_trailing_append)
 qed
 
 lemma no_trailing_upt [simp]:
   "no_trailing P [n..<m] \<longleftrightarrow> (n < m \<longrightarrow> \<not> P (m - 1))"
   by (auto simp add: no_trailing_unfold)
 
 
 definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
 where
   "nth_default dflt xs n = (if n < length xs then xs ! n else dflt)"
 
 lemma nth_default_nth:
   "n < length xs \<Longrightarrow> nth_default dflt xs n = xs ! n"
   by (simp add: nth_default_def)
 
 lemma nth_default_beyond:
   "length xs \<le> n \<Longrightarrow> nth_default dflt xs n = dflt"
   by (simp add: nth_default_def)
 
 lemma nth_default_Nil [simp]:
   "nth_default dflt [] n = dflt"
   by (simp add: nth_default_def)
 
 lemma nth_default_Cons:
   "nth_default dflt (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default dflt xs n')"
   by (simp add: nth_default_def split: nat.split)
 
 lemma nth_default_Cons_0 [simp]:
   "nth_default dflt (x # xs) 0 = x"
   by (simp add: nth_default_Cons)
 
 lemma nth_default_Cons_Suc [simp]:
   "nth_default dflt (x # xs) (Suc n) = nth_default dflt xs n"
   by (simp add: nth_default_Cons)
 
 lemma nth_default_replicate_dflt [simp]:
   "nth_default dflt (replicate n dflt) m = dflt"
   by (simp add: nth_default_def)
 
 lemma nth_default_append:
   "nth_default dflt (xs @ ys) n =
     (if n < length xs then nth xs n else nth_default dflt ys (n - length xs))"
   by (auto simp add: nth_default_def nth_append)
 
 lemma nth_default_append_trailing [simp]:
   "nth_default dflt (xs @ replicate n dflt) = nth_default dflt xs"
   by (simp add: fun_eq_iff nth_default_append) (simp add: nth_default_def)
 
 lemma nth_default_snoc_default [simp]:
   "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
   by (auto simp add: nth_default_def fun_eq_iff nth_append)
 
 lemma nth_default_eq_dflt_iff:
   "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
   by (simp add: nth_default_def)
 
 lemma nth_default_take_eq:
   "nth_default dflt (take m xs) n =
     (if n < m then nth_default dflt xs n else dflt)"
   by (simp add: nth_default_def)
 
 lemma in_enumerate_iff_nth_default_eq:
   "x \<noteq> dflt \<Longrightarrow> (n, x) \<in> set (enumerate 0 xs) \<longleftrightarrow> nth_default dflt xs n = x"
   by (auto simp add: nth_default_def in_set_conv_nth enumerate_eq_zip)
 
 lemma last_conv_nth_default:
   assumes "xs \<noteq> []"
   shows "last xs = nth_default dflt xs (length xs - 1)"
   using assms by (simp add: nth_default_def last_conv_nth)
   
 lemma nth_default_map_eq:
   "f dflt' = dflt \<Longrightarrow> nth_default dflt (map f xs) n = f (nth_default dflt' xs n)"
   by (simp add: nth_default_def)
 
 lemma finite_nth_default_neq_default [simp]:
   "finite {k. nth_default dflt xs k \<noteq> dflt}"
   by (simp add: nth_default_def)
 
 lemma sorted_list_of_set_nth_default:
   "sorted_list_of_set {k. nth_default dflt xs k \<noteq> dflt} = map fst (filter (\<lambda>(_, x). x \<noteq> dflt) (enumerate 0 xs))"
   by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth
     sorted_filter distinct_map_filter enumerate_eq_zip intro: rev_image_eqI)
 
 lemma map_nth_default:
   "map (nth_default x xs) [0..<length xs] = xs"
 proof -
   have *: "map (nth_default x xs) [0..<length xs] = map (List.nth xs) [0..<length xs]"
     by (rule map_cong) (simp_all add: nth_default_nth)
   show ?thesis by (simp add: * map_nth)
 qed
 
 lemma range_nth_default [simp]:
   "range (nth_default dflt xs) = insert dflt (set xs)"
   by (auto simp add: nth_default_def [abs_def] in_set_conv_nth)
 
 lemma nth_strip_while:
   assumes "n < length (strip_while P xs)"
   shows "strip_while P xs ! n = xs ! n"
 proof -
   have "length (dropWhile P (rev xs)) + length (takeWhile P (rev xs)) = length xs"
     by (subst add.commute)
       (simp add: arg_cong [where f=length, OF takeWhile_dropWhile_id, unfolded length_append])
   then show ?thesis using assms
     by (simp add: strip_while_def rev_nth dropWhile_nth)
 qed
 
 lemma length_strip_while_le:
   "length (strip_while P xs) \<le> length xs"
   unfolding strip_while_def o_def length_rev
   by (subst (2) length_rev[symmetric])
     (simp add: strip_while_def length_dropWhile_le del: length_rev)
 
 lemma nth_default_strip_while_dflt [simp]:
   "nth_default dflt (strip_while ((=) dflt) xs) = nth_default dflt xs"
   by (induct xs rule: rev_induct) auto
 
 lemma nth_default_eq_iff:
   "nth_default dflt xs = nth_default dflt ys
      \<longleftrightarrow> strip_while (HOL.eq dflt) xs = strip_while (HOL.eq dflt) ys" (is "?P \<longleftrightarrow> ?Q")
 proof
   let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
   assume ?P
   then have eq: "nth_default dflt ?xs = nth_default dflt ?ys"
     by simp
   have len: "length ?xs = length ?ys"
   proof (rule ccontr)
     assume len: "length ?xs \<noteq> length ?ys"
     { fix xs ys :: "'a list"
       let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
       assume eq: "nth_default dflt ?xs = nth_default dflt ?ys"
       assume len: "length ?xs < length ?ys"
       then have "length ?ys > 0" by arith
       then have "?ys \<noteq> []" by simp
       with last_conv_nth_default [of ?ys dflt]
       have "last ?ys = nth_default dflt ?ys (length ?ys - 1)"
         by auto
       moreover from \<open>?ys \<noteq> []\<close> no_trailing_strip_while [of "HOL.eq dflt" ys]
         have "last ?ys \<noteq> dflt" by (simp add: no_trailing_unfold)
       ultimately have "nth_default dflt ?xs (length ?ys - 1) \<noteq> dflt"
         using eq by simp
       moreover from len have "length ?ys - 1 \<ge> length ?xs" by simp
       ultimately have False by (simp only: nth_default_beyond) simp
     } 
     from this [of xs ys] this [of ys xs] len eq show False
       by (auto simp only: linorder_class.neq_iff)
   qed
   then show ?Q
   proof (rule nth_equalityI [rule_format])
     fix n
     assume n: "n < length ?xs"
     with len have "n < length ?ys"
       by simp
     with n have xs: "nth_default dflt ?xs n = ?xs ! n"
       and ys: "nth_default dflt ?ys n = ?ys ! n"
       by (simp_all only: nth_default_nth)
     with eq show "?xs ! n = ?ys ! n"
       by simp
   qed
 next
   assume ?Q
   then have "nth_default dflt (strip_while (HOL.eq dflt) xs) = nth_default dflt (strip_while (HOL.eq dflt) ys)"
     by simp
   then show ?P
     by simp
 qed
 
+lemma nth_default_map2:
+  \<open>nth_default d (map2 f xs ys) n = f (nth_default d1 xs n) (nth_default d2 ys n)\<close>
+    if \<open>length xs = length ys\<close> and \<open>f d1 d2 = d\<close> for bs cs
+using that proof (induction xs ys arbitrary: n rule: list_induct2)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons x xs y ys)
+  then show ?case
+    by (cases n) simp_all
+qed
+
 end
 
diff --git a/src/HOL/ex/Bit_Lists.thy b/src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy
+++ b/src/HOL/ex/Bit_Lists.thy
@@ -1,367 +1,385 @@
 (*  Author:  Florian Haftmann, TUM
 *)
 
 section \<open>Proof(s) of concept for algebraically founded lists of bits\<close>
 
 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
 begin
  
 primrec radix_value :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'a"
   where "radix_value f b [] = 0"
   | "radix_value f b (a # as) = f a + radix_value f b as * b"
 
 abbreviation (input) unsigned_of_bits :: "bool list \<Rightarrow> 'a"
   where "unsigned_of_bits \<equiv> radix_value of_bool 2"
 
 lemma unsigned_of_bits_replicate_False [simp]:
   "unsigned_of_bits (replicate n False) = 0"
   by (induction n) simp_all
 
 end
 
 context unique_euclidean_semiring_with_bit_shifts
 begin
 
 lemma unsigned_of_bits_append [simp]:
   "unsigned_of_bits (bs @ cs) = unsigned_of_bits bs
     + push_bit (length bs) (unsigned_of_bits cs)"
   by (induction bs) (simp_all add: push_bit_double,
     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
     by simp
 next
   case (Cons b bs)
   then show ?case
     by (cases n) (simp_all add: ac_simps)
 qed
 
 lemma unsigned_of_bits_drop [simp]:
   "unsigned_of_bits (drop n bs) = Parity.drop_bit n (unsigned_of_bits bs)"
 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
 
+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 = []"
   | "n_bits_of (Suc n) a = odd a # n_bits_of n (a div 2)"
 
 lemma n_bits_of_eq_iff:
   "n_bits_of n a = n_bits_of n b \<longleftrightarrow> Parity.take_bit n a = Parity.take_bit n b"
   apply (induction n arbitrary: a b)
    apply (auto elim!: evenE oddE)
    apply (metis dvd_triv_right even_plus_one_iff)
   apply (metis dvd_triv_right even_plus_one_iff)
   done
 
 lemma take_n_bits_of [simp]:
   "take m (n_bits_of n a) = n_bits_of (min m n) a"
 proof -
   define q and v and w where "q = min m n" and "v = m - q" and "w = n - q"
   then have "v = 0 \<or> w = 0"
     by auto
   then have "take (q + v) (n_bits_of (q + w) a) = n_bits_of q a"
     by (induction q arbitrary: a) auto
   with q_def v_def w_def show ?thesis
     by simp
 qed
 
 lemma unsigned_of_bits_n_bits_of [simp]:
   "unsigned_of_bits (n_bits_of n a) = Parity.take_bit n a"
   by (induction n arbitrary: a) (simp_all add: ac_simps)
 
 end
 
 
 subsection \<open>Syntactic bit representation\<close>
 
 class bit_representation =
   fixes bits_of :: "'a \<Rightarrow> bool list"
     and of_bits :: "bool list \<Rightarrow> 'a"
   assumes of_bits_of [simp]: "of_bits (bits_of a) = a"
 
 text \<open>Unclear whether a \<^typ>\<open>bool\<close> instantiation is needed or not\<close>
 
 instantiation nat :: bit_representation
 begin
 
 fun bits_of_nat :: "nat \<Rightarrow> bool list"
   where "bits_of (n::nat) =
     (if n = 0 then [] else odd n # bits_of (n div 2))"
 
 lemma bits_of_nat_simps [simp]:
   "bits_of (0::nat) = []"
   "n > 0 \<Longrightarrow> bits_of n = odd n # bits_of (n div 2)" for n :: nat
   by simp_all
 
 declare bits_of_nat.simps [simp del]
 
 definition of_bits_nat :: "bool list \<Rightarrow> nat"
   where [simp]: "of_bits_nat = unsigned_of_bits"
   \<comment> \<open>remove simp\<close>
 
 instance proof
   show "of_bits (bits_of n) = n" for n :: nat
     by (induction n rule: nat_bit_induct) simp_all
 qed
 
 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
 
 lemma bits_of_1_nat [simp]:
   "bits_of (1 :: nat) = [True]"
   by simp
 
 lemma bits_of_nat_numeral_simps [simp]:
   "bits_of (numeral Num.One :: nat) = [True]" (is ?One)
   "bits_of (numeral (Num.Bit0 n) :: nat) = False # bits_of (numeral n :: nat)" (is ?Bit0)
   "bits_of (numeral (Num.Bit1 n) :: nat) = True # bits_of (numeral n :: nat)" (is ?Bit1)
 proof -
   show ?One
     by simp
   define m :: nat where "m = numeral n"
   then have "m > 0" and *: "numeral n = m" "numeral (Num.Bit0 n) = 2 * m" "numeral (Num.Bit1 n) = Suc (2 * m)"
     by simp_all
   from \<open>m > 0\<close> show ?Bit0 ?Bit1
     by (simp_all add: *)
 qed
 
 lemma unsigned_of_bits_of_nat [simp]:
   "unsigned_of_bits (bits_of n) = n" for n :: nat
   using of_bits_of [of n] by simp
 
 instantiation int :: bit_representation
 begin
 
 fun bits_of_int :: "int \<Rightarrow> bool list"
   where "bits_of_int k = odd k #
     (if k = 0 \<or> k = - 1 then [] else bits_of_int (k div 2))"
 
 lemma bits_of_int_simps [simp]:
   "bits_of (0 :: int) = [False]"
   "bits_of (- 1 :: int) = [True]"
   "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> bits_of k = odd k # bits_of (k div 2)" for k :: int
   by simp_all
 
 lemma bits_of_not_Nil [simp]:
   "bits_of k \<noteq> []" for k :: int
   by simp
 
 declare bits_of_int.simps [simp del]
 
 definition of_bits_int :: "bool list \<Rightarrow> int"
   where "of_bits_int bs = (if bs = [] \<or> \<not> last bs then unsigned_of_bits bs
     else unsigned_of_bits bs - 2 ^ length bs)"
 
 lemma of_bits_int_simps [simp]:
   "of_bits [] = (0 :: int)"
   "of_bits [False] = (0 :: int)"
   "of_bits [True] = (- 1 :: int)"
   "of_bits (bs @ [b]) = (unsigned_of_bits bs :: int) - (2 ^ length bs) * of_bool b"
   "of_bits (False # bs) = 2 * (of_bits bs :: int)"
   "bs \<noteq> [] \<Longrightarrow> of_bits (True # bs) = 1 + 2 * (of_bits bs :: int)"
   by (simp_all add: of_bits_int_def push_bit_of_1)
 
 instance proof
   show "of_bits (bits_of k) = k" for k :: int
     by (induction k rule: int_bit_induct) simp_all
 qed
 
 lemma bits_of_1_int [simp]:
   "bits_of (1 :: int) = [True, False]"
   by simp
 
 lemma bits_of_int_numeral_simps [simp]:
   "bits_of (numeral Num.One :: int) = [True, False]" (is ?One)
   "bits_of (numeral (Num.Bit0 n) :: int) = False # bits_of (numeral n :: int)" (is ?Bit0)
   "bits_of (numeral (Num.Bit1 n) :: int) = True # bits_of (numeral n :: int)" (is ?Bit1)
   "bits_of (- numeral (Num.Bit0 n) :: int) = False # bits_of (- numeral n :: int)" (is ?nBit0)
   "bits_of (- numeral (Num.Bit1 n) :: int) = True # bits_of (- numeral (Num.inc n) :: int)" (is ?nBit1)
 proof -
   show ?One
     by simp
   define k :: int where "k = numeral n"
   then have "k > 0" and *: "numeral n = k" "numeral (Num.Bit0 n) = 2 * k" "numeral (Num.Bit1 n) = 2 * k + 1"
     "numeral (Num.inc n) = k + 1"
     by (simp_all add: add_One)
   have "- (2 * k) div 2 = - k" "(- (2 * k) - 1) div 2 = - k - 1"
     by simp_all
   with \<open>k > 0\<close> show ?Bit0 ?Bit1 ?nBit0 ?nBit1
     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"
 using that proof (induction bs rule: list_nonempty_induct)
   case (single b)
   then show ?case
     by simp
 next
   case (cons b bs)
   then show ?case
     by (cases b) (simp_all add: push_bit_double)
 qed
 
 lemma of_bits_replicate_False [simp]:
   "of_bits (replicate n False) = (0 :: int)"
   by (auto simp add: of_bits_int_def)
 
 lemma of_bits_drop [simp]:
   "of_bits (drop n bs) = Parity.drop_bit n (of_bits bs :: int)"
     if "n < length bs"
 using that proof (induction bs arbitrary: n)
   case Nil
   then show ?case
     by simp
 next
   case (Cons b bs)
   show ?case
   proof (cases n)
     case 0
     then show ?thesis
       by simp
   next
     case (Suc n)
     with Cons.prems have "bs \<noteq> []"
       by auto
     with Suc Cons.IH [of n] Cons.prems show ?thesis
       by (cases b) simp_all
   qed
 qed
 
 end
 
 lemma unsigned_of_bits_eq_of_bits:
   "unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)"
   by (simp add: of_bits_int_def)
 
 instantiation word :: (len) bit_representation
 begin
 
 lift_definition bits_of_word :: "'a word \<Rightarrow> bool list"
   is "n_bits_of LENGTH('a)"
   by (simp add: n_bits_of_eq_iff)
 
 lift_definition of_bits_word :: "bool list \<Rightarrow> 'a word"
   is unsigned_of_bits .
 
 instance proof
   fix a :: "'a word"
   show "of_bits (bits_of a) = a"
     by transfer simp
 qed
 
 end
 
 
 subsection \<open>Bit representations with bit operations\<close>
 
 class semiring_bit_representation = semiring_bit_operations + bit_representation +
   assumes and_eq: "length bs = length cs \<Longrightarrow>
       of_bits bs AND of_bits cs = of_bits (map2 (\<and>) bs cs)"
     and or_eq: "length bs = length cs \<Longrightarrow>
       of_bits bs OR of_bits cs = of_bits (map2 (\<or>) bs cs)"
     and xor_eq: "length bs = length cs \<Longrightarrow>
       of_bits bs XOR of_bits cs = of_bits (map2 (\<noteq>) bs cs)"
     and push_bit_eq: "push_bit n a = of_bits (replicate n False @ bits_of a)"
     and drop_bit_eq: "n < length (bits_of a) \<Longrightarrow> drop_bit n a = of_bits (drop n (bits_of a))"
 
 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
   apply standard
       apply (simp_all only: and_nat.of_bits or_nat.of_bits xor_nat.of_bits)
    apply simp_all
   done
 
 context zip_int
 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
 
 instance int :: ring_bit_representation
 proof
   show "(not :: int \<Rightarrow> _) = of_bits \<circ> map Not \<circ> bits_of"
   proof (rule sym, rule ext)
     fix k :: int
     show "(of_bits \<circ> map Not \<circ> bits_of) k = NOT k"
       by (induction k rule: int_bit_induct) (simp_all add: not_int_def)
   qed
   show "push_bit n k = of_bits (replicate n False @ bits_of k)"
     for k :: int and n :: nat
     by (cases "n = 0") simp_all
 qed (simp_all add: and_int.of_bits or_int.of_bits xor_int.of_bits)
 
 end
diff --git a/src/HOL/ex/Bit_Operations.thy b/src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy
+++ b/src/HOL/ex/Bit_Operations.thy
@@ -1,758 +1,472 @@
 (*  Author:  Florian Haftmann, TUM
 *)
 
 section \<open>Proof of concept for purely algebraically founded lists of bits\<close>
 
 theory Bit_Operations
   imports
     "HOL-Library.Boolean_Algebra"
     Main
 begin
 
 context semiring_bit_shifts
 begin
 
 (*lemma bit_push_bit_iff:
   \<open>bit (push_bit m a) n \<longleftrightarrow> n \<ge> m \<and> 2 ^ n \<noteq> 0 \<and> bit a (n - m)\<close>*)
 
 end
 
 
 subsection \<open>Bit operations in suitable algebraic structures\<close>
 
 class semiring_bit_operations = semiring_bit_shifts +
   fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr "AND" 64)
     and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr "OR"  59)
     and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr "XOR" 59)
   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>
 begin
 
 text \<open>
   We want the bitwise operations to bind slightly weaker
   than \<open>+\<close> and \<open>-\<close>.
   For the sake of code generation
   the operations \<^const>\<open>and\<close>, \<^const>\<open>or\<close> and \<^const>\<open>xor\<close>
   are specified as definitional class operations.
 \<close>
 
 definition map_bit :: \<open>nat \<Rightarrow> (bool \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   where \<open>map_bit n f a = take_bit n a + push_bit n (of_bool (f (bit a n)) + 2 * drop_bit (Suc n) a)\<close>
 
 definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   where \<open>set_bit n = map_bit n top\<close>
 
 definition unset_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   where \<open>unset_bit n = map_bit n bot\<close>
 
 definition flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   where \<open>flip_bit n = map_bit n Not\<close>
 
 text \<open>
   Having 
   \<^const>\<open>set_bit\<close>, \<^const>\<open>unset_bit\<close> and \<^const>\<open>flip_bit\<close> as separate
   operations allows to implement them using bit masks later.
 \<close>
 
 lemma stable_imp_drop_eq:
   \<open>drop_bit n a = a\<close> if \<open>a div 2 = a\<close>
   by (induction n) (simp_all add: that)
 
 lemma map_bit_0 [simp]:
   \<open>map_bit 0 f a = of_bool (f (odd a)) + 2 * (a div 2)\<close>
   by (simp add: map_bit_def)
 
 lemma map_bit_Suc [simp]:
   \<open>map_bit (Suc n) f a = a mod 2 + 2 * map_bit n f (a div 2)\<close>
   by (auto simp add: map_bit_def algebra_simps mod2_eq_if push_bit_add mult_2
     elim: evenE oddE)
 
 lemma set_bit_0 [simp]:
   \<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
   by (simp add: set_bit_def)
 
 lemma set_bit_Suc [simp]:
   \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close>
   by (simp add: set_bit_def)
 
 lemma unset_bit_0 [simp]:
   \<open>unset_bit 0 a = 2 * (a div 2)\<close>
   by (simp add: unset_bit_def)
 
 lemma unset_bit_Suc [simp]:
   \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
   by (simp add: unset_bit_def)
 
 lemma flip_bit_0 [simp]:
   \<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
   by (simp add: flip_bit_def)
 
 lemma flip_bit_Suc [simp]:
   \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
   by (simp add: flip_bit_def)
 
 sublocale "and": semilattice \<open>(AND)\<close>
   by standard (auto simp add: bit_eq_iff bit_and_iff)
 
 sublocale or: semilattice_neutr \<open>(OR)\<close> 0
   by standard (auto simp add: bit_eq_iff bit_or_iff)
 
 sublocale xor: comm_monoid \<open>(XOR)\<close> 0
   by standard (auto simp add: bit_eq_iff bit_xor_iff)
 
 lemma zero_and_eq [simp]:
   "0 AND a = 0"
   by (simp add: bit_eq_iff bit_and_iff)
 
 lemma and_zero_eq [simp]:
   "a AND 0 = 0"
   by (simp add: bit_eq_iff bit_and_iff)
 
 lemma one_and_eq [simp]:
   "1 AND a = of_bool (odd a)"
   by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff)
 
 lemma and_one_eq [simp]:
   "a AND 1 = of_bool (odd a)"
   using one_and_eq [of a] by (simp add: ac_simps)
 
 lemma one_or_eq [simp]:
   "1 OR a = a + of_bool (even a)"
   by (simp add: bit_eq_iff bit_or_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff)
 
 lemma or_one_eq [simp]:
   "a OR 1 = a + of_bool (even a)"
   using one_or_eq [of a] by (simp add: ac_simps)
 
 lemma one_xor_eq [simp]:
   "1 XOR a = a + of_bool (even a) - of_bool (odd a)"
   by (simp add: bit_eq_iff bit_xor_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff odd_bit_iff_bit_pred elim: oddE)
 
 lemma xor_one_eq [simp]:
   "a XOR 1 = a + of_bool (even a) - of_bool (odd a)"
   using one_xor_eq [of a] by (simp add: ac_simps)
 
 lemma take_bit_and [simp]:
   \<open>take_bit n (a AND b) = take_bit n a AND take_bit n b\<close>
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_and_iff)
 
 lemma take_bit_or [simp]:
   \<open>take_bit n (a OR b) = take_bit n a OR take_bit n b\<close>
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_or_iff)
 
 lemma take_bit_xor [simp]:
   \<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)
 
 end
 
 class ring_bit_operations = semiring_bit_operations + ring_parity +
   fixes not :: \<open>'a \<Rightarrow> 'a\<close>  (\<open>NOT\<close>)
   assumes bit_not_iff: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
   assumes minus_eq_not_minus_1: \<open>- a = NOT (a - 1)\<close>
 begin
 
 text \<open>
   For the sake of code generation \<^const>\<open>not\<close> is specified as
   definitional class operation.  Note that \<^const>\<open>not\<close> has no
   sensible definition for unlimited but only positive bit strings
   (type \<^typ>\<open>nat\<close>).
 \<close>
 
 lemma bits_minus_1_mod_2_eq [simp]:
   \<open>(- 1) mod 2 = 1\<close>
   by (simp add: mod_2_eq_odd)
 
 lemma not_eq_complement:
   \<open>NOT a = - a - 1\<close>
   using minus_eq_not_minus_1 [of \<open>a + 1\<close>] by simp
 
 lemma minus_eq_not_plus_1:
   \<open>- a = NOT a + 1\<close>
   using not_eq_complement [of a] by simp
 
 lemma bit_minus_iff:
   \<open>bit (- a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit (a - 1) n\<close>
   by (simp add: minus_eq_not_minus_1 bit_not_iff)
 
 lemma even_not_iff [simp]:
   "even (NOT a) \<longleftrightarrow> odd a"
   using bit_not_iff [of a 0] by auto
 
 lemma bit_not_exp_iff:
   \<open>bit (NOT (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<noteq> m\<close>
   by (auto simp add: bit_not_iff bit_exp_iff)
 
 lemma bit_minus_1_iff [simp]:
   \<open>bit (- 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close>
   by (simp add: bit_minus_iff)
 
 lemma bit_minus_exp_iff:
   \<open>bit (- (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<ge> m\<close>
   oops
 
 lemma bit_minus_2_iff [simp]:
   \<open>bit (- 2) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n > 0\<close>
   by (simp add: bit_minus_iff bit_1_iff)
 
 lemma not_one [simp]:
   "NOT 1 = - 2"
   by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)
 
 sublocale "and": semilattice_neutr \<open>(AND)\<close> \<open>- 1\<close>
   apply standard
   apply (auto simp add: bit_eq_iff bit_and_iff)
   apply (simp add: bit_exp_iff)
   apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
   done
 
 sublocale bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
   rewrites \<open>bit.xor = (XOR)\<close>
 proof -
   interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
     apply standard
          apply simp_all
        apply (auto simp add: bit_eq_iff bit_and_iff bit_or_iff bit_not_iff)
     apply (simp add: bit_exp_iff)
     apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
     done
   show \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
     by standard
   show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close> 
     apply (auto simp add: fun_eq_iff bit.xor_def bit_eq_iff bit_and_iff bit_or_iff bit_not_iff bit_xor_iff)
          apply (simp_all add: bit_exp_iff, simp_all add: bit_def)
         apply (metis local.bit_exp_iff local.bits_div_by_0)
        apply (metis local.bit_exp_iff local.bits_div_by_0)
     done
 qed
 
 lemma push_bit_minus:
   \<open>push_bit n (- a) = - push_bit n a\<close>
   by (simp add: push_bit_eq_mult)
 
 lemma take_bit_not_take_bit:
   \<open>take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\<close>
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff)
 
 lemma take_bit_not_iff:
   "take_bit n (NOT a) = take_bit n (NOT b) \<longleftrightarrow> take_bit n a = take_bit n b"
   apply (simp add: bit_eq_iff bit_not_iff bit_take_bit_iff)
   apply (simp add: bit_exp_iff)
   apply (use local.exp_eq_0_imp_not_bit in blast)
   done
 
 end
 
 
 subsubsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
 
 locale zip_nat = single: abel_semigroup f
-    for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl "\<^bold>*" 70) +
-  assumes end_of_bits: "\<not> False \<^bold>* False"
+    for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl \<open>\<^bold>*\<close> 70) +
+  assumes end_of_bits: \<open>\<not> False \<^bold>* False\<close>
 begin
 
-lemma False_P_imp:
-  "False \<^bold>* True \<and> P" if "False \<^bold>* P"
-  using that end_of_bits by (cases P) simp_all
-
-function F :: "nat \<Rightarrow> nat \<Rightarrow> nat"  (infixl "\<^bold>\<times>" 70)
-  where "m \<^bold>\<times> n = (if m = 0 \<and> n = 0 then 0
-    else of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2)"
+function F :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>  (infixl \<open>\<^bold>\<times>\<close> 70)
+  where \<open>m \<^bold>\<times> n = (if m = 0 \<and> n = 0 then 0
+    else of_bool (odd m \<^bold>* odd n) + 2 * ((m div 2) \<^bold>\<times> (n div 2)))\<close>
   by auto
 
 termination
   by (relation "measure (case_prod (+))") auto
 
-lemma zero_left_eq:
-  "0 \<^bold>\<times> n = of_bool (False \<^bold>* True) * n"
-  by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits)
-
-lemma zero_right_eq:
-  "m \<^bold>\<times> 0 = of_bool (True \<^bold>* False) * m"
-  by (induction m rule: nat_bit_induct) (simp_all add: end_of_bits)
-
-lemma simps [simp]:
-  "0 \<^bold>\<times> 0 = 0"
-  "0 \<^bold>\<times> n = of_bool (False \<^bold>* True) * n"
-  "m \<^bold>\<times> 0 = of_bool (True \<^bold>* False) * m"
-  "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> m \<^bold>\<times> n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2"
-  by (simp_all only: zero_left_eq zero_right_eq) simp
+declare F.simps [simp del]
 
 lemma rec:
   "m \<^bold>\<times> n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2"
-  by (cases "m = 0 \<and> n = 0") (auto simp add: end_of_bits)
+proof (cases \<open>m = 0 \<and> n = 0\<close>)
+  case True
+  then have \<open>m \<^bold>\<times> n = 0\<close>
+    using True by (simp add: F.simps [of 0 0])
+  moreover have \<open>(m div 2) \<^bold>\<times> (n div 2) = m \<^bold>\<times> n\<close>
+    using True by simp
+  ultimately show ?thesis
+    using True by (simp add: end_of_bits)
+next
+  case False
+  then show ?thesis
+    by (auto simp add: ac_simps F.simps [of m n])
+qed
 
-declare F.simps [simp del]
+lemma bit_eq_iff:
+  \<open>bit (m \<^bold>\<times> n) q \<longleftrightarrow> bit m q \<^bold>* bit n q\<close>
+proof (induction q arbitrary: m n)
+  case 0
+  then show ?case
+    by (simp add: rec [of m n])
+next
+  case (Suc n)
+  then show ?case
+    by (simp add: rec [of m n])
+qed
 
 sublocale abel_semigroup F
-proof
-  show "m \<^bold>\<times> n \<^bold>\<times> q = m \<^bold>\<times> (n \<^bold>\<times> q)" for m n q :: nat
-  proof (induction m arbitrary: n q rule: nat_bit_induct)
-    case zero
-    show ?case
-      by simp
-  next
-    case (even m)
-    with rec [of "2 * m"] rec [of _ q] show ?case
-      by (cases "even n") (auto simp add: ac_simps dest: False_P_imp)
-  next
-    case (odd m)
-    with rec [of "Suc (2 * m)"] rec [of _ q] show ?case
-      by (cases "even n"; cases "even q")
-        (auto dest: False_P_imp simp add: ac_simps)
-  qed
-  show "m \<^bold>\<times> n = n \<^bold>\<times> m" for m n :: nat
-  proof (induction m arbitrary: n rule: nat_bit_induct)
-    case zero
-    show ?case
-      by (simp add: ac_simps)
-  next
-    case (even m)
-    with rec [of "2 * m" n] rec [of n "2 * m"] show ?case
-      by (simp add: ac_simps)
-  next
-    case (odd m)
-    with rec [of "Suc (2 * m)" n] rec [of n "Suc (2 * m)"] show ?case
-      by (simp add: ac_simps)
-  qed
-qed
-
-lemma self [simp]:
-  "n \<^bold>\<times> n = of_bool (True \<^bold>* True) * n"
-  by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits)
-
-lemma even_iff [simp]:
-  "even (m \<^bold>\<times> n) \<longleftrightarrow> \<not> (odd m \<^bold>* odd n)"
-proof (induction m arbitrary: n rule: nat_bit_induct)
-  case zero
-  show ?case
-    by (cases "even n") (simp_all add: end_of_bits)
-next
-  case (even m)
-  then show ?case
-    by (simp add: rec [of "2 * m"])
-next
-  case (odd m)
-  then show ?case
-    by (simp add: rec [of "Suc (2 * m)"])
-qed
+  by standard (simp_all add: Parity.bit_eq_iff bit_eq_iff ac_simps)
 
 end
 
 instantiation nat :: semiring_bit_operations
 begin
 
-global_interpretation and_nat: zip_nat "(\<and>)"
+global_interpretation and_nat: zip_nat \<open>(\<and>)\<close>
   defines and_nat = and_nat.F
   by standard auto
 
-global_interpretation and_nat: semilattice "(AND) :: nat \<Rightarrow> nat \<Rightarrow> nat"
+global_interpretation and_nat: semilattice \<open>(AND) :: nat \<Rightarrow> nat \<Rightarrow> nat\<close>
 proof (rule semilattice.intro, fact and_nat.abel_semigroup_axioms, standard)
-  show "n AND n = n" for n :: nat
-    by (simp add: and_nat.self)
+  show \<open>n AND n = n\<close> for n :: nat
+    by (simp add: bit_eq_iff and_nat.bit_eq_iff)
 qed
 
-declare and_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
-global_interpretation or_nat: zip_nat "(\<or>)"
+global_interpretation or_nat: zip_nat \<open>(\<or>)\<close>
   defines or_nat = or_nat.F
   by standard auto
 
-global_interpretation or_nat: semilattice "(OR) :: nat \<Rightarrow> nat \<Rightarrow> nat"
+global_interpretation or_nat: semilattice \<open>(OR) :: nat \<Rightarrow> nat \<Rightarrow> nat\<close>
 proof (rule semilattice.intro, fact or_nat.abel_semigroup_axioms, standard)
-  show "n OR n = n" for n :: nat
-    by (simp add: or_nat.self)
+  show \<open>n OR n = n\<close> for n :: nat
+    by (simp add: bit_eq_iff or_nat.bit_eq_iff)
 qed
 
-declare or_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
-global_interpretation xor_nat: zip_nat "(\<noteq>)"
+global_interpretation xor_nat: zip_nat \<open>(\<noteq>)\<close>
   defines xor_nat = xor_nat.F
   by standard auto
 
-declare xor_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
 instance proof
   fix m n q :: nat
   show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
-  proof (rule sym, induction q arbitrary: m n)
-    case 0
-    then show ?case
-      by (simp add: and_nat.even_iff)
-  next
-    case (Suc q)
-    with and_nat.rec [of m n] show ?case
-      by simp
-  qed
+    by (fact and_nat.bit_eq_iff)
   show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
-  proof (rule sym, induction q arbitrary: m n)
-    case 0
-    then show ?case
-      by (simp add: or_nat.even_iff)
-  next
-    case (Suc q)
-    with or_nat.rec [of m n] show ?case
-      by simp
-  qed
+    by (fact or_nat.bit_eq_iff)
   show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
-  proof (rule sym, induction q arbitrary: m n)
-    case 0
-    then show ?case
-      by (simp add: xor_nat.even_iff)
-  next
-    case (Suc q)
-    with xor_nat.rec [of m n] show ?case
-      by simp
-  qed
+    by (fact xor_nat.bit_eq_iff)
 qed
 
 end
 
-global_interpretation or_nat: semilattice_neutr "(OR)" "0 :: nat"
-  by standard simp
-
-global_interpretation xor_nat: comm_monoid "(XOR)" "0 :: nat"
-  by standard simp
-
 lemma Suc_0_and_eq [simp]:
   \<open>Suc 0 AND n = of_bool (odd n)\<close>
   using one_and_eq [of n] by simp
 
 lemma and_Suc_0_eq [simp]:
   \<open>n AND Suc 0 = of_bool (odd n)\<close>
   using and_one_eq [of n] by simp
 
 lemma Suc_0_or_eq [simp]:
   \<open>Suc 0 OR n = n + of_bool (even n)\<close>
   using one_or_eq [of n] by simp
 
 lemma or_Suc_0_eq [simp]:
   \<open>n OR Suc 0 = n + of_bool (even n)\<close>
   using or_one_eq [of n] by simp
 
 lemma Suc_0_xor_eq [simp]:
   \<open>Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)\<close>
   using one_xor_eq [of n] by simp
 
 lemma xor_Suc_0_eq [simp]:
   \<open>n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)\<close>
   using xor_one_eq [of n] by simp
 
 
 subsubsection \<open>Instance \<^typ>\<open>int\<close>\<close>
 
-abbreviation (input) complement :: "int \<Rightarrow> int"
-  where "complement k \<equiv> - k - 1"
-
-lemma complement_half:
-  "complement (k * 2) div 2 = complement k"
-  by simp
-
-lemma complement_div_2:
-  "complement (k div 2) = complement k div 2"
-  by linarith
-
 locale zip_int = single: abel_semigroup f
-  for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl "\<^bold>*" 70)
+  for f :: \<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>  (infixl \<open>\<^bold>*\<close> 70)
 begin
- 
-lemma False_False_imp_True_True:
-  "True \<^bold>* True" if "False \<^bold>* False"
-proof (rule ccontr)
-  assume "\<not> True \<^bold>* True"
-  with that show False
-    using single.assoc [of False True True]
-    by (cases "False \<^bold>* True") simp_all
-qed
 
-function F :: "int \<Rightarrow> int \<Rightarrow> int"  (infixl "\<^bold>\<times>" 70)
-  where "k \<^bold>\<times> l = (if k \<in> {0, - 1} \<and> l \<in> {0, - 1}
+function F :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>  (infixl \<open>\<^bold>\<times>\<close> 70)
+  where \<open>k \<^bold>\<times> l = (if k \<in> {0, - 1} \<and> l \<in> {0, - 1}
     then - of_bool (odd k \<^bold>* odd l)
-    else of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2)"
+    else of_bool (odd k \<^bold>* odd l) + 2 * ((k div 2) \<^bold>\<times> (l div 2)))\<close>
   by auto
 
 termination
   by (relation "measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>))") auto
 
-lemma zero_left_eq:
-  "0 \<^bold>\<times> l = (case (False \<^bold>* False, False \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> l
-     | (True, False) \<Rightarrow> complement l
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction l rule: int_bit_induct)
-   (simp_all split: bool.split) 
-
-lemma minus_left_eq:
-  "- 1 \<^bold>\<times> l = (case (True \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> l
-     | (True, False) \<Rightarrow> complement l
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction l rule: int_bit_induct)
-   (simp_all split: bool.split) 
-
-lemma zero_right_eq:
-  "k \<^bold>\<times> 0 = (case (False \<^bold>* False, False \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, False) \<Rightarrow> complement k
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction k rule: int_bit_induct)
-    (simp_all add: ac_simps split: bool.split)
-
-lemma minus_right_eq:
-  "k \<^bold>\<times> - 1 = (case (True \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, False) \<Rightarrow> complement k
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction k rule: int_bit_induct)
-    (simp_all add: ac_simps split: bool.split)
-
-lemma simps [simp]:
-  "0 \<^bold>\<times> 0 = - of_bool (False \<^bold>* False)"
-  "- 1 \<^bold>\<times> 0 = - of_bool (True \<^bold>* False)"
-  "0 \<^bold>\<times> - 1 = - of_bool (False \<^bold>* True)"
-  "- 1 \<^bold>\<times> - 1 = - of_bool (True \<^bold>* True)"
-  "0 \<^bold>\<times> l = (case (False \<^bold>* False, False \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> l
-     | (True, False) \<Rightarrow> complement l
-     | (True, True) \<Rightarrow> - 1)"
-  "- 1 \<^bold>\<times> l = (case (True \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> l
-     | (True, False) \<Rightarrow> complement l
-     | (True, True) \<Rightarrow> - 1)"
-  "k \<^bold>\<times> 0 = (case (False \<^bold>* False, False \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, False) \<Rightarrow> complement k
-     | (True, True) \<Rightarrow> - 1)"
-  "k \<^bold>\<times> - 1 = (case (True \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, False) \<Rightarrow> complement k
-     | (True, True) \<Rightarrow> - 1)"
-  "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> l \<noteq> - 1
-    \<Longrightarrow> k \<^bold>\<times> l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2"
-  by simp_all[4] (simp_all only: zero_left_eq minus_left_eq zero_right_eq minus_right_eq, simp)
-
 declare F.simps [simp del]
 
 lemma rec:
-  "k \<^bold>\<times> l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2"
-  by (cases "k \<in> {0, - 1} \<and> l \<in> {0, - 1}") (auto simp add: ac_simps F.simps [of k l] split: bool.split)
+  \<open>k \<^bold>\<times> l = of_bool (odd k \<^bold>* odd l) + 2 * ((k div 2) \<^bold>\<times> (l div 2))\<close>
+proof (cases \<open>k \<in> {0, - 1} \<and> l \<in> {0, - 1}\<close>)
+  case True
+  then have \<open>(k div 2) \<^bold>\<times> (l div 2) = k \<^bold>\<times> l\<close>
+    by auto
+  moreover have \<open>of_bool (odd k \<^bold>* odd l) = - (k \<^bold>\<times> l)\<close>
+    using True by (simp add: F.simps [of k l])
+  ultimately show ?thesis by simp
+next
+  case False
+  then show ?thesis
+    by (auto simp add: ac_simps F.simps [of k l])
+qed
+
+lemma bit_eq_iff:
+  \<open>bit (k \<^bold>\<times> l) n \<longleftrightarrow> bit k n \<^bold>* bit l n\<close>
+proof (induction n arbitrary: k l)
+  case 0
+  then show ?case
+    by (simp add: rec [of k l])
+next
+  case (Suc n)
+  then show ?case
+    by (simp add: rec [of k l])
+qed
 
 sublocale abel_semigroup F
-proof
-  show "k \<^bold>\<times> l \<^bold>\<times> r = k \<^bold>\<times> (l \<^bold>\<times> r)" for k l r :: int
-  proof (induction k arbitrary: l r rule: int_bit_induct)
-    case zero
-    have "complement l \<^bold>\<times> r = complement (l \<^bold>\<times> r)" if "False \<^bold>* False" "\<not> False \<^bold>* True"
-    proof (induction l arbitrary: r rule: int_bit_induct)
-      case zero
-      from that show ?case
-        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case minus
-      from that show ?case
-        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case (even l)
-      with that rec [of _ r] show ?case
-        by (cases "even r")
-          (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case (odd l)
-      moreover have "- l - 1 = - 1 - l"
-        by simp
-      ultimately show ?case
-        using that rec [of _ r]
-        by (cases "even r")
-          (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    qed
-    then show ?case
-      by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-  next
-    case minus
-    have "complement l \<^bold>\<times> r = complement (l \<^bold>\<times> r)" if "\<not> True \<^bold>* True" "False \<^bold>* True"
-    proof (induction l arbitrary: r rule: int_bit_induct)
-      case zero
-      from that show ?case
-        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case minus
-      from that show ?case
-        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case (even l)
-      with that rec [of _ r] show ?case
-        by (cases "even r")
-          (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case (odd l)
-      moreover have "- l - 1 = - 1 - l"
-        by simp
-      ultimately show ?case
-        using that rec [of _ r]
-        by (cases "even r")
-          (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    qed
-    then show ?case
-      by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-  next
-    case (even k)
-    with rec [of "k * 2"] rec [of _ r] show ?case
-      by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True)
-  next
-    case (odd k)
-    with rec [of "1 + k * 2"] rec [of _ r] show ?case
-      by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True)
-  qed
-  show "k \<^bold>\<times> l = l \<^bold>\<times> k" for k l :: int
-  proof (induction k arbitrary: l rule: int_bit_induct)
-    case zero
-    show ?case
-      by simp
-  next
-    case minus
-    show ?case
-      by simp
-  next
-    case (even k)
-    with rec [of "k * 2" l] rec [of l "k * 2"] show ?case
-      by (simp add: ac_simps)
-  next
-    case (odd k)
-    with rec [of "k * 2 + 1" l] rec [of l "k * 2 + 1"] show ?case
-      by (simp add: ac_simps)
-  qed
-qed
-
-lemma self [simp]:
-  "k \<^bold>\<times> k = (case (False \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction k rule: int_bit_induct) (auto simp add: False_False_imp_True_True split: bool.split)
-
-lemma even_iff [simp]:
-  "even (k \<^bold>\<times> l) \<longleftrightarrow> \<not> (odd k \<^bold>* odd l)"
-proof (induction k arbitrary: l rule: int_bit_induct)
-  case zero
-  show ?case
-    by (cases "even l") (simp_all split: bool.splits)
-next
-  case minus
-  show ?case
-    by (cases "even l") (simp_all split: bool.splits)
-next
-  case (even k)
-  then show ?case
-    by (simp add: rec [of "k * 2"])
-next
-  case (odd k)
-  then show ?case
-    by (simp add: rec [of "1 + k * 2"])
-qed
+  by standard (simp_all add: Parity.bit_eq_iff bit_eq_iff ac_simps)
 
 end
 
 instantiation int :: ring_bit_operations
 begin
 
-definition not_int :: "int \<Rightarrow> int"
-  where "not_int = complement"
-
 global_interpretation and_int: zip_int "(\<and>)"
   defines and_int = and_int.F
   by standard
 
-declare and_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
 global_interpretation and_int: semilattice "(AND) :: int \<Rightarrow> int \<Rightarrow> int"
 proof (rule semilattice.intro, fact and_int.abel_semigroup_axioms, standard)
   show "k AND k = k" for k :: int
-    by (simp add: and_int.self)
+    by (simp add: bit_eq_iff and_int.bit_eq_iff)
 qed
 
 global_interpretation or_int: zip_int "(\<or>)"
   defines or_int = or_int.F
   by standard
 
-declare or_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
 global_interpretation or_int: semilattice "(OR) :: int \<Rightarrow> int \<Rightarrow> int"
 proof (rule semilattice.intro, fact or_int.abel_semigroup_axioms, standard)
   show "k OR k = k" for k :: int
-    by (simp add: or_int.self)
+    by (simp add: bit_eq_iff or_int.bit_eq_iff)
 qed
 
 global_interpretation xor_int: zip_int "(\<noteq>)"
   defines xor_int = xor_int.F
   by standard
 
-declare xor_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
+definition not_int :: \<open>int \<Rightarrow> int\<close>
+  where \<open>not_int k = - k - 1\<close>
+
+lemma not_int_rec:
+  "NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
+  by (auto simp add: not_int_def elim: oddE)
+
+lemma even_not_iff_int:
+  \<open>even (NOT k) \<longleftrightarrow> odd k\<close> for k :: int
+  by (simp add: not_int_def)
+
+lemma not_int_div_2:
+  \<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
+  by (simp add: not_int_def)
 
 lemma bit_not_iff_int:
   \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
     for k :: int
-    by (induction n arbitrary: k)
-      (simp_all add: not_int_def flip: complement_div_2)
+  by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int)
 
 instance proof
   fix k l :: int and n :: nat
   show \<open>- k = NOT (k - 1)\<close>
     by (simp add: not_int_def)
   show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
-  proof (rule sym, induction n arbitrary: k l)
-    case 0
-    then show ?case
-      by (simp add: and_int.even_iff)
-  next
-    case (Suc n)
-    with and_int.rec [of k l] show ?case
-      by simp
-  qed
+    by (fact and_int.bit_eq_iff)
   show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
-  proof (rule sym, induction n arbitrary: k l)
-    case 0
-    then show ?case
-      by (simp add: or_int.even_iff)
-  next
-    case (Suc n)
-    with or_int.rec [of k l] show ?case
-      by simp
-  qed
+    by (fact or_int.bit_eq_iff)
   show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
-  proof (rule sym, induction n arbitrary: k l)
-    case 0
-    then show ?case
-      by (simp add: xor_int.even_iff)
-  next
-    case (Suc n)
-    with xor_int.rec [of k l] show ?case
-      by simp
-  qed
-qed (simp_all add: minus_1_div_exp_eq_int bit_not_iff_int)
+    by (fact xor_int.bit_eq_iff)
+qed (simp_all add: bit_not_iff_int)
 
 end
 
-lemma not_int_div_2:
-  "NOT k div 2 = NOT (k div 2)" for k :: int
-  by (simp add: complement_div_2 not_int_def)
-
-lemma not_int_rec [simp]:
-  "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
-  by (auto simp add: not_int_def elim: oddE)
-
 end