src/HOL/ex/Bit_Operations.thy

   than \<open>+\<close> and \<open>-\<close>.
   For the sake of code generation
   the operations \<^const>\<open>and\<close>, \<^const>\<open>or\<close> and \<^const>\<open>xor\<close>
   are specified as definitional class operations.
 \<close>
-
-lemma stable_imp_drop_eq:
-  \<open>drop_bit n a = a\<close> if \<open>a div 2 = a\<close>
-  by (induction n) (simp_all add: that)
 
 sublocale "and": semilattice \<open>(AND)\<close>
   by standard (auto simp add: bit_eq_iff bit_and_iff)
 
 sublocale or: semilattice_neutr \<open>(OR)\<close> 0

 proof (rule bit_eqI)
   fix m
   assume *: \<open>2 ^ m \<noteq> 0\<close>
   then show \<open>bit (set_bit 0 a) m = bit (1 + 2 * (a div 2)) m\<close>
     by (simp add: bit_set_bit_iff bit_double_iff even_bit_succ_iff)
-      (cases m, simp_all)
+      (cases m, simp_all add: bit_Suc)
 qed
 
 lemma set_bit_Suc [simp]:
   \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close>
 proof (rule bit_eqI)

     with * have \<open>2 ^ m \<noteq> 0\<close>
       using mult_2 by auto
     show ?thesis
       by (cases a rule: parity_cases)
         (simp_all add: bit_set_bit_iff bit_double_iff even_bit_succ_iff *,
-        simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close>)
+        simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close> bit_Suc)
   qed
 qed
 
 lemma unset_bit_0 [simp]:
   \<open>unset_bit 0 a = 2 * (a div 2)\<close>
 proof (rule bit_eqI)
   fix m
   assume *: \<open>2 ^ m \<noteq> 0\<close>
   then show \<open>bit (unset_bit 0 a) m = bit (2 * (a div 2)) m\<close>
     by (simp add: bit_unset_bit_iff bit_double_iff)
-      (cases m, simp_all)
+      (cases m, simp_all add: bit_Suc)
 qed
 
 lemma unset_bit_Suc [simp]:
   \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
 proof (rule bit_eqI)

   next
     case (Suc m)
     show ?thesis
       by (cases a rule: parity_cases)
         (simp_all add: bit_unset_bit_iff bit_double_iff even_bit_succ_iff *,
-         simp_all add: Suc)
+         simp_all add: Suc bit_Suc)
   qed
 qed
 
 lemma flip_bit_0 [simp]:
   \<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
 proof (rule bit_eqI)
   fix m
   assume *: \<open>2 ^ m \<noteq> 0\<close>
   then show \<open>bit (flip_bit 0 a) m = bit (of_bool (even a) + 2 * (a div 2)) m\<close>
     by (simp add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff)
-      (cases m, simp_all)
+      (cases m, simp_all add: bit_Suc)
 qed
 
 lemma flip_bit_Suc [simp]:
   \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
 proof (rule bit_eqI)

     with * have \<open>2 ^ m \<noteq> 0\<close>
       using mult_2 by auto
     show ?thesis
       by (cases a rule: parity_cases)
         (simp_all add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff,
-        simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close>)
+        simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close> bit_Suc)
   qed
 qed
 
 end
 

   then show ?case
     by (simp add: rec [of m n])
 next
   case (Suc n)
   then show ?case
-    by (simp add: rec [of m n])
+    by (simp add: rec [of m n] bit_Suc)
 qed
 
 sublocale abel_semigroup F
   by standard (simp_all add: Parity.bit_eq_iff bit_eq_iff ac_simps)
 

   then show ?case
     by (simp add: rec [of k l])
 next
   case (Suc n)
   then show ?case
-    by (simp add: rec [of k l])
+    by (simp add: rec [of k l] bit_Suc)
 qed
 
 sublocale abel_semigroup F
   by standard (simp_all add: Parity.bit_eq_iff bit_eq_iff ac_simps)
 

   by (simp add: not_int_def)
 
 lemma bit_not_iff_int:
   \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
     for k :: int
-  by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int)
+  by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int bit_Suc)
 
 instance proof
   fix k l :: int and n :: nat
   show \<open>- k = NOT (k - 1)\<close>
     by (simp add: not_int_def)