# HG changeset patch
# User haftmann
# Date 1574023475 0
# Node ID 9de7f10675209f8f70a89a31e4013956f1f7193e
# Parent  3c0a26b8b49a171d221b4fc7eadee33f770ee642
strengthened type class for bit operations

diff -r 3c0a26b8b49a -r 9de7f1067520 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Nov 15 21:09:03 2019 +0100
+++ b/src/HOL/Code_Numeral.thy	Sun Nov 17 20:44:35 2019 +0000
@@ -297,7 +297,9 @@
   is \<open>drop_bit\<close> .
 
 instance by (standard; transfer)
-  (fact bit_split_eq bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div)+
+  (fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
+    bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
+    div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
 
 end
 
@@ -991,7 +993,9 @@
   is \<open>drop_bit\<close> .
 
 instance by (standard; transfer)
-  (fact bit_split_eq bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div)+
+  (fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
+    bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
+    div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
 
 end
 
diff -r 3c0a26b8b49a -r 9de7f1067520 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Nov 15 21:09:03 2019 +0100
+++ b/src/HOL/Divides.thy	Sun Nov 17 20:44:35 2019 +0000
@@ -393,26 +393,6 @@
                    zero_less_mult_iff distrib_left [symmetric]
                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
 
-lemma zdiv_zmult2_eq:
-  fixes a b c :: int
-  assumes "0 \<le> c"
-  shows "a div (b * c) = (a div b) div c"
-proof (cases "b = 0")
-  case False
-  with assms show ?thesis
-    by (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
-qed auto
-
-lemma zmod_zmult2_eq:
-  fixes a b c :: int
-  assumes "0 \<le> c"
-  shows "a mod (b * c) = b * (a div b mod c) + a mod b"
-proof (cases "b = 0")
-  case False
-  with assms show ?thesis
-    by (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
-qed auto
-
 lemma div_pos_geq:
   fixes k l :: int
   assumes "0 < l" and "l \<le> k"
diff -r 3c0a26b8b49a -r 9de7f1067520 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Fri Nov 15 21:09:03 2019 +0100
+++ b/src/HOL/Lattices.thy	Sun Nov 17 20:44:35 2019 +0000
@@ -772,6 +772,14 @@
 lemma split_max [no_atp]: "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
   by (simp add: max_def)
 
+lemma split_min_lin [no_atp]:
+  \<open>P (min a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P a) \<and> (b < a \<longrightarrow> P b)\<close>
+  by (cases a b rule: linorder_cases) (auto simp add: min.absorb1 min.absorb2)
+
+lemma split_max_lin [no_atp]:
+  \<open>P (max a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P b) \<and> (b < a \<longrightarrow> P a)\<close>
+  by (cases a b rule: linorder_cases) (auto simp add: max.absorb1 max.absorb2)
+
 lemma min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" for f :: "'a \<Rightarrow> 'b::linorder"
   by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
 
diff -r 3c0a26b8b49a -r 9de7f1067520 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Fri Nov 15 21:09:03 2019 +0100
+++ b/src/HOL/Parity.thy	Sun Nov 17 20:44:35 2019 +0000
@@ -480,6 +480,17 @@
   finally show ?thesis .
 qed
 
+lemma exp_mod_exp:
+  \<open>2 ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close>
+proof -
+  have \<open>(2::nat) ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close> (is \<open>?lhs = ?rhs\<close>)
+    by (auto simp add: not_less monoid_mult_class.power_add dest!: le_Suc_ex)
+  then have \<open>of_nat ?lhs = of_nat ?rhs\<close>
+    by simp
+  then show ?thesis
+    by (simp add: of_nat_mod)
+qed
+
 end
 
 class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat
@@ -600,6 +611,7 @@
   qed
 qed
 
+
 subsection \<open>Parity and powers\<close>
 
 context ring_1
@@ -745,16 +757,99 @@
 lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
   by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
 
+lemma zdiv_zmult2_eq:
+  \<open>a div (b * c) = (a div b) div c\<close> if \<open>c \<ge> 0\<close> for a b c :: int
+proof (cases \<open>b \<ge> 0\<close>)
+  case True
+  with that show ?thesis
+    using div_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
+next
+  case False
+  with that show ?thesis
+    using div_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
+qed
+
+lemma zmod_zmult2_eq:
+  \<open>a mod (b * c) = b * (a div b mod c) + a mod b\<close> if \<open>c \<ge> 0\<close> for a b c :: int
+proof (cases \<open>b \<ge> 0\<close>)
+  case True
+  with that show ?thesis
+    using mod_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
+next
+  case False
+  with that show ?thesis
+    using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
+qed
+
 
 subsection \<open>Abstract bit shifts\<close>
 
 class semiring_bits = semiring_parity +
-  assumes bit_split_eq: \<open>\<And>a. of_bool (odd a) + 2 * (a div 2) = a\<close>
-    and bit_eq_rec: \<open>\<And>a b. a = b \<longleftrightarrow> (even a = even b) \<and> a div 2 = b div 2\<close>
+  assumes bit_eq_rec: \<open>a = b \<longleftrightarrow> (even a = even b) \<and> a div 2 = b div 2\<close>
     and bit_induct [case_names stable rec]:
     \<open>(\<And>a. a div 2 = a \<Longrightarrow> P a)
      \<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a))
         \<Longrightarrow> P a\<close>
+  assumes bits_div_0 [simp]: \<open>0 div a = 0\<close>
+    and bits_div_by_1 [simp]: \<open>a div 1 = a\<close>
+    and bit_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
+    and even_succ_div_2 [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
+    and div_exp_eq: \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close>
+    and mod_exp_eq: \<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close>
+    and mult_exp_mod_exp_eq: \<open>m \<le> n \<Longrightarrow> (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\<close>
+    and div_exp_mod_exp_eq: \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
+begin
+
+lemma bits_1_div_2 [simp]:
+  \<open>1 div 2 = 0\<close>
+  using even_succ_div_2 [of 0] by simp
+
+lemma bits_1_div_exp [simp]:
+  \<open>1 div 2 ^ n = of_bool (n = 0)\<close>
+  using div_exp_eq [of 1 1] by (cases n) simp_all
+
+lemma even_succ_div_exp [simp]:
+  \<open>(1 + a) div 2 ^ n = a div 2 ^ n\<close> if \<open>even a\<close> and \<open>n > 0\<close>
+proof (cases n)
+  case 0
+  with that show ?thesis
+    by simp
+next
+  case (Suc n)
+  with \<open>even a\<close> have \<open>(1 + a) div 2 ^ Suc n = a div 2 ^ Suc n\<close>
+  proof (induction n)
+    case 0
+    then show ?case
+      by simp
+  next
+    case (Suc n)
+    then show ?case
+      using div_exp_eq [of _ 1 \<open>Suc n\<close>, symmetric]
+      by simp
+  qed
+  with Suc show ?thesis
+    by simp
+qed
+
+lemma even_succ_mod_exp [simp]:
+  \<open>(1 + a) mod 2 ^ n = 1 + (a mod 2 ^ n)\<close> if \<open>even a\<close> and \<open>n > 0\<close>
+  using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] that
+  apply simp
+  by (metis local.add.left_commute local.add_left_cancel local.div_mult_mod_eq)
+
+lemma bits_mod_by_1 [simp]:
+  \<open>a mod 1 = 0\<close>
+  using div_mult_mod_eq [of a 1] by simp
+
+lemma bits_mod_0 [simp]:
+  \<open>0 mod a = 0\<close>
+  using div_mult_mod_eq [of 0 a] by simp
+
+lemma one_mod_two_eq_one [simp]:
+  \<open>1 mod 2 = 1\<close>
+  by (simp add: mod2_eq_if)
+
+end
 
 lemma nat_bit_induct [case_names zero even odd]:
   "P n" if zero: "P 0"
@@ -787,9 +882,6 @@
 
 instance nat :: semiring_bits
 proof
-  show \<open>of_bool (odd n) + 2 * (n div 2) = n\<close>
-    for n :: nat
-    by simp
   show \<open>m = n \<longleftrightarrow> (even m \<longleftrightarrow> even n) \<and> m div 2 = n div 2\<close>
     for m n :: nat
     by (auto dest: odd_two_times_div_two_succ)
@@ -809,7 +901,18 @@
     with rec [of n True] show ?case
       by simp
   qed
-qed
+  show \<open>q mod 2 ^ m mod 2 ^ n = q mod 2 ^ min m n\<close>
+    for q m n :: nat
+    apply (auto simp add: less_iff_Suc_add power_add mod_mod_cancel split: split_min_lin)
+    apply (metis div_mult2_eq mod_div_trivial mod_eq_self_iff_div_eq_0 mod_mult_self2_is_0 power_commutes)
+    done
+  show \<open>(q * 2 ^ m) mod (2 ^ n) = (q mod 2 ^ (n - m)) * 2 ^ m\<close> if \<open>m \<le> n\<close>
+    for q m n :: nat
+    using that
+    apply (auto simp add: mod_mod_cancel div_mult2_eq power_add mod_mult2_eq le_iff_add split: split_min_lin)
+    apply (simp add: mult.commute)
+    done
+qed (auto simp add: div_mult2_eq mod_mult2_eq power_add)
 
 lemma int_bit_induct [case_names zero minus even odd]:
   "P k" if zero_int: "P 0"
@@ -870,9 +973,6 @@
 
 instance int :: semiring_bits
 proof
-  show \<open>of_bool (odd k) + 2 * (k div 2) = k\<close>
-    for k :: int
-    by (auto elim: oddE)
   show \<open>k = l \<longleftrightarrow> (even k \<longleftrightarrow> even l) \<and> k div 2 = l div 2\<close>
     for k l :: int
     by (auto dest: odd_two_times_div_two_succ)
@@ -896,7 +996,21 @@
     with rec [of k True] show ?case
       by (simp add: ac_simps)
   qed
-qed
+  show \<open>k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n\<close>
+    for m n :: nat and k :: int
+    using mod_exp_eq [of \<open>nat k\<close> m n]
+    apply (auto simp add: mod_mod_cancel zdiv_zmult2_eq power_add zmod_zmult2_eq le_iff_add split: split_min_lin)
+     apply (auto simp add: less_iff_Suc_add mod_mod_cancel power_add)
+    apply (simp only: flip: mult.left_commute [of \<open>2 ^ m\<close>])
+    apply (subst zmod_zmult2_eq) apply simp_all
+    done
+  show \<open>(k * 2 ^ m) mod (2 ^ n) = (k mod 2 ^ (n - m)) * 2 ^ m\<close>
+    if \<open>m \<le> n\<close> for m n :: nat and k :: int
+    using that
+    apply (auto simp add: power_add zmod_zmult2_eq le_iff_add split: split_min_lin)
+    apply (simp add: ac_simps)
+    done
+qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add)
 
 class semiring_bit_shifts = semiring_bits +
   fixes push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
@@ -920,6 +1034,146 @@
   differently wrt. code generation.
 \<close>
 
+lemma bit_ident:
+  "push_bit n (drop_bit n a) + take_bit n a = a"
+  using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
+
+lemma push_bit_push_bit [simp]:
+  "push_bit m (push_bit n a) = push_bit (m + n) a"
+  by (simp add: push_bit_eq_mult power_add ac_simps)
+
+lemma push_bit_0_id [simp]:
+  "push_bit 0 = id"
+  by (simp add: fun_eq_iff push_bit_eq_mult)
+
+lemma push_bit_of_0 [simp]:
+  "push_bit n 0 = 0"
+  by (simp add: push_bit_eq_mult)
+
+lemma push_bit_of_1:
+  "push_bit n 1 = 2 ^ n"
+  by (simp add: push_bit_eq_mult)
+
+lemma push_bit_Suc [simp]:
+  "push_bit (Suc n) a = push_bit n (a * 2)"
+  by (simp add: push_bit_eq_mult ac_simps)
+
+lemma push_bit_double:
+  "push_bit n (a * 2) = push_bit n a * 2"
+  by (simp add: push_bit_eq_mult ac_simps)
+
+lemma push_bit_add:
+  "push_bit n (a + b) = push_bit n a + push_bit n b"
+  by (simp add: push_bit_eq_mult algebra_simps)
+
+lemma take_bit_0 [simp]:
+  "take_bit 0 a = 0"
+  by (simp add: take_bit_eq_mod)
+
+lemma take_bit_Suc [simp]:
+  \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
+proof -
+  have \<open>take_bit (Suc n) (a div 2 * 2 + of_bool (odd a)) = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
+    using even_succ_mod_exp [of \<open>2 * (a div 2)\<close> \<open>Suc n\<close>]
+      mult_exp_mod_exp_eq [of 1 \<open>Suc n\<close> \<open>a div 2\<close>]
+    by (auto simp add: take_bit_eq_mod ac_simps)
+  then show ?thesis
+    using div_mult_mod_eq [of a 2] by (simp add: mod_2_eq_odd)
+qed
+
+lemma take_bit_of_0 [simp]:
+  "take_bit n 0 = 0"
+  by (simp add: take_bit_eq_mod)
+
+lemma take_bit_of_1 [simp]:
+  "take_bit n 1 = of_bool (n > 0)"
+  by (cases n) simp_all
+
+lemma drop_bit_of_0 [simp]:
+  "drop_bit n 0 = 0"
+  by (simp add: drop_bit_eq_div)
+
+lemma drop_bit_of_1 [simp]:
+  "drop_bit n 1 = of_bool (n = 0)"
+  by (simp add: drop_bit_eq_div)
+
+lemma drop_bit_0 [simp]:
+  "drop_bit 0 = id"
+  by (simp add: fun_eq_iff drop_bit_eq_div)
+
+lemma drop_bit_Suc [simp]:
+  "drop_bit (Suc n) a = drop_bit n (a div 2)"
+  using div_exp_eq [of a 1] by (simp add: drop_bit_eq_div)
+
+lemma drop_bit_half:
+  "drop_bit n (a div 2) = drop_bit n a div 2"
+  by (induction n arbitrary: a) simp_all
+
+lemma drop_bit_of_bool [simp]:
+  "drop_bit n (of_bool d) = of_bool (n = 0 \<and> d)"
+  by (cases n) simp_all
+
+lemma take_bit_eq_0_imp_dvd:
+  "take_bit n a = 0 \<Longrightarrow> 2 ^ n dvd a"
+  by (simp add: take_bit_eq_mod mod_0_imp_dvd)
+
+lemma even_take_bit_eq [simp]:
+  \<open>even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a\<close>
+  by (cases n) simp_all
+
+lemma take_bit_take_bit [simp]:
+  "take_bit m (take_bit n a) = take_bit (min m n) a"
+  by (simp add: take_bit_eq_mod mod_exp_eq ac_simps)
+
+lemma drop_bit_drop_bit [simp]:
+  "drop_bit m (drop_bit n a) = drop_bit (m + n) a"
+  by (simp add: drop_bit_eq_div power_add div_exp_eq ac_simps)
+
+lemma push_bit_take_bit:
+  "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)"
+  apply (simp add: push_bit_eq_mult take_bit_eq_mod power_add ac_simps)
+  using mult_exp_mod_exp_eq [of m \<open>m + n\<close> a] apply (simp add: ac_simps power_add)
+  done
+
+lemma take_bit_push_bit:
+  "take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)"
+proof (cases "m \<le> n")
+  case True
+  then show ?thesis
+    apply (simp add:)
+    apply (simp_all add: push_bit_eq_mult take_bit_eq_mod)
+    apply (auto dest!: le_Suc_ex simp add: power_add ac_simps)
+    using mult_exp_mod_exp_eq [of m m \<open>a * 2 ^ n\<close> for n]
+    apply (simp add: ac_simps)
+    done
+next
+  case False
+  then show ?thesis
+    using push_bit_take_bit [of n "m - n" a]
+    by simp
+qed
+
+lemma take_bit_drop_bit:
+  "take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)"
+  by (simp add: drop_bit_eq_div take_bit_eq_mod ac_simps div_exp_mod_exp_eq)
+
+lemma drop_bit_take_bit:
+  "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)"
+proof (cases "m \<le> n")
+  case True
+  then show ?thesis
+    using take_bit_drop_bit [of "n - m" m a] by simp
+next
+  case False
+  then obtain q where \<open>m = n + q\<close>
+    by (auto simp add: not_le dest: less_imp_Suc_add)
+  then have \<open>drop_bit m (take_bit n a) = 0\<close>
+    using div_exp_eq [of \<open>a mod 2 ^ n\<close> n q]
+    by (simp add: take_bit_eq_mod drop_bit_eq_div)
+  with False show ?thesis
+    by simp
+qed
+
 end
 
 instantiation nat :: semiring_bit_shifts
@@ -962,115 +1216,18 @@
   unique_euclidean_semiring_with_nat + semiring_bit_shifts
 begin
 
-lemma bit_ident:
-  "push_bit n (drop_bit n a) + take_bit n a = a"
-  using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
-
-lemma push_bit_push_bit [simp]:
-  "push_bit m (push_bit n a) = push_bit (m + n) a"
-  by (simp add: push_bit_eq_mult power_add ac_simps)
-
-lemma take_bit_take_bit [simp]:
-  "take_bit m (take_bit n a) = take_bit (min m n) a"
-proof (cases "m \<le> n")
-  case True
-  then show ?thesis
-    by (simp add: take_bit_eq_mod not_le min_def mod_mod_cancel le_imp_power_dvd)
-next
-  case False
-  then have "n < m" and "min m n = n"
-    by simp_all
-  then have "2 ^ m = of_nat (2 ^ n) * of_nat (2 ^ (m - n))"
-    by (simp add: power_add [symmetric])
-  then have "a mod 2 ^ n mod 2 ^ m = a mod 2 ^ n mod (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))"
-    by simp
-  also have "\<dots> = of_nat (2 ^ n) * (a mod 2 ^ n div of_nat (2 ^ n) mod of_nat (2 ^ (m - n))) + a mod 2 ^ n mod of_nat (2 ^ n)"
-    by (simp only: mod_mult2_eq')
-  finally show ?thesis
-    using \<open>min m n = n\<close> by (simp add: take_bit_eq_mod)
-qed
-
-lemma drop_bit_drop_bit [simp]:
-  "drop_bit m (drop_bit n a) = drop_bit (m + n) a"
-proof -
-  have "a div (2 ^ m * 2 ^ n) = a div (of_nat (2 ^ n) * of_nat (2 ^ m))"
-    by (simp add: ac_simps)
-  also have "\<dots> = a div of_nat (2 ^ n) div of_nat (2 ^ m)"
-    by (simp only: div_mult2_eq')
-  finally show ?thesis
-    by (simp add: drop_bit_eq_div power_add)
-qed
-
-lemma push_bit_take_bit:
-  "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)"
-  by (simp add: push_bit_eq_mult take_bit_eq_mod power_add mult_mod_right ac_simps)
+lemma take_bit_of_exp [simp]:
+  \<open>take_bit m (2 ^ n) = of_bool (n < m) * 2 ^ n\<close>
+  by (simp add: take_bit_eq_mod exp_mod_exp)
 
-lemma take_bit_push_bit:
-  "take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)"
-proof (cases "m \<le> n")
-  case True
-  then show ?thesis
-    by (simp_all add: push_bit_eq_mult take_bit_eq_mod mod_eq_0_iff_dvd dvd_power_le)
-next
-  case False
-  then show ?thesis
-    using push_bit_take_bit [of n "m - n" a]
-    by simp
-qed
-
-lemma take_bit_drop_bit:
-  "take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)"
-  using mod_mult2_eq' [of a "2 ^ n" "2 ^ m"]
-  by (simp add: drop_bit_eq_div take_bit_eq_mod power_add ac_simps)
-
-lemma drop_bit_take_bit:
-  "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)"
-proof (cases "m \<le> n")
-  case True
-  then show ?thesis
-    using take_bit_drop_bit [of "n - m" m a] by simp
-next
-  case False
-  then have "a mod 2 ^ n div 2 ^ m = a mod 2 ^ n div 2 ^ (n + (m - n))"
-    by simp
-  also have "\<dots> = a mod 2 ^ n div (2 ^ n * 2 ^ (m - n))"
-    by (simp add: power_add)
-  also have "\<dots> = a mod 2 ^ n div (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))"
-    by simp
-  also have "\<dots> = a mod 2 ^ n div of_nat (2 ^ n) div of_nat (2 ^ (m - n))"
-    by (simp only: div_mult2_eq')
-  finally show ?thesis
-    using False by (simp add: take_bit_eq_mod drop_bit_eq_div)
-qed
-
-lemma push_bit_0_id [simp]:
-  "push_bit 0 = id"
-  by (simp add: fun_eq_iff push_bit_eq_mult)
-
-lemma push_bit_of_0 [simp]:
-  "push_bit n 0 = 0"
-  by (simp add: push_bit_eq_mult)
-
-lemma push_bit_of_1:
-  "push_bit n 1 = 2 ^ n"
-  by (simp add: push_bit_eq_mult)
-
-lemma push_bit_Suc [simp]:
-  "push_bit (Suc n) a = push_bit n (a * 2)"
-  by (simp add: push_bit_eq_mult ac_simps)
-
-lemma push_bit_double:
-  "push_bit n (a * 2) = push_bit n a * 2"
-  by (simp add: push_bit_eq_mult ac_simps)
+lemma take_bit_of_2 [simp]:
+  \<open>take_bit n 2 = of_bool (2 \<le> n) * 2\<close>
+  using take_bit_of_exp [of n 1] by simp
 
 lemma push_bit_eq_0_iff [simp]:
   "push_bit n a = 0 \<longleftrightarrow> a = 0"
   by (simp add: push_bit_eq_mult)
 
-lemma push_bit_add:
-  "push_bit n (a + b) = push_bit n a + push_bit n b"
-  by (simp add: push_bit_eq_mult algebra_simps)
-
 lemma push_bit_numeral [simp]:
   "push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))"
   by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric]) (simp add: ac_simps)
@@ -1079,31 +1236,6 @@
   "push_bit n (of_nat m) = of_nat (push_bit n m)"
   by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult)
 
-lemma take_bit_0 [simp]:
-  "take_bit 0 a = 0"
-  by (simp add: take_bit_eq_mod)
-
-lemma take_bit_Suc [simp]:
-  "take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)"
-proof -
-  have "1 + 2 * (a div 2) mod (2 * 2 ^ n) = (a div 2 * 2 + a mod 2) mod (2 * 2 ^ n)"
-    if "odd a"
-    using that mod_mult2_eq' [of "1 + 2 * (a div 2)" 2 "2 ^ n"]
-    by (simp add: ac_simps odd_iff_mod_2_eq_one mult_mod_right)
-  also have "\<dots> = a mod (2 * 2 ^ n)"
-    by (simp only: div_mult_mod_eq)
-  finally show ?thesis
-    by (simp add: take_bit_eq_mod algebra_simps mult_mod_right)
-qed
-
-lemma take_bit_of_0 [simp]:
-  "take_bit n 0 = 0"
-  by (simp add: take_bit_eq_mod)
-
-lemma take_bit_of_1 [simp]:
-  "take_bit n 1 = of_bool (n > 0)"
-  by (simp add: take_bit_eq_mod)
-
 lemma take_bit_add:
   "take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)"
   by (simp add: take_bit_eq_mod mod_simps)
@@ -1116,10 +1248,6 @@
   "take_bit n 1 = 0 \<longleftrightarrow> n = 0"
   by (simp add: take_bit_eq_mod)
 
-lemma even_take_bit_eq [simp]:
-  "even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a"
-  by (cases n) (simp_all add: take_bit_eq_mod dvd_mod_iff)
-
 lemma take_bit_numeral_bit0 [simp]:
   "take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2"
   by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] take_bit_Suc
@@ -1134,45 +1262,6 @@
   "take_bit n (of_nat m) = of_nat (take_bit n m)"
   by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod of_nat_mod [of m "2 ^ n"])
 
