diff -r 7759f1766189 -r 50c715579715 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -308,17 +308,12 @@
 
 lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n"
   apply (induct n arbitrary: w)
-   apply simp
-   apply (subst mod_add_left_eq)
-   apply (simp add: bin_last_def)
-   apply arith
-  apply (simp add: bin_last_def bin_rest_def Bit_def)
-  apply (clarsimp simp: mod_mult_mult1 [symmetric] 
-         mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
-  apply (rule trans [symmetric, OF _ emep1])
-  apply auto
+   apply (auto simp add: bin_last_odd bin_rest_def Bit_def elim!: evenE oddE)
+   apply (smt pos_zmod_mult_2 zle2p)
+  apply (simp add: mult_mod_right)
   done
 
+
 subsection "Simplifications for (s)bintrunc"
 
 lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
@@ -647,28 +642,6 @@
   "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
   unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
 
-lemmas zmod_uminus' = zminus_zmod [where m=c] for c
-lemmas zpower_zmod' = power_mod [where b=c and n=k] for c k
-
-lemmas brdmod1s' [symmetric] =
-  mod_add_left_eq mod_add_right_eq
-  mod_diff_left_eq mod_diff_right_eq
-  mod_mult_left_eq mod_mult_right_eq
-
-lemmas brdmods' [symmetric] = 
-  zpower_zmod' [symmetric]
-  trans [OF mod_add_left_eq mod_add_right_eq] 
-  trans [OF mod_diff_left_eq mod_diff_right_eq] 
-  trans [OF mod_mult_right_eq mod_mult_left_eq] 
-  zmod_uminus' [symmetric]
-  mod_add_left_eq [where b = "1::int"]
-  mod_diff_left_eq [where b = "1::int"]
-
-lemmas bintr_arith1s =
-  brdmod1s' [where c="2^n::int", folded bintrunc_mod2p] for n
-lemmas bintr_ariths =
-  brdmods' [where c="2^n::int", folded bintrunc_mod2p] for n
-
 lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p]
 
 lemma bintr_ge0: "0 \<le> bintrunc n w"