src/HOL/Set_Interval.thy

 
 context unique_euclidean_semiring_with_bit_shifts
 begin
 
 lemma take_bit_sum:
-  "take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (odd (drop_bit k a))))"
+  "take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))"
   for n :: nat
 proof (induction n arbitrary: a)
   case 0
   then show ?case
     by simp
 next
   case (Suc n)
-  have "(\<Sum>k = 0..<Suc n. push_bit k (of_bool (odd (drop_bit k a)))) = 
-    of_bool (odd a) + (\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (odd (drop_bit k a))))"
+  have "(\<Sum>k = 0..<Suc n. push_bit k (of_bool (bit a k))) = 
+    of_bool (odd a) + (\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (bit a k)))"
     by (simp add: sum.atLeast_Suc_lessThan ac_simps)
-  also have "(\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (odd (drop_bit k a))))
-    = (\<Sum>k = 0..<n. push_bit k (of_bool (odd (drop_bit k (a div 2))))) * 2"
-    by (simp only: sum.atLeast_Suc_lessThan_Suc_shift) (simp add: sum_distrib_right push_bit_double)
+  also have "(\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (bit a k)))
+    = (\<Sum>k = 0..<n. push_bit k (of_bool (bit (a div 2) k))) * 2"
+    by (simp only: sum.atLeast_Suc_lessThan_Suc_shift) (simp add: sum_distrib_right push_bit_double drop_bit_Suc bit_Suc)
   finally show ?case
-    using Suc [of "a div 2"] by (simp add: ac_simps)
+    using Suc [of "a div 2"] by (simp add: ac_simps take_bit_Suc)
 qed
 
 end