-lemma drop_bit_0 [simp]:
-  "drop_bit 0 = id"
-  by (simp add: fun_eq_iff drop_bit_eq_div)
-
-lemma drop_bit_of_0 [simp]:
-  "drop_bit n 0 = 0"
-  by (simp add: drop_bit_eq_div)
-
-lemma drop_bit_of_1 [simp]:
-  "drop_bit n 1 = of_bool (n = 0)"
-  by (simp add: drop_bit_eq_div)
-
-lemma drop_bit_Suc [simp]:
-  "drop_bit (Suc n) a = drop_bit n (a div 2)"
-proof (cases "even a")
-  case True
-  then obtain b where "a = 2 * b" ..
-  moreover have "drop_bit (Suc n) (2 * b) = drop_bit n b"
-    by (simp add: drop_bit_eq_div)
-  ultimately show ?thesis
-    by simp
-next
-  case False
-  then obtain b where "a = 2 * b + 1" ..
-  moreover have "drop_bit (Suc n) (2 * b + 1) = drop_bit n b"
-    using div_mult2_eq' [of "1 + b * 2" 2 "2 ^ n"]
-    by (auto simp add: drop_bit_eq_div ac_simps)
-  ultimately show ?thesis
-    by simp
-qed
-
-lemma drop_bit_half:
-  "drop_bit n (a div 2) = drop_bit n a div 2"
-  by (induction n arbitrary: a) simp_all
-
-lemma drop_bit_of_bool [simp]:
-  "drop_bit n (of_bool d) = of_bool (n = 0 \<and> d)"
-  by (cases n) simp_all
-
 lemma drop_bit_numeral_bit0 [simp]:
   "drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)"
   by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] drop_bit_Suc
