src/HOL/Word/WordShift.thy

 subsection "Bit shifting"
 
 lemma shiftl1_number [simp] :
   "shiftl1 (number_of w) = number_of (w BIT bit.B0)"
   apply (unfold shiftl1_def word_number_of_def)
-  apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
+  apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm
+              del: BIT_simps)
   apply (subst refl [THEN bintrunc_BIT_I, symmetric])
   apply (subst bintrunc_bintrunc_min)
   apply simp
   done
 

 
 (* note - the following results use 'a :: len word < number_ring *)
 
 lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
   apply (simp add: shiftl1_def_u)
-  apply (simp only:  double_number_of_BIT [symmetric])
+  apply (simp only:  double_number_of_Bit0 [symmetric])
   apply simp
   done
 
 lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
   apply (simp add: shiftl1_def_u)
-  apply (simp only: double_number_of_BIT [symmetric])
+  apply (simp only: double_number_of_Bit0 [symmetric])
   apply simp
   done
 
 lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
   unfolding shiftl_def