src/HOL/Word/Bit_Representation.thy

   unfolding bin_rest_def Bit_def
   by (cases b, simp_all)
 
 lemma bin_last_BIT [simp]: "bin_last (x BIT b) = b"
   unfolding bin_last_def Bit_def
-  by (cases b, simp_all add: z1pmod2)
+  by (cases b) simp_all
 
 lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c"
   apply (auto simp add: Bit_def)
   apply arith
   apply arith

   by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps)
 
 lemma B_mod_2': 
   "X = 2 ==> (w BIT True) mod X = 1 & (w BIT False) mod X = 0"
   apply (simp (no_asm) only: Bit_B0 Bit_B1)
-  apply (simp add: z1pmod2)
+  apply simp
   done
 
 lemma bin_ex_rl: "EX w b. w BIT b = bin"
   by (metis bin_rl_simp)
 

   done
 
 primrec bin_nth where
   Z: "bin_nth w 0 \<longleftrightarrow> bin_last w"
   | Suc: "bin_nth w (Suc n) \<longleftrightarrow> bin_nth (bin_rest w) n"
-
-find_theorems "bin_rest _ = _"
 
 lemma bin_abs_lem:
   "bin = (w BIT b) ==> bin ~= -1 --> bin ~= 0 -->
     nat (abs w) < nat (abs bin)"
   apply clarsimp

   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 mod_2_neq_1_eq_eq_0)
+  apply (simp add: bin_last_def bin_rest_def Bit_def)
   apply (clarsimp simp: mod_mult_mult1 [symmetric] 
          zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
   apply (rule trans [symmetric, OF _ emep1])
      apply auto
   apply (auto simp: even_def)