diff -r 3c0a26b8b49a -r 9de7f1067520 src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Fri Nov 15 21:09:03 2019 +0100
+++ b/src/HOL/ex/Word.thy	Sun Nov 17 20:44:35 2019 +0000
@@ -12,6 +12,10 @@
 
 subsection \<open>Preliminaries\<close>
 
+lemma length_not_greater_eq_2_iff [simp]:
+  \<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = 1\<close>
+  by (auto simp add: not_le dest: less_2_cases)
+
 lemma take_bit_uminus:
   "take_bit n (- (take_bit n k)) = take_bit n (- k)" for k :: int
   by (simp add: take_bit_eq_mod mod_minus_eq)
@@ -565,22 +569,14 @@
 
 instance word :: (len) semiring_bits
 proof
-  show \<open>of_bool (odd a) + 2 * (a div 2) = a\<close>
-    for a :: \<open>'a word\<close>
-    apply (cases \<open>even a\<close>; simp, transfer; cases rule: length_cases [where ?'a = 'a])
-      apply auto
-    apply (auto simp add: take_bit_eq_mod)
-    apply (metis add.commute even_take_bit_eq len_not_eq_0 mod_mod_trivial odd_two_times_div_two_succ take_bit_eq_mod)
-    done
   show \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close>
     for a b :: \<open>'a word\<close>
     apply transfer
-    apply (cases rule: length_cases [where ?'a = 'a])
-     apply auto
-       apply (metis even_take_bit_eq len_not_eq_0)
+    apply auto
+       apply (metis bit_ident drop_bit_eq_div drop_bit_half even_take_bit_eq even_two_times_div_two mod_div_trivial odd_two_times_div_two_succ take_bit_eq_mod)
       apply (metis even_take_bit_eq len_not_eq_0)
-    apply (metis (no_types, hide_lams) diff_add_cancel dvd_div_mult_self even_take_bit_eq mult_2_right take_bit_add take_bit_minus)
-    apply (metis bit_ident drop_bit_eq_div drop_bit_half even_take_bit_eq even_two_times_div_two mod_div_trivial odd_two_times_div_two_succ take_bit_eq_mod)
+     apply (metis even_take_bit_eq len_not_eq_0)
+    apply (metis (no_types, hide_lams) div_0 drop_bit_eq_div drop_bit_half dvd_mult_div_cancel even_take_bit_eq mod_div_trivial mod_eq_self_iff_div_eq_0 take_bit_eq_mod)
     done
   show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
     and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close>
@@ -598,6 +594,56 @@
     with rec [of a True] show ?case
       using bit_word_half_eq [of a True] by (simp add: ac_simps)
   qed
+  show \<open>0 div a = 0\<close>
+    for a :: \<open>'a word\<close>
+    by transfer simp
+  show \<open>a div 1 = a\<close>
+    for a :: \<open>'a word\<close>
+    by transfer simp
+  show \<open>a mod b div b = 0\<close>
+    for a b :: \<open>'a word\<close>
+    apply transfer
+    apply (simp add: take_bit_eq_mod)
+    apply (subst (3) mod_pos_pos_trivial [of _ \<open>2 ^ LENGTH('a)\<close>])
+      apply simp_all
+     apply (metis le_less mod_by_0 pos_mod_conj zero_less_numeral zero_less_power)
+    using pos_mod_bound [of \<open>2 ^ LENGTH('a)\<close>] apply simp
+  proof -
+    fix aa :: int and ba :: int
+    have f1: "\<And>i n. (i::int) mod 2 ^ n = 0 \<or> 0 < i mod 2 ^ n"
+      by (metis le_less take_bit_eq_mod take_bit_nonnegative)
+    have "(0::int) < 2 ^ len_of (TYPE('a)::'a itself) \<and> ba mod 2 ^ len_of (TYPE('a)::'a itself) \<noteq> 0 \<or> aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)"
+      by (metis (no_types) mod_by_0 unique_euclidean_semiring_numeral_class.pos_mod_bound zero_less_numeral zero_less_power)
+    then show "aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)"
+      using f1 by (meson le_less less_le_trans unique_euclidean_semiring_numeral_class.pos_mod_bound)
+  qed
+  show \<open>(1 + a) div 2 = a div 2\<close>
+    if \<open>even a\<close>
+    for a :: \<open>'a word\<close>
+    using that by transfer (auto dest: le_Suc_ex)
+  show "a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)"
+    for a :: "'a word" and m n :: nat
+    apply transfer
+    apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div)
+    apply (simp add: drop_bit_take_bit)
+    done
+  show "a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n"
+    for a :: "'a word" and m n :: nat
+    apply transfer
+    apply (auto simp flip: take_bit_eq_mod)
+    apply (simp add: ac_simps)
+    done
+  show \<open>a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n - m) * 2 ^ m\<close>
+    if \<open>m \<le> n\<close> for a :: "'a word" and m n :: nat
+    using that apply transfer
+    apply (auto simp flip: take_bit_eq_mod)
+           apply (auto simp flip: push_bit_eq_mult simp add: push_bit_take_bit split: split_min_lin)
+    done
+  show \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
+    for a :: "'a word" and m n :: nat
+    apply transfer
+    apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin)
+    done
 qed
 
 instantiation word :: (len) semiring_bit_shifts